Remove variadic functions from Constructors.scala

runtimeverification · Dec 11, 2023 · aba2d44 · aba2d44
1 parent d4ae252
commit aba2d44
Show file tree

Hide file tree

Showing 9 changed files with 77 additions and 61 deletions.
diff --git a/kore/src/main/scala/org/kframework/compile/AssocCommToAssoc.scala b/kore/src/main/scala/org/kframework/compile/AssocCommToAssoc.scala
@@ -1,7 +1,6 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.compile
 
-import collection.JavaConverters._
 import org.kframework.attributes.Att
 import org.kframework.definition.Module
 import org.kframework.definition.Rule
@@ -11,7 +10,7 @@ import org.kframework.kore.KORE.KApply
 import org.kframework.kore.KORE.KRewrite
 import org.kframework.kore.SortedADT.SortedKVariable
 import org.kframework.Collections._
-import scala.collection.Set
+import scala.collection.JavaConverters._
 
 /**
  * Compiler pass for merging the rules as expected by FastRuleMatcher
@@ -59,7 +58,7 @@ class AssocCommToAssoc extends Function[Module, Module] {
     case Unapply.KApply(label: KLabel, children: List[K]) if isAssocComm(label) =>
       convert(label, children)
     case Unapply.KApply(label: KLabel, children: List[K]) =>
-      crossProduct(children.map(apply)).map(KApply(label, _: _*))
+      crossProduct(children.map(apply)).map(KApply(label, _))
     case Unapply.KRewrite(left: K, right: K) =>
       apply(left).map(KRewrite(_, right, Att.empty))
     case _ =>
@@ -103,7 +102,7 @@ class AssocCommToAssoc extends Function[Module, Module] {
         elements.toList.permutations.toList
     }
 
-    convertedChildren.flatMap(cs => crossProduct(cs.map(apply))).map(KApply(label, _: _*))
+    convertedChildren.flatMap(cs => crossProduct(cs.map(apply))).map(KApply(label, _))
   }
 
   private def computeSubstitution(label: KLabel, children: List[K])(implicit
@@ -124,14 +123,14 @@ class AssocCommToAssoc extends Function[Module, Module] {
 
     frameOption match {
       case Some(v: KVariable) if v.name.startsWith("_DotVar") || v.att.contains(Att.ANONYMOUS) =>
-        Map(v -> KApply(label, (0 to elements.size).map(dotVariable(opSort, _)): _*))
+        Map(v -> KApply(label, (0 to elements.size).map(dotVariable(opSort, _))))
       case _ => Map()
     }
   }
 
   private def substituteFrame(k: K, name: String, substitute: K): K = k match {
     case Unapply.KApply(label: KLabel, children: List[K]) =>
-      KApply(label, children.map(substituteFrame(_, name, substitute)): _*)
+      KApply(label, children.map(substituteFrame(_, name, substitute)))
     case Unapply.KVariable(`name`) => substitute
     case _: K                      => k
   }

diff --git a/kore/src/main/scala/org/kframework/compile/MergeRules.scala b/kore/src/main/scala/org/kframework/compile/MergeRules.scala
@@ -1,24 +1,16 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.compile
 
-import collection._
 import org.kframework.attributes.Att
 import org.kframework.builtin.KLabels
 import org.kframework.builtin.Sorts
 import org.kframework.definition.Module
-import org.kframework.definition.ModuleTransformer
 import org.kframework.definition.Rule
 import org.kframework.kore._
-import org.kframework.kore.Assoc
-import org.kframework.kore.K
-import org.kframework.kore.KApply
-import org.kframework.kore.KLabel
 import org.kframework.kore.KORE.KApply
 import org.kframework.kore.KORE.KLabel
 import org.kframework.kore.KORE.KToken
-import org.kframework.kore.KORE.Sort
-import org.kframework.kore.KVariable
-import org.kframework.kore.Unapply
+import scala.collection._
 import scala.collection.immutable.Iterable
 import scala.collection.JavaConverters._
 
@@ -47,7 +39,7 @@ class MergeRules(val automatonAttribute: Att.Key, filterAttribute: Att.Key)
       val newBody = pushDisjunction(rulesToMerge.map { r =>
         (
           convertKRewriteToKApply(r.body),
-          KApply(isRulePredicate, KToken(r.hashCode.toString, Sorts.K, Att.empty))
+          KApply(isRulePredicate, KToken(r.hashCode.toString, Sorts.K, Att.empty)).asInstanceOf[K]
         )
       })(m)
       val automatonRule = Rule(newBody, TrueToken, TrueToken, Att.empty.add(automatonAttribute))
@@ -58,7 +50,7 @@ class MergeRules(val automatonAttribute: Att.Key, filterAttribute: Att.Key)
   }
 
   private def convertKRewriteToKApply(k: K): K = k match {
-    case Unapply.KApply(label, children) => KApply(label, children.map(convertKRewriteToKApply): _*)
+    case Unapply.KApply(label, children) => KApply(label, children.map(convertKRewriteToKApply))
     case Unapply.KRewrite(l, r)          => KApply(KLabels.KREWRITE, l, r)
     case other                           => other
   }
@@ -67,7 +59,7 @@ class MergeRules(val automatonAttribute: Att.Key, filterAttribute: Att.Key)
     if (ks.size == 1) {
       ks.head
     } else {
-      KApply(or, ks: _*)
+      KApply(or, ks)
     }
 
   private def pushDisjunction(terms: Set[(K, K)])(implicit m: Module): K = {
@@ -114,7 +106,7 @@ class MergeRules(val automatonAttribute: Att.Key, filterAttribute: Att.Key)
             .map(pushDisjunction)
         val rulePs = ks.map(_._2) toSeq
 
-        (KApply(klabel, childrenDisjunctionsOfklabel: _*), KApply(or, rulePs: _*))
+        (KApply(klabel, childrenDisjunctionsOfklabel), KApply(or, rulePs))
       }
 
     val disjunctionOfVarKApplies: Iterable[(K, K)] = termsWithoutRewrites.collect {

diff --git a/kore/src/main/scala/org/kframework/compile/NormalizeAssoc.scala b/kore/src/main/scala/org/kframework/compile/NormalizeAssoc.scala
@@ -31,17 +31,17 @@ class NormalizeAssoc(c: Constructors) extends ((Module, Sentence) => Sentence) {
           KRewrite(
             KApply(
               opKLabel,
-              KList(flatten(RewriteToTop.toLeft(k), opKLabel, unitKLabel).map(apply): _*),
+              KList(flatten(RewriteToTop.toLeft(k), opKLabel, unitKLabel).map(apply)),
               kApply.att
             ),
             RewriteToTop.toRight(k),
             Att.empty
           )
         } else {
-          KApply(opKLabel, KList(flattenChildren.map(apply): _*), kApply.att)
+          KApply(opKLabel, KList(flattenChildren.map(apply)), kApply.att)
         }
       } else {
-        KApply(kApply.klabel, KList(immutable(kApply.klist.items).map(apply): _*), kApply.att)
+        KApply(kApply.klabel, KList(immutable(kApply.klist.items).map(apply)), kApply.att)
       }
     case kRewrite: KRewrite => KRewrite(apply(kRewrite.left), kRewrite.right, kRewrite.att)
     case _                  => k

diff --git a/kore/src/main/scala/org/kframework/compile/RewriteToTop.scala b/kore/src/main/scala/org/kframework/compile/RewriteToTop.scala
@@ -87,7 +87,7 @@ object RewriteToTop {
             "Injection compaction error: found nested injections with incompatible sorts"
           )
         }
-        KApply(KLabel("inj", List(sortInnerIn, sortOuterOut): _*), kappInner.klist, kapp.att)
+        KApply(KLabel("inj", List(sortInnerIn, sortOuterOut)), kappInner.klist, kapp.att)
       } else {
         kapp
       }

diff --git a/kore/src/main/scala/org/kframework/kore/Constructors.scala b/kore/src/main/scala/org/kframework/kore/Constructors.scala
@@ -5,8 +5,8 @@ import org.kframework.attributes._
 import scala.collection.JavaConverters._
 
 trait Constructors {
-  def KLabel(name: String, params: Sort*): KLabel
-  def Sort(name: String, params: Sort*): Sort
+  def KLabel(name: String, params: Seq[Sort]): KLabel
+  def Sort(name: String, params: Seq[Sort]): Sort
   def KList(items: java.util.List[K]): KList
   def KToken(s: String, sort: Sort, att: Att): KToken
   def KApply(klabel: KLabel, klist: KList, att: Att): KApply
@@ -16,13 +16,55 @@ trait Constructors {
   def KAs(pattern: K, alias: K, att: Att): KAs
   def InjectedKLabel(klabel: KLabel, att: Att): InjectedKLabel
 
-  // default methods:
-  @annotation.varargs
-  def KList(items: K*): KList = KList(items.asJava)
-  @annotation.varargs
-  def KApply(klabel: KLabel, items: K*): KApply = KApply(klabel, KList(items.asJava), Att.empty)
-  @annotation.varargs
-  def KSequence(list: K*): KSequence     = KSequence(list.toList.asJava, Att.empty)
+  // Unfortunately, IntelliJ struggles to resolve variadic functions,
+  // so we instead provide specialized functions for 0-4 elements below
+  def KLabel(name: String, params: Array[Sort]): KLabel        = KLabel(name, params.toSeq)
+  def KLabel(name: String): KLabel                             = KLabel(name, Seq())
+  def KLabel(name: String, param: Sort): KLabel                = KLabel(name, Seq(param))
+  def KLabel(name: String, param1: Sort, param2: Sort): KLabel = KLabel(name, Seq(param1, param2))
+  def KLabel(name: String, param1: Sort, param2: Sort, param3: Sort): KLabel =
+    KLabel(name, Seq(param1, param2, param3))
+  def KLabel(name: String, param1: Sort, param2: Sort, param3: Sort, param4: Sort): KLabel =
+    KLabel(name, Seq(param1, param2, param3, param4))
+
+  def Sort(name: String, params: Array[Sort]): Sort        = Sort(name, params.toSeq)
+  def Sort(name: String): Sort                             = Sort(name, Seq())
+  def Sort(name: String, param: Sort): Sort                = Sort(name, Seq(param))
+  def Sort(name: String, param1: Sort, param2: Sort): Sort = Sort(name, Seq(param1, param2))
+  def Sort(name: String, param1: Sort, param2: Sort, param3: Sort): Sort =
+    Sort(name, Seq(param1, param2, param3))
+  def Sort(name: String, param1: Sort, param2: Sort, param3: Sort, param4: Sort): Sort =
+    Sort(name, Seq(param1, param2, param3, param4))
+
+  def KList(items: Array[K]): KList                        = KList(items.toList.asJava)
+  def KList(items: Seq[K]): KList                          = KList(items.asJava)
+  def KList(): KList                                       = KList(Seq())
+  def KList(item: K): KList                                = KList(Seq(item))
+  def KList(item1: K, item2: K): KList                     = KList(Seq(item1, item2))
+  def KList(item1: K, item2: K, item3: K): KList           = KList(Seq(item1, item2, item3))
+  def KList(item1: K, item2: K, item3: K, item4: K): KList = KList(Seq(item1, item2, item3, item4))
+
+  def KApply(klabel: KLabel, items: Array[K]): KApply =
+    KApply(klabel, KList(items.toList.asJava), Att.empty)
+  def KApply(klabel: KLabel, items: Seq[K]): KApply = KApply(klabel, KList(items.asJava), Att.empty)
+  def KApply(klabel: KLabel): KApply                = KApply(klabel, Seq())
+  def KApply(klabel: KLabel, item: K): KApply       = KApply(klabel, Seq(item))
+  def KApply(klabel: KLabel, item1: K, item2: K): KApply = KApply(klabel, Seq(item1, item2))
+  def KApply(klabel: KLabel, item1: K, item2: K, item3: K): KApply =
+    KApply(klabel, Seq(item1, item2, item3))
+  def KApply(klabel: KLabel, item1: K, item2: K, item3: K, item4: K): KApply =
+    KApply(klabel, Seq(item1, item2, item3, item4))
+
+  def KSequence(list: Array[K]): KSequence               = KSequence(list.toList.asJava, Att.empty)
+  def KSequence(list: Seq[K]): KSequence                 = KSequence(list.toList.asJava, Att.empty)
+  def KSequence(): KSequence                             = KSequence(Seq())
+  def KSequence(item: K): KSequence                      = KSequence(Seq(item))
+  def KSequence(item1: K, item2: K): KSequence           = KSequence(Seq(item1, item2))
+  def KSequence(item1: K, item2: K, item3: K): KSequence = KSequence(Seq(item1, item2, item3))
+  def KSequence(item1: K, item2: K, item3: K, item4: K): KSequence = KSequence(
+    Seq(item1, item2, item3, item4)
+  )
+
   def KVariable(name: String): KVariable = KVariable(name, Att.empty)
 
   def convert(l: KLabel): KLabel = l match {

diff --git a/kore/src/main/scala/org/kframework/kore/KORE.scala b/kore/src/main/scala/org/kframework/kore/KORE.scala
@@ -1,13 +1,10 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.kore
 
-import collection._
-import collection.JavaConverters._
 import org.kframework.attributes
 import org.kframework.attributes.Att
-import org.kframework.Collector
-import org.kframework.CombinerFromBuilder
-import scala.collection.mutable.ListBuffer
+import scala.collection._
+import scala.collection.JavaConverters._
 
 /**
  * Basic implementation of a Constructor of inner KORE classes. It can be used by either creating a
@@ -44,8 +41,7 @@ object KORE extends Constructors with ScalaSugared {
   //  def toKSequence: Collector[K, KSequence] =
   //    Collector(() => new CombinerFromBuilder(KSequence.newBuilder()))
 
-  @annotation.varargs
-  override def KLabel(name: String, params: Sort*): KLabel = ADT.KLabel(name, params: _*)
+  override def KLabel(name: String, params: Seq[Sort]): KLabel = ADT.KLabel(name, params: _*)
 
   override def KApply(klabel: KLabel, klist: KList, att: Att): KApply =
     ADT.KApply(klabel, klist, att)
@@ -55,8 +51,7 @@ object KORE extends Constructors with ScalaSugared {
 
   override def KVariable(name: String, att: Att): KVariable = ADT.KVariable(name, att)
 
-  @annotation.varargs
-  override def Sort(name: String, params: Sort*): Sort = ADT.Sort(name, params: _*)
+  override def Sort(name: String, params: Seq[Sort]): Sort = ADT.Sort(name, params: _*)
 
   def Sort(name: SortHead): Sort = {
     assert(name.params == 0)
@@ -81,7 +76,4 @@ object KORE extends Constructors with ScalaSugared {
     ADT.InjectedKLabel(klabel, att)
 
   def self = this
-
-  @annotation.varargs
-  override def KApply(klabel: KLabel, items: K*): KApply = KApply(klabel, KList(items.asJava), Att)
 }
diff --git a/kore/src/main/scala/org/kframework/kore/ScalaSugar.scala b/kore/src/main/scala/org/kframework/kore/ScalaSugar.scala
@@ -4,7 +4,6 @@ package org.kframework.kore
 import org.kframework.attributes.Att
 import org.kframework.builtin.KLabels
 import org.kframework.builtin.Sorts
-import org.kframework.kore
 import scala.collection.JavaConverters._
 
 trait ScalaSugared {
@@ -18,7 +17,7 @@ trait ScalaSugared {
   implicit def intToToken(n: Int): K    = KToken(n.toString, Sorts.Int, Att.empty)
 
   implicit class ApplicableKLabel(klabel: KLabel) {
-    def apply(l: K*): K = c.KApply(klabel, l: _*)
+    def apply(l: K*): K = c.KApply(klabel, l)
   }
 
   implicit class EnhancedK(k: K) {
@@ -34,8 +33,6 @@ trait ScalaSugared {
     def ||(other: K)  = KLabels.OR.apply(k, other)
   }
 
-  def KList(ks: Seq[K]): KList = c.KList(ks.asJava)
-
   def KApply(klabel: KLabel, ks: Seq[K], att: Att = Att.empty): KApply =
     c.KApply(klabel, c.KList(ks.asJava), att)
 }
diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
@@ -8,7 +8,6 @@ import org.kframework.builtin.Sorts
 import org.kframework.kore.ADT.KVariable
 import org.kframework.kore.Assoc
 import org.kframework.kore.KORE
-import org.kframework.kore.KVariable
 import org.kframework.parser.kore
 import org.kframework.utils.StringUtil
 import scala.collection.JavaConverters._
@@ -71,12 +70,12 @@ class KoreToK(sortAtt: Map[String, String]) {
       Sorts.K
     case kore.CompoundSort(ctr, params) =>
       assert(ctr.startsWith("Sort"))
-      KORE.Sort(ctr.substring(4), params.map(apply): _*);
+      KORE.Sort(ctr.substring(4), params.map(apply));
   }
 
   /** Returns a [[k.KLabel]] from [[kore.SymbolOrAlias]] */
   def apply(head: kore.SymbolOrAlias): k.KLabel =
