sections: expand&clear module aliases that contain generalized modules

src/ecPath.ml

@@ -90,6 +90,9 @@ let rec pappend p1 p2 =
  | Psymbol id -> pqname p1 id
  | Pqname(p2,id) -> pqname (pappend p1 p2) id
 
+let poappend (p1 : path) (p2 : path option) =
+ ofold ((^~) pappend) p1 p2
+
 let pqoname p id =
  match p with
  | None -> psymbol id
@@ -260,6 +263,12 @@ let m_apply mp args =
 (* if args' = [] then mpath mp.m_top args
  else (assert (args = []); mp) *)
 
+let is_abstract (mp : mpath) =
+ match mp.m_top with `Local _ -> true | _ -> false
+
+let is_concrete (mp : mpath) =
+ match mp.m_top with `Concrete _ -> true | _ -> false
+
 let m_functor mp =
  let top =
  match mp.m_top with

src/ecPath.mli

@@ -14,10 +14,11 @@ and path_node =
 | Pqname of path * symbol
 
 (* -------------------------------------------------------------------- *)
-val psymbol : symbol -> path
-val pqname : path -> symbol -> path
-val pqoname : path option -> symbol -> path
-val pappend : path -> path -> path
+val psymbol : symbol -> path
+val pqname : path -> symbol -> path
+val pqoname : path option -> symbol -> path
+val pappend : path -> path -> path
+val poappend : path -> path option -> path
 
 val p_equal : path -> path -> bool
 val p_compare : path -> path -> int
@@ -78,6 +79,9 @@ val m_hash : mpath -> int
 val m_apply : mpath -> mpath list -> mpath
 val m_fv : int EcIdent.Mid.t -> mpath -> int EcIdent.Mid.t
 
+val is_abstract : mpath -> bool
+val is_concrete : mpath -> bool
+
 val m_functor : mpath -> mpath
 
 val mget_ident : mpath -> ident

src/ecSection.ml

@@ -951,13 +951,44 @@ let generalize_modtype to_gen (name, ms) =
  let ms = EcSubst.subst_top_modsig to_gen.tg_subst ms in
  to_gen, Some (Th_modtype (name, ms))
 
-let generalize_module to_gen me =
+let generalize_module to_gen prefix me =
  match me.tme_loca with
  | `Local -> to_gen, None
- | `Global ->
-  (* FIXME section: we can generalize declare module *)
+
+ | `Global -> begin
  let me = EcSubst.subst_top_module to_gen.tg_subst me in
- to_gen, Some (Th_module me)
+
+ match me.tme_expr.me_body with
+ | ME_Alias (_, mp) -> begin
+ let bds = to_gen.tg_binds in
+ let bds = List.filter_map (function Binding (m, GTmodty _) -> Some m | _ -> None) bds in
+ let bds = Sid.of_list bds in
+
+ let exception Inline in
+
+ let check_gen (x : cbarg) =
+ match x with
+ | `Module { m_top = `Local x } ->
+ if Sid.mem x bds then raise Inline
+ | _ -> () in
+
+ try
+ on_mp check_gen mp;
+ to_gen, Some (Th_module me)
+
+ with Inline ->
+ let to_gen = { to_gen with tg_subst =
+ EcSubst.add_moddef
+ ~src:(EcPath.pqname prefix me.tme_expr.me_name)
+ ~dst:mp to_gen.tg_subst } in
+ to_gen, None
+ end
+
+ | _ ->
+ (* FIXME section: we can generalize declare module *)
+ to_gen, Some (Th_module me)
+ end
+
  | `Declare -> assert false (* should be a LC_decl_mod *)
 
 let generalize_export to_gen (p,lc) =
@@ -1336,7 +1367,7 @@ let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_i
  | Th_operator opdecl -> generalize_opdecl to_gen prefix opdecl
  | Th_axiom ax -> generalize_axiom to_gen prefix ax
  | Th_modtype ms -> generalize_modtype to_gen ms
- | Th_module me -> generalize_module to_gen me
+ | Th_module me -> generalize_module to_gen prefix me
  | Th_theory th -> (generalize_ctheory to_gen prefix th, None)
  | Th_export (p,lc) -> generalize_export to_gen (p,lc)
  | Th_instance (ty,i,lc) -> generalize_instance to_gen (ty,i,lc)

src/ecSubst.ml

@@ -32,7 +32,7 @@ type subst = {
  sb_fmem : EcIdent.t Mid.t;
  sb_tydef : (EcIdent.t list * ty) Mp.t;
  sb_def : (EcIdent.t list * [`Op of expr | `Pred of form]) Mp.t;
- sb_moddef : EcPath.path Mp.t;
+ sb_moddef : EcPath.mpath Mp.t; (* Only top-level modules *)
 }
 
 (* -------------------------------------------------------------------- *)
@@ -74,14 +74,27 @@ let subst_path (s : subst) (p : EcPath.path) = _subst_path s.sb_path p
 
 (* -------------------------------------------------------------------- *)
 let subst_mpath (s : subst) (mp : EcPath.mpath) =
- let crt_ps = Mp.union (fun _ _ x -> Some x) s.sb_path s.sb_moddef in
-
  let rec doit s (mp : EcPath.mpath) =
  let args = List.map (doit s) mp.m_args in
  match mp.m_top with
+ | `Concrete (p, sub) when Mp.mem p s.sb_moddef -> begin
+ let s_p, s_sub, s_args =
+ match Mp.find p s.sb_moddef with
+ | { m_top = `Concrete (s_p, s_sub); m_args } -> (s_p, s_sub, m_args)
+ | _ -> assert false in
+
+ let cat_sub =
+ match s_sub with
+ | None -> sub
+ | Some s_sub -> Some (EcPath.poappend s_sub sub) in
+
+ EcPath.mpath_crt s_p (s_args @ mp.m_args) cat_sub
+ end
+
  | `Concrete (p, sub) ->
- let p = _subst_path crt_ps p in
- EcPath.mpath_crt p args sub
+ let p = _subst_path s.sb_path p in
+ EcPath.mpath_crt p args sub
+
  | `Local id ->
  match Mid.find_opt id s.sb_module with
  | None -> EcPath.mpath_abs id args
