From 986d9635e18d27b9b938047d22eefdf85be88fde Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Aug 2013 15:08:52 -0700 Subject: [PATCH] Add syntax sugar for forall/exists expressions. Fix problem when pretty printing nested equalities. Signed-off-by: Leonardo de Moura --- examples/ex8.lean | 15 +++++++++++++++ src/frontend/parser.cpp | 31 +++++++++++++++++++++++++++++++ src/frontend/pp.cpp | 25 +++++++++++++++++++------ src/frontend/scanner.cpp | 16 ++++++++++++++++ src/frontend/scanner.h | 2 +- 5 files changed, 82 insertions(+), 7 deletions(-) create mode 100644 examples/ex8.lean diff --git a/examples/ex8.lean b/examples/ex8.lean new file mode 100644 index 0000000000..ce0732e903 --- /dev/null +++ b/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) diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp index 159e52b297..f0ee47675b 100644 --- a/src/frontend/parser.cpp +++ b/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> 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 'forall' bindings ',' expr. */ + expr parse_forall() { + return parse_quantifier(true); + } + + /** \brief Parse 'exists' bindings ',' expr. */ + 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(); diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp index b9b18200f4..b3669ce042 100644 --- a/src/frontend/pp.cpp +++ b/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); diff --git a/src/frontend/scanner.cpp b/src/frontend/scanner.cpp index 5b63e07ed2..142945c0c4 100644 --- a/src/frontend/scanner.cpp +++ b/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; diff --git a/src/frontend/scanner.h b/src/frontend/scanner.h index c10a3e9845..a0e91ab1ef 100644 --- a/src/frontend/scanner.h +++ b/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