Mlw: type definitions - fixes and improvements

src/mlw/ity.ml

@@ -1259,7 +1259,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
       "Unbound region %a" print_reg r
   | ImpureField ity -> fprintf fmt
       "Field type %a is mutable, it cannot be used in a type which is \
-        private, recursive, or has an invariant" print_ity_full ity
+        private, recursive, or has an invariant" print_ity ity
 (*
   | UnboundException xs -> fprintf fmt
       "This function raises %a but does not specify a post-condition for it"

src/mlw/pdecl.ml

@@ -71,7 +71,6 @@ let create_semi_constructor id s fl pjl invl =
   create_rsymbol id c
 
 let create_flat_record_decl id args priv mut fldl invl =
-  (* TODO: replace Invalid_argument by well-located error messages *)
   let exn = Invalid_argument "Mdecl.create_flat_record_decl" in
   let cid = id_fresh ?loc:id.pre_loc ("mk " ^ id.pre_name) in
   let add_fd fs (fm,fd) = Mpv.add_new exn fd fm fs in
@@ -118,7 +117,6 @@ let create_rec_record_decl s fldl =
   mk_itd s pjl [cs] []
 
 let create_variant_decl get_its cl =
-  (* TODO: replace Invalid_argument by well-located error messages *)
   let exn = Invalid_argument "Mdecl.create_variant_decl" in
   let pjl, fds = match cl with
     | cs::cl ->
@@ -299,14 +297,32 @@ let mk_decl = let r = ref 0 in fun node pure ->
     pd_tag  = (incr r; !r) }
 
 let create_type_decl dl =
-  let add_itd ({itd_its = s} as itd) (abst,defn,proj) =
+  let add_itd ({itd_its = s} as itd) (abst,defn,rest) =
     match itd.itd_fields, itd.itd_constructors with
-    | fl, ([{rs_logic = RLnone}]|[]) ->
+    | [], [] when s.its_def <> None ->
+        abst, defn, create_ty_decl s.its_ts :: rest
+    | fl, _ when itd.itd_invariant <> [] ->
+        let {id_string = nm; id_loc = loc} = s.its_ts.ts_name in
+        let u = create_vsymbol (id_fresh "self")
+          (ty_app s.its_ts (List.map ty_var s.its_ts.ts_args)) in
+        let t = [t_var u] in
+        let get_ld s (ldd,sbs) = match s.rs_logic, s.rs_field with
+          | RLls s, Some v ->
+              create_param_decl s :: ldd,
+              Mvs.add v.pv_vs (t_app_infer s t) sbs
+          | _ -> assert false in
+        let proj, sbs = List.fold_right get_ld fl ([],Mvs.empty) in
+        let pr = create_prsymbol (id_fresh ?loc ("inv " ^ nm)) in
+        let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
+        let inv = t_forall_close [u] [] inv in
+        let inv = create_prop_decl Paxiom pr inv in
+        create_ty_decl s.its_ts :: abst, defn, proj @ inv :: rest
+    | fl, [] ->
         let get_ld s ldd = match s.rs_logic with
-          | RLls s -> create_param_decl s :: ldd | _ -> assert false in
-        (* TODO: add axioms for the invariants *)
-        let proj = List.fold_right get_ld fl proj in
-        create_ty_decl s.its_ts :: abst, defn, proj
+          | RLls s -> create_param_decl s :: ldd
+          | _ -> assert false in
+        let rest = List.fold_right get_ld fl rest in
+        create_ty_decl s.its_ts :: abst, defn, rest
     | fl, cl ->
         let add s f = Mpv.add (Opt.get f.rs_field) f s in
         let mf = List.fold_left add Mpv.empty fl in
@@ -316,10 +332,10 @@ let create_type_decl dl =
         let get_cs s = match s.rs_logic with
           | RLls cs -> cs, List.map get_pj s.rs_cty.cty_args
           | _ -> assert false in
-        abst, (s.its_ts, List.map get_cs cl) :: defn, proj in
-  let abst,defn,proj = List.fold_right add_itd dl ([],[],[]) in
+        abst, (s.its_ts, List.map get_cs cl) :: defn, rest in
+  let abst,defn,rest = List.fold_right add_itd dl ([],[],[]) in
   let defn = if defn = [] then [] else [create_data_decl defn] in
-  mk_decl (PDtype dl) (abst @ defn @ proj)
+  mk_decl (PDtype dl) (abst @ defn @ rest)
 
 let create_let_decl ld =
   let ls_of_rs s dl = match s.rs_logic with
