fix(clone): theory overrides of nested or overlapping theories

src/ecThCloning.ml

@@ -87,6 +87,7 @@ type evclone = {
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
   evc_ths      : (evclone * bool) Msym.t;
+  evc_target   : EcPath.path option;
 }
 
 
@@ -108,7 +109,8 @@ let evc_empty =
       evc_modexprs = Msym.empty;
       evc_modtypes = Msym.empty;
       evc_lemmas   = evl;
-      evc_ths      = Msym.empty; }
+      evc_ths      = Msym.empty;
+      evc_target   = None; }
 
 let rec evc_update (upt : evclone -> evclone) (nm : symbol list) (evc : evclone) =
   match nm with
@@ -519,12 +521,48 @@ end = struct
         List.find_map (fun rnm -> rename rnm (kind, name)) prerenames
       with Not_found -> name in
 
-    assert (not (Msym.mem x evc.evc_ths));
+    let evc =
+      evc_update
+        (fun evc ->
+          let ths =
+            Msym.change (fun sub ->
+              let sub, clear = odfl (evc_empty, false) sub in
+              if is_some sub.evc_target then
+                clone_error oc.oc_env (CE_DupOverride (OVK_Theory, name));
+              let sub = { sub with evc_target = Some sp } in
+              Some (sub, clear || (mode <> `Alias)))
+            x evc.evc_ths
+          in { evc with evc_ths = ths })
+        nm evc in
+
+    (* A more specific override takes precedence over the one implied
+     * by the theory override. *)
+    let overridden (prefix : symbol list) (dth : theory_item_r) =
+      let sub = odfl evc_empty (evc_get (xdth @ prefix) evc) in
 
-    let evc = { evc with
-      evc_ths = Msym.change (fun sub ->
-        let sub, clear = odfl (evc_empty, false) sub in
-        Some (sub, clear || (mode <> `Alias))) x evc.evc_ths } in
+      match dth with
+      | Th_type (x, _) ->
+         Msym.mem x sub.evc_types
+      | Th_operator (x, { op_kind = OB_oper _ }) ->
+         Msym.mem x sub.evc_ops
+      | Th_operator (x, { op_kind = OB_pred _ }) ->
+         Msym.mem x sub.evc_preds
+      | Th_operator (x, { op_kind = OB_nott _ }) ->
+         Msym.mem x sub.evc_abbrevs
+      | Th_module me ->
+         Msym.mem me.tme_expr.me_name sub.evc_modexprs
+      | Th_modtype (x, _) ->
+         Msym.mem x sub.evc_modtypes
+      | Th_theory (x, _) ->
+         Msym.find_opt x sub.evc_ths
+           |> obind (fun (sub, _) -> sub.evc_target)
+           |> is_some
+      | Th_axiom (x, _) ->
+         List.exists (fun prf ->
+           match prf.pthp_mode with
+           | `Named (y, _) -> unloc y = (xdth @ prefix, x)
+           | `All _ -> false) proofs
+      | _ -> false in
 
     let rec doit_r (prefix, tgprefix) (proofs, evc) dth =
       let dtpath (x : symbol) =
@@ -534,6 +572,8 @@ end = struct
         let x = Option.fold ~none:x ~some:(fun k -> rename (k, x)) kind in
         EcPath.fromqsymbol (thd @ tgprefix, x) in
 
+      if overridden prefix dth then (proofs, evc) else
+
       match dth with
       | Th_type (x, _) ->
          let ovrd = `ByPath (tgpath ~kind:`Type x), mode in
@@ -677,10 +717,19 @@ let clone (scenv : EcSection.scenv) (thcl : theory_cloning) =
   let name = odfl (EcPath.basename opath) (thcl.pthc_name |> omap unloc) in
   let oc   = { oc_env = env; oc_oth = oth; } in
 
