change case classes and parser to support multi-ary \and/\or. (#3676)

At this stage, actually parsing a multi-ary term will lead to an
internal representation that is handled incorrectly by all the code that
interprets KORE. However, this change ought to pass CI and be sufficient
to be able to modify the llvm backend without anything breaking.

kore/src/main/scala/org/kframework/parser/kore/Default.scala

@@ -5,7 +5,8 @@ import org.kframework.parser.{kore => i}
 
 object implementation {
 
-  private object ConcreteClasses {
+  // TODO: make private again
+  object ConcreteClasses {
 
     case class Definition(att: i.Attributes, modules: Seq[i.Module]) extends i.Definition
 
@@ -39,9 +40,17 @@ object implementation {
 
     case class Bottom(s: i.Sort) extends i.Bottom
 
-    case class And(s: i.Sort, _1: i.Pattern, _2: i.Pattern) extends i.And
+    case class And(s: i.Sort, args: Seq[i.Pattern]) extends i.And {
+      val _1 = args(0)
 
-    case class Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern) extends i.Or
+      val _2 = args(1)
+    }
+
+    case class Or(s: i.Sort, args: Seq[i.Pattern]) extends i.Or {
+      val _1 = args(0)
+
+      val _2 = args(1)
+    }
 
     case class Not(s: i.Sort, _1: i.Pattern) extends i.Not
 
@@ -127,9 +136,13 @@ object implementation {
 
     def Bottom(s: i.Sort): i.Pattern = d.Bottom(s)
 
-    def And(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.And(s, _1, _2)
+    def And(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.And(s, Seq(_1, _2))
+
+    def And(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = d.And(s, args)
+
+    def Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Or(s, Seq(_1, _2))
 
-    def Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Or(s, _1, _2)
+    def Or(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = d.Or(s, args)
 
     def Not(s: i.Sort, _1: i.Pattern): i.Pattern = d.Not(s, _1)
 

kore/src/main/scala/org/kframework/parser/kore/Interface.scala

@@ -167,6 +167,8 @@ trait And extends Pattern {
   def _1: Pattern
 
   def _2: Pattern
+
+  def args: Seq[Pattern]
 }
 
 object And {
@@ -179,6 +181,8 @@ trait Or extends Pattern {
   def _1: Pattern
 
   def _2: Pattern
+
+  def args: Seq[Pattern]
 }
 
 object Or {
@@ -511,8 +515,12 @@ trait Builders {
 
   def And(s: Sort, _1: Pattern, _2: Pattern): Pattern
 
+  def And(s: Sort, args: Seq[Pattern]): Pattern
+
   def Or(s: Sort, _1: Pattern, _2: Pattern): Pattern
 
+  def Or(s: Sort, args: Seq[Pattern]): Pattern
+
   def Not(s: Sort, _1: Pattern): Pattern
 
   def Implies(s: Sort, _1: Pattern, _2: Pattern): Pattern

kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala

@@ -379,21 +379,17 @@ class TextToKore(b: Builders = DefaultBuilders) {
             val s = parseSort()
             consumeWithLeadingWhitespaces("}")
             consumeWithLeadingWhitespaces("(")
-            val p1 = parsePattern()
-            consumeWithLeadingWhitespaces(",")
-            val p2 = parsePattern()
+            val args = parseList(() => parsePattern(), ',', ')')
             consumeWithLeadingWhitespaces(")")
-            b.And(s, p1, p2)
+            b.And(s, args)
           case ('o', 'r') => // or
             consumeWithLeadingWhitespaces("{")
             val s = parseSort()
             consumeWithLeadingWhitespaces("}")
             consumeWithLeadingWhitespaces("(")
-            val p1 = parsePattern()
-            consumeWithLeadingWhitespaces(",")
-            val p2 = parsePattern()
+            val args = parseList(() => parsePattern(), ',', ')')
             consumeWithLeadingWhitespaces(")")
-            b.Or(s, p1, p2)
+            b.Or(s, args)
           case ('n', 'o') => // not
             consume("t")
             consumeWithLeadingWhitespaces("{")