Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Miscellaneous Scala cleanup #1006

Merged
merged 10 commits into from
Mar 19, 2024
22 changes: 9 additions & 13 deletions matching/pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -75,22 +75,26 @@
<version>1.4</version>
<classifier>linux64</classifier>
</dependency>
<dependency>
<groupId>org.scala-sbt</groupId>
<artifactId>compiler-bridge_2.12</artifactId>
<version>1.8.0</version>
</dependency>
</dependencies>

<build>
<plugins>
<plugin>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.7.0</version>
<version>3.12.1</version>
<configuration>
<source>${java.version}</source>
<target>${java.version}</target>
<release>${java.version}</release>
</configuration>
</plugin>
<plugin>
<groupId>net.alchim31.maven</groupId>
<artifactId>scala-maven-plugin</artifactId>
<version>3.3.1</version>
<version>4.8.1</version>
<executions>
<execution>
<id>scala-compile-first</id>
Expand All @@ -110,18 +114,10 @@
</executions>
<configuration>
<args>
<arg>-Xexperimental</arg>
<arg>-Werror</arg>
<arg>-feature</arg>
<arg>-deprecation</arg>
<arg>-language:implicitConversions</arg>
<arg>-language:postfixOps</arg>
</args>
<javacArgs>
<javacArg>-source</javacArg>
<javacArg>${java.version}</javacArg>
<javacArg>-target</javacArg>
<javacArg>${java.version}</javacArg>
</javacArgs>
</configuration>
</plugin>
<plugin>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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) =>
Expand All @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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) =>
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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) =>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
9 changes: 5 additions & 4 deletions nix/build-maven-package.nix
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
6 changes: 6 additions & 0 deletions nix/llvm-backend-matching.nix
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion nix/overlay.nix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
};

Expand Down
Loading