From f6b9328f735aec0c8eecc0614909df79887c1395 Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 4 Aug 2025 11:07:02 +0200 Subject: [PATCH 01/13] Start on polymorphic sorts and functions --- key.core/src/main/antlr4/KeYLexer.g4 | 2 + key.core/src/main/antlr4/KeYLexer.tokens | 388 ++++++++++++++++++ key.core/src/main/antlr4/KeYParser.g4 | 31 +- .../uka/ilkd/key/logic/GenericArgument.java | 40 ++ .../uka/ilkd/key/logic/GenericParameter.java | 19 + .../de/uka/ilkd/key/logic/NamespaceSet.java | 43 +- .../key/logic/op/ParametricFunctionDecl.java | 75 ++++ .../logic/op/ParametricFunctionInstance.java | 119 ++++++ .../key/logic/sort/ParametricSortDecl.java | 63 +++ .../logic/sort/ParametricSortInstance.java | 204 +++++++++ .../nparser/builder/DeclarationBuilder.java | 163 +++++--- .../key/nparser/builder/DefaultBuilder.java | 44 +- .../nparser/builder/ExpressionBuilder.java | 12 +- .../key/nparser/builder/TacletPBuilder.java | 7 +- .../ilkd/key/parser/DefaultTermParser.java | 13 +- .../proof/io/IntermediateProofReplayer.java | 2 + .../key/rule/SyntacticalReplaceVisitor.java | 18 +- .../key/rule/conditions/TypeResolver.java | 29 ++ .../key/rule/inst/GenericSortCondition.java | 46 ++- .../rule/inst/GenericSortInstantiations.java | 21 +- .../SyntaxElementMatchProgramGenerator.java | 84 ++-- .../JavaDLMatchVMInstructionSet.java | 5 + .../SimilarParametricFunctionInstruction.java | 30 ++ .../quantifierHeuristics/TestTriggersSet.java | 6 +- .../key_project/util/java/CollectionUtil.java | 12 + 25 files changed, 1357 insertions(+), 119 deletions(-) create mode 100644 key.core/src/main/antlr4/KeYLexer.tokens create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/SimilarParametricFunctionInstruction.java diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 544c9371a42..37e4ecaff27 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -381,6 +381,8 @@ GREATEREQUAL : '>' '=' | '\u2265' ; +OPENTYPEPARAMS : '<['; +CLOSETYPEPARAMS : ']>'; WS: [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ; diff --git a/key.core/src/main/antlr4/KeYLexer.tokens b/key.core/src/main/antlr4/KeYLexer.tokens new file mode 100644 index 00000000000..45228a531f6 --- /dev/null +++ b/key.core/src/main/antlr4/KeYLexer.tokens @@ -0,0 +1,388 @@ +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 6c262484c93..921243124ae 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -94,10 +94,16 @@ 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 ) ; +parametric_sort_decl +: + simple_ident_dots + formal_sort_param_decls +; + simple_ident_dots : simple_ident (DOT simple_ident)* @@ -243,7 +249,7 @@ datatype_decl: doc=DOC_COMMENT? // weigl: all datatypes are free! // FREE? - name=simple_ident + name=simple_ident formal_sort_param_decls? EQUALS datatype_constructor (OR datatype_constructor)* SEMI @@ -260,6 +266,17 @@ datatype_constructor: )? ; +formal_sort_param_decls +: OPENTYPEPARAMS + formal_sort_param_decl (COMMA formal_sort_param_decl)* + CLOSETYPEPARAMS +; + +formal_sort_param_decl +: + (PLUS | MINUS)? simple_ident +; + func_decls : FUNCTIONS @@ -326,7 +343,14 @@ ruleset_decls sortId : - id=simple_ident_dots (EMPTYBRACKETS)* + id=simple_ident_dots formal_sort_args? (EMPTYBRACKETS)* +; + +formal_sort_args +: + OPENTYPEPARAMS + sortId (COMMA sortId)* + CLOSETYPEPARAMS ; id_declaration @@ -480,6 +504,7 @@ accessterm // OLD (sortId DOUBLECOLON)? firstName=simple_ident + formal_sort_args? /*Faster version simple_ident_dots diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java new file mode 100644 index 00000000000..8973db36d72 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java @@ -0,0 +1,40 @@ +/* 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; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.TerminalSyntaxElement; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; + +import org.jspecify.annotations.NonNull; + +public record GenericArgument(Sort sort) implements TerminalSyntaxElement { + @Override + public @NonNull String toString() { + return sort.toString(); + } + + public GenericArgument instantiate(SVInstantiations svInst, Services services) { + if (sort instanceof GenericSort gs) { + return new GenericArgument( + svInst.getGenericSortInstantiations().getRealSort(gs, services)); + } else if (sort instanceof ParametricSortInstance psi) { + ImmutableList args = ImmutableSLList.nil(); + + for (int i = psi.getArgs().size() - 1; i >= 0; i--) { + args = args.prepend(psi.getArgs().get(i).instantiate(svInst, services)); + } + + return new GenericArgument(ParametricSortInstance.get(psi.getBase(), args)); + } else { + return this; + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java new file mode 100644 index 00000000000..45ead7cc045 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java @@ -0,0 +1,19 @@ +/* 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; + +import de.uka.ilkd.key.logic.sort.GenericSort; + +import org.jspecify.annotations.NonNull; + +public record GenericParameter(GenericSort sort, Variance variance) { + @Override + public @NonNull String toString() { + return sort.toString(); + } + + public enum Variance { + COVARIANT, CONTRAVARIANT, INVARIANT + } +} 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 e87be8f8072..47221e72b27 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 @@ -5,6 +5,8 @@ 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 org.key_project.logic.Choice; import org.key_project.logic.Name; @@ -25,6 +27,8 @@ 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 ParametricSortDecl> parametricSortNS = new Namespace<>(); + private Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS = new Namespace<>(); private Namespace<@NonNull Choice> choiceNS = new Namespace<>(); public NamespaceSet() { @@ -33,6 +37,8 @@ public NamespaceSet() { public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, Namespace<@NonNull Function> funcNS, Namespace<@NonNull Sort> sortNS, Namespace<@NonNull RuleSet> ruleSetNS, + Namespace<@NonNull ParametricSortDecl> parametricSortNS, + Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS, Namespace<@NonNull Choice> choiceNS, Namespace<@NonNull IProgramVariable> programVarNS) { this.varNS = varNS; @@ -41,16 +47,20 @@ public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, this.sortNS = sortNS; this.ruleSetNS = ruleSetNS; this.choiceNS = choiceNS; + this.parametricSortNS = parametricSortNS; + this.parametricFuncNS = parametricFuncNS; } public NamespaceSet copy() { return new NamespaceSet(variables().copy(), functions().copy(), sorts().copy(), - ruleSets().copy(), choices().copy(), programVariables().copy()); + ruleSets().copy(), parametricSortNS.copy(), parametricFuncNS.copy(), choices().copy(), + programVariables().copy()); } public NamespaceSet shallowCopy() { - return new NamespaceSet(variables(), functions(), sorts(), ruleSets(), + return new NamespaceSet(variables(), functions(), sorts(), ruleSets(), parametricSorts(), + parametricFunctions(), choices(), programVariables()); } @@ -59,7 +69,8 @@ public NamespaceSet shallowCopy() { public NamespaceSet copyWithParent() { return new NamespaceSet(new Namespace<>(variables()), new Namespace<>(functions()), new Namespace<>(sorts()), - new Namespace<>(ruleSets()), new Namespace<>(choices()), + new Namespace<>(ruleSets()), new Namespace<>(parametricSorts()), + new Namespace<>(parametricFunctions()), new Namespace<>(choices()), new Namespace<>(programVariables())); } @@ -103,6 +114,23 @@ public void setSorts(Namespace<@NonNull Sort> sortNS) { this.sortNS = sortNS; } + public Namespace<@NonNull ParametricSortDecl> parametricSorts() { + return parametricSortNS; + } + + public void setParametricSorts(Namespace<@NonNull ParametricSortDecl> parametricSortNS) { + this.parametricSortNS = parametricSortNS; + } + + public Namespace<@NonNull ParametricFunctionDecl> parametricFunctions() { + return parametricFuncNS; + } + + public void setParametricFunctions( + Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS) { + this.parametricFuncNS = parametricFuncNS; + } + public Namespace<@NonNull Choice> choices() { return choiceNS; } @@ -211,12 +239,14 @@ public boolean isEmpty() { // create a namespace public NamespaceSet simplify() { return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(), - ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify()); + ruleSetNS.simplify(), parametricSortNS.simplify(), parametricFuncNS.simplify(), + choiceNS.simplify(), progVarNS.simplify()); } public NamespaceSet getCompression() { return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(), - ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress()); + ruleSetNS.compress(), parametricSortNS.compress(), parametricFuncNS.compress(), + choiceNS.compress(), progVarNS.compress()); } public void flushToParent() { @@ -227,7 +257,8 @@ public void flushToParent() { public NamespaceSet getParent() { return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(), - ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent()); + ruleSetNS.parent(), parametricSortNS.parent(), parametricFuncNS.parent(), + choiceNS.parent(), progVarNS.parent()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java new file mode 100644 index 00000000000..5d757411915 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java @@ -0,0 +1,75 @@ +/* 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.op; + +import de.uka.ilkd.key.logic.GenericParameter; + +import org.key_project.logic.Name; +import org.key_project.logic.Named; +import org.key_project.logic.Sorted; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +public final class ParametricFunctionDecl implements Named, Sorted { + private final Name name; + private final ImmutableList parameters; + private final ImmutableArray argSorts; + private final Sort sort; + private final @Nullable ImmutableArray whereToBind; + private final boolean unique; + private final boolean isRigid; + private final boolean isSkolemConstant; + + public ParametricFunctionDecl(Name name, ImmutableList parameters, + ImmutableArray argSorts, Sort sort, + @Nullable ImmutableArray whereToBind, boolean unique, boolean isRigid, + boolean isSkolemConstant) { + this.name = name; + this.parameters = parameters; + this.argSorts = argSorts; + this.sort = sort; + this.whereToBind = whereToBind; + this.unique = unique; + this.isRigid = isRigid; + this.isSkolemConstant = isSkolemConstant; + } + + @Override + public @NonNull Sort sort() { + return sort; + } + + public ImmutableArray argSorts() { + return argSorts; + } + + public @Nullable ImmutableArray getWhereToBind() { + return whereToBind; + } + + public boolean isUnique() { + return unique; + } + + public boolean isRigid() { + return isRigid; + } + + public boolean isSkolemConstant() { + return isSkolemConstant; + } + + public ImmutableList getParameters() { + return parameters; + } + + @Override + public @NonNull Name name() { + return name; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java new file mode 100644 index 00000000000..de271d4a4e6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java @@ -0,0 +1,119 @@ +/* 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.op; + +import java.util.HashMap; +import java.util.Map; +import java.util.Objects; +import java.util.WeakHashMap; + +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; + +import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; + +import org.jspecify.annotations.NonNull; + +public class ParametricFunctionInstance extends JFunction { + private static final Map CACHE = + new WeakHashMap<>(); + + private final ImmutableList args; + private final ParametricFunctionDecl base; + + public static ParametricFunctionInstance get(ParametricFunctionDecl decl, + ImmutableList args) { + assert args.size() == decl.getParameters().size(); + var instMap = getInstMap(decl, args); + var argSorts = instantiate(decl, instMap); + var sort = instantiate(decl.sort(), instMap); + var fn = new ParametricFunctionInstance(decl, args, argSorts, sort); + var cached = CACHE.get(fn); + if (cached != null) { + return cached; + } + CACHE.put(fn, fn); + return fn; + } + + private ParametricFunctionInstance(ParametricFunctionDecl base, + ImmutableList args, ImmutableArray argSorts, Sort sort) { + super(makeName(base, args), sort, argSorts, base.getWhereToBind(), base.isUnique(), + base.isRigid(), + base.isSkolemConstant()); + this.base = base; + this.args = args; + } + + public ParametricFunctionDecl getBase() { + return base; + } + + public ImmutableList getArgs() { + return args; + } + + private static Name makeName(ParametricFunctionDecl base, + ImmutableList parameters) { + // The [ ] are produced by the list's toString method. + return new Name(base.name() + "<" + parameters + ">"); + } + + private static ImmutableArray instantiate(ParametricFunctionDecl base, + Map instMap) { + var baseArgSorts = base.argSorts(); + var argSorts = new Sort[baseArgSorts.size()]; + + for (int i = 0; i < baseArgSorts.size(); i++) { + var sort = baseArgSorts.get(i); + argSorts[i] = instantiate(sort, instMap); + } + + return new ImmutableArray<>(argSorts); + } + + private static Map getInstMap(ParametricFunctionDecl base, + ImmutableList args) { + var map = new HashMap(); + for (int i = 0; i < base.getParameters().size(); i++) { + var param = base.getParameters().get(i); + var arg = args.get(i); + map.put(param.sort(), arg); + } + return map; + } + + public static Sort instantiate(Sort sort, Map map) { + if (sort instanceof GenericSort gs) { + var arg = map.get(gs); + return arg == null ? gs : arg.sort(); + } else if (sort instanceof ParametricSortInstance psi) { + var base = psi.getBase(); + ImmutableList args = ImmutableSLList.nil(); + for (int i = psi.getArgs().size() - 1; i >= 0; i--) { + var psiArg = psi.getArgs().get(i); + args = args.prepend(new GenericArgument(instantiate(psiArg.sort(), map))); + } + return ParametricSortInstance.get(base, args); + } else { + return sort; + } + } + + @Override + public int getChildCount() { + return args.size(); + } + + @Override + public @NonNull SyntaxElement getChild(int n) { + return Objects.requireNonNull(args.get(n)); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java new file mode 100644 index 00000000000..41ec63662a7 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java @@ -0,0 +1,63 @@ +/* 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.ldt.JavaDLTheory; +import de.uka.ilkd.key.logic.GenericParameter; + +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; + +import org.jspecify.annotations.NonNull; + +public class ParametricSortDecl implements Named { + private final Name name; + private final boolean isAbstract; + private final String documentation; + + private final ImmutableList parameters; + private final ImmutableSet extendedSorts; + private final String origin; + + public ParametricSortDecl(Name name, boolean isAbstract, ImmutableSet ext, + ImmutableList sortParams, String documentation, String origin) { + this.name = name; + this.isAbstract = isAbstract; + this.extendedSorts = ext.isEmpty() ? ImmutableSet.singleton(JavaDLTheory.ANY) : ext; + this.documentation = documentation; + this.parameters = sortParams; + this.origin = origin; + assert Immutables.isDuplicateFree(parameters) + : "The caller should have made sure that generic sorts are not duplicated"; + } + + public ImmutableList getParameters() { + return parameters; + } + + @Override + public @NonNull Name name() { + return name; + } + + public boolean isAbstract() { + return isAbstract; + } + + public ImmutableSet getExtendedSorts() { + return extendedSorts; + } + + 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..49253e0319c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java @@ -0,0 +1,204 @@ +/* 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.HashMap; +import java.util.Map; +import java.util.Objects; +import java.util.WeakHashMap; + +import de.uka.ilkd.key.ldt.JavaDLTheory; +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.GenericParameter; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +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.ImmutableSLList; +import org.key_project.util.collection.ImmutableSet; + +import org.jspecify.annotations.NonNull; + +public final class ParametricSortInstance extends AbstractSort { + private static final Map CACHE = + new WeakHashMap<>(); + + private final ImmutableList args; + private final ParametricSortDecl base; + private final ImmutableSet extendsSorts; + + public static ParametricSortInstance get(ParametricSortDecl base, + ImmutableList args) { + assert args.size() == base.getParameters().size(); + ParametricSortInstance sort = + new ParametricSortInstance(base, args); + ParametricSortInstance cached = CACHE.get(sort); + if (cached != null) { + return cached; + } else { + CACHE.put(sort, sort); + return sort; + } + } + + /// This must only be called in [ParametricSortInstance#get], which ensures that the cache is + /// used. + private ParametricSortInstance(ParametricSortDecl base, ImmutableList args) { + super(makeName(base, args), base.isAbstract()); + + this.extendsSorts = ImmutableSet.singleton(JavaDLTheory.ANY); + this.base = base; + this.args = args; + } + + private static Name makeName(ParametricSortDecl base, + ImmutableList parameters) { + // The [ ] are produced by the list's toString method. + return new Name(base.name() + "<" + parameters + ">"); + } + + private static ImmutableSet computeExt(ParametricSortDecl base, + ImmutableList args) { + ImmutableSet result = DefaultImmutableSet.nil(); + + // 1. extensions by base sort + ImmutableSet baseExt = base.getExtendedSorts(); + if (!baseExt.isEmpty()) { + for (Sort s : baseExt) { + result = + result.add(ParametricFunctionInstance.instantiate(s, getInstMap(base, args))); + } + } + + // 2. extensions by variances + ImmutableList cov = base.getParameters(); + int number = 0; + for (GenericParameter 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 = args.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; + } + + public ParametricSortDecl getBase() { + return base; + } + + public ImmutableList getArgs() { + return args; + } + + @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(args, that.args) && + base == that.base; + } + + @Override + public int hashCode() { + return Objects.hash(args, base); + } + + @Override + public @NonNull ImmutableSet extendsSorts() { + return extendsSorts; + } + + @Override + public boolean extendsTrans(@NonNull Sort sort) { + return sort == this || extendsSorts() + .exists((Sort superSort) -> superSort == sort || superSort.extendsTrans(sort)); + } + + private static Map getInstMap(ParametricSortDecl base, + ImmutableList args) { + var map = new HashMap(); + for (int i = 0; i < base.getParameters().size(); i++) { + var param = base.getParameters().get(i); + var arg = args.get(i); + map.put(param.sort(), arg); + } + return map; + } + + 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 = + args.map(s -> new GenericArgument(instantiate(template, instantiation, s.sort()))); + return get(base, newParameters); + } + + public boolean isComplete(SVInstantiations instMap) { + for (GenericArgument arg : args) { + var sort = arg.sort(); + if (sort instanceof ParametricSortInstance psi) { + if (!psi.isComplete(instMap)) + return false; + } else if (sort instanceof GenericSort gs) { + if (instMap.getGenericSortInstantiations().getInstantiation(gs) == null) + return false; + } + } + return true; + } + + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, + SVInstantiations instMap) { + ImmutableList newArgs = ImmutableSLList.nil(); + for (int i = args.size() - 1; i >= 0; i--) { + GenericArgument arg = args.get(i); + var sort = arg.sort(); + if (sort instanceof ParametricSortInstance psi) { + newArgs = + newArgs.prepend( + new GenericArgument(psi.resolveSort(sv, instCandidate, instMap))); + } else if (sort instanceof GenericSort gs) { + newArgs = newArgs.prepend( + new GenericArgument( + instMap.getGenericSortInstantiations().getInstantiation(gs))); + } else { + newArgs = newArgs.prepend(arg); + } + } + return get(base, newArgs); + } +} 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 30d94ea933c..69b05b8f37d 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; @@ -23,10 +20,13 @@ import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleSet; +import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; import org.key_project.util.collection.Immutables; +import org.key_project.util.java.CollectionUtil; import org.antlr.v4.runtime.Token; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -70,8 +70,21 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { ? 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); + List typeParameters = accept(ctx.formal_sort_param_decls()); + if (typeParameters == null) { + var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); + sorts().addSafely(s); + } else { + var doubled = CollectionUtil.findDuplicates(typeParameters); + if (!doubled.isEmpty()) { + semanticError(ctx.formal_sort_param_decls(), + "Type parameters must be unique within a declaration. Found duplicate: %s", + doubled.getFirst()); + } + var s = new ParametricSortDecl(new Name(name), false, ImmutableSet.empty(), + ImmutableList.fromList(typeParameters), doc, origin); + namespaces().parametricSorts().addSafely(s); + } return null; } @@ -143,55 +156,111 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { boolean isAbstractSort = ctx.ABSTRACT() != null; List createdSorts = new LinkedList<>(); 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; + + ImmutableSet ext = sortExt == null ? ImmutableSet.empty() + : Immutables.createSetFrom(sortExt); + + if (ctx.sortIds != null) { + for (var idCtx : ctx.sortIds.simple_ident_dots()) { + String sortId = accept(idCtx); + Name sortName = new Name(sortId); + + + 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 { - var si = new SortImpl(sortName, ext, isAbstractSort, - documentation, BuilderHelpers.getPosition(idCtx)); - s = si; + if (isProxySort) { + var ps = new ProxySort(sortName, ext, documentation, + BuilderHelpers.getPosition(idCtx)); + s = ps; + } else { + var si = new SortImpl(sortName, ext, isAbstractSort, + documentation, BuilderHelpers.getPosition(idCtx)); + s = si; + } } + 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()); } + } else { + // parametric sort + var declCtx = ctx.parametric_sort_decl(); + assert declCtx != null : "One of the two must be present"; + List typeParams = + visitFormal_sort_param_decls(declCtx.formal_sort_param_decls()); + ImmutableList params = ImmutableList.fromList(typeParams); + var doubled = CollectionUtil.findDuplicates(params.map(GenericParameter::sort)); + 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 ParametricSortDecl(sortName, isAbstractSort, ext, params, + documentation, BuilderHelpers.getPosition(declCtx)); + namespaces().parametricSorts().add(sortDecl); } return createdSorts; } + @Override + public @Nullable List visitFormal_sort_param_decls( + KeYParser.Formal_sort_param_declsContext ctx) { + return mapOf(ctx.formal_sort_param_decl()); + } + + @Override + public @Nullable GenericParameter visitFormal_sort_param_decl( + KeYParser.Formal_sort_param_declContext ctx) { + + GenericParameter.Variance variance; + if (ctx.PLUS() != null) { + variance = GenericParameter.Variance.COVARIANT; + } else if (ctx.MINUS() != null) { + variance = GenericParameter.Variance.CONTRAVARIANT; + } else { + variance = GenericParameter.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 GenericParameter((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 059f24f1696..7bc7dcdb919 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 @@ -20,6 +20,8 @@ import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.ArraySort; import de.uka.ilkd.key.logic.sort.NullSort; +import de.uka.ilkd.key.logic.sort.ParametricSortDecl; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.nparser.KeYParser; import org.key_project.logic.*; @@ -30,6 +32,8 @@ import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleSet; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.Pair; import org.antlr.v4.runtime.ParserRuleContext; @@ -141,10 +145,10 @@ public Sort visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_help * @param varfuncName the String with the symbols name */ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, String sortName, - Sort sort) { + Sort sort, KeYParser.Formal_sort_argsContext genericArgsCtxt) { Name name = new Name(varfuncName); Operator[] operators = - { (JOperatorSV) schemaVariables().lookup(name), variables().lookup(name), + { schemaVariables().lookup(name), variables().lookup(name), programVariables().lookup(new ProgramElementName(varfuncName)), functions().lookup(name), AbstractTermTransformer.name2metaop(varfuncName), @@ -161,7 +165,7 @@ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, St Name fqName = new Name((sort != null ? sort.toString() : sortName) + "::" + varfuncName); operators = - new Operator[] { (JOperatorSV) schemaVariables().lookup(fqName), + new Operator[] { schemaVariables().lookup(fqName), variables().lookup(fqName), programVariables().lookup(new ProgramElementName(fqName.toString())), functions().lookup(fqName), @@ -184,6 +188,15 @@ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, St } } } + if (genericArgsCtxt != null) { + var d = nss.parametricFunctions().lookup(name); + if (d == null) { + semanticError(ctx, "Could not find parametric function: %s", name); + return null; + } + var args = getGenericArgs(genericArgsCtxt, d.getParameters()); + return ParametricFunctionInstance.get(d, args); + } semanticError(ctx, "Could not find (program) variable or constant %s", varfuncName); return null; } @@ -323,6 +336,16 @@ public List visitArg_sorts(KeYParser.Arg_sortsContext ctx) { @Override public Sort visitSortId(KeYParser.SortIdContext ctx) { String primitiveName = ctx.id.getText(); + if (ctx.formal_sort_args() != null) { + // parametric sorts should be instantiated + ParametricSortDecl sortDecl = nss.parametricSorts().lookup(primitiveName); + if (sortDecl == null) { + semanticError(ctx, "Could not find polymorphic sort: %s", primitiveName); + } + ImmutableList params = + getGenericArgs(ctx.formal_sort_args(), sortDecl.getParameters()); + return ParametricSortInstance.get(sortDecl, params); + } // Special handling for byte, char, short, long: // these are *not* sorts, but they are nevertheless valid // prefixes for array sorts such as byte[], char[][][]. @@ -360,6 +383,21 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) { return s; } + private ImmutableList getGenericArgs(KeYParser.Formal_sort_argsContext ctx, + ImmutableList params) { + if (ctx.sortId().size() != params.size()) { + semanticError(ctx, "Expected %d sort arguments, got only %d", + params.size(), ctx.sortId().size()); + } + ImmutableList args = ImmutableSLList.nil(); + for (int i = params.size() - 1; i >= 0; i--) { + var arg = ctx.sortId(i); + var sort = visitSortId(arg); + args = args.prepend(new GenericArgument(sort)); + } + return args; + } + @Override public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { boolean array = false; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index d4d4c6dcc57..3eb0281837d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -1219,7 +1219,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { if (varfuncid.endsWith(LIMIT_SUFFIX)) { varfuncid = varfuncid.substring(0, varfuncid.length() - 5); op = lookupVarfuncId(ctx, varfuncid, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId, null); if (ObserverFunction.class.isAssignableFrom(op.getClass())) { op = getServices().getSpecificationRepository() .limitObs((ObserverFunction) op).first; @@ -1231,7 +1231,7 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { ctx.name == null ? ctx.INT_LITERAL().getText() : ctx.name.simple_ident(0).getText(); op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId, null); if (op instanceof ProgramVariable v && ctx.name.simple_ident().size() > 1) { List otherParts = ctx.name.simple_ident().subList(1, ctx.name.simple_ident().size()); @@ -1470,6 +1470,10 @@ public JTerm visitAccessterm(KeYParser.AccesstermContext ctx) { ImmutableArray boundVars = null; Namespace orig = null; + KeYParser.Formal_sort_argsContext genericArgsCtxt = null; + if (ctx.formal_sort_args() != null) { + genericArgsCtxt = ctx.formal_sort_args(); + } JTerm[] args = null; if (ctx.call() != null) { orig = variables(); @@ -1490,7 +1494,7 @@ public JTerm visitAccessterm(KeYParser.AccesstermContext ctx) { } else if (firstName.endsWith(LIMIT_SUFFIX)) { firstName = firstName.substring(0, firstName.length() - 5); op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId, null); if (ObserverFunction.class.isAssignableFrom(op.getClass())) { op = getServices().getSpecificationRepository() .limitObs((ObserverFunction) op).first; @@ -1499,7 +1503,7 @@ public JTerm visitAccessterm(KeYParser.AccesstermContext ctx) { } } else { op = lookupVarfuncId(ctx, firstName, - ctx.sortId() != null ? ctx.sortId().getText() : null, sortId); + ctx.sortId() != null ? ctx.sortId().getText() : null, sortId, genericArgsCtxt); } JTerm current; 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 a72c2a7279c..8f668d623ee 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 @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; 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 de.uka.ilkd.key.nparser.KeYParser; import de.uka.ilkd.key.nparser.varexp.ArgumentType; @@ -649,8 +650,10 @@ public Object buildTypeResolver(KeYParser.Varexp_argumentContext ctx) { Sort s = visitSortId(ctx.term().getText(), ctx.term()); if (s != null) { - if (s instanceof GenericSort) { - return TypeResolver.createGenericSortResolver((GenericSort) s); + if (s instanceof GenericSort gs) { + return TypeResolver.createGenericSortResolver(gs); + } else if (s instanceof ParametricSortInstance psi) { + return TypeResolver.createParametricSortResolver(psi); } else { return TypeResolver.createNonGenericSortResolver(s); } 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 e0b494ad19f..67dd48204e6 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 @@ -10,6 +10,8 @@ import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.NamespaceSet; 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.nparser.KeyIO; import de.uka.ilkd.key.pp.AbbrevMap; @@ -21,6 +23,7 @@ import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.RecognitionException; +import org.jspecify.annotations.NonNull; /** @@ -43,12 +46,14 @@ public final class DefaultTermParser { * correctly or the term has an invalid sort. */ public JTerm parse(Reader in, Sort sort, Services services, - Namespace var_ns, - Namespace func_ns, - Namespace sort_ns, Namespace progVar_ns, AbbrevMap scm) + Namespace<@NonNull QuantifiableVariable> var_ns, + Namespace<@NonNull Function> func_ns, + Namespace<@NonNull Sort> sort_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, - new Namespace<>(), new Namespace<>(), progVar_ns), scm); + 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 5316abdbed6..d22d7eae28a 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 @@ -962,6 +962,8 @@ public static JTerm parseTerm(String value, Proof proof, Namespace args = ImmutableSLList.nil(); + + for (int i = pfi.getArgs().size() - 1; i >= 0; i--) { + args = args.prepend(pfi.getArgs().get(i).instantiate(svInst, services)); + } + + return ParametricFunctionInstance.get(pfi.getBase(), args); + } + private JTerm resolveSubst(JTerm t) { if (t.op() instanceof SubstOp) { JTerm resolved = ((SubstOp) t.op()).apply(t, tb); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index c6ad9bba00e..d4b07282738 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.util.Debug; @@ -49,6 +50,9 @@ public static TypeResolver createNonGenericSortResolver(Sort s) { return new NonGenericSortResolver(s); } + public static TypeResolver createParametricSortResolver(ParametricSortInstance psi) { + return new ParametricSortResolver(psi); + } public abstract boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services); @@ -233,4 +237,29 @@ public String toString() { return "\\containerType(" + memberSV + ")"; } } + + private static class ParametricSortResolver extends TypeResolver { + private final ParametricSortInstance psi; + + public ParametricSortResolver(ParametricSortInstance psi) { + this.psi = psi; + } + + @Override + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, + SVInstantiations instMap, TermServices services) { + return psi.isComplete(instMap); + } + + @Override + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, + SVInstantiations instMap, Services services) { + return psi.resolveSort(sv, instCandidate, instMap); + } + + @Override + public String toString() { + return psi.toString(); + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java index cc3a36e70dc..14ec53f828d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java @@ -4,15 +4,18 @@ package de.uka.ilkd.key.rule.inst; import de.uka.ilkd.key.ldt.JavaDLTheory; -import de.uka.ilkd.key.logic.op.JOperatorSV; +import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.op.TermSV; import de.uka.ilkd.key.logic.sort.ArraySort; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.instantiation.InstantiationEntry; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; import org.jspecify.annotations.NonNull; @@ -32,7 +35,7 @@ public abstract class GenericSortCondition { * are either always compatible (no generic sorts) or never compatible (non generic * sorts that don't match) */ - public static GenericSortCondition createCondition( + public static ImmutableList createCondition( SchemaVariable sv, InstantiationEntry p_entry) { @@ -40,7 +43,7 @@ public static GenericSortCondition createCondition( return null; } - return createCondition(((JOperatorSV) sv).sort(), instantiation.sort(), + return createCondition(sv.sort(), instantiation.sort(), !subSortsAllowed(sv)); } @@ -54,16 +57,18 @@ static boolean subSortsAllowed(SchemaVariable p_sv) { } /** - * Create the condition to make a generic sort (s0) (or a collection sort of a generic sort) and + * Create the conditions to make a generic sort (s0) (or a collection sort of a generic sort) + * and * a concrete sort (s1) equal * * @param p_identity true iff an identity condition should be generated (otherwise: a supersort * condition is generated) - * @return the resulting condition, if "s0" is of generic sort; null, if the sorts are either + * @return the resulting conditions, if "s0" is of generic sort; null, if the sorts are either * always compatible (no generic sorts) or never compatible (e.g. non generic sorts that * don't match) */ - protected static GenericSortCondition createCondition(Sort s0, Sort s1, boolean p_identity) { + protected static ImmutableList createCondition(Sort s0, Sort s1, + boolean p_identity) { while (s0 instanceof ArraySort) { // Currently the sort hierarchy is not inherited by // collection sorts; therefore identity has to be ensured @@ -77,16 +82,35 @@ protected static GenericSortCondition createCondition(Sort s0, Sort s1, boolean s1 = ((ArraySort) s1).elementSort(); } - if (!(s0 instanceof GenericSort gs) || s1 == JavaDLTheory.FORMULA + if (!(s0 instanceof GenericSort || s0 instanceof ParametricSortInstance) + || s1 == JavaDLTheory.FORMULA || s1 == JavaDLTheory.UPDATE) { return null; } - if (p_identity) { - return createIdentityCondition(gs, s1); - } else { - return createSupersortCondition(gs, s1); + if (s0 instanceof GenericSort gs) { + if (p_identity) { + return ImmutableList.of(createIdentityCondition(gs, s1)); + } else { + return ImmutableList.of(createSupersortCondition(gs, s1)); + } + } + var psi = (ParametricSortInstance) s0; + if (!(s1 instanceof ParametricSortInstance ps1) || ps1.getBase() != psi.getBase()) { + return null; + } + ImmutableList conds = ImmutableSLList.nil(); + for (int i = psi.getArgs().size() - 1; i >= 0; i--) { + var a0 = psi.getArgs().get(i); + var a1 = ps1.getArgs().get(i); + if (a0 instanceof GenericArgument(Sort sort)) { + var c = createCondition(sort, a1.sort(), p_identity); + if (c != null) { + conds = conds.prepend(c); + } + } } + return conds; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java index 36ff32c323a..05d9b825e60 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java @@ -59,7 +59,7 @@ public static GenericSortInstantiations create( ImmutableList p_conditions, LogicServices services) { ImmutableList sorts = ImmutableSLList.nil(); - GenericSortCondition c; + ImmutableList c; final Iterator it; @@ -75,8 +75,10 @@ public static GenericSortInstantiations create( p_instantiations.next(); c = GenericSortCondition.createCondition(entry.key(), entry.value()); if (c != null) { - p_conditions = p_conditions.prepend(c); - sorts = sorts.prepend(c.getGenericSort()); + for (var cond : c) { + p_conditions = p_conditions.prepend(c); + sorts = sorts.prepend(cond.getGenericSort()); + } } } return create(sorts, p_conditions, services); @@ -112,9 +114,10 @@ public Boolean checkSorts(OperatorSV sv, InstantiationEntry p_entry) { return Boolean.TRUE; } - final GenericSortCondition c = GenericSortCondition.createCondition(sv, p_entry); + final ImmutableList c = + GenericSortCondition.createCondition(sv, p_entry); if (c != null) { - return checkCondition(c); + return checkConditions(c); } if (GenericSortCondition.subSortsAllowed(sv)) { @@ -124,6 +127,14 @@ public Boolean checkSorts(OperatorSV sv, InstantiationEntry p_entry) { } } + public Boolean checkConditions(ImmutableList p_condition) { + for (var cond : p_condition) { + var r = checkCondition(cond); + if (r == null || !r) + return null; + } + return true; + } /** * @return Boolean.TRUE if the generic sort instantiations within "this" satisfy "p_condition", diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java index 3eab9950c88..a53c10c720d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java @@ -5,9 +5,11 @@ import java.util.ArrayList; +import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import org.key_project.logic.op.Modality; import org.key_project.logic.op.Operator; @@ -66,40 +68,62 @@ private static void createProgram(JTerm pattern, ArrayList progra } else { program.add(getCheckNodeKindInstruction(JTerm.class)); program.add(gotoNextInstruction()); - if (op instanceof final SortDependingFunction sortDependingFunction) { - program.add(getCheckNodeKindInstruction(SortDependingFunction.class)); - program.add(getSimilarSortDependingFunctionInstruction(sortDependingFunction)); - program.add(gotoNextInstruction()); - if (sortDependingFunction.getSortDependingOn() instanceof GenericSort gs) { - program.add(getMatchGenericSortInstruction(gs)); - } else { - program.add(getMatchIdentityInstruction(sortDependingFunction.getChild(0))); + switch (op) { + case ParametricFunctionInstance pfi -> { + program.add(getCheckNodeKindInstruction(ParametricFunctionInstance.class)); + program.add(getSimilarParametricFunctionInstruction(pfi)); + program.add(gotoNextInstruction()); + for (int i = 0; i < pfi.getChildCount(); i++) { + var arg = (GenericArgument) pfi.getChild(i); + if (arg.sort() instanceof GenericSort gs) { + program.add(getMatchGenericSortInstruction(gs)); + } else if (arg.sort() instanceof ParametricSortInstance) { + throw new UnsupportedOperationException( + "TODO @ DD: Parametric sort in generic args!"); + } else { + program.add(getMatchIdentityInstruction(arg)); + } + program.add(gotoNextInstruction()); + } } - program.add(gotoNextInstruction()); - } else if (op instanceof ElementaryUpdate elUp) { - program.add(getCheckNodeKindInstruction(ElementaryUpdate.class)); - program.add(gotoNextInstruction()); - if (elUp.lhs() instanceof SchemaVariable sv) { - program.add(getMatchInstructionForSV(sv)); - program.add(gotoNextSiblingInstruction()); - } else if (elUp.lhs() instanceof LocationVariable locVar) { - program.add(getMatchIdentityInstruction(locVar)); + case final SortDependingFunction sortDependingFunction -> { + program.add(getCheckNodeKindInstruction(SortDependingFunction.class)); + program.add(getSimilarSortDependingFunctionInstruction(sortDependingFunction)); + program.add(gotoNextInstruction()); + if (sortDependingFunction.getSortDependingOn() instanceof GenericSort gs) { + program.add(getMatchGenericSortInstruction(gs)); + } else { + program.add(getMatchIdentityInstruction(sortDependingFunction.getChild(0))); + } program.add(gotoNextInstruction()); } - } else if (op instanceof Modality mod) { - program.add(getCheckNodeKindInstruction(Modality.class)); - program.add(gotoNextInstruction()); - if (mod.kind() instanceof ModalOperatorSV modKindSV) { - program.add(matchModalOperatorSV(modKindSV)); - } else { - program.add(getMatchIdentityInstruction(mod.kind())); + case ElementaryUpdate elUp -> { + program.add(getCheckNodeKindInstruction(ElementaryUpdate.class)); + program.add(gotoNextInstruction()); + if (elUp.lhs() instanceof SchemaVariable sv) { + program.add(getMatchInstructionForSV(sv)); + program.add(gotoNextSiblingInstruction()); + } else if (elUp.lhs() instanceof LocationVariable locVar) { + program.add(getMatchIdentityInstruction(locVar)); + program.add(gotoNextInstruction()); + } + } + case Modality mod -> { + program.add(getCheckNodeKindInstruction(Modality.class)); + program.add(gotoNextInstruction()); + if (mod.kind() instanceof ModalOperatorSV modKindSV) { + program.add(matchModalOperatorSV(modKindSV)); + } else { + program.add(getMatchIdentityInstruction(mod.kind())); + } + program.add(gotoNextInstruction()); + program.add(matchProgram(pattern.javaBlock().program())); + program.add(gotoNextSiblingInstruction()); + } + default -> { + program.add(getMatchIdentityInstruction(op)); + program.add(gotoNextInstruction()); } - program.add(gotoNextInstruction()); - program.add(matchProgram(pattern.javaBlock().program())); - program.add(gotoNextSiblingInstruction()); - } else { - program.add(getMatchIdentityInstruction(op)); - program.add(gotoNextInstruction()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/JavaDLMatchVMInstructionSet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/JavaDLMatchVMInstructionSet.java index 1c21f68e9ff..b71c734d4a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/JavaDLMatchVMInstructionSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/JavaDLMatchVMInstructionSet.java @@ -94,6 +94,11 @@ public static SimilarSortDependingFunctionInstruction getSimilarSortDependingFun return new SimilarSortDependingFunctionInstruction(sortDependingFunction); } + public static SimilarParametricFunctionInstruction getSimilarParametricFunctionInstruction( + ParametricFunctionInstance psi) { + return new SimilarParametricFunctionInstruction(psi); + } + public static MatchIdentityInstruction getMatchIdentityInstruction( SyntaxElement syntaxElement) { return new MatchIdentityInstruction(syntaxElement); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/SimilarParametricFunctionInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/SimilarParametricFunctionInstruction.java new file mode 100644 index 00000000000..88554f7a5ee --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/SimilarParametricFunctionInstruction.java @@ -0,0 +1,30 @@ +/* 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.rule.match.vm.instructions; + +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; + +import org.jspecify.annotations.Nullable; + +public class SimilarParametricFunctionInstruction implements MatchInstruction { + private final ParametricFunctionInstance pfi; + + public SimilarParametricFunctionInstruction(ParametricFunctionInstance pfi) { + this.pfi = pfi; + } + + @Override + public @Nullable MatchResultInfo match(SyntaxElement actualElement, + MatchResultInfo matchConditions, LogicServices services) { + if (((ParametricFunctionInstance) actualElement).getBase() == pfi.getBase()) { + return matchConditions; + } + return null; + } +} 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 d291665158e..ee6d03869b2 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 @@ -195,13 +195,15 @@ public void setUp() { proof.add(g); proof.setNamespaces(new NamespaceSet(variables, functions, sorts, 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<>())); + return TacletForTests.parseTerm(termstr, + new NamespaceSet(variables, functions, sorts, new Namespace<>(), new Namespace<>(), + new Namespace<>(), new Namespace<>(), new Namespace<>())); } @Test 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..2c856a0d1a6 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,16 @@ public static void addAll(Collection collection, Iterable iterable) { list.add(index, toInsert); } } + + public static List findDuplicates( + Iterable it) { + List result = new ArrayList<>(); + Set alreadySeen = new HashSet<>(); + for (T element : it) { + if (!alreadySeen.add(element)) { + result.add(element); + } + } + return result; + } } From d8083c9ebc81db2ed64b686c4eb1ac0cd2bf223f Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 13 Aug 2025 13:48:17 +0200 Subject: [PATCH 02/13] Fix SortDepFn and add test --- .../key/logic/op/SortDependingFunction.java | 11 +- .../key/logic/sort/TestParametricSorts.java | 123 ++++++++++++++++++ 2 files changed, 128 insertions(+), 6 deletions(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java 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 b0051025fc1..3b9d652a7d7 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 @@ -8,6 +8,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), + ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, template.sort), instantiateArgSorts(template, sortDependingOn), null, template.unique, false); this.template = template; this.sortDependingOn = sortDependingOn; @@ -55,8 +56,8 @@ private static Name instantiateName(Name kind, Sort sortDependingOn) { } - private static Sort instantiateResultSort(SortDependingFunctionTemplate template, - Sort sortDependingOn) { + private static Sort instantiateSort(SortDependingFunctionTemplate template, + Sort sortDependingOn) { return template.sort == template.sortDependingOn ? sortDependingOn : template.sort; } @@ -65,8 +66,7 @@ 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); } @@ -109,7 +109,6 @@ public synchronized SortDependingFunction getInstanceFor(Sort sort, TermServices SortDependingFunction n = (SortDependingFunction) services.getNamespaces() .lookup(instantiateName(getKind(), sort)); - if (sort instanceof ProgramSVSort) { throw new AssertionError(); } 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..e4ef0d2062e --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java @@ -0,0 +1,123 @@ +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.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; +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.ImmutableArray; +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 ParametricSortDecl addParametricSort(String name, GenericParameter.Variance... variance) { + ImmutableList params = ImmutableList.of(); + for (int i = 0; i < variance.length; i++) { + GenericParameter.Variance varia = variance[i]; + GenericSort genSort = (GenericSort) nss.sorts().lookup("G" + (i + 1)); + params = params.prepend(new GenericParameter(genSort, varia)); + } + ParametricSortDecl psd = new ParametricSortDecl(new Name(name), false,ImmutableSet.empty(), + params, "", ""); + nss.parametricSorts().add(psd); + return psd; + } + + + @Test + public void testParametricSortIdentical() { + ParametricSortDecl psd = addParametricSort("List", GenericParameter.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() { + ParametricSortDecl psd = addParametricSort("List", GenericParameter.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(new GenericArgument(intSort))); + var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(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(new Sort[0]).toString()); + assertSame(term.sub(0).sort(), term.sub(1).sort()); + } + + @Test + public void testParametricFunctionInstantiation() { + ParametricSortDecl psd = addParametricSort("List", GenericParameter.Variance.COVARIANT); + Sort intSort = nss.sorts().lookup("int"); + + var someConst = new ParametricFunctionDecl(new Name("someConst"), ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), new ImmutableArray<>(), g1, null, false, true, false); + nss.parametricFunctions().add(someConst); + + var listOfInt = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); + var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1))); + + var head = new ParametricFunctionDecl(new Name("head"),ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), new ImmutableArray<>(listOfG1), g1, null, false, true, false); + nss.parametricFunctions().add(head); + + var headInst = ParametricFunctionInstance.get(head, ImmutableList.of(new GenericArgument(intSort))); + assertEquals(intSort, headInst.sort()); + assertEquals(listOfInt, headInst.argSort(0)); + + var term = io.parseExpression("head<[int]>(someConst<[List<[int]>]>) = someConst<[int]>"); + 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(new Sort[0]).toString()); + assertSame(term.sub(0).sort(), term.sub(1).sort()); + } +} \ No newline at end of file From 7a4544399cd8a649b69f6a0b4b7c01cc4019a788 Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 13 Aug 2025 14:37:10 +0200 Subject: [PATCH 03/13] Fix fns and preds parsing; add test --- key.core/src/main/antlr4/KeYParser.g4 | 4 +- .../key/logic/op/SortDependingFunction.java | 8 ++- .../nparser/builder/DeclarationBuilder.java | 38 ++---------- .../key/nparser/builder/DefaultBuilder.java | 36 ++++++++++-- .../builder/FunctionPredicateBuilder.java | 58 +++++++++++++++++-- .../key/logic/sort/TestParametricSorts.java | 48 ++++++++++----- .../proof/runallproofs/ProofCollections.java | 3 + .../standard_key/polymorphic/pseq.key | 42 ++++++++++++++ 8 files changed, 176 insertions(+), 61 deletions(-) create mode 100644 key.ui/examples/standard_key/polymorphic/pseq.key diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 921243124ae..6d64eec5c61 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -215,6 +215,7 @@ pred_decl : doc=DOC_COMMENT? pred_name = funcpred_name + formal_sort_param_decls? (whereToBind=where_to_bind)? argSorts=arg_sorts SEMI @@ -231,7 +232,8 @@ func_decl (UNIQUE)? retSort = sortId func_name = funcpred_name - whereToBind=where_to_bind? + formal_sort_param_decls? + whereToBind=where_to_bind? argSorts = arg_sorts SEMI ; 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 3b9d652a7d7..ce5bde2e368 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 @@ -40,7 +40,8 @@ public final class SortDependingFunction extends JFunction { private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortDependingOn) { super(instantiateName(template.kind, sortDependingOn), - ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, template.sort), + ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, + template.sort), instantiateArgSorts(template, sortDependingOn), null, template.unique, false); this.template = template; this.sortDependingOn = sortDependingOn; @@ -57,7 +58,7 @@ private static Name instantiateName(Name kind, Sort sortDependingOn) { private static Sort instantiateSort(SortDependingFunctionTemplate template, - Sort sortDependingOn) { + Sort sortDependingOn) { return template.sort == template.sortDependingOn ? sortDependingOn : template.sort; } @@ -66,7 +67,8 @@ private static ImmutableArray instantiateArgSorts(SortDependingFunctionTem Sort sortDependingOn) { Sort[] result = new Sort[template.argSorts.size()]; for (int i = 0; i < result.length; i++) { - result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, template.argSorts.get(i)); + result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, + sortDependingOn, template.argSorts.get(i)); } return new ImmutableArray<>(result); } 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 69b05b8f37d..156f6be9a51 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 @@ -26,7 +26,6 @@ import org.key_project.util.java.CollectionUtil; import org.antlr.v4.runtime.Token; -import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -224,43 +223,18 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { } String name = declCtx.simple_ident_dots().getText(); Name sortName = new Name(name); + if (sorts().lookup(sortName) != null) { + semanticError(declCtx, + "Cannot declare parametric sort %s, as a sort of the same name has already been declared", + sortName); + } var sortDecl = new ParametricSortDecl(sortName, isAbstractSort, ext, params, documentation, BuilderHelpers.getPosition(declCtx)); - namespaces().parametricSorts().add(sortDecl); + namespaces().parametricSorts().addSafely(sortDecl); } return createdSorts; } - @Override - public @Nullable List visitFormal_sort_param_decls( - KeYParser.Formal_sort_param_declsContext ctx) { - return mapOf(ctx.formal_sort_param_decl()); - } - - @Override - public @Nullable GenericParameter visitFormal_sort_param_decl( - KeYParser.Formal_sort_param_declContext ctx) { - - GenericParameter.Variance variance; - if (ctx.PLUS() != null) { - variance = GenericParameter.Variance.COVARIANT; - } else if (ctx.MINUS() != null) { - variance = GenericParameter.Variance.CONTRAVARIANT; - } else { - variance = GenericParameter.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 GenericParameter((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 7bc7dcdb919..2dbbb035279 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 @@ -18,10 +18,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; -import de.uka.ilkd.key.logic.sort.ArraySort; -import de.uka.ilkd.key.logic.sort.NullSort; -import de.uka.ilkd.key.logic.sort.ParametricSortDecl; -import de.uka.ilkd.key.logic.sort.ParametricSortInstance; +import de.uka.ilkd.key.logic.sort.*; import de.uka.ilkd.key.nparser.KeYParser; import org.key_project.logic.*; @@ -37,6 +34,7 @@ import org.key_project.util.collection.Pair; import org.antlr.v4.runtime.ParserRuleContext; +import org.jspecify.annotations.Nullable; /** * Helper class for are visitor that requires a namespaces and services. Also it provides the @@ -446,4 +444,34 @@ public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return ctx.getText(); } + + @Override + public @Nullable List visitFormal_sort_param_decls( + KeYParser.Formal_sort_param_declsContext ctx) { + return mapOf(ctx.formal_sort_param_decl()); + } + + @Override + public @Nullable GenericParameter visitFormal_sort_param_decl( + KeYParser.Formal_sort_param_declContext ctx) { + + GenericParameter.Variance variance; + if (ctx.PLUS() != null) { + variance = GenericParameter.Variance.COVARIANT; + } else if (ctx.MINUS() != null) { + variance = GenericParameter.Variance.CONTRAVARIANT; + } else { + variance = GenericParameter.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 GenericParameter((GenericSort) paramSort, variance); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index 3163365d1f8..dd620a9a227 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java @@ -7,8 +7,10 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.ldt.JavaDLTheory; +import de.uka.ilkd.key.logic.GenericParameter; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; import de.uka.ilkd.key.logic.op.SortDependingFunction; import de.uka.ilkd.key.logic.op.Transformer; import de.uka.ilkd.key.logic.sort.GenericSort; @@ -19,6 +21,7 @@ import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; /** @@ -85,6 +88,8 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { @Override public Object visitPred_decl(KeYParser.Pred_declContext ctx) { String pred_name = accept(ctx.funcpred_name()); + List params = ctx.formal_sort_param_decls() == null ? null + : visitFormal_sort_param_decls(ctx.formal_sort_param_decls()); List whereToBind = accept(ctx.where_to_bind()); List argSorts = accept(ctx.arg_sorts()); if (whereToBind != null && whereToBind.size() != argSorts.size()) { @@ -107,9 +112,30 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { if (p == null) { assert argSorts != null; - p = new JFunction(new Name(pred_name), JavaDLTheory.FORMULA, - argSorts.toArray(new Sort[0]), - whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), false); + Name name = new Name(pred_name); + Boolean[] whereToBind1 = + whereToBind == null ? null : whereToBind.toArray(new Boolean[0]); + if (params == null) { + if (nss.parametricFunctions().lookup(name) != null) { + semanticError(ctx, + "Cannot declare predicate %s: Parametric predicate already exists", name); + } + p = new JFunction(name, JavaDLTheory.FORMULA, + argSorts.toArray(new Sort[0]), + whereToBind1, false); + } else { + if (functions().lookup(name) != null) { + semanticError(ctx, + "Cannot declare parametric predicate %s: Predicate already exists", name); + } + var d = new ParametricFunctionDecl(name, ImmutableList.fromList(params), + new ImmutableArray<>(argSorts), + JavaDLTheory.FORMULA, + whereToBind == null ? null : new ImmutableArray<>(whereToBind1), false, true, + false); + nss.parametricFunctions().addSafely(d); + return null; + } } if (lookup(p.name()) == null) { @@ -126,6 +152,8 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { boolean unique = ctx.UNIQUE() != null; Sort retSort = accept(ctx.sortId()); String funcName = accept(ctx.funcpred_name()); + List params = ctx.formal_sort_param_decls() == null ? null + : visitFormal_sort_param_decls(ctx.formal_sort_param_decls()); List whereToBind = accept(ctx.where_to_bind()); List argSorts = accept(ctx.arg_sorts()); assert argSorts != null; @@ -148,8 +176,28 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { } if (f == null) { - f = new JFunction(new Name(funcName), retSort, argSorts.toArray(new Sort[0]), - whereToBind == null ? null : whereToBind.toArray(new Boolean[0]), unique); + Name name = new Name(funcName); + Boolean[] whereToBind1 = + whereToBind == null ? null : whereToBind.toArray(new Boolean[0]); + if (params == null) { + if (nss.parametricFunctions().lookup(name) != null) { + semanticError(ctx, + "Cannot declare function %s: Parametric function already exists", name); + } + f = new JFunction(name, retSort, argSorts.toArray(new Sort[0]), + whereToBind1, unique); + } else { + if (functions().lookup(name) != null) { + semanticError(ctx, + "Cannot declare parametric function %s: Function already exists", name); + } + var d = new ParametricFunctionDecl(name, ImmutableList.fromList(params), + new ImmutableArray<>(argSorts), + retSort, whereToBind == null ? null : new ImmutableArray<>(whereToBind1), + unique, true, false); + nss.parametricFunctions().add(d); + return null; + } } if (lookup(f.name()) == null) { 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 index e4ef0d2062e..de92bfcda7c 100644 --- 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 @@ -1,3 +1,6 @@ +/* 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; @@ -12,14 +15,16 @@ 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.ImmutableArray; 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.*; class TestParametricSorts { @@ -47,15 +52,16 @@ public void setUp() { r2k.parseSpecialClasses(); } - private ParametricSortDecl addParametricSort(String name, GenericParameter.Variance... variance) { + private ParametricSortDecl addParametricSort(String name, + GenericParameter.Variance... variance) { ImmutableList params = ImmutableList.of(); for (int i = 0; i < variance.length; i++) { GenericParameter.Variance varia = variance[i]; GenericSort genSort = (GenericSort) nss.sorts().lookup("G" + (i + 1)); params = params.prepend(new GenericParameter(genSort, varia)); } - ParametricSortDecl psd = new ParametricSortDecl(new Name(name), false,ImmutableSet.empty(), - params, "", ""); + ParametricSortDecl psd = new ParametricSortDecl(new Name(name), false, ImmutableSet.empty(), + params, "", ""); nss.parametricSorts().add(psd); return psd; } @@ -64,7 +70,8 @@ private ParametricSortDecl addParametricSort(String name, GenericParameter.Varia @Test public void testParametricSortIdentical() { ParametricSortDecl psd = addParametricSort("List", GenericParameter.Variance.COVARIANT); - var sdf = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, new Sort[0], false); + 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"); @@ -77,12 +84,15 @@ public void testParametricSortDependentFunctionInstantiation() { ParametricSortDecl psd = addParametricSort("List", GenericParameter.Variance.COVARIANT); Sort intSort = nss.sorts().lookup("int"); - var someConst = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, new Sort[0], false); + var someConst = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, + new Sort[0], false); nss.functions().add(someConst); - var listOfInt = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); + var listOfInt = + ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1))); - var sdf = SortDependingFunction.createFirstInstance(g1, new Name("head"), g1, new Sort[] {listOfG1}, false); + var sdf = SortDependingFunction.createFirstInstance(g1, new Name("head"), g1, + new Sort[] { listOfG1 }, false); nss.functions().add(sdf); SortDependingFunction sdfInst = sdf.getInstanceFor(intSort, services); @@ -91,7 +101,7 @@ public void testParametricSortDependentFunctionInstantiation() { 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("List<[int]>", ((JFunction) term.sub(0).op()).argSorts().get(0).toString()); assertEquals("int", term.sub(0).op().sort(new Sort[0]).toString()); assertSame(term.sub(0).sort(), term.sub(1).sort()); } @@ -101,23 +111,29 @@ public void testParametricFunctionInstantiation() { ParametricSortDecl psd = addParametricSort("List", GenericParameter.Variance.COVARIANT); Sort intSort = nss.sorts().lookup("int"); - var someConst = new ParametricFunctionDecl(new Name("someConst"), ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), new ImmutableArray<>(), g1, null, false, true, false); + var someConst = new ParametricFunctionDecl(new Name("someConst"), + ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), + new ImmutableArray<>(), g1, null, false, true, false); nss.parametricFunctions().add(someConst); - var listOfInt = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); + var listOfInt = + ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1))); - var head = new ParametricFunctionDecl(new Name("head"),ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), new ImmutableArray<>(listOfG1), g1, null, false, true, false); + var head = new ParametricFunctionDecl(new Name("head"), + ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), + new ImmutableArray<>(listOfG1), g1, null, false, true, false); nss.parametricFunctions().add(head); - var headInst = ParametricFunctionInstance.get(head, ImmutableList.of(new GenericArgument(intSort))); + var headInst = + ParametricFunctionInstance.get(head, ImmutableList.of(new GenericArgument(intSort))); assertEquals(intSort, headInst.sort()); assertEquals(listOfInt, headInst.argSort(0)); var term = io.parseExpression("head<[int]>(someConst<[List<[int]>]>) = someConst<[int]>"); assertEquals("List<[int]>", term.sub(0).sub(0).sort().toString()); - assertEquals("List<[int]>", ((JFunction)term.sub(0).op()).argSorts().get(0).toString()); + assertEquals("List<[int]>", ((JFunction) term.sub(0).op()).argSorts().get(0).toString()); assertEquals("int", term.sub(0).op().sort(new Sort[0]).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/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index c255c3a1308..4b6cea4efe9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -996,6 +996,9 @@ public static ProofCollection automaticJavaDL() throws IOException { g.loadable("standard_key/adt/dt_color.proof"); g.loadable("standard_key/adt/dt_list_deconstruct.key"); + g = c.group("PolymorphicSorts"); + g.loadable("standard_key/polymorphic/pseq.key"); + // use for debugging purposes. // c.keep("VSTTE10"); String s = System.getenv(ENV_KEY_RAP_FUN_KEEP); diff --git a/key.ui/examples/standard_key/polymorphic/pseq.key b/key.ui/examples/standard_key/polymorphic/pseq.key new file mode 100644 index 00000000000..6c48e88ba4c --- /dev/null +++ b/key.ui/examples/standard_key/polymorphic/pseq.key @@ -0,0 +1,42 @@ +\sorts { + \generic E; + PSeq<[E]>; +} + +\functions { + PSeq<[int]> s1; + PSeq<[int]> s2; + + // getters + E pseqGet<[E]>(PSeq<[E]>, int); + int pseqLen<[E]>(PSeq<[E]>); + int pseqIndexOf<[E]>(PSeq<[E]>, E); + E pseqGetOutside<[E]>; + + // constructors + PSeq<[E]> pseqEmpty<[E]>; + PSeq<[E]> pseqSingleton<[E]>(E); + PSeq<[E]> pseqConcat<[E]>(PSeq<[E]>, PSeq<[E]>); + PSeq<[E]> pseqSub<[E]>(PSeq<[E]>, int, int); + PSeq<[E]> pseqReverse<[E]>(PSeq<[E]>); + PSeq<[E]> pseqUpd<[E]>(PSeq<[E]>, int, E); + PSeq<[E]> pseqDef {false, false, true}(int, int, E); + + PSeq<[E]> pseqSwap<[E]>(PSeq<[E]>, int, int); + PSeq<[E]> pseqRemove<[E]>(PSeq<[E]>, int); + PSeq<[E]> pseqNPermInv<[E]>(PSeq<[E]>); +} + +\problem { + s1 = pseqConcat<[int]>(pseqConcat<[int]>(pseqSingleton<[int]>(54), pseqSingleton<[int]>(4)), pseqSingleton<[int]>(100)) + & s2 = pseqConcat<[int]>(pseqEmpty<[int]>, pseqSub<[int]>(s1, 1, 3)) + -> + \forall int i; (0 <= i & i < pseqLen<[int]>(s1) -> pseqGet<[int]>(s1, i) > 0) + & pseqGet<[int]>(s1, 1) = 4 + & pseqLen<[int]>(s1) = 3 + & pseqLen<[int]>(s2) = 2 + & pseqGet<[int]>(s2, 1) = 100 + & pseqReverse<[int]>(s1) = pseqConcat<[int]>(pseqConcat<[int]>(pseqSingleton<[int]>(100), pseqSingleton<[int]>(4)), pseqSingleton<[int]>(54)) + & pseqConcat<[int]>(pseqEmpty<[int]>, pseqReverse<[int]>(pseqEmpty<[int]>)) = pseqEmpty<[int]> + & \forall PSeq<[int]> s; (pseqSub<[int]>(s, 0, pseqLen<[int]>(s)) = s) +} \ No newline at end of file From a73bcdd05aae64f485446c2f7b7d2d3967fc6b62 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 14 Aug 2025 12:03:00 +0200 Subject: [PATCH 04/13] Finish example; slight fixes --- .../logic/op/ParametricFunctionInstance.java | 12 + .../MatchGenericSortInstruction.java | 9 +- .../standard_key/polymorphic/pseq.key | 663 +++++++++++++++++- 3 files changed, 682 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java index de271d4a4e6..af61c8f2217 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java @@ -116,4 +116,16 @@ public int getChildCount() { public @NonNull SyntaxElement getChild(int n) { return Objects.requireNonNull(args.get(n)); } + + @Override + public boolean equals(Object o) { + if (o == null || getClass() != o.getClass()) return false; + ParametricFunctionInstance that = (ParametricFunctionInstance) o; + return Objects.equals(args, that.args) && Objects.equals(base, that.base); + } + + @Override + public int hashCode() { + return Objects.hash(args, base); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java index 1c8d4d20018..27ded81f5cb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.match.vm.instructions; +import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.op.QualifierWrapper; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.inst.GenericSortCondition; @@ -56,7 +57,13 @@ private MatchResultInfo matchSorts(Sort dependingSortToMatch, MatchResultInfo ma @Override public MatchResultInfo match(SyntaxElement actualElement, MatchResultInfo mc, LogicServices services) { - return matchSorts(((QualifierWrapper) actualElement).getQualifier(), mc, services); + if (actualElement instanceof GenericArgument(Sort sort)) { + return matchSorts(sort, mc, services); + } + if (actualElement instanceof QualifierWrapper w && w.getQualifier() instanceof Sort sort) { + return matchSorts(sort, mc, services); + } + return null; } } diff --git a/key.ui/examples/standard_key/polymorphic/pseq.key b/key.ui/examples/standard_key/polymorphic/pseq.key index 6c48e88ba4c..7d32a4de6b8 100644 --- a/key.ui/examples/standard_key/polymorphic/pseq.key +++ b/key.ui/examples/standard_key/polymorphic/pseq.key @@ -20,13 +20,200 @@ PSeq<[E]> pseqSub<[E]>(PSeq<[E]>, int, int); PSeq<[E]> pseqReverse<[E]>(PSeq<[E]>); PSeq<[E]> pseqUpd<[E]>(PSeq<[E]>, int, E); - PSeq<[E]> pseqDef {false, false, true}(int, int, E); + PSeq<[E]> pseqDef<[E]> {false, false, true}(int, int, E); PSeq<[E]> pseqSwap<[E]>(PSeq<[E]>, int, int); PSeq<[E]> pseqRemove<[E]>(PSeq<[E]>, int); PSeq<[E]> pseqNPermInv<[E]>(PSeq<[E]>); } +\rules { + \lemma + pseqConcatWithPSeqEmpty1 { + \schemaVar \term Seq seq; + + \find(seqConcat(seq, seqEmpty)) + + \replacewith(seq) + + \heuristics(concrete) + \displayname "pseqConcatWithEmpty" + }; + + \lemma + pseqConcatWithPSeqEmpty2 { + \schemaVar \term PSeq<[E]> seq; + + \find(pseqConcat<[E]>(pseqEmpty<[E]>, seq)) + + \replacewith(seq) + + \heuristics(concrete) + \displayname "pseqConcatWithEmpty" + }; + + \lemma + pseqReverseOfPSeqEmpty { + \find(pseqReverse<[E]>(pseqEmpty<[E]>)) + + \replacewith(pseqEmpty<[E]>) + + \heuristics(concrete) + }; + + subPSeqEmpty { + \schemaVar \term PSeq<[E]> seq; + \schemaVar \term int i; + \find(pseqSub<[E]>(seq, i, i)) + \replacewith(pseqEmpty<[E]>) + \heuristics(concrete) + }; + + \lemma + subPSeqComplete { + \schemaVar \term PSeq<[E]> seq; + + \find(pseqSub<[E]>(seq, 0, pseqLen<[E]>(seq))) + \replacewith(seq) + \heuristics(concrete) + }; + + subPSeqSingleton { + \schemaVar \term PSeq<[E]> seq; + \schemaVar \term E x; + + \find(pseqSub<[E]>(pseqSingleton<[E]>(x), 0, 1)) + + \replacewith(pseqSingleton<[E]>(x)) + + \heuristics(concrete) + }; + + subPSeqConcat { + \schemaVar \term PSeq<[E]> s1, s2; + \schemaVar \term int l, u; + + \find(pseqSub<[E]>(pseqConcat<[E]>(s1, s2), l, u)) + + \replacewith(pseqConcat<[E]>(pseqSub<[E]>(s1, l, \if(pseqLen<[E]>(s1) < u) \then(pseqLen<[E]>(s1)) \else(u)), + pseqSub<[E]>(s2, \if(l < pseqLen<[E]>(s1)) \then(0) \else(l - pseqLen<[E]>(s1)), u - pseqLen<[E]>(s1)))) + + \heuristics(simplify_enlarging) + }; + + \lemma + lenOfPSeqSubEQ { + \schemaVar \term PSeq<[E]> seq; + \schemaVar \term int from, to; + \schemaVar \term PSeq<[E]> EQ; + + \assumes(pseqSub<[E]>(seq, from, to) = EQ ==>) + \find(pseqLen<[E]>(EQ)) + \sameUpdateLevel + + \replacewith(\if(from < to) \then(to - from) \else(0)) + + \heuristics(simplify, find_term_not_in_assumes) + \displayname "lenOfSeqSub" + }; + + \lemma + lenOfPSeqSingleton { + \schemaVar \term E x; + + \find(pseqLen<[E]>(pseqSingleton<[E]>(x))) + + \replacewith(1) + + \heuristics(concrete) + }; + + \lemma + lenOfPSeqConcat { + \schemaVar \term PSeq<[E]> seq, seq2; + + \find(pseqLen<[E]>(pseqConcat<[E]>(seq, seq2))) + + \replacewith(pseqLen<[E]>(seq) + pseqLen<[E]>(seq2)) + + \heuristics(simplify) + }; + + \lemma + lenOfPSeqReverse { + \schemaVar \term PSeq<[E]> seq; + + \find(pseqLen<[E]>(pseqReverse<[E]>(seq))) + + \replacewith(pseqLen<[E]>(seq)) + + \heuristics(simplify) + }; + + \lemma + getOfPSeqSingleton { + \schemaVar \term E x; + \schemaVar \term int idx; + + \find(pseqGet<[E]>(pseqSingleton<[E]>(x), idx)) + + \replacewith(\if(idx = 0) + \then(x) + \else(pseqGetOutside<[E]>)) + + \heuristics(simplify) + }; + + \lemma + getOfPSeqSingletonConcrete { + \schemaVar \term E x; + \find(pseqGet<[E]>(pseqSingleton<[E]>(x), 0)) + \replacewith(x) + \heuristics(concrete) + }; + + \lemma + getOfPSeqConcat { + \schemaVar \term PSeq<[E]> seq, seq2; + \schemaVar \term int idx; + + \find(pseqGet<[E]>(pseqConcat<[E]>(seq, seq2), idx)) + + \replacewith(\if(idx < pseqLen<[E]>(seq)) + \then(pseqGet<[E]>(seq, idx)) + \else(pseqGet<[E]>(seq2, idx - pseqLen<[E]>(seq)))) + + \heuristics(simplify_enlarging) + }; + + \lemma + getOfPSeqReverse { + \schemaVar \term PSeq<[E]> seq; + \schemaVar \term int idx; + + \find(pseqGet<[E]>(pseqReverse<[E]>(seq), idx)) + + \replacewith(pseqGet<[E]>(seq, pseqLen<[E]>(seq) - 1 - idx)) + + \heuristics(simplify_enlarging) + }; + + \lemma + equalityToPSeqGetAndPSeqLenRight { + \schemaVar \term PSeq<[E]> s, s2; + \schemaVar \variables int iv; + + \find( ==> s = s2) + \varcond(\notFreeIn(iv, s, s2)) + + \replacewith( ==> pseqLen<[E]>(s) = pseqLen<[E]>(s2) + & \forall iv; (0 <= iv & iv < pseqLen<[E]>(s) + -> pseqGet<[E]>(s, iv) = pseqGet<[E]>(s2, iv))) + + \heuristics(simplify_enlarging) + }; +} + \problem { s1 = pseqConcat<[int]>(pseqConcat<[int]>(pseqSingleton<[int]>(54), pseqSingleton<[int]>(4)), pseqSingleton<[int]>(100)) & s2 = pseqConcat<[int]>(pseqEmpty<[int]>, pseqSub<[int]>(s1, 1, 3)) @@ -39,4 +226,478 @@ & pseqReverse<[int]>(s1) = pseqConcat<[int]>(pseqConcat<[int]>(pseqSingleton<[int]>(100), pseqSingleton<[int]>(4)), pseqSingleton<[int]>(54)) & pseqConcat<[int]>(pseqEmpty<[int]>, pseqReverse<[int]>(pseqEmpty<[int]>)) = pseqEmpty<[int]> & \forall PSeq<[int]> s; (pseqSub<[int]>(s, 0, pseqLen<[int]>(s)) = s) +} + +\proof { + (branch "dummy ID" + (rule "pseqConcatWithPSeqEmpty2" (formula "1") (term "1,1,0")) + (rule "subPSeqComplete" (formula "1") (term "0,0,1,1")) + (rule "eqClose" (formula "1") (term "0,1,1")) + (rule "pseqConcatWithPSeqEmpty2" (formula "1") (term "0,1,0,1")) + (rule "pseqReverseOfPSeqEmpty" (formula "1") (term "0,1,0,1")) + (rule "eqClose" (formula "1") (term "1,0,1")) + (rule "concrete_and_3" (formula "1") (term "0,1")) + (rule "impRight" (formula "1")) + (rule "andLeft" (formula "1")) + (rule "eqSymm" (formula "2")) + (rule "lenOfPSeqSubEQ" (formula "3") (term "0,1,0,0,0") (ifseqformula "2")) + (rule "less_literals" (formula "3") (term "0,0,1,0,0,0")) + (rule "ifthenelse_true" (formula "3") (term "0,1,0,0,0")) + (rule "sub_literals" (formula "3") (term "0,1,0,0,0")) + (rule "eqClose" (formula "3") (term "1,0,0,0")) + (rule "concrete_and_3" (formula "3") (term "0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "3") (term "1,0,0,0,0,0,0,0")) + (rule "polySimp_mulComm0" (formula "3") (term "1,0,0,1,0,0,0,0,0,0,0")) + (rule "inEqSimp_gtToGeq" (formula "3") (term "1,0,0,0,0,0,0")) + (rule "times_zero_1" (formula "3") (term "1,0,0,1,0,0,0,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,1,0,0,0,0,0,0")) + (rule "inEqSimp_commuteLeq" (formula "3") (term "0,0,0,0,0,0,0,0")) + (rule "applyEqRigid" (formula "2") (term "0,0") (ifseqformula "1")) + (rule "applyEqRigid" (formula "3") (term "0,0,1,0") (ifseqformula "1")) + (rule "applyEqRigid" (formula "3") (term "0,1,0,1,0,0,0,0,0,0") (ifseqformula "1")) + (rule "applyEq" (formula "3") (term "0,0,1,0,0,0,0") (ifseqformula "1")) + (rule "applyEq" (formula "3") (term "0,0,1,0,0,1,0,0,0,0,0,0,0") (ifseqformula "1")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,1,0,0,1,0,0,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,1,0,0,1,0,0,0,0,0,0,0")) + (rule "polySimp_mulComm0" (formula "3") (term "1,0,0,1,0,0,0,0,0,0,0")) + (rule "polySimp_addComm0" (formula "3") (term "1,1,0,0,1,0,0,0,0,0,0,0")) + (rule "polySimp_rightDist" (formula "3") (term "1,0,0,1,0,0,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "0,1,0,0,1,0,0,0,0,0,0,0")) + (rule "polySimp_addAssoc" (formula "3") (term "0,0,1,0,0,0,0,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,0,1,0,0,0,0,0,0,0")) + (rule "add_zero_left" (formula "3") (term "0,0,1,0,0,0,0,0,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,0,0,1,0,0,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,0,0,1,0,0,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,0,0,0,1,0,0,0,0,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,0,1,0,0,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "0,0,1,0,0,0,0,0,0,0")) + (rule "applyEqRigid" (formula "3") (term "0,0,1,0,0,0") (ifseqformula "1")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,1,0,0,0")) + (rule "polySimp_homoEq" (formula "3") (term "1,0,0,0")) + (rule "polySimp_mulComm0" (formula "3") (term "1,0,1,0,0,0")) + (rule "polySimp_addComm0" (formula "3") (term "1,1,0,1,0,0,0")) + (rule "polySimp_rightDist" (formula "3") (term "1,0,1,0,0,0")) + (rule "mul_literals" (formula "3") (term "0,1,0,1,0,0,0")) + (rule "polySimp_addAssoc" (formula "3") (term "0,1,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,1,0,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,1,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,0,1,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,1,0,1,0,0,0")) + (rule "add_literals" (formula "3") (term "0,1,0,1,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,1,0,0,0")) + (rule "add_literals" (formula "3") (term "0,1,0,0,0")) + (rule "eqClose" (formula "3") (term "1,0,0,0")) + (rule "concrete_and_3" (formula "3") (term "0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "3") (term "1,0,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,1,0,0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "3") (term "1,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,1,0,0,0,0,0")) + (rule "subPSeqConcat" (formula "2") (term "0")) + (rule "polySimp_elimSub" (formula "2") (term "2,1,1,0")) + (rule "polySimp_elimSub" (formula "2") (term "2,1,0")) + (rule "lenOfPSeqConcat" (formula "2") (term "1,2,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,1,2,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "0,1,2,0,0")) + (rule "add_literals" (formula "2") (term "1,2,0,0")) + (rule "lenOfPSeqConcat" (formula "2") (term "0,0,2,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,0,0,2,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "0,0,0,2,0,0")) + (rule "add_literals" (formula "2") (term "0,0,2,0,0")) + (rule "less_literals" (formula "2") (term "0,2,0,0")) + (rule "ifthenelse_true" (formula "2") (term "2,0,0")) + (rule "lenOfPSeqConcat" (formula "2") (term "1,0,1,1,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "0,1,0,1,1,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,1,0,1,1,0")) + (rule "add_literals" (formula "2") (term "1,0,1,1,0")) + (rule "less_literals" (formula "2") (term "0,1,1,0")) + (rule "ifthenelse_true" (formula "2") (term "1,1,0")) + (rule "lenOfPSeqConcat" (formula "2") (term "0,1,2,1,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "0,0,1,2,1,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,0,1,2,1,0")) + (rule "add_literals" (formula "2") (term "0,1,2,1,0")) + (rule "mul_literals" (formula "2") (term "1,2,1,0")) + (rule "add_literals" (formula "2") (term "2,1,0")) + (rule "subPSeqSingleton" (formula "2") (term "1,0")) + (rule "getOfPSeqConcat" (formula "3") (term "0,1,0,0,0")) + (rule "polySimp_elimSub" (formula "3") (term "1,2,0,1,0,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "1,0,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,0,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,1,0,0,1,0,0,0")) + (rule "add_literals" (formula "3") (term "1,0,0,1,0,0,0")) + (rule "less_literals" (formula "3") (term "0,0,1,0,0,0")) + (rule "ifthenelse_true" (formula "3") (term "0,1,0,0,0")) + (rule "getOfPSeqConcat" (formula "3") (term "0,1,0,0,0,0,0")) + (rule "polySimp_elimSub" (formula "3") (term "1,2,0,1,0,0,0,0,0")) + (rule "polySimp_addComm0" (formula "3") (term "1,2,0,1,0,0,0,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "1,0,0,1,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,0,0,1,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,1,0,0,1,0,0,0,0,0")) + (rule "add_literals" (formula "3") (term "1,0,0,1,0,0,0,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,0,1,2,0,1,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,0,1,2,0,1,0,0,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,0,0,1,2,0,1,0,0,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,1,2,0,1,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "0,1,2,0,1,0,0,0,0,0")) + (rule "getOfPSeqSingleton" (formula "3") (term "2,0,1,0,0,0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "3") (term "0,0,1,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,0,0,0,1,0,0,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,0,0,1,0,0,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "3") (term "0,2,0,1,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,2,0,1,0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "3") (term "0,0,1,0,0,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,0,1,0,0,0,0,0")) + (rule "subPSeqConcat" (formula "2") (term "0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,2,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,2,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,2,1,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "0,0,2,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "2") (term "1,0,1,1,0,0")) + (rule "sub_literals" (formula "2") (term "2,1,0,0")) + (rule "sub_literals" (formula "2") (term "2,1,1,0,0")) + (rule "ifthenelse_same_branches" (formula "2") (term "1,1,0,0")) + (rule "subPSeqSingleton" (formula "2") (term "1,0,0")) + (rule "less_literals" (formula "2") (term "0,2,0,0,0")) + (rule "ifthenelse_true" (formula "2") (term "2,0,0,0")) + (rule "subPSeqEmpty" (formula "2") (term "0,0,0")) + (rule "pseqConcatWithPSeqEmpty2" (formula "2") (term "0,0")) + (rule "eqSymm" (formula "2")) + (rule "applyEq" (formula "3") (term "0,0,1,0,0") (ifseqformula "2")) + (rule "getOfPSeqConcat" (formula "3") (term "0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,2,0,1,0,0,0")) + (rule "less_literals" (formula "3") (term "0,0,1,0,0,0")) + (rule "ifthenelse_false" (formula "3") (term "0,1,0,0,0")) + (rule "sub_literals" (formula "3") (term "1,0,1,0,0,0")) + (rule "getOfPSeqSingletonConcrete" (formula "3") (term "0,1,0,0,0")) + (rule "eqClose" (formula "3") (term "1,0,0,0")) + (rule "concrete_and_3" (formula "3") (term "0,0,0")) + (rule "getOfPSeqConcat" (formula "3") (term "0,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,0,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,2,0,1,0,0")) + (rule "less_literals" (formula "3") (term "0,0,1,0,0")) + (rule "ifthenelse_false" (formula "3") (term "0,1,0,0")) + (rule "sub_literals" (formula "3") (term "1,0,1,0,0")) + (rule "getOfPSeqSingletonConcrete" (formula "3") (term "0,1,0,0")) + (rule "eqClose" (formula "3") (term "1,0,0")) + (rule "concrete_and_3" (formula "3") (term "0,0")) + (rule "getOfPSeqConcat" (formula "3") (term "1,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,1,0,1,0,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,2,1,0,1,0,0,0")) + (rule "polySimp_elimSub" (formula "3") (term "1,2,1,0,1,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,1,2,1,0,1,0,0,0")) + (rule "polySimp_addComm0" (formula "3") (term "1,2,1,0,1,0,0,0")) + (rule "getOfPSeqSingleton" (formula "3") (term "1,1,0,1,0,0,0")) + (rule "getOfPSeqSingleton" (formula "3") (term "2,1,0,1,0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "3") (term "0,1,0,1,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,0,0,1,0,1,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,0,1,0,1,0,0,0")) + (rule "add_zero_left" (formula "3") (term "0,0,1,0,1,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "3") (term "0,2,1,0,1,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,2,1,0,1,0,0,0")) + (rule "all_unused" (formula "3") (term "1")) + (rule "concrete_and_3" (formula "3")) + (rule "nnf_imp2or" (formula "3") (term "0,0")) + (rule "nnf_notAnd" (formula "3") (term "0,0,0")) + (rule "inEqSimp_notGeq" (formula "3") (term "0,0,0,0")) + (rule "times_zero_1" (formula "3") (term "1,0,0,0,0,0,0")) + (rule "add_zero_right" (formula "3") (term "0,0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "3") (term "0,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,0,0,0")) + (rule "inEqSimp_notLeq" (formula "3") (term "1,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,0,1,0,0,0")) + (rule "add_literals" (formula "3") (term "0,0,1,0,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "3") (term "1,0,0,0")) + (rule "mul_literals" (formula "3") (term "1,1,0,0,0")) + (rule "cut_direct" (formula "3") (term "1")) + (branch "CUT: pseqReverse(pseqConcat(pseqConcat(pseqSingleton(54), pseqSingleton(4)), pseqSingleton(100))) = pseqConcat(pseqConcat(pseqSingleton(100), pseqSingleton(4)), pseqSingleton(54)) TRUE" + (rule "concrete_and_3" (formula "4")) + (rule "allRight" (formula "4") (inst "sk=i_0")) + (rule "orRight" (formula "4")) + (rule "orRight" (formula "4")) + (rule "inEqSimp_geqRight" (formula "6")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_geqRight" (formula "6")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "inEqSimp_leqRight" (formula "6")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_sepPosMonomial0" (formula "2")) + (rule "mul_literals" (formula "2") (term "1")) + (rule "ifthenelse_split" (formula "3") (term "0")) + (branch "i_0 <= 1 TRUE" + (rule "ifthenelse_split" (formula "4") (term "0")) + (branch "i_0 <= 0 TRUE" + (rule "inEqSimp_antiSymm" (formula "1") (ifseqformula "4")) + (rule "replace_known_left" (formula "6") (term "0,0") (ifseqformula "1")) + (rule "ifthenelse_true" (formula "6") (term "0")) + (rule "leq_literals" (formula "6")) + (rule "closeFalse" (formula "6")) + ) + (branch "i_0 <= 0 FALSE" + (rule "inEqSimp_leqRight" (formula "8")) + (rule "times_zero_1" (formula "1") (term "1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "inEqSimp_antiSymm" (formula "1") (ifseqformula "4")) + (rule "replace_known_left" (formula "6") (term "0,0") (ifseqformula "1")) + (rule "ifthenelse_true" (formula "6") (term "0")) + (rule "leq_literals" (formula "6")) + (rule "closeFalse" (formula "6")) + ) + ) + (branch "i_0 <= 1 FALSE" + (rule "inEqSimp_leqRight" (formula "7")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "inEqSimp_antiSymm" (formula "1") (ifseqformula "3")) + (rule "replace_known_left" (formula "5") (term "0,0") (ifseqformula "1")) + (rule "ifthenelse_true" (formula "5") (term "0")) + (rule "leq_literals" (formula "5")) + (rule "closeFalse" (formula "5")) + ) + ) + (branch "b" + (rule "equalityToPSeqGetAndPSeqLenRight" (formula "3") (inst "iv=iv")) + (rule "lenOfPSeqReverse" (formula "3") (term "1,1,0,0,1")) + (rule "lenOfPSeqConcat" (formula "3") (term "1,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,0")) + (rule "polySimp_addComm0" (formula "3") (term "1,0")) + (rule "lenOfPSeqReverse" (formula "3") (term "0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "1,1,0,0,1")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,1,0,0,1")) + (rule "polySimp_addComm0" (formula "3") (term "1,1,0,0,1")) + (rule "lenOfPSeqConcat" (formula "3") (term "1,1,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,1,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,1,1,0")) + (rule "add_literals" (formula "3") (term "1,1,0")) + (rule "add_literals" (formula "3") (term "1,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,0")) + (rule "polySimp_homoEq" (formula "3") (term "0")) + (rule "polySimp_mulComm0" (formula "3") (term "1,0,0")) + (rule "polySimp_addComm0" (formula "3") (term "1,1,0,0")) + (rule "polySimp_rightDist" (formula "3") (term "1,0,0")) + (rule "mul_literals" (formula "3") (term "0,1,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "1,1,1,0,0,1")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,1,1,1,0,0,1")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,1,1,1,0,0,1")) + (rule "add_literals" (formula "3") (term "1,1,1,0,0,1")) + (rule "add_literals" (formula "3") (term "1,1,0,0,1")) + (rule "polySimp_addAssoc" (formula "3") (term "0,0")) + (rule "add_literals" (formula "3") (term "0,0,0")) + (rule "lenOfPSeqConcat" (formula "3") (term "0,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "1,0,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "3") (term "0,0,1,0,0")) + (rule "add_literals" (formula "3") (term "0,1,0,0")) + (rule "mul_literals" (formula "3") (term "1,0,0")) + (rule "add_literals" (formula "3") (term "0,0")) + (rule "eqClose" (formula "3") (term "0")) + (rule "concrete_and_1" (formula "3")) + (rule "allRight" (formula "3") (inst "sk=iv_0")) + (rule "impRight" (formula "3")) + (rule "andLeft" (formula "1")) + (rule "inEqSimp_ltToLeq" (formula "2")) + (rule "mul_literals" (formula "2") (term "1,0,0")) + (rule "add_literals" (formula "2") (term "0,0")) + (rule "inEqSimp_commuteLeq" (formula "1")) + (rule "inEqSimp_sepPosMonomial0" (formula "2")) + (rule "mul_literals" (formula "2") (term "1")) + (rule "getOfPSeqConcat" (formula "5") (term "1")) + (rule "eqSymm" (formula "5")) + (rule "polySimp_elimSub" (formula "5") (term "1,2,0")) + (rule "lenOfPSeqConcat" (formula "5") (term "1,0,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "0,1,0,0")) + (rule "add_literals" (formula "5") (term "1,0,0")) + (rule "getOfPSeqSingleton" (formula "5") (term "2,0")) + (rule "lenOfPSeqConcat" (formula "5") (term "0,1,0,0,2,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,0,1,0,0,2,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "0,0,1,0,0,2,0")) + (rule "add_literals" (formula "5") (term "0,1,0,0,2,0")) + (rule "mul_literals" (formula "5") (term "1,0,0,2,0")) + (rule "polySimp_addComm0" (formula "5") (term "0,0,2,0")) + (rule "inEqSimp_ltToLeq" (formula "5") (term "0,0")) + (rule "mul_literals" (formula "5") (term "1,0,0,0,0")) + (rule "add_literals" (formula "5") (term "0,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "5") (term "0,2,0")) + (rule "mul_literals" (formula "5") (term "1,0,2,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "5") (term "0,0")) + (rule "mul_literals" (formula "5") (term "1,0,0")) + (rule "getOfPSeqConcat" (formula "5") (term "1,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,0,1,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,1,2,1,0")) + (rule "polySimp_elimSub" (formula "5") (term "1,2,1,0")) + (rule "mul_literals" (formula "5") (term "1,1,2,1,0")) + (rule "polySimp_addComm0" (formula "5") (term "1,2,1,0")) + (rule "getOfPSeqSingleton" (formula "5") (term "1,1,0")) + (rule "getOfPSeqSingleton" (formula "5") (term "2,1,0")) + (rule "inEqSimp_ltToLeq" (formula "5") (term "0,1,0")) + (rule "mul_literals" (formula "5") (term "1,0,0,0,1,0")) + (rule "add_literals" (formula "5") (term "0,0,0,1,0")) + (rule "add_zero_left" (formula "5") (term "0,0,1,0")) + (rule "polySimp_sepPosMonomial" (formula "5") (term "0,2,1,0")) + (rule "mul_literals" (formula "5") (term "1,0,2,1,0")) + (rule "getOfPSeqReverse" (formula "5") (term "1")) + (rule "polySimp_elimSub" (formula "5") (term "0,1,1")) + (rule "mul_literals" (formula "5") (term "1,0,1,1")) + (rule "polySimp_elimSub" (formula "5") (term "1,1")) + (rule "polySimp_addComm0" (formula "5") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "5") (term "1,1")) + (rule "lenOfPSeqConcat" (formula "5") (term "1,1,1")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,1,1,1")) + (rule "polySimp_addComm0" (formula "5") (term "1,1,1")) + (rule "polySimp_addAssoc" (formula "5") (term "1,1")) + (rule "polySimp_addComm1" (formula "5") (term "0,1,1")) + (rule "add_literals" (formula "5") (term "0,0,1,1")) + (rule "add_zero_left" (formula "5") (term "0,1,1")) + (rule "lenOfPSeqConcat" (formula "5") (term "1,1,1")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,1,1,1")) + (rule "lenOfPSeqSingleton" (formula "5") (term "0,1,1,1")) + (rule "add_literals" (formula "5") (term "1,1,1")) + (rule "polySimp_addComm0" (formula "5") (term "1,1")) + (rule "getOfPSeqConcat" (formula "5") (term "1")) + (rule "eqSymm" (formula "5")) + (rule "polySimp_elimSub" (formula "5") (term "1,2,0")) + (rule "lenOfPSeqConcat" (formula "5") (term "1,0,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "0,1,0,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,1,0,0")) + (rule "add_literals" (formula "5") (term "1,0,0")) + (rule "getOfPSeqSingleton" (formula "5") (term "2,0")) + (rule "lenOfPSeqConcat" (formula "5") (term "0,1,0,0,2,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "0,0,1,0,0,2,0")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,0,1,0,0,2,0")) + (rule "add_literals" (formula "5") (term "0,1,0,0,2,0")) + (rule "mul_literals" (formula "5") (term "1,0,0,2,0")) + (rule "polySimp_addComm1" (formula "5") (term "0,0,2,0")) + (rule "add_literals" (formula "5") (term "0,0,0,2,0")) + (rule "add_zero_left" (formula "5") (term "0,0,2,0")) + (rule "inEqSimp_ltToLeq" (formula "5") (term "0,0")) + (rule "mul_literals" (formula "5") (term "1,0,0,0,0")) + (rule "add_literals" (formula "5") (term "0,0,0,0")) + (rule "polySimp_addAssoc" (formula "5") (term "0,0,0")) + (rule "add_literals" (formula "5") (term "0,0,0,0")) + (rule "polySimp_invertEq" (formula "5") (term "0,2,0")) + (rule "times_zero_2" (formula "5") (term "1,0,2,0")) + (rule "polySimp_mulLiterals" (formula "5") (term "0,0,2,0")) + (rule "polySimp_elimOne" (formula "5") (term "0,0,2,0")) + (rule "inEqSimp_sepNegMonomial0" (formula "5") (term "0,0")) + (rule "polySimp_mulLiterals" (formula "5") (term "0,0,0")) + (rule "eqSymm" (formula "5")) + (rule "polySimp_elimOne" (formula "5") (term "0,0,1")) + (rule "getOfPSeqConcat" (formula "5") (term "1,1")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,0,1,1")) + (rule "lenOfPSeqSingleton" (formula "5") (term "1,1,2,1,1")) + (rule "eqSymm" (formula "5")) + (rule "polySimp_elimSub" (formula "5") (term "1,2,1,0")) + (rule "mul_literals" (formula "5") (term "1,1,2,1,0")) + (rule "polySimp_addComm1" (formula "5") (term "1,2,1,0")) + (rule "add_literals" (formula "5") (term "0,1,2,1,0")) + (rule "getOfPSeqSingleton" (formula "5") (term "1,1,0")) + (rule "getOfPSeqSingleton" (formula "5") (term "2,1,0")) + (rule "inEqSimp_ltToLeq" (formula "5") (term "0,1,0")) + (rule "mul_literals" (formula "5") (term "1,0,0,0,1,0")) + (rule "add_literals" (formula "5") (term "0,0,0,1,0")) + (rule "add_zero_left" (formula "5") (term "0,0,1,0")) + (rule "polySimp_sepNegMonomial" (formula "5") (term "0,1,1,0")) + (rule "polySimp_mulLiterals" (formula "5") (term "0,0,1,1,0")) + (rule "polySimp_elimOne" (formula "5") (term "0,0,1,1,0")) + (rule "polySimp_sepNegMonomial" (formula "5") (term "0,2,1,0")) + (rule "polySimp_mulLiterals" (formula "5") (term "0,0,2,1,0")) + (rule "polySimp_elimOne" (formula "5") (term "0,0,2,1,0")) + (rule "inEqSimp_sepNegMonomial0" (formula "5") (term "0,1,0")) + (rule "polySimp_mulLiterals" (formula "5") (term "0,0,1,0")) + (rule "eqSymm" (formula "5")) + (rule "polySimp_elimOne" (formula "5") (term "0,0,1,1")) + (rule "ifthenelse_split" (formula "5") (term "2,0")) + (branch "iv_0 = 2 TRUE" + (rule "replace_known_left" (formula "6") (term "0,1,1,1") (ifseqformula "1")) + (rule "ifthenelse_true" (formula "6") (term "1,1,1")) + (rule "applyEqRigid" (formula "6") (term "0,0,2,1,0") (ifseqformula "1")) + (rule "equal_literals" (formula "6") (term "0,2,1,0")) + (rule "ifthenelse_false" (formula "6") (term "2,1,0")) + (rule "applyEq" (formula "6") (term "0,0,0") (ifseqformula "1")) + (rule "leq_literals" (formula "6") (term "0,0")) + (rule "ifthenelse_false" (formula "6") (term "0")) + (rule "eqSymm" (formula "6")) + (rule "ifEqualsInteger" (formula "6")) + (rule "ifthenelse_concrete3" (formula "6") (term "1,0")) + (rule "orRight" (formula "6")) + (rule "ifEqualsInteger" (formula "6") (term "1,1")) + (rule "equal_literals" (formula "6") (term "1,0,1,1")) + (rule "concrete_and_4" (formula "6") (term "0,1,1")) + (rule "concrete_or_2" (formula "6") (term "1,1")) + (rule "applyEq" (formula "6") (term "0,0,0,1,1") (ifseqformula "1")) + (rule "equal_literals" (formula "6") (term "0,0,1,1")) + (rule "concrete_not_2" (formula "6") (term "0,1,1")) + (rule "concrete_and_1" (formula "6") (term "1,1")) + (rule "applyEq" (formula "6") (term "0,0,1") (ifseqformula "1")) + (rule "qeq_literals" (formula "6") (term "0,1")) + (rule "concrete_or_1" (formula "6") (term "1")) + (rule "concrete_and_3" (formula "6")) + (rule "inEqSimp_geqRight" (formula "6")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "2")) + (rule "leq_literals" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "iv_0 = 2 FALSE" + (rule "replace_known_right" (formula "6") (term "0,1,1,1") (ifseqformula "5")) + (rule "ifthenelse_false" (formula "6") (term "1,1,1")) + (rule "inEqSimp_strengthen0" (formula "2") (ifseqformula "5")) + (rule "add_literals" (formula "2") (term "1")) + (rule "replace_known_left" (formula "6") (term "0,0") (ifseqformula "2")) + (rule "ifthenelse_true" (formula "6") (term "0")) + (rule "inEqSimp_contradInEq0" (formula "6") (term "0,1,1") (ifseqformula "2")) + (rule "qeq_literals" (formula "6") (term "0,0,1,1")) + (rule "concrete_and_2" (formula "6") (term "0,1,1")) + (rule "ifthenelse_false" (formula "6") (term "1,1")) + (rule "ifthenelse_split" (formula "6") (term "2,1")) + (branch "iv_0 = 0 TRUE" + (rule "replace_known_left" (formula "7") (term "0,1,0") (ifseqformula "1")) + (rule "ifthenelse_true" (formula "7") (term "1,0")) + (rule "applyEqRigid" (formula "7") (term "0,0,2,0") (ifseqformula "1")) + (rule "equal_literals" (formula "7") (term "0,2,0")) + (rule "ifthenelse_false" (formula "7") (term "2,0")) + (rule "applyEq" (formula "7") (term "0,0,0") (ifseqformula "1")) + (rule "leq_literals" (formula "7") (term "0,0")) + (rule "ifthenelse_true" (formula "7") (term "0")) + (rule "eqSymm" (formula "7")) + (rule "ifthenelse_concrete4" (formula "7")) + (rule "orRight" (formula "7")) + (rule "notRight" (formula "7")) + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "2")) + (rule "qeq_literals" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch "iv_0 = 0 FALSE" + (rule "replace_known_right" (formula "7") (term "0,1,0") (ifseqformula "6")) + (rule "ifthenelse_false" (formula "7") (term "1,0")) + (rule "inEqSimp_strengthen1" (formula "1") (ifseqformula "6")) + (rule "add_zero_right" (formula "1") (term "1")) + (rule "replace_known_left" (formula "7") (term "0,1") (ifseqformula "1")) + (rule "ifthenelse_true" (formula "7") (term "1")) + (rule "ifthenelse_concrete4" (formula "7")) + (rule "orRight" (formula "7")) + (rule "notRight" (formula "7")) + (rule "eqSymm" (formula "8")) + (rule "ifthenelse_concrete4" (formula "8")) + (rule "orRight" (formula "8")) + (rule "notRight" (formula "8")) + (rule "applyEqRigid" (formula "2") (term "0") (ifseqformula "1")) + (rule "leq_literals" (formula "2")) + (rule "closeFalse" (formula "2")) + ) + ) + ) + ) } \ No newline at end of file From 2071d1296436fd9b41b934d0e112ac6ce8bf2047 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 14 Aug 2025 12:12:30 +0200 Subject: [PATCH 05/13] Spotless --- .../de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java | 3 ++- .../match/vm/instructions/MatchGenericSortInstruction.java | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java index af61c8f2217..76046826577 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java @@ -119,7 +119,8 @@ public int getChildCount() { @Override public boolean equals(Object o) { - if (o == null || getClass() != o.getClass()) return false; + if (o == null || getClass() != o.getClass()) + return false; ParametricFunctionInstance that = (ParametricFunctionInstance) o; return Objects.equals(args, that.args) && Objects.equals(base, that.base); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java index 27ded81f5cb..d748d9a443c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java @@ -60,7 +60,8 @@ public MatchResultInfo match(SyntaxElement actualElement, MatchResultInfo mc, if (actualElement instanceof GenericArgument(Sort sort)) { return matchSorts(sort, mc, services); } - if (actualElement instanceof QualifierWrapper w && w.getQualifier() instanceof Sort sort) { + if (actualElement instanceof QualifierWrapper w + && w.getQualifier() instanceof Sort sort) { return matchSorts(sort, mc, services); } return null; From 46f7c7a0a390883a966ab550208290b0764fa3df Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 24 Sep 2025 21:48:06 +0200 Subject: [PATCH 06/13] Prepare datatype handling --- .../de/uka/ilkd/key/logic/op/SubstOp.java | 3 +- .../builder/FunctionPredicateBuilder.java | 68 +++++++++++++---- .../key/nparser/builder/TacletPBuilder.java | 74 +++++++++++++------ .../standard_key/adt/dt_polymorphic.key | 66 +++++++++++++++++ key.ui/examples/standard_key/adt/list.key | 3 - 5 files changed, 176 insertions(+), 38 deletions(-) create mode 100644 key.ui/examples/standard_key/adt/dt_polymorphic.key diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java index a7add6cdc6d..ada6ed42c83 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java @@ -8,6 +8,7 @@ import org.key_project.logic.Name; import org.key_project.logic.SyntaxElement; +import org.key_project.logic.Term; import org.key_project.logic.TermCreationException; import org.key_project.logic.op.AbstractOperator; import org.key_project.logic.op.Operator; @@ -48,7 +49,7 @@ public Sort sort(Sort[] sorts) { * @throws TermCreationException if the check fails */ @Override - public void validTopLevelException(T term) + public void validTopLevelException(T term) throws TermCreationException { super.validTopLevelException(term); if (term.varsBoundHere(1).size() != 1) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index f5bbbd7aa99..0c88affe11d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java @@ -7,13 +7,12 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.ldt.JavaDLTheory; +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.logic.op.JFunction; -import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; -import de.uka.ilkd.key.logic.op.SortDependingFunction; -import de.uka.ilkd.key.logic.op.Transformer; +import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.nparser.KeYParser; import org.key_project.logic.Name; @@ -24,6 +23,8 @@ import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.NonNull; + /** * This visitor evaluates all secondary (level 1) declarations. This includes: @@ -58,8 +59,25 @@ public Object visitDecls(KeYParser.DeclsContext ctx) { public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { // weigl: all datatypes are free ==> functions are unique! // boolean freeAdt = ctx.FREE() != null; - var sort = sorts().lookup(ctx.name.getText()); - var dtNamespace = new Namespace(); + Sort sort; + var dtFnNamespace = new Namespace<@NonNull Function>(); + var dtPfnNamespace = new Namespace<@NonNull ParametricFunctionDecl>(); + ImmutableList genericParams; + if (sorts().lookup(ctx.name.getText()) == null) { + // Is polymorphic + var psd = namespaces().parametricSorts().lookup(ctx.name.getText()); + assert psd != null; + genericParams = psd.getParameters(); + ImmutableList args = ImmutableList.of(); + for (int i = psd.getParameters().size() - 1; i >= 0; i--) { + var param = psd.getParameters().get(i); + args = args.prepend(new GenericArgument(param.sort())); + } + sort = ParametricSortInstance.get(psd, args); + } else { + sort = sorts().lookup(ctx.name.getText()); + genericParams = null; + } for (KeYParser.Datatype_constructorContext constructorContext : ctx .datatype_constructor()) { Name name = new Name(constructorContext.name.getText()); @@ -69,13 +87,20 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { Sort argSort = accept(constructorContext.sortId(i)); args[i] = argSort; var argName = argNames.get(i).getText(); - SortedOperator alreadyDefinedFn = dtNamespace.lookup(argName); + SortedOperator alreadyDefinedFn = dtFnNamespace.lookup(argName); if (alreadyDefinedFn == null) { alreadyDefinedFn = namespaces().functions().lookup(argName); } if (alreadyDefinedFn == null) { alreadyDefinedFn = namespaces().programVariables().lookup(argName); } + if (alreadyDefinedFn == null) { + var alreadyDefinedPfn = dtPfnNamespace.lookup(argName); + if (alreadyDefinedPfn != null) { + alreadyDefinedFn = ParametricFunctionInstance.get(alreadyDefinedPfn, + ImmutableList.of(new GenericArgument(sort))); + } + } if (alreadyDefinedFn != null && (!alreadyDefinedFn.sort().equals(argSort) || !alreadyDefinedFn.argSorts().equals(ImmutableList.of(sort)))) { @@ -89,14 +114,31 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { ". Identifiers in datatype definitions must be unique (also wrt. global functions).", argName); } - Function fn = new JFunction(new Name(argName), argSort, new Sort[] { sort }, null, - false, false); - dtNamespace.add(fn); + if (genericParams == null) { + Function fn = + new JFunction(new Name(argName), argSort, new Sort[] { sort }, null, + false, false); + dtFnNamespace.add(fn); + } else { + var fn = new ParametricFunctionDecl(new Name(argName), genericParams, + new ImmutableArray<>(sort), argSort, null, false, true, false); + dtPfnNamespace.add(fn); + } + } + if (genericParams == null) { + var fn = new JFunction(name, sort, args, null, true, false); + functions().addSafely(fn); + } else { + var fn = new ParametricFunctionDecl(name, genericParams, new ImmutableArray<>(args), + sort, null, true, true, false); + namespaces().parametricFunctions().add(fn); } - Function function = new JFunction(name, sort, args, null, true, false); - namespaces().functions().addSafely(function); } - namespaces().functions().addSafely(dtNamespace.allElements()); + if (genericParams != null) { + namespaces().parametricFunctions().addSafely(dtPfnNamespace.allElements()); + } else { + namespaces().functions().addSafely(dtFnNamespace.allElements()); + } return null; } 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 94649b7d653..a3e5af2d340 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 @@ -31,6 +31,7 @@ import org.key_project.logic.ChoiceExpr; import org.key_project.logic.Name; import org.key_project.logic.Namespace; +import org.key_project.logic.op.Function; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; @@ -250,24 +251,38 @@ private TacletBuilder peekTBuilder() { @Override public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { - var tbAx = createAxiomTaclet(ctx); + var genParams = ctx.formal_sort_param_decls() == null ? null + : visitFormal_sort_param_decls(ctx.formal_sort_param_decls()); + final Sort sort; + if (genParams != null) { + var psd = namespaces().parametricSorts().lookup(ctx.name.getText()); + assert psd != null; + ImmutableList args = ImmutableSLList.nil(); + for (int i = psd.getParameters().size() - 1; i >= 0; i--) { + args = args.prepend(new GenericArgument(psd.getParameters().get(i).sort())); + } + sort = ParametricSortInstance.get(psd, args); + } else { + sort = sorts().lookup(ctx.name.getText()); + } + + var tbAx = createAxiomTaclet(ctx, sort); registerTaclet(ctx, tbAx); - var tbInd = createInductionTaclet(ctx); + var tbInd = createInductionTaclet(ctx, sort); registerTaclet(ctx, tbInd); - var tbSplit = createConstructorSplit(ctx); + var tbSplit = createConstructorSplit(ctx, sort); registerTaclet(ctx, tbSplit); - Sort dtSort = namespaces().sorts().lookup(ctx.name.getText()); for (var constructor : ctx.datatype_constructor()) { for (int i = 0; i < constructor.sortId().size(); i++) { var argName = constructor.argName.get(i).getText(); - var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i, dtSort); + var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i, sort); registerTaclet(ctx, tbDeconstructor); - var tbDeconsEq = createDeconstructorEQTaclet(constructor, argName, i, dtSort); + var tbDeconsEq = createDeconstructorEQTaclet(constructor, argName, i, sort); registerTaclet(ctx, tbDeconsEq); } } @@ -300,8 +315,8 @@ private TacletBuilder createDeconstructorTaclet( args[i] = tb.var(sv); } - var function = namespaces().functions().lookup(argName); - var consFn = namespaces().functions().lookup(constructor.name.getText()); + var function = getPossiblyParametricFunction(argName, dtSort); + var consFn = getPossiblyParametricFunction(constructor.name.getText(), dtSort); // Find, e.g, tail(Cons(head_sv, tail_sv)) tacletBuilder.setFind(tb.func(function, tb.func(consFn, args))); @@ -339,8 +354,8 @@ private TacletBuilder createDeconstructorEQTaclet( args[i] = tb.var(sv); } - var function = namespaces().functions().lookup(argName); - var consFn = namespaces().functions().lookup(constructor.name.getText()); + var function = getPossiblyParametricFunction(argName, dtSort); + var consFn = getPossiblyParametricFunction(constructor.name.getText(), dtSort); var x = declareSchemaVariable(constructor, argName + "_x", dtSort, false, false, false, new SchemaVariableModifierSet.TermSV()); @@ -358,11 +373,29 @@ private TacletBuilder createDeconstructorEQTaclet( return tacletBuilder; } + private Function getPossiblyParametricFunction(String name, Sort sort) { + var fn = functions().lookup(name); + if (fn != null) + return fn; + var psi = (ParametricSortInstance) sort; + var pfn = namespaces().parametricFunctions().lookup(name); + assert pfn != null; + return ParametricFunctionInstance.get(pfn, psi.getArgs()); + } + + private Sort getPossiblyParametricSort(String name, Sort sort) { + var s = sorts().lookup(name); + if (s != null) + return s; + var psi = (ParametricSortInstance) sort; + var ps = namespaces().parametricSorts().lookup(name); + assert ps != null; + return ParametricSortInstance.get(ps, psi.getArgs()); + } private TacletBuilder createInductionTaclet( - KeYParser.Datatype_declContext ctx) { + KeYParser.Datatype_declContext ctx, Sort sort) { var tacletBuilder = new NoFindTacletBuilder(); - final var sort = sorts().lookup(ctx.name.getText()); var phi = declareSchemaVariable(ctx, "phi", JavaDLTheory.FORMULA, true, false, false, new SchemaVariableModifierSet.FormulaSV()); var tb = services.getTermBuilder(); @@ -401,9 +434,8 @@ private TacletGoalTemplate createGoalDtConstructor(KeYParser.Datatype_constructo private TacletBuilder createAxiomTaclet( - KeYParser.Datatype_declContext ctx) { + KeYParser.Datatype_declContext ctx, Sort sort) { var tacletBuilder = new NoFindTacletBuilder(); - final var sort = sorts().lookup(ctx.name.getText()); var phi = declareSchemaVariable(ctx, "phi", JavaDLTheory.FORMULA, true, false, false, new SchemaVariableModifierSet.FormulaSV()); var tb = services.getTermBuilder(); @@ -432,7 +464,7 @@ private TacletBuilder createAxiomTaclet( private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext context, QuantifiableVariable qvX, JTerm phi, Sort dt) { var tb = services.getTermBuilder(); - var fn = functions().lookup(context.name.getText()); + var fn = getPossiblyParametricFunction(context.name.getText(), dt); if (context.argName.isEmpty()) return tb.subst(qvX, tb.func(fn), phi); @@ -440,7 +472,7 @@ private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext cont var argSort = context.argSort.stream() - .map(it -> sorts().lookup(it.getText())) + .map(it -> getPossiblyParametricSort(it.simple_ident_dots().getText(), dt)) .toList(); var argNames = context.argName.stream() @@ -468,7 +500,7 @@ private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext cont } private RewriteTacletBuilder createConstructorSplit( - KeYParser.Datatype_declContext ctx) { + KeYParser.Datatype_declContext ctx, Sort sort) { final var tb = services.getTermBuilder(); final String prefix = ctx.name.getText() + "_"; @@ -477,8 +509,9 @@ private RewriteTacletBuilder createConstructorSplit( for (KeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { for (int i = 0; i < context.argName.size(); i++) { var name = context.argName.get(i).getText(); - var sort = sorts().lookup(context.argSort.get(i).getText()); - var sv = declareSchemaVariable(ctx, prefix + name, sort, + var argSort = getPossiblyParametricSort( + context.argSort.get(i).simple_ident_dots().getText(), sort); + var sv = declareSchemaVariable(ctx, prefix + name, argSort, false, true, false, new SchemaVariableModifierSet.TermSV()); variables.put(name, tb.var(sv)); @@ -488,7 +521,6 @@ private RewriteTacletBuilder createConstructorSplit( final var b = new RewriteTacletBuilder<>(); b.setApplicationRestriction( new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL)); - final var sort = sorts().lookup(ctx.name.getText()); b.setName(new Name("DT_" + sort.name() + "_ctor_split")); b.setDisplayName(String.format("DT %s case distinction ", sort.name())); @@ -498,7 +530,7 @@ private RewriteTacletBuilder createConstructorSplit( new SchemaVariableModifierSet.TermSV()); b.setFind(tb.var(phi)); for (KeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { - var func = functions().lookup(context.name.getText()); + var func = getPossiblyParametricFunction(context.name.getText(), sort); JTerm[] args = new JTerm[context.argName.size()]; for (int i = 0; i < args.length; i++) { args[i] = variables.get(context.argName.get(i).getText()); diff --git a/key.ui/examples/standard_key/adt/dt_polymorphic.key b/key.ui/examples/standard_key/adt/dt_polymorphic.key new file mode 100644 index 00000000000..fb0e4b1fc13 --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.key @@ -0,0 +1,66 @@ +// In this example, the abstract polymorphic data type list is defined. The ADT has +// the constructors "nil" and "cons". The proof obligations states that +// a function "rev" really has the intended behaviour, namely to revert a +// list. To succesfully finish the proof several lemmata have to be proven +// as subgoals (currently the lemmata have to be introduced by cuts): + +// 1. \forall List<[E]> l1;\forall List<[E]> l2;( rev<[E]>(app<[E]>(l1,l2))=app<[E]>(rev<[E]>(l2),rev<[E]>(l1)) ) +// 2. \forall List<[E]> l;( app<[E]>(l,nil<[E]>)=l ) +// 3. \forall List<[E]> l1;\forall List<[E]> l2;\forall List<[E]> l3;( app<[E]>(l1,app<[E]>(l2,l3))=app<[E]>(app<[E]>(l1,l2),l3) ) + +// This example is taken from an introduction to Isabelle/HOL. You can +// find the relevant pages describing the proof in file isabelleTutorial.ps.gz. +// Take a look at it if you get stuck in the proof. + +\heuristicsDecl { + LIST; +} + +\sorts { + \generic E; + S; +} + +\datatypes { + List<[E]> = Nil | Cons(E head, List<[E]> tail); +} + +\predicates { + contains<[E]>(E, List<[E]>); +} + +\functions{ + // append to lists + List<[E]> app<[E]>(List<[E]>, List<[E]>); + // revert a list + List<[E]> rev<[E]>(List<[E]>); +} + +\schemaVariables { + \term List<[E]> list, list1; + \term E e; + \variables List<[E]> nv; + \variables E el; + \formula b; +} + +\rules { + // axioms + concat_base{ + \find (app<[E]>(Nil<[E]>, list)) + \replacewith (list) + \heuristics (LIST) + }; + concat_step{ + \find( app<[E]>(Cons<[E]>(e, list1), list) ) + \replacewith (Cons<[E]>(e, app<[E]>(list1,list) )) + \heuristics (LIST)}; + + // definition of revert + revert_base {\find (rev<[E]>(Nil<[E]>)) \replacewith(Nil<[E]>) }; + revert_step {\find (rev<[E]>(Cons<[E]>(e,list))) \replacewith (app<[E]>(rev<[E]>(list),Cons<[E]>(e,Nil<[E]>)))}; +} + +\problem { + \forall List<[S]> l;( app<[S]>(l,Nil<[S]>)=l ) +} \ No newline at end of file diff --git a/key.ui/examples/standard_key/adt/list.key b/key.ui/examples/standard_key/adt/list.key index 0f1bf6a34f7..8998d0703b5 100644 --- a/key.ui/examples/standard_key/adt/list.key +++ b/key.ui/examples/standard_key/adt/list.key @@ -38,8 +38,6 @@ List rev(List); } - - \schemaVariables { \term List list, list1; \term Element e; @@ -48,7 +46,6 @@ \formula b; } - \rules { // axioms concat_base{ From 4f540f58ed9dd280717f9ac31b6733809018409e Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 25 Sep 2025 10:56:28 +0200 Subject: [PATCH 07/13] Fix taclets for datatypes w/ polymorphic params --- .../key/control/AbstractProofControl.java | 13 +- .../instantiation_model/TacletFindModel.java | 2 - .../uka/ilkd/key/logic/GenericArgument.java | 2 +- .../uka/ilkd/key/logic/op/LogicVariable.java | 4 + .../logic/op/ParametricFunctionInstance.java | 18 +- .../key/logic/op/SortDependingFunction.java | 19 ++- .../logic/sort/ParametricSortInstance.java | 42 +++-- .../key/nparser/builder/DefaultBuilder.java | 4 +- .../builder/FunctionPredicateBuilder.java | 9 +- .../key/nparser/builder/TacletPBuilder.java | 54 ++++-- .../java/de/uka/ilkd/key/pp/NotationInfo.java | 7 + .../de/uka/ilkd/key/proof/TacletIndex.java | 2 + .../key/rule/SyntacticalReplaceVisitor.java | 4 +- .../java/de/uka/ilkd/key/rule/TacletApp.java | 3 +- .../key/rule/conditions/TypeResolver.java | 2 +- .../rule/inst/GenericSortInstantiations.java | 27 ++- .../proof/runallproofs/ProofCollections.java | 1 + .../standard_key/adt/dt_polymorphic.key | 1 + .../standard_key/adt/dt_polymorphic.proof | 159 ++++++++++++++++++ 19 files changed, 302 insertions(+), 71 deletions(-) create mode 100644 key.ui/examples/standard_key/adt/dt_polymorphic.proof diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index ad0cfa1f370..7313aab4618 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.prover.impl.ApplyStrategy; import de.uka.ilkd.key.rule.*; +import de.uka.ilkd.key.rule.inst.GenericSortException; import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager; import de.uka.ilkd.key.strategy.FocussedRuleApplicationManager; @@ -215,12 +216,14 @@ public boolean selectedTaclet(ImmutableSet applics, Goal goal) { ifSeqInteraction = false; firstApp = ifSeqCandidates.head(); } - TacletApp tmpApp = - firstApp.tryToInstantiate(services.getOverlay(goal.getLocalNamespaces())); - if (tmpApp != null) { - firstApp = tmpApp; + try { + TacletApp tmpApp = + firstApp.tryToInstantiate(services.getOverlay(goal.getLocalNamespaces())); + if (tmpApp != null) { + firstApp = tmpApp; + } + } catch (GenericSortException ge) { } - } if (ifSeqInteraction || !firstApp.complete()) { LinkedList l = new LinkedList<>(); 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 0e4e53a806b..d78dd88ac7b 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 @@ -339,7 +339,6 @@ private ProgramElement parseRow(int irow) throws SVInstantiationParserException * @throws SVInstantiationException if the instantiation is incorrect */ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException { - final TermBuilder tb = services.getTermBuilder(); TacletApp result = originalApp; SchemaVariable sv = null; @@ -392,7 +391,6 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException { } for (irow = noEditRow + 1; irow < entries.size(); irow++) { - if (!isInputAvailable(irow)) { continue; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java index 8973db36d72..e9d514ae417 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java @@ -32,7 +32,7 @@ public GenericArgument instantiate(SVInstantiations svInst, Services services) { args = args.prepend(psi.getArgs().get(i).instantiate(svInst, services)); } - return new GenericArgument(ParametricSortInstance.get(psi.getBase(), args)); + return new GenericArgument(ParametricSortInstance.get(psi.getBase(), args, services)); } else { return this; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java index 4e1131feac3..cbe3cb47ba0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; +import de.uka.ilkd.key.logic.sort.GenericSort; import org.key_project.logic.Name; import org.key_project.logic.SyntaxElement; @@ -20,6 +21,9 @@ public final class LogicVariable extends JAbstractSortedOperator public LogicVariable(Name name, Sort sort) { super(name, sort, true); + if (sort instanceof GenericSort) { + throw new IllegalArgumentException("Cannot have logic variable of generic sort!"); + } assert sort != JavaDLTheory.FORMULA; assert sort != JavaDLTheory.UPDATE; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java index 76046826577..d301d908c7e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java @@ -8,6 +8,7 @@ import java.util.Objects; import java.util.WeakHashMap; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.logic.sort.ParametricSortInstance; @@ -29,11 +30,11 @@ public class ParametricFunctionInstance extends JFunction { private final ParametricFunctionDecl base; public static ParametricFunctionInstance get(ParametricFunctionDecl decl, - ImmutableList args) { + ImmutableList args, Services services) { assert args.size() == decl.getParameters().size(); var instMap = getInstMap(decl, args); - var argSorts = instantiate(decl, instMap); - var sort = instantiate(decl.sort(), instMap); + var argSorts = instantiate(decl, instMap, services); + var sort = instantiate(decl.sort(), instMap, services); var fn = new ParametricFunctionInstance(decl, args, argSorts, sort); var cached = CACHE.get(fn); if (cached != null) { @@ -67,13 +68,13 @@ private static Name makeName(ParametricFunctionDecl base, } private static ImmutableArray instantiate(ParametricFunctionDecl base, - Map instMap) { + Map instMap, Services services) { var baseArgSorts = base.argSorts(); var argSorts = new Sort[baseArgSorts.size()]; for (int i = 0; i < baseArgSorts.size(); i++) { var sort = baseArgSorts.get(i); - argSorts[i] = instantiate(sort, instMap); + argSorts[i] = instantiate(sort, instMap, services); } return new ImmutableArray<>(argSorts); @@ -90,7 +91,8 @@ private static Map getInstMap(ParametricFunctionDe return map; } - public static Sort instantiate(Sort sort, Map map) { + public static Sort instantiate(Sort sort, Map map, + Services services) { if (sort instanceof GenericSort gs) { var arg = map.get(gs); return arg == null ? gs : arg.sort(); @@ -99,9 +101,9 @@ public static Sort instantiate(Sort sort, Map map) ImmutableList args = ImmutableSLList.nil(); for (int i = psi.getArgs().size() - 1; i >= 0; i--) { var psiArg = psi.getArgs().get(i); - args = args.prepend(new GenericArgument(instantiate(psiArg.sort(), map))); + args = args.prepend(new GenericArgument(instantiate(psiArg.sort(), map, services))); } - return ParametricSortInstance.get(base, args); + return ParametricSortInstance.get(base, args, services); } else { return sort; } 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 ce5bde2e368..0fee59de13b 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 @@ -38,11 +38,12 @@ public final class SortDependingFunction extends JFunction { // constructors // ------------------------------------------------------------------------- - private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortDependingOn) { + private SortDependingFunction(SortDependingFunctionTemplate template, Sort sortDependingOn, + Services services) { super(instantiateName(template.kind, sortDependingOn), ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, - template.sort), - instantiateArgSorts(template, sortDependingOn), null, template.unique, false); + template.sort, services), + instantiateArgSorts(template, sortDependingOn, services), null, template.unique, false); this.template = template; this.sortDependingOn = sortDependingOn; } @@ -64,11 +65,11 @@ private static Sort instantiateSort(SortDependingFunctionTemplate template, private static ImmutableArray instantiateArgSorts(SortDependingFunctionTemplate template, - Sort sortDependingOn) { + Sort sortDependingOn, Services services) { Sort[] result = new Sort[template.argSorts.size()]; for (int i = 0; i < result.length; i++) { result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, - sortDependingOn, template.argSorts.get(i)); + sortDependingOn, template.argSorts.get(i), services); } return new ImmutableArray<>(result); } @@ -84,10 +85,10 @@ public int hashCode() { } public static SortDependingFunction createFirstInstance(GenericSort sortDependingOn, Name kind, - Sort sort, Sort[] argSorts, boolean unique) { + Sort sort, Sort[] argSorts, boolean unique, Services services) { SortDependingFunctionTemplate template = new SortDependingFunctionTemplate(sortDependingOn, kind, sort, new ImmutableArray<>(argSorts), unique); - return new SortDependingFunction(template, JavaDLTheory.ANY); + return new SortDependingFunction(template, JavaDLTheory.ANY, services); } @@ -128,7 +129,7 @@ public synchronized SortDependingFunction getInstanceFor(Sort sort, TermServices if (result != null && sort instanceof GenericSort && result.getSortDependingOn() != sort) { - result = new SortDependingFunction(template, sort); + result = new SortDependingFunction(template, sort, (Services) services); synchronized (functions) { functions.add(result); if (instantiateName(getKind(), sort).toString().contains("String") @@ -138,7 +139,7 @@ && instantiateName(getKind(), sort).toString().contains("seqGet") } } } else if (result == null) { - result = new SortDependingFunction(template, sort); + result = new SortDependingFunction(template, sort, (Services) services); // The namespaces may be wrapped for local symbols // Sort depending on functions are to be added to the "root" namespace, however. // Therefore, let's rewind to the root (MU, 2017-03) 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 index 49253e0319c..904477e5b6f 100644 --- 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 @@ -8,6 +8,7 @@ import java.util.Objects; import java.util.WeakHashMap; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.GenericParameter; @@ -15,8 +16,6 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; -import org.key_project.logic.SyntaxElement; -import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.AbstractSort; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.DefaultImmutableSet; @@ -35,7 +34,7 @@ public final class ParametricSortInstance extends AbstractSort { private final ImmutableSet extendsSorts; public static ParametricSortInstance get(ParametricSortDecl base, - ImmutableList args) { + ImmutableList args, Services services) { assert args.size() == base.getParameters().size(); ParametricSortInstance sort = new ParametricSortInstance(base, args); @@ -44,6 +43,8 @@ public static ParametricSortInstance get(ParametricSortDecl base, return cached; } else { CACHE.put(sort, sort); + if (!sort.containsGenericSort()) + services.getNamespaces().sorts().addSafely(sort); return sort; } } @@ -65,7 +66,7 @@ private static Name makeName(ParametricSortDecl base, } private static ImmutableSet computeExt(ParametricSortDecl base, - ImmutableList args) { + ImmutableList args, Services services) { ImmutableSet result = DefaultImmutableSet.nil(); // 1. extensions by base sort @@ -73,7 +74,8 @@ private static ImmutableSet computeExt(ParametricSortDecl base, if (!baseExt.isEmpty()) { for (Sort s : baseExt) { result = - result.add(ParametricFunctionInstance.instantiate(s, getInstMap(base, args))); + result.add(ParametricFunctionInstance.instantiate(s, getInstMap(base, args), + services)); } } @@ -151,20 +153,21 @@ private static Map getInstMap(ParametricSortDecl b } public static Sort instantiate(GenericSort genericSort, Sort instantiation, - Sort toInstantiate) { + Sort toInstantiate, Services services) { if (genericSort == toInstantiate) { return instantiation; } else if (toInstantiate instanceof ParametricSortInstance psort) { - return psort.instantiate(genericSort, instantiation); + return psort.instantiate(genericSort, instantiation, services); } else { return toInstantiate; } } - public Sort instantiate(GenericSort template, Sort instantiation) { + public Sort instantiate(GenericSort template, Sort instantiation, Services services) { ImmutableList newParameters = - args.map(s -> new GenericArgument(instantiate(template, instantiation, s.sort()))); - return get(base, newParameters); + args.map( + s -> new GenericArgument(instantiate(template, instantiation, s.sort(), services))); + return get(base, newParameters, services); } public boolean isComplete(SVInstantiations instMap) { @@ -181,8 +184,7 @@ public boolean isComplete(SVInstantiations instMap) { return true; } - public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, - SVInstantiations instMap) { + public Sort resolveSort(SVInstantiations instMap, Services services) { ImmutableList newArgs = ImmutableSLList.nil(); for (int i = args.size() - 1; i >= 0; i--) { GenericArgument arg = args.get(i); @@ -190,7 +192,7 @@ public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, if (sort instanceof ParametricSortInstance psi) { newArgs = newArgs.prepend( - new GenericArgument(psi.resolveSort(sv, instCandidate, instMap))); + new GenericArgument(psi.resolveSort(instMap, services))); } else if (sort instanceof GenericSort gs) { newArgs = newArgs.prepend( new GenericArgument( @@ -199,6 +201,18 @@ public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, newArgs = newArgs.prepend(arg); } } - return get(base, newArgs); + return get(base, newArgs, services); + } + + public boolean containsGenericSort() { + for (GenericArgument arg : args) { + if (arg.sort() instanceof ParametricSortInstance psi && psi.containsGenericSort()) { + return true; + } + if (arg.sort() instanceof GenericSort) { + return true; + } + } + return false; } } 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 2dbbb035279..216d8c6528e 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 @@ -193,7 +193,7 @@ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, St return null; } var args = getGenericArgs(genericArgsCtxt, d.getParameters()); - return ParametricFunctionInstance.get(d, args); + return ParametricFunctionInstance.get(d, args, services); } semanticError(ctx, "Could not find (program) variable or constant %s", varfuncName); return null; @@ -342,7 +342,7 @@ public Sort visitSortId(KeYParser.SortIdContext ctx) { } ImmutableList params = getGenericArgs(ctx.formal_sort_args(), sortDecl.getParameters()); - return ParametricSortInstance.get(sortDecl, params); + return ParametricSortInstance.get(sortDecl, params, services); } // Special handling for byte, char, short, long: // these are *not* sorts, but they are nevertheless valid diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index 0c88affe11d..344ab2ef9be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java @@ -73,7 +73,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { var param = psd.getParameters().get(i); args = args.prepend(new GenericArgument(param.sort())); } - sort = ParametricSortInstance.get(psd, args); + sort = ParametricSortInstance.get(psd, args, services); } else { sort = sorts().lookup(ctx.name.getText()); genericParams = null; @@ -98,7 +98,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { var alreadyDefinedPfn = dtPfnNamespace.lookup(argName); if (alreadyDefinedPfn != null) { alreadyDefinedFn = ParametricFunctionInstance.get(alreadyDefinedPfn, - ImmutableList.of(new GenericArgument(sort))); + ImmutableList.of(new GenericArgument(sort)), services); } } if (alreadyDefinedFn != null @@ -163,7 +163,8 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { if (genSort instanceof GenericSort) { assert argSorts != null; p = SortDependingFunction.createFirstInstance((GenericSort) genSort, - new Name(baseName), JavaDLTheory.FORMULA, argSorts.toArray(new Sort[0]), false); + new Name(baseName), JavaDLTheory.FORMULA, argSorts.toArray(new Sort[0]), false, + services); } } @@ -228,7 +229,7 @@ public Object visitFunc_decl(KeYParser.Func_declContext ctx) { Sort genSort = lookupSort(sortName); if (genSort instanceof GenericSort) { f = SortDependingFunction.createFirstInstance((GenericSort) genSort, - new Name(baseName), retSort, argSorts.toArray(new Sort[0]), unique); + new Name(baseName), retSort, argSorts.toArray(new Sort[0]), unique, services); } } 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 a3e5af2d340..5f86564a040 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 @@ -261,7 +261,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { for (int i = psd.getParameters().size() - 1; i >= 0; i--) { args = args.prepend(new GenericArgument(psd.getParameters().get(i).sort())); } - sort = ParametricSortInstance.get(psd, args); + sort = ParametricSortInstance.get(psd, args, services); } else { sort = sorts().lookup(ctx.name.getText()); } @@ -380,7 +380,7 @@ private Function getPossiblyParametricFunction(String name, Sort sort) { var psi = (ParametricSortInstance) sort; var pfn = namespaces().parametricFunctions().lookup(name); assert pfn != null; - return ParametricFunctionInstance.get(pfn, psi.getArgs()); + return ParametricFunctionInstance.get(pfn, psi.getArgs(), services); } private Sort getPossiblyParametricSort(String name, Sort sort) { @@ -390,7 +390,7 @@ private Sort getPossiblyParametricSort(String name, Sort sort) { var psi = (ParametricSortInstance) sort; var ps = namespaces().parametricSorts().lookup(name); assert ps != null; - return ParametricSortInstance.get(ps, psi.getArgs()); + return ParametricSortInstance.get(ps, psi.getArgs(), services); } private TacletBuilder createInductionTaclet( @@ -408,30 +408,41 @@ private TacletBuilder createInductionTaclet( .map(it -> createGoalDtConstructor(it, qvar, tb.var(phi), sort)) .collect(Collectors.toList()); + for (var c : cases) { + if (c.vars == null) + continue; + for (var v : c.vars) { + tacletBuilder.addVarsNotFreeIn((SchemaVariable) v, phi); + } + } + var use = tb.all(qvar, tb.var(phi)); var useCase = new TacletGoalTemplate( JavaDLSequentKit.createAnteSequent(ImmutableSLList.singleton(new SequentFormula(use))), ImmutableSLList.nil()); useCase.setName("Use case of " + ctx.name.getText()); - cases.add(useCase); + cases.add(new GoalTemplAndVars(useCase, null)); - cases.forEach(tacletBuilder::addTacletGoalTemplate); + cases.stream().map(GoalTemplAndVars::tgt).forEach(tacletBuilder::addTacletGoalTemplate); tacletBuilder.setName(new Name(String.format("DT_%s_Induction", sort.name()))); tacletBuilder.setDisplayName(String.format("DT %s Induction", sort.name())); return tacletBuilder; } - private TacletGoalTemplate createGoalDtConstructor(KeYParser.Datatype_constructorContext it, + private GoalTemplAndVars createGoalDtConstructor(KeYParser.Datatype_constructorContext it, VariableSV qvar, JTerm var, Sort sort) { var constr = createQuantifiedFormula(it, qvar, var, sort); var goal = new TacletGoalTemplate( JavaDLSequentKit - .createSuccSequent(ImmutableSLList.singleton(new SequentFormula(constr))), + .createSuccSequent(ImmutableSLList.singleton(new SequentFormula(constr.term))), ImmutableSLList.nil()); goal.setName(it.getText()); - return goal; + return new GoalTemplAndVars(goal, constr.vars); } + private record GoalTemplAndVars(TacletGoalTemplate tgt, + @Nullable List vars) { + } private TacletBuilder createAxiomTaclet( KeYParser.Datatype_declContext ctx, Sort sort) { @@ -448,7 +459,15 @@ private TacletBuilder createAxiomTaclet( .map(it -> createQuantifiedFormula(it, qvar, tb.var(phi), sort)) .collect(Collectors.toList()); - var axiom = tb.equals(find, tb.and(cases)); + for (var c : cases) { + if (c.vars == null) + continue; + for (var v : c.vars) { + tacletBuilder.addVarsNotFreeIn((SchemaVariable) v, phi); + } + } + + var axiom = tb.equals(find, tb.and(cases.stream().map(TermAndVars::term).toList())); var goal = new TacletGoalTemplate( JavaDLSequentKit @@ -461,12 +480,12 @@ private TacletBuilder createAxiomTaclet( return tacletBuilder; } - private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext context, + private TermAndVars createQuantifiedFormula(KeYParser.Datatype_constructorContext context, QuantifiableVariable qvX, JTerm phi, Sort dt) { var tb = services.getTermBuilder(); var fn = getPossiblyParametricFunction(context.name.getText(), dt); if (context.argName.isEmpty()) - return tb.subst(qvX, tb.func(fn), phi); + return new TermAndVars(tb.subst(qvX, tb.func(fn), phi), null); var args = new JTerm[context.argName.size()]; @@ -482,7 +501,8 @@ private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext cont var ind = new ArrayList(args.length); for (int i = 0; i < argSort.size(); i++) { - final var qv = new LogicVariable(new Name(argNames.get(i)), argSort.get(i)); + final var qv = + SchemaVariableFactory.createVariableSV(new Name(argNames.get(i)), argSort.get(i)); qvs.add(qv); args[i] = services.getTermFactory().createTerm(qvs.get(i)); @@ -492,13 +512,17 @@ private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext cont } if (ind.isEmpty()) { - return tb.all(qvs, tb.subst(qvX, tb.func(fn, args), phi)); + return new TermAndVars(tb.all(qvs, tb.subst(qvX, tb.func(fn, args), phi)), qvs); } else { var base = tb.and(ind); - return tb.all(qvs, tb.imp(base, tb.subst(qvX, tb.func(fn, args), phi))); + return new TermAndVars(tb.all(qvs, tb.imp(base, tb.subst(qvX, tb.func(fn, args), phi))), + qvs); } } + private record TermAndVars(JTerm term, @Nullable List vars) { + } + private RewriteTacletBuilder createConstructorSplit( KeYParser.Datatype_declContext ctx, Sort sort) { final var tb = services.getTermBuilder(); @@ -523,7 +547,7 @@ private RewriteTacletBuilder createConstructorSplit( new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL)); b.setName(new Name("DT_" + sort.name() + "_ctor_split")); - b.setDisplayName(String.format("DT %s case distinction ", sort.name())); + b.setDisplayName(String.format("DT %s case distinction", sort.name())); var phi = declareSchemaVariable(ctx, "var", sort, false, false, false, diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java index e124f39f0cc..d8282834177 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java @@ -496,6 +496,13 @@ Notation getNotation(Operator op) { } } + if (op instanceof ParametricFunctionInstance pfi) { + result = notationTable.get(pfi.getBase()); + if (result != null) { + return result; + } + } + return new Notation.FunctionNotation(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java index 21df139cf98..29b92981fe7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java @@ -98,6 +98,7 @@ private static Object getIndexObj(FindTaclet tac) { case SortDependingFunction sortDependingFunction -> // indexed independently of sort indexObj = sortDependingFunction.getKind(); + case ParametricFunctionInstance pfi -> indexObj = pfi.getBase(); case ElementaryUpdate ignored -> indexObj = ElementaryUpdate.class; case JModality ignored -> @@ -341,6 +342,7 @@ private ImmutableList getListHelp( final ImmutableList inMap = switch (op) { case SortDependingFunction sortDependingFunction -> map.get(sortDependingFunction.getKind()); + case ParametricFunctionInstance pfi -> map.get(pfi.getBase()); case ElementaryUpdate ignored -> map.get(ElementaryUpdate.class); case JModality ignored -> map.get(JModality.class); default -> map.get(op); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java index 238b36c83fc..b9c605cf928 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java @@ -314,7 +314,7 @@ private ImmutableArray instantiateBoundVariables(JTerm vis QuantifiableVariable boundVar = vBoundVars.get(j); if (boundVar instanceof SchemaVariable boundSchemaVariable) { final JTerm instantiationForBoundSchemaVariable = - (JTerm) svInst.getInstantiation(boundSchemaVariable); + svInst.getInstantiation(boundSchemaVariable); // instantiation might be null in case of PO generation for taclets if (instantiationForBoundSchemaVariable != null) { boundVar = (QuantifiableVariable) instantiationForBoundSchemaVariable.op(); @@ -422,7 +422,7 @@ private Operator handleParametricFunction(ParametricFunctionInstance pfi) { args = args.prepend(pfi.getArgs().get(i).instantiate(svInst, services)); } - return ParametricFunctionInstance.get(pfi.getBase(), args); + return ParametricFunctionInstance.get(pfi.getBase(), args, services); } private JTerm resolveSubst(JTerm t) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index 9898de0aba3..806ecb1cc4b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java @@ -658,12 +658,11 @@ private static TacletApp forceGenericSortInstantiation(TacletApp app, JOperatorS } /** - * @param services the Services class allowing access to the type model * @return p_s iff p_s is not a generic sort, the concrete sort p_s is instantiated with * currently otherwise * @throws GenericSortException iff p_s is a generic sort which is not yet instantiated */ - public Sort getRealSort(JOperatorSV p_sv, TermServices services) { + public Sort getRealSort(JOperatorSV p_sv, Services services) { return instantiations().getGenericSortInstantiations().getRealSort(p_sv, services); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index d4b07282738..d6fb42812cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -254,7 +254,7 @@ public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, @Override public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { - return psi.resolveSort(sv, instCandidate, instMap); + return psi.resolveSort(instMap, services); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java index 05d9b825e60..7c97e9309ac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java @@ -8,10 +8,12 @@ import java.util.LinkedHashSet; import java.util.Set; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.ProgramSV; import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import org.key_project.logic.LogicServices; import org.key_project.logic.op.sv.OperatorSV; @@ -183,21 +185,34 @@ public ImmutableList toConditions() { /** - * @param services the Services class * @return p_s iff p_s is not a generic sort, the concrete sort p_s is instantiated with * currently otherwise * @throws GenericSortException iff p_s is a generic sort which is not yet instantiated */ - public Sort getRealSort(OperatorSV p_sv, TermServices services) { + public Sort getRealSort(OperatorSV p_sv, Services services) { return getRealSort(p_sv.sort(), services); } - public Sort getRealSort(Sort p_s, TermServices services) { - if (p_s instanceof GenericSort) { - p_s = getInstantiation((GenericSort) p_s); + public Sort getRealSort(Sort p_s, Services services) { + if (p_s instanceof GenericSort gs) { + p_s = getInstantiation(gs); if (p_s == null) { throw new GenericSortException("Generic sort is not yet instantiated", null); } + } else if (p_s instanceof ParametricSortInstance psi && psi.containsGenericSort()) { + ImmutableList args = ImmutableSLList.nil(); + for (int i = psi.getArgs().size() - 1; i >= 0; i--) { + GenericArgument oa = psi.getArgs().get(i); + Sort realSort = getRealSort(oa.sort(), services); + if (realSort == null) { + throw new GenericSortException("Generic sort is not yet instantiated", null); + } + args = args.prepend(new GenericArgument(realSort)); + } + var inst = ParametricSortInstance.get(psi.getBase(), args, services); + if (inst.containsGenericSort()) + throw new GenericSortException("Generic sort is not yet instantiated", null); + p_s = inst; } return p_s; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index 4b6cea4efe9..76a5a332114 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -995,6 +995,7 @@ public static ProofCollection automaticJavaDL() throws IOException { g.loadable("standard_key/adt/dt_list_appnil.proof"); g.loadable("standard_key/adt/dt_color.proof"); g.loadable("standard_key/adt/dt_list_deconstruct.key"); + g.loadable("standard_key/adt/dt_polymorphic.proof"); g = c.group("PolymorphicSorts"); g.loadable("standard_key/polymorphic/pseq.key"); diff --git a/key.ui/examples/standard_key/adt/dt_polymorphic.key b/key.ui/examples/standard_key/adt/dt_polymorphic.key index fb0e4b1fc13..67a4171971b 100644 --- a/key.ui/examples/standard_key/adt/dt_polymorphic.key +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.key @@ -18,6 +18,7 @@ \sorts { \generic E; + \generic F; S; } diff --git a/key.ui/examples/standard_key/adt/dt_polymorphic.proof b/key.ui/examples/standard_key/adt/dt_polymorphic.proof new file mode 100644 index 00000000000..50065874303 --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.proof @@ -0,0 +1,159 @@ +\profile "Java Profile"; + +\settings // Proof-Settings-Config-File +{ + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on", + "wdChecks" : "wdChecks:off", + "wdOperator" : "wdOperator:L" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "JavaCardDLStrategy", + "MaximumNumberOfAutomaticApplications" : 10000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_OFF", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } + } + +\heuristicsDecl { + LIST; +} + +\sorts { + \generic E; + S; +} + +\datatypes { + List<[E]> = Nil | Cons(E head, List<[E]> tail); +} + +\predicates { + contains<[E]>(E, List<[E]>); +} + +\functions{ + // append to lists + List<[E]> app<[E]>(List<[E]>, List<[E]>); + // revert a list + List<[E]> rev<[E]>(List<[E]>); +} + +\schemaVariables { + \term List<[E]> list, list1; + \term E e; + \variables List<[E]> nv; + \variables E el; + \formula b; +} + +\rules { + // axioms + concat_base{ + \find (app<[E]>(Nil<[E]>, list)) + \replacewith (list) + \heuristics (LIST) + }; + concat_step{ + \find( app<[E]>(Cons<[E]>(e, list1), list) ) + \replacewith (Cons<[E]>(e, app<[E]>(list1,list) )) + \heuristics (LIST)}; + + // definition of revert + revert_base {\find (rev<[E]>(Nil<[E]>)) \replacewith(Nil<[E]>) }; + revert_step {\find (rev<[E]>(Cons<[E]>(e,list))) \replacewith (app<[E]>(rev<[E]>(list),Cons<[E]>(e,Nil<[E]>)))}; +} +\problem { +\forall List<[S]> l; app<[S]>(l, Nil<[S]>) = l +} + +\proof { +(keyLog "0" (keyUser "daniel" ) (keyVersion "04c4de851611b1341e40b4e6f9ebe57d93bed7ea")) + +(autoModeTime "0") + +(branch "dummy ID" +(rule "DT_List<[E]>_Induction" (newnames "heapAtPre,savedHeapAtPre,arg0AtPre,arg1AtPre,heapAtPre,savedHeapAtPre,arg0AtPre,arg1AtPre,heapAtPre,savedHeapAtPre,arg0AtPre,heapAtPre,savedHeapAtPre,vAtPre") (inst "phi=(app<[S]>(x, Nil<[S]>) = x)< Induction)\",\"[]\")>>") (inst "x=x") (inst "tail=tail") (inst "head=head") (userinteraction)) +(branch "Nil" + (rule "concat_base" (formula "1") (term "0") (userinteraction)) + (rule "equalUnique" (formula "1") (userinteraction)) + (rule "closeTrue" (formula "1") (userinteraction)) +) +(branch "Cons(Ehead,List<[E]>tail)" + (rule "allRight" (formula "1") (inst "sk=tail_0") (userinteraction)) + (rule "allRight" (formula "1") (inst "sk=head_0") (userinteraction)) + (rule "impRight" (formula "1") (userinteraction)) + (rule "concat_step" (formula "2") (term "0") (userinteraction)) + (rule "applyEqRigid" (formula "2") (term "1,0") (ifseqformula "1") (userinteraction)) + (rule "equalUnique" (formula "2") (userinteraction)) + (rule "eqClose" (formula "2") (term "0") (userinteraction)) + (rule "concrete_and_1" (formula "2") (userinteraction)) + (rule "eqClose" (formula "2") (userinteraction)) + (rule "closeTrue" (formula "2") (userinteraction)) +) +(branch "Use case of List" + (rule "close" (formula "2") (ifseqformula "1") (userinteraction)) +) +) +} From 412e84aa3d5b3fb8b316c38bd4220183321a8c97 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 25 Sep 2025 11:18:02 +0200 Subject: [PATCH 08/13] Slightly improve error messages --- .../java/de/uka/ilkd/key/rule/TacletApp.java | 30 ++++++++++ .../rule/TacletSchemaVariableCollector.java | 2 +- .../UninstantiatedGenericSortCollector.java | 55 +++++++++++++++++++ .../standard_key/adt/dt_polymorphic.key | 5 ++ 4 files changed, 91 insertions(+), 1 deletion(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/UninstantiatedGenericSortCollector.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index 806ecb1cc4b..7dee2134ace 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.ClashFreeSubst.VariableCollectVisitor; import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.logic.sort.ProgramSVSort; import de.uka.ilkd.key.proof.VariableNameProposer; import de.uka.ilkd.key.rule.inst.GenericSortCondition; @@ -78,6 +79,8 @@ public abstract class TacletApp implements RuleApp { */ private volatile ImmutableSet missingVars = null; + private volatile ImmutableSet missingSorts = null; + /** * the update context given by the current instantiations must not be changed */ @@ -399,6 +402,23 @@ protected ImmutableSet calculateNonInstantiatedSV() { return missingVars; } + /** + * calculate needed GenericSorts that have not been instantiated yet. This means to ignore + * GenericSorts that appear only in addrule-sections of Taclets + * + * @return ImmutableSet that need to be instantiated but are not + */ + protected ImmutableSet calculateNonInstantiatedGenericSorts() { + if (missingSorts == null) { + var coll = + new UninstantiatedGenericSortCollector(instantiations()); + coll.visitWithoutAddrule(taclet()); + missingSorts = Immutables.createSetFrom(coll.getSortList()); + } + + return missingSorts; + } + /** * creates a new Tacletapp where the SchemaVariable sv is instantiated with the given term. @@ -447,6 +467,15 @@ public TacletApp addCheckedInstantiation(SchemaVariable sv, JTerm term, Services return calculateNonInstantiatedSV(); } + /// returns the generic sorts that have not yet been instantiated and need to be instantiated to + /// apply the Taclet. (These are not all sorts like the one that appear only in the + /// addrule sections) + /// + /// @return ImmutableSet with GenericSorts that have not been instantiated yet + public @NonNull ImmutableSet uninstantiatedGenericSorts() { + return calculateNonInstantiatedGenericSorts(); + } + /** * returns true if the given {@link SchemaVariable} must be explicitly instantiated it does not @@ -712,6 +741,7 @@ public void registerSkolemConstants(Namespace<@NonNull Function> fns) { public final boolean complete() { return (posInOccurrence() != null || taclet instanceof NoFindTaclet) && uninstantiatedVars().isEmpty() + && uninstantiatedGenericSorts().isEmpty() && assumesInstantionsComplete(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java index 324c8600d8d..64221c86128 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java @@ -44,7 +44,7 @@ public class TacletSchemaVariableCollector implements DefaultVisitor { /** collects all found variables */ protected @NonNull ImmutableList varList; /** the instantiations needed for unwind loop constructs */ - private @NonNull SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS; + protected @NonNull SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS; public TacletSchemaVariableCollector() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UninstantiatedGenericSortCollector.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UninstantiatedGenericSortCollector.java new file mode 100644 index 00000000000..e76e153b32c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UninstantiatedGenericSortCollector.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 de.uka.ilkd.key.rule; + +import java.util.HashSet; +import java.util.Set; + +import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.logic.Term; +import org.key_project.logic.sort.Sort; + +import org.jspecify.annotations.NonNull; + +public class UninstantiatedGenericSortCollector extends TacletSchemaVariableCollector { + /** collects all found variables */ + protected @NonNull Set sortList = new HashSet<>(); + + /** + * @param svInsts the SVInstantiations that have been already found (needed by unwind loop + * constructs to determine which labels are needed) + */ + public UninstantiatedGenericSortCollector(@NonNull SVInstantiations svInsts) { + super(svInsts); + } + + @Override + public void visit(@NonNull Term p_visited) { + visit(p_visited.sort()); + for (var t : p_visited.subs()) { + visit(t); + } + for (var bv : p_visited.boundVars()) { + visit(bv.sort()); + } + } + + private void visit(Sort s) { + if (s instanceof GenericSort gs + && !instantiations.getGenericSortInstantiations().isInstantiated(gs)) { + sortList.add(gs); + } else if (s instanceof ParametricSortInstance psi) { + for (var a : psi.getArgs()) { + visit(a.sort()); + } + } + } + + public Set getSortList() { + return sortList; + } +} diff --git a/key.ui/examples/standard_key/adt/dt_polymorphic.key b/key.ui/examples/standard_key/adt/dt_polymorphic.key index 67a4171971b..d5ff8f58a8e 100644 --- a/key.ui/examples/standard_key/adt/dt_polymorphic.key +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.key @@ -60,6 +60,11 @@ // definition of revert revert_base {\find (rev<[E]>(Nil<[E]>)) \replacewith(Nil<[E]>) }; revert_step {\find (rev<[E]>(Cons<[E]>(e,list))) \replacewith (app<[E]>(rev<[E]>(list),Cons<[E]>(e,Nil<[E]>)))}; + + // This tests that rules are not applicable if uninstantiated generic sorts remain. + my_weird_sort { + \add(==> Nil<[F]> = Nil<[F]>) + }; } \problem { From d1555e55e3fad9d6c3d51e5072d411538da57e69 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 25 Sep 2025 11:21:49 +0200 Subject: [PATCH 09/13] Fix test classes --- .../key/logic/sort/TestParametricSorts.java | 21 ++++++++++++------- 1 file changed, 13 insertions(+), 8 deletions(-) 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 index de92bfcda7c..da218ebe9f2 100644 --- 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 @@ -71,7 +71,7 @@ private ParametricSortDecl addParametricSort(String name, public void testParametricSortIdentical() { ParametricSortDecl psd = addParametricSort("List", GenericParameter.Variance.COVARIANT); var sdf = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, - new Sort[0], false); + new Sort[0], false, services); nss.functions().add(sdf); var term = io.parseExpression("List<[int]>::someConst = List<[int]>::someConst"); @@ -85,14 +85,16 @@ public void testParametricSortDependentFunctionInstantiation() { Sort intSort = nss.sorts().lookup("int"); var someConst = SortDependingFunction.createFirstInstance(g1, new Name("someConst"), g1, - new Sort[0], false); + new Sort[0], false, services); nss.functions().add(someConst); var listOfInt = - ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); - var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1))); + ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort)), + services); + var listOfG1 = + ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1)), services); var sdf = SortDependingFunction.createFirstInstance(g1, new Name("head"), g1, - new Sort[] { listOfG1 }, false); + new Sort[] { listOfG1 }, false, services); nss.functions().add(sdf); SortDependingFunction sdfInst = sdf.getInstanceFor(intSort, services); @@ -117,8 +119,10 @@ public void testParametricFunctionInstantiation() { nss.parametricFunctions().add(someConst); var listOfInt = - ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort))); - var listOfG1 = ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1))); + ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(intSort)), + services); + var listOfG1 = + ParametricSortInstance.get(psd, ImmutableList.of(new GenericArgument(g1)), services); var head = new ParametricFunctionDecl(new Name("head"), ImmutableList.of(new GenericParameter(g1, GenericParameter.Variance.COVARIANT)), @@ -126,7 +130,8 @@ public void testParametricFunctionInstantiation() { nss.parametricFunctions().add(head); var headInst = - ParametricFunctionInstance.get(head, ImmutableList.of(new GenericArgument(intSort))); + ParametricFunctionInstance.get(head, ImmutableList.of(new GenericArgument(intSort)), + services); assertEquals(intSort, headInst.sort()); assertEquals(listOfInt, headInst.argSort(0)); From f8acedaca79fce22e50d5f8a67207445c32448d0 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 25 Sep 2025 11:37:29 +0200 Subject: [PATCH 10/13] Some documentation --- .../key/control/AbstractProofControl.java | 4 +++ .../uka/ilkd/key/logic/GenericArgument.java | 1 + .../uka/ilkd/key/logic/GenericParameter.java | 1 + .../key/logic/op/ParametricFunctionDecl.java | 4 +++ .../logic/op/ParametricFunctionInstance.java | 29 +++++------------ .../key/logic/sort/ParametricSortDecl.java | 4 +++ .../logic/sort/ParametricSortInstance.java | 32 +++++++++++++++++-- 7 files changed, 51 insertions(+), 24 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index 7313aab4618..535d6032acd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java @@ -223,6 +223,10 @@ public boolean selectedTaclet(ImmutableSet applics, Goal goal) { firstApp = tmpApp; } } catch (GenericSortException ge) { + // If we just "try" to instantiate, it is fine to fail at this point. + // In many cases, we add instantiations later (e.g., through a dialog) that + // clear up any missing + // generic sort instantiations. } } if (ifSeqInteraction || !firstApp.complete()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java index e9d514ae417..e366e043ff4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java @@ -15,6 +15,7 @@ import org.jspecify.annotations.NonNull; +/// An argument for a [ParametricSortInstance] or [ParametricFunctionInstance]. public record GenericArgument(Sort sort) implements TerminalSyntaxElement { @Override public @NonNull String toString() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java index 45ead7cc045..20432a8c1d2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java @@ -7,6 +7,7 @@ import org.jspecify.annotations.NonNull; +/// Abstract parameter for [ParametricFunctionDecl] or [ParametricSortDecl] public record GenericParameter(GenericSort sort, Variance variance) { @Override public @NonNull String toString() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java index 5d757411915..78b7a6a1c49 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java @@ -15,6 +15,10 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; +/// The abstract declaration of a parametric function, e.g., `append<[E]>(List<[E]>, List<[E]>)`. +/// +/// To get an instantiated instance, use [ParametricFunctionInstance#get(ParametricFunctionDecl, +/// ImmutableList, Services)]. public final class ParametricFunctionDecl implements Named, Sorted { private final Name name; private final ImmutableList parameters; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java index d301d908c7e..b9a7337535c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java @@ -18,10 +18,10 @@ import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableSLList; import org.jspecify.annotations.NonNull; +/// A concrete instance of a [ParametricFunctionDecl]. public class ParametricFunctionInstance extends JFunction { private static final Map CACHE = new WeakHashMap<>(); @@ -29,12 +29,14 @@ public class ParametricFunctionInstance extends JFunction { private final ImmutableList args; private final ParametricFunctionDecl base; + /// Returns the function of `decl` instantiated with the arguments `arg`. If necessary, a new + /// object is created. public static ParametricFunctionInstance get(ParametricFunctionDecl decl, ImmutableList args, Services services) { assert args.size() == decl.getParameters().size(); var instMap = getInstMap(decl, args); var argSorts = instantiate(decl, instMap, services); - var sort = instantiate(decl.sort(), instMap, services); + var sort = ParametricSortInstance.instantiate(decl.sort(), instMap, services); var fn = new ParametricFunctionInstance(decl, args, argSorts, sort); var cached = CACHE.get(fn); if (cached != null) { @@ -67,6 +69,8 @@ private static Name makeName(ParametricFunctionDecl base, return new Name(base.name() + "<" + parameters + ">"); } + /// Instantiates the arguments of `base` with the instantiations for the generic sorts in + /// `instMap`. private static ImmutableArray instantiate(ParametricFunctionDecl base, Map instMap, Services services) { var baseArgSorts = base.argSorts(); @@ -74,12 +78,13 @@ private static ImmutableArray instantiate(ParametricFunctionDecl base, for (int i = 0; i < baseArgSorts.size(); i++) { var sort = baseArgSorts.get(i); - argSorts[i] = instantiate(sort, instMap, services); + argSorts[i] = ParametricSortInstance.instantiate(sort, instMap, services); } return new ImmutableArray<>(argSorts); } + /// Computes an instantiation mapping for `base`. private static Map getInstMap(ParametricFunctionDecl base, ImmutableList args) { var map = new HashMap(); @@ -91,24 +96,6 @@ private static Map getInstMap(ParametricFunctionDe return map; } - public static Sort instantiate(Sort sort, Map map, - Services services) { - if (sort instanceof GenericSort gs) { - var arg = map.get(gs); - return arg == null ? gs : arg.sort(); - } else if (sort instanceof ParametricSortInstance psi) { - var base = psi.getBase(); - ImmutableList args = ImmutableSLList.nil(); - for (int i = psi.getArgs().size() - 1; i >= 0; i--) { - var psiArg = psi.getArgs().get(i); - args = args.prepend(new GenericArgument(instantiate(psiArg.sort(), map, services))); - } - return ParametricSortInstance.get(base, args, services); - } else { - return sort; - } - } - @Override public int getChildCount() { return args.size(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java index 41ec63662a7..a0484a75d9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java @@ -15,6 +15,10 @@ import org.jspecify.annotations.NonNull; +/// Abstract declaration of a parametric sort, e.g., `List<[E]>`. +/// +/// Get instantiated versions using [ParametricSortInstance#get(ParametricSortDecl, ImmutableList, +/// Services)]. public class ParametricSortDecl implements Named { private final Name name; private final boolean isAbstract; 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 index 904477e5b6f..1a56d276d30 100644 --- 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 @@ -12,7 +12,6 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.GenericParameter; -import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; @@ -25,6 +24,7 @@ import org.jspecify.annotations.NonNull; +/// Concrete sort of a parametric sort. public final class ParametricSortInstance extends AbstractSort { private static final Map CACHE = new WeakHashMap<>(); @@ -33,6 +33,8 @@ public final class ParametricSortInstance extends AbstractSort { private final ParametricSortDecl base; private final ImmutableSet extendsSorts; + /// Returns the sort of `decl` instantiated with the arguments `arg`. If necessary, a new object + /// is created. public static ParametricSortInstance get(ParametricSortDecl base, ImmutableList args, Services services) { assert args.size() == base.getParameters().size(); @@ -74,7 +76,7 @@ private static ImmutableSet computeExt(ParametricSortDecl base, if (!baseExt.isEmpty()) { for (Sort s : baseExt) { result = - result.add(ParametricFunctionInstance.instantiate(s, getInstMap(base, args), + result.add(instantiate(s, getInstMap(base, args), services)); } } @@ -141,6 +143,7 @@ public boolean extendsTrans(@NonNull Sort sort) { .exists((Sort superSort) -> superSort == sort || superSort.extendsTrans(sort)); } + /// Compute an instantiation mapping. private static Map getInstMap(ParametricSortDecl base, ImmutableList args) { var map = new HashMap(); @@ -163,13 +166,34 @@ public static Sort instantiate(GenericSort genericSort, Sort instantiation, } } - public Sort instantiate(GenericSort template, Sort instantiation, Services services) { + /// Instantiate a sort that may be or contain generic sorts with `map`. + public static Sort instantiate(Sort sort, Map map, + Services services) { + if (sort instanceof GenericSort gs) { + var arg = map.get(gs); + return arg == null ? gs : arg.sort(); + } else if (sort instanceof ParametricSortInstance psi) { + var base = psi.getBase(); + ImmutableList args = ImmutableSLList.nil(); + for (int i = psi.getArgs().size() - 1; i >= 0; i--) { + var psiArg = psi.getArgs().get(i); + args = args.prepend(new GenericArgument(instantiate(psiArg.sort(), map, services))); + } + return ParametricSortInstance.get(base, args, services); + } else { + return sort; + } + } + + public ParametricSortInstance instantiate(GenericSort template, Sort instantiation, + Services services) { ImmutableList newParameters = args.map( s -> new GenericArgument(instantiate(template, instantiation, s.sort(), services))); return get(base, newParameters, services); } + /// Whether this sort is complete when instantiated with `instMap`. public boolean isComplete(SVInstantiations instMap) { for (GenericArgument arg : args) { var sort = arg.sort(); @@ -184,6 +208,7 @@ public boolean isComplete(SVInstantiations instMap) { return true; } + /// Get the sort if this parametric sort with all generics instantiated with `instMap`. public Sort resolveSort(SVInstantiations instMap, Services services) { ImmutableList newArgs = ImmutableSLList.nil(); for (int i = args.size() - 1; i >= 0; i--) { @@ -204,6 +229,7 @@ public Sort resolveSort(SVInstantiations instMap, Services services) { return get(base, newArgs, services); } + /// Whether this sort contains generic sorts. public boolean containsGenericSort() { for (GenericArgument arg : args) { if (arg.sort() instanceof ParametricSortInstance psi && psi.containsGenericSort()) { From cb55569e945961d595287c26e79234ba20c796e3 Mon Sep 17 00:00:00 2001 From: Drodt Date: Fri, 26 Sep 2025 13:45:17 +0200 Subject: [PATCH 11/13] Fix proof loading/storing when generics are instantiated in NoFindTaclets --- .../proof/io/IntermediateProofReplayer.java | 13 ++++++++++- .../key/proof/io/OutputStreamProofSaver.java | 8 +++++++ .../standard_key/adt/dt_polymorphic.proof | 23 +++++++++++-------- 3 files changed, 33 insertions(+), 11 deletions(-) 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 d22d7eae28a..d1a530d37bb 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 @@ -995,7 +995,18 @@ public static JTerm parseTerm(String value, Proof proof) { */ public static TacletApp parseSV1(TacletApp app, VariableSV sv, String value, Services services) { - LogicVariable lv = new LogicVariable(new Name(value), app.getRealSort(sv, services)); + var colon = value.indexOf(':'); + Sort sort; + String name; + if (colon < 0) { + name = value; + sort = app.getRealSort(sv, services); + } else { + name = value.substring(0, colon); + sort = services.getNamespaces().sorts().lookup(value.substring(colon + 1)); + + } + LogicVariable lv = new LogicVariable(new Name(name), sort); JTerm instance = services.getTermFactory().createTerm(lv); return app.addCheckedInstantiation(sv, instance, services, true); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 0db5b7fd9f5..a8711470751 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -17,6 +17,8 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.pp.PrettyPrinter; @@ -753,6 +755,12 @@ public Collection getInterestingInstantiations(SVInstantiations inst) { String singleInstantiation = var.name() + "=" + printAnything(value, proof.getServices(), false); + if ((var.sort() instanceof GenericSort + || var.sort() instanceof ParametricSortInstance psi + && psi.containsGenericSort())) { + var t = (JTerm) value; + singleInstantiation += ":" + t.sort().name(); + } s.add(singleInstantiation); } diff --git a/key.ui/examples/standard_key/adt/dt_polymorphic.proof b/key.ui/examples/standard_key/adt/dt_polymorphic.proof index 50065874303..cd47b69b6eb 100644 --- a/key.ui/examples/standard_key/adt/dt_polymorphic.proof +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.proof @@ -60,7 +60,7 @@ "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", "MPS_OPTIONS_KEY" : "MPS_MERGE", "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", - "OSS_OPTIONS_KEY" : "OSS_OFF", + "OSS_OPTIONS_KEY" : "OSS_ON", "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", @@ -82,6 +82,7 @@ \sorts { \generic E; + \generic F; S; } @@ -123,6 +124,11 @@ // definition of revert revert_base {\find (rev<[E]>(Nil<[E]>)) \replacewith(Nil<[E]>) }; revert_step {\find (rev<[E]>(Cons<[E]>(e,list))) \replacewith (app<[E]>(rev<[E]>(list),Cons<[E]>(e,Nil<[E]>)))}; + + // This tests that rules are not applicable if uninstantiated generic sorts remain. + my_weird_sort { + \add(==> Nil<[F]> = Nil<[F]>) + }; } \problem { \forall List<[S]> l; app<[S]>(l, Nil<[S]>) = l @@ -134,26 +140,23 @@ (autoModeTime "0") (branch "dummy ID" -(rule "DT_List<[E]>_Induction" (newnames "heapAtPre,savedHeapAtPre,arg0AtPre,arg1AtPre,heapAtPre,savedHeapAtPre,arg0AtPre,arg1AtPre,heapAtPre,savedHeapAtPre,arg0AtPre,heapAtPre,savedHeapAtPre,vAtPre") (inst "phi=(app<[S]>(x, Nil<[S]>) = x)< Induction)\",\"[]\")>>") (inst "x=x") (inst "tail=tail") (inst "head=head") (userinteraction)) +(rule "DT_List<[E]>_Induction" (newnames "heapAtPre,savedHeapAtPre,arg0AtPre,arg1AtPre,heapAtPre,savedHeapAtPre,arg0AtPre,arg1AtPre,heapAtPre,savedHeapAtPre,arg0AtPre,heapAtPre,savedHeapAtPre,vAtPre") (inst "phi=(app<[S]>(l, Nil<[S]>) = l)< Induction)\",\"[]\")>>") (inst "x=l:List<[S]>") (inst "tail=tail:List<[S]>") (inst "head=head:S") (userinteraction)) (branch "Nil" (rule "concat_base" (formula "1") (term "0") (userinteraction)) - (rule "equalUnique" (formula "1") (userinteraction)) + (builtin "One Step Simplification" (formula "1") (userinteraction)) (rule "closeTrue" (formula "1") (userinteraction)) ) (branch "Cons(Ehead,List<[E]>tail)" - (rule "allRight" (formula "1") (inst "sk=tail_0") (userinteraction)) - (rule "allRight" (formula "1") (inst "sk=head_0") (userinteraction)) + (rule "allRight" (formula "1") (inst "sk=tail_0:List<[S]>") (userinteraction)) + (rule "allRight" (formula "1") (inst "sk=head_0:S") (userinteraction)) (rule "impRight" (formula "1") (userinteraction)) (rule "concat_step" (formula "2") (term "0") (userinteraction)) (rule "applyEqRigid" (formula "2") (term "1,0") (ifseqformula "1") (userinteraction)) - (rule "equalUnique" (formula "2") (userinteraction)) - (rule "eqClose" (formula "2") (term "0") (userinteraction)) - (rule "concrete_and_1" (formula "2") (userinteraction)) - (rule "eqClose" (formula "2") (userinteraction)) + (builtin "One Step Simplification" (formula "2") (userinteraction)) (rule "closeTrue" (formula "2") (userinteraction)) ) (branch "Use case of List" - (rule "close" (formula "2") (ifseqformula "1") (userinteraction)) + (rule "closeAntec" (formula "1") (ifseqformula "2") (userinteraction)) ) ) } From 8115a30897ee074a1cf5fabe28387bd466b0b3f2 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 30 Oct 2025 13:08:11 +0100 Subject: [PATCH 12/13] Fix parsing of proof files --- .../de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java | 4 ++++ 1 file changed, 4 insertions(+) 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 d1a530d37bb..62c55da4c90 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 @@ -925,6 +925,10 @@ public static TacletApp constructInsts(@NonNull TacletApp app, Goal currGoal, } String value = s.substring(eq + 1); + int colon = value.indexOf(':'); + if (colon != -1) { + value = value.substring(0, colon); + } app = parseSV2(app, sv, value, currGoal); } From 0f8b28add13081d3a7fa32e22493e994d49191da Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 30 Oct 2025 14:10:31 +0100 Subject: [PATCH 13/13] Fix inst with sort depending fn --- .../de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java | 4 ++-- .../java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) 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 62c55da4c90..c920ce8722d 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 @@ -925,8 +925,8 @@ public static TacletApp constructInsts(@NonNull TacletApp app, Goal currGoal, } String value = s.substring(eq + 1); - int colon = value.indexOf(':'); - if (colon != -1) { + int colon = value.lastIndexOf(':'); + if (colon != -1 && value.charAt(colon - 1) != ':') { value = value.substring(0, colon); } app = parseSV2(app, sv, value, currGoal); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java index 88e87ee5f9e..f46b1133ff9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java @@ -56,7 +56,7 @@ public class ProveRulesTest { public void loadTacletProof(String tacletName, Taclet taclet, @Nullable Path proofFile) throws Exception { assertNotNull(proofFile, - "Taclet " + tacletName + " was annoted with \\lemma but no taclet proof was found."); + "Taclet " + tacletName + " was annotated with \\lemma but no taclet proof was found."); assertNotNull(taclet, "Proof file " + proofFile + " claims that it contains a proof for taclet " + tacletName + " but corresponding taclet seems to be unavailable (maybe it is not annotated with \\lemma?).");