From 33b72f1dd092ce184df56227f3eb954880a3450e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Dec 2013 13:09:39 -0800 Subject: [PATCH] feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac) Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 37 +++++++++++++++++------ src/kernel/type_checker_justification.cpp | 14 +++++++++ src/kernel/type_checker_justification.h | 20 ++++++++++++ tests/lean/tactic13.lean | 20 ++++++++++++ tests/lean/tactic13.lean.expected.out | 9 ++++++ 5 files changed, 91 insertions(+), 9 deletions(-) create mode 100644 tests/lean/tactic13.lean create mode 100644 tests/lean/tactic13.lean.expected.out diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 70d865991..3606eb22a 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "kernel/printer.h" #include "kernel/metavar.h" #include "kernel/for_each_fn.h" +#include "kernel/type_checker_justification.h" #include "library/expr_lt.h" #include "library/type_inferer.h" #include "library/arith/arith.h" @@ -43,6 +44,7 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" #include "library/tactic/tactic.h" #include "library/tactic/apply_tactic.h" +#include "library/elaborator/elaborator.h" #include "frontends/lean/frontend.h" #include "frontends/lean/frontend_elaborator.h" #include "frontends/lean/parser.h" @@ -1338,12 +1340,27 @@ class parser::imp { It basically applies the proof_builder if \c s does not contain any goals left. The position information is used to throw an exception if \c s is not a final state. + + The resultant proof must have type \c expected_type in the context \c ctx. */ - expr mk_proof_for(proof_state const & s, pos_info const & p) { + expr mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type) { if (s.is_proof_final_state()) { assignment a(s.get_menv()); proof_map m; expr pr = s.get_proof_builder()(m, a); + if (has_metavar(pr)) { + // Some tactics generate metavariables that can only be instantiated by type inference elaboration. + // Example: apply_tactic. + metavar_env menv = s.get_menv(); + buffer ucs; + expr pr_type = type_checker(m_frontend).infer_type(pr, ctx, &menv, &ucs); + ucs.push_back(mk_convertible_constraint(ctx, pr_type, expected_type, mk_type_match_justification(ctx, expected_type, pr))); + elaborator elb(m_frontend, s.get_menv(), ucs.size(), ucs.data(), m_frontend.get_options()); + metavar_env new_menv = elb.next(); + pr = instantiate_metavars(pr, new_menv); + if (has_metavar(pr)) + throw exception("synthesized proof object has unsolved metavars"); + } return pr; } else { throw tactic_cmd_error("invalid 'done' command, proof cannot be produced from this state", p, s); @@ -1410,16 +1427,18 @@ class parser::imp { \brief Execute the \c done tactic command. It succeeds if a proof for \c s can be built. */ - expr done_cmd(proof_state const & s) { + expr done_cmd(proof_state const & s, context const & ctx, expr const & expected_type) { auto p = pos(); next(); - return mk_proof_for(s, p); + return mk_proof_for(s, p, ctx, expected_type); } /** \brief Parse tactic command sequence for solving input state \c s. + + The proof for \c s must have type \c expected_type in the context \c ctx. */ - expr parse_tactic_cmds(proof_state s) { + expr parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type) { proof_state_seq_stack stack; expr pr; enum class status { Continue, Done, Eof, Abort }; @@ -1446,7 +1465,7 @@ class parser::imp { } else if (id == g_back) { back_cmd(stack, s); } else if (id == g_done) { - pr = done_cmd(s); + pr = done_cmd(s, ctx, expected_type); if (pr) st = status::Done; } else if (id == g_abort) { @@ -1519,12 +1538,12 @@ class parser::imp { if (hint_and_pos.first) { // metavariable has an associated tactic hint s = apply_tactic(s, hint_and_pos.first, hint_and_pos.second).first; - return mk_proof_for(s, hint_and_pos.second); + return mk_proof_for(s, hint_and_pos.second, context(), expected_type); } else { display_proof_state_if_interactive(s); show_tactic_prompt(); check_period_next("invalid theorem, '.' expected before tactical proof"); - return parse_tactic_cmds(s); + return parse_tactic_cmds(s, context(), expected_type); } } else { buffer mvars; @@ -1553,14 +1572,14 @@ class parser::imp { if (hint_and_pos.first) { // metavariable has an associated tactic hint s = apply_tactic(s, hint_and_pos.first, hint_and_pos.second).first; - menv.assign(mvar, mk_proof_for(s, hint_and_pos.second)); + menv.assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type)); } else { if (curr_is_period()) { display_proof_state_if_interactive(s); show_tactic_prompt(); next(); } - expr mvar_val = parse_tactic_cmds(s); + expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type); if (mvar_val) menv.assign(mvar, mvar_val); } diff --git a/src/kernel/type_checker_justification.cpp b/src/kernel/type_checker_justification.cpp index e9529e67d..1c52af185 100644 --- a/src/kernel/type_checker_justification.cpp +++ b/src/kernel/type_checker_justification.cpp @@ -91,4 +91,18 @@ void def_type_match_justification_cell::get_children(buffer expr const & def_type_match_justification_cell::get_main_expr() const { return m_value; } + +type_match_justification_cell::~type_match_justification_cell() { +} + +format type_match_justification_cell::pp_header(formatter const &, options const &) const { + return format("Type of expression must be convertible to expected type."); +} + +void type_match_justification_cell::get_children(buffer &) const { +} + +expr const & type_match_justification_cell::get_main_expr() const { + return m_value; +} } diff --git a/src/kernel/type_checker_justification.h b/src/kernel/type_checker_justification.h index fb90937e5..ebd947527 100644 --- a/src/kernel/type_checker_justification.h +++ b/src/kernel/type_checker_justification.h @@ -120,9 +120,29 @@ public: expr const & get_value() const { return m_value; } }; +/** + \brief Similar to def_type_match_justification_cell. It is used to sign that type of \c m_value + must be convertible to \c m_type at context \c m_ctx. +*/ +class type_match_justification_cell : public justification_cell { + context m_ctx; + expr m_type; + expr m_value; +public: + type_match_justification_cell(context const & c, expr const & t, expr const & v):m_ctx(c), m_type(t), m_value(v) {} + virtual ~type_match_justification_cell(); + virtual format pp_header(formatter const & fmt, options const & opts) const; + virtual void get_children(buffer &) const; + virtual expr const & get_main_expr() const; + context const & get_context() const { return m_ctx; } + expr const & get_type() const { return m_type; } + expr const & get_value() const { return m_value; } +}; + inline justification mk_function_expected_justification(context const & ctx, expr const & app) { return justification(new function_expected_justification_cell(ctx, app)); } inline justification mk_app_type_match_justification(context const & ctx, expr const & app, unsigned i) { return justification(new app_type_match_justification_cell(ctx, app, i)); } inline justification mk_type_expected_justification(context const & ctx, expr const & type) { return justification(new type_expected_justification_cell(ctx, type)); } inline justification mk_max_type_justification(context const & ctx, expr const & type) { return justification(new max_type_justification_cell(ctx, type)); } inline justification mk_def_type_match_justification(context const & ctx, name const & n, expr const & v) { return justification(new def_type_match_justification_cell(ctx, n, v)); } +inline justification mk_type_match_justification(context const & ctx, expr const & t, expr const & v) { return justification(new type_match_justification_cell(ctx, t, v)); } } diff --git a/tests/lean/tactic13.lean b/tests/lean/tactic13.lean new file mode 100644 index 000000000..cef22110a --- /dev/null +++ b/tests/lean/tactic13.lean @@ -0,0 +1,20 @@ +Variable f : Int -> Int -> Int + +(** +refl_tac = apply_tac("Refl") +congr_tac = apply_tac("Congr") +symm_tac = apply_tac("Symm") +trans_tac = apply_tac("Trans") +unfold_homo_eq_tac = unfold_tac("eq") +auto = unfold_homo_eq_tac .. REPEAT(ORELSE(refl_tac, congr_tac, assumption_tac, THEN(symm_tac, assumption_tac, now_tac))) +**) + +Theorem T1 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a). + apply auto. + done. + +Theorem T2 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)). + apply auto. + done. + +Show Environment 2. \ No newline at end of file diff --git a/tests/lean/tactic13.lean.expected.out b/tests/lean/tactic13.lean.expected.out new file mode 100644 index 000000000..8a57a54a4 --- /dev/null +++ b/tests/lean/tactic13.lean.expected.out @@ -0,0 +1,9 @@ + Set: pp::colors + Set: pp::unicode + Assumed: f + Proved: T1 + Proved: T2 +Theorem T1 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a) := + Congr (Congr (Refl f) (Congr (Congr (Refl f) H1) H2)) (Symm H1) +Theorem T2 (a b c : ℤ) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)) := + Congr (Refl f) (Congr (Congr (Refl f) H1) (Symm H2))