Merge pull request #10 from tobias-rnh/taclet-pbuilder

Taclet pbuilder

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

@@ -10,12 +10,14 @@
 import org.key_project.rusty.logic.op.ProgramVariable;
 
 import org.jspecify.annotations.NonNull;
+import org.key_project.rusty.rule.RuleSet;
 
 public class NamespaceSet {
     private Namespace<@NonNull QuantifiableVariable> varNS = new Namespace<>();
     private Namespace<@NonNull ProgramVariable> progVarNS = new Namespace<>();
     // TODO: Operators should not be local to goals
     private Namespace<@NonNull Function> funcNS = new Namespace<>();
+    private Namespace<@NonNull RuleSet> ruleSetNS = new Namespace<RuleSet>();
     private Namespace<@NonNull Sort> sortNS = new Namespace<>();
 
     public NamespaceSet() {}
@@ -53,6 +55,14 @@ public void setFunctions(Namespace<@NonNull Function> funcNS) {
         this.funcNS = funcNS;
     }
 
+    public Namespace<@NonNull RuleSet> ruleSets() {
+        return ruleSetNS;
+    }
+
+    public void setRuleSets(Namespace<@NonNull RuleSet> ruleSetNS) {
+        this.ruleSetNS = ruleSetNS;
+    }
+
     public Namespace<@NonNull Sort> sorts() {
         return sortNS;
     }
@@ -65,6 +75,7 @@ public void add(NamespaceSet ns) {
         variables().add(ns.variables());
         programVariables().add(ns.programVariables());
         sorts().add(ns.sorts());
+        ruleSets().add(ns.ruleSets());
         functions().add(ns.functions());
     }
 

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

@@ -29,6 +29,31 @@ public Semisequent(SequentFormula seqFormula) {
         this.seqList = ImmutableSLList.<SequentFormula>nil().append(seqFormula);
     }
 
+    /**
+     * inserts an element at a specified index performing redundancy checks, this may result in
+     * 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
+     * @return a semi sequent change information object with the new semisequent and information
+     *         which formulas have been added or removed
+     */
+    public SemisequentChangeInfo insert(int idx, SequentFormula sequentFormula) {
+        return removeRedundance(idx, sequentFormula);
+    }
+
+    /**
+     * inserts element at index 0 performing redundancy checks, this may result in returning same
+     * semisequent if inserting would create redundancies
+     *
+     * @param sequentFormula SequentFormula to be inserted
+     * @return a semi sequent change information object with the new semisequent and information
+     *         which formulas have been added or removed
+     */
+    public SemisequentChangeInfo insertFirst(SequentFormula sequentFormula) {
+        return insert(0, sequentFormula);
+    }
+
     /**
      * is this a semisequent that contains no formulas
      *
@@ -86,6 +111,12 @@ public boolean equals(Object o) {
         return seqList.equals(((Semisequent) o).seqList);
     }
 
+    /** @return String representation of this Semisequent */
+    @Override
+    public String toString() {
+        return seqList.toString();
+    }
+
     // inner class used to represent an empty semisequent
     private static class Empty extends Semisequent {
 

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

@@ -0,0 +1,236 @@
+package org.key_project.rusty.logic;
+
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+
+public class SemisequentChangeInfo {
+
+    /** contains the added formulas to the semisequent */
+    private ImmutableList<SequentFormula> added = ImmutableSLList.nil();
+    /** contains the removed formulas from the semisequent */
+    private ImmutableList<SequentFormula> removed = ImmutableSLList.nil();
+    /** contains the modified formulas from the semisequent */
+    private ImmutableList<FormulaChangeInfo> modified = ImmutableSLList.nil();
+    /** stores the redundance free formula list of the semisequent */
+    private ImmutableList<SequentFormula> modifiedSemisequent = ImmutableSLList.nil();
+    /**
+     * contains formulas that have been tried to add, but which have been rejected due to already
+     * existing formulas in the sequent subsuming these formulas
+     */
+    private ImmutableList<SequentFormula> rejected = ImmutableSLList.nil();
+
+    /** */
+    private int lastFormulaIndex = -1;
+
+    public SemisequentChangeInfo() {
+    }
+
+    public SemisequentChangeInfo(ImmutableList<SequentFormula> formulas) {
+        this.modifiedSemisequent = formulas;
+    }
+
+    private SemisequentChangeInfo(SemisequentChangeInfo o) {
+        this.added = o.added;
+        this.removed = o.removed;
+        this.modified = o.modified;
+        this.modifiedSemisequent = o.modifiedSemisequent;
+        this.rejected = o.rejected;
+        this.lastFormulaIndex = o.lastFormulaIndex;
+    }
+
+    public SemisequentChangeInfo copy() {
+        return new SemisequentChangeInfo(this);
+    }
+
+    /**
+     * returns true if the semisequent has changed
+     */
+    public boolean hasChanged() {
+        return !added.isEmpty() || !removed.isEmpty() || !modified.isEmpty();
+    }
+
+    /**
+     * sets the list of constrained formula containing all formulas of the semisequent after the
+     * operation
+     */
+    public void setFormulaList(ImmutableList<SequentFormula> list) {
+        modifiedSemisequent = list;
+    }
+
+    /**
+     * returns the list of constrained formula of the new semisequent
+     */
+    public ImmutableList<SequentFormula> getFormulaList() {
+        return modifiedSemisequent;
+    }
+
+    /**
+     * logs an added formula at position idx
+     */
+    public void addedFormula(int idx, SequentFormula cf) {
+        added = added.prepend(cf);
+        lastFormulaIndex = idx;
+    }
+
+    /**
+     * logs a modified formula at position idx
+     */
+    public void modifiedFormula(int idx, FormulaChangeInfo fci) {
+        // This information can overwrite older records about removed
+        // formulas
+        removed = removed.removeAll(fci.positionOfModification().sequentFormula());
+        modified = modified.prepend(fci);
+        lastFormulaIndex = idx;
+    }
+
+    /**
+     * returns the list of all added constrained formulas
+     *
+     * @return IList<SequentFormula> added to the semisequent
+     */
+    public ImmutableList<SequentFormula> addedFormulas() {
+        return added;
+    }
+
+    /**
+     * returns the list of all removed constrained formulas
+     *
+     * @return IList<SequentFormula> removed from the semisequent
+     */
+    public ImmutableList<SequentFormula> removedFormulas() {
+        return removed;
+    }
+
+    /**
+     * returns a list of formulas that have been tried to add to the semisequent but got rejected as
+     * they were redundant
+     *
+     * @return list of formulas rejected due to redundancy
+     */
+    public ImmutableList<SequentFormula> rejectedFormulas() {
+        return this.rejected;
+    }
+
+
+    /**
+     * adding formula <tt>f</tt> to the semisequent failed due to a redundance check. This means an
+     * equal or stronger formula is already present in the semisequent
+     *
+     * @param f the SequentFormula
+     */
+    public void rejectedFormula(SequentFormula f) {
+        this.rejected = this.rejected.append(f);
+    }
+
+    /**
+     * returns the list of all modification positions
+     *
+     * @return IList<SequentFormula> modified within the semisequent
+     */
+    public ImmutableList<FormulaChangeInfo> modifiedFormulas() {
+        return modified;
+    }
+
+    /**
+     * logs an added formula at position idx
+     */
+    public void removedFormula(int idx, SequentFormula cf) {
+        removed = removed.prepend(cf);
+
+        lastFormulaIndex = (lastFormulaIndex == idx) ? -1
+                : lastFormulaIndex > idx ? lastFormulaIndex - 1 : lastFormulaIndex;
+
+        if (lastFormulaIndex < -1) {
+            lastFormulaIndex = -1;
+        }
+
+    }
+
+    /**
+     * This method combines this change information from this info and its successor. ATTENTION: it
+     * takes over ownership over <code>succ</code> and does not release it. This means when
+     * invoking the method it must be snsured that succ is never used afterwards.
+     *
+     * @param succ the SemisequentChangeInfo to combine with
+     */
+    public void combine(SemisequentChangeInfo succ) {
+        final SemisequentChangeInfo predecessor = this;
+        if (succ == predecessor) {
+            return;
+        }
+
+        for (SequentFormula sf : succ.removed) {
+            predecessor.added = predecessor.added.removeAll(sf);
+
+            boolean skip = false;
+            for (FormulaChangeInfo fci : predecessor.modified) {
+                if (fci.newFormula() == sf) {
+                    predecessor.modified = predecessor.modified.removeAll(fci);
+                    if (!predecessor.removed.contains(fci.getOriginalFormula())) {
+                        predecessor.removed = predecessor.removed.append(fci.getOriginalFormula());
+                    }
+                    skip = true;
+                    break;
+                }
+            }
+            if (!skip) {
+                predecessor.removedFormula(succ.lastFormulaIndex, sf);
+            }
+        }
+
+        for (FormulaChangeInfo fci : succ.modified) {
+            if (predecessor.addedFormulas().contains(fci.getOriginalFormula())) {
+                predecessor.added = predecessor.added.removeAll(fci.getOriginalFormula());
+                predecessor.addedFormula(succ.lastFormulaIndex, fci.newFormula());
+            } else {
+                predecessor.modifiedFormula(succ.lastFormulaIndex, fci);
+            }
+        }
+
+        for (SequentFormula sf : succ.added) {
+            predecessor.removed = predecessor.removed.removeAll(sf);
+            if (!predecessor.added.contains(sf)) {
+                predecessor.addedFormula(succ.lastFormulaIndex, sf);
+            }
+        }
+
+        for (SequentFormula sf : succ.rejected) {
+            if (!predecessor.rejected.contains(sf)) {
+                predecessor.rejectedFormula(sf);
+            }
+        }
+
+        predecessor.lastFormulaIndex = succ.lastFormulaIndex;
+        predecessor.modifiedSemisequent = succ.modifiedSemisequent;
+    }
+
+    /**
+     * returns the index of the last added formula
+     */
+    public int getIndex() {
+        return lastFormulaIndex;
+    }
+
+    /**
+     * returns the semisequent that is the result of the change operation
+     */
+    public Semisequent semisequent() {
+        final Semisequent semisequent;
+        if (modifiedSemisequent.isEmpty()) {
+            semisequent = Semisequent.EMPTY_SEMISEQUENT;
+        } else {
+            semisequent = new Semisequent(modifiedSemisequent);
+        }
+        return semisequent;
+    }
+
+
+    /**
+     * toString
+     */
+    public String toString() {
+        return "changed:" + hasChanged() + "\n  added (pos):" + added + "(" + lastFormulaIndex + ")"
+                + "\n  removed:" + removed + "\n  modified:" + modified + "\n  rejected:" + rejected
+                + "\n  new semisequent:" + modifiedSemisequent;
+    }
+}

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

@@ -94,6 +94,16 @@ public Semisequent succedent() {
         return succedent;
     }
 
+    /**
+     * String representation of the sequent
+     *
+     * @return String representation of the sequent
+     */
+    @Override
+    public String toString() {
+        return antecedent().toString() + "==>" + succedent().toString();
+    }
+
     @Override
     public @NonNull Iterator<SequentFormula> iterator() {
         return new SequentIterator(antecedent(), succedent());