diff --git a/matching/pom.xml b/matching/pom.xml
index 334f5e565..66ec6d4ab 100644
--- a/matching/pom.xml
+++ b/matching/pom.xml
@@ -75,22 +75,26 @@
1.4
linux64
+
+ org.scala-sbt
+ compiler-bridge_2.12
+ 1.8.0
+
maven-compiler-plugin
- 3.7.0
+ 3.12.1
- ${java.version}
- ${java.version}
+ ${java.version}
net.alchim31.maven
scala-maven-plugin
- 3.3.1
+ 4.8.1
scala-compile-first
@@ -110,18 +114,10 @@
- -Xexperimental
+ -Werror
-feature
-deprecation
- -language:implicitConversions
- -language:postfixOps
-
- -source
- ${java.version}
- -target
- ${java.version}
-
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 5b1a1a127..5e115bed4 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
@@ -19,6 +19,7 @@ case class Empty() extends Constructor {
f.sortInfo.category match {
case SetS() => SetP(Seq(), None, symbol, SymbolP(symbol, Seq()))
case MapS() => MapP(Seq(), Seq(), None, symbol, SymbolP(symbol, Seq()))
+ case _ => ???
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
@@ -118,6 +119,7 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
concat(element(key, value), child)
)
}
+ case _ => ???
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
@@ -166,6 +168,7 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex
concat(element(wildcard, wildcard), child)
)
}
+ case _ => ???
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
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 e327a6efb..bc495def4 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
@@ -781,18 +781,20 @@ 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,
- 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,
+ 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) {
case ((SymbolC(inj), f, v), dt) =>
@@ -810,6 +812,7 @@ class Matrix private (
),
dt
)
+ case _ => ???
}
val withSpecials = row.clause.specializedVars.foldRight(withOverloads) { case ((o, p), dt) =>
MakePattern(o, p._1.hookAtt, p._2, dt)
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 878c69f47..e9ab71be9 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
@@ -429,6 +429,7 @@ object Parser {
val heuristicMap: Map[Char, Heuristic] = {
import scala.reflect.runtime.universe
+ import universe.LiteralTag
val heuristicType = universe.typeOf[Heuristic]
val heuristicClass = heuristicType.typeSymbol.asClass
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 8f63cc406..4af8acc26 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,7 +4,6 @@ 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.math.min
sealed trait Pattern[T] {
def signature(clause: Clause): Seq[Constructor]
@@ -365,6 +364,7 @@ case class MapP[T] private (
case (HasNoKey(_, Some(p)), _) => !keys.map(_.canonicalize(clause)).contains(p)
case (HasKey(_, _, None), None) => keys.nonEmpty && clause.action.priority <= maxPriority
case (HasNoKey(_, None), _) => keys.nonEmpty && clause.action.priority > maxPriority
+ case _ => ???
}
def score(
h: Heuristic,
@@ -419,6 +419,7 @@ case class MapP[T] private (
} else {
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) =>
@@ -593,6 +594,7 @@ case class SetP[T] private (
case (HasNoKey(_, Some(p)), _) => !elements.map(_.canonicalize(clause)).contains(p)
case (HasKey(_, _, None), None) => elements.nonEmpty && clause.action.priority <= maxPriority
case (HasNoKey(_, None), _) => elements.nonEmpty && clause.action.priority > maxPriority
+ case _ => ???
}
def score(
h: Heuristic,
@@ -640,6 +642,7 @@ case class SetP[T] private (
} else {
Seq(elements.head, SetP(elements.tail, frame, ctr, orig))
}
+ case _ => ???
}
def expandOr: Seq[Pattern[T]] = {
val withElements = elements.indices.foldLeft(Seq(this))((accum, ix) =>
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 b14de285e..210587a90 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
@@ -49,6 +49,7 @@ object SortCategory {
MatchingException.Type.COMPILER_ERROR,
"LLVM Backend does not support multisets. If you are seeing this error due to a configuration cell tagged with multiplicity=\"*\", please add either type=\"Map\" or type=\"Set\". If you still need the collection to not contain duplicates, it is recommended you also add a unique identifier each time a cell is created. You can do this with !X:Int."
);
+ case _ => ???
}
private def getBitwidth(s: Sort, symlib: Parser.SymLib): Int =
diff --git a/nix/build-maven-package.nix b/nix/build-maven-package.nix
index 8ff94f033..890645c1b 100644
--- a/nix/build-maven-package.nix
+++ b/nix/build-maven-package.nix
@@ -26,12 +26,13 @@ let
mvn dependency:get -Dartifact="$artifactId" -Dmaven.repo.local=$out/.m2
done
- for artifactId in ${builtins.toString manualMvnSourceArtifacts}
+ for artifact in ${builtins.toString manualMvnSourceArtifacts}
do
- group=$(echo $artifactId | cut -d':' -f1)
- artifact=$(echo $artifactId | cut -d':' -f2)
+ groupId=$(echo $artifact | cut -d':' -f1)
+ artifactId=$(echo $artifact | cut -d':' -f2)
+ version=$(echo $artifact | cut -d':' -f3)
echo "downloading manual sources $artifactId"
- mvn dependency:sources -DincludeGroupIds=$group -DincludeArtifactIds=$artifact -Dmaven.repo.local=$out/.m2
+ mvn dependency:get -Dclassifier=sources -DgroupId=$groupId -DartifactId=$artifactId -Dversion=$version -Dmaven.repo.local=$out/.m2
done
'' + lib.optionalString (!buildOffline) ''
mvn package -Dmaven.repo.local=$out/.m2 ${mvnParameters}
diff --git a/nix/llvm-backend-matching.nix b/nix/llvm-backend-matching.nix
index 4dcaf0063..fc6ae97db 100644
--- a/nix/llvm-backend-matching.nix
+++ b/nix/llvm-backend-matching.nix
@@ -12,11 +12,17 @@ let self = maven.buildMavenPackage rec {
"org.apache.maven.plugins:maven-compiler-plugin:3.7.0"
];
+ manualMvnSourceArtifacts = [
+ "org.scala-sbt:compiler-bridge_2.12:1.8.0"
+ ];
+
passthru = {
jar =
"${self}/share/java/llvm-backend-matching-1.0-SNAPSHOT-jar-with-dependencies.jar";
};
+ mvnParameters = "-DsecondaryCacheDir=secondary-cache";
+
installPhase = ''
mkdir -p $out/share/java
install -Dm644 target/*.jar $out/share/java
diff --git a/nix/overlay.nix b/nix/overlay.nix
index 0978acdf7..1f96aedee 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-HF6BXeCnV5I7+oRVGK8DGHjaAtHWLfEaCwtkVcQHoGU";
+ mvnHash = "sha256-2X8G3T05Pk1apA0f04Mdu/8DAB89oB9XwTBQ3KVoc/A=";
inherit (final) maven;
};