Proof reordering (WIP)

.git-blame-ignore-revs

@@ -4,3 +4,5 @@
 b1ed8d6bc836ea40f357a839707d41fbb04ed6e2
 # commit with manual formatting corrections
 a9fcedc6c8d96f2480549254a307b3fbe31f04bd
+# formatting
+f91bf7fa6d3a63720cbcfee5147a78854faa8e8a

key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java

@@ -9,7 +9,8 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.logic.op.ElementaryUpdate;
-import de.uka.ilkd.key.logic.op.Operator;
+
+import org.key_project.logic.op.Operator;
 
 /**
  * Collects all operators occurring in the traversed term.

key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java

@@ -30,7 +30,7 @@
  * @author weigl
  * @deprecated Use the facade new KeyIO(services).parseTerm directly
  */
-@Deprecated // java11:(forRemoval = true, since = "2.8.0")
+@Deprecated(forRemoval = true, since = "2.8.0")
 public final class DefaultTermParser {
 
     /**

key.core/src/main/java/de/uka/ilkd/key/proof/BranchLocation.java

@@ -16,7 +16,7 @@
  *
  * @author Arne Keller
  */
-public class BranchLocation {
+public class BranchLocation implements Comparable<BranchLocation> {
     /**
      * Branch location of the initial proof branch.
      */
@@ -82,6 +82,9 @@ public static BranchLocation commonPrefix(BranchLocation... locations) {
      * @return the remaining suffix
      */
     public BranchLocation stripPrefix(BranchLocation prefix) {
+        if (prefix.size() == location.size()) {
+            return BranchLocation.ROOT;
+        }
         return new BranchLocation(location.stripPrefix(prefix.location));
     }
 
@@ -103,6 +106,9 @@ public BranchLocation append(Pair<Node, Integer> newBranch) {
     public BranchLocation removeLast() {
         List<Pair<Node, Integer>> list = location.toList();
         list.remove(list.size() - 1);
+        if (list.isEmpty()) {
+            return BranchLocation.ROOT;
+        }
         return new BranchLocation(ImmutableList.fromList(list));
     }
 
@@ -170,4 +176,17 @@ public boolean equals(Object o) {
     public int hashCode() {
         return Objects.hash(location);
     }
+
+    @Override
+    public int compareTo(BranchLocation other) {
+        if (this == other) {
+            return 0;
+        } else if (this == BranchLocation.ROOT) {
+            return -1;
+        } else if (other == BranchLocation.ROOT) {
+            return 1;
+        } else {
+            return location.compareTo(other.location);
+        }
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/FunctionTracker.java

@@ -0,0 +1,26 @@
+/* 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 de.uka.ilkd.key.proof;
+
+import java.lang.ref.WeakReference;
+import java.util.WeakHashMap;
+
+import org.key_project.logic.op.Function;
+
+public final class FunctionTracker {
+    private static final WeakHashMap<Function, WeakReference<Node>> MAPPING = new WeakHashMap<>();
+
+    private FunctionTracker() {
+
+    }
+
+    public static void setIntroducedBy(Function f, Node n) {
+        MAPPING.put(f, new WeakReference<>(n));
+    }
+
+    public static Node getIntroducedBy(Function f) {
+        var x = MAPPING.get(f);
+        return x != null ? x.get() : null;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java

@@ -30,6 +30,7 @@
 import de.uka.ilkd.key.util.properties.Properties;
 import de.uka.ilkd.key.util.properties.Properties.Property;
 
+import org.key_project.logic.op.Function;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -657,6 +658,9 @@ private void adaptNamespacesNewGoals(final ImmutableList<Goal> goalList) {
         boolean first = true;
         for (Goal goal : goalList) {
             goal.node().addLocalProgVars(newProgVars);
+            for (Function f : newFunctions) {
+                FunctionTracker.setIntroducedBy(f, goal.node.parent());
+            }
             goal.node().addLocalFunctions(newFunctions);
 
             if (first) {

key.core/src/main/java/de/uka/ilkd/key/proof/Node.java

@@ -33,7 +33,7 @@
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
-public class Node implements Iterable<Node> {
+public class Node implements Iterable<Node>, Comparable<Node> {
     private static final String RULE_WITHOUT_NAME = "rule without name";
 
     private static final String RULE_APPLICATION_WITHOUT_RULE = "rule application without rule";
@@ -113,6 +113,10 @@ public class Node implements Iterable<Node> {
     @Nullable
     private Lookup userData = null;
 
+    private List<Node> group = null;
+    private boolean hideInProofTree = false;
+    private String extraNodeLabel = null;
+
 
     /**
      * If the rule base has been extended e.g. by loading a new taclet as lemma or by applying a
@@ -837,4 +841,42 @@ public int getStepIndex() {
     void setStepIndex(int stepIndex) {
         this.stepIndex = stepIndex;
     }
+
+    public Node getFirstInBranch() {
+        Node candidate = this;
+        while (candidate.parent != null
+                && candidate.parent.getBranchLocation().equals(candidate.getBranchLocation())) {
+            candidate = candidate.parent;
+        }
+        return candidate;
+    }
+
+    public List<Node> getGroup() {
+        return group;
+    }
+
+    public void setGroup(List<Node> group) {
+        this.group = group;
+    }
+
+    public String getExtraNodeLabel() {
+        return extraNodeLabel;
+    }
+
+    public void setExtraNodeLabel(String extraNodeLabel) {
+        this.extraNodeLabel = extraNodeLabel;
+    }
+
+    public boolean isHideInProofTree() {
+        return hideInProofTree;
+    }
+
+    public void setHideInProofTree(boolean hideInProofTree) {
+        this.hideInProofTree = hideInProofTree;
+    }
+
+    @Override
+    public int compareTo(Node node) {
+        return Integer.compare(this.serialNr, node.serialNr);
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java

@@ -68,7 +68,7 @@ public abstract class AbstractProofReplayer {
     /**
      * The new proof.
      */
-    private final Proof proof;
+    protected final Proof proof;
 
     /**
      * Instantiate a new replayer.
@@ -93,6 +93,7 @@ protected ImmutableList<Goal> reApplyRuleApp(Node node, Goal openGoal)
             throws IntermediateProofReplayer.BuiltInConstructionException {
         RuleApp ruleApp = node.getAppliedRuleApp();
         ImmutableList<Goal> nextGoals;
+
         if (ruleApp.rule() instanceof BuiltInRule) {
             IBuiltInRuleApp builtInRuleApp = constructBuiltinApp(node, openGoal);
             if (!builtInRuleApp.complete()) {
@@ -318,6 +319,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
         }
 
         if (!ourApp.complete()) {
+            System.out.println("incomplete!");
             ourApp = ourApp.tryToInstantiate(proof.getServices());
         }
 

key.core/src/main/java/de/uka/ilkd/key/rule/PosRuleApp.java

@@ -0,0 +1,18 @@
+/* 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 de.uka.ilkd.key.rule;
+
+import de.uka.ilkd.key.logic.PosInOccurrence;
+
+/**
+ * Interface for rule applications with associated position information.
+ *
+ * @author Arne Keller
+ */
+public interface PosRuleApp {
+    /**
+     * @return the position the rule was applied on
+     */
+    PosInOccurrence posInOccurrence();
+}

key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java

@@ -27,7 +27,7 @@
  * ({@link de.uka.ilkd.key.rule.NoPosTacletApp}) is used to keep track of the (partial)
  * instantiation information.
  */
-public class PosTacletApp extends TacletApp {
+public class PosTacletApp extends TacletApp implements PosRuleApp {
 
     /**
      * stores the information where the Taclet is to be applied. This means where the find section

key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.label.TermLabel;
-import de.uka.ilkd.key.logic.op.Operator;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 import de.uka.ilkd.key.logic.op.SchemaVariable;
 import de.uka.ilkd.key.proof.Goal;
@@ -23,6 +22,7 @@
 
 import org.key_project.logic.Name;
 import org.key_project.logic.Named;
+import org.key_project.logic.op.Operator;
 import org.key_project.util.EqualsModProofIrrelevancy;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
@@ -728,8 +728,8 @@ public Set<SchemaVariable> collectSchemaVars() {
         }
 
         for (Operator op : oc.ops()) {
-            if (op instanceof SchemaVariable) {
-                result.add((SchemaVariable) op);
+            if (op instanceof SchemaVariable sv) {
+                result.add(sv);
             }
         }
 

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java

@@ -812,7 +812,7 @@ private TermAndBoundVarPair replaceBoundLogicVars(Term t, TermServices services)
         final OpCollector oc = new OpCollector();
         oc.visit(t);
         final Set<Name> usedNames = new LinkedHashSet<>();
-        for (Operator op : oc.ops()) {
+        for (var op : oc.ops()) {
             usedNames.add(op.name());
         }
 

key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java

@@ -76,6 +76,9 @@ public void addSettings(Settings settings) {
             settings.addPropertyChangeListener(settingsListener);
             if (lastReadedProperties != null) {
                 settings.readSettings(lastReadedProperties);
+            } else {
+                // special case: no settings file present
+                settings.readSettings(new Properties());
             }
             if (lastReadedConfiguration != null) {
                 settings.readSettings(lastReadedConfiguration);

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key

@@ -1806,7 +1806,7 @@
                 \then(aePseudoRight * aePseudoTargetFactor
                     = aePseudoTargetRight * aePseudoLeftCoeff)
                 \else(aePseudoTargetLeft = aePseudoTargetRight))
-        \heuristics(polySimp_leftNonUnit, polySimp_applyEqPseudo, notHumanReadable, notHumanReadable)
+        \heuristics(polySimp_leftNonUnit, polySimp_applyEqPseudo, notHumanReadable)
     };
 
     apply_eq_pseudo_leq {

key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt

@@ -1032,7 +1032,7 @@ apply_eq_pseudo_eq {
 \assumes ([equals(mul(aePseudoLeft,aePseudoLeftCoeff),aePseudoRight)]==>[]) 
 \find(equals(aePseudoTargetLeft,aePseudoTargetRight))
 \sameUpdateLevel\replacewith(if-then-else(and(equals(aePseudoTargetLeft,mul(aePseudoLeft,aePseudoTargetFactor)),not(equals(aePseudoLeftCoeff,Z(0(#))))),equals(mul(aePseudoRight,aePseudoTargetFactor),mul(aePseudoTargetRight,aePseudoLeftCoeff)),equals(aePseudoTargetLeft,aePseudoTargetRight))) 
-\heuristics(notHumanReadable, notHumanReadable, polySimp_applyEqPseudo, polySimp_leftNonUnit)
+\heuristics(notHumanReadable, polySimp_applyEqPseudo, polySimp_leftNonUnit)
 Choices: true}
 -----------------------------------------------------
 == apply_eq_pseudo_geq (apply_eq_pseudo_geq) =========================================

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java

@@ -65,7 +65,9 @@ public TreeNode[] getPath() {
         LinkedList<TreeNode> path = new LinkedList<>();
         TreeNode n = this;
         path.addFirst(n);
-        while ((n = n.getParent()) != null) {
+        // walk up the parent chain
+        // (robustness: do not continue indefinitely for self-parents)
+        while (n.getParent() != n && (n = n.getParent()) != null) {
             path.addFirst(n);
         }
         return path.toArray(new TreeNode[0]);