From 5c7b39ac3ab02c3a676366b06c17fdb721b98add Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 14 Oct 2026 14:35:18 +0200 Subject: [PATCH] fix(clone): theory overrides of nested or overlapping theories Two problems with theory overrides `theory X <- T` in clones. An override of a nested theory, `theory B.A <- T`, was recorded under its last component, at the top level: an unrelated theory `A` of the cloned theory lost its import, and a second override `theory A <- T'` failed with an assertion failure. Theory overrides are now recorded under their full path, and a duplicate one is reported as such. A theory override together with a more specific override, as in: clone Leaf as L with theory B.A <- Arr, theory B <- B0. failed with an assertion failure, or reported a duplicate override when given in the other order. Theory overrides are now processed after the other overrides, the most specific first, and leave alone the items that already have an override: the more specific override wins, whatever the order. In particular, a theory `B` produced by a clone that overrode its sub-theory `A` with `theory A <- U` can now be threaded through further clones with `<-`. That sub-theory was cleared, so that `theory B <- B` alone fails, as `B.A` has no target; the clones give: theory B <- B, theory B.A <- U where `<=` was needed so far, at the cost of a copy of the threaded theory in every clone. Also, a clone now replays a theory alias with its substituted target, instead of the original one. --- src/ecThCloning.ml | 63 ++++++++++++++++++--- src/ecThCloning.mli | 2 + src/ecTheoryReplay.ml | 2 +- tests/clone-alias-target.ec | 23 ++++++++ tests/clone-theory-override-chain.ec | 74 +++++++++++++++++++++++++ tests/clone-theory-override-nested.ec | 57 +++++++++++++++++++ tests/clone-theory-override-specific.ec | 59 ++++++++++++++++++++ 7 files changed, 272 insertions(+), 8 deletions(-) create mode 100644 tests/clone-alias-target.ec create mode 100644 tests/clone-theory-override-chain.ec create mode 100644 tests/clone-theory-override-nested.ec create mode 100644 tests/clone-theory-override-specific.ec diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 7d49e32e4..93a208095 100644 --- a/src/ecThCloning.ml +++ b/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 diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli index 31a453703..2d1b56fa3 100644 --- a/src/ecThCloning.mli +++ b/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 = { diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 9502ea40b..ab811f9ed 100644 --- a/src/ecTheoryReplay.ml +++ b/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) (* -------------------------------------------------------------------- *) diff --git a/tests/clone-alias-target.ec b/tests/clone-alias-target.ec new file mode 100644 index 000000000..dd294fb4c --- /dev/null +++ b/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. diff --git a/tests/clone-theory-override-chain.ec b/tests/clone-theory-override-chain.ec new file mode 100644 index 000000000..3bdedb919 --- /dev/null +++ b/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. diff --git a/tests/clone-theory-override-nested.ec b/tests/clone-theory-override-nested.ec new file mode 100644 index 000000000..a3c8a27a0 --- /dev/null +++ b/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. diff --git a/tests/clone-theory-override-specific.ec b/tests/clone-theory-override-specific.ec new file mode 100644 index 000000000..6a95d3c3e --- /dev/null +++ b/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. +