Skip to content

Commit

Permalink
Format with Play Framework config
Browse files Browse the repository at this point in the history
  • Loading branch information
Scott-Guest committed Dec 5, 2023
1 parent 02dde4e commit ea8435b
Show file tree
Hide file tree
Showing 50 changed files with 1,023 additions and 871 deletions.
Original file line number Diff line number Diff line change
@@ -1,30 +1,30 @@
// Copyright (c) K Team. All Rights Reserved.
package org.kframework.backend.kore

import java.io.File
import java.nio.file.Files

import org.kframework.compile.Backend
import org.kframework.kompile.Kompile
import org.kframework.kompile.KompileOptions
import org.kframework.main.GlobalOptions
import org.kframework.main.Tool
import org.kframework.parser.kore._
import org.kframework.parser.kore.implementation.{ DefaultBuilders => B }
import org.kframework.parser.kore.parser.TextToKore
import org.kframework.utils.errorsystem.KExceptionManager
import org.kframework.utils.file.FileUtil
import org.kframework.utils.options.InnerParsingOptions
import org.kframework.utils.options.OuterParsingOptions
import org.kframework.parser.kore._
import org.kframework.parser.kore.implementation.{DefaultBuilders => B}
import org.kframework.parser.kore.parser.TextToKore
import org.kframework.utils.Stopwatch
import org.kframework.utils.options.InnerParsingOptions

import java.io.File
import java.nio.file.Files

class KoreTest {

val global: GlobalOptions = new GlobalOptions()

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
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
// Copyright (c) K Team. All Rights Reserved.
package org.kframework.backend.kore

import org.kframework.parser.kore.implementation.{DefaultBuilders => B}

import org.junit.Test
import org.junit.Assert._
import org.junit.Test
import org.kframework.parser.kore.implementation.{ DefaultBuilders => B }

class NoAppendIT extends KoreTest {

Expand Down
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
2 changes: 1 addition & 1 deletion kore/project/build.sbt
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright (c) 2014-2019 K Team. All Rights Reserved.

resolvers += "Sonatype snapshots" at "https://oss.sonatype.org/content/repositories/snapshots/"
resolvers += "Sonatype snapshots".at("https://oss.sonatype.org/content/repositories/snapshots/")

addSbtPlugin("com.github.shivawu" %% "sbt-maven-plugin" % "0.1.3-SNAPSHOT")

Expand Down
67 changes: 34 additions & 33 deletions kore/src/main/scala/org/kframework/POSet.scala
Original file line number Diff line number Diff line change
@@ -1,63 +1,61 @@
// Copyright (c) K Team. All Rights Reserved.
package org.kframework

import org.kframework.utils.errorsystem.KEMException

import java.util
import collection._

import scala.annotation.tailrec

import collection._
import org.kframework.utils.errorsystem.KEMException

/**
* A partially ordered set based on an initial set of direct relations.
*/
class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
// convert the input set of relations to Map form for performance
private val directRelationsMap: Map[T, Set[T]] = directRelations groupBy { _._1 } mapValues {
_ map { _._2 } toSet
} map identity
private val directRelationsMap: Map[T, Set[T]] =
directRelations.groupBy { _._1 }.mapValues { _.map { _._2 } toSet }.map(identity)

lazy val elements: Set[T] = directRelations.flatMap(a => Set(a._1, a._2))

lazy val sortedElements: scala.collection.immutable.List[T] =
TopologicalSort.tsort(directRelations).toList

/**
* Internal private method. Computes the transitive closer of the initial relations. It also
* checks for cycles during construction and throws an exception if it finds any.
* Internal private method. Computes the transitive closer of the initial relations.
* It also checks for cycles during construction and throws an exception if it finds any.
*
* The implementation is simple. It links each element to the successors of its successors. TODO:
* there may be a more efficient algorithm (low priority)
* The implementation is simple. It links each element to the successors of its successors.
* TODO: there may be a more efficient algorithm (low priority)
*/
@tailrec
private def transitiveClosure(relations: Map[T, Set[T]]): Map[T, Set[T]] = {
val newRelations = relations map { case (start, succ) =>
val newSucc = succ flatMap { relations.getOrElse(_, Set()) }
if (newSucc.contains(start))
constructAndThrowCycleException(start, start, Seq())
(start, succ | newSucc)
val newRelations = relations.map {
case (start, succ) =>
val newSucc = succ.flatMap { relations.getOrElse(_, Set()) }
if (newSucc.contains(start))
constructAndThrowCycleException(start, start, Seq())
(start, succ | newSucc)
}
if (relations != newRelations) transitiveClosure(newRelations) else relations
}

/**
* Recursive method constructing and throwing and the cycle exception.
*
* @param start
* (or tail) element to look for when constructing the cycle
* @param current
* element
* @param path
* so far
* @param start (or tail) element to look for when constructing the cycle
* @param current element
* @param path so far
*/
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(" < ")
)
}
succs foreach { constructAndThrowCycleException(start, _, currentPath) }
succs.foreach { constructAndThrowCycleException(start, _, currentPath) }
}

