feat(clone): reintroduce module overriding for stateless modules

src/ecCoreModules.ml

@@ -553,6 +553,18 @@ type top_module_expr = {
 let is_me_body_alias (body : module_body) =
   match body with ME_Alias _ -> true | _ -> false
 
+let module_own_state (me : module_expr) : symbol list option =
+  let rec for_comps (comps : module_comps) : symbol list option =
+    List.opick for_item comps
+
+  and for_item (item : module_item) : symbol list option =
+    match item with
+    | MI_Variable v -> Some [v.v_name]
+    | MI_Function _ -> None
+    | MI_Module  me -> omap (fun p -> me.me_name :: p) (for_comps me.me_comps)
+
+  in for_comps me.me_comps
+
 (* -------------------------------------------------------------------- *)
 let ur_hash = EcAst.ur_hash
 

src/ecCoreModules.mli

@@ -257,6 +257,10 @@ type top_module_expr = {
 
 val is_me_body_alias : module_body -> bool
 
+(* Component path of the first program variable owned by the module, [None] if
+   it owns none (transitively through its sub-modules). *)
+val module_own_state : module_expr -> symbol list option
+
 (* -------------------------------------------------------------------- *)
 val mty_equal :
   module_type ->

src/ecParser.mly

@@ -3911,11 +3911,8 @@ clone_override:
 | LEMMA x=qoident mode=loc(opclmode) y=qoident
   { x, PTHO_Axiom (y, unloc mode) }
 
-| MODULE uqident loc(opclmode) uqident
-   { parse_error
-       (EcLocation.make $startpos $endpos)
-       (Some "Module overriding is no longer supported.")
-   }
+| MODULE x=uqident mode=loc(opclmode) y=uqident
+   { (x, PTHO_Module (y, unloc mode)) }
 
 | MODULE TYPE x=uqident mode=loc(opclmode) y=uqident
    { (x, PTHO_ModTyp (y, unloc mode)) }

src/ecParsetree.ml

@@ -1359,6 +1359,7 @@ and theory_override =
 | PTHO_Op     of op_override
 | PTHO_Pred   of pr_override
 | PTHO_Axiom  of ax_override
+| PTHO_Module of me_override
 | PTHO_ModTyp of mt_override
 | PTHO_Theory of th_override
 

src/ecReduction.ml

@@ -343,6 +343,9 @@ end) = struct
   let rec for_module_expr env ~norm ~body me1 me2 =
     me1.me_name = me2.me_name &&
       for_module_sig_body env me1.me_sig_body me2.me_sig_body &&
+    List.for_all2
+      (fun (_, mt1) (_, mt2) -> for_module_type env ~norm mt1 mt2)
+      me1.me_params me2.me_params &&
     let env, s = add_modules env me2.me_params me1.me_params in
     let comps1 = me1.me_comps in
     let comps2 = EcSubst.subst_module_comps s me2.me_comps in

src/ecThCloning.ml

@@ -25,20 +25,23 @@ type ovkind =
 | OVK_Abbrev
 | OVK_Theory
 | OVK_Lemma
+| OVK_ModExpr
 | OVK_ModType
 
 type clone_error =
 | CE_UnkTheory         of qsymbol
 | CE_DupOverride       of ovkind * qsymbol
 | CE_UnkOverride       of ovkind * qsymbol
-| CE_ThyOverride       of qsymbol
+| CE_ThyOverride       of qsymbol * qsymbol
 | CE_UnkAbbrev         of qsymbol
 | CE_TypeArgMism       of ovkind * qsymbol
 | CE_OpIncompatible    of qsymbol * incompatible
 | CE_PrIncompatible    of qsymbol * incompatible
 | CE_TyIncompatible    of qsymbol * incompatible
 | CE_ModTyIncompatible of qsymbol
 | CE_ModIncompatible   of qsymbol
+| CE_ModStateful       of qsymbol * symbol list
+| CE_ModNotConcrete    of qsymbol
 | CE_InvalidRE         of string
 | CE_InlinedOpIsForm   of qsymbol
 | CE_ProofForLemma     of qsymbol
@@ -80,6 +83,7 @@ type evclone = {
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
+  evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
   evc_ths      : (evclone * bool) Msym.t;
@@ -101,6 +105,7 @@ let evc_empty =
       evc_ops      = Msym.empty;
       evc_preds    = Msym.empty;
       evc_abbrevs  = Msym.empty;
+      evc_modexprs = Msym.empty;
       evc_modtypes = Msym.empty;
       evc_lemmas   = evl;
       evc_ths      = Msym.empty; }
@@ -407,6 +412,46 @@ end = struct
                pthp_tactic = Some tc; } in
     (pr :: proofs, evc)
 
