Remove module overriding when cloning a theory. (#458)

Author: Cameron-Low

src/ecParser.mly

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

src/ecParsetree.ml

@@ -1191,7 +1191,6 @@ 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/ecThCloning.ml

@@ -23,13 +23,13 @@ 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_UnkAbbrev         of qsymbol
 | CE_TypeArgMism       of ovkind * qsymbol
 | CE_OpIncompatible    of qsymbol * incompatible
@@ -335,26 +335,6 @@ end = struct
                pthp_tactic = Some tc; } in
     (pr :: proofs, evc)
 
-  (* ------------------------------------------------------------------ *)
-  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));
-      | _ -> () 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
@@ -388,6 +368,18 @@ end = struct
       | Some ({cth_mode = `Concrete} as th) -> th
     in
 
+    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 sp =
       match EcEnv.Theory.lookup_opt (unloc thd) oc.oc_env with
       | None -> clone_error oc.oc_env (CE_UnkOverride (OVK_Theory, unloc thd))
@@ -436,10 +428,8 @@ end = struct
       | Th_export _ ->
          (proofs, evc)
 
-      | Th_module m ->
-         modexpr_ovrd
-           oc (proofs, evc) (loced (xdth @ prefix, m.tme_expr.me_name))
-           (loced (thd @ prefix, m.tme_expr.me_name), mode)
+      | Th_module _ ->
+         (proofs, evc)
 
       | Th_modtype (x, _) ->
          modtype_ovrd
@@ -474,9 +464,6 @@ 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

@@ -17,13 +17,13 @@ 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_UnkAbbrev         of qsymbol
 | CE_TypeArgMism       of ovkind * qsymbol
 | CE_OpIncompatible    of qsymbol * incompatible

src/ecUserMessages.ml

@@ -703,7 +703,6 @@ 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
@@ -735,6 +734,10 @@ end = struct
         msg "unknown %s `%s'"
           (string_of_ovkind kd) (string_of_qsymbol x)
 
+    | CE_ThyOverride x ->
+        msg "Cannot override theory `%s`: contains module"
+          (string_of_qsymbol x)
+
     | CE_UnkAbbrev x ->
         msg "unknown abbreviation: `%s'" (string_of_qsymbol x)