-    KORE.KLabel(extractKLabel(head.ctr), head.params.map(p => apply(p)): _*)
+    KORE.KLabel(extractKLabel(head.ctr), head.params.map(p => apply(p)))
 
   private def extractKLabel(head: String): String =
     if (head.startsWith("Lbl")) {
@@ -123,9 +122,9 @@ class KoreToK(sortAtt: Map[String, String]) {
             case body => body
           }
         case "kseq" =>
-          KORE.KSequence(args.map(apply(_)): _*)
+          KORE.KSequence(args.map(apply(_)))
         case "append" =>
-          KORE.KSequence(args.map(apply(_)): _*)
+          KORE.KSequence(args.map(apply(_)))
         case "dotk" =>
           KORE.KSequence()
         case _ =>

diff --git a/kore/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala b/kore/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala
@@ -1,22 +1,17 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.unparser
 
-import collection._
-import java.util
 import org.kframework.attributes.Att
 import org.kframework.attributes.Location
 import org.kframework.attributes.Source
 import org.kframework.builtin.Sorts
 import org.kframework.definition._
 import org.kframework.kore._
-import org.kframework.kore.KApply
-import org.kframework.kore.KToken
-import org.kframework.kore.KVariable
 import org.kframework.parser._
-import org.kframework.utils.StringUtil
 import org.kframework.POSet
 import org.pcollections.ConsPStack
-import JavaConverters._
+import scala.collection._
+import scala.collection.JavaConverters._
 
 object KOREToTreeNodes {
 
@@ -74,7 +69,7 @@ object KOREToTreeNodes {
       else
         KToken(v.name, Sorts.KVariable, v.att)
     case t: KToken =>
-      val sort = Sort(t.sort.name, t.sort.params: _*)
+      val sort = Sort(t.sort.name, t.sort.params)
       KToken(t.s, sort, t.att)
     case s: KSequence =>
       upList(mod)(s.items.asScala).foldRight(KApply(KLabel("#EmptyK"), KList(), s.att))((k1, k2) =>