Do not print a space after a quantifier

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
             }

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(