Fix various warnings. Update to Scala 2.13.13

matching/pom.xml

@@ -14,8 +14,8 @@
     <java.version>17</java.version>
     <scala-kore.version>0.3.0</scala-kore.version>
     <spotless.version>2.41.1</spotless.version>
-    <scala.majorVersion>2.12</scala.majorVersion>
-    <scala.minorVersion>18</scala.minorVersion>
+    <scala.majorVersion>2.13</scala.majorVersion>
+    <scala.minorVersion>13</scala.minorVersion>
     <scala.version>${scala.majorVersion}.${scala.minorVersion}</scala.version>
     <scalafmt.version>3.7.17</scalafmt.version>
   </properties>
@@ -48,6 +48,11 @@
       <artifactId>scala-reflect</artifactId>
       <version>${scala.version}</version>
     </dependency>
+    <dependency>
+      <groupId>org.scala-lang.modules</groupId>
+      <artifactId>scala-parallel-collections_2.13</artifactId>
+      <version>1.0.4</version>
+    </dependency>
     <dependency>
       <groupId>com.runtimeverification.k</groupId>
       <artifactId>scala-kore</artifactId>

matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala

@@ -21,7 +21,7 @@ case class Empty() extends Constructor {
       case SetS() => SetP(immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq()))
       case MapS() =>
         MapP(immutable.Seq(), immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq()))
-      case _      => ???
+      case _ => ???
     }
   }
   override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
@@ -31,7 +31,7 @@ case class NonEmpty() extends Constructor {
   def name: String                                      = ???
   def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
   def expand(f: Fringe): Option[immutable.Seq[Fringe]]  = Some(immutable.Seq(f))
-  def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = children(0)
+  def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = children.head
   override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
 }
 
@@ -46,27 +46,27 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
         if (isSet) {
           Some(
             immutable.Seq(
-              new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false),
-              new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false)
+              Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false),
+              Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false)
             )
           )
         } else {
           Some(
             immutable.Seq(
-              new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false),
-              new Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), false),
-              new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false)
+              Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false),
+              Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), isExact = false),
+              Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false)
             )
           )
         }
       case Some(k) =>
         if (isSet) {
-          Some(immutable.Seq(new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), f))
+          Some(immutable.Seq(Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false), f))
         } else {
           Some(
             immutable.Seq(
-              new Fringe(f.symlib, sorts(1), Value(k, f.occurrence), false),
-              new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false),
+              Fringe(f.symlib, sorts(1), Value(k, f.occurrence), isExact = false),
+              Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false),
               f
             )
           )
@@ -80,17 +80,17 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
     assert((isSet && children.size == 2) || (!isSet && children.size == 3))
     if (this.key.isEmpty) {
       if (isSet) {
-        key = children(0)
+        key = children.head
       } else {
-        key = children(0)
+        key = children.head
         value = children(1)
       }
     } else {
       if (isSet) {
         key = this.key.get.decanonicalize
       } else {
         key = this.key.get.decanonicalize
-        value = children(0)
+        value = children.head
       }
     }
     def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
@@ -132,7 +132,7 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex
   def isBest(pat: Pattern[Option[Occurrence]]): Boolean = key.isDefined && pat == key.get
   def expand(f: Fringe): Option[immutable.Seq[Fringe]]  = Some(immutable.Seq(f))
   def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
-    val child = children(0)
+    val child = children.head
     def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
       SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k, v))
     def setElement(k: Pattern[String]): Pattern[String] =
