Skip to content

Commit

Permalink
Format with alignment
Browse files Browse the repository at this point in the history
  • Loading branch information
Scott-Guest committed Dec 5, 2023
1 parent d677510 commit b0960a8
Show file tree
Hide file tree
Showing 36 changed files with 529 additions and 529 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ class KoreTest {

val files: FileUtil = {
val tempRoot = Files.createTempDirectory("kore-test").toFile
val tempDir = new File(tempRoot, "tmp")
val tempDir = new File(tempRoot, "tmp")
tempDir.mkdirs()
val kompiledDir = new File(tempRoot, "kompiled")
kompiledDir.mkdirs()
Expand Down Expand Up @@ -125,7 +125,7 @@ class KoreTest {
) =>
Some(eq)
case eq @ Equals(_, _, Application(_, _), _) => Some(eq)
case _ => None
case _ => None

}
go(axiom.pattern)
Expand All @@ -136,21 +136,21 @@ class KoreTest {

def symbols(pat: Pattern): Seq[SymbolOrAlias] =
pat match {
case And(_, ps) => ps.flatMap(symbols)
case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
case Ceil(_, _, p) => symbols(p)
case And(_, ps) => ps.flatMap(symbols)
case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols)
case Ceil(_, _, p) => symbols(p)
case Equals(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
case Exists(_, _, p) => symbols(p)
case Floor(_, _, p) => symbols(p)
case Forall(_, _, p) => symbols(p)
case Iff(_, p1, p2) => symbols(p1) ++ symbols(p2)
case Implies(_, p1, p2) => symbols(p1) ++ symbols(p2)
case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
case Exists(_, _, p) => symbols(p)
case Floor(_, _, p) => symbols(p)
case Forall(_, _, p) => symbols(p)
case Iff(_, p1, p2) => symbols(p1) ++ symbols(p2)
case Implies(_, p1, p2) => symbols(p1) ++ symbols(p2)
case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2)
// case Next(_, p) => symbols(p)
case Not(_, p) => symbols(p)
case Or(_, ps) => ps.flatMap(symbols)
case Not(_, p) => symbols(p)
case Or(_, ps) => ps.flatMap(symbols)
case Rewrites(_, p1, p2) => symbols(p1) ++ symbols(p2)
case _ => Seq()
case _ => Seq()
}

}
6 changes: 3 additions & 3 deletions kore/build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@
net.virtualvoid.sbt.graph.Plugin.graphSettings

libraryDependencies ++= Seq(
"org.scalacheck" %% "scalacheck" % "1.11.4" % "test",
"com.novocode" % "junit-interface" % "0.9" % "test",
"junit" % "junit" % "4.11" % "test"
"org.scalacheck" %% "scalacheck" % "1.11.4" % "test",
"com.novocode" % "junit-interface" % "0.9" % "test",
"junit" % "junit" % "4.11" % "test"
)

EclipseKeys.withSource := true
16 changes: 8 additions & 8 deletions kore/src/main/scala/org/kframework/POSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
*/
private def constructAndThrowCycleException(start: T, current: T, path: Seq[T]): Unit = {
val currentPath = path :+ current
val succs = directRelationsMap.getOrElse(current, Set())
val succs = directRelationsMap.getOrElse(current, Set())
if (succs.contains(start)) {
throw KEMException.compilerError(
"Illegal circular relation: " + (currentPath :+ start).mkString(" < ")
Expand Down Expand Up @@ -82,21 +82,21 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
/**
* Returns true if x < y
*/
def lessThan(x: T, y: T): Boolean = <(x, y)
def lessThanEq(x: T, y: T): Boolean = x == y || <(x, y)
def lessThan(x: T, y: T): Boolean = <(x, y)
def lessThanEq(x: T, y: T): Boolean = x == y || <(x, y)
def directlyLessThan(x: T, y: T): Boolean = directRelationsMap.get(x).exists(_.contains(y))

/**
* Returns true if y < x
*/
def greaterThan(x: T, y: T): Boolean = >(x, y)
def greaterThanEq(x: T, y: T): Boolean = x == y || >(x, y)
def greaterThan(x: T, y: T): Boolean = >(x, y)
def greaterThanEq(x: T, y: T): Boolean = x == y || >(x, y)
def directlyGreaterThan(x: T, y: T): Boolean = directRelationsMap.get(y).exists(_.contains(x))

/**
* Returns true if y < x or y < x
*/
def inSomeRelation(x: T, y: T): Boolean = this.~(x, y)
def inSomeRelation(x: T, y: T): Boolean = this.~(x, y)
def inSomeRelationEq(x: T, y: T): Boolean = x == y || this.~(x, y)

/**
Expand Down Expand Up @@ -157,13 +157,13 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {

override def equals(that: Any): Boolean = that match {
case that: POSet[_] => relations == that.relations
case _ => false
case _ => false
}
}

object POSet {
def apply[T](relations: (T, T)*) = new POSet(relations.toSet)
def apply[T](s: Set[(T, T)]) = new POSet(s)
def apply[T](s: Set[(T, T)]) = new POSet(s)

/**
* Import this for Scala syntactic sugar.
Expand Down
2 changes: 1 addition & 1 deletion kore/src/main/scala/org/kframework/Strategy.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ import org.kframework.kore.Unapply.KApply
import org.kframework.kore.Unapply.KLabel

object Strategy {
val strategyCellName = "<s>"
val strategyCellName = "<s>"
val strategyCellLabel = KORE.KLabel(strategyCellName)

def addStrategyRuleToMainModule(mainModuleName: String) =
Expand Down
Loading

0 comments on commit b0960a8

Please sign in to comment.