From 51422fe6540c1c9173b0e21511958bca7e0660d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 17:24:05 -0700 Subject: [PATCH] Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0' Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 65 ++++++++++++++++++++------ tests/lean/implicit1.lean | 20 ++++++++ tests/lean/implicit1.lean.expected.out | 30 ++++++++++++ 3 files changed, 100 insertions(+), 15 deletions(-) create mode 100644 tests/lean/implicit1.lean create mode 100644 tests/lean/implicit1.lean.expected.out diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index a0e602315..538ffdd9f 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -705,33 +705,58 @@ class parser::imp { /** \brief Parse ID ... ID ':' expr, where the expression represents the type of the identifiers. + + \remark If \c implicit_decl is true, then the bindings should be + marked as implicit. This flag is set to true, for example, + when we are parsing definitions such as: + Definition f {A : Type} (a b : A), A := ... + The {A : Type} is considered an implicit argument declaration. + + \remark If \c suppress_type is true, then the type doesn't + need to be provided. That is, we automatically include a placeholder. */ - void parse_simple_bindings(buffer> & result, bool implicit) { + void parse_simple_bindings(buffer> & result, bool implicit_decl, bool supress_type) { buffer> names; parse_names(names); - check_colon_next("invalid binder, ':' expected"); + expr type; + if (curr_is_colon()) { + next(); + type = parse_expr(); + } unsigned sz = result.size(); result.resize(sz + names.size()); - expr type = parse_expr(); for (std::pair const & n : names) register_binding(n.second); unsigned i = names.size(); while (i > 0) { --i; - result[sz + i] = std::make_tuple(names[i].first, names[i].second, lift_free_vars(type, i), implicit); + expr arg_type; + if (type) + arg_type = lift_free_vars(type, i); + else + arg_type = mk_placholder(); + result[sz + i] = std::make_tuple(names[i].first, names[i].second, arg_type, implicit_decl); } } /** \brief Parse a sequence of '(' ID ... ID ':' expr ')'. - This is used when parsing lambda, Pi, forall/exists expressions and definitions. + This is used when parsing lambda, Pi, forall/exists expressions and + definitions. + + \remark If implicit_decls is true, then we allow declarations + with curly braces. These declarations are used to tag implicit + arguments. Such as: + Definition f {A : Type} (a b : A), A := ... + + \see parse_simple_bindings */ - void parse_bindings(buffer> & result, bool allow_implicit = false) { + void parse_bindings(buffer> & result, bool implicit_decls, bool suppress_type) { if (curr_is_identifier()) { - parse_simple_bindings(result, false); + parse_simple_bindings(result, false, suppress_type); } else { // (ID ... ID : type) ... (ID ... ID : type) - if (allow_implicit) { + if (implicit_decls) { if (!curr_is_lparen() && !curr_is_lcurly()) throw parser_error("invalid binder, '(', '{' or identifier expected", pos()); } else { @@ -740,15 +765,15 @@ class parser::imp { } bool implicit = curr_is_lcurly(); next(); - parse_simple_bindings(result, implicit); + parse_simple_bindings(result, implicit, suppress_type); if (!implicit) check_rparen_next("invalid binder, ')' expected"); else check_rcurly_next("invalid binder, '}' expected"); - while (curr_is_lparen() || (allow_implicit && curr_is_lcurly())) { + while (curr_is_lparen() || (implicit_decls && curr_is_lcurly())) { bool implicit = curr_is_lcurly(); next(); - parse_simple_bindings(result, implicit); + parse_simple_bindings(result, implicit, suppress_type); if (!implicit) check_rparen_next("invalid binder, ')' expected"); else @@ -757,6 +782,16 @@ class parser::imp { } } + /** \brief Parse bindings for object such as: definitions, theorems, axioms, variables ... */ + void parse_object_bindings(buffer> & result) { + parse_bindings(result, true, false); + } + + /** \brief Parse bindings for expressions such as: lambda, pi, forall, exists */ + void parse_expr_bindings(buffer> & result) { + parse_bindings(result, false, true); + } + /** \brief Create a lambda/Pi abstraction, using the giving binders and body. @@ -780,7 +815,7 @@ class parser::imp { next(); mk_scope scope(*this); buffer> bindings; - parse_bindings(bindings); + parse_expr_bindings(bindings); check_comma_next("invalid abstraction, ',' expected"); expr result = parse_expr(); return mk_abstraction(is_lambda, bindings, result); @@ -801,7 +836,7 @@ class parser::imp { next(); mk_scope scope(*this); buffer> bindings; - parse_bindings(bindings); + parse_expr_bindings(bindings); check_comma_next("invalid quantifier, ',' expected"); expr result = parse_expr(); unsigned i = bindings.size(); @@ -1013,7 +1048,7 @@ class parser::imp { val = elaborate(parse_expr()); } else { mk_scope scope(*this); - parse_bindings(bindings, true); + parse_object_bindings(bindings); check_colon_next("invalid definition, ':' expected"); expr type_body = parse_expr(); check_assign_next("invalid definition, ':=' expected"); @@ -1066,7 +1101,7 @@ class parser::imp { type = elaborate(parse_expr()); } else { mk_scope scope(*this); - parse_bindings(bindings, true); + parse_object_bindings(bindings); check_colon_next("invalid variable/axiom declaration, ':' expected"); expr type_body = parse_expr(); type = elaborate(mk_abstraction(false, bindings, type_body)); diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean new file mode 100644 index 000000000..ed7049971 --- /dev/null +++ b/tests/lean/implicit1.lean @@ -0,0 +1,20 @@ +Variable f : Int -> Int -> Int +Show forall a, f a a > 0 +Show forall a b, f a b > 0 +Variable g : Int -> Real -> Int +Show forall a b, g a b > 0 +Show forall a b, g a (f a b) > 0 +Set pp::coercion true +Show forall a b, g a (f a b) > 0 +Show fun a, a + 1 +Show fun a b, a + b +Show fun (a b) (c : Int), a + c + b +(* + The next example shows a limitation of the current elaborator. + The current elaborator resolves overloads before solving the implicit argument constraints. + So, it does not have enough information for deciding which overload to use. +*) +Show (fun a b, a + b) 10 20. +Variable x : Int +(* The following one works because the type of x is used to decide which + should be used *) +Show fun a b, a + x + b \ No newline at end of file diff --git a/tests/lean/implicit1.lean.expected.out b/tests/lean/implicit1.lean.expected.out new file mode 100644 index 000000000..4d6d60f5b --- /dev/null +++ b/tests/lean/implicit1.lean.expected.out @@ -0,0 +1,30 @@ + Set: pp::colors + Set: pp::unicode + Assumed: f +∀ a : Int, (f a a) > 0 +∀ a b : Int, (f a b) > 0 + Assumed: g +∀ (a : Int) (b : Real), (g a b) > 0 +∀ a b : Int, (g a (f a b)) > 0 + Set: lean::pp::coercion +∀ a b : Int, (g a (int_to_real (f a b))) > (nat_to_int 0) +λ a : Nat, a + 1 +Error (line: 10, pos: 18) ambiguous overloads +Candidates: + Real::add : Real → Real → Real + Int::add : Int → Int → Int + Nat::add : Nat → Nat → Nat +Arguments: + a : lift:0:2 ?M0 + b : lift:0:1 ?M2 +λ a b c : Int, a + c + b +Error (line: 17, pos: 19) ambiguous overloads +Candidates: + Real::add : Real → Real → Real + Int::add : Int → Int → Int + Nat::add : Nat → Nat → Nat +Arguments: + a : lift:0:2 ?M0 + b : lift:0:1 ?M2 + Assumed: x +λ a b : Int, a + x + b