@@ -181,7 +181,7 @@ case class ListC(element: SymbolOrAlias, length: Int) extends Constructor {
   def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
   def expand(f: Fringe): Option[immutable.Seq[Fringe]] = {
     val sort = f.symlib.signatures(element)._1.head
-    Some((0 until length).map(i => new Fringe(f.symlib, sort, Num(i, f.occurrence), false)))
+    Some((0 until length).map(i => Fringe(f.symlib, sort, Num(i, f.occurrence), isExact = false)))
   }
   def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
     def element(v: Pattern[String]): Pattern[String] =
@@ -211,7 +211,7 @@ case class SymbolC(sym: SymbolOrAlias) extends Constructor {
       val sorts = f.symlib.signatures(sym)._1
       Some(
         sorts.zipWithIndex.map(t =>
-          new Fringe(f.symlib, t._1, Num(t._2, f.occurrence), sym.ctr == "inj")
+          Fringe(f.symlib, t._1, Num(t._2, f.occurrence), sym.ctr == "inj")
         )
       )
     }

matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala

@@ -48,6 +48,7 @@ object Generator {
         ListP(immutable.Seq(), None, immutable.Seq(), c, SymbolP(sym, immutable.Seq()))
       case (Element(), immutable.Seq(p)) =>
         ListP(immutable.Seq(p), None, immutable.Seq(), c, SymbolP(sym, immutable.Seq(p)))
+      case _ => ???
     }
 
   private def mapPattern(
@@ -76,6 +77,7 @@ object Generator {
         MapP(immutable.Seq(), immutable.Seq(), None, c, SymbolP(sym, immutable.Seq()))
       case (Element(), immutable.Seq(k, v)) =>
         MapP(immutable.Seq(k), immutable.Seq(v), None, c, SymbolP(sym, immutable.Seq(k, v)))
+      case _ => ???
     }
 
   private def setPattern(
@@ -104,6 +106,7 @@ object Generator {
         SetP(immutable.Seq(), None, c, SymbolP(sym, immutable.Seq()))
       case (Element(), immutable.Seq(e)) =>
         SetP(immutable.Seq(e), None, c, SymbolP(sym, immutable.Seq(e)))
+      case _ => ???
     }
 
   private def genPatterns(
@@ -181,18 +184,18 @@ object Generator {
       case _         => immutable.Seq()
     }
 
-  def genClauseMatrix[T](
+  def genClauseMatrix(
       symlib: Parser.SymLib,
       mod: Definition,
       axioms: immutable.IndexedSeq[AxiomInfo],
       sorts: immutable.Seq[Sort]
   ): Matrix = {
     val actions = axioms.map { a =>
-      val lhsVars     = a.rewrite.getLeftHandSide.flatMap(genVars(_))
+      val lhsVars     = a.rewrite.getLeftHandSide.flatMap(genVars)
       val lhsVarNames = lhsVars.map(_.name)
       val rhsVars     = genVars(a.rewrite.getRightHandSide)
-      val scVars      = a.sideCondition.map(genVars(_))
-      new Action(
+      val scVars      = a.sideCondition.map(genVars)
+      Action(
         a.ordinal,
         lhsVars,
         rhsVars.map(_.name).sorted.distinct,
@@ -209,10 +212,11 @@ object Generator {
     }
     val patterns = axioms.map(a => genPatterns(mod, symlib, a.rewrite.getLeftHandSide)).transpose
     val cols =
-      (
-        sorts,
-        if (axioms.isEmpty) sorts.map(_ => immutable.IndexedSeq()) else patterns
-      ).zipped.toIndexedSeq
+      sorts
+        .lazyZip(
+          if (axioms.isEmpty) sorts.map(_ => immutable.IndexedSeq()) else patterns
+        )
+        .toIndexedSeq
     new Matrix(symlib, cols, actions).expand
   }
 
@@ -246,7 +250,7 @@ object Generator {
     val numerator   = originalMatrix.rows.size * threshold._1
     val denominator = finalMatrix.rows.size * threshold._2
     if (Matching.logging) {
-      System.out.println(finalMatrix.rows.size + "/" + originalMatrix.rows.size)
+      System.out.println(finalMatrix.rows.size.toString + "/" + originalMatrix.rows.size.toString)
     }
     numerator <= denominator
   }
@@ -260,7 +264,7 @@ object Generator {
   ): Option[(DecisionTree, immutable.Seq[(P[String], Occurrence)])] = {
     val rhs = genPatterns(mod, symlib, immutable.Seq(axiom.rewrite.getRightHandSide))
     val (specialized, residuals) = matrix.specializeBy(rhs.toIndexedSeq)
-    val residualMap = (residuals, specialized.fringe.map(_.occurrence)).zipped.to[immutable.Seq]
+    val residualMap = residuals.lazyZip(specialized.fringe.map(_.occurrence)).to(immutable.Seq)
     if (Matching.logging) {
       System.out.println("Residuals: " + residualMap.toList)
     }
@@ -269,7 +273,7 @@ object Generator {
       symlib,
       specialized.columns.map(c => new Column(c.fringe.inexact, c.patterns, newClauses)),
       newClauses,
-      false
+      search = false
     )
     if (isPoorlySpecialized(finalMatrix, matrix, threshold)) {
       None

matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala

@@ -82,7 +82,7 @@ object Heuristic {
       allCols: immutable.Seq[MatrixColumn]
   ): immutable.Seq[MatrixColumn] = {
     var result: List[MatrixColumn] = Nil
-    var best                       = cols(0).score
+    var best                       = cols.head.score
     for (col <- cols) {
       import Ordering.Implicits._
       val bestInvalid = allCols
@@ -311,7 +311,7 @@ object RHeuristic extends Heuristic {
             .patterns(i)
             .isSpecialized(
               con,
-              false,
+              isExact = false,
               c.column.fringe,
               c.column.clauses(i),
               c.column.maxPriorityForKey(key)
@@ -415,7 +415,7 @@ sealed trait PseudoHeuristic extends Heuristic {
 @NamedHeuristic(name = 'N')
 object NPseudoHeuristic extends PseudoHeuristic {
   override def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn =
-    cols(0)
+    cols.head
 }
 
 @NamedHeuristic(name = 'L')

matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala

@@ -6,10 +6,8 @@ import java.io.File
 import java.io.FileWriter
 import java.util.Optional
 import org.kframework.backend.llvm.matching.dt._
-
-import java.io.{File, FileWriter}
-import java.util.Optional
 import scala.collection.immutable
+import scala.collection.parallel.CollectionConverters._
 
 object Matching {
   def writeDecisionTreeToFile(
@@ -21,12 +19,12 @@ object Matching {
       warn: Boolean,
       genSearch: Boolean,
       kem: MatchingException => Unit
-  ) {
+  ): Unit = {
     val defn = new TextToKore().parse(filename)
     outputFolder.mkdirs()
     val allAxioms    = Parser.getAxioms(defn)
-    val axioms       = Parser.parseTopAxioms(allAxioms, false)
-    val searchAxioms = Parser.parseTopAxioms(allAxioms, true)
+    val axioms       = Parser.parseTopAxioms(allAxioms, search = false)
+    val searchAxioms = Parser.parseTopAxioms(allAxioms, search = true)
     val symlib       = Parser.parseSymbols(defn, heuristic)
     val (dt, dtSearch, matrix) = if (axioms.isEmpty) {
       (Failure(), Failure(), null)
@@ -63,7 +61,7 @@ object Matching {
         dt.serializeToYaml(new File(outputFolder, filename))
       }
     }
-    val funcAxioms = Parser.parseFunctionAxioms(allAxioms, false)
+    val funcAxioms = Parser.parseFunctionAxioms(allAxioms, simplification = false)
     val dts = symlib.functions.map { f =>
       if (logging) {
         System.out.println("Compiling " + f)
@@ -90,7 +88,7 @@ object Matching {
         if (logging) {
           System.out.println("Compiling decision tree for axiom " + a.ordinal)
         }
-        Matrix.clearCache
+        Matrix.clearCache()
         val dt       = Generator.mkSpecialDecisionTree(symlib, defn, matrix, a, threshold.get)
         val ordinal  = a.ordinal
         val filename = "dt_" + ordinal + ".yaml"
@@ -99,7 +97,7 @@ object Matching {
         }
       }
     }
-    val files  = (symlib.functions, dts).zipped.toIterable
+    val files  = symlib.functions.lazyZip(dts).toSeq
     val index  = new File(outputFolder, "index.txt")
     val writer = new FileWriter(index)
     var idx    = 0
@@ -110,7 +108,7 @@ object Matching {
       writer.write(pair._1.ctr + "\t" + filename + "\n")
       idx += 1
     }
-    writer.close
+    writer.close()
   }
 
   var logging = false
@@ -133,16 +131,16 @@ object Matching {
   def main(args: Array[String]): Unit = {
     val file         = new File(args(0))
     val outputFolder = new File(args(2))
-    logging = args.size > 4
+    logging = args.length > 4
     writeDecisionTreeToFile(
       file,
       args(1),
       outputFolder,
       getThreshold(args(3)),
-      true,
-      true,
-      true,
-      e => ()
+      genSingleRuleTrees = true,
+      warn = true,
+      genSearch = true,
+      _ => ()
     )
   }
 }