Things compile.

All the program logic tactics are out of order but core logic mostly works with new module system.

Author: Cameron-Low

src/ecCommands.ml

@@ -199,28 +199,42 @@ let process_locate scope x =
 (* -------------------------------------------------------------------- *)
 module HiPrinting = struct
   let pr_glob fmt env pm =
+    match pm with
+    | FM_ff _ -> failwith "implement."
+    | FM_FunOrVar _ -> failwith "implement."
+    | FM_Mod pm -> begin
     let ppe = EcPrinting.PPEnv.ofenv env in
     let (p, _) = EcTyping.trans_msymbol env pm in
-    let us = EcEnv.NormMp.mod_use env p in
-
-    Format.fprintf fmt "Globals [# = %d]:@."
-      (Sid.cardinal us.EcEnv.us_gl);
-    Sid.iter (fun id ->
-      Format.fprintf fmt "  %s@." (EcIdent.name id))
-      us.EcEnv.us_gl;
-
-    Format.fprintf fmt "@.";
-
-    Format.fprintf fmt "Prog. variables [# = %d]:@."
-      (Mx.cardinal us.EcEnv.us_pv);
-    List.iter (fun (xp,_) ->
+    let _fp, us = EcMemRestr.module_uses env p None in
+
+    Format.fprintf fmt "Calls [# = %d]:@."
+      (EcPath.Sx.cardinal us.us_calls);
+    EcPath.Sx.iter (fun xp -> 
+      Format.fprintf fmt "  @[%a@]@."
+        (EcPrinting.pp_funname ppe) xp
+      )
+      us.us_calls;
+    Format.fprintf fmt "Reads [# = %d]:@."
+      (EcPath.Sx.cardinal us.us_reads);
+    EcPath.Sx.iter (fun xp -> 
       let pv = EcTypes.pv_glob xp in
       let ty = EcEnv.Var.by_xpath xp env in
       Format.fprintf fmt "  @[%a : %a@]@."
         (EcPrinting.pp_pv ppe) pv
-        (EcPrinting.pp_type ppe) ty)
-      (List.rev (Mx.bindings us.EcEnv.us_pv))
-
+        (EcPrinting.pp_type ppe) ty
+      )
+      us.us_reads;
+    Format.fprintf fmt "Writes [# = %d]:@."
+      (EcPath.Sx.cardinal us.us_writes);
+    EcPath.Sx.iter (fun xp -> 
+      let pv = EcTypes.pv_glob xp in
+      let ty = EcEnv.Var.by_xpath xp env in
+      Format.fprintf fmt "  @[%a : %a@]@."
+        (EcPrinting.pp_pv ppe) pv
+        (EcPrinting.pp_type ppe) ty
+      )
+      us.us_writes
+      end
 
   let pr_goal fmt scope n =
     match EcScope.xgoal scope with

src/ecCorePrinting.ml

@@ -56,11 +56,12 @@ module type PrinterAPI = sig
   val pp_tcname  : PPEnv.t -> path pp
   val pp_thname  : PPEnv.t -> path pp
 
-  val pp_mem      : PPEnv.t -> EcIdent.t pp
-  val pp_memtype  : PPEnv.t -> EcMemory.memtype pp
-  val pp_tyvar    : PPEnv.t -> ident pp
-  val pp_tyunivar : PPEnv.t -> EcUid.uid pp
-  val pp_path     : path pp
+  val pp_mem       : PPEnv.t -> EcIdent.t pp
+  val pp_memtype   : PPEnv.t -> EcMemory.memtype pp
+  val pp_mem_restr : PPEnv.t -> EcAst.mem_restr pp
+  val pp_tyvar     : PPEnv.t -> ident pp
+  val pp_tyunivar  : PPEnv.t -> EcUid.uid pp
+  val pp_path      : path pp
 
   (* ------------------------------------------------------------------ *)
   val pp_typedecl    : PPEnv.t -> (path * tydecl                  ) pp

src/ecEnv.ml

@@ -1792,7 +1792,8 @@ module Mod = struct
         (fun s (x, _) a -> EcSubst.add_module s x a)
         EcSubst.empty params args
     in
-      f s o
+
+    f s o
 
   let clearparams n params =
     let _, remaining = List.takedrop n params in

src/ecLowGoal.ml

@@ -169,7 +169,7 @@ module LowApply = struct
           (* FIXME: poor API ==> poor error recovery *)
           try
             EcTyping.check_modtype env mp mt emt;
-            (EcFol.f_bind_mod sbt x mp env, f)
+            (Fsubst.f_bind_mod sbt x mp, f)
           with _ -> raise InvalidProofTerm
         end
 
@@ -1627,7 +1627,7 @@ let t_rewrite_hyp ?xconv ?mode ?donot (id : EcIdent.t) pos (tc : tcenv1) =
 (* -------------------------------------------------------------------- *)
 type vsubst = [
   | `Local of EcIdent.t
-  | `Glob  of EcIdent.t * EcMemory.memory
+  | `Glob  of EcAst.functor_fun * EcMemory.memory
   | `PVar  of EcTypes.prog_var * EcMemory.memory
 ]
 
