mlw_typing: parse type declarations

src/whyml/mlw_decl.ml

@@ -26,7 +26,7 @@ open Decl
 open Mlw_ty
 open Mlw_expr
 
-type ps_ls = { ps: psymbol; ls: lsymbol }
+type ps_ls = { ps : psymbol; ls : lsymbol }
 
 type pconstructor = ps_ls * ps_ls option list
 

src/whyml/mlw_decl.mli

@@ -26,7 +26,7 @@ open Mlw_expr
 
 (** {2 Type declaration} *)
 
-type ps_ls = private { ps: psymbol; ls: lsymbol }
+type ps_ls = private { ps : psymbol; ls : lsymbol }
 
 type pconstructor = ps_ls * ps_ls option list
 
@@ -66,4 +66,4 @@ type known_map = pdecl Mid.t
 
 val known_id : known_map -> ident -> unit
 val known_add_decl : Decl.known_map -> known_map -> pdecl -> known_map
-val merge_known: known_map -> known_map -> known_map
+val merge_known : known_map -> known_map -> known_map

src/whyml/mlw_ty.ml

@@ -26,10 +26,12 @@ open Term
 (** value types (w/o effects) *)
 
 type itysymbol = {
-  its_pure  : tysymbol;
-  its_args  : tvsymbol list;
-  its_regs  : region   list;
-  its_def   : ity option;
+  its_pure : tysymbol;
+  its_args : tvsymbol list;
+  its_regs : region   list;
+  its_def  : ity option;
+  its_abst : bool;
+  its_priv : bool;
 }
 
 and ity = {
@@ -43,9 +45,9 @@ and ity_node =
   | Ityapp of itysymbol * ity list * region list
 
 and region = {
-  reg_name : ident;
-  reg_ity  : ity;
-  reg_ghost: bool;
+  reg_name  : ident;
+  reg_ity   : ity;
+  reg_ghost : bool;
 }
 
 (** regions *)
@@ -181,10 +183,11 @@ let ity_v_any prv prr ity =
 let ity_full_inst mv mr ity =
   ity_v_map (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) ity
 
-let ity_freevars s ity = ity_v_fold (fun s v -> Stv.add v s) Util.const s ity
+let ity_freevars = ity_v_fold (fun s v -> Stv.add v s) Util.const
+let ity_topregions = ity_v_fold Util.const (fun s r -> Sreg.add r s)
 
-let ity_closed ity = ity_v_all Util.ffalse Util.ttrue ity
-let ity_pure ity = ity_v_all Util.ttrue Util.ffalse ity
+let ity_closed = ity_v_all Util.ffalse Util.ttrue
+let ity_pure = ity_v_all Util.ttrue Util.ffalse
 
 (* smart constructors *)
 
@@ -202,8 +205,8 @@ let ity_equal_check ty1 ty2 =
   if not (ity_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
 
 type ity_subst = {
-  ity_subst_tv:  ity Mtv.t;
-  ity_subst_reg: region Mreg.t;
+  ity_subst_tv  : ity Mtv.t;
+  ity_subst_reg : region Mreg.t;
 }
 
 let ity_subst_empty = {
@@ -258,27 +261,58 @@ let rec ity_of_ty ty = match ty.ty_node with
   | Tyvar v -> ity_var v
   | Tyapp (s,tl) -> ity_pur s (List.map ity_of_ty tl)
 
+let rec ity_inst_fresh mv mr ity = match ity.ity_node with
+  | Ityvar v ->
+      mr, Mtv.find v mv
+  | Itypur (s,tl) ->
+      let mr,tl = Util.map_fold_left (ity_inst_fresh mv) mr tl in
+      mr, ity_pur s tl
+  | Ityapp (s,tl,rl) ->
+      let mr,tl = Util.map_fold_left (ity_inst_fresh mv) mr tl in
+      let mr,rl = Util.map_fold_left (reg_refresh mv) mr rl in
+      mr, ity_app s tl rl
+
+and reg_refresh mv mr r = match Mreg.find_opt r mr with
+  | Some r ->
+      mr, r
+  | None ->
+      let mr,ity = ity_inst_fresh mv mr r.reg_ity in
+      let id = id_clone r.reg_name and ghost = r.reg_ghost in
+      let reg = create_region id ~ghost ity in
+      Mreg.add r reg mr, reg
+
+let ity_app_fresh s tl =
+  (* type variable map *)
+  let add m v t = Mtv.add v t m in
+  let mv = try List.fold_left2 add Mtv.empty s.its_args tl
+    with Invalid_argument _ ->
+      raise (BadItyArity (s, List.length s.its_args, List.length tl)) in
+  (* refresh regions *)
+  let mr,rl = Util.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
+  (* every external region in def is guaranteed to be in mr *)
+  match s.its_def with
+  | Some ity -> ity_full_inst mv mr ity
+  | None -> ity_app s tl rl
+
 let ity_app s tl rl =
-  let tll = List.length tl in
-  let rll = List.length rl in
-  let stl = List.length s.its_args in
-  let srl = List.length s.its_regs in
-  if tll <> stl then raise (BadItyArity (s,stl,tll));
-  if rll <> srl then raise (BadRegArity (s,srl,rll));
+  (* type variable map *)
   let add m v t = Mtv.add v t m in
-  let mv = List.fold_left2 add Mtv.empty s.its_args tl in
+  let mv = try List.fold_left2 add Mtv.empty s.its_args tl
+    with Invalid_argument _ ->
+      raise (BadItyArity (s, List.length s.its_args, List.length tl)) in
+  (* region map *)
   let add m v r = Mreg.add v r m in
-  let mr = List.fold_left2 add Mreg.empty s.its_regs rl in
+  let mr = try List.fold_left2 add Mreg.empty s.its_regs rl
+    with Invalid_argument _ ->
+      raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
   (* check that region types do unify *)
   let sub = { ity_subst_tv = mv; ity_subst_reg = mr } in
   let rmatch sub r1 r2 = ity_match sub r1.reg_ity r2.reg_ity in
   ignore (List.fold_left2 rmatch sub s.its_regs rl);
   (* to instantiate def, mv and mr are enough *)
   match s.its_def with
-  | Some ity ->
-      ity_full_inst mv mr ity
-  | None ->
-      ity_app s tl rl
+  | Some ity -> ity_full_inst mv mr ity
+  | None -> ity_app s tl rl
 
 let ity_pur s tl = match s.ts_def with
   | Some ty ->
@@ -288,7 +322,7 @@ let ity_pur s tl = match s.ts_def with
   | None ->
       ity_pur s tl
 
-let create_itysymbol name args regs def (* model *) =
+let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
   let puredef = option_map ty_of_ity def in
   let purets = create_tysymbol name args puredef in
   (* all regions *)
@@ -302,19 +336,20 @@ let create_itysymbol name args regs def (* model *) =
   (* all regions in [def] must be in [regs] *)
   let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
   ignore (option_map (ity_v_all Util.ttrue check) def);
-  (* if a type is a model alias, expand everything on the RHS *)
-  (* let def = if model then option_map (ity_mod purets) def else def in *)
+  (* if a type is an alias then abst and priv will be ignored *)
   { its_pure  = purets;
     its_args  = args;
     its_regs  = regs;
-    its_def   = def; }
+    its_def   = def;
+    its_abst  = abst;
+    its_priv  = priv }
 
 (** computation types (with effects) *)
 
 (* exception symbols *)
 type xsymbol = {
   xs_name : ident;
-  xs_ity:   ity; (* closed and pure *)
+  xs_ity  : ity; (* closed and pure *)
 }
 
 exception PolymorphicException of ident * ity
@@ -330,24 +365,25 @@ module Exn = StructMake (struct
   type t = xsymbol
   let tag xs = Hashweak.tag_hash xs.xs_name.id_tag
 end)
+
 module Sexn = Exn.S
 module Mexn = Exn.M
 
 (* effects *)
 type effect = {
-  eff_reads:   Sreg.t;
-  eff_writes:  Sreg.t;
-  eff_erases:  Sreg.t;
-  eff_renames: region Mreg.t; (* if r1->r2 then r1 appears in ty(r2) *)
-  eff_raises:  Sexn.t;
+  eff_reads   : Sreg.t;
+  eff_writes  : Sreg.t;
+  eff_erases  : Sreg.t;
+  eff_renames : region Mreg.t; (* if r1->r2 then r1 appears in ty(r2) *)
+  eff_raises  : Sexn.t;
 }
 
 let eff_empty = {
-  eff_reads = Sreg.empty;
-  eff_writes = Sreg.empty;
-  eff_erases = Sreg.empty;
+  eff_reads   = Sreg.empty;
+  eff_writes  = Sreg.empty;
+  eff_erases  = Sreg.empty;
   eff_renames = Mreg.empty;
-  eff_raises = Sexn.empty
+  eff_raises  = Sexn.empty
 }
 
 let eff_union x y =
@@ -372,10 +408,10 @@ let eff_remove_raise xs e = { e with eff_raises = Sexn.remove xs e.eff_raises }
 
 (* program variables *)
 type pvsymbol = {
-  pv_vs:      vsymbol;
-  pv_ity:     ity;
-  pv_ghost:   bool;
-  pv_mutable: region option;
+  pv_vs      : vsymbol;
+  pv_ity     : ity;
+  pv_ghost   : bool;
+  pv_mutable : region option;
 }
 
 exception InvalidPVsymbol of ident
@@ -403,11 +439,11 @@ type vty =
 
 (* computation types *)
 and cty = {
-  c_pre: term;
-  c_vty: vty;
-  c_eff: effect;
-  c_post: term;
-  c_xpost: xpost;
+  c_pre   : term;
+  c_vty   : vty;
+  c_eff   : effect;
+  c_post  : term;
+  c_xpost : xpost;
 }
 
 and xpost = (pvsymbol * term) Mexn.t

src/whyml/mlw_ty.mli

@@ -30,6 +30,8 @@ type itysymbol = private {
   its_args : tvsymbol list;
   its_regs : region   list;
   its_def  : ity option;
+  its_abst : bool;
+  its_priv : bool;
 }
 
 and ity = private {
@@ -80,13 +82,14 @@ exception InvalidRegion of region
 
 val create_region : preid -> ?ghost:bool -> ity -> region
 
-val create_itysymbol :
-  preid -> tvsymbol list -> region list -> ity option -> itysymbol
+val create_itysymbol : preid -> ?abst:bool -> ?priv:bool ->
+  tvsymbol list -> region list -> ity option -> itysymbol
 
 val ity_var : tvsymbol -> ity
 val ity_pur : tysymbol -> ity list -> ity
 
 val ity_app : itysymbol -> ity list -> region list -> ity
+val ity_app_fresh : itysymbol -> ity list -> ity
 
 (* all aliases expanded, all regions removed *)
 val ty_of_ity : ity -> ty
@@ -124,18 +127,19 @@ val ity_s_any : (itysymbol -> bool) -> ity -> bool
 *)
 
 val ity_freevars : Stv.t -> ity -> Stv.t
+val ity_topregions : Sreg.t -> ity -> Sreg.t
 val ity_closed : ity -> bool
-val ity_pure: ity -> bool
+val ity_pure : ity -> bool
 
 exception RegionMismatch of region * region
 exception TypeMismatch of ity * ity
 
 type ity_subst = private {
-  ity_subst_tv:  ity Mtv.t;
-  ity_subst_reg: region Mreg.t;
+  ity_subst_tv  : ity Mtv.t;
+  ity_subst_reg : region Mreg.t;
 }
 
-val ity_subst_empty: ity_subst
+val ity_subst_empty : ity_subst
 
 val ity_match : ity_subst -> ity -> ity -> ity_subst
 
@@ -146,40 +150,42 @@ val ity_equal_check : ity -> ity -> unit
 (* exception symbols *)
 type xsymbol = private {
   xs_name : ident;
-  xs_ity:   ity; (* closed and pure *)
+  xs_ity  : ity; (* closed and pure *)
 }
 
-val create_xsymbol: preid -> ity -> xsymbol
+val create_xsymbol : preid -> ity -> xsymbol
 
 module Mexn: Map.S with type key = xsymbol
 module Sexn: Mexn.Set
 
 (* effects *)
 type effect = private {
-  eff_reads:   Sreg.t;
-  eff_writes:  Sreg.t;
-  eff_erases:  Sreg.t;
-  eff_renames: region Mreg.t; (* if r1->r2 then r1 appears in ty(r2) *)
-  eff_raises:  Sexn.t;
+  eff_reads   : Sreg.t;
+  eff_writes  : Sreg.t;
+  eff_erases  : Sreg.t;
+  eff_renames : region Mreg.t; (* if r1->r2 then r1 appears in ty(r2) *)
+  eff_raises  : Sexn.t;
 }
 
-val eff_empty: effect
-val eff_union: effect -> effect -> effect
-val eff_read: region -> effect
-val eff_write: region -> effect
-val eff_erase: region -> effect
-val eff_raise: xsymbol -> effect
-val eff_remove_raise: xsymbol -> effect -> effect
+val eff_empty : effect
+val eff_union : effect -> effect -> effect
+
+val eff_read  : region -> effect
+val eff_write : region -> effect
+val eff_erase : region -> effect
+val eff_raise : xsymbol -> effect
+
+val eff_remove_raise : xsymbol -> effect -> effect
 
 (* program variables *)
 type pvsymbol = private {
-  pv_vs:      vsymbol;
-  pv_ity:     ity;
-  pv_ghost:   bool;
-  pv_mutable: region option;
+  pv_vs      : vsymbol;
+  pv_ity     : ity;
+  pv_ghost   : bool;
+  pv_mutable : region option;
 }
 
-val create_pvsymbol: preid -> ?mut:region -> ?ghost:bool -> ity -> pvsymbol
+val create_pvsymbol : preid -> ?mut:region -> ?ghost:bool -> ity -> pvsymbol
 
 val pv_equal : pvsymbol -> pvsymbol -> bool
 
@@ -190,19 +196,19 @@ type vty = private
 
 (* computation types *)
 and cty = private {
-  c_pre: term;
-  c_vty: vty;
-  c_eff: effect;
-  c_post: term;
-  c_xpost: xpost;
+  c_pre   : term;
+  c_vty   : vty;
+  c_eff   : effect;
+  c_post  : term;
+  c_xpost : xpost;
 }
 
 and xpost = (pvsymbol * term) Mexn.t
 
 (* smart constructors *)
-val create_cty:
+val create_cty :
   ?pre:term -> ?post:term -> ?xpost:xpost -> ?effect:effect -> vty -> cty
 
-val vty_value: pvsymbol -> vty
-val vty_arrow: pvsymbol -> cty -> vty
+val vty_value : pvsymbol -> vty
+val vty_arrow : pvsymbol -> cty -> vty
 

src/whyml/mlw_typing.ml

@@ -23,14 +23,306 @@ open Ident
 open Theory
 open Env
 open Ptree
+open Mlw_ty
+open Mlw_expr
+open Mlw_decl
 open Mlw_module
 
+(** errors *)
+
+exception DuplicateVar of string
+exception DuplicateTypeVar of string
+(*
+exception PredicateExpected
+exception TermExpected
+exception FSymExpected of lsymbol
+exception PSymExpected of lsymbol
+exception ClashTheory of string
+exception UnboundTheory of qualid
+exception UnboundType of string list
+*)
+exception UnboundTypeVar of string
+exception UnboundSymbol of string list
+
+let error = Loc.error
+let errorm = Loc.errorm
+
+let rec print_qualid fmt = function
+  | Qident s -> Format.fprintf fmt "%s" s.id
+  | Qdot (m, s) -> Format.fprintf fmt "%a.%s" print_qualid m s.id
+
+let () = Exn_printer.register (fun fmt e -> match e with
+  | DuplicateTypeVar s ->
+      Format.fprintf fmt "Duplicate type parameter %s" s
+  | DuplicateVar s ->
+      Format.fprintf fmt "Duplicate variable %s" s
+(*
+  | PredicateExpected ->
+      Format.fprintf fmt "syntax error: predicate expected"
+  | TermExpected ->
+      Format.fprintf fmt "syntax error: term expected"
+  | FSymExpected ls ->
+      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
+  | PSymExpected ls ->
+      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
+  | ClashTheory s ->
+      Format.fprintf fmt "Clash with previous theory %s" s
+  | UnboundTheory q ->
+      Format.fprintf fmt "unbound theory %a" print_qualid q
+  | UnboundType sl ->
+      Format.fprintf fmt "Unbound type '%a'"
+        (Pp.print_list Pp.dot Pp.pp_print_string) sl
+*)
+  | UnboundTypeVar s ->
+      Format.fprintf fmt "unbound type variable '%s" s
+  | UnboundSymbol sl ->
+      Format.fprintf fmt "Unbound symbol '%a'"
+        (Pp.print_list Pp.dot Format.pp_print_string) sl
+  | _ -> raise e)
+
+(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
+
+(** Type declaration *)
+
+type tys = ProgTS of itysymbol | PureTS of Ty.tysymbol
+
+let find_tysymbol q uc =
+  let loc = Typing.qloc q in
+  let sl = Typing.string_list_of_qualid [] q in
+  try ProgTS (ns_find_it (get_namespace uc) sl)
+  with Not_found ->
+  try PureTS (ns_find_ts (Theory.get_namespace (get_theory uc)) sl)
+  with Not_found -> error ~loc (UnboundSymbol sl)
+
+let add_types uc tdl =
+  let add m d =
+    let id = d.td_ident.id in
+    Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d m in
+  let def = List.fold_left add Mstr.empty tdl in
+
+  (* detect cycles *)
+
+  let rec cyc_visit x d seen = match Mstr.find_opt x seen with
+    | Some true -> seen
+    | Some false -> errorm ~loc:d.td_loc "Cyclic type definition"
+    | None ->
+        let ts_seen seen = function
+          | Qident { id = x } ->
+              begin try cyc_visit x (Mstr.find x def) seen
+              with Not_found -> seen end
+          | _ -> seen in
+        let rec check seen = function
+          | PPTtyvar _ -> seen
+          | PPTtyapp (tyl,q) -> List.fold_left check (ts_seen seen q) tyl
+          | PPTtuple tyl -> List.fold_left check seen tyl in
+        let seen = match d.td_def with
+          | TDabstract | TDalgebraic _ | TDrecord _ -> seen
+          | TDalias ty -> check (Mstr.add x false seen) ty in
+        Mstr.add x true seen in
+  ignore (Mstr.fold cyc_visit def Mstr.empty);
+
+  (* detect mutable types *)
+
+  let mutables = Hashtbl.create 5 in
+  let rec mut_visit x =
+    try Hashtbl.find mutables x
+    with Not_found ->
+      let ts_mut = function
+        | Qident { id = x } when Mstr.mem x def -> mut_visit x
+        | q ->
+            begin match find_tysymbol q uc with
+              | ProgTS s -> s.its_regs <> []
+              | PureTS _ -> false end in
+      let rec check = function
+        | PPTtyvar _ -> false
+        | PPTtyapp (tyl,q) -> ts_mut q || List.exists check tyl
+        | PPTtuple tyl -> List.exists check tyl in
+      Hashtbl.replace mutables x false;
+      let mut = match (Mstr.find x def).td_def with
+        | TDabstract -> false
+        | TDalias ty -> check ty
+        | TDalgebraic csl ->
+            let proj (_,pty) = check pty in
+            List.exists (fun (_,_,l) -> List.exists proj l) csl
+        | TDrecord fl ->
+            let field f = f.f_mutable || check f.f_pty in
+            List.exists field fl in
+      Hashtbl.replace mutables x mut;
+      mut
+  in
+  Mstr.iter (fun x _ -> ignore (mut_visit x)) def;
+
+  (* create type symbols and predefinitions for mutable types *)
+
+  let tysymbols = Hashtbl.create 5 in
+  let predefs = Hashtbl.create 5 in
+  let rec its_visit x =
+    try match Hashtbl.find tysymbols x with
+      | Some ts -> ts
+      | None ->
+          let loc = (Mstr.find x def).td_loc in
+          errorm ~loc "Mutable type in a recursive type definition"
+    with Not_found ->
+      let d = Mstr.find x def in
+      let add_tv acc id =
+        let e = Loc.Located (id.id_loc, DuplicateTypeVar id.id) in
+        let tv = Ty.create_tvsymbol (Denv.create_user_id id) in
+        Mstr.add_new e id.id tv acc in
+      let vars = List.fold_left add_tv Mstr.empty d.td_params in
+      let vl = List.map (fun id -> Mstr.find id.id vars) d.td_params in
+      let id = Denv.create_user_id d.td_ident in
+      let abst = d.td_vis = Abstract in
+      let priv = d.td_vis = Private in
+      Hashtbl.add tysymbols x None;
+      let get_ts = function
+        | Qident { id = x } when Mstr.mem x def -> ProgTS (its_visit x)
+        | q -> find_tysymbol q uc
+      in
+      let rec parse = function
+        | PPTtyvar { id = v ; id_loc = loc } ->
+            let e = Loc.Located (loc, UnboundTypeVar v) in
+            ity_var (Mstr.find_exn e v vars)
+        | PPTtyapp (tyl,q) ->
+            let tyl = List.map parse tyl in
+            begin match get_ts q with
+              | PureTS ts -> Loc.try2 (Typing.qloc q) ity_pur ts tyl
+              | ProgTS ts -> Loc.try2 (Typing.qloc q) ity_app_fresh ts tyl
+            end
+        | PPTtuple tyl ->
+            let ts = Ty.ts_tuple (List.length tyl) in
+            ity_pur ts (List.map parse tyl)
+      in
+      let ts = match d.td_def with
+        | TDalias ty ->
+            let def = parse ty in
+            let s = ity_topregions Sreg.empty def in
+            create_itysymbol id ~abst ~priv vl (Sreg.elements s) (Some def)
+        | TDalgebraic csl when Hashtbl.mem mutables x ->
+            let projs = Hashtbl.create 5 in
+            (* to check projections' types we must fix the tyvars *)
+            let add s v = let t = ity_var v in ity_match s t t in
+            let sbs = List.fold_left add ity_subst_empty vl in
+            let mk_proj s (id,pty) =
+              let ity = parse pty in
+              match id with
+                | None ->
+                    let pv = create_pvsymbol (id_fresh "pj") ity in
+                    ity_topregions s ity, (pv, false)
+                | Some id ->
+                    try
+                      let pv = Hashtbl.find projs id.id in
+                      ignore (ity_match sbs pv.pv_ity ity);
+                      s, (pv, true)
+                    with Not_found ->
+                      let pv = create_pvsymbol (Denv.create_user_id id) ity in
+                      Hashtbl.replace projs id.id pv;
+                      ity_topregions s ity, (pv, true)
+            in
+            let mk_constr s (_loc,cid,pjl) =
+              let s,pjl = Util.map_fold_left mk_proj s pjl in
+              s, (Denv.create_user_id cid, pjl)
+            in
+            let s,def = Util.map_fold_left mk_constr Sreg.empty csl in
+            Hashtbl.replace predefs x (PITalgebraic def);
+            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
+        | TDrecord fl when Hashtbl.mem mutables x ->
+            let mk_field s f =
+              let ghost = f.f_ghost in
+              let ity = parse f.f_pty in
+              let fid = Denv.create_user_id f.f_ident in
+              let s,mut = if f.f_mutable then
+                let r = create_region fid ~ghost ity in
+                Sreg.add r s, Some r
+              else
+                ity_topregions s ity, None
+              in
+              s, (create_pvsymbol fid ?mut ~ghost ity, true)
+            in
+            let s,pjl = Util.map_fold_left mk_field Sreg.empty fl in
+            let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
+            let def = PITalgebraic [Denv.create_user_id cid, pjl] in
+            Hashtbl.replace