Merge branch 'main' into weigl/abbrevmgr

.gitignore

@@ -65,5 +65,8 @@ key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/solvers.txt
 key/key.ui/examples/**/**.proof
 **/testresults/**
 
+# generated by the antlr plugin of IntelliJ
+key.core/src/main/antlr4/gen/
+
 scripts/tools/checkstyle/key_checks_incremental.xml
 checkstyle-diff.txt

build.gradle

@@ -21,7 +21,7 @@ plugins {
     // id "com.github.ben-manes.versions" version "0.39.0"
 
     // Code formatting
-    id "com.diffplug.spotless" version "6.23.0"
+    id "com.diffplug.spotless" version "6.25.0"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -70,9 +70,9 @@ subprojects {
     }
 
     dependencies {
-        implementation("org.slf4j:slf4j-api:2.0.9")
+        implementation("org.slf4j:slf4j-api:2.0.11")
 
-        testImplementation("ch.qos.logback:logback-classic:1.4.12")
+        testImplementation("ch.qos.logback:logback-classic:1.4.14")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.1'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.1'
         testImplementation project(':key.util')

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java

@@ -0,0 +1,8 @@
+/**
+ * RIFL is short for "Requirements for Information Flow Language",
+ * a tool-indepentent specification language developed in the RS3 project.
+ * The RIFL/Java dialect is documented in XXX.
+ * This package contains a transformer from input RIFL files (XML) and
+ * original Java files to JML* annotated files.
+ */
+package de.uka.ilkd.key.util.rifl;

key.core/src/main/antlr4/KeYLexer.g4

@@ -185,6 +185,7 @@ PROFILE : '\\profile';
 TRUE : 'true';
 FALSE : 'false';
 
+
 // Keywords related to taclets
 SAMEUPDATELEVEL : '\\sameUpdateLevel';
 INSEQUENTSTATE : '\\inSequentState';
@@ -207,8 +208,10 @@ AVOID : '\\avoid';
 
 PREDICATES : '\\predicates';
 FUNCTIONS : '\\functions';
+DATATYPES : '\\datatypes';
 TRANSFORMERS : '\\transformers';
 UNIQUE : '\\unique';
+FREE : '\\free';
 
 RULES : '\\rules';
 AXIOMS : '\\axioms';

key.core/src/main/antlr4/KeYParser.g4

@@ -27,6 +27,7 @@ decls
     | pred_decls
     | func_decls
     | transform_decls
+    | datatype_decls
     | ruleset_decls
     | contracts             // for problems
     | invariants            // for problems
@@ -229,6 +230,36 @@ func_decl
   SEMI
 ;
 
+/**
+\datatypes {
+ \free List = Nil | Cons(any head, List tail);
+}
+*/
+datatype_decls:
+  DATATYPES LBRACE datatype_decl* RBRACE
+;
+
+datatype_decl:
+  doc=DOC_COMMENT?
+  // weigl: all datatypes are free!
+  // FREE?
+  name=simple_ident
+  EQUALS
+  datatype_constructor (OR datatype_constructor)*
+  SEMI
+;
+
+datatype_constructor:
+  name=simple_ident
+  (
+    LPAREN
+    (argSort+=sortId argName+=simple_ident
+     (COMMA argSort+=sortId argName+=simple_ident)*
+    )?
+    RPAREN
+  )?
+;
+
 func_decls
     :
         FUNCTIONS
@@ -267,6 +298,7 @@ transform_decl
     SEMI
 ;
 
+
 transform_decls:
     TRANSFORMERS LBRACE (transform_decl)* RBRACE
 ;

key.core/src/main/java/de/uka/ilkd/key/java/abstraction/package-info.java

@@ -0,0 +1,19 @@
+/**
+ * This package contains the metamodel abstractions as used by the
+ * semantical services. The {@link recoder.abstraction.ProgramModelElement}s
+ * hide the origin of the information, be it from Java source code,
+ * Java byte code, or predefined lacking any syntactical representation.
+ * <p>
+ * There are three implicitly defined entities -
+ * {@link recoder.abstraction.ArrayType},
+ * {@link recoder.abstraction.DefaultConstructor}, and
+ * {@link recoder.abstraction.Package}, as well as the predefined
+ * types {@link recoder.abstraction.NullType} and the base class for
+ * the small number of {@link recoder.abstraction.PrimitiveType}s.
+ * <p>
+ * {@link recoder.abstraction.Scope}s are attached to
+ * {@link recoder.abstraction.ScopeDefiningElement}s by
+ * {@link recoder.service.SourceInfo} implementations and should
+ * not be modified from others.
+ */
+package de.uka.ilkd.key.java.abstraction;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/package-info.java

@@ -0,0 +1,6 @@
+/**
+ * This package collects all Java modifiers. The sole abstraction beneath
+ * the parent {@link recoder.java.declaration.Modifier} is the
+ * {@link recoder.java.declaration.modifier.VisibilityModifier}.
+ */
+package de.uka.ilkd.key.java.declaration.modifier;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/package-info.java

@@ -0,0 +1,11 @@
+/**
+ * Elements of the Java syntax tree representing declarations.
+ * For each declaration, there exists a corresponding
+ * {@link recoder.java.Reference} in the {@link recoder.java.reference}
+ * package.
+ * Each {@link recoder.java.Declaration}
+ * provides some convenience methods that query the possible modifiers.
+ * The modifiers themselves are collected in the subpackage
+ * {@link recoder.java.declaration.modifier}.
+ */
+package de.uka.ilkd.key.java.declaration;

key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/package-info.java

@@ -0,0 +1,7 @@
+/**
+ * This package contains representations for the various Java literal types.
+ * Quite special are the non-primitive
+ * {@link recoder.java.expression.literal.NullLiteral} and
+ * {@link recoder.java.expression.literal.StringLiteral}.
+ */
+package de.uka.ilkd.key.java.expression.literal;

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/package-info.java

@@ -0,0 +1,7 @@
+/**
+ * Elements of the Java syntax tree representing operators and operator-like
+ * expressions.
+ * {@link recoder.java.expression.operator.New} is also considered an
+ * operator ({@link recoder.java.expression.operator.TypeOperator}).
+ */
+package de.uka.ilkd.key.java.expression.operator;

key.core/src/main/java/de/uka/ilkd/key/java/expression/package-info.java

@@ -0,0 +1,6 @@
+/**
+ * Elements of the Java syntax tree representing expressions.
+ * The various operators and literals are bundled in the corresponding
+ * subpackages.
+ */
+package de.uka.ilkd.key.java.expression;