diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/logic/WaryClashFreeSubst.java b/keyext.rusty/src/main/java/org/key_project/rusty/logic/WaryClashFreeSubst.java new file mode 100644 index 00000000000..443d0463d3c --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/logic/WaryClashFreeSubst.java @@ -0,0 +1,75 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.logic; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.rusty.logic.op.LogicVariable; +import org.key_project.rusty.logic.op.RModality; +import org.key_project.rusty.logic.op.TermTransformer; +import org.key_project.rusty.logic.op.UpdateApplication; +import org.key_project.util.collection.ImmutableArray; + +/// De Bruijn substitution that does **not** push the replacement into "state-dependent" positions +/// — the post-formula of a modality, the target of an update application, or an operand of a +/// transformer. Occurrences in such positions are kept (and [#wasBlocked] is set), so the caller +/// can wrap the result in a residual substitution; occurrences elsewhere are substituted normally. +/// +/// Used by [org.key_project.rusty.logic.op.WarySubstOp] for non-rigid replacements. The +/// replacement is assumed ground (no free logic variables, e.g. a program variable), so no de +/// Bruijn shifting of the replacement is needed. +public class WaryClashFreeSubst { + private final Term s; + private final TermBuilder tb; + private boolean blocked = false; + + public WaryClashFreeSubst(Term s, TermBuilder tb) { + this.s = s; + this.tb = tb; + } + + /// Whether at least one occurrence was left unsubstituted because it sat below a protected + /// operator. + public boolean wasBlocked() { + return blocked; + } + + public Term apply(Term body) { + return apply1(body, 1, false); + } + + private Term apply1(Term t, int index, boolean below) { + if (t.op() instanceof LogicVariable lv && lv.getIndex() == index) { + if (below) { + // keep the variable below a modality/update/transformer; the caller re-wraps the + // substitution as a residual + blocked = true; + return t; + } + return s; + } + final int arity = t.arity(); + final Term[] newSubterms = new Term[arity]; + for (int i = 0; i < arity; i++) { + int subIndex = index; + if (t.op().bindVarsAt(i)) { + subIndex += t.varsBoundHere(i).size(); + } + newSubterms[i] = apply1(t.sub(i), subIndex, below || isProtected(t.op())); + } + return tb.tf().createTerm(t.op(), newSubterms, + (ImmutableArray) t.boundVars()); + } + + /// Whether the subterms of an `op`-rooted term are state dependent: a modality, an update + /// application, or a transformer. This is conservative for updates — the replacement is not + /// pushed into an update application at all (neither into the update nor behind it); the + /// update-simplification taclets take care of propagating into the update where sound. + static boolean isProtected(Operator op) { + return op instanceof RModality + || op == UpdateApplication.UPDATE_APPLICATION + || op instanceof TermTransformer; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/WarySubstOp.java b/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/WarySubstOp.java new file mode 100644 index 00000000000..557ec5b8682 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/WarySubstOp.java @@ -0,0 +1,50 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.logic.op; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.rusty.logic.Subst; +import org.key_project.rusty.logic.TermBuilder; +import org.key_project.rusty.logic.WaryClashFreeSubst; + +/// Wary first-order substitution operator (de Bruijn). Like [SubstOp] it replaces the bound +/// variable by the substituted term, but it does **not** push a *non-rigid* term across a modality, +/// behind an update, or into a transformer — doing so would be unsound, because the value of a +/// non-rigid term (e.g. a program variable) depends on the state. +/// +/// This mirrors KeY-Java's `WarySubstOp` / `WaryClashFreeSubst`, adapted to de Bruijn indices. +/// Capture avoidance is automatic under de Bruijn, so the only "wary" concern left is state +/// dependence: when the substituted term is non-rigid and the variable occurs below a protected +/// operator, the substitution is left unreduced (a residual `{\subst …}` term). The `subst_to_eq` +/// rule can then introduce a fresh rigid Skolem constant capturing the term's current value, after +/// which the (now rigid) substitution is pushed through soundly. +public final class WarySubstOp extends SubstOp { + + /// the wary substitution operator; the one actually used by the parser + public static final SubstOp SUBST = new WarySubstOp(new Name("subst")); + + private WarySubstOp(Name name) { + super(name); + } + + @Override + public Term apply(Term term, TermBuilder tb) { + final Term substTerm = term.sub(0); + final Term origTerm = term.sub(1); + if (substTerm.isRigid()) { + // a rigid term may be pushed anywhere + return new Subst(substTerm, tb).apply(origTerm); + } + // a non-rigid term is pushed into ordinary (state-independent) positions, e.g. the update + // of an update application, but NOT across a modality / behind an update / into a + // transformer; occurrences there are kept and wrapped in a residual substitution + final WaryClashFreeSubst cfs = new WaryClashFreeSubst(substTerm, tb); + final Term res = cfs.apply(origTerm); + if (cfs.wasBlocked()) { + return tb.subst(this, term.varsBoundHere(1).get(0), substTerm, res); + } + return res; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/builder/ExpressionBuilder.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/builder/ExpressionBuilder.java index 505ce6977b6..bea95adb896 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/builder/ExpressionBuilder.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/builder/ExpressionBuilder.java @@ -741,27 +741,38 @@ public Term visitQuantifierterm(KeYRustyParser.QuantifiertermContext ctx) { @Override public Object visitSubstitution_term(KeYRustyParser.Substitution_termContext ctx) { - SubstOp op = SubstOp.SUBST; + SubstOp op = WarySubstOp.SUBST; Namespace orig = variables(); AbstractSortedOperator v = accept(ctx.bv); unbindVars(orig); - if (v instanceof LogicVariable) { - // bindVar((LogicVariable) v); - throw new RuntimeException("TODO @ DD"); + // the substitution binds its own variable; declare it so that occurrences in the body + // resolve to it (de Bruijn index 1) + BoundVariable declared = null; + if (v instanceof BoundVariable bv) { + // a sort was given: visitOne_bound_variable already registered the bound variable + declared = bv; + bindVar(); + } else if (v instanceof LogicVariable lv) { + // no sort given and the name resolved to an enclosing variable: declare the + // substitution's own (shadowing) bound variable of the same sort + declared = bindVar(ctx.bv.id.getText(), lv.sort()); + v = declared; } else { + // schema variable (taclets) bindVar(); } Term a1 = accept(ctx.replacement); Term a2 = oneOf(ctx.atom_prefix(), ctx.unary_formula()); try { - Term result = - getServices().getTermBuilder().subst(op, (QuantifiableVariable) v, a1, a2); - return result; + return getServices().getTermBuilder().subst(op, (QuantifiableVariable) v, a1, a2); } catch (Exception e) { throw new BuildingException(ctx, e); } finally { unbindVars(orig); + if (declared != null) { + unbindVars(List.of(declared)); + } } } @@ -943,9 +954,11 @@ private Term toNum(String number) { @Override protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, KeYRustyParser.Formal_sort_argsContext genericArgsCtxt) { - // Might be quantified variable + // Might be quantified variable. Search from the innermost binder outwards so that, when + // several bound variables share a name, an occurrence binds to the innermost one + // (de Bruijn shadowing). var idx = -1; - for (int i = 0; i < boundVars.size(); ++i) { + for (int i = boundVars.size() - 1; i >= 0; --i) { if (varfuncName.equals(boundVars.get(i).name().toString())) { idx = i; break; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/pp/NotationInfo.java b/keyext.rusty/src/main/java/org/key_project/rusty/pp/NotationInfo.java index 23a829fbaa1..fb078958633 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/pp/NotationInfo.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/pp/NotationInfo.java @@ -92,7 +92,7 @@ private HashMap createDefaultNotation() { new Notation.ModalSVNotation(PRIORITY_MODALITY, PRIORITY_POST_MODALITY)); tbl.put(IfThenElse.IF_THEN_ELSE, new Notation.IfThenElse(PRIORITY_ATOM, "\\if")); // tbl.put(IfExThenElse.IF_EX_THEN_ELSE, new Notation.IfThenElse(PRIORITY_ATOM, "\\ifEx")); - tbl.put(SubstOp.SUBST, new Notation.Subst()); + tbl.put(WarySubstOp.SUBST, new Notation.Subst()); tbl.put(UpdateApplication.UPDATE_APPLICATION, new Notation.UpdateApplicationNotation()); tbl.put(UpdateJunctor.PARALLEL_UPDATE, new Notation.ParallelUpdateNotation()); diff --git a/keyext.rusty/src/test/java/org/key_project/rusty/parser/WarySubstAndShadowingTest.java b/keyext.rusty/src/test/java/org/key_project/rusty/parser/WarySubstAndShadowingTest.java new file mode 100644 index 00000000000..fa4cc52ed08 --- /dev/null +++ b/keyext.rusty/src/test/java/org/key_project/rusty/parser/WarySubstAndShadowingTest.java @@ -0,0 +1,81 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.parser; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.logic.sort.Sort; +import org.key_project.rusty.ast.expr.BlockExpression; +import org.key_project.rusty.logic.RustyBlock; +import org.key_project.rusty.logic.op.BoundVariable; +import org.key_project.rusty.logic.op.LogicVariable; +import org.key_project.rusty.logic.op.ProgramVariable; +import org.key_project.rusty.logic.op.SubstOp; +import org.key_project.rusty.logic.op.WarySubstOp; +import org.key_project.rusty.util.TacletForTests; +import org.key_project.util.collection.ImmutableSLList; + +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; + +/// Parser tests for de Bruijn substitution: concrete `{\subst …}` parsing, innermost binding of +/// shadowed quantified variables, and the wariness of the substitution operator (a non-rigid +/// replacement is not pushed across a modality). Uses the `testrules.key` signature (sort `s`, +/// predicate `p(s)`, constant `cnst -> s`, program variable `i: u32`). +public class WarySubstAndShadowingTest { + + @BeforeAll + static void setUp() { + TacletForTests.parse(); + } + + @Test + void shadowedQuantifiedVariableBindsInnermost() { + // the x in p(x) binds to the inner \forall (de Bruijn index 1), not the outer one + Term t = TacletForTests.parseTerm("\\forall s x;\\forall s x; p(x)"); + Term body = t.sub(0).sub(0); // p(x) + assertEquals(1, ((LogicVariable) body.sub(0).op()).getIndex()); + } + + @Test + void parseConcreteSubstitution() { + Term t = TacletForTests.parseTerm("{\\subst s x; cnst} p(x)"); + assertInstanceOf(SubstOp.class, t.op()); + Term body = t.sub(1); + assertEquals(1, ((LogicVariable) body.sub(0).op()).getIndex()); + + // cnst is rigid, so it is substituted: p(cnst) + var tb = TacletForTests.services().getTermBuilder(); + Term applied = WarySubstOp.SUBST.apply(t, tb); + Term expected = TacletForTests.parseTerm("p(cnst)"); + assertEquals(expected, applied); + } + + @Test + void nonRigidReplacementIsNotPushedAcrossModality() { + // {\subst u32 x; i}\<{}\>(x = i): i is a (non-rigid) program variable, so it is not pushed + // into the modality — the substitution is left as a residual. Built programmatically to + // avoid the empty-modality concrete syntax. + var services = TacletForTests.services(); + var tb = services.getTermBuilder(); + ProgramVariable i = + (ProgramVariable) services.getNamespaces().programVariables().lookup(new Name("i")); + Sort u32 = i.sort(); + + BoundVariable x = new BoundVariable(new Name("x"), u32); + Term lvX = tb.var(LogicVariable.create(1, u32)); + Term iTerm = tb.var(i); + RustyBlock emptyBlock = + new RustyBlock(new BlockExpression(ImmutableSLList.nil(), null)); + Term body = tb.dia(emptyBlock, tb.equals(lvX, iTerm)); // \<{}\>(x = i) + Term substTerm = tb.subst(WarySubstOp.SUBST, x, iTerm, body); + + Term applied = WarySubstOp.SUBST.apply(substTerm, tb); + assertEquals(substTerm, applied, + "a non-rigid replacement must not be pushed across a modality"); + } +}