Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/hs-backend-booster

.github/workflows/test-pr.yml

@@ -30,26 +30,23 @@ jobs:
           fi
 
   format-check:
-    name: 'Check Java code formatting'
+    name: 'Check code formatting'
     runs-on: ubuntu-latest
     needs: version-sync
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
         with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          # fetch-depth 0 means deep clone the repo
-          fetch-depth: 0
+          submodules: recursive
       - name: 'Set up Java 17'
         uses: actions/setup-java@v3
         with:
           distribution: 'zulu'
           java-version: 17
+      - name: 'Install Maven'
+        run: sudo apt-get update && sudo apt-get install --yes maven
       - name: 'Check code is formatted correctly'
-        uses: axel-op/googlejavaformat-action@v3
-        with:
-          version: v1.18.1
-          args: "--dry-run --set-exit-if-changed"
+        run: mvn spotless:check --batch-mode -U
 
   test-k:
     name: 'K Tests'
@@ -68,7 +65,7 @@ jobs:
           distro: jammy
           llvm: 15
       - name: 'Build and Test K'
-        run: docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'mvn verify --batch-mode -U'
+        run: docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'mvn verify -Dspotless.check.skip=true --batch-mode -U'
       - name: 'Check out k-exercises'
         uses: actions/checkout@v3
         with:

flake.nix

@@ -62,7 +62,7 @@
 
             k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-515qtUCNyqq+PchTLObbb4FtlHjtmTAnI+MDidjiENE=";