@@ -1673,10 +1673,12 @@ module LowSubst = struct
 
     (* Substitution of globs *)
     | Fglob (mp, m), None when kind.sk_glob -> Some (`Glob (mp, m))
-    | Fglob (mp, m), Some (`Glob (mp', _)) when kind.sk_glob ->
+    | Fglob (mp, m), Some (`Glob (mp', _)) when kind.sk_glob -> assert false
+      (*
         if   EcIdent.id_equal mp mp'
         then Some (`Glob (mp, m))
         else None
+        *)
 
     | _, _ -> None
 
@@ -1725,10 +1727,13 @@ module LowSubst = struct
         if EcPV.PV.mem_pv env pv fv then None else Some aout
 
       (* Substitution of globs *)
-      | Some ((_, `Glob (mp, m), f) as aout) ->
+      | Some ((_, `Glob (mp, m), f) as aout) -> assert false
+        (*
         let f  = simplify { no_red with delta_h = predT } hyps f in
         let fv = EcPV.PV.fv env m f in
-        if EcPV.PV.mem_glob env (EcPath.mident mp) fv then None else Some aout in
+        if EcPV.PV.mem_glob env (EcPath.mident mp) fv then None else Some aout
+          *)
+            in
     match aout with
     | None -> None
     | Some(side,v,f) ->
@@ -1759,8 +1764,8 @@ module LowSubst = struct
         let check _tg = true in
         (subst f, check)
 
-    | `Glob (mp, m) ->
-        let subst f = EcPV.PVM.subst env (EcPV.PVM.add_glob env (EcPath.mident mp) m f EcPV.PVM.empty) in
+    | `Glob (_ff, _m) ->
+        let subst _f = EcPV.PVM.subst env EcPV.PVM.empty in (* (EcPV.PVM.add_glob env (EcPath.mident mp) m f EcPV.PVM.empty) in *)
         (* FIXME *)
         let check _tg = true in
         (subst f, check)

src/ecLowGoal.mli

@@ -191,7 +191,7 @@ val t_cutdef : proofterm -> form -> FApi.backward
 (* -------------------------------------------------------------------- *)
 type vsubst = [
   | `Local of EcIdent.t
-  | `Glob  of EcIdent.t * EcMemory.memory
+  | `Glob  of EcAst.functor_fun * EcMemory.memory
   | `PVar  of EcTypes.prog_var * EcMemory.memory
 ]
 

src/ecLowPhlGoal.ml

@@ -453,7 +453,8 @@ let subst_form_lv env m lv t f =
 
 (* -------------------------------------------------------------------- *)
 (* Remark: m is only used to create fresh name, id_of_pv *)
-let generalize_subst_ env m uelts uglob =
+let generalize_subst_ env m uelts uglob = assert false
+(*
   let create (pv, ty) = id_of_pv pv m, GTty ty in
   let b = List.map create uelts in
   let s =
@@ -471,8 +472,10 @@ let generalize_subst_ env m uelts uglob =
       s uglob b'
   in
     (b', b, s)
+*)
 
-let generalize_mod_ env m modi f =
+let generalize_mod_ env m modi f = assert false
+(*
   let (melts, mglob) = PV.ntr_elements modi in
 
   (* 1. Compute the prog-vars and the globals used in [f] *)
@@ -512,7 +515,7 @@ let generalize_mod_ env m modi f =
   let s = PVM.of_mpv s m in
   let f = PVM.subst env s f in
   f_forall_simpl (bd'@bd) f, (bd', uglob), (bd, uelts)
-
+    *)
 let generalize_subst env m uelts uglob =
   let (b',b,f) = generalize_subst_ env m uelts uglob in
   b'@b, f

src/ecMatching.ml

@@ -321,10 +321,10 @@ module MEV = struct
     let v = EV.fold (fun x k v -> f x (`Mod  k) v) m.evm_mod  v in
     v
 
-  let assubst ue ev env =
+  let assubst ue ev _env =
     let subst = f_subst_init ~tu:(EcUnify.UniEnv.assubst ue) () in
     let subst = EV.fold (fun x m s -> Fsubst.f_bind_mem s x m) ev.evm_mem subst in
-    let subst = EV.fold (fun x mp s -> EcFol.f_bind_mod s x mp env) ev.evm_mod subst in
+    let subst = EV.fold (fun _x _mp _s -> assert false) ev.evm_mod subst in
     let seen  = ref Sid.empty in
 
     let rec for_ident x binding subst =
@@ -527,10 +527,13 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
       | Fint i1, Fint i2 ->
           if not (EcBigInt.equal i1 i2) then failure ();
 
-      | Fglob (mp1, me1), Fglob (mp2, me2) ->
+      | Fglob _, Fglob _ ->
+          assert false;
+        (*
             if not (EcIdent.id_equal mp1 mp2) then
               failure ();
             doit_mem env mxs me1 me2
+          *)
 
       | Ftuple fs1, Ftuple fs2 ->
           if List.length fs1 <> List.length fs2 then
@@ -717,7 +720,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
             in (env, subst)
 
         | GTmodty p1, GTmodty p2 ->
-            if not (NormMp.mod_type_equiv env p1 p2) then
+            if not (NormMp.module_type_equiv env (fst p1) (fst p2)) then
               raise MatchFailure;
 
             let subst =

src/ecMemRestr.ml

@@ -97,6 +97,9 @@ let ff_norm env ff mem =
   let _, fuses = funs_uses_core env ff.ff_params [ff.ff_xp] in
   Uses.to_form env ff.ff_params fuses mem
 
+let ff_norm_ty env ff =
+  let _, fuses = funs_uses_core env ff.ff_params [ff.ff_xp] in
+  Uses.to_type env ff.ff_params fuses
 
 let funs_uses_mr env params fs =
   let env, fuses = funs_uses_core env params fs in
@@ -157,6 +160,54 @@ let rec norm_mem_restr env mr =
   | Inter(s1, s2) -> mr_inter (norm_mem_restr env s1) (norm_mem_restr env s2)
   | Diff (s1, s2) -> mr_diff  (norm_mem_restr env s1) (norm_mem_restr env s2)
 
+
+let rec norm_globs_restrs env f =
+  let has_mod b =
+    List.exists (fun (_,gty) ->
+      match gty with GTmodty _ -> true | _ -> false) b in
+
+  let norm_bind env (x, gty) =
+    match gty with
+    | GTty ty -> begin
+      match ty.ty_node with
+      | Tglob ff -> (x, GTty (ff_norm_ty env ff))
+      | _ -> (x, gty)
+      end
+    | GTmodty (mt, mr) -> (x, (GTmodty (mt, norm_mem_restr env mr)))
+    | GTmem _ -> (x, gty)
+  in
+
+  match f.f_node with
+  | Fquant (q, bd, f) -> 
+    let env = if has_mod bd then EcEnv.Mod.add_mod_binding bd env else env in
+    f_quant q (List.map (norm_bind env) bd) (norm_globs_restrs env f)
+  | Fglob (ff, m) -> ff_norm env ff m
+  | Fif (f1, f2, f3) -> 
+    f_if
+      (norm_globs_restrs env f1)
+      (norm_globs_restrs env f2)
+      (norm_globs_restrs env f3)
+  | Fmatch (b, fs, ty) ->
+    f_match 
+      (norm_globs_restrs env b)
+      (List.map (norm_globs_restrs env) fs)
+      ty
+  | Flet (lv, f1, f2) ->
+    f_let 
+      lv 
+      (norm_globs_restrs env f1)
+      (norm_globs_restrs env f2)
+  | Fapp (e, es) -> 
+    f_app 
+      (norm_globs_restrs env e)
+      (List.map (norm_globs_restrs env) es)
+      f.f_ty
+  | Ftuple es -> 
+      f_tuple (List.map (norm_globs_restrs env) es)
+  | Fproj (e, i) -> 
+    f_proj (norm_globs_restrs env e) i f.f_ty
+  | _ -> f
+
 let sup env ff =
   (* The xpath is know to be normalised so it is abstract *)
   match (Fun.by_xpath ff.ff_xp env).f_def with
@@ -457,6 +508,16 @@ and process (env : env) (r : mem) (st : local_state) =
 
 (* ------------------------------------------------------------------- *)
 
+let rec dump_mem_restr mr =
+  match mr with
+  | Empty -> "Empty"
+  | All -> "All"
+  | Var x -> Format.sprintf "Var (%s)" (EcPath.x_tostring x)
+  | GlobFun ff -> Format.sprintf "GlobFun (%s)" (EcPath.x_tostring ff.ff_xp)
+  | Inter (l, r) -> Format.sprintf "Inter (%s, %s)" (dump_mem_restr l) (dump_mem_restr r)
+  | Union (l, r) -> Format.sprintf "Union (%s, %s)" (dump_mem_restr l) (dump_mem_restr r)
+  | Diff (l, r) -> Format.sprintf "Diff (%s, %s)" (dump_mem_restr l) (dump_mem_restr r)
+
 (* /!\ Precondition s1 and s2 should have been normalised *)
 let core_subset env s1 s2 =
   (* add clause !(s1 subset s2)

src/ecMemRestr.mli

@@ -6,10 +6,10 @@ module Uses : sig
   val to_form : env -> functor_params -> EcModules.uses -> memory -> form
 end
 
-
 val ff_alpha_equal : functor_fun -> functor_fun -> bool
 
 val ff_norm : env -> functor_fun -> memory -> form
+val ff_norm_ty : env -> functor_fun -> ty
 
 val fun_uses_mr : env -> xpath -> mem_restr
 
@@ -21,6 +21,8 @@ val module_uses_form : env -> mpath -> module_type option -> memory -> form
 
 val module_uses : env -> mpath -> module_type option -> functor_params * EcModules.uses
 
+val norm_globs_restrs : env -> form -> form
+
 val equal    : env -> mem_restr -> mem_restr -> bool
 val subset   : env -> mem_restr -> mem_restr -> bool
 val disjoint : env -> mem_restr -> mem_restr -> bool