SemiSequent and EqualsModProperty

keyext.rusty_while/src/main/java/org/key_project/rusty/ast/stmt/LetStatement.java

@@ -36,6 +36,14 @@ public int getChildCount() {
         return 3;
     }
 
+    public Type getType() {
+        return type;
+    }
+
+    public Pattern getPattern() {
+        return pat;
+    }
+
     @Override
     public String toString() {
         return "let " + pat + ": " + type + " = " + init;

keyext.rusty_while/src/main/java/org/key_project/rusty/logic/FormulaChangeInfo.java

@@ -0,0 +1,21 @@
+package org.key_project.rusty.logic;
+
+public record FormulaChangeInfo(PosInOccurrence positionOfModification, SequentFormula newFormula) {
+
+    public SequentFormula getOriginalFormula() {
+        return positionOfModification().sequentFormula();
+    }
+
+    /**
+     * @return position within the original formula
+     */
+    @Override
+    public PosInOccurrence positionOfModification() {
+        return positionOfModification;
+    }
+
+    public String toString() {
+        return "Replaced " + positionOfModification + " with " + newFormula;
+    }
+
+}

keyext.rusty_while/src/main/java/org/key_project/rusty/logic/NameAbstractionTable.java

@@ -0,0 +1,60 @@
+package org.key_project.rusty.logic;
+
+import org.key_project.rusty.ast.RustyProgramElement;
+
+import java.util.Iterator;
+import java.util.LinkedList;
+import java.util.List;
+
+public class NameAbstractionTable {
+
+    /**
+     * The order in which symbols are declared in the two terms or programs that are compared. The
+     * latest declaration of a symbol will be the first matching entry in the list
+     */
+    private List<RustyProgramElement> declarations0 = null, declarations1 = null;
+
+    /**
+     * adds the given two elements to the table
+     *
+     * @param pe1 RustyProgramElement to be added
+     * @param pe2 RustyProgramElement to be added
+     */
+    public void add(RustyProgramElement pe1, RustyProgramElement pe2) {
+        if (declarations0 == null) {
+            declarations0 = new LinkedList<>();
+            declarations1 = new LinkedList<>();
+        }
+
+        declarations0.add(0, pe1);
+        declarations1.add(0, pe2);
+    }
+
+    /**
+     * tests if the given elements have been assigned to the same abstract name.
+     *
+     * @param pe0 RustyProgramElement
+     * @param pe1 RustyProgramElement
+     * @returns true if the pe1 and pe2 have been assigned to the same name
+     */
+    public boolean sameAbstractName(RustyProgramElement pe0, RustyProgramElement pe1) {
+        if (declarations0 != null) {
+            final Iterator<RustyProgramElement> it0 = declarations0.iterator();
+            final Iterator<RustyProgramElement> it1 = declarations1.iterator();
+
+            while (it0.hasNext()) {
+                // both lists are assumed to hold the same number of elements
+                final Object o0 = it0.next();
+                final Object o1 = it1.next();
+
+                if (pe0.equals(o0)) {
+                    return pe1.equals(o1);
+                } else if (pe1.equals(o1)) {
+                    return false;
+                }
+            }
+        }
+
+        return pe0.equals(pe1);
+    }
+}

keyext.rusty_while/src/main/java/org/key_project/rusty/logic/Semisequent.java

@@ -10,6 +10,8 @@
 
 import org.jspecify.annotations.NonNull;
 
+import static org.key_project.rusty.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
+
 public class Semisequent implements Iterable<SequentFormula> {
     /** the empty semisequent (using singleton pattern) */
     public static final Semisequent EMPTY_SEMISEQUENT = new Empty();
@@ -21,6 +23,18 @@ private Semisequent() {
         seqList = ImmutableSLList.nil();
     }
 
+    /**
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided list must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
+     *
+     * @param seqList list of sequent formulas
+     */
+    public Semisequent(ImmutableList<SequentFormula> seqList) {
+        assert !seqList.isEmpty();
+        this.seqList = seqList;
+    }
+
     /**
      * creates a new Semisequent with the Semisequent elements in seqList
      */
@@ -34,7 +48,7 @@ public Semisequent(SequentFormula seqFormula) {
      * returning same semisequent if inserting would create redundancies
      *
      * @param idx int encoding the place the element has to be put
-     * @param sequentFormula {@link de.uka.ilkd.key.logic.SequentFormula} to be inserted
+     * @param sequentFormula {@link SequentFormula} to be inserted
      * @return a semi sequent change information object with the new semisequent and information
      *         which formulas have been added or removed
      */
@@ -63,6 +77,75 @@ public boolean isEmpty() {
         return seqList.isEmpty();
     }
 
+    /**
+     * inserts new SequentFormula at index idx and removes duplicates, perform simplifications etc.
+     *
+     * @param fci null if the formula to be added is new, otherwise an object telling which formula
+     *        is replaced with the new formula <code>sequentFormula</code>, and what are the
+     *        differences between the two formulas
+     * @return a semi sequent change information object with the new semisequent and information
+     *         which formulas have been added or removed
+     */
+    private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx,
+                                                                  SequentFormula sequentFormula, SemisequentChangeInfo semiCI, FormulaChangeInfo fci) {
+
+        // Search for equivalent formulas and weakest constraint
+        ImmutableList<SequentFormula> searchList = semiCI.getFormulaList();
+        final SequentFormula[] newSeqList = new SequentFormula[searchList.size()];
+        SequentFormula cf;
+        int pos = -1;
+
+        while (!searchList.isEmpty()) {
+            ++pos;
+            cf = searchList.head();
+            searchList = searchList.tail();
+
+            if (sequentFormula != null
+                    && RENAMING_TERM_PROPERTY.equalsModThisProperty(cf.formula(), sequentFormula.formula())) {
+                semiCI.rejectedFormula(sequentFormula);
+                return semiCI; // semisequent already contains formula
+
+            }
+            newSeqList[pos] = cf;
+        }
+
+
+        // compose resulting formula list
+        if (fci == null) {
+            semiCI.addedFormula(idx, sequentFormula);
+        } else {
+            semiCI.modifiedFormula(idx, fci);
+        }
+
+        final ImmutableList<SequentFormula> orig = semiCI.getFormulaList();
+        pos = Math.min(idx, orig.size());
+
+        searchList = semiCI.getFormulaList().take(pos).prepend(sequentFormula);
+
+        while (pos > 0) {
+            --pos;
+            searchList = searchList.prepend(newSeqList[pos]);
+        }
+
+        // add new formula list to result object
+        semiCI.setFormulaList(searchList);
+
+        return semiCI;
+    }
+
+    /**
+     * . inserts new SequentFormula at index {@code idx} and removes duplicates, perform
+     * simplifications etc.
+     *
+     * @param sequentFormula the SequentFormula to be inserted at position idx
+     * @param idx an int that means insert sequentFormula at the idx-th position in the semisequent
+     * @return new Semisequent with sequentFormula at index idx and removed redundancies
+     */
+    private SemisequentChangeInfo removeRedundance(int idx, SequentFormula sequentFormula) {
+        return insertAndRemoveRedundancyHelper(idx, sequentFormula,
+                new SemisequentChangeInfo(seqList), null);
+    }
+
     /**
      * gets the element at a specific index
      *

keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/EqualsModProperty.java

@@ -0,0 +1,13 @@
+package org.key_project.rusty.logic.equality;
+
+public interface EqualsModProperty<T> {
+    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
+
+    /**
+     * Computes the hash code according to the given ignored {@code property}.
+     *
+     * @param property the ignored property according to which the hash code is computed
+     * @return the hash code of this object
+     */
+    int hashCodeModProperty(Property<T> property);
+}

keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/Property.java

@@ -0,0 +1,24 @@
+package org.key_project.rusty.logic.equality;
+
+public interface Property<T> {
+    /**
+     * Checks {@code t1} and {@code t2} for equality ignoring a certain property.
+     *
+     * @param t1 the first element of the equality check
+     * @param t2 the second element of the equality check
+     * @param v the additional arguments needed for the equality check
+     * @return whether {@code t1} and {@code t2} are equal ignoring a certain property
+     * @param <V> the type of the additional parameters needed for the comparison
+     */
+    <V> boolean equalsModThisProperty(T t1, T t2, V... v);
+
+    /**
+     * Computes the hash code of {@code t} in a context where
+     * {@link this#equalsModThisProperty(Object, Object, Object[])}
+     * is used as an equality check, so that it can be used in, e.g., a HashMap.
+     *
+     * @param t the object to compute the hash code for
+     * @return the hash code of {@code t} ignoring a certain property
+     */
+    int hashCodeModThisProperty(T t);
+}