diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java index 0ce6ffefce0..5ae9b318d38 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/InfiniteLoopExpression.java @@ -12,6 +12,7 @@ import org.key_project.rusty.ast.Label; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.ast.abstraction.Never; +import org.key_project.rusty.ast.abstraction.TupleType; import org.key_project.rusty.ast.abstraction.Type; import org.key_project.rusty.ast.visitor.RustyASTWalker; import org.key_project.rusty.ast.visitor.Visitor; @@ -87,10 +88,11 @@ private Type computeType(Services services) { return Never.INSTANCE; } var breaksIt = breaks.iterator(); - Type tyMax = breaksIt.next().type(services); + Expr expr = breaksIt.next().expr(); + Type tyMax = expr == null ? TupleType.UNIT : expr.type(services); while (breaksIt.hasNext()) { - var b = breaksIt.next(); - var ty = b.type(services); + expr = breaksIt.next().expr(); + var ty = expr == null ? TupleType.UNIT : expr.type(services); if (ty == Never.INSTANCE) { continue; } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java b/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java index b7e2fccc900..5e69a37a3d7 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/logic/TermBuilder.java @@ -54,6 +54,25 @@ public TermFactory tf() { return tf; } + private static final Name CAST_NAME = new Name("cast"); + + /// Builds `cast<[sort]>(term)`, reinterpreting `term` as `sort` via the parametric `cast` + /// function (see cast.key). Returns `term` unchanged when it already has that sort, or when the + /// `cast` operator is not declared. + public Term cast(Sort sort, Term term) { + if (term.sort() == sort) { + return term; + } + ParametricFunctionDecl decl = + services.getNamespaces().parametricFunctions().lookup(CAST_NAME); + if (decl == null) { + return term; + } + ImmutableList args = ImmutableSLList.singleton(new SortArg(sort)); + ParametricFunctionInstance castFn = ParametricFunctionInstance.get(decl, args); + return tf.createTerm(castFn, term); + } + // ------------------------------------------------------------------------- // constructors for special classes of term operators // ------------------------------------------------------------------------- diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java index 45cf4a5a072..33f629f0c1b 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/RewriteTacletExecutor.java @@ -6,12 +6,15 @@ import org.key_project.logic.IntIterator; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.op.SortedOperator; import org.key_project.logic.sort.Sort; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentChangeInfo; import org.key_project.prover.sequent.SequentFormula; import org.key_project.rusty.Services; +import org.key_project.rusty.logic.RustyDLTheory; +import org.key_project.rusty.logic.op.IfThenElse; import org.key_project.rusty.proof.Goal; import org.key_project.rusty.rule.MatchConditions; import org.key_project.rusty.rule.RuleApp; @@ -101,8 +104,7 @@ private Term replace(Term term, Term with, PosInOccurrence posOfFind, IntIterato final Term[] subs = new Term[term.arity()]; term.subs().arraycopy(0, subs, 0, term.arity()); - final Sort newMaxSort = maxSort; // TODO? TermHelper.getMaxSort(term, - // indexOfNextSubTerm); + final Sort newMaxSort = getMaxSort(term, indexOfNextSubTerm); subs[indexOfNextSubTerm] = replace(term.sub(indexOfNextSubTerm), with, posOfFind, it, mc, newMaxSort, goal, services, ruleApp); @@ -112,12 +114,28 @@ private Term replace(Term term, Term with, PosInOccurrence posOfFind, IntIterato with = syntacticalReplace(with, posOfFind, mc, goal, ruleApp, services); - /* - * if (!with.sort().extendsTrans(maxSort)) { - * with = services.getTermBuilder().cast(maxSort, with); - * } - */ + // If the replacewith result does not fit the sort required at this position, wrap it in a + // cast so the surrounding term stays well-sorted (mirrors KeY's RewriteTacletExecutor). + if (!with.sort().extendsTrans(maxSort)) { + with = services.getTermBuilder().cast(maxSort, with); + } return with; } + + /// The maximal sort allowed at the `i`-th argument of `term` (port of KeY's + /// `TermHelper.getMaxSort`): a formula stays a formula, the branches of an if-then-else may + /// carry the if-then-else's own sort, and otherwise the operator's declared argument sort. + private static Sort getMaxSort(Term term, int i) { + if (term.sub(i).sort() == RustyDLTheory.FORMULA) { + return RustyDLTheory.FORMULA; + } + if (term.op() instanceof IfThenElse && i > 0) { + return term.sort(); + } + if (term.op() instanceof SortedOperator sortedOp) { + return sortedOp.argSort(i); + } + return term.sub(i).sort(); + } } diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key new file mode 100644 index 00000000000..b641c37ccb9 --- /dev/null +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/cast.key @@ -0,0 +1,41 @@ +/* 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 */ + +/* + * Casts in the logic. + * + * A parametric cast function `cast<[E]>(any) -> E` reinterprets a value of any + * sort as the type parameter `E` (the counterpart of the parametric `ghost<[E]>` + * / `read<[E]>` functions). It is meant to be inserted by the taclet-application + * logic (RewriteTacletExecutor) so that a replacewith result of the top sort + * `any` is given the concrete sort required by its position. + * + * The taclets are adapted from the cast family of legacy KeY's genericRules.key + * (castDel, nested-cast collapse). They are deliberately conservative. + */ + +\sorts { + \generic alpha; + \generic beta; +} + +\functions { + cast<[E]>(any) -> E; +} + +\schemaVariables { + \term any castArg; + \term alpha castAlphaArg; +} + +\rules { + // genericRules.key: castDel + // A cast to a sort the argument already has is the identity. `castAlphaArg : alpha` only + // matches an argument whose sort already fits `alpha`, so a genuine narrowing cast is not removed. + castDel { + \find(cast<[alpha]>(castAlphaArg)) + \replacewith(castAlphaArg) + \heuristics(simplify, cast_deletion) + }; +} diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key index 81f8845eab5..8aeea3a95f5 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ruleSetDeclarations.key @@ -33,6 +33,7 @@ split_cond; simplify; + cast_deletion; simplify_enlarging; simplify_ENLARGING; // Simplification rules which make formulas much bigger // and therefore should be used less frequently than diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key index 43db1710452..6e2b10bbad1 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/standardRustRules.key @@ -8,6 +8,7 @@ // general propositional and first-order rules \include propRule; \include firstOrderRules; +\include cast; \include ifThenElseRules; \include formulaNormalizationRules; \include updateRules;