+                mvnHash = "sha256-AMxXqu1bbpnmsmLTizNw1n2llSdvx6AuNZRGUHqPn14=";
                 manualMvnArtifacts = [
                   "org.scala-lang:scala-compiler:2.12.18"
                   "ant-contrib:ant-contrib:1.0b3"

k-distribution/include/kframework/builtin/domains.md

@@ -1932,7 +1932,7 @@ module STRING-BUFFER-IN-K [symbolic]
   syntax StringBuffer ::= String
   syntax String ::= StringBuffer2String ( StringBuffer ) [function, total]
 
-  rule {SB:String +String S:String}<:StringBuffer => (SB +String S)::String
+  rule {SB:String +String S:String}::StringBuffer => (SB +String S)::String
   rule .StringBuffer => ""
   rule StringBuffer2String(S:String) => S
 endmodule

k-distribution/include/kframework/builtin/kast.md

@@ -387,7 +387,7 @@ module AUTO-CASTS
   // generates, for all sorts, productions of the form:
   // Sort  ::= Sort ":Sort"  // semantic cast - force the inner term to be `Sort` or a subsort
   // Sort  ::= Sort "::Sort" // strict cast - force the inner term to be exactly `Sort`. Useful for disambiguation
-  // Sort ::= "{" Sort "}" "<:Sort" // synonym for strict cast
+  // Sort ::= "{" Sort "}" "::Sort" // synonym for strict cast
   // Sort  ::= "{" K "}"    ":>Sort" // projection cast. Allows any term to be placed in a context that expects `Sort`
   // this is part of the mechanism that allows concrete user syntax in K
 endmodule

k-distribution/include/kframework/ktest.mak

@@ -53,7 +53,7 @@ ifeq ($(UNAME), Darwin)
 endif
 
 KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked
-KPROVE_FLAGS+=--no-exc-wrap
+KPROVE_FLAGS+=--no-exc-wrap --type-inference-mode checked
 KRUN_FLAGS+=--no-exc-wrap
 
 KRUN_OR_LEGACY=$(KRUN)

k-distribution/k-tutorial/1_basic/11_casts/README.md

@@ -94,16 +94,18 @@ example, consider the following definition:
 module LESSON-11-C
   imports INT
 
-  syntax Exp ::= Int | Exp "+" Exp [group(exp)]
-  syntax Exp2 ::= Exp | Exp2 "+" Exp2 [group(exp2)]
+  syntax Exp ::= Int
+               | "add[" Exp "," Exp "]"   [group(exp)]
+  syntax Exp2 ::= Exp
+               | "add[" Exp2 "," Exp2 "]" [group(exp2)]
 endmodule
 ```
 
 This grammar is a little ambiguous and contrived, but it serves to demonstrate
 how a semantic cast might be insufficient to disambiguate a term. If we were
-to write the term `(I1:Int + I2:Int):Exp2`, the term would be ambiguous,
+to write the term `add[ I1:Int , I2:Int ]:Exp2`, the term would be ambiguous,
 because the cast is not sufficiently strict to determine whether you mean
-to derive the "+" production in the group `exp` or the one in the group `exp2`.
+to derive the "add" production defined in group `exp` or the one in group `exp2`.
 
 In this situation, there is a solution: the **strict cast**. For every sort
 `S` in your grammar, K also defines the following production:
@@ -120,9 +122,39 @@ in the **type system** of K: namely, the term inside the cast cannot be a
 `syntax S ::= S2` exists.
 
 As a result, if we were to write in the above grammar the term
-`(I1:Int + I2:Int)::Exp2`, then we would know that the second derivation above
+`add[ I1:Int , I2:Int ]::Exp2`, then we would know that the second derivation above
 should be chosen, whereas if we want the first derivation, we could write
-`(I1:Int + I2:Int)::Exp`.
+`add[ I1:Int , I2:Int ]::Exp`.
+
+Care must be taken when using a strict cast with brackets. For example, consider a
+similar grammar but using an infix "+":
+
+```k
+module LESSON-11-D
+  imports INT
+
+  syntax Exp ::= Int
+               | Exp "+" Exp   [group(exp)]
+  syntax Exp2 ::= Exp
+               | Exp2 "+" Exp2 [group(exp2)]
+               | "(" Exp2 ")"  [bracket]
+endmodule
+```
+
+The term `I1:Int + I2:Int` is ambiguous and could refer to either the production
+in group `exp` or the one in group `exp2`. To differentiate, you might try to write
+`(I1:Int + I2:Int)::Exp2` similarly to the previous example.
+
+Unfortunately though, this is still ambiguous. Here, the strict cast `::Exp2` applies
+directly to the brackets themselves rather than the underlying term within those brackets.
+As a result, it enforces that `(I1:Int + I2:Int)` cannot be a strict subsort of `Exp2`, but
+it has no effect on the sort of the subterm `I1:Int + I2:Int`.
+
+For cases like this, K provides an alternative syntax for strict casts:
+```
+  syntax S ::= "{" S "}::S"
+```
+The ambiguity can then be resolved with `{I1:Int + I2:Int}::Exp` or `{I1:Int + I2:Int}::Exp2`.
 
 ### Projection casts
 
@@ -162,7 +194,7 @@ inserted into the code that runs when the rule applies.
 For example, here is a module that makes use of projection casts:
 
 ```k
-module LESSON-11-D
+module LESSON-11-E
   imports INT
   imports BOOL
 
@@ -186,12 +218,12 @@ the projection cast will fail.
 
 ## Exercises
 
-1. Extend the `eval` function in `LESSON-11-D` to include Strings and add a `.`
+1. Extend the `eval` function in `LESSON-11-E` to include Strings and add a `.`
 operator which concatenates them.
 
 2. Modify your solution from Lesson 1.9, Exercise 2 by using an `Exp` sort to
 express the integer and Boolean expressions that it supports, in the same style
-as `LESSON-11-D`. Then write an `eval` function that evaluates all terms of
+as `LESSON-11-E`. Then write an `eval` function that evaluates all terms of
 sort `Exp` to either a `Bool` or an `Int`.
 
 ## Next lesson

k-distribution/k-tutorial/1_basic/13_rewrite_rules/README.md

@@ -117,7 +117,7 @@ Haskell Backend which performs **symbolic execution**.
 ### Exercise
 
 Pass a program containing no functions to `krun`. You can use a term of sort
-`Exp` from `LESSON-11-D`. Observe the output and try to understand why you get
+`Exp` from `LESSON-11-E`. Observe the output and try to understand why you get
 the output you do. Then write two rules that rewrite that program to another.
 Run `krun --search` on that program and observe both results. Then add a third
 rule that rewrites one of those results again. Test that that rule applies as

k-distribution/k-tutorial/1_basic/commands.sh

@@ -32,6 +32,7 @@ kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11
 kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-B --syntax-module LESSON-11-B --output-definition build/11b
 kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-C --syntax-module LESSON-11-C --output-definition build/11c
 kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-D --syntax-module LESSON-11-D --output-definition build/11d
+kompile 11_casts/README.md --md-selector "k & ! exclude" --main-module LESSON-11-E --syntax-module LESSON-11-E --output-definition build/11e
 kompile 12_syntactic_lists/README.md --md-selector "k & ! exclude" --main-module LESSON-12-A --output-definition build/12a
 kompile 12_syntactic_lists/README.md --md-selector "k & ! exclude" --main-module LESSON-12-B --output-definition build/12b
 kompile 12_syntactic_lists/README.md --md-selector "k & ! exclude" --main-module LESSON-12-C --syntax-module LESSON-12-C --output-definition build/12c

k-distribution/src/test/scala/org/kframework/backend/kore/ClaimAttributes.scala

@@ -10,24 +10,31 @@ import org.kframework.parser.kore._
 class ClaimAttributes extends KoreTest {
 
   @Test def test() {
-    val definition = this.kompile("module TEST [all-path] configuration <k> $PGM:K </k> syntax Exp ::= \"a\" | \"b\" " +
-      "rule a => b [one-path] " +
-      "rule a => b [all-path] " +
-      "rule a => b " +
-      "endmodule")
+    val definition = this.kompile(
+      "module TEST [all-path] configuration <k> $PGM:K </k> syntax Exp ::= \"a\" | \"b\" " +
+        "rule a => b [one-path] " +
+        "rule a => b [all-path] " +
+        "rule a => b " +
+        "endmodule"
+    )
     val claims = this.claims(definition)
     assertEquals(3, claims.size)
     var one_path = 0
     var all_path = 0
-    for (claim <- claims)  {
+    for (claim <- claims)
       if (this.hasAttribute(claim.att, Att.ONE_PATH.key)) {
-        one_path=one_path+1;
-        assertEquals(KLabels.RL_wEF.name, claim.pattern.asInstanceOf[Implies]._2.asInstanceOf[Application].head.ctr);
+        one_path = one_path + 1;
+        assertEquals(
+          KLabels.RL_wEF.name,
+          claim.pattern.asInstanceOf[Implies]._2.asInstanceOf[Application].head.ctr
+        );
       } else {
-        assertEquals(KLabels.RL_wAF.name, claim.pattern.asInstanceOf[Implies]._2.asInstanceOf[Application].head.ctr);
-        all_path=all_path+1;
+        assertEquals(
+          KLabels.RL_wAF.name,
+          claim.pattern.asInstanceOf[Implies]._2.asInstanceOf[Application].head.ctr
+        );
+        all_path = all_path + 1;
       }
-    }
     assertEquals(1, one_path);
     assertEquals(2, all_path);
   }