+  (* Theory overrides are processed last, the most specific first: a
+   * theory override does not override the items that already have an
+   * override, so that the more specific override wins. *)
+  let ovrds =
+    let isth = function (_, PTHO_Theory _) -> true | _ -> false in
+    let ths, others = List.partition isth thcl.pthc_ext in
+    let depth (name, _) = List.length (fst (unloc name)) in
+    others @ List.stable_sort (fun o1 o2 -> compare (depth o2) (depth o1)) ths in
+
   let (genproofs, ovrds) =
     List.fold_left
       (fun st -> curry (OVRD.ovrd oc st))
-      ([], evc_empty) thcl.pthc_ext
+      ([], evc_empty) ovrds
   in
 
   let ovrds = List.fold_left (Proofs.proof ~intheory:true oc) ovrds genproofs in

src/ecThCloning.mli

@@ -69,6 +69,8 @@ type evclone = {
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
   evc_ths      : (evclone * bool) Msym.t;
+  evc_target   : EcPath.path option;
+    (* the target of the theory override of this (sub-)theory, if any *)
 }
 
 and evlemma = {

src/ecTheoryReplay.ml

@@ -1324,7 +1324,7 @@ and replay_alias
   if is_none (EcEnv.Theory.by_path_opt p env) then
     (subst, ops, proofs, scope)
   else
-    let scope = ove.ovre_hooks.hadd_item scope ~import (Th_alias (name, target)) in
+    let scope = ove.ovre_hooks.hadd_item scope ~import (Th_alias (name, p)) in
     (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)

tests/clone-alias-target.ec

@@ -0,0 +1,23 @@
+(* A clone replays a theory alias with its target substituted: an alias
+   to a theory of the cloned theory points to its copy in the clone. It
+   used to keep pointing to the original theory, printed `T.X`. *)
+
+theory T.
+  theory X.
+    type u.
+  end X.
+
+  theory Y = X.
+end T.
+
+clone T as T1.
+
+expect "
+theory T1.
+  (* import *) theory X.
+                 (* import *) type u.
+               end X.
+
+  (* import *) theory Y = X.
+end T1.
+" by print theory T1.

tests/clone-theory-override-chain.ec

@@ -0,0 +1,74 @@
+(* Threading theories through a chain of clones with theory overrides
+   `theory B <- B`, when `B` was produced by a clone that overrode its
+   sub-theory `A` with `theory A <- Arr`. That sub-theory was cleared:
+   each clone that threads `B` gives `theory B.A <- Arr` as well, which
+   takes precedence over `theory B <- B` for `B.A`. *)
+
+require import AllCore.
+
+theory Arr.
+  type 'a t.
+  op get : 'a t -> int -> 'a.
+end Arr.
+
+abstract theory Base.
+  theory A.
+    type 'a t.
+    op get : 'a t -> int -> 'a.
+  end A.
+
+  op k : int.
+end Base.
+
+abstract theory PreludeT.
+  clone import Base as B.
+
+  op f (x : int A.t) = A.get x k.
+  lemma f_def x : f x = A.get x k by done.
+end PreludeT.
+
+abstract theory RowT.
+  clone import Base as B.
+  clone import PreludeT as PR with theory B <- B.
+
+  op g (x : int A.t) = PR.f x + 1.
+  lemma g_def x : g x = A.get x k + 1 by rewrite /g PR.f_def.
+end RowT.
+
+abstract theory TopT.
+  clone import Base as B.
+  clone import PreludeT as PR with theory B <- B.
+  clone import RowT as RV with theory B <- B, theory PR <- PR.
+
+  lemma top x : RV.g x = A.get x k + 1 by apply RV.g_def.
+end TopT.
+
+abstract theory Chain.
+  clone import Base as B with theory A <- Arr.
+
+  clone import PreludeT as PR with
+    theory B <- B, theory B.A <- Arr.
+
+  clone import RowT as RV with
+    theory B <- B, theory B.A <- Arr, theory PR <- PR.
+
+  clone import TopT as T with
+    theory B <- B, theory B.A <- Arr, theory PR <- PR, theory RV <- RV.
+
+  expect "
+(* Chain.T.top (shorten name: top) *)
+lemma top: forall (x : int Arr.t), g x = Arr.get x k + 1.
+" by print lemma T.top.
+end Chain.
+
+(* With `<=`, the sub-theory is kept, and `theory B <- B` suffices. *)
+abstract theory Kept.
+  clone import Base as B with theory A <= Arr.
+  clone import PreludeT as PR with theory B <- B.
+  clone import RowT as RV with theory B <- B, theory PR <- PR.
+
+  expect "
+(* Kept.RV.g_def (shorten name: g_def) *)
+lemma g_def: forall (x : int Arr.t), g x = Arr.get x k + 1.
+" by print lemma RV.g_def.
+end Kept.

tests/clone-theory-override-nested.ec

@@ -0,0 +1,57 @@
+(* A theory override of a nested theory, `theory B.A <- T`, concerns
+   `B.A` only. It used to be recorded under its last component `A`: an
+   unrelated top-level theory `A` lost its import, and a second override
+   `theory A <- T'` was rejected by an assertion failure. *)
+
+require import AllCore.
+
+theory Arr.
+  type 'a t.
+  op get : 'a t -> int -> 'a.
+end Arr.
+
+theory Arr2.
+  type u.
+end Arr2.
+
+abstract theory Base.
+  theory A.
+    type 'a t.
+    op get : 'a t -> int -> 'a.
+  end A.
+end Base.
+
+abstract theory Leaf.
+  clone import Base as B.
+
+  theory A.
+    type u.
+  end A.
+
+  op h : A.u -> int B.A.t.
+end Leaf.
+
+(* The top-level `A` is still imported. *)
+clone Leaf as L1 with theory B.A <- Arr.
+
+expect "
+theory L1.
+  (* import *) theory A.
+                 (* import *) type u.
+               end A.
+
+  (* import *) op h : A.u -> int Arr.t.
+end L1.
+" by print theory L1.
+
+(* `B.A` and `A` are overridden independently. *)
+clone Leaf as L2 with theory B.A <- Arr, theory A <- Arr2.
+
+expect "
+(* L2.h *)
+op h : Arr2.u -> int Arr.t.
+" by print op L2.h.
+
+(* Overriding the same theory twice is an error. *)
+expect fail "the theory `B.A' is instantiate twice"
+clone Leaf as L3 with theory B.A <- Arr, theory B.A <- Arr.

tests/clone-theory-override-specific.ec

@@ -0,0 +1,59 @@
+(* A theory override `theory B <- T` does not override the items of `B`
+   that have a more specific override, whatever the order in which the
+   two overrides are given. It used to fail with an assertion failure
+   when the more specific override came first, and to report a
+   duplicate override otherwise. *)
+
+require import AllCore.
+
+theory Arr.
+  type 'a t.
+  op get : 'a t -> int -> 'a.
+end Arr.
+
+theory Arr2.
+  type 'a t.
+  op get : 'a t -> int -> 'a.
+end Arr2.
+
+abstract theory Base.
+  theory A.
+    type 'a t.
+    op get : 'a t -> int -> 'a.
+  end A.
+
+  op k : int.
+end Base.
+
+abstract theory Leaf.
+  clone import Base as B.
+
+  lemma leaflm (x : int A.t) : A.get x k = A.get x k by done.
+end Leaf.
+
+clone Base as B0 with theory A <= Arr.
+
+(* The more specific override first... *)
+clone Leaf as L1 with theory B.A <- Arr2, theory B <- B0.
+
+expect "
+(* L1.leaflm *)
+lemma leaflm: forall (x : int Arr2.t), Arr2.get x B0.k = Arr2.get x B0.k.
+" by print lemma L1.leaflm.
+
+(* ... or last. *)
+clone Leaf as L2 with theory B <- B0, theory B.A <- Arr2.
+
+expect "
+(* L2.leaflm *)
+lemma leaflm: forall (x : int Arr2.t), Arr2.get x B0.k = Arr2.get x B0.k.
+" by print lemma L2.leaflm.
+
+(* The same holds for an override of a single item. *)
+clone Leaf as L3 with theory B <- B0, op B.k <- 0.
+
+expect "
+(* L3.leaflm *)
+lemma leaflm: forall (x : int Arr.t), Arr.get x 0 = Arr.get x 0.
+" by print lemma L3.leaflm.
+