@@ -420,9 +436,15 @@ let print_its_defn fst fmt itd =
       then "mutable " else "") (if rs_ghost f then "ghost " else "")
     print_rs f Pretty.print_id_labels f.rs_name
     print_ity f.rs_cty.cty_result in
+  let is_big ity = match ity.ity_node with
+    | Ityreg {reg_args = []; reg_regs = []}
+    | Ityapp (_,[],[]) | Itypur (_,[]) | Ityvar _ -> false
+    | Itypur (s,_) when is_ts_tuple s.its_ts -> false
+    | _ -> true in
   let print_proj mf fmt f = match Mpv.find_opt f mf with
     | Some f -> fprintf fmt "@ (%a)" print_field f
     | _ when f.pv_ghost -> fprintf fmt "@ (ghost %a)" print_ity f.pv_ity
+    | _ when is_big f.pv_ity -> fprintf fmt "@ (%a)" print_ity f.pv_ity
     | _ -> fprintf fmt "@ %a" print_ity f.pv_ity in
   let print_constr mf fmt c = fprintf fmt "@\n@[<hov 4>| %a%a%a@]"
     print_rs c Pretty.print_id_labels c.rs_name

src/mlw/pmodule.ml

@@ -285,7 +285,7 @@ let create_module env ?(path=[]) n =
   let m = use_export m unit_module in
   m
 
-let add_pdecl ~wp uc d =
+let add_pdecl ~vc uc d =
   let ids = Mid.set_diff d.pd_syms uc.muc_known in
   let uc = Sid.fold (fun id uc ->
     if id_equal id ts_func.ts_name then
@@ -293,7 +293,7 @@ let add_pdecl ~wp uc d =
     else match is_ts_tuple_id id with
     | Some n -> use_export uc (tuple_module n)
     | None -> uc) ids uc in
-  ignore wp; (* TODO *)
+  ignore vc; (* TODO *)
   let uc = add_pdecl uc d in
   let th = List.fold_left Theory.add_decl uc.muc_theory d.pd_pure in
   { uc with muc_theory = th }

src/mlw/pmodule.mli

@@ -94,9 +94,9 @@ val add_meta : pmodule_uc -> meta -> meta_arg list -> pmodule_uc
 
 (** {2 Program decls} *)
 
-val add_pdecl : wp:bool -> pmodule_uc -> pdecl -> pmodule_uc
-(** [add_pdecl ~wp m d] adds declaration [d] in module [m].
-    If [wp] is [true], VC is computed and added to [m]. *)
+val add_pdecl : vc:bool -> pmodule_uc -> pdecl -> pmodule_uc
+(** [add_pdecl ~vc m d] adds declaration [d] in module [m].
+    If [vc] is [true], VC is computed and added to [m]. *)
 
 (** {2 Builtin symbols} *)
 

src/parser/typing.ml

@@ -363,11 +363,11 @@ let type_fmla uc gvars f =
 open Pdecl
 open Pmodule
 
-let add_pdecl ~wp uc d =
+let add_pdecl ~vc uc d =
   if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
-  add_pdecl ~wp uc d
+  add_pdecl ~vc uc d
 
-let add_decl uc d = add_pdecl ~wp:false uc (create_pure_decl d)
+let add_decl uc d = add_pdecl ~vc:false uc (create_pure_decl d)
 
 let add_types uc tdl =
   let add m d =
@@ -403,21 +403,34 @@ let add_types uc tdl =
         let hfd = Hstr.create 5 in
         let alias = Sstr.empty in
         let alg = Mstr.add x (id,args) alg in
-        let get_pj (_, id, ghost, pty) = match id with
-          | Some ({id_str = n} as id) ->
+        let get_pj nms (_, id, ghost, pty) = match id with
+          | Some ({id_str = nm} as id) ->
+              let exn = Loc.Located (id.id_loc, Loc.Message ("Field " ^
+                nm ^ " is used more than once in the same constructor")) in
+              let nms = Sstr.add_new exn nm nms in
               let ity = parse ~loc ~alias ~alg pty in
-              let v = try Hstr.find hfd n with Not_found ->
+              let v = try Hstr.find hfd nm with Not_found ->
                 let v = create_pvsymbol (create_user_id id) ~ghost ity in
-                Hstr.add hfd n v;
+                Hstr.add hfd nm v;
                 v in
               if not (ity_equal v.pv_ity ity && ghost = v.pv_ghost) then
