diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java index 7067e1ac3ee..a6a8de38319 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java +++ b/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 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 subs, + ImmutableArray boundVars, JavaBlock javaBlock, + ImmutableArray 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 subs, ImmutableArray boundVars, JavaBlock javaBlock, ImmutableArray 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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java index 310481d250b..2d06d45cd38 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java @@ -64,7 +64,7 @@ public Term createTerm(@Nonnull Operator op, ImmutableArray subs, subs = NO_SUBTERMS; } - return doCreateTerm(op, subs, boundVars, javaBlock, labels); + return doCreateTerm(op, subs, boundVars, javaBlock, labels, ""); } public Term createTerm(Operator op, ImmutableArray subs, @@ -126,10 +126,12 @@ private ImmutableArray createSubtermArray(Term[] subs) { private Term doCreateTerm(Operator op, ImmutableArray subs, ImmutableArray boundVars, JavaBlock javaBlock, - ImmutableArray labels) { + ImmutableArray 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 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); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java index 74617076af6..4318d253541 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java +++ b/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 subs, - ImmutableArray boundVars, JavaBlock javaBlock) { + ImmutableArray 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 subs, + ImmutableArray 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; - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabelFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabelFactory.java index d1bde558691..3c3b0e2c707 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabelFactory.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java index 995b3c73bb7..03a386446fc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java +++ b/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 ext; + private final ImmutableSet 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 ext, boolean isAbstract) { + public AbstractSort(Name name, + ImmutableSet extendedSorts, + boolean isAbstract, + String documentation, + String origin) { this.name = name; - this.ext = ext; this.isAbstract = isAbstract; + if (extendedSorts != null && extendedSorts.isEmpty()) { + this.ext = DefaultImmutableSet.nil().add(ANY); + } else { + this.ext = extendedSorts == null ? DefaultImmutableSet.nil() : extendedSorts; + } + this.documentation = documentation; + this.origin = origin; } - @Override public final ImmutableSet extendsSorts() { - if (this == Sort.FORMULA || this == Sort.UPDATE || this == Sort.ANY) { - return DefaultImmutableSet.nil(); - } else { - if (ext.isEmpty()) { - ext = DefaultImmutableSet.nil().add(ANY); - } - return ext; - } + return ext; } - @Override public final ImmutableSet 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; - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java index 3fbda204dc8..745d4293128 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java +++ b/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 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" diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java index b9a0a558715..b5f517045cd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java +++ b/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 ext, ImmutableSet oneOf) + public GenericSort(Name name, ImmutableSet ext, ImmutableSet 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 ext, ImmutableSet 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(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index a61b890cf76..b5c6b70296f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/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); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java index 41cb3abba28..7e6e4faec19 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java +++ b/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 ext) { - super(name, ext, false); + public ProxySort(Name name, ImmutableSet ext, String documentation, String origin) { + super(name, ext, false, documentation, origin); } public ProxySort(Name name) { - this(name, DefaultImmutableSet.nil()); + this(name, DefaultImmutableSet.nil(), "", ""); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java index 3e12ff7024d..8caf4d46566 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java +++ b/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)}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java index 6b6f6faca83..d195b2eeee1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java +++ b/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 ext, boolean isAbstract, String documentation, + String origin) { + super(name, ext, isAbstract, documentation, origin); + } + + public SortImpl(Name name, ImmutableSet ext, String documentation, String origin) { + this(name, ext, false, documentation, origin); + } + public SortImpl(Name name, ImmutableSet ext, boolean isAbstract) { - super(name, ext, isAbstract); + super(name, ext, isAbstract, "", ""); } public SortImpl(Name name, ImmutableSet ext) { - this(name, ext, false); + this(name, ext, false, "", ""); } public SortImpl(Name name, Sort ext) { - this(name, DefaultImmutableSet.nil().add(ext), false); + this(name, DefaultImmutableSet.nil().add(ext), false, "", ""); } public SortImpl(Name name) { - this(name, DefaultImmutableSet.nil()); + this(name, DefaultImmutableSet.nil(), "", ""); } public boolean equals(Object o) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 12e71a16a45..3fcef655f26 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/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; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 1d45254f8b2..a3516ebcce1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -85,11 +85,11 @@ public ExpressionBuilder(Services services, NamespaceSet nss, setSchemaVariables(schemaNamespace); } - public static Term updateOrigin(Term t, ParserRuleContext ctx) { + public static Term updateOrigin(Term t, ParserRuleContext ctx, Services services) { try { - TermImpl ti = (TermImpl) t; - ti.setOrigin(ctx.start.getTokenSource().getSourceName() + "@" + ctx.start.getLine() - + ":" + ctx.start.getCharPositionInLine() + 1); + t = services.getTermFactory().createTermWithOrigin(t, + ctx.start.getTokenSource().getSourceName() + "@" + ctx.start.getLine() + + ":" + ctx.start.getCharPositionInLine() + 1); } catch (ClassCastException ignored) { } return t; @@ -175,7 +175,7 @@ public Term visitParallel_term(KeYParser.Parallel_termContext ctx) { for (int i = 1; i < t.size(); i++) { a = getTermFactory().createTerm(UpdateJunctor.PARALLEL_UPDATE, a, t.get(i)); } - return updateOrigin(a, ctx); + return updateOrigin(a, ctx, services); } @Override @@ -188,9 +188,9 @@ public Term visitElementary_update_term(KeYParser.Elementary_update_termContext Term a = accept(ctx.a); Term b = accept(ctx.b); if (b != null) { - return updateOrigin(getServices().getTermBuilder().elementary(a, b), ctx); + return updateOrigin(getServices().getTermBuilder().elementary(a, b), ctx, services); } - return updateOrigin(a, ctx); + return updateOrigin(a, ctx, services); } @Override @@ -211,10 +211,10 @@ public Term visitEquivalence_term(KeYParser.Equivalence_termContext ctx) { private Term binaryTerm(ParserRuleContext ctx, Operator operator, Term left, Term right) { if (right == null) { - return updateOrigin(left, ctx); + return updateOrigin(left, ctx, services); } return capsulateTf(ctx, - () -> updateOrigin(getTermFactory().createTerm(operator, left, right), ctx)); + () -> updateOrigin(getTermFactory().createTerm(operator, left, right), ctx, services)); } @Override @@ -306,7 +306,7 @@ public Object visitComparison_term(KeYParser.Comparison_termContext ctx) { Term termR = accept(ctx.b); if (termR == null) { - return updateOrigin(termL, ctx); + return updateOrigin(termL, ctx, services); } String op_name = ""; @@ -330,7 +330,7 @@ public Object visitComparison_term(KeYParser.Comparison_termContext ctx) { public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) { Term termL = Objects.requireNonNull(accept(ctx.a)); if (ctx.op.isEmpty()) { - return updateOrigin(termL, ctx); + return updateOrigin(termL, ctx, services); } List terms = mapOf(ctx.b); @@ -373,7 +373,7 @@ private Term binaryLDTSpecificTerm(ParserRuleContext ctx, String opname, Term la public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx) { Term termL = accept(ctx.a); if (ctx.b.isEmpty()) { - return updateOrigin(termL, ctx); + return updateOrigin(termL, ctx, services); } List terms = mapOf(ctx.b); Term last = termL; @@ -386,7 +386,7 @@ public Object visitStrong_arith_term_1(KeYParser.Strong_arith_term_1Context ctx) @Override public Object visitEmptyset(KeYParser.EmptysetContext ctx) { var op = services.getTypeConverter().getLocSetLDT().getEmpty(); - return updateOrigin(getTermFactory().createTerm(op), ctx); + return updateOrigin(getTermFactory().createTerm(op), ctx, services); } @Override @@ -923,7 +923,7 @@ public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContex t = getServices().getTermBuilder().addLabel(t, labels); } } - return updateOrigin(t, ctx); + return updateOrigin(t, ctx, services); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index 4c3c7fe42c9..0fa82ba5b3a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.logic.PosInProgram; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.TermImpl; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.ModalOperatorSV; import de.uka.ilkd.key.logic.op.Operator; @@ -537,9 +536,8 @@ public boolean equals(Object obj) { final ImmutableMapEntry> e = it.next(); final Object inst = e.value().getInstantiation(); assert inst != null : "Illegal null instantiation."; - if (inst instanceof TermImpl) { - if (!((TermImpl) inst) - .equalsModIrrelevantTermLabels(cmp.getInstantiation(e.key()))) { + if (inst instanceof Term instAsTerm) { + if (!instAsTerm.equalsModIrrelevantTermLabels(cmp.getInstantiation(e.key()))) { return false; } } else if (!inst.equals(cmp.getInstantiation(e.key()))) { @@ -568,9 +566,8 @@ public boolean equalsModProofIrrelevancy(Object obj) { final ImmutableMapEntry> e = it.next(); final Object inst = e.value().getInstantiation(); assert inst != null : "Illegal null instantiation."; - if (inst instanceof TermImpl) { - if (!((TermImpl) inst) - .equalsModProofIrrelevancy(cmp.getInstantiation(e.key()))) { + if (inst instanceof Term instAsTerm) { + if (!instAsTerm.equalsModProofIrrelevancy(cmp.getInstantiation(e.key()))) { return false; } } else if (!inst.equals(cmp.getInstantiation(e.key()))) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java index a194c451e22..1a05bd52697 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java @@ -70,7 +70,7 @@ protected Sort replaceSort(Sort sort, TermServices services) { } ImmutableSet extSorts = replaceSorts(sort.extendsSorts(), services); - ProxySort result = new ProxySort(sort.name(), extSorts); + ProxySort result = new ProxySort(sort.name(), extSorts, "", ""); sortMap.put(sort, result); return result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java index 5fe559c193a..3328a155654 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java @@ -122,7 +122,8 @@ public void replaceGenericByProxySorts() { Set result = new HashSet<>(); for (Sort sort : usedExtraSorts) { if (sort instanceof GenericSort genSort) { - ProxySort proxySort = new ProxySort(genSort.name(), genSort.extendsSorts()); + ProxySort proxySort = new ProxySort(genSort.name(), genSort.extendsSorts(), + "", ""); result.add(proxySort); } else { result.add(sort);