diff --git a/matching/deps/scala_kore_release b/matching/deps/scala_kore_release
index 0d91a54c7..1c09c74e2 100644
--- a/matching/deps/scala_kore_release
+++ b/matching/deps/scala_kore_release
@@ -1 +1 @@
-0.3.0
+0.3.3
diff --git a/matching/pom.xml b/matching/pom.xml
index 66ec6d4ab..3adc0681b 100644
--- a/matching/pom.xml
+++ b/matching/pom.xml
@@ -12,10 +12,10 @@
17
- 0.3.0
+ 0.3.3
2.41.1
- 2.12
- 18
+ 2.13
+ 13
${scala.majorVersion}.${scala.minorVersion}
3.7.17
@@ -48,6 +48,11 @@
scala-reflect
${scala.version}
+
+ org.scala-lang.modules
+ scala-parallel-collections_2.13
+ 1.0.4
+
com.runtimeverification.k
scala-kore
@@ -77,7 +82,7 @@
org.scala-sbt
- compiler-bridge_2.12
+ compiler-bridge_2.13
1.8.0
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala
index 5e115bed4..67f6ad78e 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala
@@ -2,34 +2,36 @@ package org.kframework.backend.llvm.matching
import com.runtimeverification.k.kore.SymbolOrAlias
import org.kframework.backend.llvm.matching.pattern._
+import scala.collection.immutable
sealed trait Constructor {
def name: String
def isBest(pat: Pattern[Option[Occurrence]]): Boolean
- def expand(f: Fringe): Option[Seq[Fringe]]
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String]
+ def expand(f: Fringe): Option[immutable.Seq[Fringe]]
+ def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String]
}
case class Empty() extends Constructor {
def name = "0"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
- def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq())
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
+ def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq())
+ def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
val symbol = Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get
f.sortInfo.category match {
- case SetS() => SetP(Seq(), None, symbol, SymbolP(symbol, Seq()))
- case MapS() => MapP(Seq(), Seq(), None, symbol, SymbolP(symbol, Seq()))
- case _ => ???
+ 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 _ => ???
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class NonEmpty() extends Constructor {
- def name: String = ???
- def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
- def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq(f))
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = children(0)
+ 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.head
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
@@ -37,50 +39,50 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
extends Constructor {
def name = "1"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = key.isDefined && pat == key.get
- def expand(f: Fringe): Option[Seq[Fringe]] = {
+ def expand(f: Fringe): Option[immutable.Seq[Fringe]] = {
val sorts = f.symlib.signatures(element)._1
key match {
case None =>
if (isSet) {
Some(
- Seq(
- new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false),
- new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false)
+ immutable.Seq(
+ Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false),
+ Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false)
)
)
} else {
Some(
- 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)
+ immutable.Seq(
+ 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(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(
- Seq(
- new Fringe(f.symlib, sorts(1), Value(k, f.occurrence), false),
- new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false),
+ immutable.Seq(
+ Fringe(f.symlib, sorts(1), Value(k, f.occurrence), isExact = false),
+ Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false),
f
)
)
}
}
}
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
+ def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
val child = children.last
var key: Pattern[String] = null
var value: Pattern[String] = null
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 {
@@ -88,15 +90,15 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
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] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k, v))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k, v))
def setElement(k: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k))
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, immutable.Seq(m1, m2))
child match {
case MapP(keys, values, frame, ctr, orig) =>
MapP(key +: keys, value +: values, frame, ctr, orig)
@@ -105,15 +107,15 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
case WildcardP() | VariableP(_, _) =>
if (isSet) {
SetP(
- Seq(key),
+ immutable.Seq(key),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(setElement(key), child)
)
} else {
MapP(
- Seq(key),
- Seq(value),
+ immutable.Seq(key),
+ immutable.Seq(value),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(element(key, value), child)
@@ -128,17 +130,17 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) extends Constructor {
def name = "0"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = key.isDefined && pat == key.get
- def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq(f))
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
- val child = children(0)
+ 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.head
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k, v))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k, v))
def setElement(k: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k))
val unit: Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, immutable.Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, immutable.Seq(m1, m2))
def wildcard = WildcardP[String]()
child match {
case MapP(keys, values, frame, ctr, orig) =>
@@ -154,15 +156,15 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex
case WildcardP() | VariableP(_, _) =>
if (isSet) {
SetP(
- Seq(wildcard),
+ immutable.Seq(wildcard),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(setElement(wildcard), child)
)
} else {
MapP(
- Seq(wildcard),
- Seq(wildcard),
+ immutable.Seq(wildcard),
+ immutable.Seq(wildcard),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(element(wildcard, wildcard), child)
@@ -177,21 +179,21 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex
case class ListC(element: SymbolOrAlias, length: Int) extends Constructor {
def name: String = length.toString
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
- def expand(f: Fringe): Option[Seq[Fringe]] = {
+ 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: Seq[Pattern[String]]): Pattern[String] = {
+ def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
def element(v: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(v))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(v))
val unit: Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, immutable.Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, immutable.Seq(m1, m2))
ListP(
children,
None,
- Seq(),
+ immutable.Seq(),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
children.map(element).fold(unit)(concat)
)
@@ -202,18 +204,18 @@ case class ListC(element: SymbolOrAlias, length: Int) extends Constructor {
case class SymbolC(sym: SymbolOrAlias) extends Constructor {
def name: String = sym.toString
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
- def expand(f: Fringe): Option[Seq[Fringe]] =
+ def expand(f: Fringe): Option[immutable.Seq[Fringe]] =
if (f.symlib.signatures(sym)._2 != f.sort) {
None
} else {
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")
)
)
}
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] =
+ def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] =
SymbolP(sym, children)
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
@@ -221,8 +223,8 @@ case class SymbolC(sym: SymbolOrAlias) extends Constructor {
case class LiteralC(literal: String) extends Constructor {
def name: String = literal
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
- def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq())
- def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] =
+ def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq())
+ def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] =
LiteralP(literal, f.sortInfo.category)
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala
index e366c9fcb..5a93c3389 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala
@@ -13,6 +13,7 @@ import org.kframework.backend.llvm.matching.pattern.SortCategory
import org.kframework.backend.llvm.matching.pattern.SymbolP
import org.kframework.backend.llvm.matching.pattern.VariableP
import org.kframework.backend.llvm.matching.pattern.WildcardP
+import scala.collection.immutable
object Generator {
@@ -24,82 +25,94 @@ object Generator {
private def listPattern(
sym: SymbolOrAlias,
cons: CollectionCons,
- ps: Seq[P[String]],
+ ps: immutable.Seq[P[String]],
c: SymbolOrAlias
): P[String] =
(cons, ps) match {
- case (Concat(), Seq(ListP(hd1, None, tl1, _, o1), ListP(hd2, frame, tl2, _, o2))) =>
- ListP(hd1 ++ tl1 ++ hd2, frame, tl2, c, SymbolP(sym, Seq(o1, o2)))
- case (Concat(), Seq(ListP(hd1, frame, tl1, _, o1), ListP(hd2, None, tl2, _, o2))) =>
- ListP(hd1, frame, tl1 ++ hd2 ++ tl2, c, SymbolP(sym, Seq(o1, o2)))
- case (Concat(), Seq(ListP(hd, None, tl, _, o), p @ VariableP(_, _))) =>
- ListP(hd ++ tl, Some(p), Seq(), c, SymbolP(sym, Seq(o, p)))
- case (Concat(), Seq(ListP(hd, None, tl, _, o), p @ WildcardP())) =>
- ListP(hd ++ tl, Some(p), Seq(), c, SymbolP(sym, Seq(o, p)))
- case (Concat(), Seq(p @ VariableP(_, _), ListP(hd, None, tl, _, o))) =>
- ListP(Seq(), Some(p), hd ++ tl, c, SymbolP(sym, Seq(p, o)))
- case (Concat(), Seq(p @ WildcardP(), ListP(hd, None, tl, _, o))) =>
- ListP(Seq(), Some(p), hd ++ tl, c, SymbolP(sym, Seq(p, o)))
- case (Concat(), Seq(p1, p2)) => ListP(Seq(), None, Seq(), c, SymbolP(sym, Seq(p1, p2))) /* not
+ case (Concat(), immutable.Seq(ListP(hd1, None, tl1, _, o1), ListP(hd2, frame, tl2, _, o2))) =>
+ ListP(hd1 ++ tl1 ++ hd2, frame, tl2, c, SymbolP(sym, immutable.Seq(o1, o2)))
+ case (Concat(), immutable.Seq(ListP(hd1, frame, tl1, _, o1), ListP(hd2, None, tl2, _, o2))) =>
+ ListP(hd1, frame, tl1 ++ hd2 ++ tl2, c, SymbolP(sym, immutable.Seq(o1, o2)))
+ case (Concat(), immutable.Seq(ListP(hd, None, tl, _, o), p @ VariableP(_, _))) =>
+ ListP(hd ++ tl, Some(p), immutable.Seq(), c, SymbolP(sym, immutable.Seq(o, p)))
+ case (Concat(), immutable.Seq(ListP(hd, None, tl, _, o), p @ WildcardP())) =>
+ ListP(hd ++ tl, Some(p), immutable.Seq(), c, SymbolP(sym, immutable.Seq(o, p)))
+ case (Concat(), immutable.Seq(p @ VariableP(_, _), ListP(hd, None, tl, _, o))) =>
+ ListP(immutable.Seq(), Some(p), hd ++ tl, c, SymbolP(sym, immutable.Seq(p, o)))
+ case (Concat(), immutable.Seq(p @ WildcardP(), ListP(hd, None, tl, _, o))) =>
+ ListP(immutable.Seq(), Some(p), hd ++ tl, c, SymbolP(sym, immutable.Seq(p, o)))
+ case (Concat(), immutable.Seq(p1, p2)) =>
+ ListP(immutable.Seq(), None, immutable.Seq(), c, SymbolP(sym, immutable.Seq(p1, p2))) /* not
* valid, but necessary for iterated pattern matching */
- case (Unit(), Seq()) => ListP(Seq(), None, Seq(), c, SymbolP(sym, Seq()))
- case (Element(), Seq(p)) => ListP(Seq(p), None, Seq(), c, SymbolP(sym, Seq(p)))
+ case (Unit(), immutable.Seq()) =>
+ 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(
sym: SymbolOrAlias,
cons: CollectionCons,
- ps: Seq[P[String]],
+ ps: immutable.Seq[P[String]],
c: SymbolOrAlias
): P[String] =
(cons, ps) match {
- case (Concat(), Seq(MapP(ks1, vs1, None, _, o1), MapP(ks2, vs2, frame, _, o2))) =>
- MapP(ks1 ++ ks2, vs1 ++ vs2, frame, c, SymbolP(sym, Seq(o1, o2)))
- case (Concat(), Seq(MapP(ks1, vs1, frame, _, o1), MapP(ks2, vs2, None, _, o2))) =>
- MapP(ks1 ++ ks2, vs1 ++ vs2, frame, c, SymbolP(sym, Seq(o1, o2)))
- case (Concat(), Seq(MapP(ks, vs, None, _, o), p @ VariableP(_, _))) =>
- MapP(ks, vs, Some(p), c, SymbolP(sym, Seq(o, p)))
- case (Concat(), Seq(MapP(ks, vs, None, _, o), p @ WildcardP())) =>
- MapP(ks, vs, Some(p), c, SymbolP(sym, Seq(o, p)))
- case (Concat(), Seq(p @ VariableP(_, _), MapP(ks, vs, None, _, o))) =>
- MapP(ks, vs, Some(p), c, SymbolP(sym, Seq(p, o)))
- case (Concat(), Seq(p @ WildcardP(), MapP(ks, vs, None, _, o))) =>
- MapP(ks, vs, Some(p), c, SymbolP(sym, Seq(p, o)))
- case (Concat(), Seq(p1, p2)) => MapP(Seq(), Seq(), None, c, SymbolP(sym, Seq(p1, p2))) /* not
+ case (Concat(), immutable.Seq(MapP(ks1, vs1, None, _, o1), MapP(ks2, vs2, frame, _, o2))) =>
+ MapP(ks1 ++ ks2, vs1 ++ vs2, frame, c, SymbolP(sym, immutable.Seq(o1, o2)))
+ case (Concat(), immutable.Seq(MapP(ks1, vs1, frame, _, o1), MapP(ks2, vs2, None, _, o2))) =>
+ MapP(ks1 ++ ks2, vs1 ++ vs2, frame, c, SymbolP(sym, immutable.Seq(o1, o2)))
+ case (Concat(), immutable.Seq(MapP(ks, vs, None, _, o), p @ VariableP(_, _))) =>
+ MapP(ks, vs, Some(p), c, SymbolP(sym, immutable.Seq(o, p)))
+ case (Concat(), immutable.Seq(MapP(ks, vs, None, _, o), p @ WildcardP())) =>
+ MapP(ks, vs, Some(p), c, SymbolP(sym, immutable.Seq(o, p)))
+ case (Concat(), immutable.Seq(p @ VariableP(_, _), MapP(ks, vs, None, _, o))) =>
+ MapP(ks, vs, Some(p), c, SymbolP(sym, immutable.Seq(p, o)))
+ case (Concat(), immutable.Seq(p @ WildcardP(), MapP(ks, vs, None, _, o))) =>
+ MapP(ks, vs, Some(p), c, SymbolP(sym, immutable.Seq(p, o)))
+ case (Concat(), immutable.Seq(p1, p2)) =>
+ MapP(immutable.Seq(), immutable.Seq(), None, c, SymbolP(sym, immutable.Seq(p1, p2))) /* not
* valid, but necessary for iterated pattern matching */
- case (Unit(), Seq()) => MapP(Seq(), Seq(), None, c, SymbolP(sym, Seq()))
- case (Element(), Seq(k, v)) => MapP(Seq(k), Seq(v), None, c, SymbolP(sym, Seq(k, v)))
+ case (Unit(), immutable.Seq()) =>
+ 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(
sym: SymbolOrAlias,
cons: CollectionCons,
- ps: Seq[P[String]],
+ ps: immutable.Seq[P[String]],
c: SymbolOrAlias
): P[String] =
(cons, ps) match {
- case (Concat(), Seq(SetP(ks1, None, _, o1), SetP(ks2, frame, _, o2))) =>
- SetP(ks1 ++ ks2, frame, c, SymbolP(sym, Seq(o1, o2)))
- case (Concat(), Seq(SetP(ks1, frame, _, o1), SetP(ks2, None, _, o2))) =>
- SetP(ks1 ++ ks2, frame, c, SymbolP(sym, Seq(o1, o2)))
- case (Concat(), Seq(SetP(ks, None, _, o), p @ VariableP(_, _))) =>
- SetP(ks, Some(p), c, SymbolP(sym, Seq(o, p)))
- case (Concat(), Seq(SetP(ks, None, _, o), p @ WildcardP())) =>
- SetP(ks, Some(p), c, SymbolP(sym, Seq(o, p)))
- case (Concat(), Seq(p @ VariableP(_, _), SetP(ks, None, _, o))) =>
- SetP(ks, Some(p), c, SymbolP(sym, Seq(p, o)))
- case (Concat(), Seq(p @ WildcardP(), SetP(ks, None, _, o))) =>
- SetP(ks, Some(p), c, SymbolP(sym, Seq(p, o)))
- case (Concat(), Seq(p1, p2)) => SetP(Seq(), None, c, SymbolP(sym, Seq(p1, p2))) /* not valid,
- * but necessary for iterated pattern matching */
- case (Unit(), Seq()) => SetP(Seq(), None, c, SymbolP(sym, Seq()))
- case (Element(), Seq(e)) => SetP(Seq(e), None, c, SymbolP(sym, Seq(e)))
+ case (Concat(), immutable.Seq(SetP(ks1, None, _, o1), SetP(ks2, frame, _, o2))) =>
+ SetP(ks1 ++ ks2, frame, c, SymbolP(sym, immutable.Seq(o1, o2)))
+ case (Concat(), immutable.Seq(SetP(ks1, frame, _, o1), SetP(ks2, None, _, o2))) =>
+ SetP(ks1 ++ ks2, frame, c, SymbolP(sym, immutable.Seq(o1, o2)))
+ case (Concat(), immutable.Seq(SetP(ks, None, _, o), p @ VariableP(_, _))) =>
+ SetP(ks, Some(p), c, SymbolP(sym, immutable.Seq(o, p)))
+ case (Concat(), immutable.Seq(SetP(ks, None, _, o), p @ WildcardP())) =>
+ SetP(ks, Some(p), c, SymbolP(sym, immutable.Seq(o, p)))
+ case (Concat(), immutable.Seq(p @ VariableP(_, _), SetP(ks, None, _, o))) =>
+ SetP(ks, Some(p), c, SymbolP(sym, immutable.Seq(p, o)))
+ case (Concat(), immutable.Seq(p @ WildcardP(), SetP(ks, None, _, o))) =>
+ SetP(ks, Some(p), c, SymbolP(sym, immutable.Seq(p, o)))
+ case (Concat(), immutable.Seq(p1, p2)) =>
+ SetP(immutable.Seq(), None, c, SymbolP(sym, immutable.Seq(p1, p2))) /* not valid, but
+ * necessary for iterated pattern matching */
+ case (Unit(), immutable.Seq()) =>
+ 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(
mod: Definition,
symlib: Parser.SymLib,
- lhs: Seq[Pattern]
+ lhs: immutable.Seq[Pattern]
): List[P[String]] = {
def getElementSym(sort: Sort): SymbolOrAlias =
Parser.getSymbolAtt(symlib.sortAtt(sort), "element").get
@@ -112,17 +125,17 @@ object Generator {
hookAtt match {
case Some("LIST.concat") =>
listPattern(sym, Concat(), ps.map(genPattern), getElementSym(sort))
- case Some("LIST.unit") => listPattern(sym, Unit(), Seq(), getElementSym(sort))
+ case Some("LIST.unit") => listPattern(sym, Unit(), immutable.Seq(), getElementSym(sort))
case Some("LIST.element") =>
listPattern(sym, Element(), ps.map(genPattern), getElementSym(sort))
case Some("MAP.concat") =>
mapPattern(sym, Concat(), ps.map(genPattern), getElementSym(sort))
- case Some("MAP.unit") => mapPattern(sym, Unit(), Seq(), getElementSym(sort))
+ case Some("MAP.unit") => mapPattern(sym, Unit(), immutable.Seq(), getElementSym(sort))
case Some("MAP.element") =>
mapPattern(sym, Element(), ps.map(genPattern), getElementSym(sort))
case Some("SET.concat") =>
setPattern(sym, Concat(), ps.map(genPattern), getElementSym(sort))
- case Some("SET.unit") => setPattern(sym, Unit(), Seq(), getElementSym(sort))
+ case Some("SET.unit") => setPattern(sym, Unit(), immutable.Seq(), getElementSym(sort))
case Some("SET.element") =>
setPattern(sym, Element(), ps.map(genPattern), getElementSym(sort))
case _ => SymbolP(sym, ps.map(genPattern))
@@ -144,7 +157,7 @@ object Generator {
val att = symlib.sortAtt(sort)
val hookAtt = Parser.getStringAtt(att, "hook")
VariableP(name, SortCategory(hookAtt.orElse(Some("STRING.String")), sort, symlib))
- case And(_, p +: (v @ Variable(_, _)) +: Seq()) =>
+ case And(_, p +: (v @ Variable(_, _)) +: immutable.Seq()) =>
val _var = genPattern(v).asInstanceOf[VariableP[String]]
AsP(_var.name, _var.sort, genPattern(p))
case Or(_, args) => args.map(genPattern).reduce(OrP(_, _))
@@ -152,9 +165,9 @@ object Generator {
lhs.map(genPattern).toList
}
- private def genVars(pat: Pattern): Seq[Variable] =
+ private def genVars(pat: Pattern): immutable.Seq[Variable] =
pat match {
- case v @ Variable(_, _) => Seq(v)
+ case v @ Variable(_, _) => immutable.Seq(v)
case And(_, ps) => ps.flatMap(genVars)
case Application(_, ps) => ps.flatMap(genVars)
case Ceil(_, _, p) => genVars(p)
@@ -168,26 +181,26 @@ object Generator {
// case Next(_, p) => genVars(p)
case Not(_, p) => genVars(p)
case Or(_, ps) => ps.flatMap(genVars)
- case _ => Seq()
+ case _ => immutable.Seq()
}
- def genClauseMatrix[T](
+ def genClauseMatrix(
symlib: Parser.SymLib,
mod: Definition,
- axioms: IndexedSeq[AxiomInfo],
- sorts: Seq[Sort]
+ 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,
scVars.map(_.map(_.name).sorted.distinct),
- (rhsVars ++ scVars.getOrElse(Seq()))
+ (rhsVars ++ scVars.getOrElse(immutable.Seq()))
.filter(_.name.startsWith("Var'Bang"))
.map(v => (v.name, v.sort)),
a.rewrite.getLeftHandSide.size,
@@ -199,15 +212,19 @@ object Generator {
}
val patterns = axioms.map(a => genPatterns(mod, symlib, a.rewrite.getLeftHandSide)).transpose
val cols =
- (sorts, if (axioms.isEmpty) sorts.map(_ => IndexedSeq()) else patterns).zipped.toIndexedSeq
+ sorts
+ .lazyZip(
+ if (axioms.isEmpty) sorts.map(_ => immutable.IndexedSeq()) else patterns
+ )
+ .toIndexedSeq
new Matrix(symlib, cols, actions).expand
}
def mkDecisionTree(
symlib: Parser.SymLib,
mod: Definition,
- axioms: IndexedSeq[AxiomInfo],
- sorts: Seq[Sort],
+ axioms: immutable.IndexedSeq[AxiomInfo],
+ sorts: immutable.Seq[Sort],
name: SymbolOrAlias,
kem: MatchingException => scala.Unit
): DecisionTree = {
@@ -233,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
}
@@ -244,10 +261,10 @@ object Generator {
matrix: Matrix,
axiom: AxiomInfo,
threshold: (Int, Int)
- ): Option[(DecisionTree, Seq[(P[String], Occurrence)])] = {
- val rhs = genPatterns(mod, symlib, Seq(axiom.rewrite.getRightHandSide))
+ ): 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.toSeq
+ val residualMap = residuals.lazyZip(specialized.fringe.map(_.occurrence)).to(immutable.Seq)
if (Matching.logging) {
System.out.println("Residuals: " + residualMap.toList)
}
@@ -256,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
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala
index 1c05e6b39..5a706705a 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala
@@ -2,6 +2,7 @@ package org.kframework.backend.llvm.matching
import com.runtimeverification.k.kore.SymbolOrAlias
import org.kframework.backend.llvm.matching.pattern._
+import scala.collection.immutable
sealed trait Heuristic {
val needsMatrix: Boolean
@@ -72,13 +73,16 @@ sealed trait Heuristic {
def computeScoreForKey(c: AbstractColumn, key: Option[Pattern[Option[Occurrence]]]): Double
- def breakTies(cols: Seq[MatrixColumn]): MatrixColumn = RPseudoHeuristic.breakTies(cols)
+ def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn = RPseudoHeuristic.breakTies(cols)
}
object Heuristic {
- def getBest(cols: Seq[MatrixColumn], allCols: Seq[MatrixColumn]): Seq[MatrixColumn] = {
+ def getBest(
+ cols: immutable.Seq[MatrixColumn],
+ 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
@@ -307,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)
@@ -410,18 +414,18 @@ sealed trait PseudoHeuristic extends Heuristic {
@NamedHeuristic(name = 'N')
object NPseudoHeuristic extends PseudoHeuristic {
- override def breakTies(cols: Seq[MatrixColumn]): MatrixColumn =
- cols(0)
+ override def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn =
+ cols.head
}
@NamedHeuristic(name = 'L')
object LPseudoHeuristic extends PseudoHeuristic {
- override def breakTies(cols: Seq[MatrixColumn]): MatrixColumn =
+ override def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn =
cols.minBy(_.column.fringe.occurrence.size)
}
@NamedHeuristic(name = 'R')
object RPseudoHeuristic extends PseudoHeuristic {
- override def breakTies(cols: Seq[MatrixColumn]): MatrixColumn =
+ override def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn =
cols.reverse.minBy(_.column.fringe.occurrence.size)
}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala
index fab7a3590..ddce22670 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala
@@ -6,6 +6,8 @@ import java.io.File
import java.io.FileWriter
import java.util.Optional
import org.kframework.backend.llvm.matching.dt._
+import scala.collection.immutable
+import scala.collection.parallel.CollectionConverters._
object Matching {
def writeDecisionTreeToFile(
@@ -17,19 +19,25 @@ 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)
} else {
- val matrix = Generator.genClauseMatrix(symlib, defn, axioms, Seq(axioms.head.rewrite.sort))
+ val matrix =
+ Generator.genClauseMatrix(symlib, defn, axioms, immutable.Seq(axioms.head.rewrite.sort))
val searchMatrix =
- Generator.genClauseMatrix(symlib, defn, searchAxioms, Seq(searchAxioms.head.rewrite.sort))
+ Generator.genClauseMatrix(
+ symlib,
+ defn,
+ searchAxioms,
+ immutable.Seq(searchAxioms.head.rewrite.sort)
+ )
if (warn) {
searchMatrix.checkUsefulness(kem)
}
@@ -42,13 +50,18 @@ object Matching {
if (genSingleRuleTrees) {
for (axiom <- axioms.par) {
val matrix =
- Generator.genClauseMatrix(symlib, defn, IndexedSeq(axiom), Seq(axiom.rewrite.sort))
+ Generator.genClauseMatrix(
+ symlib,
+ defn,
+ immutable.IndexedSeq(axiom),
+ immutable.Seq(axiom.rewrite.sort)
+ )
val dt = matrix.compile
val filename = "match_" + axiom.ordinal + ".yaml"
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)
@@ -59,7 +72,7 @@ object Matching {
Generator.mkDecisionTree(
symlib,
defn,
- funcAxioms.getOrElse(f, IndexedSeq()),
+ funcAxioms.getOrElse(f, immutable.IndexedSeq()),
symlib.signatures(f)._1,
f,
kem
@@ -75,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"
@@ -84,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
@@ -95,7 +108,7 @@ object Matching {
writer.write(pair._1.ctr + "\t" + filename + "\n")
idx += 1
}
- writer.close
+ writer.close()
}
var logging = false
@@ -118,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,
+ _ => ()
)
}
}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
index 0d1ff2f3a..568c54186 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
@@ -10,6 +10,8 @@ import java.util.concurrent.ConcurrentHashMap
import java.util.Optional
import org.kframework.backend.llvm.matching.dt._
import org.kframework.backend.llvm.matching.pattern._
+import scala.annotation.tailrec
+import scala.collection.immutable
trait AbstractColumn {
def column: Column
@@ -36,15 +38,15 @@ trait AbstractColumn {
}
}
-case class MatrixColumn(val matrix: Matrix, colIx: Int) extends AbstractColumn {
- def column: Column = matrix.columns(colIx)
- lazy val score: Seq[Double] = column.score(this)
+case class MatrixColumn(matrix: Matrix, colIx: Int) extends AbstractColumn {
+ def column: Column = matrix.columns(colIx)
+ lazy val score: immutable.Seq[Double] = column.score(this)
}
class Column(
val fringe: Fringe,
- val patterns: IndexedSeq[Pattern[String]],
- val clauses: IndexedSeq[Clause]
+ val patterns: immutable.IndexedSeq[Pattern[String]],
+ val clauses: immutable.IndexedSeq[Clause]
) extends AbstractColumn {
def column: Column = this
@@ -57,9 +59,9 @@ class Column(
}
}
- lazy val score: Seq[Double] = computeScore
+ lazy val score: immutable.Seq[Double] = computeScore
- def score(matrixCol: MatrixColumn): Seq[Double] = {
+ def score(matrixCol: MatrixColumn): immutable.Seq[Double] = {
def zeroOrHeuristic(h: Heuristic): Double =
if (h.needsMatrix) {
matrixCol.computeScoreForKey(h, bestKey)
@@ -71,17 +73,17 @@ class Column(
.map((hs: (Heuristic, Double)) => hs._2 + zeroOrHeuristic(hs._1))
}
- def computeScore: Seq[Double] =
+ def computeScore: immutable.Seq[Double] =
computeScoreForKey(bestKey)
- def computeScoreForKey(key: Option[Pattern[Option[Occurrence]]]): Seq[Double] = {
+ def computeScoreForKey(key: Option[Pattern[Option[Occurrence]]]): immutable.Seq[Double] = {
def zeroOrHeuristic(h: Heuristic): Double =
if (h.needsMatrix) {
- return 0.0
+ 0.0
} else {
- return computeScoreForKey(h, key)
+ computeScoreForKey(h, key)
}
- fringe.symlib.heuristics.map(zeroOrHeuristic(_))
+ fringe.symlib.heuristics.map(zeroOrHeuristic)
}
def isValid: Boolean = isValidForKey(bestKey)
@@ -89,19 +91,19 @@ class Column(
def isValidForKey(key: Option[Pattern[Option[Occurrence]]]): Boolean =
!fringe.sortInfo.isCollection || key.isDefined || !patterns.exists(_.isChoice)
- lazy val keyVars: Seq[Set[String]] = {
+ lazy val keyVars: immutable.Seq[Set[String]] = {
val keys = patterns.map(_.mapOrSetKeys)
keys.map(_.flatMap(_.variables).toSet)
}
- private lazy val boundVars: Seq[Set[String]] = patterns.map(_.variables)
- def needed(vars: Seq[Set[String]]): Boolean = {
- val intersection = (vars, boundVars).zipped.map(_.intersect(_))
+ private lazy val boundVars: immutable.Seq[Set[String]] = patterns.map(_.variables)
+ def needed(vars: immutable.Seq[Set[String]]): Boolean = {
+ val intersection = vars.lazyZip(boundVars).map(_.intersect(_))
intersection.exists(_.nonEmpty)
}
- lazy val isEmpty = fringe.sortInfo.isCollection && rawSignature.contains(Empty())
+ lazy val isEmpty: Boolean = fringe.sortInfo.isCollection && rawSignature.contains(Empty())
- private lazy val rawSignature: Seq[Constructor] =
+ private lazy val rawSignature: immutable.Seq[Constructor] =
patterns.zipWithIndex.flatMap(p => p._1.signature(clauses(p._2)))
def signatureForKey(key: Option[Pattern[Option[Occurrence]]]): List[Constructor] = {
@@ -139,18 +141,19 @@ class Column(
def isChoice: Boolean = isChoiceForKey(bestKey)
- def isChoiceForKey(key: Option[Pattern[Option[Occurrence]]]) =
- fringe.sortInfo.isCollection && key == None
+ def isChoiceForKey(key: Option[Pattern[Option[Occurrence]]]): Boolean =
+ fringe.sortInfo.isCollection && key.isEmpty
- private def asListP(p: Pattern[String]): Seq[ListP[String]] =
+ @tailrec
+ private def asListP(p: Pattern[String]): immutable.Seq[ListP[String]] =
p match {
- case l @ ListP(_, _, _, _, _) => Seq(l)
+ case l @ ListP(_, _, _, _, _) => immutable.Seq(l)
case AsP(_, _, pat) => asListP(pat)
- case _ => Seq()
+ case _ => immutable.Seq()
}
def maxListSize: (Int, Int) = {
- val listPs = patterns.flatMap(asListP(_))
+ val listPs = patterns.flatMap(asListP)
if (listPs.isEmpty) {
(0, 0)
} else {
@@ -160,10 +163,10 @@ class Column(
}
}
- lazy val validKeys: Seq[Pattern[Option[Occurrence]]] = {
+ lazy val validKeys: immutable.Seq[Pattern[Option[Occurrence]]] = {
val possibleKeys = rawSignature.flatMap {
- case HasKey(_, _, Some(k)) => Seq(k)
- case _ => Seq()
+ case HasKey(_, _, Some(k)) => immutable.Seq(k)
+ case _ => immutable.Seq()
}
if (possibleKeys.isEmpty) {
possibleKeys
@@ -187,20 +190,21 @@ class Column(
def maxPriority: Int = maxPriorityForKey(bestKey)
- def maxPriorityForKey(key: Option[Pattern[Option[Occurrence]]]) =
+ def maxPriorityForKey(key: Option[Pattern[Option[Occurrence]]]): Int =
if (isChoiceForKey(key)) {
clauses(0).action.priority
} else {
Int.MaxValue
}
- def expand(ix: Constructor, isExact: Boolean): IndexedSeq[Column] = {
+ def expand(ix: Constructor, isExact: Boolean): immutable.IndexedSeq[Column] = {
val fringes = fringe.expand(ix)
- val ps = (patterns, clauses).zipped.toIterable.map(t =>
- t._1.expand(ix, isExact, fringes, fringe, t._2, maxPriority)
- )
- val transposed = if (ps.isEmpty) fringes.map(_ => IndexedSeq()) else ps.transpose
- (fringes, transposed).zipped.toIndexedSeq.map(t => new Column(t._1, t._2.toIndexedSeq, clauses))
+ val ps = patterns
+ .lazyZip(clauses)
+ .toSeq
+ .map(t => t._1.expand(ix, isExact, fringes, fringe, t._2, maxPriority))
+ val transposed = if (ps.isEmpty) fringes.map(_ => immutable.IndexedSeq()) else ps.transpose
+ fringes.lazyZip(transposed).toIndexedSeq.map(t => new Column(t._1, t._2.toIndexedSeq, clauses))
}
lazy val isWildcard: Boolean = patterns.forall(_.isWildcard)
@@ -209,39 +213,39 @@ class Column(
override def equals(other: Any): Boolean = other match {
case that: Column =>
- (that.canEqual(this)) &&
+ that.canEqual(this) &&
fringe == that.fringe &&
patterns == that.patterns
case _ => false
}
override lazy val hashCode: Int = {
- val state = Seq(patterns)
+ val state = immutable.Seq(patterns)
state.map(_.hashCode()).foldLeft(0)((a, b) => 31 * a + b)
}
}
case class VariableBinding[T](
- val name: T,
- val category: SortCategory,
- val occurrence: Occurrence,
- val pattern: Option[Pattern[String]]
+ name: T,
+ category: SortCategory,
+ occurrence: Occurrence,
+ pattern: Option[Pattern[String]]
) {
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Fringe(
- val symlib: Parser.SymLib,
- val sort: Sort,
- val occurrence: Occurrence,
- val isExact: Boolean
+ symlib: Parser.SymLib,
+ sort: Sort,
+ occurrence: Occurrence,
+ isExact: Boolean
) {
- val sortInfo = SortInfo(sort, symlib)
+ val sortInfo: SortInfo = SortInfo(sort, symlib)
- def overloads(sym: SymbolOrAlias): Seq[SymbolOrAlias] =
- symlib.overloads.getOrElse(sym, Seq())
+ def overloads(sym: SymbolOrAlias): immutable.Seq[SymbolOrAlias] =
+ symlib.overloads.getOrElse(sym, immutable.Seq())
- def injections(ix: Constructor): Seq[Constructor] =
+ def injections(ix: Constructor): immutable.Seq[Constructor] =
ix match {
case SymbolC(sym) =>
if (symlib.overloads.contains(sym) || sym.ctr == "inj") {
@@ -251,37 +255,38 @@ case class Fringe(
}
sortInfo.trueInjMap(sym).map(SymbolC)
} else {
- Seq()
+ immutable.Seq()
}
- case _ => Seq()
+ case _ => immutable.Seq()
}
def contains(ix: Constructor): Boolean =
lookup(ix).isDefined
- def expand(ix: Constructor): Seq[Fringe] =
+ def expand(ix: Constructor): immutable.Seq[Fringe] =
lookup(ix).get
- def lookup(ix: Constructor): Option[Seq[Fringe]] =
+ def lookup(ix: Constructor): Option[immutable.Seq[Fringe]] =
ix.expand(this)
def inexact: Fringe =
- Fringe(symlib, sort, occurrence, false)
+ Fringe(symlib, sort, occurrence, isExact = false)
override def toString: String = new util.Formatter().format("%12.12s", sort.toString).toString
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
class SortInfo private (sort: Sort, symlib: Parser.SymLib) {
- val constructors = symlib.constructorsForSort.getOrElse(sort, Seq())
+ val constructors: immutable.Seq[SymbolOrAlias] =
+ symlib.constructorsForSort.getOrElse(sort, immutable.Seq())
lazy val nonEmptyConstructors: Set[SymbolOrAlias] = constructors
.filter(c =>
- c.ctr != "inj" || SortInfo(c.params(0), symlib).category
- .hasIncompleteSignature(Seq(), true, SortInfo(c.params(0), symlib))
+ c.ctr != "inj" || SortInfo(c.params.head, symlib).category
+ .hasIncompleteSignature(immutable.Seq(), isExact = true, SortInfo(c.params.head, symlib))
)
.toSet
- val exactConstructors = constructors.filter(_.ctr != "inj")
- private val rawInjections = constructors.filter(_.ctr == "inj")
+ val exactConstructors: immutable.Seq[SymbolOrAlias] = constructors.filter(_.ctr != "inj")
+ private val rawInjections = constructors.filter(_.ctr == "inj")
private val injMap = rawInjections
.map(b => (b, rawInjections.filter(a => symlib.isSubsorted(a.params.head, b.params.head))))
.toMap
@@ -291,11 +296,11 @@ class SortInfo private (sort: Sort, symlib: Parser.SymLib) {
(
e._1,
e._2.map(g =>
- B.SymbolOrAlias("inj", Seq(symlib.signatures(g)._2, symlib.signatures(e._1)._2))
+ B.SymbolOrAlias("inj", immutable.Seq(symlib.signatures(g)._2, symlib.signatures(e._1)._2))
)
)
)
- val trueInjMap = injMap ++ overloadInjMap
+ val trueInjMap: Map[SymbolOrAlias, immutable.Seq[SymbolOrAlias]] = injMap ++ overloadInjMap
val category: SortCategory =
SortCategory(Parser.getStringAtt(symlib.sortAtt(sort), "hook"), sort, symlib)
lazy val length: Int = category.length(nonEmptyConstructors.size)
@@ -312,13 +317,13 @@ object SortInfo {
}
case class Action(
- val ordinal: Int,
- val lhsVars: Seq[Variable],
- val rhsVars: Seq[String],
- val scVars: Option[Seq[String]],
- val freshConstants: Seq[(String, Sort)],
- val arity: Int,
- val priority: Int,
+ ordinal: Int,
+ lhsVars: immutable.Seq[Variable],
+ rhsVars: immutable.Seq[String],
+ scVars: Option[immutable.Seq[String]],
+ freshConstants: immutable.Seq[(String, Sort)],
+ arity: Int,
+ priority: Int,
source: Optional[Source],
location: Optional[Location],
nonlinear: Boolean
@@ -328,23 +333,23 @@ case class Action(
case class Clause(
// the rule to be applied if this row succeeds
- val action: Action,
+ action: Action,
// the variable bindings made so far while matching this row
- val bindings: Vector[VariableBinding[String]],
+ bindings: Vector[VariableBinding[String]],
// the length of the head and tail of any list patterns
// with frame variables bound so far in this row
- val listRanges: Vector[(Occurrence, Int, Int)],
+ listRanges: Vector[(Occurrence, Int, Int)],
// variable bindings to injections that need to be constructed
// since they do not actually exist in the original subject term
- val overloadChildren: Vector[(Constructor, Fringe, VariableBinding[String])],
- val specializedVars: Map[Occurrence, (SortCategory, Pattern[Option[Occurrence]])]
+ overloadChildren: Vector[(Constructor, Fringe, VariableBinding[String])],
+ specializedVars: Map[Occurrence, (SortCategory, Pattern[Option[Occurrence]])]
) {
lazy val bindingsMap: Map[String, VariableBinding[String]] =
- bindings.groupBy(_.name).mapValues(_.head)
+ bindings.groupBy(_.name).view.mapValues(_.head).toMap
lazy val boundOccurrences: Set[Occurrence] = bindings.map(_.occurrence).toSet
- def isBound(binding: Any) =
+ def isBound(binding: Any): Boolean =
binding match {
case name: String => bindingsMap.contains(name)
case o: Option[_] => boundOccurrences.contains(o.get.asInstanceOf[Occurrence])
@@ -365,7 +370,7 @@ case class Clause(
pat: Pattern[String],
f: Fringe
): Clause =
- new Clause(
+ Clause(
action,
bindings ++ pat.bindings(ix, residual, f.occurrence, f.symlib),
listRanges ++ pat.listRange(ix, f.occurrence),
@@ -374,7 +379,7 @@ case class Clause(
)
private def translateVars(
- residuals: Seq[(Pattern[String], Occurrence)],
+ residuals: immutable.Seq[(Pattern[String], Occurrence)],
allVars: Vector[VariableBinding[String]],
symlib: Parser.SymLib
): Map[Occurrence, (SortCategory, Pattern[Option[Occurrence]])] = {
@@ -402,7 +407,7 @@ case class Clause(
}
def specializeBy(
- residualMap: Seq[(Pattern[String], Occurrence)],
+ residualMap: immutable.Seq[(Pattern[String], Occurrence)],
symlib: Parser.SymLib
): Clause = {
val overloadVars = overloadChildren.map(_._3)
@@ -420,23 +425,23 @@ case class Clause(
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
-case class Row(val patterns: IndexedSeq[Pattern[String]], val clause: Clause) {
+case class Row(patterns: immutable.IndexedSeq[Pattern[String]], clause: Clause) {
// returns whether the row is done matching
def isWildcard: Boolean = patterns.forall(_.isWildcard)
- def expand(colIx: Int): Seq[Row] = {
+ def expand(colIx: Int): immutable.Seq[Row] = {
val p0s = patterns(colIx).expandOr
- p0s.map(p => new Row(patterns.updated(colIx, p), clause))
+ p0s.map(p => Row(patterns.updated(colIx, p), clause))
}
def specialize(
ix: Constructor,
colIx: Int,
symlib: Parser.SymLib,
- fringe: IndexedSeq[Fringe]
+ fringe: immutable.IndexedSeq[Fringe]
): Option[Row] =
Matrix
- .fromRows(symlib, IndexedSeq(this), fringe, false)
+ .fromRows(symlib, immutable.IndexedSeq(this), fringe, search = false)
.specialize(ix, colIx, None)
._3
.rows
@@ -444,13 +449,13 @@ case class Row(val patterns: IndexedSeq[Pattern[String]], val clause: Clause) {
def default(
colIx: Int,
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
symlib: Parser.SymLib,
- fringe: IndexedSeq[Fringe],
- matrixColumns: IndexedSeq[Column]
+ fringe: immutable.IndexedSeq[Fringe],
+ matrixColumns: immutable.IndexedSeq[Column]
): Option[Row] =
Matrix
- .fromRows(symlib, IndexedSeq(this), fringe, false)
+ .fromRows(symlib, immutable.IndexedSeq(this), fringe, search = false)
.trueDefault(colIx, sigma, Some(matrixColumns))
.rows
.headOption
@@ -463,73 +468,75 @@ case class Row(val patterns: IndexedSeq[Pattern[String]], val clause: Clause) {
class Matrix private (
val symlib: Parser.SymLib,
- private val rawColumns: IndexedSeq[Column],
- private val rawRows: IndexedSeq[Row],
- private val rawClauses: IndexedSeq[Clause],
- private val rawFringe: IndexedSeq[Fringe],
+ private val rawColumns: immutable.IndexedSeq[Column],
+ private val rawRows: immutable.IndexedSeq[Row],
+ private val rawClauses: immutable.IndexedSeq[Clause],
+ private val rawFringe: immutable.IndexedSeq[Fringe],
val search: Boolean
) {
- lazy val clauses: IndexedSeq[Clause] =
+ lazy val clauses: immutable.IndexedSeq[Clause] =
if (rawClauses != null) {
rawClauses
} else {
rawRows.map(_.clause)
}
- lazy val fringe: IndexedSeq[Fringe] =
+ lazy val fringe: immutable.IndexedSeq[Fringe] =
if (rawFringe != null) {
rawFringe
} else {
rawColumns.map(_.fringe)
}
- lazy val columns: IndexedSeq[Column] =
+ lazy val columns: immutable.IndexedSeq[Column] =
if (rawColumns != null) {
rawColumns
} else if (rawRows.isEmpty) {
- rawFringe.map(f => new Column(f, IndexedSeq(), IndexedSeq()))
+ rawFringe.map(f => new Column(f, immutable.IndexedSeq(), immutable.IndexedSeq()))
} else {
computeColumns
}
- private def computeColumns: IndexedSeq[Column] = {
+ private def computeColumns: immutable.IndexedSeq[Column] = {
val ps = rawRows.map(_.patterns).transpose
rawFringe.indices.map(col => new Column(rawFringe(col), ps(col), clauses))
}
- lazy val rows: IndexedSeq[Row] =
+ lazy val rows: immutable.IndexedSeq[Row] =
if (rawRows != null) {
rawRows
} else if (rawColumns.isEmpty) {
- rawClauses.map(clause => new Row(IndexedSeq(), clause))
+ rawClauses.map(clause => Row(immutable.IndexedSeq(), clause))
} else {
computeRows
}
- private def computeRows: IndexedSeq[Row] = {
+ private def computeRows: immutable.IndexedSeq[Row] = {
val ps = rawColumns.map(_.patterns).transpose
- rawClauses.indices.map(row => new Row(ps(row), rawClauses(row)))
+ rawClauses.indices.map(row => Row(ps(row), rawClauses(row)))
}
def this(
symlib: Parser.SymLib,
- cols: IndexedSeq[(Sort, IndexedSeq[Pattern[String]])],
- actions: IndexedSeq[Action]
+ cols: immutable.IndexedSeq[(Sort, immutable.IndexedSeq[Pattern[String]])],
+ actions: immutable.IndexedSeq[Action]
) =
this(
symlib,
- (
- cols,
- (1 to cols.size).map(i => new Fringe(symlib, cols(i - 1)._1, Num(i, Base()), false))
- ).zipped.toIndexedSeq.map(pair =>
- new Column(
- pair._2,
- pair._1._2,
- actions.map(new Clause(_, Vector(), Vector(), Vector(), Map()))
+ cols
+ .lazyZip(
+ (1 to cols.size).map(i => Fringe(symlib, cols(i - 1)._1, Num(i, Base()), isExact = false))
)
- ),
+ .to(immutable.IndexedSeq)
+ .map(pair =>
+ new Column(
+ pair._2,
+ pair._1._2,
+ actions.map(Clause(_, Vector(), Vector(), Vector(), Map()))
+ )
+ ),
null,
- actions.map(new Clause(_, Vector(), Vector(), Vector(), Map())),
+ actions.map(Clause(_, Vector(), Vector(), Vector(), Map())),
null,
false
)
@@ -537,17 +544,17 @@ class Matrix private (
private def isWildcardOrResidual(pat: Pattern[String]): Boolean =
pat.isWildcard || pat.isResidual(symlib)
- private lazy val matrixColumns: Seq[MatrixColumn] =
+ private lazy val matrixColumns: immutable.Seq[MatrixColumn] =
columns.indices.map(MatrixColumn(this, _))
- private lazy val validCols: Seq[MatrixColumn] =
+ private lazy val validCols: immutable.Seq[MatrixColumn] =
matrixColumns.filter(col =>
col.column.isValid || columns.forall(c =>
c == col.column || !c.needed(col.column.keyVars) || col.column.needed(c.keyVars)
)
)
- private var specializing: Option[IndexedSeq[Pattern[String]]] = None
+ private var specializing: Option[immutable.IndexedSeq[Pattern[String]]] = None
// compute the column with the best score, choosing the first such column if they are equal
lazy val bestColIx: Int =
@@ -575,7 +582,7 @@ class Matrix private (
ix: Constructor,
colIx: Int,
residual: Option[Pattern[String]]
- ): (String, Seq[String], Matrix) = {
+ ): (String, immutable.Seq[String], Matrix) = {
val filtered = filterMatrix(
Some(ix),
residual,
@@ -593,9 +600,10 @@ class Matrix private (
(ix.name, justExpanded.map(_.fringe.sortInfo.category.hookAtt), expanded)
}
- def cases: List[(String, Seq[String], Matrix)] = sigma.map(specialize(_, bestColIx, None))
+ def cases: List[(String, immutable.Seq[String], Matrix)] =
+ sigma.map(specialize(_, bestColIx, None))
- lazy val compiledCases: Seq[(String, Seq[String], DecisionTree)] = {
+ lazy val compiledCases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)] = {
Matrix.remaining += sigma.length
if (Matching.logging) {
System.out.println("Signature:")
@@ -620,15 +628,15 @@ class Matrix private (
val newRows = rows
.filter(row => checkPattern(row.clause, row.patterns(colIx)))
.map(row =>
- new Row(row.patterns, row.clause.addVars(ix, residual, row.patterns(colIx), fringe(colIx)))
+ Row(row.patterns, row.clause.addVars(ix, residual, row.patterns(colIx), fringe(colIx)))
)
Matrix.fromRows(symlib, newRows, fringe, search)
}
def defaultConstructor(
colIx: Int,
- sigma: Seq[Constructor],
- matrixColumns: Option[IndexedSeq[Column]]
+ sigma: immutable.Seq[Constructor],
+ matrixColumns: Option[immutable.IndexedSeq[Column]]
): Option[Constructor] =
if (sigma.contains(Empty())) Some(NonEmpty())
else if (sigma.isEmpty) None
@@ -646,8 +654,8 @@ class Matrix private (
def trueDefault(
colIx: Int,
- sigma: Seq[Constructor],
- matrixColumns: Option[IndexedSeq[Column]]
+ sigma: immutable.Seq[Constructor],
+ matrixColumns: Option[immutable.IndexedSeq[Column]]
): Matrix = {
val ctr = defaultConstructor(colIx, sigma, matrixColumns)
val filtered = filterMatrix(ctr, None, (_, p) => p.isDefault, colIx)
@@ -655,7 +663,7 @@ class Matrix private (
if (columns(colIx).fringe.sortInfo.category.isExpandDefault) {
Matrix.fromColumns(
symlib,
- filtered.columns(colIx).expand(ctr.get, true) ++ filtered.notBestCol(colIx),
+ filtered.columns(colIx).expand(ctr.get, isExact = true) ++ filtered.notBestCol(colIx),
filtered.clauses,
search
)
@@ -668,7 +676,7 @@ class Matrix private (
expanded
}
- def default(colIx: Int, sigma: Seq[Constructor]): Option[Matrix] =
+ def default(colIx: Int, sigma: immutable.Seq[Constructor]): Option[Matrix] =
if (
columns(colIx).fringe.sortInfo.category.hasIncompleteSignature(sigma, columns(colIx).fringe)
) {
@@ -693,13 +701,13 @@ class Matrix private (
Function(
category.equalityFun,
Equal(os._1, os._2),
- Seq((os._1, category.hookAtt), (os._2, category.hookAtt)),
+ immutable.Seq((os._1, category.hookAtt), (os._2, category.hookAtt)),
"BOOL.Bool",
SwitchLit(
Equal(os._1, os._2),
"BOOL.Bool",
1,
- Seq(("1", Seq(), dt), ("0", Seq(), child)),
+ immutable.Seq(("1", immutable.Seq(), dt), ("0", immutable.Seq(), child)),
None
)
)
@@ -710,19 +718,21 @@ class Matrix private (
symlib
)
// first, add all remaining variable bindings to the clause
- val vars = row.clause.bindings ++ (fringe, row.patterns).zipped.toSeq.flatMap(t =>
- t._2.bindings(None, None, t._1.occurrence, symlib)
- )
+ val vars = row.clause.bindings ++ fringe
+ .lazyZip(row.patterns)
+ .to(immutable.Seq)
+ .flatMap(t => t._2.bindings(None, None, t._1.occurrence, symlib))
val overloadVars = row.clause.overloadChildren.map(_._3)
val freshVars = row.clause.action.freshConstants.map(t =>
VariableBinding(t._1, sortCat(t._2), Fresh(t._1), None)
)
val allVars = vars ++ overloadVars ++ freshVars
// then group the bound variables by their name
- val grouped = allVars.groupBy(v => v.name).mapValues(_.map(v => (v.category, v.occurrence)))
+ val grouped =
+ allVars.groupBy(v => v.name).view.mapValues(_.map(v => (v.category, v.occurrence))).toMap
// compute the variables bound more than once
val nonlinear = grouped.filter(_._2.size > 1)
- val nonlinearPairs = nonlinear.mapValues(l => (l, l.tail).zipped)
+ val nonlinearPairs = nonlinear.view.mapValues(l => l.lazyZip(l.tail)).toMap
val uniqueLhsVars =
row.clause.action.lhsVars.filterNot(v => row.clause.action.rhsVars.contains(v.name)).distinct
val newVars = {
@@ -750,7 +760,7 @@ class Matrix private (
SearchLeaf(
row.clause.action.ordinal,
newVars,
- Matrix.fromRows(symlib, firstGroup.patch(bestRowIx, Nil, 1), fringe, true).compile
+ Matrix.fromRows(symlib, firstGroup.patch(bestRowIx, Nil, 1), fringe, search = true).compile
)
} else {
Leaf(row.clause.action.ordinal, newVars)
@@ -775,7 +785,7 @@ class Matrix private (
newO,
"BOOL.Bool",
1,
- Seq(("1", Seq(), nonlinearLeaf), ("0", Seq(), child)),
+ immutable.Seq(("1", immutable.Seq(), nonlinearLeaf), ("0", immutable.Seq(), child)),
None
)
)
@@ -786,7 +796,7 @@ class Matrix private (
Function(
"hook_LIST_range_long",
o,
- Seq(
+ immutable.Seq(
(o2, "LIST.List"),
(Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"),
(Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64")
@@ -803,10 +813,10 @@ class Matrix private (
v.category.hookAtt,
SymbolP(
inj,
- Seq(
+ immutable.Seq(
VariableP(
Some(v.occurrence.asInstanceOf[Inj].rest),
- f.expand(SymbolC(inj))(0).sortInfo.category
+ f.expand(SymbolC(inj)).head.sortInfo.category
)
)
),
@@ -827,7 +837,8 @@ class Matrix private (
Function(
"get_fresh_constant",
Fresh(name),
- Seq((litO, "STRING.String"), (Num(row.clause.action.arity, Base()), "STRING.String")),
+ immutable
+ .Seq((litO, "STRING.String"), (Num(row.clause.action.arity, Base()), "STRING.String")),
sortCat(sort).hookAtt,
dt
)
@@ -844,11 +855,12 @@ class Matrix private (
)
}
- lazy val firstGroup = rows.takeWhile(_.clause.action.priority == rows.head.clause.action.priority)
+ lazy val firstGroup: immutable.IndexedSeq[Row] =
+ rows.takeWhile(_.clause.action.priority == rows.head.clause.action.priority)
- lazy val bestRowIx = firstGroup.indexWhere(_.isWildcard)
+ lazy val bestRowIx: Int = firstGroup.indexWhere(_.isWildcard)
- lazy val bestRow = rows(bestRowIx)
+ lazy val bestRow: Row = rows(bestRowIx)
def compile: DecisionTree = {
val result = Matrix.cache.get(this)
@@ -876,11 +888,12 @@ class Matrix private (
else {
bestRowIx match {
case -1 =>
- if (matrixColumns(bestColIx).score(0).isPosInfinity) {
+ if (matrixColumns(bestColIx).score.head.isPosInfinity) {
// decompose this column as it contains only wildcards
- val newClauses = (bestCol.clauses, bestCol.patterns).zipped.toIndexedSeq.map(t =>
- t._1.addVars(None, None, t._2, bestCol.fringe)
- )
+ val newClauses = bestCol.clauses
+ .lazyZip(bestCol.patterns)
+ .toIndexedSeq
+ .map(t => t._1.addVars(None, None, t._2, bestCol.fringe))
Matrix
.fromColumns(
symlib,
@@ -931,7 +944,7 @@ class Matrix private (
} else if (r.patterns(0).isWildcard) {
for (con <- sigma) {
if (Matching.logging) {
- System.out.println("Testing constructor " + con);
+ System.out.println("Testing constructor " + con)
}
val rowSpec = r.specialize(con, 0, symlib, fringe)
if (rowSpec.isDefined && specialize(con, 0, None)._3.useful(rowSpec.get)) {
@@ -941,11 +954,15 @@ class Matrix private (
false
} else {
val rowColumn =
- new Column(columns(0).fringe, IndexedSeq(r.patterns(0)), IndexedSeq(r.clause))
+ new Column(
+ columns(0).fringe,
+ immutable.IndexedSeq(r.patterns(0)),
+ immutable.IndexedSeq(r.clause)
+ )
val rowSigma = rowColumn.signatureForUsefulness
for (con <- rowSigma) {
if (Matching.logging) {
- System.out.println("Testing constructor " + con);
+ System.out.println("Testing constructor " + con)
}
val rowSpec = r.specialize(con, 0, symlib, fringe)
if (rowSpec.isDefined && specialize(con, 0, None)._3.useful(rowSpec.get)) {
@@ -969,17 +986,17 @@ class Matrix private (
val row = rows(rowIx)
val result = !matrix.useful(row)
if (Matching.logging && result) {
- System.out.println("Row " + row.clause.action.ordinal + " is useless");
+ System.out.println("Row " + row.clause.action.ordinal + " is useless")
}
result
}
- def nonExhaustive: Option[IndexedSeq[Pattern[String]]] =
+ def nonExhaustive: Option[immutable.IndexedSeq[Pattern[String]]] =
if (fringe.isEmpty) {
if (clauses.nonEmpty) {
None
} else {
- Some(IndexedSeq())
+ Some(immutable.IndexedSeq())
}
} else {
val sigma = columns(0).signatureForUsefulness
@@ -1024,7 +1041,7 @@ class Matrix private (
for (con <- sigma) {
val id = Matrix.id
if (Matching.logging) {
- System.out.println("Testing constructor " + con);
+ System.out.println("Testing constructor " + con)
System.out.println("-- Exhaustive --")
System.out.println("Matrix " + id + ": ")
System.out.println(this)
@@ -1100,11 +1117,13 @@ class Matrix private (
}
}
- def specializeBy(ps: IndexedSeq[Pattern[String]]): (Matrix, IndexedSeq[Pattern[String]]) = {
- def expandChildren(pat: Pattern[String]): IndexedSeq[Pattern[String]] =
+ def specializeBy(
+ ps: immutable.IndexedSeq[Pattern[String]]
+ ): (Matrix, immutable.IndexedSeq[Pattern[String]]) = {
+ def expandChildren(pat: Pattern[String]): immutable.IndexedSeq[Pattern[String]] =
pat match {
case SymbolP(_, ps) => ps.toIndexedSeq
- case LiteralP(_, _) => IndexedSeq()
+ case LiteralP(_, _) => immutable.IndexedSeq()
case _ => ???
}
def getConstructor(pat: Pattern[String]): Constructor =
@@ -1128,7 +1147,7 @@ class Matrix private (
} else {
val residual = ps(bestColIx)
if (Matching.logging) {
- System.out.println("Chose column " + bestColIx);
+ System.out.println("Chose column " + bestColIx)
}
val constructor = getConstructor(residual)
val specialized = specialize(constructor, bestColIx, Some(residual))
@@ -1140,7 +1159,7 @@ class Matrix private (
def notBestRow: Matrix =
Matrix.fromRows(symlib, rows.patch(bestRowIx, Nil, 1), fringe, search)
- def notBestCol(colIx: Int): IndexedSeq[Column] =
+ def notBestCol(colIx: Int): immutable.IndexedSeq[Column] =
columns.patch(colIx, Nil, 1)
def notCol(colIx: Int): Matrix =
@@ -1179,7 +1198,7 @@ class Matrix private (
override def equals(other: Any): Boolean = other match {
case that: Matrix =>
- (that.canEqual(this)) &&
+ that.canEqual(this) &&
symlib == that.symlib &&
fringe == that.fringe &&
rows == that.rows &&
@@ -1188,7 +1207,7 @@ class Matrix private (
}
override lazy val hashCode: Int = {
- val state = Seq(symlib, rows, search)
+ val state = immutable.Seq(symlib, rows, search)
state.map(_.hashCode()).foldLeft(0)((a, b) => 31 * a + b)
}
}
@@ -1198,24 +1217,24 @@ object Matrix {
def fromRows(
symlib: Parser.SymLib,
- rows: IndexedSeq[Row],
- fringe: IndexedSeq[Fringe],
+ rows: immutable.IndexedSeq[Row],
+ fringe: immutable.IndexedSeq[Fringe],
search: Boolean
): Matrix =
new Matrix(symlib, null, rows, null, fringe, search)
def fromColumns(
symlib: Parser.SymLib,
- cols: IndexedSeq[Column],
- clauses: IndexedSeq[Clause],
+ cols: immutable.IndexedSeq[Column],
+ clauses: immutable.IndexedSeq[Clause],
search: Boolean
): Matrix =
new Matrix(symlib, cols, null, clauses, null, search)
private val cache = new ConcurrentHashMap[Matrix, DecisionTree]()
- def clearCache: Unit =
- cache.clear
+ def clearCache(): Unit =
+ cache.clear()
var id = 0
}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Occurrence.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Occurrence.scala
index 4f02be8e2..07d4b0487 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Occurrence.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Occurrence.scala
@@ -1,7 +1,6 @@
package org.kframework.backend.llvm.matching
import java.util
-import java.util.ArrayList
import org.kframework.backend.llvm.matching.pattern.Pattern
sealed trait Occurrence {
@@ -18,14 +17,14 @@ case class Num(i: Int, rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add(i.toString)
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Inj(rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add("-1")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Lit(name: String, hook: String) extends Occurrence {
@@ -55,48 +54,48 @@ case class Equal(o1: Occurrence, o2: Occurrence) extends Occurrence {
representation.addAll(o1.representation)
representation.add("and")
representation.addAll(o2.representation)
- val size = o1.size
+ val size: Int = o1.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Size(rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add("size")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Value(pat: Pattern[Option[Occurrence]], rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add(pat.toString + "_val")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Rem(pat: Pattern[Option[Occurrence]], rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add(pat.toString + "_rem")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class Choice(rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add("key")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class ChoiceValue(rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add("val")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
case class ChoiceRem(rest: Occurrence) extends Occurrence {
val representation = new util.ArrayList[AnyRef]()
representation.add("rem")
representation.addAll(rest.representation)
- val size = 1 + rest.size
+ val size: Int = 1 + rest.size
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
index e9ab71be9..299106bed 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
@@ -4,6 +4,7 @@ import com.runtimeverification.k.kore._
import com.runtimeverification.k.kore.implementation.{ DefaultBuilders => B }
import java.util
import java.util.Optional
+import scala.collection.immutable
case class AxiomInfo(
priority: Int,
@@ -47,11 +48,11 @@ object Parser {
}
class SymLib(
- symbols: Seq[SymbolOrAlias],
- sorts: Seq[Sort],
+ symbols: immutable.Seq[SymbolOrAlias],
+ sorts: immutable.Seq[Sort],
mod: Definition,
- overloadSeq: Seq[(SymbolOrAlias, SymbolOrAlias)],
- val heuristics: Seq[Heuristic]
+ overloadSeq: immutable.Seq[(SymbolOrAlias, SymbolOrAlias)],
+ val heuristics: immutable.Seq[Heuristic]
) {
val sortCache = new util.HashMap[Sort, SortInfo]()
@@ -67,8 +68,12 @@ object Parser {
.map(_.asInstanceOf[SortDeclaration])
.groupBy(_.sort.asInstanceOf[CompoundSort].ctr)
- private def instantiate(s: Sort, params: Seq[Sort], args: Seq[Sort]): Sort = {
- val map = (params, args).zipped.toMap
+ private def instantiate(
+ s: Sort,
+ params: immutable.Seq[Sort],
+ args: immutable.Seq[Sort]
+ ): Sort = {
+ val map = params.lazyZip(args).toMap
s match {
case v @ SortVariable(_) => map(v)
case _ => s
@@ -76,15 +81,19 @@ object Parser {
}
def isHooked(symbol: SymbolOrAlias): Boolean =
- return symbolDecls(symbol.ctr).head.isInstanceOf[HookSymbolDeclaration]
+ symbolDecls(symbol.ctr).head.isInstanceOf[HookSymbolDeclaration]
- private def instantiate(s: Seq[Sort], params: Seq[Sort], args: Seq[Sort]): Seq[Sort] =
+ private def instantiate(
+ s: immutable.Seq[Sort],
+ params: immutable.Seq[Sort],
+ args: immutable.Seq[Sort]
+ ): immutable.Seq[Sort] =
s.map(instantiate(_, params, args))
- val signatures: Map[SymbolOrAlias, (Seq[Sort], Sort, Attributes)] =
+ val signatures: Map[SymbolOrAlias, (immutable.Seq[Sort], Sort, Attributes)] =
symbols.map { symbol =>
if (symbol.ctr == "\\dv") {
- (symbol, (Seq(), symbol.params(0), B.Attributes(Seq())))
+ (symbol, (immutable.Seq(), symbol.params.head, B.Attributes(immutable.Seq())))
} else {
(
symbol,
@@ -105,10 +114,12 @@ object Parser {
}
}.toMap
- val constructorsForSort: Map[Sort, Seq[SymbolOrAlias]] =
+ val constructorsForSort: Map[Sort, immutable.Seq[SymbolOrAlias]] =
signatures
.groupBy(_._2._2)
- .mapValues(_.keys.filter(k => !hasAtt(signatures(k)._3, "function")).toSeq)
+ .view
+ .mapValues(_.keys.filter(k => !hasAtt(signatures(k)._3, "function")).to(immutable.Seq))
+ .toMap
private val sortAttData: Map[String, Attributes] =
sorts
@@ -124,23 +135,23 @@ object Parser {
def sortAtt(s: Sort): Attributes =
sortAttData(s.asInstanceOf[CompoundSort].ctr)
- val functions: Seq[SymbolOrAlias] =
+ val functions: immutable.Seq[SymbolOrAlias] =
signatures
.filter(s =>
s._2._3.patterns.exists(isAtt("anywhere", _)) || s._2._3.patterns
.exists(isAtt("function", _))
)
.keys
- .toSeq
+ .to(immutable.Seq)
- val overloads: Map[SymbolOrAlias, Seq[SymbolOrAlias]] =
- overloadSeq.groupBy(_._1).mapValues(_.map(_._2).toSeq)
+ val overloads: Map[SymbolOrAlias, immutable.Seq[SymbolOrAlias]] =
+ overloadSeq.groupBy(_._1).view.mapValues(_.map(_._2).to(immutable.Seq)).toMap
def isSubsorted(less: Sort, greater: Sort): Boolean =
- signatures.contains(B.SymbolOrAlias("inj", Seq(less, greater)))
+ signatures.contains(B.SymbolOrAlias("inj", immutable.Seq(less, greater)))
private val hookAtts: Map[String, String] =
- sortAttData.map(t => (t._1.substring(4), getStringAtt(t._2, "hook").getOrElse(""))).toMap
+ sortAttData.map(t => (t._1.substring(4), getStringAtt(t._2, "hook").getOrElse("")))
}
private def rulePriority(axiom: AxiomDeclaration, search: Boolean): Int =
@@ -180,7 +191,7 @@ object Parser {
axiom: (AxiomDeclaration, Int),
simplification: Boolean,
search: Boolean
- ): Seq[(Option[SymbolOrAlias], AxiomInfo)] = {
+ ): immutable.Seq[(Option[SymbolOrAlias], AxiomInfo)] = {
val splitted = split(axiom._1.pattern)
if (splitted.isDefined) {
val s = axiom._1
@@ -190,9 +201,9 @@ object Parser {
"non-executable"
) || (hasAtt(s, "simplification") && !simplification)
) {
- Seq()
+ immutable.Seq()
} else {
- Seq(
+ immutable.Seq(
(
splitted.get._1,
AxiomInfo(
@@ -209,7 +220,7 @@ object Parser {
)
}
} else {
- Seq()
+ immutable.Seq()
}
}
@@ -219,21 +230,25 @@ object Parser {
topPattern match {
case Rewrites(
s,
- And(_, (req @ Equals(_, _, _, _)) +: l +: Seq()),
- And(_, ens +: r +: Seq())
+ And(_, (req @ Equals(_, _, _, _)) +: l +: immutable.Seq()),
+ And(_, ens +: r +: immutable.Seq())
) =>
Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
- case Rewrites(s, And(_, (req @ Top(_)) +: l +: Seq()), And(_, ens +: r +: Seq())) =>
+ case Rewrites(
+ s,
+ And(_, (req @ Top(_)) +: l +: immutable.Seq()),
+ And(_, ens +: r +: immutable.Seq())
+ ) =>
Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
case Rewrites(
s,
- And(_, Not(_, _) +: And(_, req +: l +: Seq()) +: Seq()),
- And(_, ens +: r +: Seq())
+ And(_, Not(_, _) +: And(_, req +: l +: immutable.Seq()) +: immutable.Seq()),
+ And(_, ens +: r +: immutable.Seq())
) =>
Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
- case Rewrites(s, And(_, l +: req +: Seq()), And(_, r +: ens +: Seq())) =>
+ case Rewrites(s, And(_, l +: req +: immutable.Seq()), And(_, r +: ens +: immutable.Seq())) =>
Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
- case Rewrites(s, And(_, l +: req +: Seq()), r @ Application(_, _)) =>
+ case Rewrites(s, And(_, l +: req +: immutable.Seq()), r @ Application(_, _)) =>
Some((None, B.Rewrites(s, l, r), splitPredicate(req), None))
case _ => None
}
@@ -247,8 +262,8 @@ object Parser {
private def getPatterns(pat: Pattern): List[Pattern] =
pat match {
- case And(_, Mem(_, _, _, pat) +: pats +: Seq()) => pat :: getPatterns(pats)
- case Top(_) => Nil
+ case And(_, Mem(_, _, _, pat) +: pats +: immutable.Seq()) => pat :: getPatterns(pats)
+ case Top(_) => Nil
}
private def splitFunction(
@@ -257,8 +272,8 @@ object Parser {
topPattern match {
case Implies(
_,
- And(_, Not(_, _) +: And(_, req +: args +: Seq()) +: Seq()),
- Equals(i, o, Application(symbol, _), And(_, rhs +: ens +: Seq()))
+ And(_, Not(_, _) +: And(_, req +: args +: immutable.Seq()) +: immutable.Seq()),
+ Equals(i, o, Application(symbol, _), And(_, rhs +: ens +: immutable.Seq()))
) =>
Some(
Some(symbol),
@@ -268,8 +283,8 @@ object Parser {
)
case Implies(
_,
- And(_, req +: args +: Seq()),
- Equals(i, o, Application(symbol, _), And(_, rhs +: ens +: Seq()))
+ And(_, req +: args +: immutable.Seq()),
+ Equals(i, o, Application(symbol, _), And(_, rhs +: ens +: immutable.Seq()))
) =>
Some(
Some(symbol),
@@ -280,7 +295,7 @@ object Parser {
case Implies(
_,
req,
- Equals(i, o, app @ Application(symbol, _), And(_, rhs +: ens +: Seq()))
+ Equals(i, o, app @ Application(symbol, _), And(_, rhs +: ens +: immutable.Seq()))
) =>
Some(Some(symbol), B.Equals(i, o, app, rhs), splitPredicate(req), splitPredicate(ens))
case Implies(_, req, eq @ Equals(_, _, Application(symbol, _), _)) =>
@@ -289,7 +304,10 @@ object Parser {
case _ => None
}
- private def getSubstitution(pat: Pattern, subject: Seq[Pattern]): Map[String, Pattern] = {
+ private def getSubstitution(
+ pat: Pattern,
+ subject: immutable.Seq[Pattern]
+ ): Map[String, Pattern] = {
val pattern = pat.asInstanceOf[Application]
pattern.args.map(_.asInstanceOf[Variable].name).zip(subject).toMap
}
@@ -348,7 +366,7 @@ object Parser {
B.AxiomDeclaration(axiom.params, expandAliases(axiom.pattern, aliases), axiom.att)
.asInstanceOf[AxiomDeclaration]
- def getAxioms(defn: Definition): Seq[AxiomDeclaration] = {
+ def getAxioms(defn: Definition): immutable.Seq[AxiomDeclaration] = {
val aliases = defn.modules
.flatMap(_.decls)
.filter(_.isInstanceOf[AliasDeclaration])
@@ -362,23 +380,28 @@ object Parser {
.map(expandAliases(_, aliases))
}
- def getSorts(defn: Definition): Seq[Sort] =
+ def getSorts(defn: Definition): immutable.Seq[Sort] =
defn.modules
.flatMap(_.decls)
.filter(_.isInstanceOf[SortDeclaration])
.map(_.asInstanceOf[SortDeclaration].sort)
- def parseTopAxioms(axioms: Seq[AxiomDeclaration], search: Boolean): IndexedSeq[AxiomInfo] = {
- val withOwise = axioms.zipWithIndex.flatMap(parseAxiomSentence(splitTop, _, false, search))
+ def parseTopAxioms(
+ axioms: immutable.Seq[AxiomDeclaration],
+ search: Boolean
+ ): immutable.IndexedSeq[AxiomInfo] = {
+ val withOwise = axioms.zipWithIndex.flatMap(
+ parseAxiomSentence(splitTop, _, simplification = false, search = search)
+ )
withOwise.map(_._2).sortWith(_.priority < _.priority).toIndexedSeq
}
def parseFunctionAxioms(
- axioms: Seq[AxiomDeclaration],
+ axioms: immutable.Seq[AxiomDeclaration],
simplification: Boolean
- ): Map[SymbolOrAlias, IndexedSeq[AxiomInfo]] = {
+ ): Map[SymbolOrAlias, immutable.IndexedSeq[AxiomInfo]] = {
val withOwise = axioms.zipWithIndex.flatMap(
- parseAxiomSentence(a => splitFunction(a), _, simplification, true)
+ parseAxiomSentence(a => splitFunction(a), _, simplification, search = true)
)
withOwise
.sortWith(_._2.priority < _._2.priority)
@@ -386,17 +409,20 @@ object Parser {
.filter(_._1.isDefined)
.map(t => (t._1.get, t._2))
.groupBy(_._1)
+ .view
.mapValues(_.map(_._2))
+ .toMap
}
private def isConcrete(symbol: SymbolOrAlias): Boolean =
symbol.params.forall(_.isInstanceOf[CompoundSort])
- private def parsePatternForSymbols(pat: Pattern): Seq[SymbolOrAlias] =
+ private def parsePatternForSymbols(pat: Pattern): immutable.Seq[SymbolOrAlias] =
pat match {
- case And(_, ps) => ps.flatMap(parsePatternForSymbols)
- case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(parsePatternForSymbols)
- case DomainValue(sort, _) => Seq(B.SymbolOrAlias("\\dv", Seq(sort)))
+ case And(_, ps) => ps.flatMap(parsePatternForSymbols)
+ case Application(s, ps) =>
+ immutable.Seq(s).filter(isConcrete) ++ ps.flatMap(parsePatternForSymbols)
+ case DomainValue(sort, _) => immutable.Seq(B.SymbolOrAlias("\\dv", immutable.Seq(sort)))
case Ceil(_, _, p) => parsePatternForSymbols(p)
case Equals(_, _, p1, p2) => parsePatternForSymbols(p1) ++ parsePatternForSymbols(p2)
case Exists(_, _, p) => parsePatternForSymbols(p)
@@ -409,12 +435,14 @@ object Parser {
case Not(_, p) => parsePatternForSymbols(p)
case Or(_, ps) => ps.flatMap(parsePatternForSymbols)
case Rewrites(_, p1, p2) => parsePatternForSymbols(p1) ++ parsePatternForSymbols(p2)
- case _ => Seq()
+ case _ => immutable.Seq()
}
- private def getOverloads(axioms: Seq[AxiomDeclaration]): Seq[(SymbolOrAlias, SymbolOrAlias)] = {
+ private def getOverloads(
+ axioms: immutable.Seq[AxiomDeclaration]
+ ): immutable.Seq[(SymbolOrAlias, SymbolOrAlias)] = {
if (axioms.isEmpty) {
- Seq()
+ immutable.Seq()
}
axioms
.filter(hasAtt(_, "symbol-overload"))
@@ -424,6 +452,7 @@ object Parser {
(args.head, args(1)) match {
case (Application(g, _), Application(l, _)) => (g, l)
}
+ case _ => ???
})
}
@@ -453,8 +482,8 @@ object Parser {
def parseHeuristic(heuristic: Char): Heuristic =
heuristicMap(heuristic)
- def parseHeuristics(heuristics: String): Seq[Heuristic] =
- heuristics.toList.map(parseHeuristic(_))
+ def parseHeuristics(heuristics: String): immutable.Seq[Heuristic] =
+ heuristics.toList.map(parseHeuristic)
def parseSymbols(defn: Definition, heuristics: String): SymLib = {
val axioms = getAxioms(defn)
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/dt/DecisionTree.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/dt/DecisionTree.scala
index f8f58c81a..6a32e3e95 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/dt/DecisionTree.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/dt/DecisionTree.scala
@@ -9,22 +9,23 @@ import java.util.concurrent.ConcurrentHashMap
import org.kframework.backend.llvm.matching.pattern._
import org.kframework.backend.llvm.matching.Occurrence
import org.yaml.snakeyaml.Yaml
+import scala.collection.immutable
sealed trait DecisionTree {
def serializeToYaml(file: File): Unit = {
val writer = new OutputStreamWriter(
new FileOutputStream(file),
Charset.forName("UTF-8").newEncoder()
- );
+ )
new Yaml().dump(representation, writer)
writer.close()
}
- def serializeToYaml(file: File, residuals: Seq[(Pattern[String], Occurrence)]): Unit = {
+ def serializeToYaml(file: File, residuals: immutable.Seq[(Pattern[String], Occurrence)]): Unit = {
val writer = new OutputStreamWriter(
new FileOutputStream(file),
Charset.forName("UTF-8").newEncoder()
- );
+ )
val residualRepr = new util.ArrayList[AnyRef]()
for (entry <- residuals) {
val pair = new util.ArrayList[AnyRef]()
@@ -49,7 +50,7 @@ case class Failure private () extends DecisionTree {
that.isInstanceOf[AnyRef] && (this eq that.asInstanceOf[AnyRef])
}
-case class Leaf private (ordinal: Int, occurrences: Seq[(Occurrence, String)])
+case class Leaf private (ordinal: Int, occurrences: immutable.Seq[(Occurrence, String)])
extends DecisionTree {
val representation = new util.HashMap[String, AnyRef]()
val action = new util.ArrayList[AnyRef]()
@@ -70,7 +71,7 @@ case class Leaf private (ordinal: Int, occurrences: Seq[(Occurrence, String)])
case class SearchLeaf private (
ordinal: Int,
- occurrences: Seq[(Occurrence, String)],
+ occurrences: immutable.Seq[(Occurrence, String)],
child: DecisionTree
) extends DecisionTree {
val representation = new util.HashMap[String, AnyRef]()
@@ -94,7 +95,7 @@ case class SearchLeaf private (
case class Switch private (
occurrence: Occurrence,
hook: String,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
) extends DecisionTree {
val representation = new util.HashMap[String, AnyRef]()
@@ -122,7 +123,7 @@ case class SwitchLit private (
occurrence: Occurrence,
hook: String,
bitwidth: Int,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
) extends DecisionTree {
val representation = new util.HashMap[String, AnyRef]()
@@ -150,7 +151,7 @@ case class SwitchLit private (
case class Function private (
name: String,
occurrence: Occurrence,
- vars: Seq[(Occurrence, String)],
+ vars: immutable.Seq[(Occurrence, String)],
hook: String,
child: DecisionTree
) extends DecisionTree {
@@ -175,7 +176,7 @@ case class Function private (
case class CheckNull private (
occurrence: Occurrence,
hook: String,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
) extends DecisionTree {
val representation = new util.HashMap[String, AnyRef]()
@@ -252,27 +253,36 @@ object Failure {
}
object Leaf {
- private val cache = new ConcurrentHashMap[(Int, Seq[(Occurrence, String)]), Leaf]()
- def apply(ordinal: Int, occurrences: Seq[(Occurrence, String)]): Leaf =
+ private val cache = new ConcurrentHashMap[(Int, immutable.Seq[(Occurrence, String)]), Leaf]()
+ def apply(ordinal: Int, occurrences: immutable.Seq[(Occurrence, String)]): Leaf =
cache.computeIfAbsent((ordinal, occurrences), k => new Leaf(k._1, k._2))
}
object SearchLeaf {
private val cache =
- new ConcurrentHashMap[(Int, Seq[(Occurrence, String)], DecisionTree), SearchLeaf]()
- def apply(ordinal: Int, occurrences: Seq[(Occurrence, String)], child: DecisionTree): SearchLeaf =
+ new ConcurrentHashMap[(Int, immutable.Seq[(Occurrence, String)], DecisionTree), SearchLeaf]()
+ def apply(
+ ordinal: Int,
+ occurrences: immutable.Seq[(Occurrence, String)],
+ child: DecisionTree
+ ): SearchLeaf =
cache.computeIfAbsent((ordinal, occurrences, child), k => new SearchLeaf(k._1, k._2, k._3))
}
object Switch {
val cache = new ConcurrentHashMap[
- (Occurrence, String, Seq[(String, Seq[String], DecisionTree)], Option[DecisionTree]),
+ (
+ Occurrence,
+ String,
+ immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
+ Option[DecisionTree]
+ ),
Switch
]()
def apply(
occurrence: Occurrence,
hook: String,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
): Switch =
cache.computeIfAbsent(
@@ -283,14 +293,20 @@ object Switch {
object SwitchLit {
val cache = new ConcurrentHashMap[
- (Occurrence, String, Int, Seq[(String, Seq[String], DecisionTree)], Option[DecisionTree]),
+ (
+ Occurrence,
+ String,
+ Int,
+ immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
+ Option[DecisionTree]
+ ),
SwitchLit
]()
def apply(
occurrence: Occurrence,
hook: String,
bitwidth: Int,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
): SwitchLit =
cache.computeIfAbsent(
@@ -301,13 +317,13 @@ object SwitchLit {
object Function {
val cache = new ConcurrentHashMap[
- (String, Occurrence, Seq[(Occurrence, String)], String, DecisionTree),
+ (String, Occurrence, immutable.Seq[(Occurrence, String)], String, DecisionTree),
Function
]()
def apply(
name: String,
occurrence: Occurrence,
- vars: Seq[(Occurrence, String)],
+ vars: immutable.Seq[(Occurrence, String)],
hook: String,
child: DecisionTree
): Function =
@@ -319,13 +335,18 @@ object Function {
object CheckNull {
val cache = new ConcurrentHashMap[
- (Occurrence, String, Seq[(String, Seq[String], DecisionTree)], Option[DecisionTree]),
+ (
+ Occurrence,
+ String,
+ immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
+ Option[DecisionTree]
+ ),
CheckNull
]()
def apply(
occurrence: Occurrence,
hook: String,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
): CheckNull =
cache.computeIfAbsent(
@@ -374,7 +395,7 @@ object MakePattern {
for (p <- ps)
args.add(representPattern(p))
}
- assert(!result.isEmpty())
+ assert(!result.isEmpty)
result
}
def representResidual(pattern: Pattern[String]): util.HashMap[String, AnyRef] = {
@@ -398,7 +419,7 @@ object MakePattern {
for (p <- ps)
args.add(representResidual(p))
}
- assert(!result.isEmpty())
+ assert(!result.isEmpty)
result
}
}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala
index 4af8acc26..cfafe2924 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala
@@ -4,9 +4,10 @@ import com.runtimeverification.k.kore
import com.runtimeverification.k.kore.implementation.{ DefaultBuilders => B }
import com.runtimeverification.k.kore.SymbolOrAlias
import org.kframework.backend.llvm.matching._
+import scala.collection.immutable
sealed trait Pattern[T] {
- def signature(clause: Clause): Seq[Constructor]
+ def signature(clause: Clause): immutable.Seq[Constructor]
def isWildcard: Boolean
def isDefault: Boolean
def isSpecialized(
@@ -28,26 +29,27 @@ sealed trait Pattern[T] {
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]]
+ ): immutable.Seq[VariableBinding[T]]
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
maxPriority: Int
- ): Seq[Pattern[T]]
- def expandOr: Seq[Pattern[T]]
+ ): immutable.Seq[Pattern[T]]
+ def expandOr: immutable.Seq[Pattern[T]]
- def isChoice: Boolean = false
- def mapOrSetKeys: Seq[Pattern[T]] = Seq()
- def listRange(ix: Option[Constructor], o: Occurrence): Seq[(Occurrence, Int, Int)] = Seq()
+ def isChoice: Boolean = false
+ def mapOrSetKeys: immutable.Seq[Pattern[T]] = immutable.Seq()
+ def listRange(ix: Option[Constructor], o: Occurrence): immutable.Seq[(Occurrence, Int, Int)] =
+ immutable.Seq()
def overloadChildren(
f: Fringe,
ix: Option[Constructor],
residual: Option[Pattern[String]],
o: Occurrence
- ): Seq[(Constructor, Fringe, VariableBinding[T])] = Seq()
+ ): immutable.Seq[(Constructor, Fringe, VariableBinding[T])] = immutable.Seq()
def category: Option[SortCategory]
def variables: Set[T]
def canonicalize(clause: Clause): Pattern[Option[Occurrence]]
@@ -68,7 +70,7 @@ object Pattern {
case (_, AsP(_, _, pat)) => Pattern.mightUnify(p1, pat)
case (LiteralP(c1, _), LiteralP(c2, _)) => c1 == c2
case (SymbolP(c1, ps1), SymbolP(c2, ps2)) =>
- c1 == c2 && (ps1, ps2).zipped.toIterable.forall(t => Pattern.mightUnify(t._1, t._2))
+ c1 == c2 && ps1.lazyZip(ps2).toSeq.forall(t => Pattern.mightUnify(t._1, t._2))
case (ListP(_, _, _, _, _), ListP(_, _, _, _, _)) => true
case (MapP(_, _, _, _, _), MapP(_, _, _, _, _)) => true
case (SetP(_, _, _, _), SetP(_, _, _, _)) => true
@@ -82,7 +84,7 @@ object Pattern {
}
case class AsP[T](name: T, sort: SortCategory, pat: Pattern[T]) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] =
+ def signature(clause: Clause): immutable.Seq[Constructor] =
pat.signature(clause)
def isWildcard: Boolean = pat.isWildcard
def isDefault: Boolean = pat.isDefault
@@ -95,15 +97,15 @@ case class AsP[T](name: T, sort: SortCategory, pat: Pattern[T]) extends Pattern[
key: Option[Pattern[Option[Occurrence]]],
isEmpty: Boolean
): Double = h.scoreAs(this, f, c, key, isEmpty)
- override def isChoice: Boolean = pat.isChoice
- override def mapOrSetKeys: Seq[Pattern[T]] = pat.mapOrSetKeys
+ override def isChoice: Boolean = pat.isChoice
+ override def mapOrSetKeys: immutable.Seq[Pattern[T]] = pat.mapOrSetKeys
def bindings(
ix: Option[Constructor],
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] =
- Seq(new VariableBinding(name, sort, occurrence, residual)) ++ pat.bindings(
+ ): immutable.Seq[VariableBinding[T]] =
+ immutable.Seq(VariableBinding(name, sort, occurrence, residual)) ++ pat.bindings(
ix,
residual,
occurrence,
@@ -112,43 +114,47 @@ case class AsP[T](name: T, sort: SortCategory, pat: Pattern[T]) extends Pattern[
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
pat.expand(ix, isExact, fringes, f, clause, m)
- def expandOr: Seq[AsP[T]] = pat.expandOr.map(AsP(name, sort, _))
+ def expandOr: immutable.Seq[AsP[T]] = pat.expandOr.map(AsP(name, sort, _))
- override def listRange(ix: Option[Constructor], o: Occurrence): Seq[(Occurrence, Int, Int)] =
+ override def listRange(
+ ix: Option[Constructor],
+ o: Occurrence
+ ): immutable.Seq[(Occurrence, Int, Int)] =
pat.listRange(ix, o)
override def overloadChildren(
f: Fringe,
ix: Option[Constructor],
residual: Option[Pattern[String]],
o: Occurrence
- ): Seq[(Constructor, Fringe, VariableBinding[T])] = pat.overloadChildren(f, ix, residual, o)
+ ): immutable.Seq[(Constructor, Fringe, VariableBinding[T])] =
+ pat.overloadChildren(f, ix, residual, o)
def category: Option[SortCategory] = pat.category
lazy val variables: Set[T] = Set(name) ++ pat.variables
def canonicalize(clause: Clause): Pattern[Option[Occurrence]] =
AsP(clause.canonicalize(name.toString), sort, pat.canonicalize(clause))
- def decanonicalize: Pattern[String] = AsP("_", sort, pat.decanonicalize)
- def isBound(clause: Clause): Boolean = clause.isBound(name) && pat.isBound(clause)
- def isResidual(symlib: Parser.SymLib) = pat.isResidual(symlib)
- override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
- def toShortString: String = pat.toShortString + " #as " + name.toString
+ def decanonicalize: Pattern[String] = AsP("_", sort, pat.decanonicalize)
+ def isBound(clause: Clause): Boolean = clause.isBound(name) && pat.isBound(clause)
+ def isResidual(symlib: Parser.SymLib): Boolean = pat.isResidual(symlib)
+ override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
+ def toShortString: String = pat.toShortString + " #as " + name.toString
def toKORE(f: Fringe): kore.Pattern =
B.And(f.sort, pat.toKORE(f), B.Variable(name.toString, f.sort))
}
case class ListP[T] private (
- head: Seq[Pattern[T]],
+ head: immutable.Seq[Pattern[T]],
frame: Option[Pattern[T]],
- tail: Seq[Pattern[T]],
+ tail: immutable.Seq[Pattern[T]],
ctr: SymbolOrAlias,
orig: Pattern[T]
) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] =
+ def signature(clause: Clause): immutable.Seq[Constructor] =
(0 to (head.size + tail.size)).map(ListC(ctr, _))
def isWildcard = false
def isDefault: Boolean = frame.isDefined
@@ -179,25 +185,25 @@ case class ListP[T] private (
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] =
+ ): immutable.Seq[VariableBinding[T]] =
if (frame.isEmpty) {
- Seq()
+ immutable.Seq()
} else
ix.get match {
case listC: ListC =>
val len = listC.length
frame.get.bindings(None, residual, Num(len, occurrence), symlib)
case _ =>
- Seq()
+ immutable.Seq()
}
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
ix match {
case ListC(_, len) =>
head ++ (0 until len - head.size - tail.size).map(_ =>
@@ -205,8 +211,8 @@ case class ListP[T] private (
) ++ tail
case _ => ???
}
- def expandOr: Seq[Pattern[T]] = {
- val withHead = head.indices.foldLeft(Seq(this))((accum, ix) =>
+ def expandOr: immutable.Seq[Pattern[T]] = {
+ val withHead = head.indices.foldLeft(immutable.Seq(this))((accum, ix) =>
accum.flatMap(l =>
l.head(ix).expandOr.map(p => new ListP(l.head.updated(ix, p), l.frame, l.tail, ctr, orig))
)
@@ -225,13 +231,16 @@ case class ListP[T] private (
}
}
- override def listRange(ix: Option[Constructor], o: Occurrence): Seq[(Occurrence, Int, Int)] =
+ override def listRange(
+ ix: Option[Constructor],
+ o: Occurrence
+ ): immutable.Seq[(Occurrence, Int, Int)] =
ix match {
- case Some(ListC(_, len)) => Seq((Num(len, o), head.size, tail.size))
- case _ => Seq()
+ case Some(ListC(_, len)) => immutable.Seq((Num(len, o), head.size, tail.size))
+ case _ => immutable.Seq()
}
- def category = Some(ListS())
+ def category: Option[SortCategory] = Some(ListS())
lazy val variables: Set[T] = head.flatMap(_.variables).toSet ++ tail
.flatMap(_.variables)
.toSet ++ frame.map(_.variables).getOrElse(Set())
@@ -261,9 +270,9 @@ case class ListP[T] private (
object ListP {
def apply[T](
- head: Seq[Pattern[T]],
+ head: immutable.Seq[Pattern[T]],
frame: Option[Pattern[T]],
- tail: Seq[Pattern[T]],
+ tail: immutable.Seq[Pattern[T]],
ctr: SymbolOrAlias,
orig: Pattern[T]
): Pattern[T] =
@@ -275,8 +284,8 @@ object ListP {
}
case class LiteralP[T](literal: String, sort: SortCategory) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] =
- Seq(LiteralC(literal))
+ def signature(clause: Clause): immutable.Seq[Constructor] =
+ immutable.Seq(LiteralC(literal))
def isWildcard = false
def isDefault = false
def isSpecialized(ix: Constructor, isExact: Boolean, f: Fringe, c: Clause, m: Int): Boolean =
@@ -295,18 +304,18 @@ case class LiteralP[T](literal: String, sort: SortCategory) extends Pattern[T] {
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] = Seq()
+ ): immutable.Seq[VariableBinding[T]] = immutable.Seq()
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] = Seq()
- def expandOr: Seq[Pattern[T]] = Seq(this)
+ ): immutable.Seq[Pattern[T]] = immutable.Seq()
+ def expandOr: immutable.Seq[Pattern[T]] = immutable.Seq(this)
- def category = Some(sort)
+ def category: Option[SortCategory] = Some(sort)
def variables: Set[T] = Set()
def canonicalize(clause: Clause): Pattern[Option[Occurrence]] = LiteralP(literal, sort)
def decanonicalize: Pattern[String] = LiteralP(literal, sort)
@@ -319,29 +328,29 @@ case class LiteralP[T](literal: String, sort: SortCategory) extends Pattern[T] {
}
case class MapP[T] private (
- keys: Seq[Pattern[T]],
- values: Seq[Pattern[T]],
+ keys: immutable.Seq[Pattern[T]],
+ values: immutable.Seq[Pattern[T]],
frame: Option[Pattern[T]],
ctr: SymbolOrAlias,
orig: Pattern[T]
) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] =
+ def signature(clause: Clause): immutable.Seq[Constructor] =
if (keys.isEmpty && frame.isEmpty) {
- Seq(Empty())
+ immutable.Seq(Empty())
} else if (keys.isEmpty) {
frame.get.signature(clause)
} else if (frame.isEmpty) {
keys.flatMap(key =>
- Seq(
+ immutable.Seq(
HasKey(isSet = false, ctr, clause.canonicalize(key)),
- HasNoKey(false, clause.canonicalize(key))
+ HasNoKey(isSet = false, clause.canonicalize(key))
)
)
} else {
keys.flatMap(key =>
- Seq(
+ immutable.Seq(
HasKey(isSet = false, ctr, clause.canonicalize(key)),
- HasNoKey(false, clause.canonicalize(key))
+ HasNoKey(isSet = false, clause.canonicalize(key))
)
) ++ frame.get.signature(clause)
}
@@ -379,28 +388,28 @@ case class MapP[T] private (
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] =
+ ): immutable.Seq[VariableBinding[T]] =
if (keys.isEmpty && values.isEmpty && frame.isDefined) {
frame.get.bindings(None, residual, occurrence, symlib)
} else {
- Seq()
+ immutable.Seq()
}
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
maxPriority: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
ix match {
- case Empty() => Seq()
+ case Empty() => immutable.Seq()
case HasKey(_, _, Some(p)) =>
val canonKs = keys.map(_.canonicalize(clause))
canonKs.indexOf(p) match {
- case -1 => Seq(WildcardP(), WildcardP(), this)
+ case -1 => immutable.Seq(WildcardP(), WildcardP(), this)
case i =>
- Seq(
+ immutable.Seq(
values(i),
MapP(
keys.take(i) ++ keys.takeRight(keys.size - i - 1),
@@ -412,17 +421,17 @@ case class MapP[T] private (
WildcardP()
)
}
- case HasNoKey(_, _) | NonEmpty() => Seq(this)
+ case HasNoKey(_, _) | NonEmpty() => immutable.Seq(this)
case HasKey(_, _, None) =>
if (keys.isEmpty && frame.isDefined) {
frame.get.expand(ix, isExact, fringes, f, clause, maxPriority)
} else {
- Seq(keys.head, values.head, MapP(keys.tail, values.tail, frame, ctr, orig))
+ immutable.Seq(keys.head, values.head, MapP(keys.tail, values.tail, frame, ctr, orig))
}
case _ => ???
}
- def expandOr: Seq[Pattern[T]] = {
- val withKeys = keys.indices.foldLeft(Seq(this))((accum, ix) =>
+ def expandOr: immutable.Seq[Pattern[T]] = {
+ val withKeys = keys.indices.foldLeft(immutable.Seq(this))((accum, ix) =>
accum.flatMap(m =>
m.keys(ix).expandOr.map(p => new MapP(m.keys.updated(ix, p), m.values, m.frame, ctr, orig))
)
@@ -443,9 +452,9 @@ case class MapP[T] private (
}
}
- override def mapOrSetKeys: Seq[Pattern[T]] = keys
+ override def mapOrSetKeys: immutable.Seq[Pattern[T]] = keys
- def category = Some(MapS())
+ def category: Option[SortCategory] = Some(MapS())
lazy val variables: Set[T] = keys.flatMap(_.variables).toSet ++ values
.flatMap(_.variables)
.toSet ++ frame.map(_.variables).getOrElse(Set())
@@ -475,8 +484,8 @@ case class MapP[T] private (
object MapP {
def apply[T](
- keys: Seq[Pattern[T]],
- values: Seq[Pattern[T]],
+ keys: immutable.Seq[Pattern[T]],
+ values: immutable.Seq[Pattern[T]],
frame: Option[Pattern[T]],
ctr: SymbolOrAlias,
orig: Pattern[T]
@@ -490,10 +499,10 @@ object MapP {
}
}
-case class OrP[T](ps: Seq[Pattern[T]]) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] = ps.flatMap(_.signature(clause))
- def isWildcard: Boolean = ps.forall(_.isWildcard)
- def isDefault: Boolean = ???
+case class OrP[T](ps: immutable.Seq[Pattern[T]]) extends Pattern[T] {
+ def signature(clause: Clause): immutable.Seq[Constructor] = ps.flatMap(_.signature(clause))
+ def isWildcard: Boolean = ps.forall(_.isWildcard)
+ def isDefault: Boolean = ???
def isSpecialized(ix: Constructor, isExact: Boolean, f: Fringe, c: Clause, m: Int): Boolean = ???
def score(
h: Heuristic,
@@ -502,23 +511,23 @@ case class OrP[T](ps: Seq[Pattern[T]]) extends Pattern[T] {
key: Option[Pattern[Option[Occurrence]]],
isEmpty: Boolean
): Double = h.scoreOr(this, f, c, key, isEmpty)
- override def isChoice: Boolean = ps.exists(_.isChoice)
- override def mapOrSetKeys: Seq[Pattern[T]] = ps.flatMap(_.mapOrSetKeys)
+ override def isChoice: Boolean = ps.exists(_.isChoice)
+ override def mapOrSetKeys: immutable.Seq[Pattern[T]] = ps.flatMap(_.mapOrSetKeys)
def bindings(
ix: Option[Constructor],
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] = ???
+ ): immutable.Seq[VariableBinding[T]] = ???
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] = ???
- def expandOr: Seq[Pattern[T]] = ps.flatMap(_.expandOr)
+ ): immutable.Seq[Pattern[T]] = ???
+ def expandOr: immutable.Seq[Pattern[T]] = ps.flatMap(_.expandOr)
def category: Option[SortCategory] = {
val s = ps.map(_.category).filter(_.isDefined)
if (s.isEmpty) {
@@ -531,11 +540,11 @@ case class OrP[T](ps: Seq[Pattern[T]]) extends Pattern[T] {
def canonicalize(clause: Clause): Pattern[Option[Occurrence]] = OrP(
ps.map(_.canonicalize(clause))
)
- def decanonicalize: Pattern[String] = OrP(ps.map(_.decanonicalize))
- def isBound(clause: Clause): Boolean = ps.forall(_.isBound(clause))
- def isResidual(symlib: Parser.SymLib) = ???
- override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
- def toShortString: String = ps.map(_.toShortString).mkString(" #Or ")
+ def decanonicalize: Pattern[String] = OrP(ps.map(_.decanonicalize))
+ def isBound(clause: Clause): Boolean = ps.forall(_.isBound(clause))
+ def isResidual(symlib: Parser.SymLib): Boolean = ???
+ override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
+ def toShortString: String = ps.map(_.toShortString).mkString(" #Or ")
def toKORE(f: Fringe): kore.Pattern =
ps.map(_.toKORE(f)).reduce((l, r) => B.Or(f.sort, l, r))
}
@@ -544,35 +553,35 @@ object OrP {
def apply[T](p1: Pattern[T], p2: Pattern[T]): OrP[T] =
(p1, p2) match {
case (OrP(ps1), OrP(ps2)) => OrP(ps1 ++ ps2)
- case (OrP(ps1), _) => OrP(ps1 ++ Seq(p2))
- case (_, OrP(ps2)) => OrP(Seq(p1) ++ ps2)
- case _ => OrP(Seq(p1, p2))
+ case (OrP(ps1), _) => OrP(ps1 ++ immutable.Seq(p2))
+ case (_, OrP(ps2)) => OrP(immutable.Seq(p1) ++ ps2)
+ case _ => OrP(immutable.Seq(p1, p2))
}
}
case class SetP[T] private (
- elements: Seq[Pattern[T]],
+ elements: immutable.Seq[Pattern[T]],
frame: Option[Pattern[T]],
ctr: SymbolOrAlias,
orig: Pattern[T]
) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] =
+ def signature(clause: Clause): immutable.Seq[Constructor] =
if (elements.isEmpty && frame.isEmpty) {
- Seq(Empty())
+ immutable.Seq(Empty())
} else if (elements.isEmpty) {
frame.get.signature(clause)
} else if (frame.isEmpty) {
elements.flatMap(elem =>
- Seq(
+ immutable.Seq(
HasKey(isSet = true, ctr, clause.canonicalize(elem)),
- HasNoKey(true, clause.canonicalize(elem))
+ HasNoKey(isSet = true, clause.canonicalize(elem))
)
)
} else {
elements.flatMap(elem =>
- Seq(
+ immutable.Seq(
HasKey(isSet = true, ctr, clause.canonicalize(elem)),
- HasNoKey(true, clause.canonicalize(elem))
+ HasNoKey(isSet = true, clause.canonicalize(elem))
)
) ++ frame.get.signature(clause)
}
@@ -609,43 +618,43 @@ case class SetP[T] private (
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] =
+ ): immutable.Seq[VariableBinding[T]] =
if (elements.isEmpty && frame.isDefined) {
frame.get.bindings(None, residual, occurrence, symlib)
} else {
- Seq()
+ immutable.Seq()
}
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
maxPriority: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
ix match {
- case Empty() => Seq()
+ case Empty() => immutable.Seq()
case HasKey(_, _, Some(p)) =>
val canonEs = elements.map(_.canonicalize(clause))
canonEs.indexOf(p) match {
- case -1 => Seq(WildcardP(), this)
+ case -1 => immutable.Seq(WildcardP(), this)
case i =>
- Seq(
+ immutable.Seq(
SetP(elements.take(i) ++ elements.takeRight(elements.size - i - 1), frame, ctr, orig),
WildcardP()
)
}
- case HasNoKey(_, _) | NonEmpty() => Seq(this)
+ case HasNoKey(_, _) | NonEmpty() => immutable.Seq(this)
case HasKey(_, _, None) =>
if (elements.isEmpty && frame.isDefined) {
frame.get.expand(ix, isExact, fringes, f, clause, maxPriority)
} else {
- Seq(elements.head, SetP(elements.tail, frame, ctr, orig))
+ immutable.Seq(elements.head, SetP(elements.tail, frame, ctr, orig))
}
case _ => ???
}
- def expandOr: Seq[Pattern[T]] = {
- val withElements = elements.indices.foldLeft(Seq(this))((accum, ix) =>
+ def expandOr: immutable.Seq[Pattern[T]] = {
+ val withElements = elements.indices.foldLeft(immutable.Seq(this))((accum, ix) =>
accum.flatMap(s =>
s.elements(ix).expandOr.map(p => new SetP(s.elements.updated(ix, p), s.frame, ctr, orig))
)
@@ -657,9 +666,9 @@ case class SetP[T] private (
}
}
- override def mapOrSetKeys: Seq[Pattern[T]] = elements
+ override def mapOrSetKeys: immutable.Seq[Pattern[T]] = elements
- def category = Some(SetS())
+ def category: Option[SortCategory] = Some(SetS())
lazy val variables: Set[T] =
elements.flatMap(_.variables).toSet ++ frame.map(_.variables).getOrElse(Set())
def canonicalize(clause: Clause): SetP[Option[Occurrence]] = new SetP(
@@ -680,7 +689,7 @@ case class SetP[T] private (
object SetP {
def apply[T](
- elements: Seq[Pattern[T]],
+ elements: immutable.Seq[Pattern[T]],
frame: Option[Pattern[T]],
ctr: SymbolOrAlias,
orig: Pattern[T]
@@ -692,19 +701,22 @@ object SetP {
}
}
-case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] = Seq(SymbolC(sym))
- def isWildcard = false
- def isDefault = false
+case class SymbolP[T](sym: SymbolOrAlias, ps: immutable.Seq[Pattern[T]]) extends Pattern[T] {
+ def signature(clause: Clause): immutable.Seq[Constructor] = immutable.Seq(SymbolC(sym))
+ def isWildcard = false
+ def isDefault = false
def isSpecialized(ix: Constructor, isExact: Boolean, f: Fringe, clause: Clause, m: Int): Boolean =
(ix, sym) match {
- case (SymbolC(SymbolOrAlias("inj", Seq(a, c))), SymbolOrAlias("inj", Seq(b, c2))) =>
+ case (
+ SymbolC(SymbolOrAlias("inj", immutable.Seq(a, c))),
+ SymbolOrAlias("inj", immutable.Seq(b, c2))
+ ) =>
lazy val f2 = f.expand(SymbolC(sym)).head
c == c2 && (a == b || (f.symlib.isSubsorted(b, a) && !isExact) || (f.symlib.isSubsorted(
a,
b
) && f2.sortInfo.category == SymbolS() && ps.head.isSpecialized(
- SymbolC(B.SymbolOrAlias("inj", Seq(a, b))),
+ SymbolC(B.SymbolOrAlias("inj", immutable.Seq(a, b))),
isExact,
f2,
clause,
@@ -715,6 +727,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
lazy val f2 = f.expand(ix).head
less.exists(isValidOverload(f2, isExact, clause, m, f.expand(SymbolC(sym)), _))
case (SymbolC(ix2), _) => ix2 == sym
+ case _ => ???
}
def score(
h: Heuristic,
@@ -728,36 +741,42 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] =
+ ): immutable.Seq[VariableBinding[T]] =
(ix, sym) match {
- case (Some(SymbolC(SymbolOrAlias("inj", Seq(a, _)))), SymbolOrAlias("inj", Seq(b, _))) =>
+ case (
+ Some(SymbolC(SymbolOrAlias("inj", immutable.Seq(a, _)))),
+ SymbolOrAlias("inj", immutable.Seq(b, _))
+ ) =>
if (a == b || !symlib.isSubsorted(a, b)) {
- Seq()
+ immutable.Seq()
} else {
ps.head.bindings(
- Some(SymbolC(B.SymbolOrAlias("inj", Seq(a, b)))),
+ Some(SymbolC(B.SymbolOrAlias("inj", immutable.Seq(a, b)))),
residual,
occurrence,
symlib
)
}
- case _ => Seq()
+ case _ => immutable.Seq()
}
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
(ix, sym) match {
- case (SymbolC(SymbolOrAlias("inj", Seq(a, _))), inj @ SymbolOrAlias("inj", Seq(b, _))) =>
+ case (
+ SymbolC(SymbolOrAlias("inj", immutable.Seq(a, _))),
+ inj @ SymbolOrAlias("inj", immutable.Seq(b, _))
+ ) =>
if (a == b) {
- Seq(ps.head)
+ immutable.Seq(ps.head)
} else if (f.symlib.isSubsorted(a, b)) {
ps.head.expand(
- SymbolC(B.SymbolOrAlias("inj", Seq(a, b))),
+ SymbolC(B.SymbolOrAlias("inj", immutable.Seq(a, b))),
isExact,
fringes,
f.expand(SymbolC(inj)).head,
@@ -765,35 +784,37 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
m
)
} else {
- Seq(SymbolP(B.SymbolOrAlias("inj", Seq(b, a)), Seq(ps.head)))
+ immutable.Seq(
+ SymbolP(B.SymbolOrAlias("inj", immutable.Seq(b, a)), immutable.Seq(ps.head))
+ )
}
case (SymbolC(SymbolOrAlias("inj", _)), _) =>
val less = f.overloads(sym)
val f2 = fringes.head
val fringePs = f.expand(SymbolC(sym))
val validLess = less.filter(isValidOverload(f2, isExact, clause, m, fringePs, _)) match {
- case Seq(head) => head
+ case immutable.Seq(head) => head
}
val fringeTs = f2.expand(SymbolC(validLess))
- val newPs = (ps, fringePs, fringeTs).zipped.map { case (p, fringeP, fringeT) =>
+ val newPs = ps.lazyZip(fringePs).lazyZip(fringeTs).map { case (p, fringeP, fringeT) =>
if (fringeP.sort == fringeT.sort) {
p
} else {
p.expand(
- SymbolC(B.SymbolOrAlias("inj", Seq(fringeT.sort, fringeP.sort))),
+ SymbolC(B.SymbolOrAlias("inj", immutable.Seq(fringeT.sort, fringeP.sort))),
isExact,
- Seq(fringeT),
+ immutable.Seq(fringeT),
fringeP,
clause,
m
).head
}
}
- Seq(SymbolP(validLess, newPs))
+ immutable.Seq(SymbolP(validLess, newPs))
case _ => ps
}
- def expandOr: Seq[Pattern[T]] =
- ps.indices.foldLeft(Seq(this))((accum, ix) =>
+ def expandOr: immutable.Seq[Pattern[T]] =
+ ps.indices.foldLeft(immutable.Seq(this))((accum, ix) =>
accum.flatMap(s => s.ps(ix).expandOr.map(p => SymbolP(sym, s.ps.updated(ix, p))))
)
@@ -804,7 +825,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
isExact: Boolean,
clause: Clause,
m: Int,
- fringePs: Seq[Fringe],
+ fringePs: immutable.Seq[Fringe],
less: SymbolOrAlias
): Boolean = {
def isValidChild(p: Pattern[T], fringeP: Fringe, fringeT: Fringe): Boolean =
@@ -812,7 +833,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
fringeT.sort,
fringeP.sort
) && fringeP.sortInfo.category == SymbolS() && p.isSpecialized(
- SymbolC(B.SymbolOrAlias("inj", Seq(fringeT.sort, fringeP.sort))),
+ SymbolC(B.SymbolOrAlias("inj", immutable.Seq(fringeT.sort, fringeP.sort))),
false,
fringeP,
clause,
@@ -822,7 +843,9 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
val cons = SymbolC(less)
if (f.contains(cons)) {
val fringeTs = f.expand(cons)
- (ps, fringePs, fringeTs).zipped.toIterable
+ ps.lazyZip(fringePs)
+ .lazyZip(fringeTs)
+ .toSeq
.map(t => isValidChild(t._1, t._2, t._3))
.forall(identity)
} else {
@@ -840,18 +863,18 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
ix: Option[Constructor],
residual: Option[Pattern[String]],
o: Occurrence
- ): Seq[(Constructor, Fringe, VariableBinding[T])] = {
+ ): immutable.Seq[(Constructor, Fringe, VariableBinding[T])] = {
def getVar(
fringeP: Fringe,
fringeT: Fringe,
pat: Pattern[T],
i: Int
- ): Seq[(Constructor, Fringe, VariableBinding[T])] = {
+ ): immutable.Seq[(Constructor, Fringe, VariableBinding[T])] = {
val vars = pat.bindings(None, residual, Inj(Num(i, o)), f.symlib) /* compute variable bindings
* for this pattern */
- val child = SymbolC(B.SymbolOrAlias("inj", Seq(fringeT.sort, fringeP.sort)))
+ val child = SymbolC(B.SymbolOrAlias("inj", immutable.Seq(fringeT.sort, fringeP.sort)))
if (fringeP.sort == fringeT.sort) {
- Seq() // exact match, so no bindings
+ immutable.Seq() // exact match, so no bindings
} else {
val childOverloads = pat.overloadChildren(fringeP, Some(child), residual, Num(i, o)) /*
* recurse into child term */
@@ -859,14 +882,17 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
}
}
(ix, sym) match {
- case (Some(SymbolC(SymbolOrAlias("inj", Seq(a, _)))), SymbolOrAlias("inj", Seq(b, _))) =>
+ case (
+ Some(SymbolC(SymbolOrAlias("inj", immutable.Seq(a, _)))),
+ SymbolOrAlias("inj", immutable.Seq(b, _))
+ ) =>
if (a == b || !f.symlib.isSubsorted(a, b)) { // exact match, don't recurse
- Seq()
+ immutable.Seq()
} else {
val fringeB = f.expand(SymbolC(sym)).head
ps.head.overloadChildren(
fringeB,
- Some(SymbolC(B.SymbolOrAlias("inj", Seq(a, b)))),
+ Some(SymbolC(B.SymbolOrAlias("inj", immutable.Seq(a, b)))),
residual,
o
)
@@ -878,13 +904,16 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
val child = less.find(c => f2.contains(SymbolC(c))).map(c => f2.expand(SymbolC(c)))
child match {
- case None => Seq() // no overloads exist
+ case None => immutable.Seq() // no overloads exist
case Some(fringeTs) =>
- (fringePs, fringeTs, ps).zipped.toSeq.zipWithIndex.flatMap(t =>
- getVar(t._1._1, t._1._2, t._1._3, t._2)
- ) // compute variable bindings
+ fringePs
+ .lazyZip(fringeTs)
+ .lazyZip(ps)
+ .to(immutable.Seq)
+ .zipWithIndex
+ .flatMap(t => getVar(t._1._1, t._1._2, t._1._3, t._2)) // compute variable bindings
}
- case _ => Seq()
+ case _ => immutable.Seq()
}
}
@@ -894,7 +923,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
SymbolP(sym, ps.map(_.canonicalize(clause)))
def decanonicalize: Pattern[String] = SymbolP(sym, ps.map(_.decanonicalize))
def isBound(clause: Clause): Boolean = ps.forall(_.isBound(clause))
- def isResidual(symlib: Parser.SymLib) =
+ def isResidual(symlib: Parser.SymLib): Boolean =
symlib.functions
.contains(sym) || Parser.getStringAtt(symlib.signatures(sym)._3, "anywhere").isDefined
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
@@ -904,9 +933,9 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T
}
case class VariableP[T](name: T, sort: SortCategory) extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] = Seq()
- def isWildcard = true
- def isDefault = true
+ def signature(clause: Clause): immutable.Seq[Constructor] = immutable.Seq()
+ def isWildcard = true
+ def isDefault = true
def isSpecialized(
ix: Constructor,
ixExact: Boolean,
@@ -930,18 +959,18 @@ case class VariableP[T](name: T, sort: SortCategory) extends Pattern[T] {
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] =
- Seq(new VariableBinding(name, sort, occurrence, residual))
+ ): immutable.Seq[VariableBinding[T]] =
+ immutable.Seq(VariableBinding(name, sort, occurrence, residual))
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
fringes.map(_ => WildcardP().asInstanceOf[Pattern[T]])
- def expandOr: Seq[Pattern[T]] = Seq(this)
+ def expandOr: immutable.Seq[Pattern[T]] = immutable.Seq(this)
def category: None.type = None
lazy val variables: Set[T] = Set(name)
@@ -963,9 +992,9 @@ case class VariableP[T](name: T, sort: SortCategory) extends Pattern[T] {
}
case class WildcardP[T]() extends Pattern[T] {
- def signature(clause: Clause): Seq[Constructor] = Seq()
- def isWildcard = true
- def isDefault = true
+ def signature(clause: Clause): immutable.Seq[Constructor] = immutable.Seq()
+ def isWildcard = true
+ def isDefault = true
def isSpecialized(
ix: Constructor,
isExact: Boolean,
@@ -990,17 +1019,17 @@ case class WildcardP[T]() extends Pattern[T] {
residual: Option[Pattern[String]],
occurrence: Occurrence,
symlib: Parser.SymLib
- ): Seq[VariableBinding[T]] = Seq()
+ ): immutable.Seq[VariableBinding[T]] = immutable.Seq()
def expand(
ix: Constructor,
isExact: Boolean,
- fringes: Seq[Fringe],
+ fringes: immutable.Seq[Fringe],
f: Fringe,
clause: Clause,
m: Int
- ): Seq[Pattern[T]] =
+ ): immutable.Seq[Pattern[T]] =
fringes.map(_ => WildcardP().asInstanceOf[Pattern[T]])
- def expandOr: Seq[Pattern[T]] = Seq(this)
+ def expandOr: immutable.Seq[Pattern[T]] = immutable.Seq(this)
def category: None.type = None
def variables: Set[T] = Set()
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
index 210587a90..eeea38831 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
@@ -7,13 +7,18 @@ import org.kframework.backend.llvm.matching._
import org.kframework.backend.llvm.matching.dt._
import org.kframework.backend.llvm.matching.MatchingException
import org.kframework.mpfr._
+import scala.collection.immutable
sealed trait SortCategory {
def hookAtt: String
- def hasIncompleteSignature(sigma: Seq[Constructor], isExact: Boolean, sortInfo: SortInfo): Boolean
- def hasIncompleteSignature(sigma: Seq[Constructor], f: Fringe): Boolean =
+ def hasIncompleteSignature(
+ sigma: immutable.Seq[Constructor],
+ isExact: Boolean,
+ sortInfo: SortInfo
+ ): Boolean
+ def hasIncompleteSignature(sigma: immutable.Seq[Constructor], f: Fringe): Boolean =
hasIncompleteSignature(sigma, f.isExact, f.sortInfo)
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String]
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String]
def isExpandDefault: Boolean = false
def equalityFun: String
def tree(matrix: Matrix): DecisionTree
@@ -43,7 +48,7 @@ object SortCategory {
case Some("BOOL.Bool") => BoolS()
case Some("KVAR.KVar") => VarS()
case Some("BUFFER.StringBuffer") => BufferS()
- case Some("MINT.MInt") => MIntS(getBitwidth(s.asInstanceOf[CompoundSort].params(0), symlib))
+ case Some("MINT.MInt") => MIntS(getBitwidth(s.asInstanceOf[CompoundSort].params.head, symlib))
case Some("BAG.Bag") =>
throw new MatchingException(
MatchingException.Type.COMPILER_ERROR,
@@ -59,19 +64,19 @@ object SortCategory {
case class SymbolS() extends SortCategory {
def hookAtt = "STRING.String"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = sigma.contains(
Empty()
) || (!isExact && sigma.size != sortInfo.length) || (isExact && sigma.size != sortInfo.exactLength)
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = {
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = {
val sym = if (f.isExact) {
(f.sortInfo.exactConstructors.toSet -- sigma.map(_.asInstanceOf[SymbolC].sym).toSet).head
} else {
(f.sortInfo.constructors.toSet -- sigma.map(_.asInstanceOf[SymbolC].sym).toSet).head
}
- SymbolP(sym, Seq.fill[Pattern[String]](f.symlib.signatures(sym)._1.size)(WildcardP()))
+ SymbolP(sym, immutable.Seq.fill[Pattern[String]](f.symlib.signatures(sym)._1.size)(WildcardP()))
}
def equalityFun = "hook_KEQUAL_eq"
// not matching a builtin, therefore construct a regular switch
@@ -81,11 +86,11 @@ case class SymbolS() extends SortCategory {
}
abstract class EqualLiteral() extends SortCategory {
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = true
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = {
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = {
var idx = 0
val strs = sigma.map(_.asInstanceOf[LiteralC].literal).toSet
while (true) {
@@ -103,13 +108,16 @@ abstract class EqualLiteral() extends SortCategory {
def tree(matrix: Matrix): DecisionTree =
tree(matrix, matrix.cases)
- private def tree(matrix: Matrix, ls: Seq[(String, Seq[String], Matrix)]): DecisionTree = {
+ private def tree(
+ matrix: Matrix,
+ ls: immutable.Seq[(String, immutable.Seq[String], Matrix)]
+ ): DecisionTree = {
val litO = matrix.bestCol.fringe.occurrence
val defaultMatrix = matrix.default(matrix.bestColIx, matrix.sigma)
if (defaultMatrix.isDefined && ls.isEmpty) {
// if no specializations remain and a default exists, consume the occurrence and continue with
// the default
- Switch(litO, hookAtt, Seq(), Some(defaultMatrix.get.compile))
+ Switch(litO, hookAtt, immutable.Seq(), Some(defaultMatrix.get.compile))
} else if (ls.isEmpty) {
// if no specializations remain and no default exists, fail the match
Failure()
@@ -126,15 +134,19 @@ abstract class EqualLiteral() extends SortCategory {
Function(
equalityFun,
eqO,
- Seq((litO, hookAtt), (newO, hookAtt)),
+ immutable.Seq((litO, hookAtt), (newO, hookAtt)),
"BOOL.Bool",
SwitchLit(
eqO,
"BOOL.Bool",
1,
- Seq(
- ("1", Seq(), Switch(litO, hookAtt, Seq(), Some(ls.head._3.compile))),
- ("0", Seq(), tree(matrix, ls.tail))
+ immutable.Seq(
+ (
+ "1",
+ immutable.Seq(),
+ Switch(litO, hookAtt, immutable.Seq(), Some(ls.head._3.compile))
+ ),
+ ("0", immutable.Seq(), tree(matrix, ls.tail))
),
None
)
@@ -144,36 +156,36 @@ abstract class EqualLiteral() extends SortCategory {
}
}
case class StringS() extends EqualLiteral {
- def hookAtt = "STRING.String"
- def equalityFun = "hook_KEQUAL_eq"
- def fresh(idx: Int) = idx.toString
+ def hookAtt = "STRING.String"
+ def equalityFun = "hook_KEQUAL_eq"
+ def fresh(idx: Int): String = idx.toString
}
case class BytesS() extends EqualLiteral {
- def hookAtt = "BYTES.Bytes"
- def equalityFun = "hook_KEQUAL_eq"
- def fresh(idx: Int) = idx.toString
+ def hookAtt = "BYTES.Bytes"
+ def equalityFun = "hook_KEQUAL_eq"
+ def fresh(idx: Int): String = idx.toString
}
case class ListS() extends SortCategory {
def hookAtt = "LIST.List"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = true
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = {
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = {
val maxSize = sigma.map(_.asInstanceOf[ListC].length).max
def element(v: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(v))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(v))
val unit: Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, immutable.Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
- SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
+ SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, immutable.Seq(m1, m2))
ListP(
- Seq.fill[Pattern[String]](maxSize + 1)(WildcardP()),
+ immutable.Seq.fill[Pattern[String]](maxSize + 1)(WildcardP()),
None,
- Seq(),
+ immutable.Seq(),
sigma.head.asInstanceOf[ListC].element,
- Seq.fill(maxSize + 1)(element(WildcardP())).fold(unit)(concat)
+ immutable.Seq.fill(maxSize + 1)(element(WildcardP())).fold(unit)(concat)
)
}
override def isExpandDefault = true
@@ -196,7 +208,7 @@ case class ListS() extends SortCategory {
Function(
"hook_LIST_get_long",
Num(i, listO),
- Seq(
+ immutable.Seq(
(listO, hookAtt),
len match {
case None => (Lit(i.toString, "MINT.MInt 64"), "MINT.MInt 64")
@@ -234,7 +246,7 @@ case class ListS() extends SortCategory {
Function(
"hook_LIST_size_long",
newO,
- Seq((listO, hookAtt)),
+ immutable.Seq((listO, hookAtt)),
"MINT.MInt 64",
SwitchLit(
newO,
@@ -257,13 +269,13 @@ case class ListS() extends SortCategory {
case class MapS() extends SortCategory {
def hookAtt = "MAP.Map"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = sigma.isEmpty || sigma.contains(Empty())
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = ???
- override def isExpandDefault = true
- def equalityFun = "hook_MAP_eq"
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = ???
+ override def isExpandDefault = true
+ def equalityFun = "hook_MAP_eq"
// matching a map, so construct a node to decompose the map by one of its elements
def tree(matrix: Matrix): DecisionTree = {
val mapO = matrix.bestCol.fringe.occurrence
@@ -273,7 +285,7 @@ case class MapS() extends SortCategory {
Function(
"hook_MAP_size_long",
newO,
- Seq((mapO, hookAtt)),
+ immutable.Seq((mapO, hookAtt)),
"MINT.MInt 64",
SwitchLit(newO, "MINT.MInt 64", 64, matrix.compiledCases, matrix.compiledDefault)
)
@@ -289,7 +301,7 @@ case class MapS() extends SortCategory {
CheckNull(
Choice(mapO),
"STRING.String",
- Seq(
+ immutable.Seq(
("0", m("0")._1, m("0")._2),
(
"1",
@@ -297,12 +309,12 @@ case class MapS() extends SortCategory {
Function(
"hook_MAP_lookup",
ChoiceValue(mapO),
- Seq((mapO, hookAtt), (Choice(mapO), "STRING.String")),
+ immutable.Seq((mapO, hookAtt), (Choice(mapO), "STRING.String")),
"STRING.String",
Function(
"hook_MAP_remove",
ChoiceRem(mapO),
- Seq((mapO, hookAtt), (Choice(mapO), "STRING.String")),
+ immutable.Seq((mapO, hookAtt), (Choice(mapO), "STRING.String")),
hookAtt,
m("1")._2
)
@@ -327,12 +339,12 @@ case class MapS() extends SortCategory {
Function(
"hook_MAP_lookup_null",
Value(k, mapO),
- Seq((mapO, hookAtt), (newO, "STRING.String")),
+ immutable.Seq((mapO, hookAtt), (newO, "STRING.String")),
"STRING.String",
Function(
"hook_MAP_remove",
Rem(k, mapO),
- Seq((mapO, hookAtt), (newO, "STRING.String")),
+ immutable.Seq((mapO, hookAtt), (newO, "STRING.String")),
"MAP.Map",
CheckNull(
Value(k, mapO),
@@ -350,13 +362,13 @@ case class MapS() extends SortCategory {
case class SetS() extends SortCategory {
def hookAtt = "SET.Set"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = sigma.isEmpty || sigma.contains(Empty())
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = ???
- override def isExpandDefault = true
- def equalityFun = "hook_SET_eq"
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = ???
+ override def isExpandDefault = true
+ def equalityFun = "hook_SET_eq"
// matching a set, so construct a node to decompose the set by one of its elements
def tree(matrix: Matrix): DecisionTree = {
val setO = matrix.bestCol.fringe.occurrence
@@ -366,7 +378,7 @@ case class SetS() extends SortCategory {
Function(
"hook_SET_size_long",
newO,
- Seq((setO, hookAtt)),
+ immutable.Seq((setO, hookAtt)),
"MINT.MInt 64",
SwitchLit(newO, "MINT.MInt 64", 64, matrix.compiledCases, matrix.compiledDefault)
)
@@ -382,7 +394,7 @@ case class SetS() extends SortCategory {
CheckNull(
Choice(setO),
"STRING.String",
- Seq(
+ immutable.Seq(
("0", m("0")._1, m("0")._2),
(
"1",
@@ -390,7 +402,7 @@ case class SetS() extends SortCategory {
Function(
"hook_SET_remove",
ChoiceRem(setO),
- Seq((setO, hookAtt), (Choice(setO), "STRING.String")),
+ immutable.Seq((setO, hookAtt), (Choice(setO), "STRING.String")),
hookAtt,
m("1")._2
)
@@ -413,12 +425,12 @@ case class SetS() extends SortCategory {
Function(
"hook_SET_in",
Value(k, setO),
- Seq((newO, "STRING.String"), (setO, hookAtt)),
+ immutable.Seq((newO, "STRING.String"), (setO, hookAtt)),
"BOOL.Bool",
Function(
"hook_SET_remove",
Rem(k, setO),
- Seq((setO, hookAtt), (newO, "STRING.String")),
+ immutable.Seq((setO, hookAtt), (newO, "STRING.String")),
"SET.Set",
SwitchLit(
Value(k, setO),
@@ -437,22 +449,22 @@ case class SetS() extends SortCategory {
case class RangeMapS() extends SortCategory {
def hookAtt = "RANGEMAP.RangeMap"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = true
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = ???
- def tree(matrix: Matrix): DecisionTree = ???
- def equalityFun = "hook_RANGEMAP_eq"
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = ???
+ def tree(matrix: Matrix): DecisionTree = ???
+ def equalityFun = "hook_RANGEMAP_eq"
}
case class FloatS() extends EqualLiteral {
- def hookAtt = "FLOAT.Float"
- def equalityFun = "hook_FLOAT_trueeq"
- def fresh(idx: Int) = idx.toString + ".0"
+ def hookAtt = "FLOAT.Float"
+ def equalityFun = "hook_FLOAT_trueeq"
+ def fresh(idx: Int): String = idx.toString + ".0"
override def equal(s1: String, s2: String): Boolean =
parseKFloat(s1) == parseKFloat(s2)
- private val precisionAndExponent = Regex.compile("(.*)[pP](\\d+)[xX](\\d+)");
+ private val precisionAndExponent = Regex.compile("(.*)[pP](\\d+)[xX](\\d+)")
def parseKFloat(s: String): (BigFloat, Int) =
try {
val m = precisionAndExponent.matcher(s)
@@ -488,12 +500,12 @@ case class FloatS() extends EqualLiteral {
case class IntS() extends SortCategory {
def hookAtt = "INT.Int"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = true
def equalityFun = "hook_INT_eq"
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = {
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = {
var idx = 0
val strs = sigma.map(_.asInstanceOf[LiteralC].literal).toSet
while (true) {
@@ -519,7 +531,7 @@ case class IntS() extends SortCategory {
Function(
"hook_INT_size_int",
sizeO,
- Seq((litO, hookAtt)),
+ immutable.Seq((litO, hookAtt)),
"MINT.MInt 32",
SwitchLit(
sizeO,
@@ -534,18 +546,18 @@ case class IntS() extends SortCategory {
def sizeCases(
litO: Occurrence,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree]
- ): Seq[(String, Seq[String], DecisionTree)] =
+ ): immutable.Seq[(String, immutable.Seq[String], DecisionTree)] =
cases
.groupBy(t => sizeOf(t._1))
- .toSeq
- .map(t => (t._1.toString, Seq(), limbSwitch(litO, t._1.abs, t._2, default, 0)))
+ .to(immutable.Seq)
+ .map(t => (t._1.toString, immutable.Seq(), limbSwitch(litO, t._1.abs, t._2, default, 0)))
def limbSwitch(
litO: Occurrence,
size: Int,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree],
i: Int
): DecisionTree =
@@ -553,13 +565,13 @@ case class IntS() extends SortCategory {
Failure()
} else if (size == i) {
assert(cases.size == 1)
- cases(0)._3
+ cases.head._3
} else {
val limbO = Num(i, litO)
Function(
"hook_INT_limb",
limbO,
- Seq((litO, hookAtt), (Lit(i.toString, "MINT.MInt 64"), "MINT.MInt 64")),
+ immutable.Seq((litO, hookAtt), (Lit(i.toString, "MINT.MInt 64"), "MINT.MInt 64")),
"MINT.MInt 64",
SwitchLit(limbO, "MINT.MInt 64", 64, limbCases(litO, size, cases, default, i), default)
)
@@ -568,14 +580,14 @@ case class IntS() extends SortCategory {
def limbCases(
litO: Occurrence,
size: Int,
- cases: Seq[(String, Seq[String], DecisionTree)],
+ cases: immutable.Seq[(String, immutable.Seq[String], DecisionTree)],
default: Option[DecisionTree],
i: Int
- ): Seq[(String, Seq[String], DecisionTree)] =
+ ): immutable.Seq[(String, immutable.Seq[String], DecisionTree)] =
cases
.groupBy(t => getLimb(t._1, i))
- .toSeq
- .map(t => (t._1, Seq(), limbSwitch(litO, size, t._2, default, i + 1)))
+ .to(immutable.Seq)
+ .map(t => (t._1, immutable.Seq(), limbSwitch(litO, size, t._2, default, i + 1)))
def sizeOf(str: String): Int = {
val i = BigInt(str)
@@ -596,11 +608,11 @@ case class IntS() extends SortCategory {
case class BoolS() extends SortCategory {
def hookAtt = "BOOL.Bool"
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = sigma.length != 2
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = {
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = {
val strs = sigma.map(_.asInstanceOf[LiteralC].literal).toSet
if (strs("1")) {
LiteralP("false", this)
@@ -620,23 +632,23 @@ case class BoolS() extends SortCategory {
override def length(rawLength: Int) = 2
}
case class VarS() extends EqualLiteral {
- def hookAtt = "KVAR.KVar"
- def equalityFun = "hook_STRING_eq"
- def fresh(idx: Int) = "_" + idx.toString
+ def hookAtt = "KVAR.KVar"
+ def equalityFun = "hook_STRING_eq"
+ def fresh(idx: Int): String = "_" + idx.toString
}
case class BufferS() extends EqualLiteral {
- def hookAtt = "BUFFER.StringBuffer"
- def equalityFun = ???
- def fresh(idx: Int) = idx.toString
+ def hookAtt = "BUFFER.StringBuffer"
+ def equalityFun: String = ???
+ def fresh(idx: Int): String = idx.toString
}
case class MIntS(bitwidth: Int) extends SortCategory {
- def hookAtt = "MINT.MInt " + bitwidth
+ def hookAtt: String = "MINT.MInt " + bitwidth
def hasIncompleteSignature(
- sigma: Seq[Constructor],
+ sigma: immutable.Seq[Constructor],
isExact: Boolean,
sortInfo: SortInfo
): Boolean = sigma.length != (1 << bitwidth)
- def missingConstructor(sigma: Seq[Constructor], f: Fringe): Pattern[String] = {
+ def missingConstructor(sigma: immutable.Seq[Constructor], f: Fringe): Pattern[String] = {
val strs = sigma.map(_.asInstanceOf[LiteralC].literal).toSet
for (i <- 0 until 1 << bitwidth)
if (!strs(i.toString))
@@ -651,6 +663,6 @@ case class MIntS(bitwidth: Int) extends SortCategory {
matrix.compiledCases,
matrix.compiledDefault
)
- def equalityFun = ???
- override def length(rawLength: Int) = 1 << bitwidth
+ def equalityFun: String = ???
+ override def length(rawLength: Int): Int = 1 << bitwidth
}
diff --git a/nix/llvm-backend-matching.nix b/nix/llvm-backend-matching.nix
index fc6ae97db..f6c33410c 100644
--- a/nix/llvm-backend-matching.nix
+++ b/nix/llvm-backend-matching.nix
@@ -8,12 +8,12 @@ let self = maven.buildMavenPackage rec {
buildOffline = true;
manualMvnArtifacts = [
- "org.scala-lang:scala-compiler:2.12.18"
+ "org.scala-lang:scala-compiler:2.13.13"
"org.apache.maven.plugins:maven-compiler-plugin:3.7.0"
];
manualMvnSourceArtifacts = [
- "org.scala-sbt:compiler-bridge_2.12:1.8.0"
+ "org.scala-sbt:compiler-bridge_2.13:1.8.0"
];
passthru = {
diff --git a/nix/overlay.nix b/nix/overlay.nix
index 1f96aedee..0fbd819ae 100644
--- a/nix/overlay.nix
+++ b/nix/overlay.nix
@@ -21,7 +21,7 @@ let
llvm-backend-matching = import ./llvm-backend-matching.nix {
src = prev.llvm-backend-matching-src;
- mvnHash = "sha256-2X8G3T05Pk1apA0f04Mdu/8DAB89oB9XwTBQ3KVoc/A=";
+ mvnHash = "sha256-jO6g5yuae6oU9XCVmDXa678Hzz1zroaMv7/wzgWbUzI=";
inherit (final) maven;
};