+  (* ------------------------------------------------------------------ *)
+  (* Sound only for state-free modules: their own glob is empty, so AST-equal
+     components (checked at replay time) make source and target indiscernible. *)
+  let modexpr_ovrd oc ((proofs, evc) : state) name (med : me_override) =
+    let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in
+
+    let () =
+      match find_modexpr oc.oc_oth name with
+      | None ->
+         clone_error oc.oc_env (CE_UnkOverride (OVK_ModExpr, name))
+      | Some src ->
+         oiter
+           (fun path -> clone_error oc.oc_env (CE_ModStateful (name, path)))
+           (EcCoreModules.module_own_state src.tme_expr) in
+
+    let () =
+      let target = unloc (fst med) in
+
+      match EcEnv.Mod.lookup_opt target oc.oc_env with
+      | None ->
+         clone_error oc.oc_env (CE_UnkOverride (OVK_ModExpr, target))
+      | Some (mp, (dst, loca)) ->
+         match mp.EcPath.m_top, loca with
+         | `Concrete (_, None), Some _ ->
+            oiter
+              (fun path -> clone_error oc.oc_env (CE_ModStateful (target, path)))
+              (EcCoreModules.module_own_state dst)
+         | _ ->
+            clone_error oc.oc_env (CE_ModNotConcrete target) in
+
+    let evc =
+      evc_update
+        (fun evc ->
+         if Msym.mem x evc.evc_modexprs then
+           clone_error oc.oc_env (CE_DupOverride (OVK_ModExpr, name));
+         { evc with evc_modexprs = Msym.add x (mk_loc lc med) evc.evc_modexprs })
+        nm evc
+
+    in (proofs, evc)
+
   (* ------------------------------------------------------------------ *)
   let modtype_ovrd oc ((proofs, evc) : state) name (mtd : mt_override) =
     let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in
@@ -442,18 +487,23 @@ end = struct
       | Some ({cth_mode = `Concrete} as th) -> th
     in
 
-    (* FIXME improve error message *)
-    let rec contains_module cth =
-      let doit it =
-        match it.ti_item with
-        | Th_module _ -> true
-        | Th_theory (_, cth) -> contains_module cth
-        | _ -> false
-      in
-      List.exists doit cth.cth_items
-    in
-    if contains_module dth then
-      clone_error oc.oc_env (CE_ThyOverride name);
+    let stateful_module (cth : ctheory) : qsymbol option =
+      let rec doit prefix cth =
+        List.opick (fun it ->
+          match it.ti_item with
+          | Th_module me ->
+             omap
+               (fun _ -> (nm @ [x] @ prefix, me.tme_expr.me_name))
+               (EcCoreModules.module_own_state me.tme_expr)
+          | Th_theory (y, cth) ->
+             doit (prefix @ [y]) cth
+          | _ -> None)
+          cth.cth_items
+      in doit [] cth in
+
+    oiter
+      (fun mp -> clone_error oc.oc_env (CE_ThyOverride (name, mp)))
+      (stateful_module dth);
 
     let sp =
       match EcEnv.Theory.lookup_opt (unloc thd) oc.oc_env with
@@ -518,8 +568,10 @@ end = struct
       | Th_export _ ->
          (proofs, evc)
 
-      | Th_module _ ->
-         (proofs, evc)
+      | Th_module me ->
+        let x = me.tme_expr.me_name in
+        let ovrd = loced (EcPath.toqsymbol (tgpath ~kind:`Module x)) in
+        modexpr_ovrd oc (proofs, evc) (dtpath x) (ovrd, mode)
 
       | Th_modtype (x, _) ->
         let ovrd = loced (EcPath.toqsymbol (tgpath ~kind:`ModType x)) in
@@ -554,6 +606,9 @@ end = struct
      | PTHO_Axiom axd ->
         ax_ovrd oc state name axd
 
+     | PTHO_Module med ->
+       modexpr_ovrd oc state name med
+
      | PTHO_ModTyp mtd ->
        modtype_ovrd oc state name mtd
 

src/ecThCloning.mli

@@ -19,20 +19,23 @@ type ovkind =
 | OVK_Abbrev
 | OVK_Theory
 | OVK_Lemma
+| OVK_ModExpr
 | OVK_ModType
 
 type clone_error =
 | CE_UnkTheory         of qsymbol
 | CE_DupOverride       of ovkind * qsymbol
 | CE_UnkOverride       of ovkind * qsymbol
