feat: parametric cast function + cast insertion in taclet application

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;
             }

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<GenericArgument> args = ImmutableSLList.singleton(new SortArg(sort));
+        ParametricFunctionInstance castFn = ParametricFunctionInstance.get(decl, args);
+        return tf.createTerm(castFn, term);
+    }
+
     // -------------------------------------------------------------------------
     // constructors for special classes of term operators
     // -------------------------------------------------------------------------

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();
+    }
 }

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)
+    };
+}

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

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;