Implement parsing and printing 'true' and 'false' constants

Represented as And() and Or() respectively.

lisa-utils/src/main/scala/lisa/utils/Parser.scala

@@ -4,6 +4,7 @@ import lisa.kernel.fol.FOL
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.fol.FOL.equality
 import lisa.kernel.proof.SequentCalculus.*
+import lisa.utils.Helpers.False
 import scallion.*
 import scallion.util.Unfolds.unfoldRight
 import silex.*
@@ -60,6 +61,10 @@ object Parser {
 
     case object NegationToken extends FormulaToken(Neg.id)
 
+    case object TrueToken extends FormulaToken("⊤")
+
+    case object FalseToken extends FormulaToken("⊥")
+
     case object EqualityToken extends FormulaToken(equality.id)
 
     // Constant functions and predicates
@@ -92,6 +97,8 @@ object Parser {
       elem('∨') | word("\\/") |> { _ => OrToken },
       elem('⇒') | word("=>") | word("==>") |> { _ => ImpliesToken },
       elem('↔') | word("<=>") | word("<==>") |> { _ => IffToken },
+      elem('⊤') | elem('T') | word("True") | word("true") |> { _ => TrueToken },
+      elem('⊥') | elem('F') | word("False") | word("false") |> { _ => FalseToken },
       elem('¬') | elem('!') |> { _ => NegationToken },
       elem('(') |> ParenthesisToken(true),
       elem(')') |> ParenthesisToken(false),
@@ -122,7 +129,7 @@ object Parser {
           case (l, t) =>
             t match {
               // do not require spaces
-              case NegationToken | ConstantToken(_) | SchematicToken(_) | ParenthesisToken(_) | SpaceToken => l :+ t.toString
+              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
               // space before and after: equality, connectors, sequent symbol
@@ -139,9 +146,9 @@ object Parser {
     case object AndKind extends TokenKind
     case object OrKind extends TokenKind
     // implies, iff are both non-associative and are of equal priority, lower than and, or
-
     case object TopLevelConnectorKind extends TokenKind
     case object NegationKind extends TokenKind
+    case object BooleanConstantKind extends TokenKind
     case object FunctionOrPredicateKind extends TokenKind
     case object EqualityKind extends TokenKind
     case object CommaKind extends TokenKind
@@ -164,6 +171,7 @@ object Parser {
       case OrToken => OrKind
       case IffToken | ImpliesToken => TopLevelConnectorKind
       case NegationToken => NegationKind
+      case TrueToken | FalseToken => BooleanConstantKind
       case _: ConstantToken | _: SchematicToken => FunctionOrPredicateKind
       case EqualityToken => EqualityKind
       case CommaToken => CommaKind
@@ -240,7 +248,7 @@ object Parser {
 
     //////////////////////// FORMULAS /////////////////////////////////
     // can appear without parentheses
-    lazy val simpleFormula: Syntax[Formula] = predicate.up[Formula] | negated.up[Formula]
+    lazy val simpleFormula: Syntax[Formula] = predicate.up[Formula] | negated.up[Formula] | bool.up[Formula]
     lazy val subformula: Syntax[Formula] = simpleFormula | open.skip ~ formula ~ closed.skip
 
     def createFunctionTerm(label: Token, args: Seq[Term]): Term = label match {
@@ -253,6 +261,18 @@ object Parser {
       case _ => throw UnreachableException
     }
 
+    val bool: Syntax[ConnectorFormula] = accept(BooleanConstantKind)(
+      {
+        case TrueToken => ConnectorFormula(And, Seq())
+        case FalseToken => ConnectorFormula(Or, Seq())
+      },
+      {
+        case ConnectorFormula(And, Seq()) => Seq(TrueToken)
+        case ConnectorFormula(Or, Seq()) => Seq(FalseToken)
+        case _ => throw UnreachableException
+      }
+    )
+
     val predicate: Syntax[PredicateFormula] = (elem(FunctionOrPredicateKind) ~ opt(args) ~ opt(eq.skip ~ elem(FunctionOrPredicateKind) ~ opt(args))).map(
       {
         // predicate application
@@ -393,6 +413,8 @@ object Parser {
       },
       {
         case Sequent(Seq(), right) => Seq(right.toSeq ~ None)
+        // TODO: use constant
+        case Sequent(left, Seq()) => Seq(left.toSeq ~ Some(Seq(False)))
         case Sequent(left, right) => Seq(left.toSeq ~ Some(right.toSeq))
       }
     )

lisa-utils/src/test/scala/lisa/utils/ParserPrinterTest.scala

+package lisa.utils
+
+import org.scalatest.funsuite.AnyFunSuite
+
+class ParserPrinterTest extends AnyFunSuite {}

lisa-utils/src/test/scala/lisa/utils/ParserTest.scala

@@ -45,6 +45,18 @@ class ParserTest extends AnyFunSuite with TestUtils {
     assert(Parser.parseFormula("a()") == PredicateFormula(ConstantPredicateLabel("a", 0), Seq()))
   }
 
+  test("boolean constants") {
+    assert(Parser.parseFormula("true") == True)
+    assert(Parser.parseFormula("True") == True)
+    assert(Parser.parseFormula("T") == True)
+    assert(Parser.parseFormula("⊤") == True)
+
+    assert(Parser.parseFormula("false") == False)
+    assert(Parser.parseFormula("False") == False)
+    assert(Parser.parseFormula("F") == False)
+    assert(Parser.parseFormula("⊥") == False)
+  }
+
   test("predicate application") {
     assert(Parser.parseFormula("p(x, y, z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz)))
     assert(Parser.parseFormula("p(?x, ?y, ?z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z)))

lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala

@@ -108,6 +108,11 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     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("connectors with no arguments") {
+    assert(Parser.printFormula(ConnectorFormula(And, Seq())) == "⊤")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq())) == "⊥")
+  }
+
   test("connector priority") {
     // a ∨ (b ∧ c)
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, ConnectorFormula(And, Seq(b, c))))) == "a ∨ b ∧ c")