@@ -266,8 +279,9 @@ let add_pddef (s : subst) p (ids, f) =
  assert (Mp.find_opt p s.sb_def = None);
  { s with sb_def = Mp.add p (ids, `Pred f) s.sb_def }
 
-let add_moddef (s : subst) ~(src : EcPath.path) ~(dst : EcPath.path) =
+let add_moddef (s : subst) ~(src : EcPath.path) ~(dst : EcPath.mpath) =
  assert (Mp.find_opt src s.sb_moddef = None);
+ assert (EcPath.is_concrete dst);
  { s with sb_moddef = Mp.add src dst s.sb_moddef }
 
 (* -------------------------------------------------------------------- *)

src/ecSubst.mli

@@ -28,7 +28,7 @@ val add_path : subst -> src:path -> dst:path -> subst
 val add_tydef : subst -> path -> (EcIdent.t list * ty) -> subst
 val add_opdef : subst -> path -> (EcIdent.t list * expr) -> subst
 val add_pddef : subst -> path -> (EcIdent.t list * form) -> subst
-val add_moddef : subst -> src:path -> dst:path -> subst
+val add_moddef : subst -> src:path -> dst:mpath -> subst (* Only concrete modules *)
 val add_memory : subst -> EcIdent.t -> EcIdent.t -> subst
 
 val add_flocal : subst -> EcIdent.t -> form -> subst

src/ecTheoryReplay.ml

@@ -756,13 +756,7 @@ and replay_mod
 
  let mp, (newme, newlc) = EcEnv.Mod.lookup (unloc newname) env in
 
- let np =
- match mp.m_top with
- | `Concrete (p, None) -> p
- | _ -> assert false
- in
-
- let substme = EcSubst.add_moddef subst ~src:(xpath ove name) ~dst:np in
+ let substme = EcSubst.add_moddef subst ~src:(xpath ove name) ~dst:mp in
 
  let me = EcSubst.subst_top_module substme me in
  let me = { me with tme_expr = { me.tme_expr with me_name = name } } in
@@ -772,12 +766,12 @@ and replay_mod
  if not (EcReduction.EqTest.for_mexpr ~body:false env me.tme_expr newme.tme_expr) then
  clone_error env (CE_ModIncompatible (snd ove.ovre_prefix, name));
 
- let (subst, _) =
+ let subst =
  match mode with
  | `Alias ->
- rename ove subst (`Module, name)
+ fst (rename ove subst (`Module, name))
  | `Inline _ ->
- substme, EcPath.basename np in
+ substme in
 
  let newme =
  if mode = `Alias || mode = `Inline `Keep then

tests/generalize-module-aliases.ec

@@ -0,0 +1,50 @@
+module type T = {
+ proc f(): bool
+}.
+
+
+module F(O1 : T, O2 : T) = {
+ module M = {
+ module N = {
+ proc g() = {
+ var r1, r2;
+
+ r1 <@ O1.f();
+ r2 <@ O2.f();
+ return (r1, r2);
+ }
+ }
+ }
+}.
+
+module M : T = {
+ proc f() = {
+ return true;
+ }
+}.
+
+section.
+declare module M_T1 <: T.
+declare module M_T2 <: T.
+
+module A1 = F(M_T1, M_T2).M.
+module A2 = F(M_T1).
+
+module C = M.
+
+hoare L1: A1.N.g: true ==> true.
+proof. admitted.
+
+hoare L2: A2(C).M.N.g: true ==> true.
+proof. admitted.
+
+end section.
+
+hoare LL1 (M1 <: T) (M2 <: T): F(M1, M2).M.N.g : true ==> true.
+proof. exact (L1 M1 M2). qed.
+
+hoare LL2 (M1 <: T): F(M1, M).M.N.g : true ==> true.
+proof. exact (L1 M1 C). qed. (* The module alias C can escape the section *)
+
+hoare LL3 (M1 <: T): F(M1, M).M.N.g : true ==> true.
+proof. exact (L2 M1). qed.