Merge remote-tracking branch 'origin/develop'

runtimeverification · Sep 28, 2023 · f624a15 · f624a15
2 parents 25367c4 + 9ddff9d
commit f624a15
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 13 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
@@ -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)
 

diff --git 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
@@ -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("{")