From 8e7c657cf77966a0e8624dc45a44dfda6871f651 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 18:00:30 -0700 Subject: [PATCH] Use expected type of a definition in the elaborator. Improve elaborator solver. Add new example Signed-off-by: Leonardo de Moura --- examples/ex1.lean | 6 ++---- examples/ex2.lean | 6 ++++++ src/frontends/lean/lean_elaborator.cpp | 29 ++++++++++++++++++++++---- src/frontends/lean/lean_elaborator.h | 1 + src/frontends/lean/lean_parser.cpp | 26 ++++++++++------------- src/shell/CMakeLists.txt | 1 + 6 files changed, 46 insertions(+), 23 deletions(-) create mode 100644 examples/ex2.lean diff --git a/examples/ex1.lean b/examples/ex1.lean index 0c4e0cbd4..49983720c 100644 --- a/examples/ex1.lean +++ b/examples/ex1.lean @@ -19,10 +19,8 @@ Axiom H2 : b = e (* Proof that (h a b) = (h c e) *) Theorem T1 : (h a b) = (h c e) := DisjCases H1 - (fun C1 : _, - CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) - (fun C2 : _, - CongrH (Trans (Conjunct1 C2) (Conjunct2 C2)) H2) + (λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) + (λ C2, CongrH (Trans (Conjunct1 C2) (Conjunct2 C2)) H2) (* We can use theorem T1 to prove other theorems *) Theorem T2 : (h a (h a b)) = (h a (h c e)) := diff --git a/examples/ex2.lean b/examples/ex2.lean new file mode 100644 index 000000000..4cef29f25 --- /dev/null +++ b/examples/ex2.lean @@ -0,0 +1,6 @@ +Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := + Discharge (λ H1, Discharge (λ H2, MP (Conjunct2 H1) (MP (Conjunct1 H1) H2))) + +Set pp::implicit true +Show Environment 1 + diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 5e3f09b18..1e257b1b9 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -570,8 +570,22 @@ class elaborator::imp { } else if (is_simple_ho_match(new_rhs, new_lhs, c.m_ctx)) { delayed = 0; unify_simple_ho_match(new_rhs, new_lhs, c); + } else if (has_assigned_metavar(new_lhs)) { + delayed = 0; + m_constraints.push_back(constraint(instantiate(new_lhs), new_rhs, c)); + } else if (has_assigned_metavar(new_rhs)) { + delayed = 0; + m_constraints.push_back(constraint(new_lhs, instantiate(new_rhs), c)); } else { - throw_unification_exception(c); + m_constraints.push_back(c); + if (delayed == 0) { + last_num_constraints = m_constraints.size(); + delayed++; + } else if (delayed > last_num_constraints) { + throw_unification_exception(c); + } else { + delayed++; + } } } } @@ -700,12 +714,18 @@ public: return m_env; } - expr operator()(expr const & e, elaborator const & elb) { + expr operator()(expr const & e, expr const & expected_type, elaborator const & elb) { m_constraints.clear(); m_metavars.clear(); m_owner = &elb; m_processing_root = true; - m_root = process(e, context()).first; + auto p = process(e, context()); + m_root = p.first; + expr given_type = p.second; + if (expected_type) { + if (has_metavar(given_type)) + m_constraints.push_back(constraint(expected_type, given_type, context(), e, context(), static_cast(-1))); + } if (has_metavar(m_root)) { solve(); return instantiate(m_root); @@ -738,7 +758,8 @@ public: }; elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {} elaborator::~elaborator() {} -expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, *this); } +expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, expr(), *this); } +expr elaborator::operator()(expr const & e, expr const & expected_type) { return (*m_ptr)(e, expected_type, *this); } expr const & elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void elaborator::clear() { m_ptr->clear(); } diff --git a/src/frontends/lean/lean_elaborator.h b/src/frontends/lean/lean_elaborator.h index 96464eac6..1937f92ea 100644 --- a/src/frontends/lean/lean_elaborator.h +++ b/src/frontends/lean/lean_elaborator.h @@ -25,6 +25,7 @@ public: ~elaborator(); expr operator()(expr const & e); + expr operator()(expr const & e, expr const & expected_type); /** \brief If \c e is an expression instantiated by the elaborator, then it diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 538ffdd9f..e397641e3 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -382,7 +382,7 @@ class parser::imp { \brief Return the function associated with the given operator. If the operator has been overloaded, it returns a choice expression of the form (choice f_1 f_2 ... f_k) where f_i's are different options. - After we finish parsing, the procedure #elaborate will + After we finish parsing, the elaborator resolve/decide which f_i should be used. */ expr mk_fun(operator_info const & op) { @@ -1009,10 +1009,6 @@ class parser::imp { } /*@}*/ - expr elaborate(expr const & e) { - return m_elaborator(e); - } - /** @name Parse Commands */ @@ -1043,9 +1039,9 @@ class parser::imp { buffer> bindings; if (curr_is_colon()) { next(); - type = elaborate(parse_expr()); + type = m_elaborator(parse_expr()); check_assign_next("invalid definition, ':=' expected"); - val = elaborate(parse_expr()); + val = m_elaborator(parse_expr(), type); } else { mk_scope scope(*this); parse_object_bindings(bindings); @@ -1053,8 +1049,8 @@ class parser::imp { expr type_body = parse_expr(); check_assign_next("invalid definition, ':=' expected"); expr val_body = parse_expr(); - type = elaborate(mk_abstraction(false, bindings, type_body)); - val = elaborate(mk_abstraction(true, bindings, val_body)); + type = m_elaborator(mk_abstraction(false, bindings, type_body)); + val = m_elaborator(mk_abstraction(true, bindings, val_body), type); } if (is_definition) { m_frontend.add_definition(id, type, val); @@ -1098,13 +1094,13 @@ class parser::imp { expr type; if (curr_is_colon()) { next(); - type = elaborate(parse_expr()); + type = m_elaborator(parse_expr()); } else { mk_scope scope(*this); 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)); + type = m_elaborator(mk_abstraction(false, bindings, type_body)); } if (is_var) m_frontend.add_var(id, type); @@ -1138,7 +1134,7 @@ class parser::imp { /** \brief Parse 'Eval' expr */ void parse_eval() { next(); - expr v = elaborate(parse_expr()); + expr v = m_elaborator(parse_expr()); normalizer norm(m_frontend); scoped_set_interruptable_ptr set(m_normalizer, &norm); expr r = norm(v); @@ -1177,7 +1173,7 @@ class parser::imp { throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos); } } else { - expr v = elaborate(parse_expr()); + expr v = m_elaborator(parse_expr()); regular(m_frontend) << v << endl; } } @@ -1185,7 +1181,7 @@ class parser::imp { /** \brief Parse 'Check' expr */ void parse_check() { next(); - expr v = elaborate(parse_expr()); + expr v = m_elaborator(parse_expr()); expr t = infer_type(v, m_frontend); regular(m_frontend) << t << endl; } @@ -1570,7 +1566,7 @@ public: /** \brief Parse an expression. */ expr parse_expr_main() { try { - return elaborate(parse_expr()); + return m_elaborator(parse_expr()); } catch (parser_error & ex) { throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second); } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 1eba1b228..f46406546 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -3,6 +3,7 @@ include_directories("${LEAN_BINARY_DIR}") add_executable(lean lean.cpp) target_link_libraries(lean ${EXTRA_LIBS}) add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex1.lean") +add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex2.lean") add_test(NAME leantests WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")