Refinement.

Exported [close_record_invariant] function from pdecl.ml so
that it can also be used in pmodule.ml

src/mlw/pdecl.ml

@@ -304,6 +304,16 @@ let mk_decl_meta = let r = ref 0 in fun meta node pure ->
 
 let mk_decl = mk_decl_meta []
 
+let close_record_invariant ts fl itd =
+  let ty = ty_app ts (List.map ty_var ts.ts_args) in
+  let u = create_vsymbol (id_fresh "self") ty in
+  let tl = [t_var u] in
+  let add_fd sbs s = let pj = ls_of_rs s in
+    Mvs.add (fd_of_rs s).pv_vs (t_app pj tl pj.ls_value) sbs in
+  let sbs = List.fold_left add_fd Mvs.empty fl in
+  let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
+  t_forall_close [u] [] inv
+
 let create_type_decl dl =
   if dl = [] then invalid_arg "Pdecl.create_type_decl";
   let conv_itd ({itd_its = s} as itd) =
@@ -352,15 +362,9 @@ let create_type_decl dl =
         let meta = Theory.(meta_float, [MAts ts; MAls pj_ls; MAls iF_ls]) in
         mk_decl_meta [meta] (PDtype [itd]) pure
     | fl, _, NoDef when itd.itd_invariant <> [] ->
-        let ty = ty_app ts (List.map ty_var ts.ts_args) in
-        let u = create_vsymbol (id_fresh "self") ty in
-        let tl = [t_var u] in
-        let add_fd sbs s = let pj = ls_of_rs s in
-          Mvs.add (fd_of_rs s).pv_vs (t_app pj tl pj.ls_value) sbs in
-        let sbs = List.fold_left add_fd Mvs.empty fl in
-        let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
+        let inv = close_record_invariant ts fl itd in
         let pr = create_prsymbol (id_derive (nm ^ "'invariant") id) in
-        let ax = create_prop_decl Paxiom pr (t_forall_close [u] [] inv) in
+        let ax = create_prop_decl Paxiom pr inv in
         let add_fd s dl = create_param_decl (ls_of_rs s) :: dl in
         let pure = create_ty_decl ts :: List.fold_right add_fd fl [ax] in
         mk_decl (PDtype [itd]) pure

src/mlw/pdecl.mli

@@ -91,6 +91,10 @@ and pdecl_node = private
 
 and meta_decl = Theory.meta * Theory.meta_arg list
 
+val close_record_invariant : tysymbol -> rsymbol list -> its_defn -> term
+(** [close_record_invariant ts fl itd] universally closes a record invariant
+    with a variable 'self', of the record type, with respect to the list [fl]. *)
+
 val create_type_decl : its_defn list -> pdecl list
 
 val create_let_decl : let_defn -> pdecl

src/mlw/pmodule.ml

@@ -615,20 +615,6 @@ let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} =
 let clone_invl cl sm invl =
   List.map (fun t -> clone_term cl sm.sm_vs t) invl
 
-let mk_record_invariant d s =
-  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 fl = d.itd_fields in
-  let _proj, sbs = List.fold_right get_ld fl ([],Mvs.empty) in
-  let inv = t_subst sbs (t_and_simp_l d.itd_invariant) in
-  t_forall_close [u] [] inv
-
 let clone_type_record cl s d s' d' =
   let id = s.its_ts.ts_name in
   let fields' = Hstr.create 16 in
@@ -693,8 +679,7 @@ let clone_type_decl inst cl tdl kn =
           let pd' = Mid.find s'.its_ts.ts_name kn in
           let d' = begin match pd'.pd_node with
             | PDtype [d'] -> d'
-            | PDtype _ ->
-              (* FIXME: we could refine with mutual types *)
+            | PDtype _ -> (* FIXME: we could refine with mutual types *)
               raise (BadInstance id)
             | PDlet _ | PDexn _ | PDpure -> raise (BadInstance id)
           end in
@@ -704,8 +689,9 @@ let clone_type_decl inst cl tdl kn =
           | [], _ -> ()
           | _, [] -> raise (BadInstance id) (* TODO? also reject the *)
                                             (* trivial invariant ? *)
-          | _ -> let d_inv = mk_record_invariant d s in
-            let inv = clone_invl cl (sm_of_cl cl) [d_inv] in
+          | _ ->
+            let inv = close_record_invariant s.its_ts d.itd_fields d in
+            let inv = clone_invl cl (sm_of_cl cl) [inv] in
             let add_vc inv = vcs := (d.itd_its, inv) :: !vcs in
             List.iter add_vc inv end
       | None -> begin match Mts.find_opt ts inst.mi_ty with