From 8faa4ec104f5d7089b07842bcf6464dc2e4c2870 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Thu, 6 Oct 2022 15:51:34 +0200
Subject: [PATCH] Print and/or connector formulas with 1 argument
---
lisa-utils/src/main/scala/lisa/utils/Parser.scala | 1 +
lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala | 9 +++++++++
2 files changed, 10 insertions(+)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index 3bc61753..7b6eda22 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -460,6 +460,7 @@ object Parser {
},
{
case ConnectorFormula(c @ (Iff | Implies), Seq(left, right)) => Seq(left ~ Some(c ~ right))
+ case ConnectorFormula((And | Or), Seq(f)) => Seq(f ~ None)
case f => Seq(f ~ None)
}
)
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 221f69e7..e7c2da63 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -98,6 +98,15 @@ class PrinterTest extends AnyFunSuite with TestUtils {
assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ∨ c")
}
+ test("and/or of 1 argument") {
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(a))) == "a")
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(a))) == "a")
+
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(ConnectorFormula(Or, Seq(a)), ConnectorFormula(And, Seq(a))))) == "(a) ⇒ (a)")
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, a))) == "a ⇒ a")
+ assert(Parser.printFormula(BinderFormula(Forall, x, ConnectorFormula(Or, Seq(a)))) == "∀'x. a")
+ }
+
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")
--
GitLab