From f7c529d3620810ef34880fcc1b9d1f9c7a8f404c Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 9 Apr 2024 09:11:52 -0400 Subject: [PATCH 1/3] Replace all unqualified usages of Seq with immutable.Seq --- .../runtimeverification/k/kore/Default.scala | 80 ++++++------ .../k/kore/interface.scala | 115 ++++++++++-------- .../k/kore/parser/TextToKore.scala | 31 ++--- .../parser/kore/InterfaceTest.scala | 31 ++--- .../parser/kore/parser/TextToKoreTest.scala | 25 ++-- 5 files changed, 155 insertions(+), 127 deletions(-) diff --git a/src/main/scala/com/runtimeverification/k/kore/Default.scala b/src/main/scala/com/runtimeverification/k/kore/Default.scala index 6fd8be5128..d6a683f634 100644 --- a/src/main/scala/com/runtimeverification/k/kore/Default.scala +++ b/src/main/scala/com/runtimeverification/k/kore/Default.scala @@ -2,47 +2,49 @@ package com.runtimeverification.k.kore import com.runtimeverification.k.kore +import scala.collection.immutable object implementation { private object ConcreteClasses { - case class Definition(att: kore.Attributes, modules: Seq[kore.Module]) extends kore.Definition + case class Definition(att: kore.Attributes, modules: immutable.Seq[kore.Module]) + extends kore.Definition - case class Module(name: String, decls: Seq[Declaration], att: kore.Attributes) + case class Module(name: String, decls: immutable.Seq[Declaration], att: kore.Attributes) extends kore.Module case class Import(name: String, att: kore.Attributes) extends kore.Import case class SortDeclaration( - params: Seq[kore.SortVariable], + params: immutable.Seq[kore.SortVariable], sort: Sort, att: kore.Attributes ) extends kore.SortDeclaration case class HookSortDeclaration( - params: Seq[kore.SortVariable], + params: immutable.Seq[kore.SortVariable], sort: Sort, att: kore.Attributes ) extends kore.HookSortDeclaration case class SymbolDeclaration( symbol: kore.Symbol, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, att: kore.Attributes ) extends kore.SymbolDeclaration case class HookSymbolDeclaration( symbol: kore.Symbol, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, att: kore.Attributes ) extends kore.HookSymbolDeclaration case class AliasDeclaration( alias: kore.Alias, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, leftPattern: Pattern, rightPattern: Pattern, @@ -50,32 +52,33 @@ object implementation { ) extends kore.AliasDeclaration case class AxiomDeclaration( - params: Seq[kore.SortVariable], + params: immutable.Seq[kore.SortVariable], pattern: Pattern, att: kore.Attributes ) extends kore.AxiomDeclaration case class ClaimDeclaration( - params: Seq[kore.SortVariable], + params: immutable.Seq[kore.SortVariable], pattern: Pattern, att: kore.Attributes ) extends kore.ClaimDeclaration - case class Attributes(patterns: Seq[Pattern]) extends kore.Attributes + case class Attributes(patterns: immutable.Seq[Pattern]) extends kore.Attributes case class Variable(name: String, sort: Sort) extends kore.Variable case class SetVariable(name: String, sort: Sort) extends kore.SetVariable - case class Application(head: kore.SymbolOrAlias, args: Seq[Pattern]) extends kore.Application + case class Application(head: kore.SymbolOrAlias, args: immutable.Seq[Pattern]) + extends kore.Application case class Top(s: Sort) extends kore.Top case class Bottom(s: Sort) extends kore.Bottom - case class And(s: Sort, args: Seq[Pattern]) extends kore.And + case class And(s: Sort, args: immutable.Seq[Pattern]) extends kore.And - case class Or(s: Sort, args: Seq[Pattern]) extends kore.Or + case class Or(s: Sort, args: immutable.Seq[Pattern]) extends kore.Or case class Not(s: Sort, _1: Pattern) extends kore.Not @@ -110,62 +113,62 @@ object implementation { override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) } - case class CompoundSort(ctr: String, params: Seq[Sort]) extends kore.CompoundSort { + case class CompoundSort(ctr: String, params: immutable.Seq[Sort]) extends kore.CompoundSort { override lazy val toString = ctr + "{" + params.map(_.toString).mkString(", ") + "}" override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) } - case class SymbolOrAlias(ctr: String, params: Seq[Sort]) extends kore.SymbolOrAlias { + case class SymbolOrAlias(ctr: String, params: immutable.Seq[Sort]) extends kore.SymbolOrAlias { override lazy val toString = ctr + "{" + params.map(_.toString).mkString(", ") + "}" override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this) } - case class Symbol(ctr: String, params: Seq[Sort]) extends kore.Symbol + case class Symbol(ctr: String, params: immutable.Seq[Sort]) extends kore.Symbol - case class Alias(ctr: String, params: Seq[Sort]) extends kore.Alias + case class Alias(ctr: String, params: immutable.Seq[Sort]) extends kore.Alias } object DefaultBuilders extends Builders { import implementation.{ ConcreteClasses => d } - def Definition(att: Attributes, modules: Seq[Module]): Definition = + def Definition(att: Attributes, modules: immutable.Seq[Module]): Definition = d.Definition(att, modules) - def Module(name: String, decls: Seq[Declaration], att: Attributes): Module = + def Module(name: String, decls: immutable.Seq[Declaration], att: Attributes): Module = d.Module(name, decls, att) def Import(name: String, att: Attributes): Declaration = d.Import(name, att) def SortDeclaration( - params: Seq[SortVariable], + params: immutable.Seq[SortVariable], sort: Sort, att: Attributes ): Declaration = d.SortDeclaration(params, sort, att) def HookSortDeclaration( - params: Seq[SortVariable], + params: immutable.Seq[SortVariable], sort: Sort, att: Attributes ): Declaration = d.HookSortDeclaration(params, sort, att) def SymbolDeclaration( symbol: Symbol, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, att: Attributes ): Declaration = d.SymbolDeclaration(symbol, argSorts, returnSort, att) def HookSymbolDeclaration( symbol: Symbol, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, att: Attributes ): Declaration = d.HookSymbolDeclaration(symbol, argSorts, returnSort, att) def AliasDeclaration( alias: Alias, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, leftPattern: Pattern, rightPattern: Pattern, @@ -174,42 +177,42 @@ object implementation { d.AliasDeclaration(alias, argSorts, returnSort, leftPattern, rightPattern, att) def AxiomDeclaration( - params: Seq[SortVariable], + params: immutable.Seq[SortVariable], _1: Pattern, att: Attributes ): Declaration = d.AxiomDeclaration(params, _1, att) def ClaimDeclaration( - params: Seq[SortVariable], + params: immutable.Seq[SortVariable], _1: Pattern, att: Attributes ): Declaration = d.ClaimDeclaration(params, _1, att) - def Attributes(patterns: Seq[Pattern]): Attributes = d.Attributes(patterns) + def Attributes(patterns: immutable.Seq[Pattern]): Attributes = d.Attributes(patterns) def Variable(name: String, sort: Sort): Variable = d.Variable(name, sort) def SetVariable(name: String, sort: Sort): SetVariable = d.SetVariable(name, sort) - def Application(head: SymbolOrAlias, args: Seq[Pattern]): Pattern = + def Application(head: SymbolOrAlias, args: immutable.Seq[Pattern]): Pattern = d.Application(head, args) def Top(s: Sort): Pattern = d.Top(s) def Bottom(s: Sort): Pattern = d.Bottom(s) - def And(s: Sort, _1: Pattern, _2: Pattern): Pattern = d.And(s, Seq(_1, _2)) + def And(s: Sort, _1: Pattern, _2: Pattern): Pattern = d.And(s, immutable.Seq(_1, _2)) - def And(s: Sort, args: Seq[Pattern]): Pattern = + def And(s: Sort, args: immutable.Seq[Pattern]): Pattern = args.size match { case 0 => Top(s) case 1 => args(0) case _ => d.And(s, args) } - def Or(s: Sort, _1: Pattern, _2: Pattern): Pattern = d.Or(s, Seq(_1, _2)) + def Or(s: Sort, _1: Pattern, _2: Pattern): Pattern = d.Or(s, immutable.Seq(_1, _2)) - def Or(s: Sort, args: Seq[Pattern]): Pattern = + def Or(s: Sort, args: immutable.Seq[Pattern]): Pattern = args.size match { case 0 => Bottom(s) case 1 => args(0) @@ -251,19 +254,20 @@ object implementation { def SortVariable(name: String): SortVariable = d.SortVariable(name) - def CompoundSort(ctr: String, params: Seq[Sort]): CompoundSort = d.CompoundSort(ctr, params) + def CompoundSort(ctr: String, params: immutable.Seq[Sort]): CompoundSort = + d.CompoundSort(ctr, params) - def SymbolOrAlias(ctr: String, params: Seq[Sort]): SymbolOrAlias = + def SymbolOrAlias(ctr: String, params: immutable.Seq[Sort]): SymbolOrAlias = d.SymbolOrAlias(ctr, params) - def Symbol(ctr: String, params: Seq[Sort]): Symbol = d.Symbol(ctr, params) + def Symbol(ctr: String, params: immutable.Seq[Sort]): Symbol = d.Symbol(ctr, params) - def Alias(ctr: String, params: Seq[Sort]): Alias = d.Alias(ctr, params) + def Alias(ctr: String, params: immutable.Seq[Sort]): Alias = d.Alias(ctr, params) - def LeftAssoc(ctr: (Pattern, Pattern) => Pattern, args: Seq[Pattern]): Pattern = + def LeftAssoc(ctr: (Pattern, Pattern) => Pattern, args: immutable.Seq[Pattern]): Pattern = args.reduceLeft((accum, p) => ctr(accum, p)) - def RightAssoc(ctr: (Pattern, Pattern) => Pattern, args: Seq[Pattern]): Pattern = + def RightAssoc(ctr: (Pattern, Pattern) => Pattern, args: immutable.Seq[Pattern]): Pattern = args.reduceRight((p, accum) => ctr(p, accum)) } } diff --git a/src/main/scala/com/runtimeverification/k/kore/interface.scala b/src/main/scala/com/runtimeverification/k/kore/interface.scala index be0e25fc69..f273abbc2a 100644 --- a/src/main/scala/com/runtimeverification/k/kore/interface.scala +++ b/src/main/scala/com/runtimeverification/k/kore/interface.scala @@ -2,27 +2,29 @@ package com.runtimeverification.k.kore import com.davekoelle.AlphanumComparator +import scala.collection.immutable trait Definition { def att: Attributes - def modules: Seq[Module] + def modules: immutable.Seq[Module] } object Definition { - def unapply(arg: Definition): Option[(Seq[Module], Attributes)] = Some(arg.modules, arg.att) + def unapply(arg: Definition): Option[(immutable.Seq[Module], Attributes)] = + Some(arg.modules, arg.att) } trait Module { def name: String - def decls: Seq[Declaration] + def decls: immutable.Seq[Declaration] def att: Attributes } object Module { - def unapply(arg: Module): Option[(String, Seq[Declaration], Attributes)] = + def unapply(arg: Module): Option[(String, immutable.Seq[Declaration], Attributes)] = Some(arg.name, arg.decls, arg.att) } @@ -39,7 +41,7 @@ object Import { } trait SortDeclaration extends Declaration { - def params: Seq[SortVariable] + def params: immutable.Seq[SortVariable] def sort: Sort @@ -47,21 +49,21 @@ trait SortDeclaration extends Declaration { } object SortDeclaration { - def unapply(arg: SortDeclaration): Option[(Seq[SortVariable], Sort, Attributes)] = + def unapply(arg: SortDeclaration): Option[(immutable.Seq[SortVariable], Sort, Attributes)] = Some(arg.params, arg.sort, arg.att) } trait HookSortDeclaration extends SortDeclaration {} object HookSortDeclaration { - def unapply(arg: HookSortDeclaration): Option[(Seq[SortVariable], Sort, Attributes)] = + def unapply(arg: HookSortDeclaration): Option[(immutable.Seq[SortVariable], Sort, Attributes)] = Some(arg.params, arg.sort, arg.att) } trait SymbolDeclaration extends Declaration { def symbol: Symbol - def argSorts: Seq[Sort] + def argSorts: immutable.Seq[Sort] def returnSort: Sort @@ -69,21 +71,21 @@ trait SymbolDeclaration extends Declaration { } object SymbolDeclaration { - def unapply(arg: SymbolDeclaration): Option[(Symbol, Seq[Sort], Sort, Attributes)] = + def unapply(arg: SymbolDeclaration): Option[(Symbol, immutable.Seq[Sort], Sort, Attributes)] = Some(arg.symbol, arg.argSorts, arg.returnSort, arg.att) } trait HookSymbolDeclaration extends SymbolDeclaration {} object HookSymbolDeclaration { - def unapply(arg: HookSymbolDeclaration): Option[(Symbol, Seq[Sort], Sort, Attributes)] = + def unapply(arg: HookSymbolDeclaration): Option[(Symbol, immutable.Seq[Sort], Sort, Attributes)] = Some(arg.symbol, arg.argSorts, arg.returnSort, arg.att) } trait AliasDeclaration extends Declaration { def alias: Alias - def argSorts: Seq[Sort] + def argSorts: immutable.Seq[Sort] def returnSort: Sort @@ -97,12 +99,12 @@ trait AliasDeclaration extends Declaration { object AliasDeclaration { def unapply( arg: AliasDeclaration - ): Option[(Alias, Seq[Sort], Sort, Pattern, Pattern, Attributes)] = + ): Option[(Alias, immutable.Seq[Sort], Sort, Pattern, Pattern, Attributes)] = Some(arg.alias, arg.argSorts, arg.returnSort, arg.leftPattern, arg.rightPattern, arg.att) } trait AxiomDeclaration extends Declaration { - def params: Seq[SortVariable] + def params: immutable.Seq[SortVariable] def pattern: Pattern @@ -112,16 +114,16 @@ trait AxiomDeclaration extends Declaration { trait ClaimDeclaration extends AxiomDeclaration {} object AxiomDeclaration { - def unapply(arg: AxiomDeclaration): Option[(Seq[SortVariable], Pattern, Attributes)] = + def unapply(arg: AxiomDeclaration): Option[(immutable.Seq[SortVariable], Pattern, Attributes)] = Some(arg.params, arg.pattern, arg.att) } trait Attributes { - def patterns: Seq[Pattern] + def patterns: immutable.Seq[Pattern] } object Attributes { - def unapply(arg: Attributes): Option[Seq[Pattern]] = Some(arg.patterns) + def unapply(arg: Attributes): Option[immutable.Seq[Pattern]] = Some(arg.patterns) } trait Pattern extends Comparable[Pattern] { @@ -213,14 +215,15 @@ trait SetVariable extends Variable {} trait Application extends Pattern { def head: SymbolOrAlias - def args: Seq[Pattern] + def args: immutable.Seq[Pattern] } object Application { import scala.math.Ordering.Implicits._ - def unapply(arg: Application): Option[(SymbolOrAlias, Seq[Pattern])] = Some(arg.head, arg.args) + def unapply(arg: Application): Option[(SymbolOrAlias, immutable.Seq[Pattern])] = + Some(arg.head, arg.args) implicit val ord: Ordering[Application] = Ordering.by(unapply) } @@ -248,14 +251,14 @@ object Bottom { trait And extends Pattern { def s: Sort - def args: Seq[Pattern] + def args: immutable.Seq[Pattern] } object And { import scala.math.Ordering.Implicits._ - def unapply(arg: And): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args) + def unapply(arg: And): Option[(Sort, immutable.Seq[Pattern])] = Some(arg.s, arg.args) implicit val ord: Ordering[And] = Ordering.by(unapply) } @@ -263,14 +266,14 @@ object And { trait Or extends Pattern { def s: Sort - def args: Seq[Pattern] + def args: immutable.Seq[Pattern] } object Or { import scala.math.Ordering.Implicits._ - def unapply(arg: Or): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args) + def unapply(arg: Or): Option[(Sort, immutable.Seq[Pattern])] = Some(arg.s, arg.args) implicit val ord: Ordering[Or] = Ordering.by(unapply) } @@ -384,7 +387,7 @@ object Floor { trait GeneralizedRewrite { def sort: Sort - def getLeftHandSide: Seq[Pattern] + def getLeftHandSide: immutable.Seq[Pattern] def getRightHandSide: Pattern } @@ -403,7 +406,7 @@ trait Rewrites extends Pattern with GeneralizedRewrite { def _2: Pattern - def getLeftHandSide: Seq[Pattern] = Seq(_1) + def getLeftHandSide: immutable.Seq[Pattern] = immutable.Seq(_1) def getRightHandSide: Pattern = _2 } @@ -426,7 +429,7 @@ trait Equals extends Pattern with GeneralizedRewrite { def _2: Pattern - def getLeftHandSide: Seq[Pattern] = _1 match { + def getLeftHandSide: immutable.Seq[Pattern] = _1 match { case Application(_, ps) => ps } @@ -560,14 +563,14 @@ object SortVariable { trait CompoundSort extends Sort { def ctr: String // sort constructor - def params: Seq[Sort] // sort parameters + def params: immutable.Seq[Sort] // sort parameters } object CompoundSort { import scala.math.Ordering.Implicits._ - def unapply(arg: CompoundSort): Option[(String, Seq[Sort])] = Some(arg.ctr, arg.params) + def unapply(arg: CompoundSort): Option[(String, immutable.Seq[Sort])] = Some(arg.ctr, arg.params) implicit val ord: Ordering[CompoundSort] = Ordering.by(unapply) } @@ -579,14 +582,14 @@ object CompoundSort { trait SymbolOrAlias { def ctr: String - def params: Seq[Sort] + def params: immutable.Seq[Sort] } object SymbolOrAlias { import scala.math.Ordering.Implicits._ - def unapply(arg: SymbolOrAlias): Option[(String, Seq[Sort])] = + def unapply(arg: SymbolOrAlias): Option[(String, immutable.Seq[Sort])] = Some(arg.ctr, arg.params) implicit val ord: Ordering[SymbolOrAlias] = Ordering.by(unapply) @@ -595,61 +598,73 @@ object SymbolOrAlias { trait Symbol extends SymbolOrAlias object Symbol { - def unapply(arg: Symbol): Option[(String, Seq[Sort])] = Some(arg.ctr, arg.params) + def unapply(arg: Symbol): Option[(String, immutable.Seq[Sort])] = Some(arg.ctr, arg.params) } trait Alias extends SymbolOrAlias object Alias { - def unapply(arg: Alias): Option[(String, Seq[Sort])] = Some(arg.ctr, arg.params) + def unapply(arg: Alias): Option[(String, immutable.Seq[Sort])] = Some(arg.ctr, arg.params) } trait Builders { - def Definition(att: Attributes, modules: Seq[Module]): Definition + def Definition(att: Attributes, modules: immutable.Seq[Module]): Definition - def Module(name: String, sens: Seq[Declaration], att: Attributes): Module + def Module(name: String, sens: immutable.Seq[Declaration], att: Attributes): Module def Import(name: String, att: Attributes): Declaration - def SortDeclaration(params: Seq[SortVariable], sort: Sort, att: Attributes): Declaration + def SortDeclaration(params: immutable.Seq[SortVariable], sort: Sort, att: Attributes): Declaration - def HookSortDeclaration(params: Seq[SortVariable], sort: Sort, att: Attributes): Declaration + def HookSortDeclaration( + params: immutable.Seq[SortVariable], + sort: Sort, + att: Attributes + ): Declaration def SymbolDeclaration( symbol: Symbol, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, att: Attributes ): Declaration def HookSymbolDeclaration( symbol: Symbol, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, att: Attributes ): Declaration def AliasDeclaration( alias: Alias, - argSorts: Seq[Sort], + argSorts: immutable.Seq[Sort], returnSort: Sort, leftPattern: Pattern, rightPattern: Pattern, att: Attributes ): Declaration - def AxiomDeclaration(params: Seq[SortVariable], pattern: Pattern, att: Attributes): Declaration + def AxiomDeclaration( + params: immutable.Seq[SortVariable], + pattern: Pattern, + att: Attributes + ): Declaration - def ClaimDeclaration(params: Seq[SortVariable], pattern: Pattern, att: Attributes): Declaration + def ClaimDeclaration( + params: immutable.Seq[SortVariable], + pattern: Pattern, + att: Attributes + ): Declaration - def Attributes(att: Seq[Pattern]): Attributes + def Attributes(att: immutable.Seq[Pattern]): Attributes def Variable(name: String, sort: Sort): Variable def SetVariable(name: String, sort: Sort): SetVariable - def Application(head: SymbolOrAlias, args: Seq[Pattern]): Pattern + def Application(head: SymbolOrAlias, args: immutable.Seq[Pattern]): Pattern def Top(s: Sort): Pattern @@ -657,11 +672,11 @@ trait Builders { def And(s: Sort, _1: Pattern, _2: Pattern): Pattern - def And(s: Sort, args: Seq[Pattern]): Pattern + def And(s: Sort, args: immutable.Seq[Pattern]): Pattern def Or(s: Sort, _1: Pattern, _2: Pattern): Pattern - def Or(s: Sort, args: Seq[Pattern]): Pattern + def Or(s: Sort, args: immutable.Seq[Pattern]): Pattern def Not(s: Sort, _1: Pattern): Pattern @@ -693,15 +708,15 @@ trait Builders { def SortVariable(name: String): SortVariable - def CompoundSort(ctr: String, params: Seq[Sort]): CompoundSort + def CompoundSort(ctr: String, params: immutable.Seq[Sort]): CompoundSort - def SymbolOrAlias(ctr: String, params: Seq[Sort]): SymbolOrAlias + def SymbolOrAlias(ctr: String, params: immutable.Seq[Sort]): SymbolOrAlias - def Symbol(str: String, params: Seq[Sort]): Symbol + def Symbol(str: String, params: immutable.Seq[Sort]): Symbol - def Alias(str: String, params: Seq[Sort]): Alias + def Alias(str: String, params: immutable.Seq[Sort]): Alias - def LeftAssoc(ctr: (Pattern, Pattern) => Pattern, ps: Seq[Pattern]): Pattern + def LeftAssoc(ctr: (Pattern, Pattern) => Pattern, ps: immutable.Seq[Pattern]): Pattern - def RightAssoc(ctr: (Pattern, Pattern) => Pattern, ps: Seq[Pattern]): Pattern + def RightAssoc(ctr: (Pattern, Pattern) => Pattern, ps: immutable.Seq[Pattern]): Pattern } diff --git a/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala b/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala index f1a534fdd6..16f953236d 100644 --- a/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala +++ b/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala @@ -14,6 +14,7 @@ import com.runtimeverification.k.kore.Sort import com.runtimeverification.k.kore.SortVariable import com.runtimeverification.k.kore.Symbol import com.runtimeverification.k.kore.Variable +import scala.collection.immutable; /** Parsing error exception. */ case class ParseError(msg: String) extends Exception(msg) { @@ -166,7 +167,7 @@ class TextToKore(b: Builders = DefaultBuilders) { // Modules = // // | Module Modules - // private def parseModules(modules: Seq[Module]): Seq[Module] = { + // private def parseModules(modules: immutable.Seq[Module]): immutable.Seq[Module] = { // if (scanner.isEOF()) modules // else { // val mod = parseModule() @@ -178,14 +179,14 @@ class TextToKore(b: Builders = DefaultBuilders) { private def parseModule(): kore.Module = { consumeWithLeadingWhitespaces("module") val name = parseId(parsingLevel = objt) - val decls = parseDeclarations(Seq()).reverse + val decls = parseDeclarations(immutable.Seq()).reverse consumeWithLeadingWhitespaces("endmodule") val att = parseAttributes() b.Module(name, decls, att) } - private def parseModules(): Seq[kore.Module] = { - var ms = Seq.empty[kore.Module] + private def parseModules(): immutable.Seq[kore.Module] = { + var ms = immutable.Seq.empty[kore.Module] while (!scanner.isEOF()) { val leading_char = scanner.nextWithSkippingWhitespaces() if (leading_char == 'm') { // a module starts @@ -205,7 +206,7 @@ class TextToKore(b: Builders = DefaultBuilders) { // | alias Alias ( SortList ) : Sort Attributes // | axiom { SortVariableList } Axiom // | import Id Attributes - private def parseDeclarations(decls: Seq[Declaration]): Seq[Declaration] = { + private def parseDeclarations(decls: immutable.Seq[Declaration]): immutable.Seq[Declaration] = { val c1 = scanner.nextWithSkippingWhitespaces() if (c1 == 'e') { // endmodule scanner.putback('e') @@ -531,7 +532,7 @@ class TextToKore(b: Builders = DefaultBuilders) { parseList(() => parseSort(parsingLevel = previousParsingLevel), ',', '}') consumeWithLeadingWhitespaces("}") (p1: Pattern, p2: Pattern) => - b.Application(b.SymbolOrAlias(id, params), Seq(p1, p2)) + b.Application(b.SymbolOrAlias(id, params), immutable.Seq(p1, p2)) } consumeWithLeadingWhitespaces("(") val args = parseList(() => parsePattern(), ',', ')') @@ -552,7 +553,7 @@ class TextToKore(b: Builders = DefaultBuilders) { parseList(() => parseSort(parsingLevel = previousParsingLevel), ',', '}') consumeWithLeadingWhitespaces("}") (p1: Pattern, p2: Pattern) => - b.Application(b.SymbolOrAlias(id, params), Seq(p1, p2)) + b.Application(b.SymbolOrAlias(id, params), immutable.Seq(p1, p2)) } consumeWithLeadingWhitespaces("(") val args = parseList(() => parsePattern(), ',', ')') @@ -581,7 +582,7 @@ class TextToKore(b: Builders = DefaultBuilders) { // consumeWithLeadingWhitespaces(")") // b.DomainValue(sortStr, valueStr) case (err1, err2) => - val known = Seq( + val known = immutable.Seq( "\\top", "\\bottom", "\\and", @@ -670,7 +671,7 @@ class TextToKore(b: Builders = DefaultBuilders) { scanner.nextWithSkippingWhitespaces() match { case '{' => if (previousParsingLevel == meta) { // name is a meta-level id - val metalevelSorts = Seq( + val metalevelSorts = immutable.Seq( "#Char", "#CharList", "#String", @@ -685,7 +686,7 @@ class TextToKore(b: Builders = DefaultBuilders) { ) if (metalevelSorts.contains(name)) { consumeWithLeadingWhitespaces("}") // no params - b.CompoundSort(name, Seq.empty[Sort]) + b.CompoundSort(name, immutable.Seq.empty[Sort]) } else { throw error("", name) // not a valid meta-level sort } @@ -762,7 +763,7 @@ class TextToKore(b: Builders = DefaultBuilders) { if (parsingLevel == both || parsingLevel == objt) { // expect both levels or only object-level val id = loop(new StringBuilder(c.toString)) - val kwds = Seq("module", "endmodule", "sort", "symbol", "alias", "axiom") + val kwds = immutable.Seq("module", "endmodule", "sort", "symbol", "alias", "axiom") if (kwds.contains(id)) { throw error(" should not be keywords", id) } @@ -804,10 +805,10 @@ class TextToKore(b: Builders = DefaultBuilders) { // | Elem List2 // List2 = // // | Elem List2 - private def parseList[T](parseElem: () => T, sep: Char, endsWith: Char): Seq[T] = { + private def parseList[T](parseElem: () => T, sep: Char, endsWith: Char): immutable.Seq[T] = { assert(sep != endsWith) - def parseList2(lst: Seq[T]): Seq[T] = + def parseList2(lst: immutable.Seq[T]): immutable.Seq[T] = scanner.nextWithSkippingWhitespaces() match { case c if c == endsWith => scanner.putback(c) @@ -821,11 +822,11 @@ class TextToKore(b: Builders = DefaultBuilders) { scanner.nextWithSkippingWhitespaces() match { case c if c == endsWith => scanner.putback(c) - Seq() + immutable.Seq() case c => scanner.putback(c) val elem = parseElem() - parseList2(Seq(elem)) + parseList2(immutable.Seq(elem)) } } diff --git a/src/test/scala/org/kframework/parser/kore/InterfaceTest.scala b/src/test/scala/org/kframework/parser/kore/InterfaceTest.scala index 068e7c8e56..c940f77caf 100644 --- a/src/test/scala/org/kframework/parser/kore/InterfaceTest.scala +++ b/src/test/scala/org/kframework/parser/kore/InterfaceTest.scala @@ -6,13 +6,14 @@ import com.runtimeverification.k.kore.implementation.{ DefaultBuilders => b } import com.runtimeverification.k.kore.Pattern import org.junit.Assert import org.junit.Test +import scala.collection.immutable class InterfaceTest { @Test def patternOrdering(): Unit = { - val sortA = b.CompoundSort("A", Seq()) - val sortB = b.CompoundSort("B", Seq()) - val sortC = b.CompoundSort("C", Seq()) + val sortA = b.CompoundSort("A", immutable.Seq()) + val sortB = b.CompoundSort("B", immutable.Seq()) + val sortC = b.CompoundSort("C", immutable.Seq()) val dvA = b.DomainValue(sortA, "A") val dvB = b.DomainValue(sortB, "B") @@ -22,13 +23,13 @@ class InterfaceTest { val varB = b.Variable("B", sortB) val varC = b.Variable("C", sortC) - val symbolA = b.SymbolOrAlias("A", Seq()) - val symbolB = b.SymbolOrAlias("B", Seq()) - val symbolC = b.SymbolOrAlias("C", Seq()) + val symbolA = b.SymbolOrAlias("A", immutable.Seq()) + val symbolB = b.SymbolOrAlias("B", immutable.Seq()) + val symbolC = b.SymbolOrAlias("C", immutable.Seq()) - val appA = b.Application(symbolA, Seq(dvA, varA)) - val appB = b.Application(symbolB, Seq(dvB, varB)) - val appC = b.Application(symbolC, Seq(dvC, varC)) + val appA = b.Application(symbolA, immutable.Seq(dvA, varA)) + val appB = b.Application(symbolB, immutable.Seq(dvB, varB)) + val appC = b.Application(symbolC, immutable.Seq(dvC, varC)) val topA = b.Top(sortA) val topB = b.Top(sortB) @@ -38,13 +39,13 @@ class InterfaceTest { val bottomB = b.Bottom(sortB) val bottomC = b.Bottom(sortC) - val andA = b.And(sortA, Seq(topA, bottomA)) - val andB = b.And(sortB, Seq(topB, bottomB)) - val andC = b.And(sortC, Seq(topC, bottomC)) + val andA = b.And(sortA, immutable.Seq(topA, bottomA)) + val andB = b.And(sortB, immutable.Seq(topB, bottomB)) + val andC = b.And(sortC, immutable.Seq(topC, bottomC)) - val orA = b.Or(sortA, Seq(topA, bottomA)) - val orB = b.Or(sortB, Seq(topB, bottomB)) - val orC = b.Or(sortC, Seq(topC, bottomC)) + val orA = b.Or(sortA, immutable.Seq(topA, bottomA)) + val orB = b.Or(sortB, immutable.Seq(topB, bottomB)) + val orC = b.Or(sortC, immutable.Seq(topC, bottomC)) val notA = b.Not(sortA, topA) val notB = b.Not(sortB, topB) diff --git a/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala b/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala index 1a2375e03c..350e5e6cf2 100644 --- a/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala +++ b/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala @@ -6,6 +6,7 @@ import com.runtimeverification.k.kore.implementation.{ DefaultBuilders => b } import com.runtimeverification.k.kore.parser.TextToKore import org.junit.Assert import org.junit.Test +import scala.collection.immutable class TextToKoreTest { @Test def testMultiOr(): Unit = { @@ -13,9 +14,12 @@ class TextToKoreTest { "\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\"))" val parser = new TextToKore() val ast1 = parser.parsePattern(kore1) - val int = b.CompoundSort("SortInt", Seq()) + val int = b.CompoundSort("SortInt", immutable.Seq()) Assert.assertEquals( - b.Or(int, Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3"))), + b.Or( + int, + immutable.Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3")) + ), ast1 ) } @@ -25,24 +29,27 @@ class TextToKoreTest { "\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\"))" val parser = new TextToKore() val ast1 = parser.parsePattern(kore1) - val int = b.CompoundSort("SortInt", Seq()) + val int = b.CompoundSort("SortInt", immutable.Seq()) Assert.assertEquals( - b.And(int, Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3"))), + b.And( + int, + immutable.Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3")) + ), ast1 ) } @Test def testAssocApplication(): Unit = { val parser = new TextToKore() - val int = b.CompoundSort("SortInt", Seq()) + val int = b.CompoundSort("SortInt", immutable.Seq()) val koreLeft = "\\left-assoc{}(Lbl'Unds'Map'Unds{}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"1\")))" val astLeft = parser.parsePattern(koreLeft) Assert.assertEquals( b.Application( - b.SymbolOrAlias("Lbl'Unds'Map'Unds", Seq()), - Seq(b.DomainValue(int, "1"), b.DomainValue(int, "1")) + b.SymbolOrAlias("Lbl'Unds'Map'Unds", immutable.Seq()), + immutable.Seq(b.DomainValue(int, "1"), b.DomainValue(int, "1")) ), astLeft ) @@ -52,8 +59,8 @@ class TextToKoreTest { val astRight = parser.parsePattern(koreRight) Assert.assertEquals( b.Application( - b.SymbolOrAlias("Lbl'Unds'Map'Unds", Seq()), - Seq(b.DomainValue(int, "1"), b.DomainValue(int, "1")) + b.SymbolOrAlias("Lbl'Unds'Map'Unds", immutable.Seq()), + immutable.Seq(b.DomainValue(int, "1"), b.DomainValue(int, "1")) ), astRight ) From 2890a0d6af2f6964a9a58e7ac69e8dec1894bf39 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 9 Apr 2024 09:17:25 -0400 Subject: [PATCH 2/3] Update to Scala 2.13.13 --- pom.xml | 4 ++-- .../com/runtimeverification/k/kore/parser/TextToKore.scala | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pom.xml b/pom.xml index 9a1168f67a..870dc54fae 100644 --- a/pom.xml +++ b/pom.xml @@ -65,8 +65,8 @@ master 17 - 2.12 - 18 + 2.13 + 13 ${scala.majorVersion}.${scala.minorVersion} 2.41.1 1.18.1 diff --git a/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala b/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala index 16f953236d..c4ab503a40 100644 --- a/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala +++ b/src/main/scala/com/runtimeverification/k/kore/parser/TextToKore.scala @@ -19,7 +19,7 @@ import scala.collection.immutable; /** Parsing error exception. */ case class ParseError(msg: String) extends Exception(msg) { // ParseError.msg eq Exception.detailMessage, i.e., msg() == getMessage() - def this(message: String, cause: Throwable) { + def this(message: String, cause: Throwable) = { this(message) initCause(cause) } From 973aa1757461df4f26960de1a5fd944b85cc20cb Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 9 Apr 2024 13:23:16 +0000 Subject: [PATCH 3/3] Set Version: 0.3.3 --- package/version | 2 +- pom.xml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index d15723fbe8..1c09c74e22 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.2 +0.3.3 diff --git a/pom.xml b/pom.xml index 870dc54fae..a4e1c3e209 100644 --- a/pom.xml +++ b/pom.xml @@ -6,7 +6,7 @@ com.runtimeverification.k scala-kore jar - 0.3.2 + 0.3.3 Scala support for KORE