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)
triggers an anomaly during the operator-compatibility check.
MRE
theory Thy.
type ATy = [ CB of int ].
op getit (x : ATy) = with x = CB n => n.
end Thy.
clone Thy as Thy1.
clone Thy as Thy2 with
type ATy = Thy1.ATy,
op getit <= Thy1.getit.
Result:
anomaly: EcLib.EcTheoryReplay.CoreIncompatible
Reproduces on main in both override modes (type ATy = ... and type ATy <- ...).
Cause
Same root cause as #989: when a datatype's type is overridden, the source
datatype's constructors are not re-created in the clone, so references to them
must be redirected to the target datatype's constructors.
EcTheoryReplay.replay_tyd performs this redirect only for OP_Constr
references, not for OP_Fix match bodies.
PR #1045 (fixing #989) extends the redirect to plain constructor references in
both override modes, but does not widen it to OP_Fix.
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)triggers an anomaly during the operator-compatibility check.
MRE
Result:
Reproduces on
mainin both override modes (type ATy = ...andtype ATy <- ...).Cause
Same root cause as #989: when a datatype's type is overridden, the source
datatype's constructors are not re-created in the clone, so references to them
must be redirected to the target datatype's constructors.
EcTheoryReplay.replay_tydperforms this redirect only forOP_Constrreferences, not for
OP_Fixmatch bodies.PR #1045 (fixing #989) extends the redirect to plain constructor references in
both override modes, but does not widen it to
OP_Fix.