Skip to content

Commit

Permalink
Update dependency: matching/deps/scala_kore_release (#1024)
Browse files Browse the repository at this point in the history 
Co-authored-by: devops <[email protected]>
Co-authored-by: Bruce Collie <[email protected]>
Co-authored-by: Scott Guest <[email protected]>
  • Loading branch information
@rv-jenkins @Baltoli @Scott-Guest
4 people authored Apr 11, 2024
1 parent 4f1a261 commit 89ced16
Show file tree
Hide file tree
Showing 14 changed files with 809 additions and 659 deletions.
2 changes: 1 addition & 1 deletion matching/deps/scala_kore_release
View file
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
View file
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
112 changes: 57 additions & 55 deletions matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala
View file
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

0 comments on commit 89ced16

Please sign in to comment.