-| CE_ThyOverride       of qsymbol
+| CE_ThyOverride       of qsymbol * qsymbol
 | CE_UnkAbbrev         of qsymbol
 | CE_TypeArgMism       of ovkind * qsymbol
 | CE_OpIncompatible    of qsymbol * incompatible
 | CE_PrIncompatible    of qsymbol * incompatible
 | CE_TyIncompatible    of qsymbol * incompatible
 | CE_ModTyIncompatible of qsymbol
 | CE_ModIncompatible   of qsymbol
+| CE_ModStateful       of qsymbol * symbol list
+| CE_ModNotConcrete    of qsymbol
 | CE_InvalidRE         of string
 | CE_InlinedOpIsForm   of qsymbol
 | CE_ProofForLemma     of qsymbol
@@ -62,6 +65,7 @@ type evclone = {
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
+  evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
   evc_ths      : (evclone * bool) Msym.t;

src/ecTheoryReplay.ml

@@ -973,12 +973,62 @@ and replay_modtype
 and replay_mod
   (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (me : top_module_expr))
 =
+  match Msym.find_opt me.tme_expr.me_name ove.ovre_ovrd.evc_modexprs with
+  | None ->
     let subst, name = rename ove subst (`Module, me.tme_expr.me_name) in
     let me = EcSubst.subst_top_module subst me in
     let me = { me with tme_expr = { me.tme_expr with me_name = name } } in
     let item = (Th_module me) in
     (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import item)
 
+  (* Both modules are state-free (enforced when the override is elaborated),
+     hence indiscernible once their components are found AST-equal below. *)
+  | Some { pl_desc = (target, mode) } ->
+    let name = me.tme_expr.me_name in
+    let env  = EcSection.env (ove.ovre_hooks.henv scope) in
+
+    assert (EcCoreModules.module_own_state me.tme_expr = None);
+
+    let mp, (newme, newlc) = EcEnv.Mod.lookup (unloc target) env in
+
+    let () =
+      match mp.EcPath.m_top with
+      | `Concrete (_, None) -> () | _ -> assert false in
+
+    let substme =
+      EcSubst.add_moddef subst
+        ~src:(EcPath.mpath_crt (xpath ove name) [] None) ~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
+    let newme = { newme with me_name = name } in
+    let newme = { tme_expr = newme; tme_loca = Option.get newlc; } in
+
+    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, name =
+      match mode with
+      | `Alias    -> rename ove subst (`Module, name)
+      | `Inline _ -> substme, name in
+
+    let scope =
+      if keep_of_mode mode then
+        let alias =
+          ME_Alias (
+            List.length newme.tme_expr.me_params,
+            EcPath.m_apply mp
+              (List.map
+                 (fun (id, _) -> EcPath.mident id)
+                 newme.tme_expr.me_params)) in
+        let newme =
+          { newme with tme_expr =
+              { newme.tme_expr with me_name = name; me_body = alias } } in
+        ove.ovre_hooks.hadd_item scope ~import (Th_module newme)
+      else scope in
+
+    (subst, ops, proofs, scope)
+
 (* -------------------------------------------------------------------- *)
 and replay_export
   (ove : _ ovrenv) (subst, ops, proofs, scope) (import, p, lc)

src/ecUserMessages.ml

@@ -825,6 +825,7 @@ end = struct
     | OVK_Abbrev    -> "abbreviation"
     | OVK_Theory    -> "theory"
     | OVK_Lemma     -> "lemma/axiom"
+    | OVK_ModExpr   -> "module"
     | OVK_ModType   -> "module type"
 
   let pp_incompatible env fmt = function
@@ -867,9 +868,9 @@ end = struct
         msg "unknown %s `%s'"
           (string_of_ovkind kd) (string_of_qsymbol x)
 
-    | CE_ThyOverride x ->
-        msg "Cannot override theory `%s`: contains module or exception"
-          (string_of_qsymbol x)
+    | CE_ThyOverride (x, m) ->
+        msg "Cannot override theory `%s': contains stateful module `%s'"
+          (string_of_qsymbol x) (string_of_qsymbol m)
 
     | CE_UnkAbbrev x ->
         msg "unknown abbreviation: `%s'" (string_of_qsymbol x)
@@ -898,6 +899,15 @@ end = struct
         msg "module `%s` is incompatible"
           (string_of_qsymbol x)
 
+    | CE_ModStateful (x, path) ->
+        let path = List.take (List.length path - 1) path in
+        msg "module `%s' declares state and cannot be overridden"
+          (String.concat "." (fst x @ [snd x] @ path))
+
+    | CE_ModNotConcrete x ->
+        msg "module `%s' is not a concrete top-level module"
+          (string_of_qsymbol x)
+
     | CE_InvalidRE x ->
         msg "invalid regexp: `%s'" x