From cf382c0f95459bd3479c5139d39d6327e6b220c1 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Mon, 3 Oct 2022 15:28:00 +0200
Subject: [PATCH] Support printing 'and' and 'or' ConnectorFormulas with more
 than two arguments

---
 lisa-utils/src/main/scala/lisa/utils/Parser.scala     | 11 +++++++++--
 .../src/test/scala/lisa/utils/PrinterTest.scala       | 10 ++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index 4d4da900..43a89048 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -328,8 +328,15 @@ object Parser {
       or is LeftAssociative
     )(
       (l, conn, r) => ConnectorFormula(conn, Seq(l, r)),
-      { case ConnectorFormula(conn, Seq(l, r)) =>
-        (l, conn, r)
+      {
+        case ConnectorFormula(conn, Seq(l, r)) =>
+          (l, conn, r)
+        case ConnectorFormula(conn, l +: rest) if rest.nonEmpty =>
+          val last = rest.last
+          val leftSide = rest.dropRight(1)
+          // parser only knows about connector formulas of two arguments, so we unfold the formula of many arguments to
+          // multiple nested formulas of two arguments
+          (leftSide.foldLeft(l)((f1, f2) => ConnectorFormula(conn, Seq(f1, f2))), conn, last)
       }
     )
 
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index f1757835..e09e288d 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -98,6 +98,16 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ∨ c")
   }
 
+  test("connectors of >2 arguments") {
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b, c))) == "a ∧ b ∧ c")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b, c))) == "a ∨ b ∨ c")
+
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b, c, a))) == "a ∧ b ∧ c ∧ a")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b, c, b))) == "a ∨ b ∨ c ∨ b")
+
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, b, c)), ConnectorFormula(And, Seq(c, b, a))))) == "a ∧ b ∧ c ∨ c ∧ b ∧ a")
+  }
+
   test("connector priority") {
     // a ∨ (b ∧ c)
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ∨ b ∧ c")
-- 
GitLab