Merge branch 'develop' into inner-cast

.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/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);
   }

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

@@ -1,30 +1,29 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.backend.kore
 
+import java.io.File
+import java.nio.file.Files
 import org.kframework.compile.Backend
 import org.kframework.kompile.Kompile
 import org.kframework.kompile.KompileOptions
 import org.kframework.main.GlobalOptions
 import org.kframework.main.Tool
+import org.kframework.parser.kore._
+import org.kframework.parser.kore.implementation.{ DefaultBuilders => B }
+import org.kframework.parser.kore.parser.TextToKore
 import org.kframework.utils.errorsystem.KExceptionManager
 import org.kframework.utils.file.FileUtil
+import org.kframework.utils.options.InnerParsingOptions
 import org.kframework.utils.options.OuterParsingOptions
-import org.kframework.parser.kore._
-import org.kframework.parser.kore.implementation.{DefaultBuilders => B}
-import org.kframework.parser.kore.parser.TextToKore
 import org.kframework.utils.Stopwatch
-import org.kframework.utils.options.InnerParsingOptions
-
-import java.io.File
-import java.nio.file.Files
 
 class KoreTest {
 
   val global: GlobalOptions = new GlobalOptions()
 
   val files: FileUtil = {
     val tempRoot = Files.createTempDirectory("kore-test").toFile
-    val tempDir = new File(tempRoot, "tmp")
+    val tempDir  = new File(tempRoot, "tmp")
     tempDir.mkdirs()
     val kompiledDir = new File(tempRoot, "kompiled")
     kompiledDir.mkdirs()
@@ -41,29 +40,45 @@ class KoreTest {
 
   def kompile(k: String): Definition = {
     val go = new GlobalOptions();
-    val compiler = new Kompile(options, new OuterParsingOptions(), new InnerParsingOptions(), go, files, kem, new Stopwatch(go), false)
+    val compiler = new Kompile(
+      options,
+      new OuterParsingOptions(),
+      new InnerParsingOptions(),
+      go,
+      files,
+      kem,
+      new Stopwatch(go),
+      false
+    )
     val backend = new KoreBackend(options, files, kem, Tool.KOMPILE)
     files.saveToDefinitionDirectory("test.k", k)
-    val defn = compiler.run(files.resolveDefinitionDirectory("test.k"), "TEST", "TEST", backend.steps, backend.excludedModuleTags)
+    val defn = compiler.run(
+      files.resolveDefinitionDirectory("test.k"),
+      "TEST",
+      "TEST",
+      backend.steps,
+      backend.excludedModuleTags
+    )
     backend.accept(new Backend.Holder(defn))
     new TextToKore().parse(files.resolveDefinitionDirectory("test.kore"))
   }
 
-  def axioms(defn: Definition): Seq[AxiomDeclaration] = {
-    defn.modules.flatMap(_.decls.filter(_.isInstanceOf[AxiomDeclaration]).map(_.asInstanceOf[AxiomDeclaration]))
-  }
+  def axioms(defn: Definition): Seq[AxiomDeclaration] =
+    defn.modules.flatMap(
+      _.decls.filter(_.isInstanceOf[AxiomDeclaration]).map(_.asInstanceOf[AxiomDeclaration])
+    )
 
   def axioms(k: String): Seq[AxiomDeclaration] = axioms(kompile(k))
 
-  def claims(defn: Definition): Seq[ClaimDeclaration] = {
-    defn.modules.flatMap(_.decls.filter(_.isInstanceOf[ClaimDeclaration]).map(_.asInstanceOf[ClaimDeclaration]))
-  }
+  def claims(defn: Definition): Seq[ClaimDeclaration] =
+    defn.modules.flatMap(
+      _.decls.filter(_.isInstanceOf[ClaimDeclaration]).map(_.asInstanceOf[ClaimDeclaration])
+    )
 
   def claims(k: String): Seq[ClaimDeclaration] = claims(kompile(k))
 
-  def hasAttribute(attributes: Attributes, name : String) : Boolean = {
+  def hasAttribute(attributes: Attributes, name: String): Boolean =
     attributes.patterns.exists { case p: Application => p.head.ctr == name }
-  }
 
   // get the rewrite associated with a rule or equational axiom
   //
@@ -77,47 +92,65 @@ class KoreTest {
   // \implies(\and(_, \top), \and(\equals(lhs, rhs), _))
   // \equals(lhs, rhs)
   def getRewrite(axiom: AxiomDeclaration): Option[GeneralizedRewrite] = {
-    def go(pattern: Pattern): Option[GeneralizedRewrite] = {
+    def go(pattern: Pattern): Option[GeneralizedRewrite] =
       pattern match {
-        case And(_, Equals(_, _, _, _) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
+        case And(
+              _,
+              Equals(_, _, _, _) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()
+            ) =>
+          Some(rw)
         case And(_, Top(_) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw)
-        case Rewrites(s, And(_, Equals(_, _, _, _) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
-        case Rewrites(s, And(_, Top(_) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r))
-        case Implies(_, Equals(_, _, _, _), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
-        case Implies(_, Top(_), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
-        case Implies(_, And(_, _ +: Equals(_, _, _, _) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
-        case Implies(_, And(_, _ +: Top(_) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq)
+        case Rewrites(s, And(_, Equals(_, _, _, _) +: l +: Seq()), And(_, _ +: r +: Seq())) =>
+          Some(B.Rewrites(s, l, r))
+        case Rewrites(s, And(_, Top(_) +: l +: Seq()), And(_, _ +: r +: Seq())) =>
+          Some(B.Rewrites(s, l, r))
+        case Implies(
+              _,
+              Equals(_, _, _, _),
+              And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())
+            ) =>
+          Some(eq)
+        case Implies(_, Top(_), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) =>
+          Some(eq)
+        case Implies(
+              _,
+              And(_, _ +: Equals(_, _, _, _) +: Seq()),
+              And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())
+            ) =>
+          Some(eq)
+        case Implies(
+              _,
+              And(_, _ +: Top(_) +: Seq()),
+              And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())
+            ) =>
+          Some(eq)
         case eq @ Equals(_, _, Application(_, _), _) => Some(eq)
-        case _ => None
+        case _                                       => None
 
       }
-    }
     go(axiom.pattern)
   }
 
-  private def isConcrete(symbol: SymbolOrAlias) : Boolean = {
+  private def isConcrete(symbol: SymbolOrAlias): Boolean =
     symbol.params.forall(_.isInstanceOf[CompoundSort])
-  }
 
-  def symbols(pat: Pattern): Seq[SymbolOrAlias] = {
+  def symbols(pat: Pattern): Seq[SymbolOrAlias] =
     pat match {
-      case And(_, ps) => ps.flatMap(symbols)
-      case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
-      case Ceil(_, _, p) => symbols(p)
+      case And(_, ps)           => ps.flatMap(symbols)
+      case Application(s, ps)   => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
+      case Ceil(_, _, p)        => symbols(p)
       case Equals(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
-      case Exists(_, _, p) => symbols(p)
-      case Floor(_, _, p) => symbols(p)
-      case Forall(_, _, p) => symbols(p)
-      case Iff(_, p1, p2) => symbols(p1) ++ symbols(p2)
-      case Implies(_, p1, p2) => symbols(p1) ++ symbols(p2)
-      case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
+      case Exists(_, _, p)      => symbols(p)
+      case Floor(_, _, p)       => symbols(p)
+      case Forall(_, _, p)      => symbols(p)
+      case Iff(_, p1, p2)       => symbols(p1) ++ symbols(p2)
+      case Implies(_, p1, p2)   => symbols(p1) ++ symbols(p2)
+      case Mem(_, _, p1, p2)    => symbols(p1) ++ symbols(p2)
 //      case Next(_, p) => symbols(p)
-      case Not(_, p) => symbols(p)
-      case Or(_, ps) => ps.flatMap(symbols)
+      case Not(_, p)           => symbols(p)
+      case Or(_, ps)           => ps.flatMap(symbols)
       case Rewrites(_, p1, p2) => symbols(p1) ++ symbols(p2)
-      case _ => Seq()
+      case _                   => Seq()
     }
-  }
-
 
 }

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

@@ -1,22 +1,22 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.backend.kore
 
-import org.kframework.parser.kore.implementation.{DefaultBuilders => B}
-
-import org.junit.Test
 import org.junit.Assert._
+import org.junit.Test
+import org.kframework.parser.kore.implementation.{ DefaultBuilders => B }
 
 class NoAppendIT extends KoreTest {
 
   @Test def test() {
-    val axioms = this.axioms("module TEST imports K-EQUAL imports DEFAULT-STRATEGY configuration <k> $PGM:K </k> <s/> endmodule")
+    val axioms = this.axioms(
+      "module TEST imports K-EQUAL imports DEFAULT-STRATEGY configuration <k> $PGM:K </k> <s/> endmodule"
+    )
     for (axiom <- axioms) {
       val rewrite = getRewrite(axiom)
       if (rewrite.isDefined) {
         val lhs = rewrite.get.getLeftHandSide
-        for (pat <- lhs) {
+        for (pat <- lhs)
           assertFalse(symbols(pat).contains(B.SymbolOrAlias("append", Seq())))
-        }
       }
     }
   }

kore/build.sbt

@@ -3,9 +3,9 @@
 net.virtualvoid.sbt.graph.Plugin.graphSettings
 
 libraryDependencies ++= Seq(
-  "org.scalacheck" %% "scalacheck" % "1.11.4" % "test",
-  "com.novocode" % "junit-interface" % "0.9" % "test",
-   "junit" % "junit" % "4.11" % "test"
+  "org.scalacheck" %% "scalacheck"      % "1.11.4" % "test",
+  "com.novocode"    % "junit-interface" % "0.9"    % "test",
+  "junit"           % "junit"           % "4.11"   % "test"
 )
 
 EclipseKeys.withSource := true

kore/project/build.sbt

@@ -1,6 +1,6 @@
 // Copyright (c) 2014-2019 K Team. All Rights Reserved.
 
-resolvers += "Sonatype snapshots" at "https://oss.sonatype.org/content/repositories/snapshots/"
+resolvers += "Sonatype snapshots".at("https://oss.sonatype.org/content/repositories/snapshots/")
 
 addSbtPlugin("com.github.shivawu" %% "sbt-maven-plugin" % "0.1.3-SNAPSHOT")