Merge branch 'develop' into _update-deps/runtimeverification/hs-backe…

…nd-booster

kernel/src/main/java/org/kframework/kil/ASTNode.java

@@ -15,8 +15,8 @@ public abstract class ASTNode implements Serializable, HasLocation {
   private static final long serialVersionUID = 1L;
 
   /**
-   * Used on any node for metadata also used on {@link Rule} and {@link Production} for the
-   * attribute list.
+   * Used on any node for metadata also used on {@link org.kframework.definition.Rule} and {@link
+   * Production} for the attribute list.
    */
   private Att att = Att.empty();
 
@@ -28,12 +28,7 @@ public ASTNode() {
     this(null, null);
   }
 
-  /**
-   * Constructor with specified location and filename.
-   *
-   * @param loc
-   * @param file
-   */
+  /** Constructor with specified location and filename. */
   public ASTNode(Location loc, Source source) {
     setLocation(loc);
     setSource(source);
@@ -48,11 +43,7 @@ public Location getLocation() {
     return location;
   }
 
-  /**
-   * Sets the location or removes it if appropriate.
-   *
-   * @param loc
-   */
+  /** Sets the location or removes it if appropriate. */
   public void setLocation(Location location) {
     this.location = location;
   }
@@ -66,11 +57,7 @@ public Source getSource() {
     return source;
   }
 
-  /**
-   * Sets the source or removes it if appropriate.
-   *
-   * @param file
-   */
+  /** Sets the source or removes it if appropriate. */
   public void setSource(Source source) {
     this.source = source;
   }

kernel/src/main/java/org/kframework/kil/Definition.java

@@ -7,11 +7,7 @@
 import java.util.List;
 import java.util.Map;
 
-/**
- * Represents a language definition. Includes contents from all {@code required}-d files.
- *
- * @see DefinitionLoader
- */
+/** Represents a language definition. Includes contents from all {@code required}-d files. */
 public class Definition extends ASTNode {
 
   private List<DefinitionItem> items;

kernel/src/main/java/org/kframework/kil/Production.java

@@ -9,7 +9,8 @@
 import org.kframework.utils.StringUtil;
 
 /**
- * A production. Any explicit attributes on the production are stored in {@link ASTNode#attributes}.
+ * A production. Any explicit attributes on the production are stored in {@link
+ * ASTNode#getAttributes()}.
  */
 public class Production extends ASTNode {
 

kernel/src/main/java/org/kframework/kompile/Kompile.java

@@ -201,7 +201,6 @@ public Kompile(
    * @param definitionFile
    * @param mainModuleName
    * @param mainProgramsModuleName
-   * @param programStartSymbol
    * @return
    */
   public CompiledDefinition run(

kernel/src/main/java/org/kframework/utils/Stopwatch.java

@@ -6,7 +6,6 @@
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 
-/** To use, access {@link #instance()} after calling {@link #init(GlobalOptions) init()}. */
 @RequestScoped
 public class Stopwatch {
   private final long start;

kore/src/main/java/org/kframework/utils/StringUtil.java

@@ -213,7 +213,7 @@ public static String unquoteKString(String str) {
    * \xFF Codepoints between 256 and 65535 are stored as \uFFFF Codepoints above 65536 are stored as
    * \u0010FFFF
    *
-   * @param value a Unicode codepoint
+   * @param codepoint a Unicode codepoint
    * @return representation of the codepoint as an escaped string
    */
   public static String getUnicodeEscape(int codepoint) {
@@ -503,7 +503,7 @@ public static String unescapeKoreKLabel(String str) {
    *
    * <p>Used by the KAST pretty printer.
    *
-   * @param str A string value corresponding to a KLabel.
+   * @param value A string value corresponding to a KLabel.
    * @return A string which can be parsed back by a KORE parser to reach the original KLabel.
    */
   public static String escapeKoreKLabel(String value) {

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
   }

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 {

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

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
       }

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,14 +16,85 @@ 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)
-  def KVariable(name: String): KVariable = KVariable(name, Att.empty)
+  // Unfortunately, IntelliJ struggles to resolve variadic functions,
+  // so we instead manually provide overloads for 0-5 elements below
+  final def KLabel(name: String, params: Array[Sort]): KLabel = KLabel(name, params.toSeq)
+  final def KLabel(name: String): KLabel                      = KLabel(name, Seq())
+  final def KLabel(name: String, param: Sort): KLabel         = KLabel(name, Seq(param))
+  final def KLabel(name: String, param1: Sort, param2: Sort): KLabel =
+    KLabel(name, Seq(param1, param2))
+  final def KLabel(name: String, param1: Sort, param2: Sort, param3: Sort): KLabel =
+    KLabel(name, Seq(param1, param2, param3))
+  final def KLabel(name: String, param1: Sort, param2: Sort, param3: Sort, param4: Sort): KLabel =
+    KLabel(name, Seq(param1, param2, param3, param4))
+  final def KLabel(
+      name: String,
+      param1: Sort,
+      param2: Sort,
+      param3: Sort,
+      param4: Sort,
+      param5: Sort
+  ): KLabel =
+    KLabel(name, Seq(param1, param2, param3, param4, param5))
+
+  final def Sort(name: String, params: Array[Sort]): Sort        = Sort(name, params.toSeq)
+  final def Sort(name: String): Sort                             = Sort(name, Seq())
+  final def Sort(name: String, param: Sort): Sort                = Sort(name, Seq(param))
+  final def Sort(name: String, param1: Sort, param2: Sort): Sort = Sort(name, Seq(param1, param2))
+  final def Sort(name: String, param1: Sort, param2: Sort, param3: Sort): Sort =
+    Sort(name, Seq(param1, param2, param3))
+  final def Sort(name: String, param1: Sort, param2: Sort, param3: Sort, param4: Sort): Sort =
+    Sort(name, Seq(param1, param2, param3, param4))
+  final def Sort(
+      name: String,
+      param1: Sort,
+      param2: Sort,
+      param3: Sort,
+      param4: Sort,
+      param5: Sort
+  ): Sort = Sort(name, Seq(param1, param2, param3, param4, param5))
+
+  final def KList(items: Array[K]): KList              = KList(items.toList.asJava)
+  final def KList(items: Seq[K]): KList                = KList(items.asJava)
+  final def KList(): KList                             = KList(Seq())
+  final def KList(item: K): KList                      = KList(Seq(item))
+  final def KList(item1: K, item2: K): KList           = KList(Seq(item1, item2))
+  final def KList(item1: K, item2: K, item3: K): KList = KList(Seq(item1, item2, item3))
+  final def KList(item1: K, item2: K, item3: K, item4: K): KList = KList(
+    Seq(item1, item2, item3, item4)
+  )
+  final def KList(item1: K, item2: K, item3: K, item4: K, item5: K): KList = KList(
+    Seq(item1, item2, item3, item4, item5)
+  )
+
+  final def KApply(klabel: KLabel, items: Array[K]): KApply =
+    KApply(klabel, KList(items.toList.asJava), Att.empty)
+  final def KApply(klabel: KLabel, items: Seq[K]): KApply =
+    KApply(klabel, KList(items.asJava), Att.empty)
+  final def KApply(klabel: KLabel): KApply                     = KApply(klabel, Seq())
+  final def KApply(klabel: KLabel, item: K): KApply            = KApply(klabel, Seq(item))
+  final def KApply(klabel: KLabel, item1: K, item2: K): KApply = KApply(klabel, Seq(item1, item2))
+  final def KApply(klabel: KLabel, item1: K, item2: K, item3: K): KApply =
+    KApply(klabel, Seq(item1, item2, item3))
+  final def KApply(klabel: KLabel, item1: K, item2: K, item3: K, item4: K): KApply =
+    KApply(klabel, Seq(item1, item2, item3, item4))
+  final def KApply(klabel: KLabel, item1: K, item2: K, item3: K, item4: K, item5: K): KApply =
+    KApply(klabel, Seq(item1, item2, item3, item4, item5))
+
+  final def KSequence(list: Array[K]): KSequence     = KSequence(list.toList.asJava, Att.empty)
+  final def KSequence(list: Seq[K]): KSequence       = KSequence(list.toList.asJava, Att.empty)
+  final def KSequence(): KSequence                   = KSequence(Seq())
+  final def KSequence(item: K): KSequence            = KSequence(Seq(item))
+  final def KSequence(item1: K, item2: K): KSequence = KSequence(Seq(item1, item2))
+  final def KSequence(item1: K, item2: K, item3: K): KSequence = KSequence(Seq(item1, item2, item3))
+  final def KSequence(item1: K, item2: K, item3: K, item4: K): KSequence = KSequence(
+    Seq(item1, item2, item3, item4)
+  )
+  final def KSequence(item1: K, item2: K, item3: K, item4: K, item5: K): KSequence = KSequence(
+    Seq(item1, item2, item3, item4, item5)
+  )
+
+  final def KVariable(name: String): KVariable = KVariable(name, Att.empty)
 
   def convert(l: KLabel): KLabel = l match {
     case Unapply.KLabel(name) => KLabel(name)
@@ -37,5 +108,3 @@ trait Constructors {
     case t @ Unapply.KApply(label, list)   => KApply(label, KList(list.map(convert).asJava), t.att)
   }
 }
-
-abstract class AbstractConstructors extends Constructors