diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index edd68fca7e3..4da5b2e431e 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -383,6 +383,9 @@ GREATEREQUAL WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ; + +OPENTYPEPARAMS:'<' '['; +CLOSETYPEPARAMS:']' '>'; LESS: '<'; LESSEQUAL: '<' '=' | '\u2264'; LGUILLEMETS: '<' '<' | '«' | '‹'; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 6d255549006..6fe081dcb7e 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -94,10 +94,26 @@ one_sort_decl (ONEOF sortOneOf = oneof_sorts)? (EXTENDS sortExt = extends_sorts)? SEMI | PROXY sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI - | ABSTRACT? sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI + | ABSTRACT? (sortIds=simple_ident_dots_comma_list | + parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI ) ; +// TODO currently you are not allowed to commatise parametric_sort_decl. Is this severe? + +parametric_sort_decl +: + simple_ident_dots + OPENTYPEPARAMS + formal_sort_param_decl (COMMA formal_sort_param_decl)* + CLOSETYPEPARAMS +; + +formal_sort_param_decl +: + (PLUS | MINUS)? simple_ident +; + simple_ident_dots : simple_ident (DOT simple_ident)* @@ -108,7 +124,6 @@ simple_ident_dots_comma_list simple_ident_dots (COMMA simple_ident_dots)* ; - extends_sorts : sortId (COMMA sortId)* @@ -243,7 +258,7 @@ datatype_decl: doc=DOC_COMMENT? // weigl: all datatypes are free! // FREE? - name=simple_ident + name=simple_ident formal_sort_parameters? EQUALS datatype_constructor (OR datatype_constructor)* SEMI @@ -326,7 +341,14 @@ ruleset_decls sortId : - id=simple_ident_dots (EMPTYBRACKETS)* + id=simple_ident_dots (EMPTYBRACKETS)* formal_sort_parameters? +; + +formal_sort_parameters +: + OPENTYPEPARAMS + sortId (COMMA sortId)* + CLOSETYPEPARAMS ; id_declaration diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java b/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java index 8b6771b1b6c..257e116b269 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java @@ -7,6 +7,8 @@ import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.logic.op.QuantifiableVariable; +import de.uka.ilkd.key.logic.sort.ParametricSortDeclaration; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.rule.RuleSet; import org.key_project.logic.Name; @@ -21,6 +23,7 @@ public class NamespaceSet { private Namespace funcNS = new Namespace<>(); private Namespace ruleSetNS = new Namespace<>(); private Namespace sortNS = new Namespace<>(); + private Namespace parametricSortNS = new Namespace<>(); private Namespace choiceNS = new Namespace<>(); public NamespaceSet() { @@ -28,32 +31,35 @@ public NamespaceSet() { public NamespaceSet(Namespace varNS, Namespace funcNS, - Namespace sortNS, Namespace ruleSetNS, Namespace choiceNS, + Namespace sortNS, + Namespace parametricSortNS, + Namespace ruleSetNS, Namespace choiceNS, Namespace programVarNS) { this.varNS = varNS; this.progVarNS = programVarNS; this.funcNS = funcNS; this.sortNS = sortNS; + this.parametricSortNS = parametricSortNS; this.ruleSetNS = ruleSetNS; this.choiceNS = choiceNS; } public NamespaceSet copy() { return new NamespaceSet(variables().copy(), functions().copy(), - sorts().copy(), + sorts().copy(), parametricSorts().copy(), ruleSets().copy(), choices().copy(), programVariables().copy()); } public NamespaceSet shallowCopy() { - return new NamespaceSet(variables(), functions(), sorts(), ruleSets(), - choices(), - programVariables()); + return new NamespaceSet(variables(), functions(), sorts(), parametricSorts(), ruleSets(), + choices(), programVariables()); } // TODO MU: Rename into sth with wrap or similar public NamespaceSet copyWithParent() { return new NamespaceSet(new Namespace<>(variables()), new Namespace<>(functions()), new Namespace<>(sorts()), + new Namespace<>(parametricSorts()), new Namespace<>(ruleSets()), new Namespace<>(choices()), new Namespace<>(programVariables())); } @@ -98,6 +104,14 @@ public void setSorts(Namespace sortNS) { this.sortNS = sortNS; } + public Namespace parametricSorts() { + return parametricSortNS; + } + + public void setParametricSorts(Namespace parametricSortNS) { + this.parametricSortNS = parametricSortNS; + } + public Namespace choices() { return choiceNS; } @@ -110,6 +124,7 @@ public void add(NamespaceSet ns) { variables().add(ns.variables()); programVariables().add(ns.programVariables()); sorts().add(ns.sorts()); + parametricSorts().add(ns.parametricSorts()); ruleSets().add(ns.ruleSets()); functions().add(ns.functions()); choices().add(ns.choices()); @@ -119,7 +134,7 @@ public void add(NamespaceSet ns) { * returns all namespaces in an array */ private Namespace[] asArray() { - return new Namespace[] { variables(), programVariables(), sorts(), ruleSets(), functions(), + return new Namespace[] { variables(), programVariables(), sorts(), parametricSorts(), ruleSets(), functions(), choices() }; } @@ -190,23 +205,26 @@ public void seal() { funcNS.seal(); ruleSetNS.seal(); sortNS.seal(); + parametricSortNS.seal(); choiceNS.seal(); } public boolean isEmpty() { return varNS.isEmpty() && programVariables().isEmpty() && funcNS.isEmpty() - && ruleSetNS.isEmpty() && sortNS.isEmpty() && choiceNS.isEmpty(); + && ruleSetNS.isEmpty() && sortNS.isEmpty() && parametricSortNS.isEmpty() && choiceNS.isEmpty(); } // create a namespace public NamespaceSet simplify() { return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(), + parametricSortNS.simplify(), ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify()); } public NamespaceSet getCompression() { return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(), + parametricSortNS.compress(), ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress()); } @@ -218,6 +236,7 @@ public void flushToParent() { public NamespaceSet getParent() { return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(), + parametricSortNS.parent(), ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java index bd675d35d89..dc1f204e80c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.logic.sort.ProgramSVSort; import org.key_project.logic.Name; @@ -39,7 +40,7 @@ public final class SortDependingFunction extends JFunction { private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortDependingOn) { super(instantiateName(template.kind, sortDependingOn), - instantiateResultSort(template, sortDependingOn), + instantiateSort(template.sortDependingOn, sortDependingOn, template.sort), instantiateArgSorts(template, sortDependingOn), null, template.unique, false); this.template = template; this.sortDependingOn = Qualifier.create(sortDependingOn); @@ -55,9 +56,10 @@ private static Name instantiateName(Name kind, Sort sortDependingOn) { } - private static Sort instantiateResultSort(SortDependingFunctionTemplate template, - Sort sortDependingOn) { - return template.sort == template.sortDependingOn ? sortDependingOn : template.sort; + private static Sort instantiateSort(GenericSort genericSort, Sort instanatiation, + Sort toInstantiate) { + // Replaces the generic sort and all occurrences in parametric sorts + return ParametricSortInstance.instantiate(genericSort, instanatiation, toInstantiate); } @@ -65,13 +67,11 @@ private static ImmutableArray instantiateArgSorts(SortDependingFunctionTem Sort sortDependingOn) { Sort[] result = new Sort[template.argSorts.size()]; for (int i = 0; i < result.length; i++) { - result[i] = (template.argSorts.get(i) == template.sortDependingOn ? sortDependingOn - : template.argSorts.get(i)); + result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, template.argSorts.get(i)); } return new ImmutableArray<>(result); } - // ------------------------------------------------------------------------- // public interface // ------------------------------------------------------------------------- diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDeclaration.java new file mode 100644 index 00000000000..01c489ac6d4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDeclaration.java @@ -0,0 +1,160 @@ +/* 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.logic.sort; + +import java.util.IdentityHashMap; +import java.util.Map; +import java.util.function.Function; + +import de.uka.ilkd.key.ldt.JavaDLTheory; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; +import org.key_project.logic.Name; +import org.key_project.logic.Named; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.collection.Immutables; + +/** + * Here is a short class diagram, written for PlantUML. + * You can create the PNG file by feeding this SourceFile into PlantUML or + * by entering the text into https://www.planttext.com/, e.g. + @formatter:off + @startuml + interface Sort + abstract class AbstractSort + class SortImpl + + class ParametricSortDeclaration + class ParametricSortInstance + class NullSort + class GenericSort + + Sort <|-- AbstractSort + AbstractSort <|-- SortImpl + AbstractSort <|-- ParametricSortInstance + AbstractSort <|-- GenericSort + Sort <|-- NullSort + + ParametricSortInstance --> ParametricSortDeclaration : base + ParametricSortInstance --> "*" Sort :args + ParametricSortDeclaration --> "n" GenericSort : typeParameters + ParametricSortDeclaration --> "*" Sort : extendsDecl + ParametricSortDeclaration --> "n" Variance : variances + + enum Variance { + COVARIANT + CONTRAVARIANT + INVARIANT + } + @enduml + @formatter:on + */ + +@NullMarked +public class ParametricSortDeclaration implements Named { + + private final Name name; + private final boolean isAbstract; + private final String documentation; + private final String origin; + + public enum Variance { + COVARIANT, + CONTRAVARIANT, + INVARIANT; + } + + public record SortParameter(@NonNull GenericSort genericSort, @NonNull Variance variance) { + } + + private final ImmutableList parameters; + + private final ImmutableSet extendedSorts; + + public ParametricSortDeclaration(Name name, ImmutableSet ext, boolean isAbstract, + ImmutableList parameters, ImmutableList covariances, + String documentation, String origin) { + this(name, ext, isAbstract, Immutables.zip(parameters, covariances, SortParameter::new), documentation, origin); + } + + public ParametricSortDeclaration(Name name, ImmutableSet ext, boolean isAbstract, + ImmutableList sortParams, String documentation, String origin) { + this.name = name; + this.extendedSorts = ext.isEmpty() ? Immutables.setOf(JavaDLTheory.ANY) : ext; + this.isAbstract = isAbstract; + this.documentation = documentation; + this.origin = origin; + this.parameters = sortParams; + assert Immutables.isDuplicateFree(parameters.map(SortParameter::genericSort)) : + "The caller should have made sure that generic sorts are not duplicated"; + } + + public Function getInstantiator(ImmutableList args) { + IdentityHashMap map = new IdentityHashMap<>(); + + if (args.size() != parameters.size()) { + throw new IllegalArgumentException("Parametric type " + name + + " expected " + parameters.size() + " arguments, but received " + + args); + } + + ImmutableList p = parameters; + while (!args.isEmpty()) { + map.put(p.head().genericSort(), args.head()); + p = p.tail(); + args = args.tail(); + } + + return new SortInstantiator(map); + } + + public static class SortInstantiator implements Function { + private final Map map; + + public SortInstantiator(Map map) { + this.map = map; + } + + @Override + public Sort apply(Sort sort) { + Sort mapped = map.get(sort); + if (mapped != null) { + return mapped; + } + if (sort instanceof ParametricSortInstance psi) { + return psi.map(this); + } else { + return sort; + } + } + } + + public ImmutableList getParameters() { + return parameters; + } + + public ImmutableSet getExtendedSorts() { + return extendedSorts; + } + + @Override + public Name name() { + return name; + } + + public boolean isAbstract() { + return isAbstract; + } + + public String getDocumentation() { + return documentation; + } + + public String getOrigin() { + return origin; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java new file mode 100644 index 00000000000..68d86c3e605 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java @@ -0,0 +1,152 @@ +/* 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.logic.sort; + +import java.util.Map; +import java.util.Objects; +import java.util.WeakHashMap; +import java.util.function.Function; + +import org.jspecify.annotations.NullMarked; +import org.key_project.logic.Name; +import org.key_project.logic.sort.AbstractSort; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.DefaultImmutableSet; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSet; + +import org.jspecify.annotations.Nullable; + +@NullMarked +public class ParametricSortInstance extends AbstractSort { + private static final Map CACHE = + new WeakHashMap<>(); + + private final ImmutableList parameters; + + private final ParametricSortDeclaration base; + + private final ImmutableSet extendsSorts; + + public static ParametricSortInstance get(ParametricSortDeclaration base, + ImmutableList parameters) { + ParametricSortInstance sort = + new ParametricSortInstance(base, parameters); + ParametricSortInstance cached = CACHE.get(sort); + if (cached != null) { + return cached; + } else { + CACHE.put(sort, sort); + return sort; + } + } + + // This must only be called in #get, which ensures that the cache is used. + private ParametricSortInstance(ParametricSortDeclaration base, ImmutableList parameters) { + super(makeName(base, parameters), base.isAbstract(), base.getDocumentation(), base.getOrigin()); + + this.extendsSorts = computeExt(base, parameters); + this.base = base; + this.parameters = parameters; + } + + private static ImmutableSet computeExt(ParametricSortDeclaration base, + ImmutableList parameters) { + ImmutableSet result = DefaultImmutableSet.nil(); + + // 1. extensions by base sort + ImmutableSet baseExt = base.getExtendedSorts(); + if (!baseExt.isEmpty()) { + Function inster = base.getInstantiator(parameters); + for (Sort s : baseExt) { + result = result.add(inster.apply(s)); + } + } + + // 2. extensions by variances + ImmutableList cov = base.getParameters(); + int number = 0; + for (ParametricSortDeclaration.SortParameter parameter : base.getParameters()) { + switch(parameter.variance()) { + case COVARIANT -> { + // take all bases of that arg and add the modified sort as ext class + /* for (Sort s : parameter.genericSort().extendsSorts()) { + ImmutableList newArgs = parameters.replace(number, s); + result = result.add(ParametricSortInstance.get(base, newArgs)); + } */ +// throw new UnsupportedOperationException( +// "Covariance currently not supported"); + } + + case CONTRAVARIANT -> throw new UnsupportedOperationException( + "Contravariance currently not supported"); + + case INVARIANT -> { + /* Nothing to be done */} + } + } + return result; + } + + private static Name makeName(ParametricSortDeclaration base, ImmutableList parameters) { + // The [ ] are produced by the list's toString method. + return new Name(base.name() + "<" + parameters + ">"); + } + + public ParametricSortDeclaration getBase() { + return base; + } + + public ImmutableList getParameters() { + return parameters; + } + + public ParametricSortInstance map(Function f) { + ImmutableList newParameters = parameters.map(f); + // The cache ensures that no unnecessary duplicates are kept. + return get(base, newParameters); + } + + @Override + public boolean equals(Object o) { + if (this == o) + return true; + if (o == null || getClass() != o.getClass()) + return false; + ParametricSortInstance that = (ParametricSortInstance) o; + return Objects.equals(parameters, that.parameters) && + base == that.base; + } + + @Override + public int hashCode() { + return Objects.hash(parameters, base); + } + + @Override + public ImmutableSet extendsSorts() { + return extendsSorts; + } + + @Override + public boolean extendsTrans(Sort sort) { + return sort == this || extendsSorts() + .exists((Sort superSort) -> superSort == sort || superSort.extendsTrans(sort)); + } + + public static Sort instantiate(GenericSort genericSort, Sort instantiation, Sort toInstantiate) { + if(genericSort == toInstantiate) { + return instantiation; + } else if(toInstantiate instanceof ParametricSortInstance psort) { + return psort.instantiate(genericSort, instantiation); + } else { + return toInstantiate; + } + } + + public Sort instantiate(GenericSort template, Sort instantiation) { + ImmutableList newParameters = parameters.map(s -> instantiate(template, instantiation, s)); + return get(base, newParameters); + } +} 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 4f344bb86a2..6da1c20ede7 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 @@ -23,12 +23,7 @@ import de.uka.ilkd.key.java.expression.ArrayInitializer; import de.uka.ilkd.key.java.expression.Literal; import de.uka.ilkd.key.java.expression.literal.StringLiteral; -import de.uka.ilkd.key.java.expression.operator.DLEmbeddedExpression; -import de.uka.ilkd.key.java.expression.operator.Instanceof; -import de.uka.ilkd.key.java.expression.operator.Intersect; -import de.uka.ilkd.key.java.expression.operator.Negative; -import de.uka.ilkd.key.java.expression.operator.New; -import de.uka.ilkd.key.java.expression.operator.NewArray; +import de.uka.ilkd.key.java.expression.operator.*; import de.uka.ilkd.key.java.expression.operator.adt.*; import de.uka.ilkd.key.java.reference.*; import de.uka.ilkd.key.java.statement.Catch; @@ -717,7 +712,6 @@ public boolean canStandFor(Term t) { } - // ----------- Types of Statement Program SVs ----------------------------- /** @@ -966,7 +960,7 @@ protected boolean canStandFor(ProgramElement check, Services services) { /** * This sort represents a type of program schema variables that match on names of method * references, i.e. the "m" of o.m(p1,pn). - * + *

