From 7a8f45f54b3c85003061308a37cc16276d1598b3 Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Thu, 30 Jul 2026 19:59:51 -0700 Subject: [PATCH] replay: redirect datatype constructors in match bodies too When a datatype's type is overridden while cloning, replay_tyd redirects the source constructors to the target's constructors with EcSubst.add_opdef. That map is consulted only where a constructor occurs as an operator expression, so the constructors stored as bare paths in the branches of a match body (OP_Fix) were left pointing at the source datatype. The operator-compatibility check compares those paths for equality, so it raised CoreIncompatible, which Compatible.for_operator does not convert and which therefore surfaced as an anomaly. Record the redirect in a dedicated map, sb_ctor, and consult it where opb_ctor is substituted, falling back to the previous behaviour on a miss. A sb_path entry would not do: _subst_path recurses into qualifiers, so keying it on a constructor path would also rewrite the paths that constructor qualifies, and constructor names share a namespace with sub-theories, types and modules. Adds tests/clone-datatype-match.ec. Fixes #1046. Signed-off-by: Onyeka Obi --- src/ecSubst.ml | 17 ++++++++- src/ecSubst.mli | 1 + src/ecTheoryReplay.ml | 12 +++++-- tests/clone-datatype-match.ec | 67 +++++++++++++++++++++++++++++++++++ 4 files changed, 93 insertions(+), 4 deletions(-) create mode 100644 tests/clone-datatype-match.ec diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 6dbf75ad4..bbf6727c6 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -27,6 +27,7 @@ exception InconsistentSubst type subst = { sb_module : EcPath.mpath Mid.t; sb_path : EcPath.path Mp.t; + sb_ctor : EcPath.path Mp.t; sb_tyvar : ty Mid.t; sb_elocal : expr Mid.t; sb_flocal : EcCoreFol.form Mid.t; @@ -40,6 +41,7 @@ type subst = { let empty : subst = { sb_module = Mid.empty; sb_path = Mp.empty; + sb_ctor = Mp.empty; sb_tyvar = Mid.empty; sb_elocal = Mid.empty; sb_flocal = Mid.empty; @@ -52,6 +54,7 @@ let empty : subst = { let is_empty s = Mid.is_empty s.sb_module && Mp.is_empty s.sb_path + && Mp.is_empty s.sb_ctor && Mid.is_empty s.sb_tyvar && Mid.is_empty s.sb_elocal && Mid.is_empty s.sb_flocal @@ -272,6 +275,10 @@ let add_path (s : subst) ~src ~dst = assert (Mp.find_opt src s.sb_path = None); { s with sb_path = Mp.add src dst s.sb_path } +(* -------------------------------------------------------------------- *) +let add_ctor (s : subst) ~src ~dst = + { s with sb_ctor = Mp.add src dst s.sb_ctor } + let add_tydef (s : subst) p (ids, ty) = assert (Mp.find_opt p s.sb_tydef = None); { s with sb_tydef = Mp.add p (ids, ty) s.sb_tydef } @@ -932,7 +939,15 @@ and subst_branches (s : subst) = function | OPB_Branch bs -> let for1 b = let (ctorp, ctori) = b.opb_ctor in - { opb_ctor = (subst_path s ctorp, ctori); + (* A branch constructor is stored as a bare path. When the datatype's + type has been overridden while cloning, it is redirected to the + target datatype's constructor, which is recorded separately from + the path substitution: the latter also rewrites the paths that its + entries qualify, which a constructor must not do. *) + let ctorp = + Option.value (Mp.find_opt ctorp s.sb_ctor) + ~default:(subst_path s ctorp) in + { opb_ctor = (ctorp, ctori); opb_sub = subst_branches s b.opb_sub; } in OPB_Branch (Parray.map for1 bs) diff --git a/src/ecSubst.mli b/src/ecSubst.mli index 64ae60cf0..b5639ff1f 100644 --- a/src/ecSubst.mli +++ b/src/ecSubst.mli @@ -25,6 +25,7 @@ val is_empty : subst -> bool (* -------------------------------------------------------------------- *) val add_module : subst -> EcIdent.t -> mpath -> subst val add_path : subst -> src:path -> dst:path -> subst +val add_ctor : 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 diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 380bc501d..333ba927d 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -574,9 +574,15 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd List.map (CS.Tvar.subst tysubst -| EcSubst.subst_ty subst) tyargs in - EcSubst.add_opdef subst - (xpath ove name) - (newtparams, e_op np newtparams_ty (toarrow newtyargs newdtype)) + let subst = + EcSubst.add_opdef subst + (xpath ove name) + (newtparams, e_op np newtparams_ty (toarrow newtyargs newdtype)) in + (* The definition above rewrites the constructor where it + occurs as an operator expression. The branches of a match + body store it as a bare path, which is redirected through + its own substitution. *) + EcSubst.add_ctor subst ~src:(xpath ove name) ~dst:np ) subst octors | _ -> subst end diff --git a/tests/clone-datatype-match.ec b/tests/clone-datatype-match.ec new file mode 100644 index 000000000..5f6bf5ac1 --- /dev/null +++ b/tests/clone-datatype-match.ec @@ -0,0 +1,67 @@ +(* Regression test for issue #1046. + + When a datatype's type is overridden during cloning, an operator whose + body pattern-matches on the datatype's constructors (i.e. compiles to + `OP_Fix`) used to crash with `anomaly: EcTheoryReplay.CoreIncompatible`. + The replay machinery redirects the source datatype's constructors to the + target datatype's constructors only through operator definitions + (`Fop`/`Eop` expression nodes), so the constructor *paths* stored in + `OP_Fix` match branches were left pointing at the source datatype and the + operator-compatibility check saw unequal constructor paths. + + Both override modes must accept these clones. *) + +require import Int. + +theory Thy. + type ATy = [ CA | CB of int ]. + + op getit (x : ATy) = + with x = CA => 0 + with x = CB n => n. + + op mk = CB 3. +end Thy. + +clone Thy as Thy1. + +(* plain alias override *) +clone Thy as Thy2 with + type ATy = Thy1.ATy, + op getit <= Thy1.getit, + op mk <= Thy1.mk. + +(* inline override *) +clone Thy as Thy3 with + type ATy <- Thy1.ATy, + op getit <= Thy1.getit, + op mk <= Thy1.mk. + +(* No operator override: the replayed match operator must have its branch + constructors redirected to the target datatype, so it reduces on the + target's constructor applications. *) +clone Thy as Thy4 with + type ATy = Thy1.ATy. + +lemma getit4 : Thy4.getit (Thy1.CB 5) = 5. +proof. done. qed. + +(* Recursive match operator: exercises the recursive occurrence + (opf_recp) together with the constructor redirect. Only the inline + override is checked here: aliasing the type of a *recursive* datatype + is rejected by the type-compatibility check for an unrelated reason + (the constructor argument that mentions the datatype itself is not + redirected), independently of this fix. *) +theory RThy. + type RTy = [ RNil | RCons of int & RTy ]. + + op total (x : RTy) = + with x = RNil => 0 + with x = RCons n xs => n + total xs. +end RThy. + +clone RThy as RThy1. + +clone RThy as RThy2 with + type RTy <- RThy1.RTy, + op total <= RThy1.total.