From 4bdf2e45c8a63f7c909057c8a011b71682b33fca Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@runtimeverification.com>
Date: Thu, 28 Sep 2023 12:46:40 -0500
Subject: [PATCH 1/2] change case classes and parser to support multi-ary
 \and/\or.

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.
---
 .../org/kframework/parser/kore/Default.scala  | 20 +++++++++++++++----
 .../kframework/parser/kore/Interface.scala    |  8 ++++++++
 .../parser/kore/parser/TextToKore.scala       | 12 ++++-------
 3 files changed, 28 insertions(+), 12 deletions(-)

diff --git a/kore/src/main/scala/org/kframework/parser/kore/Default.scala b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
index e36953b0dbc..7fa704e5eb4 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Default.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
@@ -39,9 +39,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 +135,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)
 
diff --git a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
index 39161f2a08e..6723c1342c7 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala
+++ b/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
diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala
index 0dc7637b627..ef16e75c7e3 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala
+++ b/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("{")

From 7c69c7e8f9f80fd76d30e426fa4159c21aaeea67 Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@runtimeverification.com>
Date: Thu, 28 Sep 2023 12:51:36 -0500
Subject: [PATCH 2/2] make something temporarily public as part of the
 migration path

---
 kore/src/main/scala/org/kframework/parser/kore/Default.scala | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/kore/src/main/scala/org/kframework/parser/kore/Default.scala b/kore/src/main/scala/org/kframework/parser/kore/Default.scala
index 7fa704e5eb4..2f80fc53674 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/Default.scala
+++ b/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