Format with minimal configuration

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

@@ -10,22 +10,30 @@ 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);

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

@@ -41,27 +41,46 @@ 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]))
+    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]))
+    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 }
   }
 
@@ -79,45 +98,66 @@ class KoreTest {
   def getRewrite(axiom: AxiomDeclaration): 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] = {
     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

@@ -9,7 +9,9 @@ import org.junit.Assert._
 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) {

kore/build.sbt

@@ -5,7 +5,7 @@ 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"
+  "junit" % "junit" % "4.11" % "test"
 )
 
 EclipseKeys.withSource := true

kore/src/main/scala/org/kframework/POSet.scala

@@ -12,43 +12,50 @@ import scala.annotation.tailrec
  */
 class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
   // convert the input set of relations to Map form for performance
-  private val directRelationsMap: Map[T, Set[T]] = directRelations groupBy { _._1 } mapValues { _ map { _._2 } toSet } map identity
+  private val directRelationsMap: Map[T, Set[T]] = directRelations groupBy { _._1 } mapValues {
+    _ map { _._2 } toSet
+  } map identity
 
   lazy val elements: Set[T] = directRelations.flatMap(a => Set(a._1, a._2))
 
-  lazy val sortedElements: scala.collection.immutable.List[T] = TopologicalSort.tsort(directRelations).toList
+  lazy val sortedElements: scala.collection.immutable.List[T] =
+    TopologicalSort.tsort(directRelations).toList
 
   /**
-   * Internal private method. Computes the transitive closer of the initial relations.
-   * It also checks for cycles during construction and throws an exception if it finds any.
+   * Internal private method. Computes the transitive closer of the initial relations. It also
+   * checks for cycles during construction and throws an exception if it finds any.
    *
-   * The implementation is simple. It links each element to the successors of its successors.
-   * TODO: there may be a more efficient algorithm (low priority)
+   * The implementation is simple. It links each element to the successors of its successors. TODO:
+   * there may be a more efficient algorithm (low priority)
    */
   @tailrec
   private def transitiveClosure(relations: Map[T, Set[T]]): Map[T, Set[T]] = {
-    val newRelations = relations map {
-      case (start, succ) =>
-        val newSucc = succ flatMap { relations.getOrElse(_, Set()) }
-        if (newSucc.contains(start))
-          constructAndThrowCycleException(start, start, Seq())
-        (start, succ | newSucc)
+    val newRelations = relations map { case (start, succ) =>
+      val newSucc = succ flatMap { relations.getOrElse(_, Set()) }
+      if (newSucc.contains(start))
+        constructAndThrowCycleException(start, start, Seq())
+      (start, succ | newSucc)
     }
     if (relations != newRelations) transitiveClosure(newRelations) else relations
   }
 
   /**
    * Recursive method constructing and throwing and the cycle exception.
    *
-   * @param start (or tail) element to look for when constructing the cycle
-   * @param current element
-   * @param path so far
+   * @param start
+   *   (or tail) element to look for when constructing the cycle
+   * @param current
+   *   element
+   * @param path
+   *   so far
    */
   private def constructAndThrowCycleException(start: T, current: T, path: Seq[T]): Unit = {
     val currentPath = path :+ current
     val succs = directRelationsMap.getOrElse(current, Set())
     if (succs.contains(start)) {
-      throw KEMException.compilerError("Illegal circular relation: " + (currentPath :+ start).mkString(" < "))
+      throw KEMException.compilerError(
+        "Illegal circular relation: " + (currentPath :+ start).mkString(" < ")
+      )
     }
     succs foreach { constructAndThrowCycleException(start, _, currentPath) }
   }
@@ -64,7 +71,11 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
    * A map from each element of the poset to the set of elements less than it.
    */
   lazy val relationsOp: Map[T, Set[T]] =
-    relations.toSet[(T, Set[T])].flatMap { case (x, ys) => ys.map(_ -> x) }.groupBy(_._1).mapValues(_.map(_._2))
+    relations
+      .toSet[(T, Set[T])]
+      .flatMap { case (x, ys) => ys.map(_ -> x) }
+      .groupBy(_._1)
+      .mapValues(_.map(_._2))
 
   def <(x: T, y: T): Boolean = relations.get(x).exists(_.contains(y))
   def >(x: T, y: T): Boolean = relations.get(y).exists(_.contains(x))
@@ -76,12 +87,14 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
   def lessThan(x: T, y: T): Boolean = <(x, y)
   def lessThanEq(x: T, y: T): Boolean = x == y || <(x, y)
   def directlyLessThan(x: T, y: T): Boolean = directRelationsMap.get(x).exists(_.contains(y))
+
   /**
    * Returns true if y < x
    */
   def greaterThan(x: T, y: T): Boolean = >(x, y)
   def greaterThanEq(x: T, y: T): Boolean = x == y || >(x, y)
   def directlyGreaterThan(x: T, y: T): Boolean = directRelationsMap.get(y).exists(_.contains(x))
+
   /**
    * Returns true if y < x or y < x
    */
@@ -116,37 +129,37 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
   lazy val minimum: Option[T] =
     if (minimalElements.size == 1) Some(minimalElements.head) else None
 
-  lazy val asOrdering: Ordering[T] = (x: T, y: T) => if (lessThanEq(x, y)) -1 else if (lessThanEq(y, x)) 1 else 0
+  lazy val asOrdering: Ordering[T] = (x: T, y: T) =>
+    if (lessThanEq(x, y)) -1 else if (lessThanEq(y, x)) 1 else 0
 
   /**
-    * Return the subset of items from the argument which are not
-    * less than any other item.
-    */
+   * Return the subset of items from the argument which are not less than any other item.
+   */
   def maximal(sorts: Iterable[T]): Set[T] =
-    sorts.filter(s1 => !sorts.exists(s2 => lessThan(s1,s2))).toSet
+    sorts.filter(s1 => !sorts.exists(s2 => lessThan(s1, s2))).toSet
 
   def maximal(sorts: util.Collection[T]): util.Set[T] =
     Collections.mutable(maximal(Collections.immutable(sorts)))
 
   /**
-    * Return the subset of items from the argument which are not
-    * greater than any other item.
-    */
+   * Return the subset of items from the argument which are not greater than any other item.
+   */
   def minimal(sorts: Iterable[T]): Set[T] =
-    sorts.filter(s1 => !sorts.exists(s2 => >(s1,s2))).toSet
+    sorts.filter(s1 => !sorts.exists(s2 => >(s1, s2))).toSet
 
   def minimal(sorts: util.Collection[T]): util.Set[T] =
     Collections.mutable(minimal(Collections.immutable(sorts)))
 
   override def toString: String = {
-    "POSet(" + (relations flatMap { case (from, tos) => tos map { to => from + "<" + to } }).mkString(",") + ")"
+    "POSet(" + (relations flatMap { case (from, tos) => tos map { to => from + "<" + to } })
+      .mkString(",") + ")"
   }
 
   override def hashCode: Int = relations.hashCode()
 
   override def equals(that: Any): Boolean = that match {
     case that: POSet[_] => relations == that.relations
-    case _ => false
+    case _              => false
   }
 }
 

kore/src/main/scala/org/kframework/RewriterResult.scala

@@ -6,6 +6,8 @@ import java.util.Optional
 /**
  * Created by manasvi on 8/13/15.
  */
-class RewriterResult(val rewriteSteps: Optional[Integer], val exitCode: Optional[Integer], val k: kore.K) {
-
-}
+class RewriterResult(
+    val rewriteSteps: Optional[Integer],
+    val exitCode: Optional[Integer],
+    val k: kore.K
+) {}