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

Update dependency: matching/deps/scala_kore_release #1024

Merged
merged 11 commits into from
Apr 11, 2024
2 changes: 1 addition & 1 deletion matching/deps/scala_kore_release
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.3.0
0.3.3
13 changes: 9 additions & 4 deletions matching/pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@

<properties>
<java.version>17</java.version>
<scala-kore.version>0.3.0</scala-kore.version>
<scala-kore.version>0.3.3</scala-kore.version>
<spotless.version>2.41.1</spotless.version>
<scala.majorVersion>2.12</scala.majorVersion>
<scala.minorVersion>18</scala.minorVersion>
<scala.majorVersion>2.13</scala.majorVersion>
<scala.minorVersion>13</scala.minorVersion>
<scala.version>${scala.majorVersion}.${scala.minorVersion}</scala.version>
<scalafmt.version>3.7.17</scalafmt.version>
</properties>
Expand Down Expand Up @@ -48,6 +48,11 @@
<artifactId>scala-reflect</artifactId>
<version>${scala.version}</version>
</dependency>
<dependency>
<groupId>org.scala-lang.modules</groupId>
<artifactId>scala-parallel-collections_2.13</artifactId>
<version>1.0.4</version>
</dependency>
<dependency>
<groupId>com.runtimeverification.k</groupId>
<artifactId>scala-kore</artifactId>
Expand Down Expand Up @@ -77,7 +82,7 @@
</dependency>
<dependency>
<groupId>org.scala-sbt</groupId>
<artifactId>compiler-bridge_2.12</artifactId>
<artifactId>compiler-bridge_2.13</artifactId>
<version>1.8.0</version>
</dependency>
</dependencies>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,101 +2,103 @@ package org.kframework.backend.llvm.matching

import com.runtimeverification.k.kore.SymbolOrAlias
import org.kframework.backend.llvm.matching.pattern._
import scala.collection.immutable

sealed trait Constructor {
def name: String
def isBest(pat: Pattern[Option[Occurrence]]): Boolean
def expand(f: Fringe): Option[Seq[Fringe]]
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String]
def expand(f: Fringe): Option[immutable.Seq[Fringe]]
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String]
}

case class Empty() extends Constructor {
def name = "0"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq())
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq())
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
val symbol = Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get
f.sortInfo.category match {
case SetS() => SetP(Seq(), None, symbol, SymbolP(symbol, Seq()))
case MapS() => MapP(Seq(), Seq(), None, symbol, SymbolP(symbol, Seq()))
case _ => ???
case SetS() => SetP(immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq()))
case MapS() =>
MapP(immutable.Seq(), immutable.Seq(), None, symbol, SymbolP(symbol, immutable.Seq()))
case _ => ???
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}

case class NonEmpty() extends Constructor {
def name: String = ???
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq(f))
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = children(0)
def name: String = ???
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq(f))
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = children.head
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}

case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Option[Occurrence]]])
extends Constructor {
def name = "1"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = key.isDefined && pat == key.get
def expand(f: Fringe): Option[Seq[Fringe]] = {
def expand(f: Fringe): Option[immutable.Seq[Fringe]] = {
val sorts = f.symlib.signatures(element)._1
key match {
case None =>
if (isSet) {
Some(
Seq(
new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false),
new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false)
immutable.Seq(
Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false),
Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false)
)
)
} else {
Some(
Seq(
new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false),
new Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), false),
new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), false)
immutable.Seq(
Fringe(f.symlib, sorts.head, Choice(f.occurrence), isExact = false),
Fringe(f.symlib, sorts(1), ChoiceValue(f.occurrence), isExact = false),
Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), isExact = false)
)
)
}
case Some(k) =>
if (isSet) {
Some(Seq(new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false), f))
Some(immutable.Seq(Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false), f))
} else {
Some(
Seq(
new Fringe(f.symlib, sorts(1), Value(k, f.occurrence), false),
new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false),
immutable.Seq(
Fringe(f.symlib, sorts(1), Value(k, f.occurrence), isExact = false),
Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false),
f
)
)
}
}
}
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
val child = children.last
var key: Pattern[String] = null
var value: Pattern[String] = null
assert((isSet && children.size == 2) || (!isSet && children.size == 3))
if (this.key.isEmpty) {
if (isSet) {
key = children(0)
key = children.head
} else {
key = children(0)
key = children.head
value = children(1)
}
} else {
if (isSet) {
key = this.key.get.decanonicalize
} else {
key = this.key.get.decanonicalize
value = children(0)
value = children.head
}
}
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
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)
Expand All @@ -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)
Expand All @@ -128,17 +130,17 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) extends Constructor {
def name = "0"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = key.isDefined && pat == key.get
def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq(f))
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
val child = children(0)
def expand(f: Fringe): Option[immutable.Seq[Fringe]] = Some(immutable.Seq(f))
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
val child = children.head
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k, v))
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k, v))
def setElement(k: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k))
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(k))
val unit: Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, immutable.Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, immutable.Seq(m1, m2))
def wildcard = WildcardP[String]()
child match {
case MapP(keys, values, frame, ctr, orig) =>
Expand All @@ -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)
Expand All @@ -177,21 +179,21 @@ case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) ex
case class ListC(element: SymbolOrAlias, length: Int) extends Constructor {
def name: String = length.toString
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[Seq[Fringe]] = {
def expand(f: Fringe): Option[immutable.Seq[Fringe]] = {
val sort = f.symlib.signatures(element)._1.head
Some((0 until length).map(i => new Fringe(f.symlib, sort, Num(i, f.occurrence), false)))
Some((0 until length).map(i => Fringe(f.symlib, sort, Num(i, f.occurrence), isExact = false)))
}
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] = {
def element(v: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(v))
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, immutable.Seq(v))
val unit: Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, immutable.Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, immutable.Seq(m1, m2))
ListP(
children,
None,
Seq(),
immutable.Seq(),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
children.map(element).fold(unit)(concat)
)
Expand All @@ -202,27 +204,27 @@ case class ListC(element: SymbolOrAlias, length: Int) extends Constructor {
case class SymbolC(sym: SymbolOrAlias) extends Constructor {
def name: String = sym.toString
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[Seq[Fringe]] =
def expand(f: Fringe): Option[immutable.Seq[Fringe]] =
if (f.symlib.signatures(sym)._2 != f.sort) {
None
} else {
val sorts = f.symlib.signatures(sym)._1
Some(
sorts.zipWithIndex.map(t =>
new Fringe(f.symlib, t._1, Num(t._2, f.occurrence), sym.ctr == "inj")
Fringe(f.symlib, t._1, Num(t._2, f.occurrence), sym.ctr == "inj")
)
)
}
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] =
def contract(f: Fringe, children: immutable.Seq[Pattern[String]]): Pattern[String] =
SymbolP(sym, children)
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}

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)
}
Loading
Loading