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 f111efcedec..6e992d132f3 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)* @@ -209,6 +215,7 @@ pred_decl : doc=DOC_COMMENT? pred_name = funcpred_name + formal_sort_param_decls? (whereToBind=where_to_bind)? argSorts=arg_sorts SEMI @@ -225,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 ; @@ -243,7 +251,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 +268,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 +345,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 +506,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/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index ad0cfa1f370..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 @@ -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,18 @@ 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 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()) { 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 new file mode 100644 index 00000000000..e366e043ff4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericArgument.java @@ -0,0 +1,41 @@ +/* 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; + +/// An argument for a [ParametricSortInstance] or [ParametricFunctionInstance]. +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, services)); + } 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..20432a8c1d2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/GenericParameter.java @@ -0,0 +1,20 @@ +/* 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; + +/// Abstract parameter for [ParametricFunctionDecl] or [ParametricSortDecl] +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/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/ParametricFunctionDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java new file mode 100644 index 00000000000..78b7a6a1c49 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java @@ -0,0 +1,79 @@ +/* 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; + +/// 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; + 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..b9a7337535c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java @@ -0,0 +1,121 @@ +/* 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.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; + +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.jspecify.annotations.NonNull; + +/// A concrete instance of a [ParametricFunctionDecl]. +public class ParametricFunctionInstance extends JFunction { + private static final Map CACHE = + new WeakHashMap<>(); + + 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 = ParametricSortInstance.instantiate(decl.sort(), instMap, services); + 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 + ">"); + } + + /// 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(); + var argSorts = new Sort[baseArgSorts.size()]; + + for (int i = 0; i < baseArgSorts.size(); i++) { + var sort = baseArgSorts.get(i); + 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(); + 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; + } + + @Override + public int getChildCount() { + return args.size(); + } + + @Override + 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/logic/op/SortDependingFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java index b0051025fc1..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 @@ -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; @@ -37,10 +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), - instantiateResultSort(template, sortDependingOn), - instantiateArgSorts(template, sortDependingOn), null, template.unique, false); + ParametricSortInstance.instantiate(template.sortDependingOn, sortDependingOn, + template.sort, services), + instantiateArgSorts(template, sortDependingOn, services), null, template.unique, false); this.template = template; this.sortDependingOn = sortDependingOn; } @@ -55,18 +58,18 @@ private static Name instantiateName(Name kind, Sort sortDependingOn) { } - private static Sort instantiateResultSort(SortDependingFunctionTemplate template, + private static Sort instantiateSort(SortDependingFunctionTemplate template, Sort sortDependingOn) { return template.sort == template.sortDependingOn ? sortDependingOn : template.sort; } 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] = (template.argSorts.get(i) == template.sortDependingOn ? sortDependingOn - : template.argSorts.get(i)); + result[i] = ParametricSortInstance.instantiate(template.sortDependingOn, + sortDependingOn, template.argSorts.get(i), services); } return new ImmutableArray<>(result); } @@ -82,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); } @@ -109,7 +112,6 @@ public synchronized SortDependingFunction getInstanceFor(Sort sort, TermServices SortDependingFunction n = (SortDependingFunction) services.getNamespaces() .lookup(instantiateName(getKind(), sort)); - if (sort instanceof ProgramSVSort) { throw new AssertionError(); } @@ -127,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") @@ -137,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/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/logic/sort/ParametricSortDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java new file mode 100644 index 00000000000..a0484a75d9f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java @@ -0,0 +1,67 @@ +/* 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; + +/// 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; + 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..1a56d276d30 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java @@ -0,0 +1,244 @@ +/* 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.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.rule.inst.SVInstantiations; + +import org.key_project.logic.Name; +import org.key_project.logic.sort.AbstractSort; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.DefaultImmutableSet; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; +import org.key_project.util.collection.ImmutableSet; + +import org.jspecify.annotations.NonNull; + +/// Concrete sort of a parametric sort. +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; + + /// 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(); + ParametricSortInstance sort = + new ParametricSortInstance(base, args); + ParametricSortInstance cached = CACHE.get(sort); + if (cached != null) { + return cached; + } else { + CACHE.put(sort, sort); + if (!sort.containsGenericSort()) + services.getNamespaces().sorts().addSafely(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, Services services) { + ImmutableSet result = DefaultImmutableSet.nil(); + + // 1. extensions by base sort + ImmutableSet baseExt = base.getExtendedSorts(); + if (!baseExt.isEmpty()) { + for (Sort s : baseExt) { + result = + result.add(instantiate(s, getInstMap(base, args), + services)); + } + } + + // 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)); + } + + /// Compute an instantiation mapping. + 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, Services services) { + if (genericSort == toInstantiate) { + return instantiation; + } else if (toInstantiate instanceof ParametricSortInstance psort) { + return psort.instantiate(genericSort, instantiation, services); + } else { + return toInstantiate; + } + } + + /// 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(); + 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; + } + + /// 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--) { + GenericArgument arg = args.get(i); + var sort = arg.sort(); + if (sort instanceof ParametricSortInstance psi) { + newArgs = + newArgs.prepend( + new GenericArgument(psi.resolveSort(instMap, services))); + } else if (sort instanceof GenericSort gs) { + newArgs = newArgs.prepend( + new GenericArgument( + instMap.getGenericSortInstantiations().getInstantiation(gs))); + } else { + newArgs = newArgs.prepend(arg); + } + } + 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()) { + 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/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 30d94ea933c..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 @@ -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,8 +20,10 @@ 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.slf4j.Logger; @@ -70,8 +69,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,51 +155,82 @@ 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); + 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().addSafely(sortDecl); } return createdSorts; } 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..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 @@ -18,8 +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.*; import de.uka.ilkd.key.nparser.KeYParser; import org.key_project.logic.*; @@ -30,9 +29,12 @@ 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; +import org.jspecify.annotations.Nullable; /** * Helper class for are visitor that requires a namespaces and services. Also it provides the @@ -141,10 +143,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 +163,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 +186,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, services); + } semanticError(ctx, "Could not find (program) variable or constant %s", varfuncName); return null; } @@ -323,6 +334,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, services); + } // 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 +381,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; @@ -408,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/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/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index d9454ff4591..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 @@ -7,11 +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.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; @@ -22,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: @@ -56,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, services); + } else { + sort = sorts().lookup(ctx.name.getText()); + genericParams = null; + } for (KeYParser.Datatype_constructorContext constructorContext : ctx .datatype_constructor()) { Name name = new Name(constructorContext.name.getText()); @@ -67,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)), services); + } + } if (alreadyDefinedFn != null && (!alreadyDefinedFn.sort().equals(argSort) || !alreadyDefinedFn.argSorts().equals(ImmutableList.of(sort)))) { @@ -87,20 +114,39 @@ 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; } @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()) { @@ -117,15 +163,37 @@ 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); } } 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) { @@ -142,6 +210,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; @@ -159,13 +229,33 @@ 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); } } 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/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 7964520a468..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 @@ -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; @@ -30,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; @@ -249,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, services); + } 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); } } @@ -299,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))); @@ -338,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()); @@ -357,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(), services); + } + + 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(), services); + } 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(); @@ -374,35 +408,45 @@ 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) { + 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(); @@ -415,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 @@ -428,18 +480,18 @@ 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 = functions().lookup(context.name.getText()); + 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()]; 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() @@ -449,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)); @@ -459,15 +512,19 @@ 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) { + KeYParser.Datatype_declContext ctx, Sort sort) { final var tb = services.getTermBuilder(); final String prefix = ctx.name.getText() + "_"; @@ -476,8 +533,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)); @@ -487,17 +545,16 @@ 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())); + b.setDisplayName(String.format("DT %s case distinction", sort.name())); var phi = declareSchemaVariable(ctx, "var", sort, false, false, false, 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()); @@ -656,8 +713,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/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/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index 5316abdbed6..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,6 +925,10 @@ public static TacletApp constructInsts(@NonNull TacletApp app, Goal currGoal, } String value = s.substring(eq + 1); + int colon = value.lastIndexOf(':'); + if (colon != -1 && value.charAt(colon - 1) != ':') { + value = value.substring(0, colon); + } app = parseSV2(app, sv, value, currGoal); } @@ -962,6 +966,8 @@ public static JTerm parseTerm(String value, Proof proof, Namespace 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.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 272054ea35b..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 @@ -36,6 +36,8 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; /** * visitor for method {@link JTerm#execPostOrder(Visitor)}. Called with that @@ -274,7 +276,7 @@ private ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op) { private Operator instantiateModality(JModality op, JavaBlock jb) { JModality.JavaModalityKind kind = op.kind(); if (op.kind() instanceof ModalOperatorSV) { - kind = (JModality.JavaModalityKind) svInst.getInstantiation(op.kind()); + kind = svInst.getInstantiation(op.kind()); } if (jb != op.programBlock() || kind != op.kind()) { return JModality.getModality(kind, jb); @@ -286,13 +288,15 @@ private Operator instantiateOperator(Operator p_operatorToBeInstantiated, JavaBl Operator instantiatedOp = p_operatorToBeInstantiated; if (p_operatorToBeInstantiated instanceof SortDependingFunction sortDependingFunction) { instantiatedOp = handleSortDependingSymbol(sortDependingFunction); + } else if (p_operatorToBeInstantiated instanceof ParametricFunctionInstance pfi) { + instantiatedOp = handleParametricFunction(pfi); } else if (p_operatorToBeInstantiated instanceof ElementaryUpdate elementaryUpdate) { instantiatedOp = instantiateElementaryUpdate(elementaryUpdate); } else if (p_operatorToBeInstantiated instanceof JModality mod) { instantiatedOp = instantiateModality(mod, jb); } else if (p_operatorToBeInstantiated instanceof SchemaVariable opAsSV) { if (!(p_operatorToBeInstantiated instanceof ProgramSV opAsPSV) || !opAsPSV.isListSV()) { - instantiatedOp = (Operator) svInst.getInstantiation(opAsSV); + instantiatedOp = svInst.getInstantiation(opAsSV); } } assert instantiatedOp != null; @@ -310,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(); @@ -411,6 +415,16 @@ private Operator handleSortDependingSymbol(SortDependingFunction depOp) { return res; } + private Operator handleParametricFunction(ParametricFunctionInstance pfi) { + ImmutableList 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, services); + } + 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/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index 9898de0aba3..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 @@ -658,12 +687,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); } @@ -713,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.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..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 @@ -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(instMap, services); + } + + @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..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; @@ -59,7 +61,7 @@ public static GenericSortInstantiations create( ImmutableList p_conditions, LogicServices services) { ImmutableList sorts = ImmutableSLList.nil(); - GenericSortCondition c; + ImmutableList c; final Iterator it; @@ -75,8 +77,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 +116,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 +129,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", @@ -172,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/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/MatchGenericSortInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchGenericSortInstruction.java index 1c8d4d20018..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 @@ -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,14 @@ 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.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/logic/sort/TestParametricSorts.java b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java new file mode 100644 index 00000000000..da218ebe9f2 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java @@ -0,0 +1,144 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.logic.sort; + +import de.uka.ilkd.key.java.Recoder2KeY; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.GenericParameter; +import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.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.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 { + 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, services); + 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, services); + nss.functions().add(someConst); + + var listOfInt = + 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, services); + 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)), + 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)), + new ImmutableArray<>(listOfG1), g1, null, false, true, false); + nss.parametricFunctions().add(head); + + var headInst = + ParametricFunctionInstance.get(head, ImmutableList.of(new GenericArgument(intSort)), + services); + 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()); + } +} 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?)."); 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..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,10 @@ 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"); // use for debugging purposes. // c.keep("VSTTE10"); 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.ui/examples/standard_key/adt/dt_polymorphic.key b/key.ui/examples/standard_key/adt/dt_polymorphic.key new file mode 100644 index 00000000000..d5ff8f58a8e --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.key @@ -0,0 +1,72 @@ +// 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; + \generic F; + 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]>)))}; + + // 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 ) +} \ No newline at end of file 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..cd47b69b6eb --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_polymorphic.proof @@ -0,0 +1,162 @@ +\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_ON", + "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; + \generic F; + 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]>)))}; + + // 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 +} + +\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]>(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)) + (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: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)) + (builtin "One Step Simplification" (formula "2") (userinteraction)) + (rule "closeTrue" (formula "2") (userinteraction)) +) +(branch "Use case of List" + (rule "closeAntec" (formula "1") (ifseqformula "2") (userinteraction)) +) +) +} 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{ 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..7d32a4de6b8 --- /dev/null +++ b/key.ui/examples/standard_key/polymorphic/pseq.key @@ -0,0 +1,703 @@ +\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<[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)) + -> + \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) +} + +\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 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; + } }