Merge branch 'main' into fix3186

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

@@ -18,7 +18,7 @@
  * The labeled term class is used for terms that have a label attached.
  *
  * Two labeled terms are equal if they have equal term structure and equal annotations. In contrast
- * the method {@link Term#equalsModRenaming(Object)} does not care about annotations and will just
+ * the method {@link Term#equalsModRenaming(Term)} does not care about annotations and will just
  * compare the term structure alone modula renaming.
  *
  * @see Term
@@ -31,6 +31,25 @@ class LabeledTermImpl extends TermImpl implements EqualsModProofIrrelevancy {
      */
     private final ImmutableArray<TermLabel> labels;
 
+    /**
+     * creates an instance of a labeled term.
+     *
+     * @param op the top level operator
+     * @param subs the Term that are the subterms of this term
+     * @param boundVars logic variables bound by the operator
+     * @param javaBlock contains the program part of the term (if any)
+     * @param labels the terms labels (must not be null or empty)
+     * @param origin a String with origin information
+     */
+    public LabeledTermImpl(Operator op, ImmutableArray<Term> subs,
+            ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock,
+            ImmutableArray<TermLabel> labels, String origin) {
+        super(op, subs, boundVars, javaBlock, origin);
+        assert labels != null : "Term labels must not be null";
+        assert !labels.isEmpty() : "There must be at least one term label";
+        this.labels = labels;
+    }
+
     /**
      * creates an instance of a labeled term.
      *
@@ -43,7 +62,7 @@ class LabeledTermImpl extends TermImpl implements EqualsModProofIrrelevancy {
     public LabeledTermImpl(Operator op, ImmutableArray<Term> subs,
             ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock,
             ImmutableArray<TermLabel> labels) {
-        super(op, subs, boundVars, javaBlock);
+        super(op, subs, boundVars, javaBlock, "");
         assert labels != null : "Term labels must not be null";
         assert !labels.isEmpty() : "There must be at least one term label";
         this.labels = labels;

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

@@ -64,7 +64,7 @@ public Term createTerm(@Nonnull Operator op, ImmutableArray<Term> subs,
             subs = NO_SUBTERMS;
         }
 
-        return doCreateTerm(op, subs, boundVars, javaBlock, labels);
+        return doCreateTerm(op, subs, boundVars, javaBlock, labels, "");
     }
 
     public Term createTerm(Operator op, ImmutableArray<Term> subs,
@@ -126,10 +126,12 @@ private ImmutableArray<Term> createSubtermArray(Term[] subs) {
 
     private Term doCreateTerm(Operator op, ImmutableArray<Term> subs,
             ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock,
-            ImmutableArray<TermLabel> labels) {
+            ImmutableArray<TermLabel> labels, String origin) {
         final Term newTerm =
-            (labels == null || labels.isEmpty() ? new TermImpl(op, subs, boundVars, javaBlock)
-                    : new LabeledTermImpl(op, subs, boundVars, javaBlock, labels)).checked();
+            (labels == null || labels.isEmpty()
+                    ? new TermImpl(op, subs, boundVars, javaBlock, origin)
+                    : new LabeledTermImpl(op, subs, boundVars, javaBlock, labels, origin))
+                            .checked();
         // Check if caching is possible. It is not possible if a non empty JavaBlock is available
         // in the term or in one of its children because the meta information like PositionInfos
         // may be different.
@@ -169,4 +171,8 @@ private Term doCreateTerm(Operator op, ImmutableArray<Term> subs,
         }
         throw new IllegalArgumentException("list of terms is empty.");
     }
+
+    public Term createTermWithOrigin(Term t, String origin) {
+        return doCreateTerm(t.op(), t.subs(), t.boundVars(), t.javaBlock(), t.getLabels(), origin);
+    }
 }

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

@@ -31,7 +31,7 @@
  * The currently only class implementing the Term interface. TermFactory should be the only class
  * dealing directly with the TermImpl class.
  */
-public class TermImpl implements Term, EqualsModProofIrrelevancy {
+class TermImpl implements Term, EqualsModProofIrrelevancy {
 
     /**
      * A static empty list of terms used for memory reasons.
@@ -102,16 +102,32 @@ private enum ThreeValuedTruth {
      * @param javaBlock the code block (if applicable) after which the term is evaluated
      */
     public TermImpl(Operator op, ImmutableArray<Term> subs,
-            ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock) {
+            ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock,
+            String origin) {
         assert op != null;
         assert subs != null;
         this.op = op;
         this.subs = subs.size() == 0 ? EMPTY_TERM_LIST : subs;
         this.boundVars = boundVars == null ? EMPTY_VAR_LIST : boundVars;
         this.javaBlock = javaBlock == null ? JavaBlock.EMPTY_JAVABLOCK : javaBlock;
+        this.origin = origin;
     }
 
+    TermImpl(Operator op, ImmutableArray<Term> subs,
+            ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock) {
+        this(op, subs, boundVars, javaBlock, "");
+    }
 
+    /**
+     * For which feature is this information needed?
+     * What is the fifference from {@link de.uka.ilkd.key.logic.label.OriginTermLabel}?
+     */
+    private final String origin;
+
+    @Override
+    public @Nullable String getOrigin() {
+        return origin;
+    }
 
     // -------------------------------------------------------------------------
     // internal methods
@@ -710,14 +726,5 @@ public boolean containsJavaBlockRecursive() {
         return containsJavaBlockRecursive == ThreeValuedTruth.TRUE;
     }
 
-    private String origin;
 
-    @Override
-    public @Nullable String getOrigin() {
-        return origin;
-    }
-
-    public void setOrigin(String origin) {
-        this.origin = origin;
-    }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabelFactory.java

@@ -102,12 +102,16 @@ private Origin parseOrigin(String str) throws TermLabelException {
 
                     String ruleName = tokenizer.nextToken();
 
-                    if (!ruleName.startsWith("(") || !ruleName.endsWith(")")) {
+                    if (ruleName.startsWith("(")) {
+                        ruleName = ruleName.substring(1);
+                        while (!ruleName.endsWith(")")) {
+                            ruleName += tokenizer.nextToken();
+                        }
+                        ruleName = ruleName.substring(0, ruleName.length() - 1);
+                    } else {
                         throw new IllegalArgumentException();
                     }
 
-                    ruleName = ruleName.substring(1, ruleName.length() - 1);
-
                     matchEnd(tokenizer, str);
 
                     return new NodeOrigin(specType, ruleName, number);

key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java

@@ -17,41 +17,41 @@
  * Abstract base class for implementations of the Sort interface.
  */
 public abstract class AbstractSort implements Sort {
-
     private final Name name;
-    private ImmutableSet<Sort> ext;
+    private final ImmutableSet<Sort> ext;
     private final boolean isAbstract;
 
     /**
-     * Documentation for this sort given by the an associated documentation comment.
+     * Documentation for this sort given by the associated documentation comment.
      *
      * @see de.uka.ilkd.key.nparser.KeYParser.One_sort_declContext#doc
      */
-    private String documentation;
+    private final String documentation;
 
     /** Information of the origin of this sort */
-    private String origin;
+    private final String origin;
 
-    public AbstractSort(Name name, ImmutableSet<Sort> ext, boolean isAbstract) {
+    public AbstractSort(Name name,
+            ImmutableSet<Sort> extendedSorts,
+            boolean isAbstract,
+            String documentation,
+            String origin) {
         this.name = name;
-        this.ext = ext;
         this.isAbstract = isAbstract;
+        if (extendedSorts != null && extendedSorts.isEmpty()) {
+            this.ext = DefaultImmutableSet.<Sort>nil().add(ANY);
+        } else {
+            this.ext = extendedSorts == null ? DefaultImmutableSet.<Sort>nil() : extendedSorts;
+        }
+        this.documentation = documentation;
+        this.origin = origin;
     }
 
-
     @Override
     public final ImmutableSet<Sort> extendsSorts() {
-        if (this == Sort.FORMULA || this == Sort.UPDATE || this == Sort.ANY) {
-            return DefaultImmutableSet.nil();
-        } else {
-            if (ext.isEmpty()) {
-                ext = DefaultImmutableSet.<Sort>nil().add(ANY);
-            }
-            return ext;
-        }
+        return ext;
     }
 
-
     @Override
     public final ImmutableSet<Sort> extendsSorts(Services services) {
         return extendsSorts();
@@ -125,10 +125,6 @@ public String declarationString() {
         return name.toString();
     }
 
-    public void setDocumentation(@Nullable String documentation) {
-        this.documentation = documentation;
-    }
-
     @Nullable
     @Override
     public String getDocumentation() {
@@ -140,8 +136,4 @@ public String getDocumentation() {
     public String getOrigin() {
         return origin;
     }
-
-    public void setOrigin(@Nullable String origin) {
-        this.origin = origin;
-    }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java

@@ -40,7 +40,7 @@ public final class ArraySort extends AbstractSort {
 
     private ArraySort(ImmutableSet<Sort> extendsSorts, SortKey sk) {
         super(new Name((sk.elemType != null ? sk.elemType.getName() : sk.elemSort.name()) + "[]"),
-            extendsSorts, false);
+            extendsSorts, false, "", "");
 
         if (extendsSorts.isEmpty()) {
             throw new IllegalArgumentException("An ArraySort extends typically three sorts"

key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java

@@ -44,16 +44,22 @@ public final class GenericSort extends AbstractSort {
      * @param ext supersorts of this sort, which have to be either concrete sorts or plain generic
      *        sorts (i.e. not collection sorts of generic sorts)
      */
-    public GenericSort(Name name, ImmutableSet<Sort> ext, ImmutableSet<Sort> oneOf)
+    public GenericSort(Name name, ImmutableSet<Sort> ext, ImmutableSet<Sort> oneOf,
+            String documentation, String origin)
             throws GenericSupersortException {
-        super(name, ext, false);
+        super(name, ext, false, documentation, origin);
         this.oneOf = oneOf;
         checkSupersorts();
     }
 
+    public GenericSort(Name name, ImmutableSet<Sort> ext, ImmutableSet<Sort> oneOf)
+            throws GenericSupersortException {
+        this(name, ext, oneOf, "", "");
+    }
+
 
     public GenericSort(Name name) {
-        super(name, DefaultImmutableSet.nil(), false);
+        super(name, DefaultImmutableSet.nil(), false, "", "");
         this.oneOf = DefaultImmutableSet.nil();
     }
 

key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java

@@ -280,7 +280,7 @@ public boolean canStandFor(ProgramElement pe, Services services) {
     // --------------------------------------------------------------------------
 
     public ProgramSVSort(Name name) {
-        super(name, DefaultImmutableSet.nil(), false);
+        super(name, DefaultImmutableSet.nil(), false, "", "");
         NAME2SORT.put(name, this);
     }
 

key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java

@@ -10,11 +10,11 @@
 
 public class ProxySort extends AbstractSort {
 
-    public ProxySort(Name name, ImmutableSet<Sort> ext) {
-        super(name, ext, false);
+    public ProxySort(Name name, ImmutableSet<Sort> ext, String documentation, String origin) {
+        super(name, ext, false, documentation, origin);
     }
 
     public ProxySort(Name name) {
-        this(name, DefaultImmutableSet.nil());
+        this(name, DefaultImmutableSet.nil(), "", "");
     }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java

@@ -20,22 +20,22 @@ public interface Sort extends Named, HasOrigin {
     /**
      * Formulas are represented as "terms" of this sort.
      */
-    Sort FORMULA = new SortImpl(new Name("Formula"));
+    Sort FORMULA = new SortImpl(new Name("Formula"), null, "", "");
 
     /**
      * Updates are represented as "terms" of this sort.
      */
-    Sort UPDATE = new SortImpl(new Name("Update"));
+    Sort UPDATE = new SortImpl(new Name("Update"), null, "", "");
 
     /**
      * Term labels are represented as "terms" of this sort.
      */
-    Sort TERMLABEL = new SortImpl(new Name("TermLabel"));
+    Sort TERMLABEL = new SortImpl(new Name("TermLabel"), null, "", "");
 
     /**
      * Any is a supersort of all sorts.
      */
-    Sort ANY = new SortImpl(new Name("any"));
+    Sort ANY = new SortImpl(new Name("any"), null, "", "");
 
     /**
      * Name of {@link #getCastSymbol(TermServices)}.

key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java

@@ -13,21 +13,30 @@
  */
 public final class SortImpl extends AbstractSort {
 
+    public SortImpl(Name name, ImmutableSet<Sort> ext, boolean isAbstract, String documentation,
+            String origin) {
+        super(name, ext, isAbstract, documentation, origin);
+    }
+
+    public SortImpl(Name name, ImmutableSet<Sort> ext, String documentation, String origin) {
+        this(name, ext, false, documentation, origin);
+    }
+
     public SortImpl(Name name, ImmutableSet<Sort> ext, boolean isAbstract) {
-        super(name, ext, isAbstract);
+        super(name, ext, isAbstract, "", "");
     }
 
     public SortImpl(Name name, ImmutableSet<Sort> ext) {
-        this(name, ext, false);
+        this(name, ext, false, "", "");
     }
 
     public SortImpl(Name name, Sort ext) {
-        this(name, DefaultImmutableSet.<Sort>nil().add(ext), false);
+        this(name, DefaultImmutableSet.<Sort>nil().add(ext), false, "", "");
     }
 
 
     public SortImpl(Name name) {
-        this(name, DefaultImmutableSet.nil());
+        this(name, DefaultImmutableSet.nil(), "", "");
     }
 
     public boolean equals(Object o) {

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java

@@ -131,9 +131,8 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
                 Sort s = null;
                 if (isGenericSort) {
                     try {
-                        var gs = new GenericSort(sortName, ext, oneOf);
-                        gs.setDocumentation(documentation);
-                        gs.setOrigin(BuilderHelpers.getPosition(idCtx));
+                        var gs = new GenericSort(sortName, ext, oneOf, documentation,
+                            BuilderHelpers.getPosition(idCtx));
                         s = gs;
                     } catch (GenericSupersortException e) {
                         semanticError(ctx, "Illegal sort given");
@@ -142,14 +141,12 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
                     s = Sort.ANY;
                 } else {
                     if (isProxySort) {
-                        var ps = new ProxySort(sortName, ext);
-                        ps.setDocumentation(documentation);
-                        ps.setOrigin(BuilderHelpers.getPosition(idCtx));
+                        var ps = new ProxySort(sortName, ext, documentation,
+                            BuilderHelpers.getPosition(idCtx));
                         s = ps;
                     } else {
-                        var si = new SortImpl(sortName, ext, isAbstractSort);
-                        si.setDocumentation(documentation);
-                        si.setOrigin(BuilderHelpers.getPosition(idCtx));
+                        var si = new SortImpl(sortName, ext, isAbstractSort,
+                            documentation, BuilderHelpers.getPosition(idCtx));
                         s = si;
                     }
                 }