* It can also be made to match only specific method names defined by the parameter "name". */ private static class MethodNameSort extends ProgramSVSort { 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 c34df7c9ded..b1952fb84ca 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 @@ -6,33 +6,22 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import org.key_project.logic.Name; +import org.key_project.logic.sort.AbstractSort; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; -import org.jspecify.annotations.Nullable; - /** * Abstract base class for implementations of the Sort interface. */ -public class SortImpl extends org.key_project.logic.sort.AbstractSort { - /** - * Documentation for this sort given by the associated documentation comment. - * - * @see de.uka.ilkd.key.nparser.KeYParser.One_sort_declContext#doc - */ - private final String documentation; - - /** Information of the origin of this sort */ - private final String origin; +public class SortImpl extends AbstractSort { + private ImmutableSet ext; public SortImpl(Name name, ImmutableSet ext, boolean isAbstract, String documentation, String origin) { - super(name, isAbstract); + super(name, isAbstract, documentation, origin); this.ext = ext; - this.documentation = documentation; - this.origin = origin; } public SortImpl(Name name, ImmutableSet ext, String documentation, String origin) { @@ -87,16 +76,6 @@ public String declarationString() { return name().toString(); } - @Override - public @Nullable String getDocumentation() { - return documentation; - } - - @Override - public @Nullable String getOrigin() { - return origin; - } - @Override public boolean equals(Object o) { if (o instanceof SortImpl) { 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 825279099a1..f6a06fb15ca 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 @@ -3,10 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.nparser.builder; -import java.util.HashMap; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; +import java.util.*; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; @@ -15,6 +12,7 @@ import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.logic.sort.*; +import de.uka.ilkd.key.logic.sort.ParametricSortDeclaration.SortParameter; import de.uka.ilkd.key.nparser.KeYParser; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.rule.RuleSet; @@ -22,10 +20,10 @@ import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; -import org.key_project.util.collection.ImmutableSet; -import org.key_project.util.collection.Immutables; +import org.key_project.util.collection.*; import org.antlr.v4.runtime.Token; +import org.key_project.util.java.CollectionUtil; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -63,14 +61,31 @@ public Object visitDecls(KeYParser.DeclsContext ctx) { @Override public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { - // boolean freeAdt = ctx.FREE() != null; var name = ctx.name.getText(); + List typeParameters = accept(ctx.formal_sort_parameters()); var doc = ctx.DOC_COMMENT() != null ? ctx.DOC_COMMENT().getText() : null; var origin = BuilderHelpers.getPosition(ctx); - var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); - sorts().addSafely(s); + if (typeParameters == null) { + var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); + sorts().addSafely(s); + } else { + var tp = typeParameters.stream().map(SortParameter::genericSort) + .collect(ImmutableList.collector()); + var doubled = CollectionUtil.findDuplicates(tp); + if (!doubled.isEmpty()) { + semanticError(ctx.formal_sort_parameters(), + "Type parameters must be unique within a declaration. Found duplicate: %s", doubled.getFirst()); + } + var variance = + typeParameters.stream().map(SortParameter::variance) + .collect(ImmutableList.collector()); + var s = new ParametricSortDeclaration( + new Name(name), ImmutableSet.empty(), false, tp, variance, + doc, origin); + namespaces().parametricSorts().add(s); + } return null; } @@ -133,64 +148,124 @@ public Object visitSort_decls(KeYParser.Sort_declsContext ctx) { return null; } + + public record NamedFormalSortParameter(String name, List parameters) {} + +// @Override +// public List visitSortList(KeYParser.SortListContext ctx) { +// List seq = new ArrayList<>(); +// for (KeYParser.SortIdContext context : ctx.sortId()) { +// String sortName = context.simple_ident_dots().getText(); +// // String brackets = StringUtil.repeat("[]", context.EMPTYBRACKETS().size()); +// List typeParams = accept(context.formal_sort_parameters()); +// seq.add(new NamedFormalSortParameter(sortName, +// typeParams != null ? typeParams : Collections.emptyList())); +// } +// return seq; +// } + + @Override public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { + // List>>> sortIds = + // accept(ctx.sortIds); List sortOneOf = accept(ctx.sortOneOf); List sortExt = accept(ctx.sortExt); boolean isGenericSort = ctx.GENERIC() != null; boolean isProxySort = ctx.PROXY() != null; boolean isAbstractSort = ctx.ABSTRACT() != null; List createdSorts = new LinkedList<>(); + // assert sortIds != null; + + ImmutableSet ext = sortExt == null ? ImmutableSet.empty() + : Immutables.setOf(sortExt); + ImmutableSet oneOf = sortOneOf == null ? ImmutableSet.empty() + : Immutables.setOf(sortOneOf); + var documentation = ParsingFacade.getValueDocumentation(ctx.DOC_COMMENT()); - for (var idCtx : ctx.sortIds.simple_ident_dots()) { - String sortId = accept(idCtx); - Name sortName = new Name(sortId); - - ImmutableSet ext = sortExt == null ? ImmutableSet.empty() - : Immutables.createSetFrom(sortExt); - ImmutableSet oneOf = sortOneOf == null ? ImmutableSet.empty() - : Immutables.createSetFrom(sortOneOf); - - // attention: no expand to java.lang here! - Sort existingSort = sorts().lookup(sortName); - if (existingSort == null) { - Sort s = null; - if (isGenericSort) { - try { - var gs = new GenericSort(sortName, ext, oneOf, documentation, - BuilderHelpers.getPosition(idCtx)); - s = gs; - } catch (GenericSupersortException e) { - semanticError(ctx, "Illegal sort given"); - } - } else if (new Name("any").equals(sortName)) { - s = JavaDLTheory.ANY; - } else { - if (isProxySort) { - var ps = new ProxySort(sortName, ext, documentation, - BuilderHelpers.getPosition(idCtx)); - s = ps; + + if(ctx.sortIds == null) { + // parametrised sorts + var declCtx = ctx.parametric_sort_decl(); + assert declCtx != null : "One of the two must be present"; + List typeParams = mapOf(declCtx.formal_sort_param_decl()); + ImmutableList params = Immutables.listOf(typeParams); + var doubled = CollectionUtil.findDuplicates(params.map(SortParameter::genericSort)); + if (!doubled.isEmpty()) { + semanticError(declCtx, + "Type parameters must be unique within a declaration. Found duplicate: %s", doubled.getFirst()); + } + String name = declCtx.simple_ident_dots().getText(); + Name sortName = new Name(name); + var sortDecl = new ParametricSortDeclaration(sortName, ext, isAbstractSort, params, documentation, BuilderHelpers.getPosition(declCtx)); + namespaces().parametricSorts().add(sortDecl); + + } else { + for (var idCtx : ctx.sortIds.simple_ident_dots()) { + var name = idCtx.getText(); + Name sortName = new Name(name); + + // attention: no expand to java.lang here! + Sort existingSort = sorts().lookup(sortName); + if (existingSort == null) { + Sort s = null; + if (isGenericSort) { + try { + s = new GenericSort(sortName, ext, oneOf, documentation, + BuilderHelpers.getPosition(ctx)); + } catch (GenericSupersortException e) { + semanticError(ctx, "Illegal sort given"); + } + } else if (new Name("any").equals(sortName)) { + s = JavaDLTheory.ANY; } else { - var si = new SortImpl(sortName, ext, isAbstractSort, - documentation, BuilderHelpers.getPosition(idCtx)); - s = si; + if (isProxySort) { + s = new ProxySort(sortName, ext, documentation, + BuilderHelpers.getPosition(idCtx)); + } else { + s = new SortImpl(sortName, ext, isAbstractSort, + documentation, BuilderHelpers.getPosition(idCtx)); + } } + // parametric sort declarations are not sorts themselves. + assert s != null; + sorts().add(s); + createdSorts.add(s); + } else { + // weigl: agreement on KaKeY meeting: this should be ignored until we finally have + // local namespaces for generic sorts + // addWarning(ctx, "Sort declaration is ignored, due to collision."); + LOGGER.debug("Sort declaration of {} in {} is ignored due to collision (already " + + "present in {}).", sortName, BuilderHelpers.getPosition(ctx), + existingSort.getOrigin()); } - assert s != null; - sorts().add(s); - createdSorts.add(s); - } else { - // weigl: agreement on KaKeY meeting: this should be ignored until we finally have - // local namespaces for generic sorts - // addWarning(ctx, "Sort declaration is ignored, due to collision."); - LOGGER.debug("Sort declaration of {} in {} is ignored due to collision (already " - + "present in {}).", sortName, BuilderHelpers.getPosition(ctx), - existingSort.getOrigin()); } } return createdSorts; } + @Override + public SortParameter visitFormal_sort_param_decl(KeYParser.Formal_sort_param_declContext ctx) { + ParametricSortDeclaration.Variance variance; + if (ctx.PLUS() != null) + variance = ParametricSortDeclaration.Variance.COVARIANT; + else if (ctx.MINUS() != null) + variance = ParametricSortDeclaration.Variance.CONTRAVARIANT; + else + variance = ParametricSortDeclaration.Variance.INVARIANT; + + var name = ctx.simple_ident().getText(); + Sort paramSort = sorts().lookup(name); + if(paramSort == null) { + semanticError(ctx, "Parameter sort %s not found", name); + } + if(!(paramSort instanceof GenericSort)) { + semanticError(ctx, "Parameter sort %s is not a generic sort", name); + } + + return new SortParameter((GenericSort) paramSort, variance); + } + @Override public Object visitOption_decls(KeYParser.Option_declsContext ctx) { return mapOf(ctx.choice()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java index be6a0efaebf..95689f600bd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java @@ -19,8 +19,9 @@ import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.sort.ArraySort; -import de.uka.ilkd.key.logic.sort.NullSort; +import de.uka.ilkd.key.logic.sort.*; +import de.uka.ilkd.key.logic.sort.ParametricSortDeclaration.Variance; +import de.uka.ilkd.key.logic.sort.ParametricSortDeclaration.SortParameter; import de.uka.ilkd.key.nparser.KeYParser; import de.uka.ilkd.key.rule.RuleSet; @@ -28,7 +29,8 @@ import org.key_project.logic.Named; import org.key_project.logic.ParsableVariable; import org.key_project.logic.sort.Sort; -import org.key_project.util.collection.Pair; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; import org.antlr.v4.runtime.ParserRuleContext; @@ -96,7 +98,7 @@ protected T doLookup(Name n, Namespace... lookups) { if (lookup != null && (l = lookup.lookup(n)) != null) { try { return (T) l; - } catch (ClassCastException e) { + } catch (ClassCastException ignored) { } } } @@ -187,10 +189,10 @@ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, St return null; } - public Sort toArraySort(Pair p, int numOfDimensions) { + public Sort toArraySort(Sort baseSort, Type t, int numOfDimensions) { if (numOfDimensions != 0) { final JavaInfo ji = getJavaInfo(); - Sort sort = ArraySort.getArraySortForDim(p.first, p.second, numOfDimensions, + Sort sort = ArraySort.getArraySortForDim(baseSort, t, numOfDimensions, ji.objectSort(), ji.cloneableSort(), ji.serializableSort()); Sort s = sort; do { @@ -200,7 +202,7 @@ public Sort toArraySort(Pair p, int numOfDimensions) { } while (s instanceof ArraySort && sorts().lookup(s.name()) == null); return sort; } else { - return p.first; + return baseSort; } } @@ -348,17 +350,45 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) { t = PrimitiveType.JAVA_BIGINT; primitiveName = PrimitiveType.JAVA_BIGINT.getName(); } - Sort s = lookupSort(primitiveName); - if (s == null) { - semanticError(ctx, "Could not find sort: %s", ctx.getText()); + + if (t != null && ctx.formal_sort_parameters() != null) { + semanticError(ctx, "Combination of primitive type and type parameters."); + } + + Sort s; + if (ctx.formal_sort_parameters() != null) { + // parametric sorts should be instantiated + ParametricSortDeclaration sortDecl = services.getNamespaces().parametricSorts().lookup(primitiveName); + if (sortDecl == null) { + semanticError(ctx, "Could not find polymorphic sort: %s", primitiveName); + } + ImmutableList parameters = getSorts(ctx.formal_sort_parameters()); + s = ParametricSortInstance.get(sortDecl, parameters); + } else { + s = lookupSort(primitiveName); + if (s == null) { + semanticError(ctx, "Could not find sort: %s", ctx.getText()); + } } if (!ctx.EMPTYBRACKETS().isEmpty()) { - return toArraySort(new Pair<>(s, t), ctx.EMPTYBRACKETS().size()); + return toArraySort(s, t, ctx.EMPTYBRACKETS().size()); } return s; } + private ImmutableList getSorts(KeYParser.Formal_sort_parametersContext ctx) { + List seq = accept(ctx); + assert seq != null; + return ImmutableList.fromList(seq); + } + + @Override + public List visitFormal_sort_parameters( + KeYParser.Formal_sort_parametersContext ctx) { + return mapOf(ctx.sortId()); + } + @Override public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { boolean array = false; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index d34c5c19a13..40494c1784a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -412,7 +412,7 @@ private Term createQuantifiedFormula(KeYParser.Datatype_constructorContext conte var argSort = context.argSort.stream() - .map(it -> sorts().lookup(it.getText())) + .map(it -> (Sort) accept(it)) .toList(); var argNames = context.argName.stream() @@ -604,7 +604,7 @@ private Sort visitSortId(String text, ParserRuleContext ctx) { if (text.contains("[")) { var num = text.indexOf('[') - text.lastIndexOf(']') / 2 + 1; - return toArraySort(new Pair<>(s, t), num); + return toArraySort(s, t, num); } return s; } @@ -748,7 +748,7 @@ public Object visitAddrules(KeYParser.AddrulesContext ctx) { @Override public ImmutableSet visitAddprogvar(KeYParser.AddprogvarContext ctx) { final Collection accept = accept(ctx.pvs); - return Immutables.createSetFrom(Objects.requireNonNull(accept)); + return Immutables.setOf(Objects.requireNonNull(accept)); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java index 6e6ffda4e91..3c6857e6584 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.logic.op.QuantifiableVariable; +import de.uka.ilkd.key.logic.sort.ParametricSortDeclaration; import de.uka.ilkd.key.nparser.KeyIO; import de.uka.ilkd.key.pp.AbbrevMap; @@ -43,11 +44,13 @@ public final class DefaultTermParser { * correctly or the term has an invalid sort. */ public Term parse(Reader in, Sort sort, Services services, - Namespace var_ns, - Namespace func_ns, - Namespace sort_ns, Namespace progVar_ns, AbbrevMap scm) + Namespace var_ns, + Namespace func_ns, + Namespace sort_ns, + Namespace paramSort_ns, + Namespace progVar_ns, AbbrevMap scm) throws ParserException { - return parse(in, sort, services, new NamespaceSet(var_ns, func_ns, sort_ns, + return parse(in, sort, services, new NamespaceSet(var_ns, func_ns, sort_ns, paramSort_ns, new Namespace<>(), new Namespace<>(), progVar_ns), scm); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index ed2304e2cc5..f4d23498c3c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -22,7 +22,6 @@ import de.uka.ilkd.key.logic.label.OriginTermLabelFactory; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.parser.schemajava.SchemaJavaParser; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.JavaModel; @@ -307,16 +306,22 @@ private void cleanupNamespaces(InitConfig initConfig) { Namespace newVarNS = new Namespace<>(); Namespace newSortNS = new Namespace<>(); Namespace newFuncNS = new Namespace<>(); + + // FIXME ulbrich. This is a temporary fix -- + // https://git.key-project.org/key/key/issues/720 + // It does not really work like this. for (Sort n : initConfig.sortNS().allElements()) { - if (!(n instanceof GenericSort)) { - newSortNS.addSafely(n); - } + // if(!(n instanceof GenericSort)) { + newSortNS.addSafely(n); + // } } for (JFunction n : initConfig.funcNS().allElements()) { - if (!(n instanceof SortDependingFunction - && ((SortDependingFunction) n).getSortDependingOn() instanceof GenericSort)) { - newFuncNS.addSafely(n); - } + /* + * if(!(n instanceof SortDependingFunction + * && ((SortDependingFunction) n).getSortDependingOn() instanceof GenericSort)) { + */ + newFuncNS.addSafely(n); + // } } initConfig.getServices().getNamespaces().setVariables(newVarNS); initConfig.getServices().getNamespaces().setSorts(newSortNS); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index b40ef0409c1..9baaaccb09a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -939,7 +939,7 @@ public static Term parseTerm(String value, Proof proof, Namespace progVarNS, Namespace functNS) { try { return new DefaultTermParser().parse(new StringReader(value), null, proof.getServices(), - varNS, functNS, proof.getNamespaces().sorts(), + varNS, functNS, proof.getNamespaces().sorts(), proof.getNamespaces().parametricSorts(), progVarNS, new AbbrevMap()); } catch (ParserException e) { throw new RuntimeException( diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java index 63ebbb3a3f8..0580fd5a410 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java @@ -332,8 +332,8 @@ public ImmutableSet readContracts() { ContractsAndInvariantsFinder cinvs = new ContractsAndInvariantsFinder(initConfig.getServices(), initConfig.namespaces()); getParseContext().accept(cinvs); - specRepos.addContracts(Immutables.createSetFrom(cinvs.getContracts())); - specRepos.addClassInvariants(Immutables.createSetFrom(cinvs.getInvariants())); + specRepos.addContracts(Immutables.setOf(cinvs.getContracts())); + specRepos.addClassInvariants(Immutables.setOf(cinvs.getInvariants())); return DefaultImmutableSet.nil(); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java new file mode 100644 index 00000000000..119837ec4ba --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java @@ -0,0 +1,95 @@ +package de.uka.ilkd.key.logic.sort; + +import de.uka.ilkd.key.java.Recoder2KeY; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.SortDependingFunction; +import de.uka.ilkd.key.nparser.KeyIO; +import de.uka.ilkd.key.nparser.NamespaceBuilder; +import de.uka.ilkd.key.proof.init.AbstractProfile; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.key_project.logic.Name; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSet; + +import static org.junit.jupiter.api.Assertions.*; + +class TestParametricSorts { + + private NamespaceSet nss; + private Services services; + private KeyIO io; + private GenericSort g1; + + @BeforeEach + public void setUp() { + this.services = new Services(AbstractProfile.getDefaultProfile()); + this.nss = services.getNamespaces(); + this.io = new KeyIO(services, nss); + + nss.sorts().add(g1 = new GenericSort(new Name("G1"))); + nss.sorts().add(new GenericSort(new Name("G2"))); + nss.sorts().add(new GenericSort(new Name("G3"))); + nss.sorts().add(new GenericSort(new Name("G4"))); + + NamespaceBuilder nb = new NamespaceBuilder(nss); + nb.addSort("boolean").addSort("int").addSort("Seq").addSort("LocSet").addSort("double") + .addSort("float"); + + Recoder2KeY r2k = new Recoder2KeY(services, nss); + r2k.parseSpecialClasses(); + } + + private ParametricSortDeclaration addParametricSort(String name, ParametricSortDeclaration.Variance... variance) { + ImmutableList params = ImmutableList.of(); + for (int i = 0; i < variance.length; i++) { + ParametricSortDeclaration.Variance varia = variance[i]; + GenericSort genSort = (GenericSort) nss.sorts().lookup("G" + (i + 1)); + params = params.prepend(new ParametricSortDeclaration.SortParameter(genSort, varia)); + } + ParametricSortDeclaration psd = new ParametricSortDeclaration(new Name(name), ImmutableSet.empty(), false, + params, "", ""); + nss.parametricSorts().add(psd); + return psd; + } + + + @Test + public void testParametricSortIdentical() { + ParametricSortDeclaration psd = addParametricSort("List", ParametricSortDeclaration.Variance.COVARIANT); + var sdf = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, new Sort[0], false); + nss.functions().add(sdf); + + var term = io.parseExpression("List<[int]>::someConst = List<[int]>::someConst"); + assertEquals(term.sub(0), term.sub(1)); + assertSame(term.sub(0).sort(), term.sub(1).sort()); + } + + @Test + public void testParametricSortDependentFunctionInstantiation() { + ParametricSortDeclaration psd = addParametricSort("List", ParametricSortDeclaration.Variance.COVARIANT); + Sort intSort = nss.sorts().lookup("int"); + + var someConst = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, new Sort[0], false); + nss.functions().add(someConst); + + var listOfInt = ParametricSortInstance.get(psd, ImmutableList.of(intSort)); + var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(g1)); + var sdf = SortDependingFunction.createFirstInstance(g1, new Name("head"), g1, new Sort[] {listOfG1}, false); + nss.functions().add(sdf); + + SortDependingFunction sdfInst = sdf.getInstanceFor(intSort, services); + assertEquals(intSort, sdfInst.sort()); + assertEquals(listOfInt, sdfInst.argSort(0)); + + var term = io.parseExpression("int::head(List<[int]>::someConst) = int::someConst"); + assertEquals("List<[int]>", term.sub(0).sub(0).sort().toString()); + assertEquals("List<[int]>", ((JFunction)term.sub(0).op()).argSorts().get(0).toString()); + assertEquals("int", term.sub(0).op().sort(null).toString()); + assertSame(term.sub(0).sort(), term.sub(1).sort()); + } + +} \ No newline at end of file diff --git a/key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java b/key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java index 6df86c5c856..60f5791fbdd 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java +++ b/key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.nparser.NamespaceBuilder; import de.uka.ilkd.key.proof.init.AbstractProfile; +import de.uka.ilkd.key.util.parsing.BuildingException; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; @@ -26,6 +27,8 @@ import org.junit.jupiter.api.Disabled; import org.junit.jupiter.api.Test; +import java.io.IOException; + import static org.junit.jupiter.api.Assertions.*; @@ -75,10 +78,12 @@ public void testSortDecl() { "find sort list"); } + + private GenericSort checkGenericSort(Named name, ImmutableSet pExt, ImmutableSet pOneOf) { assertNotNull(name, "Generic sort does not exist"); - assertTrue(name instanceof GenericSort, + assertInstanceOf(GenericSort.class, name, "Generic sort does not have type GenericSort, but " + name.getClass()); GenericSort gs = (GenericSort) name; @@ -91,7 +96,7 @@ private GenericSort checkGenericSort(Named name, ImmutableSet pExt, private Sort checkSort(Named name) { assertNotNull(name, "Sort does not exist"); - assertTrue(name instanceof Sort, "Sort does not have type Sort, but " + name.getClass()); + assertInstanceOf(Sort.class, name, "Sort does not have type Sort, but " + name.getClass()); return (Sort) name; } @@ -102,19 +107,19 @@ public void testProxySortDecl() { Sort P = nss.sorts().lookup(new Name("P")); assertNotNull(P); - assertTrue(P instanceof ProxySort); + assertInstanceOf(ProxySort.class, P); assertEquals("P", P.name().toString()); assertEquals(DefaultImmutableSet.nil().add(JavaDLTheory.ANY), P.extendsSorts()); Sort A = nss.sorts().lookup(new Name("A")); Sort B = nss.sorts().lookup(new Name("B")); Sort Q = nss.sorts().lookup(new Name("Q")); - assertTrue(Q instanceof ProxySort); + assertInstanceOf(ProxySort.class, Q); assertEquals("Q", Q.name().toString()); assertEquals(DefaultImmutableSet.nil().add(A).add(B), Q.extendsSorts()); Sort R = nss.sorts().lookup(new Name("R")); - assertTrue(P instanceof ProxySort); + assertInstanceOf(ProxySort.class, P); assertEquals("R", R.name().toString()); assertEquals(DefaultImmutableSet.nil().add(Q), R.extendsSorts()); } @@ -202,22 +207,69 @@ public void testGenericSortDecl5() { } } + + @Test + public void testParametrisedSortDecls() { + evaluateDeclarations("\\sorts { \\generic G, H; ADT<[+G]>; Fun<[-G,-H]>; Invar<[G]>; }"); + var adt = serv.getNamespaces().parametricSorts().lookup("ADT"); + assertNotNull(adt); + assertEquals("ADT", adt.name().toString()); + assertEquals("[SortParameter[genericSort=G, variance=COVARIANT]]", adt.getParameters().toString()); + + var fun = serv.getNamespaces().parametricSorts().lookup("Fun"); + assertNotNull(fun); + assertEquals("Fun", fun.name().toString()); + assertEquals("[SortParameter[genericSort=G, variance=CONTRAVARIANT]," + + "SortParameter[genericSort=H, variance=CONTRAVARIANT]]", fun.getParameters().toString()); + + var invar = serv.getNamespaces().parametricSorts().lookup("Invar"); + assertNotNull(invar); + assertEquals("Invar", invar.name().toString()); + assertEquals("[SortParameter[genericSort=G, variance=INVARIANT]]", invar.getParameters().toString()); + + var exc = assertThrowsExactly(BuildingException.class, () -> { + KeyIO.Loader l = io.load("\\sorts { \\generic G; ADT<[+G,G]>; }"); + l.parseFile().loadDeclarations().loadSndDegreeDeclarations().loadTaclets(); + }); + assertTrue(exc.getMessage().contains("Type parameters must be unique within a declaration")); + + exc = assertThrowsExactly(BuildingException.class, () -> { + KeyIO.Loader l = io.load("\\sorts { X; ADT<[X]>; }"); + l.parseFile().loadDeclarations().loadSndDegreeDeclarations().loadTaclets(); + }); + + assertTrue(exc.getMessage().contains("Sort 'X' is not a generic sort")); + + exc = assertThrowsExactly(BuildingException.class, () -> { + KeyIO.Loader l = io.load("\\sorts { ADT<[Y]>; }"); + l.parseFile().loadDeclarations().loadSndDegreeDeclarations().loadTaclets(); + }); + assertTrue(exc.getMessage().contains("Could not find sort 'Y'.")); + } + + @Test + public void testParametrisedFunDecls() throws IOException { + KeyIO.Loader l = io.load("\\sorts { \\generic A; \\generic G; ADT<[+G]>; } " + + "\\functions { int f(ADT<[int]>); A A::g(ADT<[A]>); }"); + l.parseFile().loadDeclarations().loadSndDegreeDeclarations().loadTaclets(); + } + /** * asserts that the found object is a schemavariable and that the allowed macthing type is * QuantifiableVariable */ private void assertVariableSV(String msg, Object o) { - assertTrue(o instanceof SchemaVariable, "The named object: " + o + " is of type " + assertInstanceOf(SchemaVariable.class, o, "The named object: " + o + " is of type " + o.getClass() + ", but the type SchemaVariable was expected"); - assertTrue(o instanceof VariableSV, msg); + assertInstanceOf(VariableSV.class, o, msg); } /** * asserts that the SchemaVariable matches to term but not to a formula */ private void assertTermSV(String msg, Object o) { - assertTrue(o instanceof TermSV, "The named object: " + o + " is of type " + assertInstanceOf(TermSV.class, o, "The named object: " + o + " is of type " + o.getClass() + ", but the type SchemaVariable was expected"); assertNotSame(((TermSV) o).sort(), JavaDLTheory.FORMULA, "Schemavariable is not allowed to match a term of sort FORMULA."); @@ -228,7 +280,7 @@ private void assertTermSV(String msg, Object o) { * Sort.FORMULA) */ private void assertFormulaSV(String msg, Object o) { - assertTrue(o instanceof FormulaSV, "The named object: " + o + " is of type " + assertInstanceOf(FormulaSV.class, o, "The named object: " + o + " is of type " + o.getClass() + ", but the type SchemaVariable was expected"); assertSame(((FormulaSV) o).sort(), JavaDLTheory.FORMULA, "Only matches to terms of sort FORMULA allowed. " + "But term has sort " diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java index 47f83efdec1..fe70256c639 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java @@ -192,13 +192,13 @@ public void setUp() { proof.add(g); proof.setNamespaces(new NamespaceSet(variables, functions, sorts, new Namespace<>(), - new Namespace<>(), new Namespace<>())); + new Namespace<>(), new Namespace<>(), new Namespace<>())); } private Term parseTerm(String termstr) { return TacletForTests.parseTerm(termstr, new NamespaceSet(variables, functions, sorts, - new Namespace<>(), new Namespace<>(), new Namespace<>())); + new Namespace<>(), new Namespace<>(), new Namespace<>(), new Namespace<>())); } @Test diff --git a/key.ncore/src/main/java/org/key_project/logic/Name.java b/key.ncore/src/main/java/org/key_project/logic/Name.java index 99b8602d8d3..b1fe26e4950 100644 --- a/key.ncore/src/main/java/org/key_project/logic/Name.java +++ b/key.ncore/src/main/java/org/key_project/logic/Name.java @@ -22,7 +22,7 @@ public class Name implements Comparable { * creates a name object */ public Name(String n) { - nameString = (n == null ? NONAME : n).intern(); + nameString = n.intern(); } @Override diff --git a/key.ncore/src/main/java/org/key_project/logic/Named.java b/key.ncore/src/main/java/org/key_project/logic/Named.java index 043993a79ad..075e759528c 100644 --- a/key.ncore/src/main/java/org/key_project/logic/Named.java +++ b/key.ncore/src/main/java/org/key_project/logic/Named.java @@ -8,12 +8,10 @@ * their name. */ public interface Named { - /** * returns the name of this element * * @return the name of the element */ Name name(); - } diff --git a/key.ncore/src/main/java/org/key_project/logic/TermCreationException.java b/key.ncore/src/main/java/org/key_project/logic/TermCreationException.java index cc7ea6a1be5..77557f3abfb 100644 --- a/key.ncore/src/main/java/org/key_project/logic/TermCreationException.java +++ b/key.ncore/src/main/java/org/key_project/logic/TermCreationException.java @@ -10,12 +10,6 @@ public class TermCreationException extends RuntimeException { - - /** - * generated serial version UID - */ - private static final long serialVersionUID = -7173044450561438150L; - public TermCreationException(String errorMessage) { super(errorMessage); } @@ -62,19 +56,9 @@ private static String subsToString(ImmutableArray subs) { for (int i = 0, n = subs.size(); i < n; i++) { sb.append(i + 1).append(".) "); Term subi = subs.get(i); - if (subi != null) { - sb.append(subi); - Sort subiSort = subi.sort(); - if (subiSort != null) { - sb.append("(sort: ").append(subi.sort()).append(", sort hash: ") - .append(subi.sort().hashCode()).append(")\n"); - } else { - sb.append("(Unknown sort, \"null pointer\")"); - } - } else { - sb.append(" !null!\n"); - } - + sb.append(subi); + sb.append("(sort: ").append(subi.sort()).append(", sort hash: ") + .append(subi.sort().hashCode()).append(")\n"); } return sb.toString(); } diff --git a/key.ncore/src/main/java/org/key_project/logic/op/AbstractOperator.java b/key.ncore/src/main/java/org/key_project/logic/op/AbstractOperator.java index c9c4dbdac84..0f1f7bd03db 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/AbstractOperator.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/AbstractOperator.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.logic.op; +import java.util.Objects; + import org.key_project.logic.Name; import org.key_project.logic.Term; import org.key_project.logic.TermCreationException; @@ -16,15 +18,18 @@ public abstract class AbstractOperator implements Operator { private final Name name; private final int arity; + + // weigl: should rather be a bit field (int) private final @Nullable ImmutableArray whereToBind; private final Modifier modifier; - protected AbstractOperator(Name name, int arity, - @Nullable ImmutableArray whereToBind, + protected AbstractOperator(Name name, int arity, @Nullable ImmutableArray whereToBind, Modifier modifier) { - assert arity >= 0; - assert whereToBind == null || whereToBind.size() == arity; - this.name = name; + if (arity < 0) + throw new IllegalArgumentException("arity is negative"); + if (whereToBind != null && whereToBind.size() != arity) + throw new AssertionError(); + this.name = Objects.requireNonNull(name); this.arity = arity; this.whereToBind = whereToBind; this.modifier = modifier; diff --git a/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java b/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java index c5fcfd7b340..3addbf95d15 100644 --- a/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java +++ b/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java @@ -15,6 +15,8 @@ public abstract class AbstractSort implements Sort { private final Name name; private final boolean isAbstract; + private final @Nullable String origin; + /** * Documentation for this sort given by the associated documentation comment. * //@see de.uka.ilkd.key.nparser.KeYParser.One_sort_declContext#doc @@ -22,8 +24,15 @@ public abstract class AbstractSort implements Sort { private @Nullable String documentation; public AbstractSort(Name name, boolean isAbstract) { + this(name, isAbstract, null, null); + } + + public AbstractSort(Name name, boolean isAbstract, @Nullable String origin, + @Nullable String documentation) { this.name = name; this.isAbstract = isAbstract; + this.origin = origin; + this.documentation = documentation; } public boolean equals(@Nullable Object o) { @@ -62,4 +71,9 @@ public void setDocumentation(@Nullable String documentation) { public @Nullable String getDocumentation() { return documentation; } + + @Override + public @Nullable String getOrigin() { + return origin; + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java b/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java index e1564edfe7d..074ef954059 100644 --- a/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java +++ b/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java @@ -12,19 +12,35 @@ public interface Sort extends Named, HasOrigin { /** - * @return the direct supersorts of this sort. Not supported by {@code NullSort}. + * Gives the set of sorts that are direct super-sorts of this sort. + * + * The NullSort implementation fails on this method. + * + * @return a non-null set of sorts. */ ImmutableSet extendsSorts(); + /** + * Gives the set of sorts that are direct super-sorts of this sort. + * + * The NullSort implementation does not fail on this method. + * + * By default, this method calls {@link #extendsSorts()}. + * + * @param services the logic services to use for computing super-sorts. + * @return a non-null set of sorts. + */ default ImmutableSet extendsSorts(Services services) { return extendsSorts(); } /** - * @param s some sort. + * Check whether this sort is a direct or indirect subsort of the given sort. + * + * @param sort some sort. * @return whether the given sort is a reflexive, transitive subsort of this sort. */ - boolean extendsTrans(Sort s); + boolean extendsTrans(Sort sort); /** * @return whether this sort has no exact elements. @@ -34,7 +50,8 @@ default ImmutableSet extendsSorts(Service String declarationString(); /** - * Returns a human explainable text describing this sort. This field is typical set by the + * Returns a human explainable text describing this sort. + * This field is typically set by the * parser, who captures the documentation comments. */ default @Nullable String getDocumentation() { return null; } diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java index ba1af27f3c9..05d00d21ce4 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java @@ -4,6 +4,7 @@ package org.key_project.util.collection; import java.util.*; +import java.util.function.Function; import java.util.function.Predicate; import java.util.stream.Stream; import java.util.stream.StreamSupport; @@ -213,6 +214,11 @@ public boolean exists(Predicate predicate) { return elementList.exists(predicate); } + @Override + public ImmutableSet map(Function f) { + return new DefaultImmutableSet<>(elementList.map(f)); + } + /** @return int the cardinality of the set */ @Override public int size() { diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index b46809d980a..80c19e0f0e9 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -372,4 +372,14 @@ default T get(int idx) { return take(idx).head(); } + /** + * Replace the element at position {@code pos} in the list + * by the value {@code t}. + * + * @param pos the position within the list {@code 0 <= pos && pos < size()} + * @param t the element to set, may be {@code null}. + * @return an immutable list in which only the element at pos has been replaced. + * @throws IndexOutOfBoundsException if pos is not a valid index in the list. + */ + ImmutableList replace(int pos, T t); } diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java index 47ac855f11f..84607a3ba87 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java @@ -175,6 +175,26 @@ public ImmutableList take(int n) { } + // Implemented imperatively to avoid arbitrarily deep recursion + @Override + public ImmutableList replace(int pos, T s) { + if (pos < 0 || pos >= size()) { + throw new IndexOutOfBoundsException(); + } + + ImmutableList already = nil(); + ImmutableList rest = this; + + while (pos > 0) { + already = already.prepend(rest.head()); + rest = rest.tail(); + pos--; + } + + return rest.tail().prepend(s).prepend(already.reverse()); + } + + private static class Cons extends ImmutableSLList { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java index ec69790c40d..c607a421ed5 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java @@ -4,6 +4,7 @@ package org.key_project.util.collection; import java.util.*; +import java.util.function.Function; import java.util.function.Predicate; import java.util.stream.Collector; import java.util.stream.Collector.Characteristics; @@ -28,7 +29,7 @@ public interface ImmutableSet return Collector.of(HashSet::new, Set::add, (set1, set2) -> { set1.addAll(set2); return set1; - }, Immutables::createSetFrom, Characteristics.UNORDERED); + }, Immutables::setOf, Characteristics.UNORDERED); } /** @@ -76,6 +77,18 @@ public interface ImmutableSet */ boolean exists(Predicate predicate); + /** + * Apply a function f to the elements of the set. + * If the set has an order: + * The result contains the elements in the same order, but after the + * application of f. + * + * @param f the function to apply to the elements + * @param result type of the mapping + * @return a new immutable list instance, not null. + */ + ImmutableSet map(Function f); + /** @return true iff obj in set */ boolean contains(T obj); diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index 03e7aca6e37..eca21e7a6f7 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/key.util/src/main/java/org/key_project/util/collection/Immutables.java @@ -4,6 +4,7 @@ package org.key_project.util.collection; import java.util.HashSet; +import java.util.function.BiFunction; import java.util.function.Function; import java.util.function.Predicate; @@ -12,7 +13,7 @@ /** * This class is a collection of methods that operate on immutable collections, in particular * {@link ImmutableSet}s and {@link ImmutableList}s. - * + *

* This class cannot be instantiated. * * @author Mattias Ulbrich @@ -25,11 +26,11 @@ private Immutables() { /** * Checks whether an immutable list is free of duplicates. - * + *

* A list has a duplicate if it during iteration it visits two objects o1 and o2 such that * o1==null ? o2 == null : o1.equals(o2) is true. null may appear in * the list. - * + *

* The implementation uses a hash set internally and thus runs in O(n). * * @param list any list, must not be null @@ -49,27 +50,26 @@ private Immutables() { /** * Removes duplicate entries from an immutable list. - * + *

* A list has a duplicate if it during iteration it visits two objects o1 and o2 such that * o1==null ? o2 == null : o1.equals(o2) is true. null may appear in * the list. - * + *

* If an element occurs duplicated, its first (in order of iteration) occurrence is kept, while * later occurrences are removeed. - * + *

* If a list iterates "a", "b", "a" in this order, removeDuplicates returns a list iterating * "a", "b". - * + *

* The implementation uses a hash set internally and thus runs in O(n). - * + *

* It reuses as much created datastructure as possible. In particular, if the list is already * duplicate-free, it does not allocate new memory (well, only temporarily) and returns the * argument. - * + *

* Sidenote: Would that not make a nice KeY-Verification condition? Eat your own dogfood. * * @param list any list, must not be null - * * @return a duplicate-free version of the argument, never null */ public static ImmutableList removeDuplicates( @@ -147,15 +147,15 @@ private Immutables() { * * @return the view onto the iterable as an immutable set */ - public static ImmutableSet createSetFrom( + public static ImmutableSet setOf( Iterable iterable) { - return DefaultImmutableSet.fromImmutableList(createListFrom(iterable)); + return DefaultImmutableSet.fromImmutableList(listOf(iterable)); } /** * Returns an immutable list consisting of the elements of the * given iterable collection. - * + *

* The iteration order of the result is identical to that of the argument. * * @param iterable the collection to iterate through to obtain the elements @@ -163,7 +163,7 @@ private Immutables() { * * @return the view onto the iterable as an immutable list */ - public static ImmutableList createListFrom(Iterable iterable) { + public static ImmutableList listOf(Iterable iterable) { ImmutableList result = ImmutableSLList.nil(); for (T t : iterable) { result = result.prepend(t); @@ -176,11 +176,9 @@ public static ImmutableList createListFrom(Iterable iterable * the given predicate. * * @param ts non-null immutable list. - * * @param predicate a non-interfering, stateless * predicate to apply to each element to determine if it * should be included - * * @returns the filtered list */ public static ImmutableList filter(ImmutableList ts, @@ -219,4 +217,42 @@ public static ImmutableList createListFrom(Iterable iterable } return acc.reverse(); } + + public static ImmutableList listOf(T... elements) { + ImmutableList result = ImmutableSLList.nil(); + for (T t : elements) { + result = result.prepend(t); + } + return result.reverse(); + } + + public static ImmutableList listOf(T element) { + ImmutableList result = ImmutableSLList.nil(); + result = result.prepend(element); + return result.reverse(); + } + + public static ImmutableSet setOf(T... elements) { + return DefaultImmutableSet.fromImmutableList(listOf(elements)); + } + + public static ImmutableSet setOf(T element) { + return DefaultImmutableSet.fromImmutableList(listOf(element)); + } + + public static ImmutableList zip(ImmutableList list1, ImmutableList list2, BiFunction zipper) { + ImmutableList result = ImmutableSLList.nil(); + while (!list1.isEmpty() && !list2.isEmpty()) { + result = result.prepend(zipper.apply(list1.head(), list2.head())); + list1 = list1.tail(); + list2 = list2.tail(); + } + return result.reverse(); + } + + @Deprecated + public static ImmutableList> zip(ImmutableList list1, ImmutableList list2) { + return zip(list1, list2, Pair::new); + } + } diff --git a/key.util/src/main/java/org/key_project/util/collection/Pair.java b/key.util/src/main/java/org/key_project/util/collection/Pair.java index 29a7d3f9393..fcc00f58af9 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Pair.java +++ b/key.util/src/main/java/org/key_project/util/collection/Pair.java @@ -15,7 +15,11 @@ * * @param type of first element * @param type of second element + * @deprecated weigl: You should not use this class. + * Since Java 17+ we have records, aka. NamedTuples. + * Use records; They can be documented; They avoid auto-boxing. */ +@Deprecated public class Pair { /** * First element. diff --git a/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java b/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java index baa70c6c94f..e78ccec4c7b 100644 --- a/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java @@ -305,4 +305,25 @@ public static void addAll(Collection collection, Iterable iterable) { list.add(index, toInsert); } } + + /** + * Finds all duplicated elements in the given collection. + * + * The order of reported elements is in order of appearance in the collection. + * They are reported on the second and subsequent occurrences. + * + * @param collection The collection to search for duplicates. + * @return A list of all duplicated elements. + */ + public static List findDuplicates(Iterable collection) { + List result = new ArrayList<>(); + Set alreadySeen = new HashSet<>(); + for (T element : collection) { + if (!alreadySeen.add(element)) { + result.add(element); + } + } + return result; + } + } diff --git a/key.util/src/test/java/org/key_project/util/collection/TestSLList.java b/key.util/src/test/java/org/key_project/util/collection/TestSLList.java new file mode 100644 index 00000000000..d198eddefda --- /dev/null +++ b/key.util/src/test/java/org/key_project/util/collection/TestSLList.java @@ -0,0 +1,55 @@ +/* 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 org.key_project.util.collection; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +public class TestSLList { + + @Test + public void testRemoveAll() { + ImmutableList l = ImmutableSLList.nil().prepend(1, 2, 1, 2); + + assertEquals("[1,1]", l.removeAll(2).toString()); + } + + @Test + public void testMap() { + ImmutableList l = ImmutableSLList.nil().prepend(1, 2, -1, -2); + + assertEquals("[1,4,1,4]", l.map(x -> x * x).toString()); + } + + @Test + public void testReplace() { + ImmutableList l = ImmutableSLList.nil().prepend(1, 2, 3, 4); + + assertEquals("[1,2,0,4]", l.replace(2, 0).toString()); + assertEquals("[0,2,3,4]", l.replace(0, 0).toString()); + assertEquals("[1,2,3,0]", l.replace(3, 0).toString()); + } + + @Test + public void testReplaceBounds1() { + Assertions.assertThrows(IndexOutOfBoundsException.class, () -> { + ImmutableList l = ImmutableSLList.nil().prepend(1, 2, 3, 4); + + System.out.println(l.replace(-1, 0)); + }); + } + + // revealed a bug + @Test + public void testReplaceBounds2() { + Assertions.assertThrows(IndexOutOfBoundsException.class, () -> { + ImmutableList l = ImmutableSLList.nil().prepend(1, 2, 3, 4); + + System.out.println(l.replace(4, 0)); + }); + } + +}