Add syntax sugar for forall/exists expressions. Fix problem when pretty printing nested equalities.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/ex8.lean

@@ -0,0 +1,15 @@
+Variable f : Type -> Bool
+Show forall a b : Type, (f a) = (f b)
+Variable g : Bool -> Bool -> Bool
+Show forall (a b : Type) (c : Bool), g c ((f a) = (f b))
+Show exists (a b : Type) (c : Bool), g c ((f a) = (f b))
+Show forall (a b : Type) (c : Bool), (g c (f a) = (f b)) ⇒ (f a)
+Check forall (a b : Type) (c : Bool), g c ((f a) = (f b))
+Show ∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
+Show ∀ a b : Type, (f a) = (f b)
+Show ∃ a b : Type, (f a) = (f b) ∧ (f a)
+Show ∃ a b : Type, (f a) = (f b) ∨ (f b)
+Variable a : Bool
+Show (f a) ∨ (f a)
+Show (f a) = a ∨ (f a)
+Show (f a) = a ∧ (f a)

src/frontend/parser.cpp

@@ -581,6 +581,35 @@ class parser_fn {
         return parse_abstraction(false);
     }
 
+    /** \brief Parse forall/exists */
+    expr parse_quantifier(bool is_forall) {
+        next();
+        mk_scope scope(*this);
+        buffer<std::pair<name, expr>> bindings;
+        parse_bindings(bindings);
+        check_comma_next("invalid quantifier, ',' expected");
+        expr result = parse_expr();
+        unsigned i = bindings.size();
+        while (i > 0) {
+            --i;
+            if (is_forall)
+                result = mk_forall(bindings[i].second, mk_lambda(bindings[i].first, bindings[i].second, result));
+            else
+                result = mk_exists(bindings[i].second, mk_lambda(bindings[i].first, bindings[i].second, result));
+        }
+        return result;
+    }
+
+    /** \brief Parse <tt>'forall' bindings ',' expr</tt>. */
+    expr parse_forall() {
+        return parse_quantifier(true);
+    }
+
+    /** \brief Parse <tt>'exists' bindings ',' expr</tt>. */
+    expr parse_exists() {
+        return parse_quantifier(false);
+    }
+
     /** \brief Parse Let expression. */
     expr parse_let() {
         next();
@@ -641,6 +670,8 @@ class parser_fn {
         case scanner::token::LeftParen:  return parse_lparen();
         case scanner::token::Lambda:     return parse_lambda();
         case scanner::token::Pi:         return parse_pi();
+        case scanner::token::Forall:     return parse_forall();
+        case scanner::token::Exists:     return parse_exists();
         case scanner::token::Let:        return parse_let();
         case scanner::token::IntVal:     return parse_int();
         case scanner::token::DecimalVal: return parse_decimal();

src/frontend/pp.cpp

@@ -193,6 +193,22 @@ class pp_fn {
             return operator_info();
     }
 
+    /**
+       \brief Return the precedence of the given expression
+    */
+    unsigned get_operator_precedence(expr const & e) {
+        if (is_constant(e)) {
+            operator_info op = get_operator(e);
+            return op ? op.get_precedence() : 0;
+        } else if (is_eq(e)) {
+            return g_eq_precedence;
+        } else if (is_arrow(e)) {
+            return g_arrow_precedence;
+        } else {
+            return 0;
+        }
+    }
+
     /** \brief Return true if the application \c e has the number of arguments expected by the operator \c op. */
     bool has_expected_num_args(expr const & e, operator_info const & op) {
         switch (op.get_fixity()) {
@@ -244,8 +260,7 @@ class pp_fn {
         if (is_atomic(e)) {
             return pp(e, depth + 1);
         } else {
-            operator_info op_child = get_operator(e);
-            if (op_child && op.get_precedence() < op_child.get_precedence())
+            if (op.get_precedence() < get_operator_precedence(e))
                 return pp(e, depth + 1);
             else
                 return pp_child_with_paren(e, depth);
@@ -260,8 +275,7 @@ class pp_fn {
         if (is_atomic(e)) {
             return pp(e, depth + 1);
         } else {
-            operator_info op_child = get_operator(e);
-            if (op_child && (op == op_child || op.get_precedence() < op_child.get_precedence()))
+            if (op.get_precedence() < get_operator_precedence(e) || op == get_operator(e))
                 return pp(e, depth + 1);
             else
                 return pp_child_with_paren(e, depth);
@@ -543,8 +557,7 @@ class pp_fn {
         if (is_atomic(e)) {
             return pp(e, depth + 1);
         } else {
-            operator_info op_child = get_operator(e);
-            if (op_child && g_eq_precedence < op_child.get_precedence())
+            if (g_eq_precedence < get_operator_precedence(e))
                 return pp(e, depth + 1);
             else
                 return pp_child_with_paren(e, depth);

src/frontend/scanner.cpp

@@ -23,6 +23,12 @@ static name g_let_name("let");
 static name g_in_name("in");
 static name g_arrow_name("->");
 static name g_eq_name("=");
+static name g_forall_name("forall");
+static name g_forall_unicode("\u2201");
+static name g_forall_unicode2("∀");
+static name g_exists_name("exists");
+static name g_exists_unicode("\u2203");
+static name g_exists_unicode2("∃");
 
 static char g_normalized[256];
 
@@ -193,6 +199,10 @@ scanner::token scanner::read_a_symbol() {
                 return token::Lambda;
             else if (m_name_val == g_pi_name)
                 return token::Pi;
+            else if (m_name_val == g_forall_name)
+                return token::Forall;
+            else if (m_name_val == g_exists_name)
+                return token::Exists;
             else if (m_name_val == g_type_name)
                 return token::Type;
             else if (m_name_val == g_let_name)
@@ -243,6 +253,10 @@ scanner::token scanner::read_c_symbol() {
                 return token::Lambda;
             else if (m_name_val == g_pi_unicode)
                 return token::Pi;
+            else if (m_name_val == g_forall_unicode || m_name_val == g_forall_unicode2)
+                return token::Forall;
+            else if (m_name_val == g_exists_unicode || m_name_val == g_exists_unicode2)
+                return token::Exists;
             else
                 return token::Id;
         }
@@ -352,6 +366,8 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Period:            out << "."; break;
     case scanner::token::Lambda:            out << g_lambda_unicode; break;
     case scanner::token::Pi:                out << g_pi_unicode; break;
+    case scanner::token::Forall:            out << g_forall_unicode; break;
+    case scanner::token::Exists:            out << g_exists_unicode; break;
     case scanner::token::Arrow:             out << g_arrow_unicode; break;
     case scanner::token::Let:               out << "let"; break;
     case scanner::token::In:                out << "in"; break;

src/frontend/scanner.h

@@ -19,7 +19,7 @@ class scanner {
 public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
-        Let, In, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Eof
+        Let, In, Forall, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Eof
     };
 protected:
     int                m_spos; // position in the current line of the stream