Hackeython: ADTs in JML

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);

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;

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;
     }
 

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 @@
         // weigl: all datatypes are free ==> functions are unique!
         // boolean freeAdt = ctx.FREE() != null;
         var sort = sorts().lookup(ctx.name.getText());
+        var dtNamespace = new Namespace<Function>();
         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;
     }
 

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -243,9 +243,95 @@
         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<? extends Taclet> 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<? extends Taclet> 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<? extends Taclet> createInductionTaclet(
             KeYParser.Datatype_declContext ctx) {
@@ -359,15 +445,17 @@
             KeYParser.Datatype_declContext ctx) {
         final var tb = services.getTermBuilder();
 
+        final String prefix = ctx.name.getText() + "_";
+
         Map<String, Term> 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));
             }
         }
 

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;
     }

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)
+}

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))
+)
+)
+}

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 {