diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index 2c39320d74edcc7350a39ee890863a13dc6fbece..3bc617538a08b2e5555898ac48ba9e68113d5398 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -197,9 +197,9 @@ object Parser {
case (l, t) =>
t match {
// do not require spaces
- case NegationToken | ConstantToken(_) | SchematicToken(_) | TrueToken | FalseToken | ParenthesisToken(_) | SpaceToken => l :+ t.toString
- // space after: quantifiers and separators
- case ForallToken | ExistsToken | ExistsOneToken | DotToken | CommaToken | SemicolonToken => l :+ t.toString :+ space
+ case ForallToken | ExistsToken | ExistsOneToken | NegationToken | ConstantToken(_) | SchematicToken(_) | TrueToken | FalseToken | ParenthesisToken(_) | SpaceToken => l :+ t.toString
+ // space after: separators
+ case DotToken | CommaToken | SemicolonToken => l :+ t.toString :+ space
// space before and after: equality, connectors, sequent symbol
case EqualityToken | AndToken | OrToken | ImpliesToken | IffToken | SequentToken => l :+ space :+ t.toString :+ space
}
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 5fd97a7f959e2d007a01a53cf13bdd51e0d500bb..221f69e70940a381b4346a3700f9cb32e8cfc442 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -28,13 +28,13 @@ class PrinterTest extends AnyFunSuite with TestUtils {
assert(Parser.printFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ 'x = 'x")
- assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ 'x. 'x = 'x")
- assert(Parser.printFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ (∀ 'x. 'x = 'x)")
- assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀ 'x. b) ∧ a")
- assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ 'x. b) ∧ a")
- assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀ 'x. b) ∨ a")
+ assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀'x. 'x = 'x")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ (∀'x. 'x = 'x)")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀'x. b) ∧ a")
+ assert(Parser.printFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀'x. b) ∧ a")
+ assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀'x. b) ∨ a")
- assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀ 'x. ∃ 'y. ∃! 'z. a")
+ assert(Parser.printFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀'x. ∃'y. ∃!'z. a")
assert(Parser.printFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f('x, 'y, 'z)")
}
@@ -144,17 +144,17 @@ class PrinterTest extends AnyFunSuite with TestUtils {
}
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")
+ 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")
+ 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(b, a)))) == "∀'x. b ∧ a")
assert(
Parser.printFormula(
BinderFormula(
@@ -162,10 +162,10 @@ class PrinterTest extends AnyFunSuite with TestUtils {
x,
ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
)
- ) == "∀ 'x. p('x) ∧ q('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, x, b), a))) == "(∀'x. b) ∧ a")
assert(
Parser.printFormula(
@@ -176,11 +176,11 @@ class PrinterTest extends AnyFunSuite with TestUtils {
PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))
)
)
- ) == "(∀ 'x. p('x)) ∧ q('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")
+ 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") {
@@ -191,15 +191,15 @@ class PrinterTest extends AnyFunSuite with TestUtils {
}
test("complex formulas") {
- assert(Parser.printFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀ 'x. 'x = 'x")
+ 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")
+ 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")
+ 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
@@ -208,11 +208,11 @@ class PrinterTest extends AnyFunSuite with TestUtils {
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"
+ 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"
+ Parser.printSequent(Sequent(Set(forallEq, PredicateFormula(ConstantPredicateLabel("p", 0), Seq())), Set(existsYEq, existsXEq))) == "∀'x. 'x = 'x; p ⊢ ∃'y. 'y = 'y; ∃'x. 'x = 'x"
)
}
@@ -220,7 +220,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
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(leftAndRight), Set(leftAndRight))) == "∃!'x. 'phi('x, 'a) ⊢ ∃!'x. 'phi('x, 'a)")
assert(
Parser.printSequent(
@@ -228,7 +228,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
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))"
+ ) == "∀'x. 'x = 'x1 ⇔ 'phi('x) ⊢ 'z = 'f('x1) ⇒ (∃'x. 'z = 'f('x) ∧ 'phi('x))"
)
assert(
Parser.printSequent(
@@ -236,7 +236,7 @@ class PrinterTest extends AnyFunSuite with TestUtils {
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))"
+ ) == "∃'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(