diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index f1a67a2afd5..c6b65084de5 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -82,6 +82,7 @@ CAPTURES: 'captures' Pred -> pushMode(expr); CODE: 'code'; //? CONSTRAINT: 'constraint' Pred -> pushMode(expr); CONTINUES: 'continues' -> pushMode(expr); +DATATYPE: 'datatype'; DEBUG: 'debug'; //? DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr); DETERMINES: 'determines' -> pushMode(expr); @@ -143,6 +144,7 @@ C_IDENT: '\\'? LETTER (LETTERORDIGIT)* -> type(IDENT); C_COLON: ':' -> type(COLON); C_DOT: '.' -> type(DOT); C_COMMA: ',' -> type(COMMA); +C_INCLUSIVEOR: '|' -> type(INCLUSIVEOR); SL_COMMENT: {jmlMarkerDecision.isComment("//")}? ('//' ('\n'|'\r'|EOF) | '//' ~'@' ~('\n'|'\r')*) -> channel(HIDDEN); ML_COMMENT: {jmlMarkerDecision.isComment("/*")}? '/*' -> more, pushMode(mlComment); diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index a66965df0fd..ff3b91d889f 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -22,6 +22,7 @@ classlevel_element | monitors_for_clause | readable_if_clause | writable_if_clause | datagroup_clause | set_statement | nowarn_pragma | accessible_clause | assert_statement | assume_statement + | datatype_declaration ; methodlevel_comment: (modifiers? methodlevel_element modifiers?)* EOF; @@ -41,7 +42,28 @@ modifier | CODE_JAVA_MATH | CODE_SAFE_MATH | CODE_BIGINT_MATH) ; +datatype_declaration: + DATATYPE + dt_name=IDENT + LBRACE + datatype_constructor (INCLUSIVEOR datatype_constructor)* + SEMI_TOPLEVEL + (datatype_function)* + RBRACE + ; + +datatype_constructor: + con_name=IDENT + ( + LPAREN + (argType+=type argName+=IDENT + (COMMA argType+=type argName+=IDENT)* + )? + RPAREN + )? +; +datatype_function: type IDENT param_list method_body; class_axiom: AXIOM expression SEMI_TOPLEVEL; initially_clause: INITIALLY expression SEMI_TOPLEVEL; 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 3f58e86f071..6844b16ccec 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 @@ -66,7 +66,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { : null; var origin = BuilderHelpers.getPosition(ctx); var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); - sorts().add(s); + sorts().addSafely(s); return null; } 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 69785ef1614..66c3f766022 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,6 +7,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Name; +import de.uka.ilkd.key.logic.Namespace; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.logic.op.SortDependingFunction; @@ -52,16 +53,30 @@ 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(); for (KeYParser.Datatype_constructorContext constructorContext : ctx .datatype_constructor()) { Name name = new Name(constructorContext.name.getText()); Sort[] args = new Sort[constructorContext.sortId().size()]; + var argNames = constructorContext.argName; for (int i = 0; i < args.length; i++) { - args[i] = accept(constructorContext.sortId(i)); + Sort argSort = accept(constructorContext.sortId(i)); + args[i] = argSort; + var argName = argNames.get(i).getText(); + var alreadyDefinedFn = dtNamespace.lookup(argName); + if (alreadyDefinedFn != null + && (!alreadyDefinedFn.sort().equals(argSort) + || !alreadyDefinedFn.argSort(0).equals(sort))) { + throw new RuntimeException("Name already in namespace: " + argName); + } + Function fn = new Function(new Name(argName), argSort, new Sort[] { sort }, null, + false, false); + dtNamespace.add(fn); } Function function = new Function(name, sort, args, null, true, false); - namespaces().functions().add(function); + namespaces().functions().addSafely(function); } + namespaces().functions().addSafely(dtNamespace.allElements()); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index f58f7a4615f..9ba6c08b0f8 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 @@ -243,9 +243,95 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { var tbSplit = createConstructorSplit(ctx); 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); + registerTaclet(ctx, tbDeconstructor); + + var tbDeconsEq = createDeconstructorEQTaclet(constructor, argName, i, dtSort); + registerTaclet(ctx, tbDeconsEq); + } + } + return null; } + private TacletBuilder createDeconstructorTaclet( + KeYParser.Datatype_constructorContext constructor, String argName, int argIndex) { + var tacletBuilder = new RewriteTacletBuilder<>(); + tacletBuilder + .setName(new Name(String.format("%s_Dec_%s", argName, constructor.name.getText()))); + tacletBuilder.setDisplayName( + String.format("%s_Deconstruct_%s", argName, constructor.name.getText())); + + var schemaVariables = new SchemaVariable[constructor.argName.size()]; + var args = new Term[constructor.argName.size()]; + var tb = services.getTermBuilder(); + + // Schema vars for constructor, e.g., Cons(head_sv, tail_sv) + for (int i = 0; i < constructor.argName.size(); i++) { + var name = constructor.argName.get(i).getText() + "_sv"; + Sort sort = accept(constructor.argSort.get(i)); + var sv = declareSchemaVariable(constructor, name, sort, false, false, false, + new SchemaVariableModifierSet.TermSV()); + schemaVariables[i] = sv; + args[i] = tb.var(sv); + } + + var function = namespaces().functions().lookup(argName); + var consFn = namespaces().functions().lookup(constructor.name.getText()); + + // Find, e.g, tail(Cons(head_sv, tail_sv)) + tacletBuilder.setFind(tb.func(function, tb.func(consFn, args))); + tacletBuilder.addTacletGoalTemplate( + new RewriteTacletGoalTemplate(tb.var(schemaVariables[argIndex]))); + tacletBuilder.setApplicationRestriction(RewriteTaclet.SAME_UPDATE_LEVEL); + + return tacletBuilder; + } + + private TacletBuilder createDeconstructorEQTaclet( + KeYParser.Datatype_constructorContext constructor, String argName, int argIndex, + Sort dtSort) { + var tacletBuilder = new RewriteTacletBuilder<>(); + tacletBuilder.setName( + new Name(String.format("%s_DecEQ_%s", argName, constructor.name.getText()))); + tacletBuilder.setDisplayName( + String.format("%s_DeconstructEQ_%s", argName, constructor.name.getText())); + + var schemaVariables = new SchemaVariable[constructor.argName.size()]; + var args = new Term[constructor.argName.size()]; + var tb = services.getTermBuilder(); + + // Schema vars for constructor, e.g., Cons(head_sv, tail_sv) + for (int i = 0; i < constructor.argName.size(); i++) { + var name = constructor.argName.get(i).getText() + "_sv"; + Sort sort = accept(constructor.argSort.get(i)); + var sv = declareSchemaVariable(constructor, name, sort, false, false, false, + new SchemaVariableModifierSet.TermSV()); + schemaVariables[i] = sv; + args[i] = tb.var(sv); + } + + var function = namespaces().functions().lookup(argName); + var consFn = namespaces().functions().lookup(constructor.name.getText()); + + var x = declareSchemaVariable(constructor, argName + "_x", dtSort, false, false, false, + new SchemaVariableModifierSet.TermSV()); + var res = schemaVariables[argIndex]; + + tacletBuilder.setFind(tb.func(function, tb.var(x))); + tacletBuilder.setIfSequent(Sequent.createAnteSequent( + new Semisequent(new SequentFormula(tb.equals(tb.var(x), tb.func(consFn, args)))))); + tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(tb.var(res))); + tacletBuilder.setApplicationRestriction(RewriteTaclet.SAME_UPDATE_LEVEL); + + return tacletBuilder; + } + private TacletBuilder createInductionTaclet( KeYParser.Datatype_declContext ctx) { @@ -359,12 +445,14 @@ private RewriteTacletBuilder createConstructorSplit( KeYParser.Datatype_declContext ctx) { final var tb = services.getTermBuilder(); + final String prefix = ctx.name.getText() + "_"; + Map variables = new HashMap<>(); 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, name, sort, + var sv = declareSchemaVariable(ctx, prefix + name, sort, false, true, false, new SchemaVariableModifierSet.TermSV()); variables.put(name, tb.var(sv)); 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 f0e986b7327..d217367f555 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 @@ -970,6 +970,7 @@ public static ProofCollection automaticJavaDL() throws IOException { g.loadable("standard_key/adt/dt_list_revrev.proof"); 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"); return c; } diff --git a/key.ui/examples/standard_key/adt/dt_list_deconstruct.key b/key.ui/examples/standard_key/adt/dt_list_deconstruct.key new file mode 100644 index 00000000000..e2e0ad56ef9 --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_list_deconstruct.key @@ -0,0 +1,11 @@ +\datatypes { + List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail); +} + +\functions { + List x; +} + +\problem { + Nil = tail(Cons(0, Nil)) & Nil = tail(Cons2(0, Nil)) & (x = Cons(0, Cons(1, Nil)) -> head(x) = 0) +} \ No newline at end of file diff --git a/key.ui/examples/standard_key/adt/dt_list_deconstruct.proof b/key.ui/examples/standard_key/adt/dt_list_deconstruct.proof new file mode 100644 index 00000000000..aa1303ee817 --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_list_deconstruct.proof @@ -0,0 +1,116 @@ +\profile "Java Profile"; + +\settings // Proof-Settings-Config-File +{ + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "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", + "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" : 500, + "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_NONE", + "OSS_OPTIONS_KEY" : "OSS_OFF", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "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" + } + } + } + +\datatypes { + List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail); +} + +\functions { + List x; +} +\problem { + Nil = tail(Cons(Z(0(#)), Nil)) +& Nil = tail(Cons2(Z(0(#)), Nil)) +& ( x = Cons(Z(0(#)), Cons(Z(1(#)), Nil)) + -> head(x) = Z(0(#))) +} + +\proof { +(keyLog "0" (keyUser "daniel" ) (keyVersion "1fb0c10630b493ce138850ae0f9803d3f2fffc51")) + +(autoModeTime "0") + +(branch "dummy ID" +(rule "andRight" (formula "1") (userinteraction)) +(branch "Case 1" + (rule "andRight" (formula "1") (userinteraction)) + (branch "Case 1" + (rule "tail_Dec_Cons" (formula "1") (term "1") (userinteraction)) + (rule "equalUnique" (formula "1") (userinteraction)) + (rule "closeTrue" (formula "1") (userinteraction)) + ) + (branch "Case 2" + (rule "tail_Dec_Cons2" (formula "1") (term "1") (userinteraction)) + (rule "equalUnique" (formula "1") (userinteraction)) + (rule "closeTrue" (formula "1") (userinteraction)) + ) +) +(branch "Case 2" + (rule "impRight" (formula "1") (userinteraction)) + (rule "head_DecEQ_Cons" (formula "2") (term "0") (ifseqformula "1") (userinteraction)) + (rule "equal_literals" (formula "2") (userinteraction)) + (rule "closeTrue" (formula "2") (userinteraction)) +) +) +} diff --git a/key.ui/examples/standard_key/adt/dt_nat.key b/key.ui/examples/standard_key/adt/dt_nat.key index 07a8b6d8845..51bed19f749 100644 --- a/key.ui/examples/standard_key/adt/dt_nat.key +++ b/key.ui/examples/standard_key/adt/dt_nat.key @@ -1,5 +1,5 @@ \datatypes { - \free Nat = zero | succ(Nat pred); + Nat = zero | succ(Nat pred); } \predicates {