Skip to content

Commit

Permalink
Adopt scalafmt for Scala code style (#920)
Browse files Browse the repository at this point in the history
In runtimeverification/k#3841, we adopted the
`scalafmt` tool to auto-format the Scala code in the K frontend. This PR
adopts a precisely identical formatting setup for the LLVM backend's
Scala code.
  • Loading branch information
Baltoli authored Dec 12, 2023
1 parent eeccaeb commit 14c372e
Show file tree
Hide file tree
Showing 15 changed files with 3,179 additions and 1,291 deletions.
23 changes: 23 additions & 0 deletions .github/workflows/clang-format-check.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,3 +26,26 @@ jobs:
name: Check that shell scripts follow best practices
with:
scandir: './bin'

scala-check:
name: Scala formatting check
runs-on: ubuntu-latest
steps:
- name: 'Check out code'
uses: actions/checkout@v3

- name: 'Set up Java 17'
uses: actions/setup-java@v3
with:
distribution: 'zulu'
java-version: 17

- name: 'Install Maven'
run: |
sudo apt-get update
sudo apt-get install --yes maven
- name: 'Check code is formatted correctly'
run: |
cd matching
mvn spotless:check --batch-mode -U
50 changes: 0 additions & 50 deletions .github/workflows/update.yml

This file was deleted.

27 changes: 27 additions & 0 deletions matching/.scalafmt.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
version = 3.7.17
runner.dialect = scala212
maxColumn = 100
align.preset = more
docstrings.style = Asterisk
comments {
wrap = trailing
wrapStandaloneSlcAsSlc = true
}
assumeStandardLibraryStripMargin = true
spaces.inImportCurlyBraces = true
rewrite {
rules = [
AvoidInfix,
RedundantBraces,
RedundantParens,
SortModifiers,
PreferCurlyFors,
Imports
]
sortModifiers.order = ["private", "protected", "final", "sealed", "abstract", "implicit", "override", "lazy"]
imports {
expand = true
sort = original
}
trailingCommas.style = never
}
15 changes: 15 additions & 0 deletions matching/pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,21 @@
</execution>
</executions>
</plugin>
<plugin>
<groupId>com.diffplug.spotless</groupId>
<artifactId>spotless-maven-plugin</artifactId>
<version>${spotless.version}</version>
<configuration>
<scala>
<includes>**/*.scala,**/*.sbt</includes>
<scalafmt>
<version>${scalafmt.version}</version>
<file>.scalafmt.conf</file>
<scalaMajorVersion>${scala.majorVersion}</scalaMajorVersion>
</scalafmt>
</scala>
</configuration>
</plugin>
</plugins>
</build>
</project>
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@ sealed trait Constructor {
}

case class Empty() extends Constructor {
def name = "0"
def name = "0"
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq())
def expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq())
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
val symbol = Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get
f.sortInfo.category match {
Expand All @@ -25,36 +25,54 @@ case class Empty() extends Constructor {
}

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 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)
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"
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]] = {
val sorts = f.symlib.signatures(element)._1
key match {
case None =>
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)))
Some(
Seq(
new Fringe(f.symlib, sorts(0), Choice(f.occurrence), false),
new Fringe(f.symlib, f.sort, ChoiceRem(f.occurrence), 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)))
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)
)
)
}
case Some(k) =>
if (isSet) {
Some(Seq(new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), 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), f))
Some(
Seq(
new Fringe(f.symlib, sorts(1), Value(k, f.occurrence), false),
new Fringe(f.symlib, f.sort, Rem(k, f.occurrence), false),
f
)
)
}
}
}
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
val child = children.last
var key: Pattern[String] = null
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) {
Expand All @@ -72,107 +90,136 @@ case class HasKey(isSet: Boolean, element: SymbolOrAlias, key: Option[Pattern[Op
value = children(0)
}
}
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] = {
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k, v))
}
def setElement(k: Pattern[String]): Pattern[String] = {
def setElement(k: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k))
}
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] = {
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
}
child match {
case MapP(keys, values, frame, ctr, orig) =>
MapP(key +: keys, value +: values, frame, ctr, orig)
case SetP(elems, frame, ctr, orig) =>
SetP(key +: elems, frame, ctr, orig)
case WildcardP() | VariableP(_, _) =>
if (isSet) {
SetP(Seq(key), Some(child), Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, concat(setElement(key), child))
SetP(
Seq(key),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(setElement(key), child)
)
} else {
MapP(Seq(key), Seq(value), Some(child), Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, concat(element(key, value), child))
MapP(
Seq(key),
Seq(value),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(element(key, value), child)
)
}
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}

case class HasNoKey(isSet: Boolean, key: Option[Pattern[Option[Occurrence]]]) extends Constructor {
def name = "0"
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 expand(f: Fringe): Option[Seq[Fringe]] = Some(Seq(f))
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
val child = children(0)
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] = {
def element(k: Pattern[String], v: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k, v))
}
def setElement(k: Pattern[String]): Pattern[String] = {
def setElement(k: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(k))
}
val unit: Pattern[String] = SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] = {
val unit: Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
}
def wildcard = WildcardP[String]()
child match {
case MapP(keys, values, frame, ctr, orig) =>
MapP(wildcard +: keys, wildcard +: values, frame, ctr, concat(element(wildcard, wildcard), orig))
case SetP(elems, frame, ctr, orig) =>
case MapP(keys, values, frame, ctr, orig) =>
MapP(
wildcard +: keys,
wildcard +: values,
frame,
ctr,
concat(element(wildcard, wildcard), orig)
)
case SetP(elems, frame, ctr, orig) =>
SetP(wildcard +: elems, frame, ctr, concat(setElement(wildcard), orig))
case WildcardP() | VariableP(_, _) =>
if (isSet) {
SetP(Seq(wildcard), Some(child), Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, concat(setElement(wildcard), child))
SetP(
Seq(wildcard),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(setElement(wildcard), child)
)
} else {
MapP(Seq(wildcard), Seq(wildcard), Some(child), Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, concat(element(wildcard, wildcard), child))
MapP(
Seq(wildcard),
Seq(wildcard),
Some(child),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
concat(element(wildcard, wildcard), child)
)
}
}
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}

case class ListC(element: SymbolOrAlias, length: Int) extends Constructor {
def name: String = length.toString
def name: String = length.toString
def isBest(pat: Pattern[Option[Occurrence]]): Boolean = true
def expand(f: Fringe): Option[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)))
}
def contract(f: Fringe, children: Seq[Pattern[String]]): Pattern[String] = {
def element(v: Pattern[String]): Pattern[String] = {
def element(v: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, Seq(v))
}
val unit: Pattern[String] = SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] = {
val unit: Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "unit").get, Seq())
def concat(m1: Pattern[String], m2: Pattern[String]): Pattern[String] =
SymbolP(Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "concat").get, Seq(m1, m2))
}
ListP(children, None, Seq(), Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get, children.map(element).fold(unit)(concat))
ListP(
children,
None,
Seq(),
Parser.getSymbolAtt(f.symlib.sortAtt(f.sort), "element").get,
children.map(element).fold(unit)(concat)
)
}
override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
}

case class SymbolC(sym: SymbolOrAlias) extends Constructor {
def name: String = sym.toString
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[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")))
Some(
sorts.zipWithIndex.map(t =>
new 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: 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 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[Seq[Fringe]] = Some(Seq())
def contract(f: Fringe, children: 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 14c372e

Please sign in to comment.