diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java index 4bc1ac4d096..65061820a14 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java +++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java @@ -80,6 +80,9 @@ protected final void mergeNamespaces(Proof initiatingProof, Proof sideProof) { mergeNamespace(initiatingProofNS.functions(), sideProofNS.functions()); mergeNamespace(initiatingProofNS.ruleSets(), sideProofNS.ruleSets()); mergeNamespace(initiatingProofNS.sorts(), sideProofNS.sorts()); + mergeNamespace(initiatingProofNS.sortAliases(), sideProofNS.sortAliases()); + mergeNamespace(initiatingProofNS.parametricSorts(), sideProofNS.parametricSorts()); + mergeNamespace(initiatingProofNS.parametricFunctions(), sideProofNS.parametricFunctions()); mergeNamespace(initiatingProofNS.choices(), sideProofNS.choices()); } diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 37e4ecaff27..60113499f8f 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -78,6 +78,7 @@ PROXY : '\\proxy'; EXTENDS : '\\extends'; ONEOF : '\\oneof'; ABSTRACT : '\\abstract'; +ALIAS: '\\alias'; // Keywords used in schema variable declarations SCHEMAVARIABLES : '\\schemaVariables'; diff --git a/key.core/src/main/antlr4/KeYLexer.tokens b/key.core/src/main/antlr4/KeYLexer.tokens deleted file mode 100644 index 45228a531f6..00000000000 --- a/key.core/src/main/antlr4/KeYLexer.tokens +++ /dev/null @@ -1,388 +0,0 @@ -MODALITY=1 -SORTS=2 -GENERIC=3 -PROXY=4 -EXTENDS=5 -ONEOF=6 -ABSTRACT=7 -SCHEMAVARIABLES=8 -SCHEMAVAR=9 -MODALOPERATOR=10 -PROGRAM=11 -FORMULA=12 -TERM=13 -UPDATE=14 -VARIABLES=15 -VARIABLE=16 -SKOLEMTERM=17 -SKOLEMFORMULA=18 -TERMLABEL=19 -MODIFIABLE=20 -PROGRAMVARIABLES=21 -STORE_TERM_IN=22 -STORE_STMT_IN=23 -HAS_INVARIANT=24 -GET_INVARIANT=25 -GET_FREE_INVARIANT=26 -GET_VARIANT=27 -IS_LABELED=28 -SAME_OBSERVER=29 -VARCOND=30 -APPLY_UPDATE_ON_RIGID=31 -DEPENDINGON=32 -DISJOINTMODULONULL=33 -DROP_EFFECTLESS_ELEMENTARIES=34 -DROP_EFFECTLESS_STORES=35 -SIMPLIFY_IF_THEN_ELSE_UPDATE=36 -ENUM_CONST=37 -FREELABELIN=38 -HASSORT=39 -FIELDTYPE=40 -FINAL=41 -ELEMSORT=42 -HASLABEL=43 -HASSUBFORMULAS=44 -ISARRAY=45 -ISARRAYLENGTH=46 -ISCONSTANT=47 -ISENUMTYPE=48 -ISINDUCTVAR=49 -ISLOCALVARIABLE=50 -ISOBSERVER=51 -DIFFERENT=52 -METADISJOINT=53 -ISTHISREFERENCE=54 -DIFFERENTFIELDS=55 -ISREFERENCE=56 -ISREFERENCEARRAY=57 -ISSTATICFIELD=58 -ISMODELFIELD=59 -ISINSTRICTFP=60 -ISSUBTYPE=61 -EQUAL_UNIQUE=62 -NEW=63 -NEW_TYPE_OF=64 -NEW_DEPENDING_ON=65 -NEW_LOCAL_VARS=66 -HAS_ELEMENTARY_SORT=67 -NEWLABEL=68 -CONTAINS_ASSIGNMENT=69 -NOT_=70 -NOTFREEIN=71 -SAME=72 -STATIC=73 -STATICMETHODREFERENCE=74 -MAXEXPANDMETHOD=75 -STRICT=76 -TYPEOF=77 -INSTANTIATE_GENERIC=78 -FORALL=79 -EXISTS=80 -SUBST=81 -IF=82 -IFEX=83 -THEN=84 -ELSE=85 -INCLUDE=86 -INCLUDELDTS=87 -CLASSPATH=88 -BOOTCLASSPATH=89 -NODEFAULTCLASSES=90 -JAVASOURCE=91 -WITHOPTIONS=92 -OPTIONSDECL=93 -KEYSETTINGS=94 -PROFILE=95 -TRUE=96 -FALSE=97 -SAMEUPDATELEVEL=98 -INSEQUENTSTATE=99 -ANTECEDENTPOLARITY=100 -SUCCEDENTPOLARITY=101 -CLOSEGOAL=102 -HEURISTICSDECL=103 -NONINTERACTIVE=104 -DISPLAYNAME=105 -HELPTEXT=106 -REPLACEWITH=107 -ADDRULES=108 -ADDPROGVARS=109 -HEURISTICS=110 -FIND=111 -ADD=112 -ASSUMES=113 -TRIGGER=114 -AVOID=115 -PREDICATES=116 -FUNCTIONS=117 -DATATYPES=118 -TRANSFORMERS=119 -UNIQUE=120 -FREE=121 -RULES=122 -AXIOMS=123 -PROBLEM=124 -CHOOSECONTRACT=125 -PROOFOBLIGATION=126 -PROOF=127 -PROOFSCRIPT=128 -CONTRACTS=129 -INVARIANTS=130 -LEMMA=131 -IN_TYPE=132 -IS_ABSTRACT_OR_INTERFACE=133 -IS_FINAL=134 -CONTAINERTYPE=135 -UTF_PRECEDES=136 -UTF_IN=137 -UTF_EMPTY=138 -UTF_UNION=139 -UTF_INTERSECT=140 -UTF_SUBSET_EQ=141 -UTF_SUBSEQ=142 -UTF_SETMINUS=143 -SEMI=144 -SLASH=145 -COLON=146 -DOUBLECOLON=147 -ASSIGN=148 -DOT=149 -DOTRANGE=150 -COMMA=151 -LPAREN=152 -RPAREN=153 -LBRACE=154 -RBRACE=155 -LBRACKET=156 -RBRACKET=157 -EMPTYBRACKETS=158 -AT=159 -PARALLEL=160 -OR=161 -AND=162 -NOT=163 -IMP=164 -EQUALS=165 -NOT_EQUALS=166 -SEQARROW=167 -EXP=168 -TILDE=169 -PERCENT=170 -STAR=171 -MINUS=172 -PLUS=173 -GREATER=174 -GREATEREQUAL=175 -OPENTYPEPARAMS=176 -CLOSETYPEPARAMS=177 -WS=178 -STRING_LITERAL=179 -LESS=180 -LESSEQUAL=181 -LGUILLEMETS=182 -RGUILLEMETS=183 -EQV=184 -CHAR_LITERAL=185 -QUOTED_STRING_LITERAL=186 -SL_COMMENT=187 -BIN_LITERAL=188 -HEX_LITERAL=189 -IDENT=190 -INT_LITERAL=191 -FLOAT_LITERAL=192 -DOUBLE_LITERAL=193 -REAL_LITERAL=194 -ERROR_UKNOWN_ESCAPE=195 -ERROR_CHAR=196 -COMMENT_END=197 -DOC_COMMENT=198 -ML_COMMENT=199 -MODALITYD=200 -MODALITYB=201 -MODALITYBB=202 -MODAILITYGENERIC1=203 -MODAILITYGENERIC2=204 -MODAILITYGENERIC3=205 -MODAILITYGENERIC4=206 -MODAILITYGENERIC5=207 -MODAILITYGENERIC6=208 -MODAILITYGENERIC7=209 -MODALITYD_END=210 -MODALITYD_STRING=211 -MODALITYD_CHAR=212 -MODALITYG_END=213 -MODALITYB_END=214 -MODALITYBB_END=215 -'\\sorts'=2 -'\\generic'=3 -'\\proxy'=4 -'\\extends'=5 -'\\oneof'=6 -'\\abstract'=7 -'\\schemaVariables'=8 -'\\schemaVar'=9 -'\\modalOperator'=10 -'\\program'=11 -'\\formula'=12 -'\\term'=13 -'\\update'=14 -'\\variables'=15 -'\\variable'=16 -'\\skolemTerm'=17 -'\\skolemFormula'=18 -'\\termlabel'=19 -'\\modifiable'=20 -'\\programVariables'=21 -'\\storeTermIn'=22 -'\\storeStmtIn'=23 -'\\hasInvariant'=24 -'\\getInvariant'=25 -'\\getFreeInvariant'=26 -'\\getVariant'=27 -'\\isLabeled'=28 -'\\sameObserver'=29 -'\\varcond'=30 -'\\applyUpdateOnRigid'=31 -'\\dependingOn'=32 -'\\disjointModuloNull'=33 -'\\dropEffectlessElementaries'=34 -'\\dropEffectlessStores'=35 -'\\simplifyIfThenElseUpdate'=36 -'\\enumConstant'=37 -'\\freeLabelIn'=38 -'\\hasSort'=39 -'\\fieldType'=40 -'\\final'=41 -'\\elemSort'=42 -'\\hasLabel'=43 -'\\hasSubFormulas'=44 -'\\isArray'=45 -'\\isArrayLength'=46 -'\\isConstant'=47 -'\\isEnumType'=48 -'\\isInductVar'=49 -'\\isLocalVariable'=50 -'\\isObserver'=51 -'\\different'=52 -'\\metaDisjoint'=53 -'\\isThisReference'=54 -'\\differentFields'=55 -'\\isReference'=56 -'\\isReferenceArray'=57 -'\\isStaticField'=58 -'\\isModelField'=59 -'\\isInStrictFp'=60 -'\\sub'=61 -'\\equalUnique'=62 -'\\new'=63 -'\\newTypeOf'=64 -'\\newDependingOn'=65 -'\\newLocalVars'=66 -'\\hasElementarySort'=67 -'\\newLabel'=68 -'\\containsAssignment'=69 -'\\not'=70 -'\\notFreeIn'=71 -'\\same'=72 -'\\static'=73 -'\\staticMethodReference'=74 -'\\mayExpandMethod'=75 -'\\strict'=76 -'\\typeof'=77 -'\\instantiateGeneric'=78 -'\\subst'=81 -'\\if'=82 -'\\ifEx'=83 -'\\then'=84 -'\\else'=85 -'\\include'=86 -'\\includeLDTs'=87 -'\\classpath'=88 -'\\bootclasspath'=89 -'\\noDefaultClasses'=90 -'\\javaSource'=91 -'\\withOptions'=92 -'\\optionsDecl'=93 -'\\settings'=94 -'\\profile'=95 -'true'=96 -'false'=97 -'\\sameUpdateLevel'=98 -'\\inSequentState'=99 -'\\antecedentPolarity'=100 -'\\succedentPolarity'=101 -'\\closegoal'=102 -'\\heuristicsDecl'=103 -'\\noninteractive'=104 -'\\displayname'=105 -'\\helptext'=106 -'\\replacewith'=107 -'\\addrules'=108 -'\\addprogvars'=109 -'\\heuristics'=110 -'\\find'=111 -'\\add'=112 -'\\assumes'=113 -'\\trigger'=114 -'\\avoid'=115 -'\\predicates'=116 -'\\functions'=117 -'\\datatypes'=118 -'\\transformers'=119 -'\\unique'=120 -'\\free'=121 -'\\rules'=122 -'\\axioms'=123 -'\\problem'=124 -'\\chooseContract'=125 -'\\proofObligation'=126 -'\\proof'=127 -'\\proofScript'=128 -'\\contracts'=129 -'\\invariants'=130 -'\\lemma'=131 -'\\inType'=132 -'\\isAbstractOrInterface'=133 -'\\isFinal'=134 -'\\containerType'=135 -';'=144 -'/'=145 -':'=146 -'::'=147 -':='=148 -'.'=149 -','=151 -'('=152 -')'=153 -'{'=154 -'}'=155 -'['=156 -']'=157 -'@'=159 -'='=165 -'^'=168 -'~'=169 -'%'=170 -'*'=171 -'-'=172 -'+'=173 -'>'=174 -'<['=176 -']>'=177 -'<'=180 -'/*!'=198 -'/*'=199 -'\\<'=200 -'\\['=201 -'\\[['=202 -'\\box'=203 -'\\diamond'=204 -'\\diamond_transaction'=205 -'\\modality'=206 -'\\box_transaction'=207 -'\\throughout'=208 -'\\throughout_transaction'=209 -'\\>'=210 -'\\endmodality'=213 -'\\]'=214 -'\\]]'=215 diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 6e992d132f3..5832a7238f7 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -95,6 +95,7 @@ one_sort_decl (EXTENDS sortExt = extends_sorts)? SEMI | PROXY 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 + | ALIAS simple_ident_dots EQUALS sortId SEMI ) ; diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java index d78dd88ac7b..14fe2cae39d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java @@ -194,7 +194,8 @@ private JTerm parseTerm(String s, Namespace<@NonNull QuantifiableVariable> varNS private IdDeclaration parseIdDeclaration(String s) throws ParserException { KeYParser.Id_declarationContext ctx = ParsingFacade.parseIdDeclaration(CharStreams.fromString(s)); - Sort sort = ctx.s != null ? services.getNamespaces().sorts().lookup(ctx.s.getText()) : null; + Sort sort = + ctx.s != null ? services.getNamespaces().lookupSortOrAlias(ctx.s.getText()) : null; return new IdDeclaration(ctx.id.getText(), sort); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java index 027dfd622e8..0b5168fc04a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java @@ -19,7 +19,6 @@ import de.uka.ilkd.key.util.Debug; import org.key_project.logic.Name; -import org.key_project.logic.Namespace; import org.key_project.logic.sort.Sort; import org.key_project.util.LRUCache; import org.key_project.util.collection.*; @@ -327,8 +326,7 @@ public KeYJavaType getPrimitiveKeYJavaType(PrimitiveType type) { ldtName = type.getCorrespondingLDTName(); } - Namespace sorts = services.getNamespaces().sorts(); - Sort sort = sorts.lookup(ldtName); + Sort sort = services.getNamespaces().lookupSortOrAlias(ldtName); if (sort == null) { throw new IllegalStateException( diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 02cb218f130..57e48d5a634 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -755,7 +755,7 @@ public DLEmbeddedExpression convert(EscapeExpression e) { if (name.startsWith(PREFIX)) { // handle default value resolution String sortName = name.substring(PREFIX.length()).trim(); - Sort sort = namespaceSet.sorts().lookup(sortName); + Sort sort = namespaceSet.lookupSortOrAlias(sortName); if (sort == null) { throw new ConvertException(format( "Requested to find the default value of an unknown sort '%s'. " + "Line/Col:%s", diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java index 030eb61b230..585048888ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java @@ -267,7 +267,7 @@ private void addKeYJavaType(recoder.abstraction.Type t, Sort s) { Debug.fail(); } } else { - if (namespaces.sorts().lookup(s.name()) == null) { + if (namespaces.lookupSortOrAlias(s.name()) == null) { namespaces.sorts().add(s); } result = new KeYJavaType(s); 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 47221e72b27..6ba5f8da3d0 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,7 @@ import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; import de.uka.ilkd.key.logic.sort.ParametricSortDecl; +import de.uka.ilkd.key.logic.sort.SortAlias; import org.key_project.logic.Choice; import org.key_project.logic.Name; @@ -18,6 +19,7 @@ import org.key_project.prover.rules.RuleSet; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; public class NamespaceSet { @@ -27,6 +29,7 @@ public class NamespaceSet { private Namespace<@NonNull Function> funcNS = new Namespace<>(); private Namespace<@NonNull RuleSet> ruleSetNS = new Namespace<>(); private Namespace<@NonNull Sort> sortNS = new Namespace<>(); + private Namespace<@NonNull SortAlias> sortAliases = new Namespace<>(); private Namespace<@NonNull ParametricSortDecl> parametricSortNS = new Namespace<>(); private Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS = new Namespace<>(); private Namespace<@NonNull Choice> choiceNS = new Namespace<>(); @@ -36,7 +39,8 @@ public NamespaceSet() { public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, Namespace<@NonNull Function> funcNS, - Namespace<@NonNull Sort> sortNS, Namespace<@NonNull RuleSet> ruleSetNS, + Namespace<@NonNull Sort> sortNS, Namespace<@NonNull SortAlias> sortAliases, + Namespace<@NonNull RuleSet> ruleSetNS, Namespace<@NonNull ParametricSortDecl> parametricSortNS, Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS, Namespace<@NonNull Choice> choiceNS, @@ -45,6 +49,7 @@ public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, this.progVarNS = programVarNS; this.funcNS = funcNS; this.sortNS = sortNS; + this.sortAliases = sortAliases; this.ruleSetNS = ruleSetNS; this.choiceNS = choiceNS; this.parametricSortNS = parametricSortNS; @@ -53,13 +58,14 @@ public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, public NamespaceSet copy() { return new NamespaceSet(variables().copy(), functions().copy(), - sorts().copy(), + sorts().copy(), sortAliases().copy(), ruleSets().copy(), parametricSortNS.copy(), parametricFuncNS.copy(), choices().copy(), programVariables().copy()); } public NamespaceSet shallowCopy() { - return new NamespaceSet(variables(), functions(), sorts(), ruleSets(), parametricSorts(), + return new NamespaceSet(variables(), functions(), sorts(), sortAliases(), ruleSets(), + parametricSorts(), parametricFunctions(), choices(), programVariables()); @@ -68,7 +74,7 @@ public NamespaceSet shallowCopy() { // 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<>(functions()), new Namespace<>(sorts()), new Namespace<>(sortAliases()), new Namespace<>(ruleSets()), new Namespace<>(parametricSorts()), new Namespace<>(parametricFunctions()), new Namespace<>(choices()), new Namespace<>(programVariables())); @@ -114,6 +120,14 @@ public void setSorts(Namespace<@NonNull Sort> sortNS) { this.sortNS = sortNS; } + public Namespace<@NonNull SortAlias> sortAliases() { + return sortAliases; + } + + public void setSortAliases(Namespace<@NonNull SortAlias> sortAliases) { + this.sortAliases = sortAliases; + } + public Namespace<@NonNull ParametricSortDecl> parametricSorts() { return parametricSortNS; } @@ -143,6 +157,9 @@ public void add(NamespaceSet ns) { variables().add(ns.variables()); programVariables().add(ns.programVariables()); sorts().add(ns.sorts()); + sortAliases().add(ns.sortAliases()); + parametricFunctions().add(ns.parametricFunctions()); + parametricSorts().add(ns.parametricSorts()); ruleSets().add(ns.ruleSets()); functions().add(ns.functions()); choices().add(ns.choices()); @@ -161,7 +178,7 @@ private Namespace[] asArray() { * namespaces without variables, choices and ruleSets) */ private Namespace[] logicAsArray() { - return new Namespace[] { programVariables(), sorts(), functions() }; + return new Namespace[] { programVariables(), sorts(), sortAliases(), functions() }; } /** @@ -203,10 +220,25 @@ private Named lookup(Name name, final Namespace[] spaces) { return null; } + public @Nullable Sort lookupSortOrAlias(String name) { + return lookupSortOrAlias(new Name(name)); + } + + public @Nullable Sort lookupSortOrAlias(Name name) { + var sort = sorts().lookup(name); + if (sort != null) + return sort; + SortAlias alias = sortAliases.lookup(name); + if (alias != null) + return alias.aliasedSort(); + return null; + } @Override public String toString() { - return "Sorts: " + sorts() + "\n" + "Functions: " + functions() + "\n" + "Variables: " + return "Sorts: " + sorts() + "\n" + "Alias sorts: " + sortAliases() + "\n" + + "Parametric sorts: " + parametricSorts() + "\n" + "Functions: " + functions() + "\n" + + "Parametric functions: " + parametricFunctions() + "\n" + "Variables: " + variables() + "\n" + "ProgramVariables: " + programVariables() + "\n" + "Heuristics: " + ruleSets() + "\n" + "Taclet Options: " + choices() + "\n"; } @@ -225,26 +257,33 @@ public void seal() { varNS.seal(); progVarNS.seal(); funcNS.seal(); + parametricFuncNS.seal(); ruleSetNS.seal(); sortNS.seal(); + sortAliases.seal(); + parametricSortNS.seal(); choiceNS.seal(); } public boolean isEmpty() { return varNS.isEmpty() && programVariables().isEmpty() && funcNS.isEmpty() - && ruleSetNS.isEmpty() && sortNS.isEmpty() && choiceNS.isEmpty(); + && parametricFuncNS.isEmpty() + && ruleSetNS.isEmpty() && sortNS.isEmpty() && sortAliases.isEmpty() + && parametricSortNS.isEmpty() && choiceNS.isEmpty(); } // create a namespace public NamespaceSet simplify() { return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(), + sortAliases.simplify(), ruleSetNS.simplify(), parametricSortNS.simplify(), parametricFuncNS.simplify(), choiceNS.simplify(), progVarNS.simplify()); } public NamespaceSet getCompression() { return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(), + sortAliases.compress(), ruleSetNS.compress(), parametricSortNS.compress(), parametricFuncNS.compress(), choiceNS.compress(), progVarNS.compress()); } @@ -257,6 +296,7 @@ public void flushToParent() { public NamespaceSet getParent() { return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(), + sortAliases.parent(), ruleSetNS.parent(), parametricSortNS.parent(), parametricFuncNS.parent(), choiceNS.parent(), progVarNS.parent()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortAlias.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortAlias.java new file mode 100644 index 00000000000..f5f72d2b235 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortAlias.java @@ -0,0 +1,16 @@ +/* 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 org.key_project.logic.Name; +import org.key_project.logic.Named; +import org.key_project.logic.sort.Sort; + +/// An alias for a sort, allowing for more ergonomic usage of parametric sorts. E.g., `LocSet` may +/// be defined in the future as `\alias LocSet = Set<[Tuple2<[Object, Field]>]>`. +/// These aliases are managed by the Services, where sort lookup takes them into account and +/// directly resolves to the aliased sort. +/// Hence, aliases are syntactic sugar in KeY files and are not directly part of the logic. +public record SortAlias(Name name, Sort aliasedSort) implements Named { +} 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 156f6be9a51..8f53ee298f1 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 @@ -159,6 +159,22 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { ImmutableSet ext = sortExt == null ? ImmutableSet.empty() : Immutables.createSetFrom(sortExt); + if (ctx.ALIAS() != null) { + String aliasId = accept(ctx.simple_ident_dots()); + assert aliasId != null; + Name name = new Name(aliasId); + if (namespaces().sorts().lookup(name) != null) { + semanticError(ctx, "A sort of name %s already exists", name); + } + if (namespaces().sortAliases().lookup(name) != null) { + semanticError(ctx, "A sort alias of name %s already exists", name); + } + Sort aliased = accept(ctx.sortId()); + var alias = new SortAlias(name, aliased); + namespaces().sortAliases().addSafely(alias); + return alias; + } + if (ctx.sortIds != null) { for (var idCtx : ctx.sortIds.simple_ident_dots()) { String sortId = accept(idCtx); 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 216d8c6528e..57227b7a310 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 @@ -236,6 +236,13 @@ protected Sort lookupSort(String name) { result = sorts().lookup(new Name("java.lang." + name)); } } + // Look for alias + if (result == null) { + SortAlias alias = namespaces().sortAliases().lookup(name); + if (alias != null) { + result = alias.aliasedSort(); + } + } return result; } 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 67dd48204e6..4139471cfcd 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 @@ -12,6 +12,7 @@ import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; import de.uka.ilkd.key.logic.sort.ParametricSortDecl; +import de.uka.ilkd.key.logic.sort.SortAlias; import de.uka.ilkd.key.nparser.KeyIO; import de.uka.ilkd.key.pp.AbbrevMap; @@ -48,11 +49,12 @@ public final class DefaultTermParser { public JTerm parse(Reader in, Sort sort, Services services, Namespace<@NonNull QuantifiableVariable> var_ns, Namespace<@NonNull Function> func_ns, - Namespace<@NonNull Sort> sort_ns, Namespace<@NonNull ParametricSortDecl> paraSort_ns, + Namespace<@NonNull Sort> sort_ns, Namespace<@NonNull SortAlias> sortAlias_ns, + Namespace<@NonNull ParametricSortDecl> paraSort_ns, Namespace<@NonNull ParametricFunctionDecl> paraFunc_ns, Namespace<@NonNull IProgramVariable> 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, sortAlias_ns, new Namespace<>(), paraSort_ns, paraFunc_ns, new Namespace<>(), progVar_ns), scm); } 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 cf88552c6b1..e847c660ec4 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 @@ -964,7 +964,7 @@ public static JTerm 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().sortAliases(), proof.getNamespaces().parametricSorts(), proof.getNamespaces().parametricFunctions(), progVarNS, new AbbrevMap()); @@ -1006,7 +1006,7 @@ public static TacletApp parseSV1(TacletApp app, VariableSV sv, String value, sort = app.getRealSort(sv, services); } else { name = value.substring(0, colon); - sort = services.getNamespaces().sorts().lookup(value.substring(colon + 1)); + sort = services.getNamespaces().lookupSortOrAlias(value.substring(colon + 1)); } LogicVariable lv = new LogicVariable(new Name(name), sort); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java index 848559a302e..ad91a17dca5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java @@ -281,7 +281,7 @@ public JTerm toTerm(String string, @Nullable Sort sort) public Sort toSort(String sortName) throws ScriptException { return (getFirstOpenAutomaticGoal() == null ? getProof().getServices().getNamespaces() - : getFirstOpenAutomaticGoal().getLocalNamespaces()).sorts().lookup(sortName); + : getFirstOpenAutomaticGoal().getLocalNamespaces()).lookupSortOrAlias(sortName); } public Sequent toSequent(String sequent) throws ParserException, ScriptException { diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java new file mode 100644 index 00000000000..cfc0f926e20 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java @@ -0,0 +1,68 @@ +/* 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 de.uka.ilkd.key.java.Recoder2KeY; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.GenericParameter; +import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.nparser.NamespaceBuilder; +import de.uka.ilkd.key.proof.init.AbstractProfile; + +import org.key_project.logic.Name; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSet; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +public class TestAlias { + private NamespaceSet nss; + private Services services; + + @BeforeEach + public void setUp() { + this.services = new Services(AbstractProfile.getDefaultProfile()); + this.nss = services.getNamespaces(); + + 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 SortAlias addAlias(String name, String aliased) { + var aliasedSort = nss.sorts().lookup(aliased); + assert aliasedSort != null; + var alias = new SortAlias(new Name(name), aliasedSort); + nss.sortAliases().add(alias); + return alias; + } + + @Test + public void testSimpleAlias() { + var alias = addAlias("myInt", "int"); + assertEquals(alias.aliasedSort(), nss.lookupSortOrAlias("myInt")); + } + + @Test + public void testAliasOfParametric() { + var pSet = new ParametricSortDecl(new Name("PSet"), false, ImmutableSet.empty(), + ImmutableList.of( + new GenericParameter(new GenericSort(new Name("A")), + GenericParameter.Variance.INVARIANT)), + "", ""); + nss.parametricSorts().add(pSet); + ParametricSortInstance intSet = ParametricSortInstance.get(pSet, + ImmutableList.of(new GenericArgument(nss.lookupSortOrAlias("int"))), services); + var alias = new SortAlias(new Name("IntSet"), intSet); + nss.sortAliases().add(alias); + assertEquals(intSet, nss.lookupSortOrAlias("IntSet")); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/AliasTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/AliasTest.java new file mode 100644 index 00000000000..0a540a59bda --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/AliasTest.java @@ -0,0 +1,32 @@ +/* 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.nparser; + +import java.nio.file.Paths; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; + +import org.key_project.util.collection.ImmutableList; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; + +public class AliasTest { + @Test + public void intSeqTest() throws ProblemLoaderException { + var path = Paths.get("../key.ui/examples/standard_key/polymorphic/pseq.key"); + var env = KeYEnvironment.load(path); + + var pSeq = env.getInitConfig().namespaces().parametricSorts().lookup("PSeq"); + var intSeq = ParametricSortInstance.get(pSeq, + ImmutableList.of( + new GenericArgument(env.getInitConfig().namespaces().lookupSortOrAlias("int"))), + env.getServices()); + Assertions.assertEquals(intSeq, + env.getInitConfig().namespaces().lookupSortOrAlias("IntSeq")); + } +} 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 ee6d03869b2..1040bbab8f1 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 @@ -194,15 +194,17 @@ public void setUp() { proof.setRoot(g.node()); proof.add(g); - proof.setNamespaces(new NamespaceSet(variables, functions, sorts, new Namespace<>(), - new Namespace<>(), new Namespace<>(), - new Namespace<>(), new Namespace<>())); + proof.setNamespaces( + new NamespaceSet(variables, functions, sorts, new Namespace<>(), new Namespace<>(), + new Namespace<>(), new Namespace<>(), + new Namespace<>(), new Namespace<>())); } private JTerm parseTerm(String termstr) { return TacletForTests.parseTerm(termstr, new NamespaceSet(variables, functions, sorts, new Namespace<>(), new Namespace<>(), + new Namespace<>(), new Namespace<>(), new Namespace<>(), new Namespace<>())); } diff --git a/key.ui/examples/standard_key/polymorphic/pseq.key b/key.ui/examples/standard_key/polymorphic/pseq.key index 7d32a4de6b8..bd2eb734310 100644 --- a/key.ui/examples/standard_key/polymorphic/pseq.key +++ b/key.ui/examples/standard_key/polymorphic/pseq.key @@ -1,6 +1,8 @@ \sorts { \generic E; PSeq<[E]>; + + \alias IntSeq = PSeq<[int]>; } \functions { @@ -30,9 +32,9 @@ \rules { \lemma pseqConcatWithPSeqEmpty1 { - \schemaVar \term Seq seq; + \schemaVar \term PSeq<[E]> seq; - \find(seqConcat(seq, seqEmpty)) + \find(pseqConcat<[E]>(seq, pseqEmpty<[E]>)) \replacewith(seq) @@ -69,6 +71,14 @@ \heuristics(concrete) }; + subIntSeqEmpty { + \schemaVar \term IntSeq seq; + \schemaVar \term int i; + \find(pseqSub<[int]>(seq, i, i)) + \replacewith(pseqEmpty<[int]>) + \heuristics(concrete) + }; + \lemma subPSeqComplete { \schemaVar \term PSeq<[E]> seq;