From e19e47a579c196691b8897be2ba9aecefb82d743 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Fri, 30 Sep 2022 11:40:24 +0200
Subject: [PATCH] Add scallion parser tests as printer tests
Simply print the formula and expect it to be equal to the string
instead of parsing the string and expecting it to be equal to the
formula. Not all tests of the parser are tests for printer, because
there exist multiple strings that correspond to the same formula
(due to extra parentheses and multiple ways to write connectors).
---
.../test/scala/lisa/utils/PrinterTest.scala | 198 +++++++++++++++++-
1 file changed, 197 insertions(+), 1 deletion(-)
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index d03d2b57..f1757835 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -1,8 +1,10 @@
package lisa.utils
import lisa.kernel.fol.FOL.*
-import lisa.utils.Printer.*
+import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.utils.Helpers.*
import lisa.utils.Parser
+import lisa.utils.Printer.*
import org.scalatest.funsuite.AnyFunSuite
import scala.language.adhocExtensions
@@ -37,4 +39,198 @@ class PrinterTest extends AnyFunSuite with TestUtils {
assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f(?x, ?y, ?z)")
}
+ test("constant") {
+ assert(Parser.printTerm(FunctionTerm(cx, Seq())) == "x")
+ }
+
+ test("variable") {
+ assert(Parser.printTerm(VariableTerm(x)) == "?x")
+ }
+
+ test("constant function application") {
+ assert(Parser.printTerm(FunctionTerm(f1, Seq(cx))) == "f(x)")
+ assert(Parser.printTerm(FunctionTerm(f2, Seq(cx, cy))) == "f(x, y)")
+ assert(Parser.printTerm(FunctionTerm(f3, Seq(cx, cy, cz))) == "f(x, y, z)")
+
+ assert(Parser.printTerm(FunctionTerm(f1, Seq(x))) == "f(?x)")
+ assert(Parser.printTerm(FunctionTerm(f2, Seq(x, y))) == "f(?x, ?y)")
+ assert(Parser.printTerm(FunctionTerm(f3, Seq(x, y, z))) == "f(?x, ?y, ?z)")
+ }
+
+ test("schematic function application") {
+ assert(Parser.printTerm(FunctionTerm(sf1, Seq(cx))) == "?f(x)")
+ assert(Parser.printTerm(FunctionTerm(sf2, Seq(cx, cy))) == "?f(x, y)")
+ assert(Parser.printTerm(FunctionTerm(sf3, Seq(cx, cy, cz))) == "?f(x, y, z)")
+
+ assert(Parser.printTerm(FunctionTerm(sf1, Seq(x))) == "?f(?x)")
+ assert(Parser.printTerm(FunctionTerm(sf2, Seq(x, y))) == "?f(?x, ?y)")
+ assert(Parser.printTerm(FunctionTerm(sf3, Seq(x, y, z))) == "?f(?x, ?y, ?z)")
+ }
+
+ test("nested function application") {
+ assert(Parser.printTerm(FunctionTerm(sf2, Seq(FunctionTerm(sf1, Seq(x)), y))) == "?f(?f(?x), ?y)")
+ }
+
+ test("0-ary predicate") {
+ assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("a", 0), Seq())) == "a")
+ }
+
+ test("predicate application") {
+ assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz))) == "p(x, y, z)")
+ assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z))) == "p(?x, ?y, ?z)")
+ }
+
+ test("equality") {
+ assert(Parser.printFormula(PredicateFormula(equality, Seq(cx, cx))) == "x = x")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ ?x = ?x")
+ }
+
+ test("unicode connectors") {
+ assert(Parser.printFormula(ConnectorFormula(Neg, Seq(a))) == "¬a")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b))) == "a ∧ b")
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b))) == "a ∨ b")
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, b))) == "a ⇒ b")
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, b))) == "a ↔ b")
+ }
+
+ test("connector associativity") {
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ∧ c")
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ∨ c")
+ }
+
+ test("connector priority") {
+ // a ∨ (b ∧ c)
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ∨ b ∧ c")
+ // (a ∧ b) ∨ c
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ∨ c")
+
+ // (a ∧ b) => c
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ⇒ c")
+ // a => (b ∧ c)
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ⇒ b ∧ c")
+ // (a ∨ b) => c
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ⇒ c")
+ // a => (b ∨ c)
+ assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ⇒ b ∨ c")
+
+ // (a ∧ b) <=> c
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(And, Seq(a, b)), c))) == "a ∧ b ↔ c")
+ // a <=> (b ∧ c)
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ↔ b ∧ c")
+ // (a ∨ b) <=> c
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ↔ c")
+ // a <=> (b ∨ c)
+ assert(Parser.printFormula(ConnectorFormula(Iff, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ↔ b ∨ c")
+ }
+
+ test("connector parentheses") {
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "(a ∨ b) ∧ c")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(a, ConnectorFormula(Or, Seq(b, c))))) == "a ∧ (b ∨ c)")
+ }
+
+ test("quantifiers") {
+ assert(Parser.printFormula(BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∀ ?x. p")
+ assert(Parser.printFormula(BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃ ?x. p")
+ assert(Parser.printFormula(BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq()))) == "∃! ?x. p")
+ }
+
+ test("nested quantifiers") {
+ assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀ ?x. ∃ ?y. ∃! ?z. a")
+ }
+
+ test("quantifier parentheses") {
+ assert(Parser.printFormula(BinderFormula(Forall, x, ConnectorFormula(And, Seq(b, a)))) == "∀ ?x. b ∧ a")
+ assert(
+ Parser.printFormula(
+ BinderFormula(
+ Forall,
+ x,
+ ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
+ )
+ ) == "∀ ?x. p(?x) ∧ q(?x)"
+ )
+
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀ ?x. b) ∧ a")
+
+ assert(
+ Parser.printFormula(
+ ConnectorFormula(
+ And,
+ Seq(
+ BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x))),
+ PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))
+ )
+ )
+ ) == "(∀ ?x. p(?x)) ∧ q(?x)"
+ )
+
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ ?x. b) ∨ a")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ ?x. b) ∧ a")
+ }
+
+ test("complex formulas with connectors") {
+ assert(Parser.printFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Or, Seq(a, b))))) == "¬(a ∨ b)")
+ assert(Parser.printFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(a))))) == "¬¬a")
+ assert(Parser.printFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(ConnectorFormula(And, Seq(a, b))))))) == "¬¬(a ∧ b)")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(Neg, Seq(b)))), ConnectorFormula(Neg, Seq(c))))) == "¬a ∧ ¬b ∧ ¬c")
+ }
+
+ test("complex formulas") {
+ assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ ?x. ?x = ?x")
+ }
+
+ test("sequent") {
+ val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
+ assert(Parser.printSequent(Sequent(Set(), Set(forallEq))) == "⊢ ∀ ?x. ?x = ?x")
+ assert(Parser.printSequent(Sequent(Set(forallEq), Set(forallEq))) == "∀ ?x. ?x = ?x ⊢ ∀ ?x. ?x = ?x")
+ val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
+ assert(Parser.printSequent(Sequent(Set(forallEq), Set(existsXEq))) == "∀ ?x. ?x = ?x ⊢ ∃ ?x. ?x = ?x")
+ }
+
+ // warning: this test might be flaky because formula order is not fixed in sequents but fixed in the string representation
+ test("sequent with multiple formulas") {
+ val forallEq = BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))
+ val existsXEq = BinderFormula(Exists, x, PredicateFormula(equality, Seq(x, x)))
+ val existsYEq = BinderFormula(Exists, y, PredicateFormula(equality, Seq(y, y)))
+ assert(
+ Parser.printSequent(Sequent(Set(forallEq), Set(existsYEq, existsXEq))) == "∀ ?x. ?x = ?x ⊢ ∃ ?y. ?y = ?y; " +
+ "∃ ?x. ?x = ?x"
+ )
+ assert(
+ Parser.printSequent(Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀ ?x. ?x = ?x; p ⊢ ∃ ?y. ?y = ?y; ∃ ?x. ?x = ?x"
+ )
+ }
+
+ // warning: this test might be flaky because formula order is not fixed in sequents but fixed in the string representation
+ test("sequents from Mapping and SetTheory") {
+ val va = VariableLabel("a")
+ val leftAndRight = BinderFormula(ExistsOne, x, PredicateFormula(sPhi2, Seq(x, va)))
+ assert(Parser.printSequent(Sequent(Set(leftAndRight), Set(leftAndRight))) == "∃! ?x. ?phi(?x, ?a) ⊢ ∃! ?x. ?phi(?x, ?a)")
+
+ assert(
+ Parser.printSequent(
+ Sequent(
+ Set(BinderFormula(Forall, x, ConnectorFormula(Iff, Seq(x === x1, sPhi1(x))))),
+ Set((z === sf1(x1)) ==> exists(x, (z === sf1(x)) /\ sPhi1(x)))
+ )
+ ) == "∀ ?x. ?x = ?x1 ↔ ?phi(?x) ⊢ ?z = ?f(?x1) ⇒ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+ )
+ assert(
+ Parser.printSequent(
+ exists(x1, forall(x, (x === x1) <=> (sPhi1(x)))) |- exists(
+ z1,
+ forall(z, (z === z1) <=> exists(x, (z === sf1(x)) /\ sPhi1(x)))
+ )
+ ) == "∃ ?x1. ∀ ?x. ?x = ?x1 ↔ ?phi(?x) ⊢ ∃ ?z1. ∀ ?z. ?z = ?z1 ↔ (∃ ?x. ?z = ?f(?x) ∧ ?phi(?x))"
+ )
+ assert(Parser.printSequent((() |- (x === x) \/ (x === y))) == "⊢ ?x = ?x ∨ ?x = ?y")
+ assert(
+ Parser.printSequent(
+ Set(
+ (x === x) \/ (x === y),
+ ((x === x) \/ (x === y)) <=> ((x === xPrime) \/ (x === yPrime))
+ ) |- (x === xPrime) \/ (x === yPrime)
+ ) == "?x = ?x ∨ ?x = ?y; ?x = ?x ∨ ?x = ?y ↔ ?x = ?x' ∨ ?x = ?y' ⊢ ?x = ?x' ∨ ?x = ?y'"
+ )
+ }
}
--
GitLab