From 813557a767e5f3c334b9f869ef822631b1eaf989 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 9 Apr 2024 14:27:07 +0000 Subject: [PATCH 1/9] matching/deps/scala_kore_release: Set Version 0.3.3 --- matching/deps/scala_kore_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From e6ccd98c61b3ab1f3159d9e01d11772eeefc39dd Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 9 Apr 2024 14:27:29 +0000 Subject: [PATCH 2/9] matching: update scala-kore to 0.3.3 --- matching/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matching/pom.xml b/matching/pom.xml index 66ec6d4ab..f9eb3b5f4 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -12,7 +12,7 @@ 17 - 0.3.0 + 0.3.3 2.41.1 2.12 18 From d036cf1dd2a70951c92fad1f4bd43698f07d578a Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 9 Apr 2024 14:27:29 +0000 Subject: [PATCH 3/9] nix: invalidate maven packages hash --- nix/overlay.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/overlay.nix b/nix/overlay.nix index 1f96aedee..47af58e53 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 = ""; inherit (final) maven; }; From 350db8444c4e3977899d4f38d3e2f9782cb31ace Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 9 Apr 2024 15:32:39 +0100 Subject: [PATCH 4/9] Bump maven hash --- nix/overlay.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/overlay.nix b/nix/overlay.nix index 47af58e53..eb51d6b35 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 = ""; + mvnHash = "sha256-ZmxDfQAQ4sq7yZEwCS8I3TNZeENTZlkiHQFObNdeSRE="; inherit (final) maven; }; From 91916ca3421995a366fea1e01b8f3563276d7a18 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Wed, 6 Mar 2024 20:52:30 -0500 Subject: [PATCH 5/9] Use immutable.Seq everywhere --- .../backend/llvm/matching/Constructor.scala | 84 ++--- .../backend/llvm/matching/Generator.scala | 145 ++++---- .../backend/llvm/matching/Heuristics.scala | 14 +- .../backend/llvm/matching/Matching.scala | 23 +- .../backend/llvm/matching/Matrix.scala | 218 ++++++------ .../backend/llvm/matching/Occurrence.scala | 1 - .../backend/llvm/matching/Parser.scala | 117 ++++--- .../llvm/matching/dt/DecisionTree.scala | 59 ++-- .../llvm/matching/pattern/Pattern.scala | 310 ++++++++++-------- .../llvm/matching/pattern/SortCategory.scala | 140 ++++---- 10 files changed, 618 insertions(+), 493 deletions(-) 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..8697fa7be 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,23 +2,25 @@ 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 SetS() => SetP(immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq())) + case MapS() => + MapP(immutable.Seq(), immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq())) case _ => ??? } } @@ -26,10 +28,10 @@ case class Empty() extends Constructor { } 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(0) override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) } @@ -37,20 +39,20 @@ 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( + immutable.Seq( new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false), new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false) ) ) } else { Some( - Seq( + immutable.Seq( new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false), new Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), false), new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false) @@ -59,10 +61,10 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op } case Some(k) => if (isSet) { - Some(Seq(new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), f)) + Some(immutable.Seq(new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), f)) } else { Some( - Seq( + immutable.Seq( new Fringe(f.symlib, sorts(1), Value(k, f.occurrence), false), new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), f @@ -71,7 +73,7 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op } } } - 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 @@ -92,11 +94,11 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op } } 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] = { + def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq(f)) + def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = { val child = children(0) 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))) } - 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,7 +204,7 @@ 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 { @@ -213,7 +215,7 @@ case class SymbolC(sym: SymbolOrAlias) extends Constructor { ) ) } - 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..0ffb487c3 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,91 @@ 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))) } 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))) } 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))) } 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 +122,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 +154,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 +162,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,14 +178,14 @@ 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]( 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(_)) @@ -187,7 +197,7 @@ object Generator { 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 +209,18 @@ 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, + if (axioms.isEmpty) sorts.map(_ => immutable.IndexedSeq()) else patterns + ).zipped.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 = { @@ -244,10 +257,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, specialized.fringe.map(_.occurrence)).zipped.to[immutable.Seq] if (Matching.logging) { System.out.println("Residuals: " + residualMap.toList) } 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..88b3234cd 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,11 +73,14 @@ 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 for (col <- cols) { @@ -410,18 +414,18 @@ sealed trait PseudoHeuristic extends Heuristic { @NamedHeuristic(name = 'N') object NPseudoHeuristic extends PseudoHeuristic { - override def breakTies(cols: Seq[MatrixColumn]): MatrixColumn = + override def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn = cols(0) } @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..172c60bd5 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 @@ -7,6 +7,10 @@ import java.io.FileWriter import java.util.Optional import org.kframework.backend.llvm.matching.dt._ +import java.io.{File, FileWriter} +import java.util.Optional +import scala.collection.immutable + object Matching { def writeDecisionTreeToFile( filename: File, @@ -27,9 +31,15 @@ object Matching { 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,7 +52,12 @@ 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)) @@ -59,7 +74,7 @@ object Matching { Generator.mkDecisionTree( symlib, defn, - funcAxioms.getOrElse(f, IndexedSeq()), + funcAxioms.getOrElse(f, immutable.IndexedSeq()), symlib.signatures(f)._1, f, kem 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..8f3832ffb 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 @@ -11,6 +11,11 @@ import java.util.Optional import org.kframework.backend.llvm.matching.dt._ import org.kframework.backend.llvm.matching.pattern._ +import java.util +import java.util.Optional +import java.util.concurrent.ConcurrentHashMap +import scala.collection.immutable + trait AbstractColumn { def column: Column @@ -37,14 +42,14 @@ 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) + 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 +62,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,10 +76,10 @@ 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 @@ -89,19 +94,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 = { + private lazy val boundVars: immutable.Seq[Set[String]] = patterns.map(_.variables) + def needed(vars: immutable.Seq[Set[String]]): Boolean = { val intersection = (vars, boundVars).zipped.map(_.intersect(_)) intersection.exists(_.nonEmpty) } lazy val isEmpty = 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] = { @@ -142,11 +147,11 @@ class Column( def isChoiceForKey(key: Option[Pattern[Option[Occurrence]]]) = fringe.sortInfo.isCollection && key == None - private def asListP(p: Pattern[String]): Seq[ListP[String]] = + 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) = { @@ -160,10 +165,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 @@ -194,12 +199,12 @@ class Column( 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 + val transposed = if (ps.isEmpty) fringes.map(_ => immutable.IndexedSeq()) else ps.transpose (fringes, transposed).zipped.toIndexedSeq.map(t => new Column(t._1, t._2.toIndexedSeq, clauses)) } @@ -216,7 +221,7 @@ class Column( } override lazy val hashCode: Int = { - val state = Seq(patterns) + val state = immutable.Seq(patterns) state.map(_.hashCode()).foldLeft(0)((a, b) => 31 * a + b) } } @@ -238,10 +243,10 @@ case class Fringe( ) { val 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,18 +256,18 @@ 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 = @@ -273,11 +278,11 @@ case class Fringe( } class SortInfo private (sort: Sort, symlib: Parser.SymLib) { - val constructors = symlib.constructorsForSort.getOrElse(sort, Seq()) + val constructors = 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)) + .hasIncompleteSignature(immutable.Seq(), true, SortInfo(c.params(0), symlib)) ) .toSet val exactConstructors = constructors.filter(_.ctr != "inj") @@ -291,7 +296,7 @@ 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)) ) ) ) @@ -313,10 +318,10 @@ 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 lhsVars: immutable.Seq[Variable], + val rhsVars: immutable.Seq[String], + val scVars: Option[immutable.Seq[String]], + val freshConstants: immutable.Seq[(String, Sort)], val arity: Int, val priority: Int, source: Optional[Source], @@ -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,11 +425,11 @@ 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(val patterns: immutable.IndexedSeq[Pattern[String]], val 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)) } @@ -433,10 +438,10 @@ case class Row(val patterns: IndexedSeq[Pattern[String]], val clause: Clause) { 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, 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, false) .trueDefault(colIx, sigma, Some(matrixColumns)) .rows .headOption @@ -463,58 +468,58 @@ 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 => new 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))) } 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, @@ -537,17 +542,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 +580,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 +598,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:") @@ -627,8 +633,8 @@ class Matrix private ( 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 +652,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) @@ -668,7 +674,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 +699,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,9 +716,9 @@ 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, row.patterns).zipped + .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) @@ -775,25 +781,24 @@ 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 ) ) } // fill out the bindings for list range variables - val withRanges = row.clause.listRanges.foldRight(sc) { - case ((o @ Num(_, o2), hd, tl), dt) => - Function( - "hook_LIST_range_long", - o, - Seq( - (o2, "LIST.List"), - (Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"), - (Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64") - ), - "LIST.List", - dt - ) + val withRanges = row.clause.listRanges.foldRight(sc) { case ((o @ Num(_, o2), hd, tl), dt) => + Function( + "hook_LIST_range_long", + o, + immutable.Seq( + (o2, "LIST.List"), + (Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"), + (Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64") + ), + "LIST.List", + dt + ) case _ => ??? } val withOverloads = row.clause.overloadChildren.foldRight(withRanges) { @@ -803,7 +808,7 @@ 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 @@ -827,7 +832,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 ) @@ -941,7 +947,11 @@ 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) { @@ -974,12 +984,12 @@ class Matrix private ( 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 @@ -1100,11 +1110,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 = @@ -1140,7 +1152,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 = @@ -1188,7 +1200,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,16 +1210,16 @@ 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) 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..95c3ac932 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 { 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..2214d6f26 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,8 @@ 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 +49,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,7 +69,11 @@ object Parser { .map(_.asInstanceOf[SortDeclaration]) .groupBy(_.sort.asInstanceOf[CompoundSort].ctr) - private def instantiate(s: Sort, params: Seq[Sort], args: Seq[Sort]): Sort = { + private def instantiate( + s: Sort, + params: immutable.Seq[Sort], + args: immutable.Seq[Sort] + ): Sort = { val map = (params, args).zipped.toMap s match { case v @ SortVariable(_) => map(v) @@ -78,13 +84,17 @@ object Parser { def isHooked(symbol: SymbolOrAlias): Boolean = return 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(0), B.Attributes(immutable.Seq()))) } else { ( symbol, @@ -105,10 +115,10 @@ 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) + .mapValues(_.keys.filter(k => !hasAtt(signatures(k)._3, "function")).to[immutable.Seq]) private val sortAttData: Map[String, Attributes] = sorts @@ -124,20 +134,20 @@ 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).mapValues(_.map(_._2).to[immutable.Seq]) 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 @@ -180,7 +190,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 +200,9 @@ object Parser { "non-executable" ) || (hasAtt(s, "simplification") && !simplification) ) { - Seq() + immutable.Seq() } else { - Seq( + immutable.Seq( ( splitted.get._1, AxiomInfo( @@ -209,7 +219,7 @@ object Parser { ) } } else { - Seq() + immutable.Seq() } } @@ -219,21 +229,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 +261,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 +271,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 +282,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 +294,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 +303,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 +365,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,21 +379,24 @@ 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] = { + def parseTopAxioms( + axioms: immutable.Seq[AxiomDeclaration], + search: Boolean + ): immutable.IndexedSeq[AxiomInfo] = { val withOwise = axioms.zipWithIndex.flatMap(parseAxiomSentence(splitTop, _, false, 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) ) @@ -392,11 +412,12 @@ object Parser { 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 +430,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")) @@ -453,7 +476,7 @@ object Parser { def parseHeuristic(heuristic: Char): Heuristic = heuristicMap(heuristic) - def parseHeuristics(heuristics: String): Seq[Heuristic] = + def parseHeuristics(heuristics: String): immutable.Seq[Heuristic] = heuristics.toList.map(parseHeuristic(_)) def parseSymbols(defn: Definition, heuristics: String): SymLib = { 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..96c593f88 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,6 +9,7 @@ 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 = { @@ -20,7 +21,7 @@ sealed trait DecisionTree { 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() @@ -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( 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..c48c19ef1 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]] @@ -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(new VariableBinding(name, sort, occurrence, residual)) ++ pat.bindings( ix, residual, occurrence, @@ -112,22 +114,26 @@ 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]] = @@ -142,13 +148,13 @@ case class AsP[T](name: T, sort: SortCategory, pat: Pattern[T]) extends Pattern[ } 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,10 +231,13 @@ 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()) @@ -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,16 +304,16 @@ 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 variables: Set[T] = Set() @@ -319,27 +328,27 @@ 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)) ) ) } else { keys.flatMap(key => - Seq( + immutable.Seq( HasKey(isSet = false, ctr, clause.canonicalize(key)), HasNoKey(false, clause.canonicalize(key)) ) @@ -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,7 +452,7 @@ case class MapP[T] private ( } } - override def mapOrSetKeys: Seq[Pattern[T]] = keys + override def mapOrSetKeys: immutable.Seq[Pattern[T]] = keys def category = Some(MapS()) lazy val variables: Set[T] = keys.flatMap(_.variables).toSet ++ values @@ -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) { @@ -544,33 +553,33 @@ 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)) ) ) } else { elements.flatMap(elem => - Seq( + immutable.Seq( HasKey(isSet = true, ctr, clause.canonicalize(elem)), HasNoKey(true, clause.canonicalize(elem)) ) @@ -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,7 +666,7 @@ case class SetP[T] private ( } } - override def mapOrSetKeys: Seq[Pattern[T]] = elements + override def mapOrSetKeys: immutable.Seq[Pattern[T]] = elements def category = Some(SetS()) lazy val variables: Set[T] = @@ -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, @@ -728,36 +740,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,14 +783,16 @@ 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) => @@ -780,20 +800,20 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: Seq[Pattern[T]]) extends Pattern[T 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 +824,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 +832,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, @@ -840,18 +860,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 +879,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 +901,14 @@ 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, fringeTs, ps).zipped + .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() } } @@ -904,9 +928,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 +954,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(new 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 +987,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 +1014,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..6681ea796 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 @@ -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 ) @@ -156,24 +168,24 @@ case class BytesS() extends EqualLiteral { 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,13 +449,13 @@ 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" @@ -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 = @@ -559,7 +571,7 @@ case class IntS() extends SortCategory { 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) @@ -632,11 +644,11 @@ case class BufferS() extends EqualLiteral { case class MIntS(bitwidth: Int) extends SortCategory { def hookAtt = "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)) From 839e2b3b83ffa3e644290a5cc5e16f296ff658bb Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 9 Apr 2024 17:33:08 -0400 Subject: [PATCH 6/9] Fix various warnings. Update to Scala 2.13.13 --- matching/pom.xml | 9 +- .../backend/llvm/matching/Constructor.scala | 32 +-- .../backend/llvm/matching/Generator.scala | 26 ++- .../backend/llvm/matching/Heuristics.scala | 6 +- .../backend/llvm/matching/Matching.scala | 28 ++- .../backend/llvm/matching/Matrix.scala | 209 +++++++++--------- .../backend/llvm/matching/Occurrence.scala | 18 +- .../backend/llvm/matching/Parser.scala | 28 ++- .../llvm/matching/dt/DecisionTree.scala | 8 +- .../llvm/matching/pattern/Pattern.scala | 57 ++--- .../llvm/matching/pattern/SortCategory.scala | 46 ++-- 11 files changed, 246 insertions(+), 221 deletions(-) diff --git a/matching/pom.xml b/matching/pom.xml index 66ec6d4ab..a751d62f1 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -14,8 +14,8 @@ 17 0.3.0 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 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 8697fa7be..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 @@ -21,7 +21,7 @@ case class Empty() extends Constructor { case SetS() => SetP(immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq())) case MapS() => MapP(immutable.Seq(), immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq())) - case _ => ??? + case _ => ??? } } override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) @@ -31,7 +31,7 @@ case class NonEmpty() extends Constructor { def name: String = ??? def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq(f)) - def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = children(0) + def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = children.head override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) } @@ -46,27 +46,27 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op if (isSet) { Some( immutable.Seq( - new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false), - new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false) + Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false), + Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false) ) ) } else { Some( immutable.Seq( - new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false), - new Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), false), - new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false) + Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false), + Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), isExact = false), + Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false) ) ) } case Some(k) => if (isSet) { - Some(immutable.Seq(new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), f)) + Some(immutable.Seq(Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false), f)) } else { Some( immutable.Seq( - new Fringe(f.symlib, sorts(1), Value(k, f.occurrence), false), - new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), + Fringe(f.symlib, sorts(1), Value(k, f.occurrence), isExact = false), + Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false), f ) ) @@ -80,9 +80,9 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op assert((isSet && children.size == 2) || (!isSet && children.size == 3)) if (this.key.isEmpty) { if (isSet) { - key = children(0) + key = children.head } else { - key = children(0) + key = children.head value = children(1) } } else { @@ -90,7 +90,7 @@ 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] = @@ -132,7 +132,7 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex def isBest(pat: Pattern[Option[Occurrence]]): Boolean = key.isDefined && pat == key.get def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq(f)) def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = { - val child = children(0) + val child = children.head def element(k: Pattern[String], v: Pattern[String]): Pattern[String] = SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k, v)) def setElement(k: Pattern[String]): Pattern[String] = @@ -181,7 +181,7 @@ case class ListC(element: SymbolOrAlias, length: Int) extends Constructor { def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true def expand(f: Fringe): Option[immutable.Seq[Fringe]] = { val sort = f.symlib.signatures(element)._1.head - Some((0 until length).map(i => new Fringe(f.symlib, sort, Num(i, f.occurrence), false))) + Some((0 until length).map(i => Fringe(f.symlib, sort, Num(i, f.occurrence), isExact = false))) } def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = { def element(v: Pattern[String]): Pattern[String] = @@ -211,7 +211,7 @@ case class SymbolC(sym: SymbolOrAlias) extends Constructor { val sorts = f.symlib.signatures(sym)._1 Some( sorts.zipWithIndex.map(t => - new Fringe(f.symlib, t._1, Num(t._2, f.occurrence), sym.ctr == "inj") + Fringe(f.symlib, t._1, Num(t._2, f.occurrence), sym.ctr == "inj") ) ) } 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 0ffb487c3..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 @@ -48,6 +48,7 @@ object Generator { ListP(immutable.Seq(), None, immutable.Seq(), c, SymbolP(sym, immutable.Seq())) case (Element(), immutable.Seq(p)) => ListP(immutable.Seq(p), None, immutable.Seq(), c, SymbolP(sym, immutable.Seq(p))) + case _ => ??? } private def mapPattern( @@ -76,6 +77,7 @@ object Generator { MapP(immutable.Seq(), immutable.Seq(), None, c, SymbolP(sym, immutable.Seq())) case (Element(), immutable.Seq(k, v)) => MapP(immutable.Seq(k), immutable.Seq(v), None, c, SymbolP(sym, immutable.Seq(k, v))) + case _ => ??? } private def setPattern( @@ -104,6 +106,7 @@ object Generator { SetP(immutable.Seq(), None, c, SymbolP(sym, immutable.Seq())) case (Element(), immutable.Seq(e)) => SetP(immutable.Seq(e), None, c, SymbolP(sym, immutable.Seq(e))) + case _ => ??? } private def genPatterns( @@ -181,18 +184,18 @@ object Generator { case _ => immutable.Seq() } - def genClauseMatrix[T]( + def genClauseMatrix( symlib: Parser.SymLib, mod: Definition, axioms: immutable.IndexedSeq[AxiomInfo], sorts: immutable.Seq[Sort] ): Matrix = { val actions = axioms.map { a => - val lhsVars = a.rewrite.getLeftHandSide.flatMap(genVars(_)) + val lhsVars = a.rewrite.getLeftHandSide.flatMap(genVars) val lhsVarNames = lhsVars.map(_.name) val rhsVars = genVars(a.rewrite.getRightHandSide) - val scVars = a.sideCondition.map(genVars(_)) - new Action( + val scVars = a.sideCondition.map(genVars) + Action( a.ordinal, lhsVars, rhsVars.map(_.name).sorted.distinct, @@ -209,10 +212,11 @@ object Generator { } val patterns = axioms.map(a => genPatterns(mod, symlib, a.rewrite.getLeftHandSide)).transpose val cols = - ( - sorts, - if (axioms.isEmpty) sorts.map(_ => immutable.IndexedSeq()) else patterns - ).zipped.toIndexedSeq + sorts + .lazyZip( + if (axioms.isEmpty) sorts.map(_ => immutable.IndexedSeq()) else patterns + ) + .toIndexedSeq new Matrix(symlib, cols, actions).expand } @@ -246,7 +250,7 @@ object Generator { val numerator = originalMatrix.rows.size * threshold._1 val denominator = finalMatrix.rows.size * threshold._2 if (Matching.logging) { - System.out.println(finalMatrix.rows.size + "/" + originalMatrix.rows.size) + System.out.println(finalMatrix.rows.size.toString + "/" + originalMatrix.rows.size.toString) } numerator <= denominator } @@ -260,7 +264,7 @@ object Generator { ): Option[(DecisionTree, immutable.Seq[(P[String], Occurrence)])] = { val rhs = genPatterns(mod, symlib, immutable.Seq(axiom.rewrite.getRightHandSide)) val (specialized, residuals) = matrix.specializeBy(rhs.toIndexedSeq) - val residualMap = (residuals, specialized.fringe.map(_.occurrence)).zipped.to[immutable.Seq] + val residualMap = residuals.lazyZip(specialized.fringe.map(_.occurrence)).to(immutable.Seq) if (Matching.logging) { System.out.println("Residuals: " + residualMap.toList) } @@ -269,7 +273,7 @@ object Generator { symlib, specialized.columns.map(c => new Column(c.fringe.inexact, c.patterns, newClauses)), newClauses, - false + search = false ) if (isPoorlySpecialized(finalMatrix, matrix, threshold)) { None 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 88b3234cd..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 @@ -82,7 +82,7 @@ object Heuristic { allCols: immutable.Seq[MatrixColumn] ): immutable.Seq[MatrixColumn] = { var result: List[MatrixColumn] = Nil - var best = cols(0).score + var best = cols.head.score for (col <- cols) { import Ordering.Implicits._ val bestInvalid = allCols @@ -311,7 +311,7 @@ object RHeuristic extends Heuristic { .patterns(i) .isSpecialized( con, - false, + isExact = false, c.column.fringe, c.column.clauses(i), c.column.maxPriorityForKey(key) @@ -415,7 +415,7 @@ sealed trait PseudoHeuristic extends Heuristic { @NamedHeuristic(name = 'N') object NPseudoHeuristic extends PseudoHeuristic { override def breakTies(cols: immutable.Seq[MatrixColumn]): MatrixColumn = - cols(0) + cols.head } @NamedHeuristic(name = 'L') 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 172c60bd5..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,10 +6,8 @@ import java.io.File import java.io.FileWriter import java.util.Optional import org.kframework.backend.llvm.matching.dt._ - -import java.io.{File, FileWriter} -import java.util.Optional import scala.collection.immutable +import scala.collection.parallel.CollectionConverters._ object Matching { def writeDecisionTreeToFile( @@ -21,12 +19,12 @@ object Matching { warn: Boolean, genSearch: Boolean, kem: MatchingException => Unit - ) { + ): Unit = { val defn = new TextToKore().parse(filename) outputFolder.mkdirs() val allAxioms = Parser.getAxioms(defn) - val axioms = Parser.parseTopAxioms(allAxioms, false) - val searchAxioms = Parser.parseTopAxioms(allAxioms, true) + val axioms = Parser.parseTopAxioms(allAxioms, search = false) + val searchAxioms = Parser.parseTopAxioms(allAxioms, search = true) val symlib = Parser.parseSymbols(defn, heuristic) val (dt, dtSearch, matrix) = if (axioms.isEmpty) { (Failure(), Failure(), null) @@ -63,7 +61,7 @@ object Matching { dt.serializeToYaml(new File(outputFolder, filename)) } } - val funcAxioms = Parser.parseFunctionAxioms(allAxioms, false) + val funcAxioms = Parser.parseFunctionAxioms(allAxioms, simplification = false) val dts = symlib.functions.map { f => if (logging) { System.out.println("Compiling " + f) @@ -90,7 +88,7 @@ object Matching { if (logging) { System.out.println("Compiling decision tree for axiom " + a.ordinal) } - Matrix.clearCache + Matrix.clearCache() val dt = Generator.mkSpecialDecisionTree(symlib, defn, matrix, a, threshold.get) val ordinal = a.ordinal val filename = "dt_" + ordinal + ".yaml" @@ -99,7 +97,7 @@ object Matching { } } } - val files = (symlib.functions, dts).zipped.toIterable + val files = symlib.functions.lazyZip(dts).toSeq val index = new File(outputFolder, "index.txt") val writer = new FileWriter(index) var idx = 0 @@ -110,7 +108,7 @@ object Matching { writer.write(pair._1.ctr + "\t" + filename + "\n") idx += 1 } - writer.close + writer.close() } var logging = false @@ -133,16 +131,16 @@ object Matching { def main(args: Array[String]): Unit = { val file = new File(args(0)) val outputFolder = new File(args(2)) - logging = args.size > 4 + logging = args.length > 4 writeDecisionTreeToFile( file, args(1), outputFolder, getThreshold(args(3)), - true, - true, - true, - e => () + genSingleRuleTrees = true, + warn = true, + genSearch = true, + _ => () ) } } 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 8f3832ffb..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,10 +10,7 @@ import java.util.concurrent.ConcurrentHashMap import java.util.Optional import org.kframework.backend.llvm.matching.dt._ import org.kframework.backend.llvm.matching.pattern._ - -import java.util -import java.util.Optional -import java.util.concurrent.ConcurrentHashMap +import scala.annotation.tailrec import scala.collection.immutable trait AbstractColumn { @@ -41,7 +38,7 @@ trait AbstractColumn { } } -case class MatrixColumn(val matrix: Matrix, colIx: Int) extends AbstractColumn { +case class MatrixColumn(matrix: Matrix, colIx: Int) extends AbstractColumn { def column: Column = matrix.columns(colIx) lazy val score: immutable.Seq[Double] = column.score(this) } @@ -82,11 +79,11 @@ class Column( 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) @@ -100,11 +97,11 @@ class Column( } private lazy val boundVars: immutable.Seq[Set[String]] = patterns.map(_.variables) def needed(vars: immutable.Seq[Set[String]]): Boolean = { - val intersection = (vars, boundVars).zipped.map(_.intersect(_)) + 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: immutable.Seq[Constructor] = patterns.zipWithIndex.flatMap(p => p._1.signature(clauses(p._2))) @@ -144,9 +141,10 @@ 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 + @tailrec private def asListP(p: Pattern[String]): immutable.Seq[ListP[String]] = p match { case l @ ListP(_, _, _, _, _) => immutable.Seq(l) @@ -155,7 +153,7 @@ class Column( } def maxListSize: (Int, Int) = { - val listPs = patterns.flatMap(asListP(_)) + val listPs = patterns.flatMap(asListP) if (listPs.isEmpty) { (0, 0) } else { @@ -192,7 +190,7 @@ 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 { @@ -201,11 +199,12 @@ class 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 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, transposed).zipped.toIndexedSeq.map(t => new Column(t._1, t._2.toIndexedSeq, clauses)) + fringes.lazyZip(transposed).toIndexedSeq.map(t => new Column(t._1, t._2.toIndexedSeq, clauses)) } lazy val isWildcard: Boolean = patterns.forall(_.isWildcard) @@ -214,7 +213,7 @@ 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 @@ -227,21 +226,21 @@ class Column( } 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): immutable.Seq[SymbolOrAlias] = symlib.overloads.getOrElse(sym, immutable.Seq()) @@ -271,22 +270,23 @@ case class 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, immutable.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(immutable.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 @@ -300,7 +300,7 @@ class SortInfo private (sort: Sort, symlib: Parser.SymLib) { ) ) ) - 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) @@ -317,13 +317,13 @@ object SortInfo { } case class Action( - val ordinal: Int, - val lhsVars: immutable.Seq[Variable], - val rhsVars: immutable.Seq[String], - val scVars: Option[immutable.Seq[String]], - val freshConstants: immutable.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 @@ -333,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]) @@ -370,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), @@ -425,13 +425,13 @@ case class Clause( override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) } -case class Row(val patterns: immutable.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): 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( @@ -441,7 +441,7 @@ case class Row(val patterns: immutable.IndexedSeq[Pattern[String]], val clause: fringe: immutable.IndexedSeq[Fringe] ): Option[Row] = Matrix - .fromRows(symlib, immutable.IndexedSeq(this), fringe, false) + .fromRows(symlib, immutable.IndexedSeq(this), fringe, search = false) .specialize(ix, colIx, None) ._3 .rows @@ -455,7 +455,7 @@ case class Row(val patterns: immutable.IndexedSeq[Pattern[String]], val clause: matrixColumns: immutable.IndexedSeq[Column] ): Option[Row] = Matrix - .fromRows(symlib, immutable.IndexedSeq(this), fringe, false) + .fromRows(symlib, immutable.IndexedSeq(this), fringe, search = false) .trueDefault(colIx, sigma, Some(matrixColumns)) .rows .headOption @@ -506,14 +506,14 @@ class Matrix private ( if (rawRows != null) { rawRows } else if (rawColumns.isEmpty) { - rawClauses.map(clause => new Row(immutable.IndexedSeq(), clause)) + rawClauses.map(clause => Row(immutable.IndexedSeq(), clause)) } else { computeRows } 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( @@ -523,18 +523,20 @@ class Matrix private ( ) = 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 ) @@ -626,7 +628,7 @@ 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) } @@ -661,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 ) @@ -716,8 +718,9 @@ class Matrix private ( symlib ) // first, add all remaining variable bindings to the clause - val vars = row.clause.bindings ++ (fringe, row.patterns).zipped - .to[immutable.Seq] + 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 => @@ -725,10 +728,11 @@ class Matrix private ( ) 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 = { @@ -756,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) @@ -787,18 +791,19 @@ class Matrix private ( ) } // fill out the bindings for list range variables - val withRanges = row.clause.listRanges.foldRight(sc) { case ((o @ Num(_, o2), hd, tl), dt) => - Function( - "hook_LIST_range_long", - o, - immutable.Seq( - (o2, "LIST.List"), - (Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"), - (Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64") - ), - "LIST.List", - dt - ) + val withRanges = row.clause.listRanges.foldRight(sc) { + case ((o @ Num(_, o2), hd, tl), dt) => + Function( + "hook_LIST_range_long", + o, + immutable.Seq( + (o2, "LIST.List"), + (Lit(hd.toString, "MINT.MInt 64"), "MINT.MInt 64"), + (Lit(tl.toString, "MINT.MInt 64"), "MINT.MInt 64") + ), + "LIST.List", + dt + ) case _ => ??? } val withOverloads = row.clause.overloadChildren.foldRight(withRanges) { @@ -811,7 +816,7 @@ class Matrix private ( immutable.Seq( VariableP( Some(v.occurrence.asInstanceOf[Inj].rest), - f.expand(SymbolC(inj))(0).sortInfo.category + f.expand(SymbolC(inj)).head.sortInfo.category ) ) ), @@ -850,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) @@ -882,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, @@ -937,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)) { @@ -955,7 +962,7 @@ class Matrix private ( 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)) { @@ -979,7 +986,7 @@ 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 } @@ -1034,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) @@ -1140,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)) @@ -1191,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 && @@ -1226,8 +1233,8 @@ object Matrix { 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 95c3ac932..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 @@ -17,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 { @@ -54,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 2214d6f26..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 @@ -6,7 +6,6 @@ import java.util import java.util.Optional import scala.collection.immutable - case class AxiomInfo( priority: Int, ordinal: Int, @@ -74,7 +73,7 @@ object Parser { params: immutable.Seq[Sort], args: immutable.Seq[Sort] ): Sort = { - val map = (params, args).zipped.toMap + val map = params.lazyZip(args).toMap s match { case v @ SortVariable(_) => map(v) case _ => s @@ -82,7 +81,7 @@ object Parser { } def isHooked(symbol: SymbolOrAlias): Boolean = - return symbolDecls(symbol.ctr).head.isInstanceOf[HookSymbolDeclaration] + symbolDecls(symbol.ctr).head.isInstanceOf[HookSymbolDeclaration] private def instantiate( s: immutable.Seq[Sort], @@ -94,7 +93,7 @@ object Parser { val signatures: Map[SymbolOrAlias, (immutable.Seq[Sort], Sort, Attributes)] = symbols.map { symbol => if (symbol.ctr == "\\dv") { - (symbol, (immutable.Seq(), symbol.params(0), B.Attributes(immutable.Seq()))) + (symbol, (immutable.Seq(), symbol.params.head, B.Attributes(immutable.Seq()))) } else { ( symbol, @@ -118,7 +117,9 @@ object Parser { val constructorsForSort: Map[Sort, immutable.Seq[SymbolOrAlias]] = signatures .groupBy(_._2._2) - .mapValues(_.keys.filter(k => !hasAtt(signatures(k)._3, "function")).to[immutable.Seq]) + .view + .mapValues(_.keys.filter(k => !hasAtt(signatures(k)._3, "function")).to(immutable.Seq)) + .toMap private val sortAttData: Map[String, Attributes] = sorts @@ -141,16 +142,16 @@ object Parser { .exists(isAtt("function", _)) ) .keys - .to[immutable.Seq] + .to(immutable.Seq) val overloads: Map[SymbolOrAlias, immutable.Seq[SymbolOrAlias]] = - overloadSeq.groupBy(_._1).mapValues(_.map(_._2).to[immutable.Seq]) + overloadSeq.groupBy(_._1).view.mapValues(_.map(_._2).to(immutable.Seq)).toMap def isSubsorted(less: Sort, greater: Sort): Boolean = 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 = @@ -389,7 +390,9 @@ object Parser { axioms: immutable.Seq[AxiomDeclaration], search: Boolean ): immutable.IndexedSeq[AxiomInfo] = { - val withOwise = axioms.zipWithIndex.flatMap(parseAxiomSentence(splitTop, _, false, search)) + val withOwise = axioms.zipWithIndex.flatMap( + parseAxiomSentence(splitTop, _, simplification = false, search = search) + ) withOwise.map(_._2).sortWith(_.priority < _.priority).toIndexedSeq } @@ -398,7 +401,7 @@ object Parser { simplification: Boolean ): 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) @@ -406,7 +409,9 @@ 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 = @@ -447,6 +452,7 @@ object Parser { (args.head, args(1)) match { case (Application(g, _), Application(l, _)) => (g, l) } + case _ => ??? }) } @@ -477,7 +483,7 @@ object Parser { heuristicMap(heuristic) def parseHeuristics(heuristics: String): immutable.Seq[Heuristic] = - heuristics.toList.map(parseHeuristic(_)) + 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 96c593f88..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 @@ -16,7 +16,7 @@ sealed trait DecisionTree { val writer = new OutputStreamWriter( new FileOutputStream(file), Charset.forName("UTF-8").newEncoder() - ); + ) new Yaml().dump(representation, writer) writer.close() } @@ -25,7 +25,7 @@ sealed trait DecisionTree { 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]() @@ -395,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] = { @@ -419,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 c48c19ef1..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 @@ -70,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 @@ -105,7 +105,7 @@ case class AsP[T](name: T, sort: SortCategory, pat: Pattern[T]) extends Pattern[ occurrence: Occurrence, symlib: Parser.SymLib ): immutable.Seq[VariableBinding[T]] = - immutable.Seq(new VariableBinding(name, sort, occurrence, residual)) ++ pat.bindings( + immutable.Seq(VariableBinding(name, sort, occurrence, residual)) ++ pat.bindings( ix, residual, occurrence, @@ -138,11 +138,11 @@ case class AsP[T](name: T, sort: SortCategory, pat: Pattern[T]) extends Pattern[ 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)) } @@ -240,7 +240,7 @@ case class ListP[T] private ( 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()) @@ -315,7 +315,7 @@ case class LiteralP[T](literal: String, sort: SortCategory) extends Pattern[T] { ): 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) @@ -343,14 +343,14 @@ case class MapP[T] private ( keys.flatMap(key => immutable.Seq( HasKey(isSet = false, ctr, clause.canonicalize(key)), - HasNoKey(false, clause.canonicalize(key)) + HasNoKey(isSet = false, clause.canonicalize(key)) ) ) } else { keys.flatMap(key => immutable.Seq( HasKey(isSet = false, ctr, clause.canonicalize(key)), - HasNoKey(false, clause.canonicalize(key)) + HasNoKey(isSet = false, clause.canonicalize(key)) ) ) ++ frame.get.signature(clause) } @@ -454,7 +454,7 @@ case class MapP[T] private ( 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()) @@ -540,11 +540,11 @@ case class OrP[T](ps: immutable.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)) } @@ -574,14 +574,14 @@ case class SetP[T] private ( elements.flatMap(elem => immutable.Seq( HasKey(isSet = true, ctr, clause.canonicalize(elem)), - HasNoKey(true, clause.canonicalize(elem)) + HasNoKey(isSet = true, clause.canonicalize(elem)) ) ) } else { elements.flatMap(elem => immutable.Seq( HasKey(isSet = true, ctr, clause.canonicalize(elem)), - HasNoKey(true, clause.canonicalize(elem)) + HasNoKey(isSet = true, clause.canonicalize(elem)) ) ) ++ frame.get.signature(clause) } @@ -668,7 +668,7 @@ case class SetP[T] private ( 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( @@ -727,6 +727,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: immutable.Seq[Pattern[T]]) extends 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, @@ -795,7 +796,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: immutable.Seq[Pattern[T]]) extends 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 { @@ -842,7 +843,9 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: immutable.Seq[Pattern[T]]) extends 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 { @@ -903,8 +906,10 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: immutable.Seq[Pattern[T]]) extends child match { case None => immutable.Seq() // no overloads exist case Some(fringeTs) => - (fringePs, fringeTs, ps).zipped - .to[immutable.Seq] + 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 } @@ -918,7 +923,7 @@ case class SymbolP[T](sym: SymbolOrAlias, ps: immutable.Seq[Pattern[T]]) extends 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) @@ -955,7 +960,7 @@ case class VariableP[T](name: T, sort: SortCategory) extends Pattern[T] { occurrence: Occurrence, symlib: Parser.SymLib ): immutable.Seq[VariableBinding[T]] = - immutable.Seq(new VariableBinding(name, sort, occurrence, residual)) + immutable.Seq(VariableBinding(name, sort, occurrence, residual)) def expand( ix: Constructor, isExact: Boolean, 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 6681ea796..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 @@ -48,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, @@ -156,14 +156,14 @@ 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" @@ -458,13 +458,13 @@ case class RangeMapS() extends SortCategory { 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) @@ -551,7 +551,7 @@ case class IntS() extends SortCategory { ): immutable.Seq[(String, immutable.Seq[String], DecisionTree)] = cases .groupBy(t => sizeOf(t._1)) - .to[immutable.Seq] + .to(immutable.Seq) .map(t => (t._1.toString, immutable.Seq(), limbSwitch(litO, t._1.abs, t._2, default, 0))) def limbSwitch( @@ -565,7 +565,7 @@ 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( @@ -586,7 +586,7 @@ case class IntS() extends SortCategory { ): immutable.Seq[(String, immutable.Seq[String], DecisionTree)] = cases .groupBy(t => getLimb(t._1, i)) - .to[immutable.Seq] + .to(immutable.Seq) .map(t => (t._1, immutable.Seq(), limbSwitch(litO, size, t._2, default, i + 1))) def sizeOf(str: String): Int = { @@ -632,17 +632,17 @@ 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: immutable.Seq[Constructor], isExact: Boolean, @@ -663,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 } From f0dbb205a7f688a6c1d9c3df9ea31d867113e2de Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 9 Apr 2024 17:46:36 -0400 Subject: [PATCH 7/9] Update mvnHash --- nix/overlay.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/overlay.nix b/nix/overlay.nix index eb51d6b35..386cfb76d 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-ZmxDfQAQ4sq7yZEwCS8I3TNZeENTZlkiHQFObNdeSRE="; + mvnHash = "sha256-lBP4WL0sgyW1mULqujaivT+uvobKQVIWpS7qGnnHCeU="; inherit (final) maven; }; From 087d7cbb4b89148de4e4196a85c705f3d4668863 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 9 Apr 2024 17:53:42 -0400 Subject: [PATCH 8/9] Update Scala compiler bridge dependency to 2.13 --- matching/pom.xml | 2 +- nix/llvm-backend-matching.nix | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/matching/pom.xml b/matching/pom.xml index f5763cdd9..3adc0681b 100644 --- a/matching/pom.xml +++ b/matching/pom.xml @@ -82,7 +82,7 @@ org.scala-sbt - compiler-bridge_2.12 + compiler-bridge_2.13 1.8.0 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 = { From 1d0effa9fd1fd2921e0a866cd780a7e01bb82f53 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 9 Apr 2024 18:08:08 -0400 Subject: [PATCH 9/9] Update mvnHash (again) --- nix/overlay.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nix/overlay.nix b/nix/overlay.nix index 386cfb76d..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-lBP4WL0sgyW1mULqujaivT+uvobKQVIWpS7qGnnHCeU="; + mvnHash = "sha256-jO6g5yuae6oU9XCVmDXa678Hzz1zroaMv7/wzgWbUzI="; inherit (final) maven; };