/**
Expand All @@ -84,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 @@ -133,7 +131,8 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
if (lessThanEq(x, y)) -1 else if (lessThanEq(y, x)) 1 else 0

/**
* Return the subset of items from the argument which are not less than any other item.
* Return the subset of items from the argument which are not
* less than any other item.
*/
def maximal(sorts: Iterable[T]): Set[T] =
sorts.filter(s1 => !sorts.exists(s2 => lessThan(s1, s2))).toSet
Expand All @@ -142,7 +141,8 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
Collections.mutable(maximal(Collections.immutable(sorts)))

/**
* Return the subset of items from the argument which are not greater than any other item.
* Return the subset of items from the argument which are not
* greater than any other item.
*/
def minimal(sorts: Iterable[T]): Set[T] =
sorts.filter(s1 => !sorts.exists(s2 => >(s1, s2))).toSet
Expand All @@ -151,7 +151,8 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {
Collections.mutable(minimal(Collections.immutable(sorts)))

override def toString: String = {
"POSet(" + (relations flatMap { case (from, tos) => tos map { to => from + "<" + to } })
"POSet(" + relations
.flatMap { case (from, tos) => tos.map { to => from + "<" + to } }
.mkString(",") + ")"
}

Expand All @@ -165,7 +166,7 @@ class POSet[T](val directRelations: Set[(T, T)]) extends Serializable {

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 All @@ -180,5 +181,5 @@ object POSet {
* using the provided relations map. Input must be non-empty.
*/
private def upperBounds[T](sorts: Iterable[T], relations: Map[T, Set[T]]): Set[T] =
sorts map { s => relations.getOrElse(s, Set.empty) + s } reduce { (a, b) => a & b }
sorts.map { s => relations.getOrElse(s, Set.empty) + s }.reduce { (a, b) => a & b }
}
21 changes: 10 additions & 11 deletions kore/src/main/scala/org/kframework/Strategy.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,21 +6,20 @@ import org.kframework.builtin.BooleanUtils
import org.kframework.builtin.KLabels
import org.kframework.builtin.Sorts
import org.kframework.compile.RewriteToTop
import org.kframework.definition.{
DefinitionTransformer,
ModuleTransformer,
Module,
Rule,
Definition
}
import org.kframework.definition.Definition
import org.kframework.definition.DefinitionTransformer
import org.kframework.definition.Module
import org.kframework.definition.ModuleTransformer
import org.kframework.definition.Rule
import org.kframework.kore.ExistsK
import org.kframework.kore.KApply
import org.kframework.kore.KORE
import org.kframework.kore.Sort
import org.kframework.kore.Unapply.{KApply, KLabel}
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 All @@ -39,15 +38,15 @@ object Strategy {
KORE.KVariable("S", Att.empty.add(classOf[Sort], Sorts.KItem)),
KORE.KSequence(
KORE.KApply(KORE.KLabel("#STUCK")),
KORE.KVariable("S", Att.empty.add(classOf[Sort], Sorts.KItem))
KORE.KVariable("S", Att.empty.add(classOf[Sort], Sorts.KItem)),
)
),
KORE.KApply(KLabels.DOTS)
),
KORE.KApply(
KLabels.NOT_EQUALS_K,
KORE.KVariable("S", Att.empty.add(classOf[Sort], Sorts.KItem)),
KORE.KApply(KORE.KLabel("#STUCK"))
KORE.KApply(KORE.KLabel("#STUCK")),
),
BooleanUtils.TRUE,
Att.empty.add(Att.OWISE)
Expand Down
Loading

0 comments on commit ea8435b

Please sign in to comment.