-                Loc.errorm ~loc "Conflicting definitions for field %s" n;
-              true, v
+                Loc.errorm ~loc "Conflicting definitions for field %s" nm;
+              nms, (true, v)
           | None ->
               let ity = parse ~loc ~alias ~alg pty in
-              false, create_pvsymbol (id_fresh "a") ~ghost ity in
-        let get_cs (_, id, pjl) = create_user_id id, List.map get_pj pjl in
-        let csl = List.map get_cs csl in
+              nms, (false, create_pvsymbol (id_fresh "a") ~ghost ity) in
+        let get_cs oms (_, id, pjl) =
+          let nms, pjl = Lists.map_fold_left get_pj Sstr.empty pjl in
+          if Sstr.equal oms nms then create_user_id id, pjl else
+            let df = Sstr.union (Sstr.diff oms nms) (Sstr.diff nms oms) in
+            Loc.errorm ~loc "Field %s is missing in some constructors"
+              (Sstr.choose df) in
+        let csl = match csl with
+          | (_, id, pjl)::csl ->
+              let oms, pjl = Lists.map_fold_left get_pj Sstr.empty pjl in
+              (create_user_id id, pjl) :: List.map (get_cs oms) csl
+          | [] -> assert false in
+        if not (Hstr.mem htd x) then
         begin match try Some (Hstr.find hts x) with Not_found -> None with
         | Some s ->
             Hstr.add htd x (create_rec_variant_decl s csl)
@@ -427,12 +440,17 @@ let add_types uc tdl =
     | TDrecord fl ->
         let alias = Sstr.empty in
         let alg = Mstr.add x (id,args) alg in
-        let get_fd fd =
+        let get_fd nms fd =
+          let {id_str = nm; id_loc = loc} = fd.f_ident in
+          let exn = Loc.Located (loc, Loc.Message ("Field " ^
+            nm ^ " is used more than once in a record")) in
+          let nms = Sstr.add_new exn nm nms in
           let id = create_user_id fd.f_ident in
           let ity = parse ~loc ~alias ~alg fd.f_pty in
           let ghost = d.td_vis = Abstract || fd.f_ghost in
-          fd.f_mutable, create_pvsymbol id ~ghost ity in
-        let fl = List.map get_fd fl in
+          nms, (fd.f_mutable, create_pvsymbol id ~ghost ity) in
+        let _,fl = Lists.map_fold_left get_fd Sstr.empty fl in
+        if not (Hstr.mem htd x) then
         begin match try Some (Hstr.find hts x) with Not_found -> None with
         | Some s ->
             if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
@@ -461,13 +479,16 @@ let add_types uc tdl =
           let s = match q with
             | Qident {id_str = x} when Sstr.mem x alias ->
                 Loc.errorm ~loc "Cyclic type definition"
+            | Qident {id_str = x} when Hstr.mem hts x ->
+                Hstr.find hts x
             | Qident {id_str = x} when Mstr.mem x alg ->
                 let id, args = Mstr.find x alg in
                 let s = create_itysymbol_pure id args in
-                Hstr.add hts x s; s
+                Hstr.add hts x s;
+                visit ~alias ~alg x (Mstr.find x def);
+                s
             | Qident {id_str = x} when Mstr.mem x def ->
-                let d = Mstr.find x def in
-                visit ~alias ~alg x d;
+                visit ~alias ~alg x (Mstr.find x def);
                 Hstr.find hts x
             | _ ->
                 find_itysymbol uc q in
@@ -479,19 +500,7 @@ let add_types uc tdl =
 
   Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
   let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
-  add_pdecl ~wp:true uc (create_type_decl tdl)
-
-(* TODO
-    | ClashSymbol s ->
-        Loc.error ?loc:(look_for_loc tdl s) (ClashSymbol s)
-    | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) ->
-        Loc.error ?loc:(look_for_loc tdl s) (RecordFieldMissing (cs,ls))
-    | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) ->
-        Loc.error ?loc:(look_for_loc tdl s) (DuplicateRecordField (cs,ls))
-    | DuplicateVar { vs_name = { id_string = s }} ->
-        Loc.errorm ?loc:(look_for_loc tdl s)
-          "Field %s is used twice in the same constructor" s
-*)
+  add_pdecl ~vc:true uc (create_type_decl tdl)
 
 let tyl_of_params uc pl =
   let ty_of_param (loc,_,gh,ty) =