From 360e9b94865353a468e372b99e4b5c78bd05f29d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Jun 2014 18:26:07 -0700 Subject: [PATCH] feat(library/tactic): add apply tactic Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_tactic_cmds.cpp | 23 +- src/frontends/lean/cmd_table.h | 2 +- src/frontends/lean/elaborator.cpp | 15 +- src/frontends/lean/local_decls.h | 13 +- src/frontends/lean/parser.cpp | 49 ++- src/frontends/lean/parser.h | 2 + src/kernel/abstract.cpp | 4 +- src/library/tactic/CMakeLists.txt | 4 +- src/library/tactic/apply_tactic.cpp | 337 ++++++--------------- src/library/tactic/apply_tactic.h | 7 +- src/library/tactic/goal.cpp | 10 +- src/library/tactic/goal.h | 1 + src/library/tactic/proof_state.cpp | 8 +- src/library/tactic/proof_state.h | 5 +- src/library/tactic/register_module.h | 4 +- src/library/tactic/tactic.cpp | 7 +- src/library/tactic/tactic.h | 2 +- src/library/unifier.cpp | 5 + src/library/unifier.h | 2 + src/util/lazy_list_fn.h | 16 + tests/lean/run/tactic3.lean | 2 +- tests/lean/run/tactic4.lean | 2 +- tests/lean/run/tactic5.lean | 2 +- tests/lean/run/tactic7.lean | 4 + tests/lean/run/tactic8.lean | 7 + 25 files changed, 250 insertions(+), 283 deletions(-) create mode 100644 tests/lean/run/tactic7.lean create mode 100644 tests/lean/run/tactic8.lean diff --git a/src/frontends/lean/builtin_tactic_cmds.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp index 3e56ba3d7..95b29e95c 100644 --- a/src/frontends/lean/builtin_tactic_cmds.cpp +++ b/src/frontends/lean/builtin_tactic_cmds.cpp @@ -9,14 +9,16 @@ Author: Leonardo de Moura namespace lean { static name g_bang("!"); +tactic parse_fail_tactic(parser &, pos_info const &) { return fail_tactic(); } +tactic parse_id_tactic(parser &, pos_info const &) { return id_tactic(); } +tactic parse_now_tactic(parser &, pos_info const &) { return now_tactic(); } +tactic parse_print_tactic(parser & p, pos_info const & pos) { + return trace_state_tactic(p.get_stream_name(), pos); +} +tactic parse_assumption_tactic(parser &, pos_info const &) { return assumption_tactic(); } +tactic parse_apply_tactic(parser & p, pos_info const &) { return p.parse_apply(); } -tactic parse_fail_tactic(parser &) { return fail_tactic(); } -tactic parse_id_tactic(parser &) { return id_tactic(); } -tactic parse_now_tactic(parser &) { return now_tactic(); } -tactic parse_show_tactic(parser &) { return trace_state_tactic(); } -tactic parse_assumption_tactic(parser &) { return assumption_tactic(); } - -tactic parse_unfold_tactic(parser & p) { +tactic parse_unfold_tactic(parser & p, pos_info const &) { auto pos = p.pos(); expr id = p.parse_expr(); if (!is_constant(id)) @@ -24,7 +26,7 @@ tactic parse_unfold_tactic(parser & p) { return unfold_tactic(const_name(id)); } -tactic parse_repeat_tactic(parser & p) { +tactic parse_repeat_tactic(parser & p, pos_info const &) { tactic t = p.parse_tactic(); if (p.curr_is_numeral()) { unsigned n = p.parse_small_nat(); @@ -34,7 +36,7 @@ tactic parse_repeat_tactic(parser & p) { } } -tactic parse_echo_tactic(parser & p) { +tactic parse_echo_tactic(parser & p, pos_info const &) { if (!p.curr_is_string()) throw parser_error("invalid 'echo' tactic, string expected", p.pos()); tactic r = trace_tactic(p.get_str_val()); @@ -47,11 +49,12 @@ void add_tactic(tactic_cmd_table & t, tactic_cmd_info && info) { t.insert(info.g tactic_cmd_table get_builtin_tactic_cmds() { tactic_cmd_table t; add_tactic(t, tactic_cmd_info("fail", "always fail tactic", parse_fail_tactic)); - add_tactic(t, tactic_cmd_info("show", "show goals tactic", parse_show_tactic)); + add_tactic(t, tactic_cmd_info("print", "print current goals", parse_print_tactic)); add_tactic(t, tactic_cmd_info("now", "succeeds only if all goals have been solved", parse_now_tactic)); add_tactic(t, tactic_cmd_info("echo", "trace tactic: display message", parse_echo_tactic)); add_tactic(t, tactic_cmd_info("unfold", "unfold definition", parse_unfold_tactic)); add_tactic(t, tactic_cmd_info("repeat", "repeat tactic", parse_repeat_tactic)); + add_tactic(t, tactic_cmd_info("apply", "apply tactic", parse_apply_tactic)); add_tactic(t, tactic_cmd_info("!", "repeat tactic", parse_repeat_tactic)); add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic)); add_tactic(t, tactic_cmd_info("assumption", "solve goal if there is an assumption that is identical to the conclusion", diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h index f3fa578c6..3e6ea1589 100644 --- a/src/frontends/lean/cmd_table.h +++ b/src/frontends/lean/cmd_table.h @@ -14,7 +14,7 @@ namespace lean { class parser; typedef std::function command_fn; -typedef std::function tactic_command_fn; +typedef std::function tactic_command_fn; template struct cmd_info_tmpl { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 56d656ffa..8f8e16ab6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -615,10 +615,17 @@ public: if (optional t = get_tactic_for(mvar)) { proof_state_seq seq = (*t)(m_env, m_ios, ps); if (auto r = seq.pull()) { - if (auto pr = to_proof(r->first)) { - subst = subst.assign(mlocal_name(mvar), *pr, justification()); - } else { - display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + try { + if (auto pr = to_proof(r->first)) { + subst = subst.assign(mlocal_name(mvar), *pr, justification()); + } else { + display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + } + } catch (exception & ex) { + regular out(m_env, m_ios); + display_error_pos(out, m_pos_provider, mvar); + out << " proof generation failed\n >> "; + display_error(out, nullptr, ex); } } else { // tactic failed to produce any result diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h index 470d3b523..35b6c8e6c 100644 --- a/src/frontends/lean/local_decls.h +++ b/src/frontends/lean/local_decls.h @@ -20,22 +20,25 @@ namespace lean { template class local_decls { typedef rb_map, name_quick_cmp> map; - typedef list> scopes; + typedef list>> scopes; map m_map; unsigned m_counter; scopes m_scopes; + list m_values; public: local_decls():m_counter(1) {} local_decls(local_decls const & d):m_map(d.m_map), m_counter(d.m_counter), m_scopes(d.m_scopes) {} - void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; } + void insert(name const & k, V const & v) { m_map.insert(k, mk_pair(v, m_counter)); m_counter++; m_values = list(v, m_values); } V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; } unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; } bool contains(name const & k) const { return m_map.contains(k); } - void push() { m_scopes = scopes(mk_pair(m_map, m_counter), m_scopes); } + list const & get_values() const { return m_values; } + void push() { m_scopes = scopes(std::make_tuple(m_map, m_counter, m_values), m_scopes); } void pop() { lean_assert(!is_nil(m_scopes)); - m_map = head(m_scopes).first; - m_counter = head(m_scopes).second; + m_map = std::get<0>(head(m_scopes)); + m_counter = std::get<1>(head(m_scopes)); + m_values = std::get<2>(head(m_scopes)); m_scopes = tail(m_scopes); } struct mk_scope { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ad48da8dc..00a25b423 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -26,6 +26,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/scoped_ext.h" #include "library/error_handling/error_handling.h" +#include "library/tactic/apply_tactic.h" #include "frontends/lean/parser.h" #include "frontends/lean/notation_cmd.h" #include "frontends/lean/elaborator.h" @@ -407,6 +408,8 @@ static name g_max("max"); static name g_imax("imax"); static name g_cup("\u2294"); static name g_import("import"); +static name g_show("show"); +static name g_have("have"); static unsigned g_level_add_prec = 10; static unsigned g_level_cup_prec = 5; @@ -552,6 +555,11 @@ expr parser::elaborate(expr const & e) { return ::lean::elaborate(m_env, m_ios, e, m_hints, &pp); } +expr parser::elaborate(expr const & e, name_generator const & ngen, list const & ctx) { + parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); + return ::lean::elaborate(m_env, m_ios, e, ngen, m_hints, substitution(), ctx, &pp); +} + expr parser::elaborate(environment const & env, expr const & e) { parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); return ::lean::elaborate(env, m_ios, e, m_hints, &pp); @@ -957,6 +965,41 @@ expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, return r; } +tactic parser::parse_apply() { + auto p = pos(); + expr e = parse_expr(); + for_each(e, [&](expr const & e, unsigned) { + if (is_local(e)) { + auto it = get_local(mlocal_name(e)); + lean_assert(it); + if (!it->m_bi.is_contextual()) + throw parser_error(sstream() << "invalid 'apply' tactic, it references non contextual local '" + << local_pp_name(e) << "'", p); + } + return has_local(e); + }); + buffer tmp; + for (parameter const & p : m_local_decls.get_values()) { + if (p.m_bi.is_contextual() && is_local(p.m_local)) + tmp.push_back(p); + } + list ctx = to_list(tmp.begin(), tmp.end()); + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + name_generator ngen = s.ngen(); + auto const & s_locals = s.get_init_locals(); + expr new_e = elaborate(e, ngen.mk_child(), ctx); + proof_state new_s(s, ngen); + buffer tmp; + for (auto const & p : ctx) + tmp.push_back(p.m_local); + std::reverse(tmp.begin(), tmp.end()); + new_e = abstract_locals(new_e, tmp.size(), tmp.data()); + for (auto const & l : s_locals) + new_e = instantiate(new_e, l); + return apply_tactic(new_e)(env, ios, new_s); + }); +} + tactic parser::parse_tactic(unsigned /* rbp */) { if (curr_is_token(g_lparen) || curr_is_token(g_lbracket)) { bool paren = curr_is_token(g_lparen); @@ -989,20 +1032,22 @@ tactic parser::parse_tactic(unsigned /* rbp */) { } return r; } + } else if (curr_is_token(g_have) || curr_is_token(g_show)) { + return parse_apply(); } else { name id; auto p = pos(); if (curr_is_identifier()) { id = get_name_val(); next(); - } else if (curr_is_keyword()) { + } else if (curr_is_keyword() || curr_is_command()) { id = get_token_info().value(); next(); } else { throw parser_error("invalid tactic, '(' or tactic command expected", p); } if (auto it = tactic_cmds().find(id)) { - return it->get_fn()(*this); + return it->get_fn()(*this, p); } else { throw parser_error(sstream() << "unknown tactic command '" << id << "'", p); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 92ff13cea..c45b5ff00 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -227,6 +227,7 @@ public: expr pi_abstract(buffer const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); } tactic parse_tactic(unsigned rbp = 0); + tactic parse_apply(); struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); }; void add_local_level(name const & n, level const & l); @@ -263,6 +264,7 @@ public: struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); }; expr elaborate(expr const & e); + expr elaborate(expr const & e, name_generator const & ngen, list const & ctx); expr elaborate(environment const & env, expr const & e); std::pair elaborate(name const & n, expr const & t, expr const & v); diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index b37437cce..d3c22c426 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -35,11 +35,11 @@ expr abstract_locals(expr const & e, unsigned n, expr const * subst) { return replace(e, [=](expr const & m, unsigned offset) -> optional { if (!has_local(m)) return some_expr(m); // expression m does not contain local constants - if (closed(e)) { + if (is_local(m)) { unsigned i = n; while (i > 0) { --i; - if (subst[i] == m) + if (mlocal_name(subst[i]) == mlocal_name(m)) return some_expr(copy_tag(m, mk_var(offset + n - i - 1))); } } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index c7b42fd37..776f1e244 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,6 +1,6 @@ -add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp proof_state.cpp tactic.cpp) +add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp proof_state.cpp + tactic.cpp apply_tactic.cpp) -# apply_tactic.cpp # simplify_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index daa73825a..f6d4e28a3 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -1,257 +1,122 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include -#include "util/sstream.h" -#include "kernel/environment.h" +#include "util/lazy_list_fn.h" +#include "kernel/for_each_fn.h" #include "kernel/instantiate.h" -#include "kernel/type_checker.h" #include "kernel/abstract.h" -#include "kernel/replace_visitor.h" -#include "library/io_state_stream.h" -#include "library/fo_unify.h" -#include "library/placeholder.h" +#include "kernel/type_checker.h" #include "library/kernel_bindings.h" -#include "library/elaborator/elaborator.h" -#include "library/tactic/goal.h" -#include "library/tactic/proof_builder.h" -#include "library/tactic/proof_state.h" -#include "library/tactic/tactic.h" +#include "library/unifier.h" #include "library/tactic/apply_tactic.h" -#include "kernel/formatter.h" - namespace lean { -static name g_tmp_mvar_name = name::mk_internal_unique_name(); -// The proof is based on an application of a function that returns a proof. -// There are two kinds of arguments: -// 1) regular arguments computed using unification. -// 2) propositions that generate new subgoals. -typedef std::pair proposition_arg; -// We use a pair to simulate this "union" type. -typedef list, optional>> arg_list; - /** - \brief Return the proof builder for the apply_tactic. - - It solves the goal \c gname by applying \c th_fun to the arguments \c alist. + \brief Traverse \c e and collect metavariable applications (?m l1 ... ln), and store in result. + The function only succeeds if all metavariable applications are "simple", i.e., the arguments + are distinct local constants. */ -proof_builder mk_apply_tac_proof_builder(proof_builder const & pb, name const & gname, expr const & th_fun, arg_list const & alist) { - return mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { - proof_map new_m(m); - if (alist) { - buffer args; - args.push_back(th_fun); - for (auto const & p2 : alist) { - optional const & arg = p2.first; - if (arg) { - // TODO(Leo): decide if we instantiate the metavars in the end or not. - args.push_back(*arg); - } else { - proposition_arg const & parg = *(p2.second); - name const & subgoal_name = parg.first; - expr pr = find(m, subgoal_name); - for (auto p : parg.second) - pr = Fun(p.first, p.second, pr); - args.push_back(pr); - new_m.erase(subgoal_name); +bool collect_simple_metas(expr const & e, buffer & result) { + bool failed = false; + // collect metavariables + for_each(e, [&](expr const & e, unsigned) { + if (is_meta(e)) { + if (!is_simple_meta(e)) { + failed = true; + } else { + result.push_back(e); + return false; /* do not visit type */ + } + } + return !failed && has_metavar(e); + }); + return !failed; +} + +tactic apply_tactic(expr const & e) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + precision prec = s.get_precision(); + if ((prec != precision::Precise && prec != precision::Over) || empty(s.get_goals())) { + // it is pointless to apply this tactic, since it will produce UnderOver + return proof_state_seq(); + } + goals const & gs = s.get_goals(); + name gname = head(gs).first; + goal g = head(gs).second; + goals rest_gs = tail(gs); + expr const & C = g.get_conclusion(); + name_generator ngen = s.ngen(); + type_checker tc(env, ngen.mk_child()); + expr new_e = e; + expr new_e_type = tc.infer(new_e); + buffer meta_buffer; + if (!collect_simple_metas(new_e, meta_buffer)) + return proof_state_seq(); + // add more metavariables while new_e_type is a Pi + while (is_pi(new_e_type)) { + expr meta = g.mk_meta(ngen.next(), binding_domain(new_e_type)); + meta_buffer.push_back(meta); + new_e = mk_app(new_e, meta); + new_e_type = instantiate(binding_body(new_e_type), meta); + } + list metas = to_list(meta_buffer.begin(), meta_buffer.end()); + // TODO(Leo): we should use unifier plugin + lazy_list substs = unify(env, C, new_e_type, ngen.mk_child(), ios.get_options()); + return map2(substs, [=](substitution const & subst) -> proof_state { + // apply substitution to remaining goals + name_generator new_ngen(ngen); + type_checker tc(env, new_ngen.mk_child()); + goals new_gs = map(rest_gs, [&](named_goal const & ng) { + return named_goal(ng.first, ng.second.instantiate_metavars(subst)); + }); + expr P = subst.instantiate_metavars_wo_jst(new_e); + goal tmp_g = g.instantiate_metavars(subst); + unsigned subgoal_idx = 1; + buffer> trace_buffer; + // add unassigned metavariables as new goals + buffer subgoals; + for (expr const & meta : metas) { + if (!subst.is_assigned(get_app_fn(meta))) { + name new_gname(gname, subgoal_idx); + expr new_C = subst.instantiate_metavars_wo_jst(tc.infer(meta)); + goal new_g(tmp_g.get_hypotheses(), new_C); + subgoals.emplace_back(new_gname, new_g); + trace_buffer.emplace_back(new_gname, meta); + subgoal_idx++; + } } - } - std::reverse(args.begin() + 1, args.end()); - new_m.insert(gname, mk_app(args)); - } else { - new_m.insert(gname, th_fun); - } - return pb(new_m, a); + new_gs = to_list(subgoals.begin(), subgoals.end(), new_gs); + list> trace = to_list(trace_buffer.begin(), trace_buffer.end()); + proof_builder pb = s.get_pb(); + proof_builder new_pb([=](proof_map const & m, substitution const & pb_subst) { + proof_map new_m(m); + substitution new_subst; + for (auto const & p : trace) { + expr pr = find(new_m, p.first); + expr meta = p.second; + buffer meta_args; + expr mvar = get_app_args(meta, meta_args); + unsigned i = meta_args.size(); + while (i > 0) { + --i; + pr = Fun(meta_args[i], pr); + } + new_subst = new_subst.assign(mlocal_name(mvar), pr, justification()); + new_m.erase(p.first); + } + new_m.insert(gname, new_subst.instantiate_metavars_wo_jst(P)); + return pb(new_m, pb_subst); + }); + return proof_state(s, new_gs, new_pb, new_ngen); + }); }); } -/** - \brief Functional object for replacing placeholders with - metavariables and attaching type to constants that refer - hypotheses in the given goal. -*/ -class apply_tactic_preprocessor_fn : public replace_visitor { - ro_environment const & m_env; - metavar_env const & m_menv; - hypotheses const & m_hypotheses; -protected: - expr visit_constant(expr const & e, context const & c) { - if (is_placeholder(e)) { - return m_menv->mk_metavar(c, const_type(e)); - } else if (m_env->find_object(const_name(e))) { - return e; - } else { - for (auto const & p : m_hypotheses) { - if (p.first == const_name(e)) - return mk_constant(const_name(e), p.second); - } - throw exception(sstream() << "apply_tactic failed, unknown identifier '" << const_name(e) << "'"); - } - } - -public: - apply_tactic_preprocessor_fn(ro_environment const & env, metavar_env const & menv, hypotheses const & hs): - m_env(env), m_menv(menv), m_hypotheses(hs) {} -}; - -/** - \brief Functional object for moving the metavariable occurring in an expression to - another metavar environment. -*/ -class move_metavars_fn : public replace_visitor { - name_map m_map; - metavar_env const & m_menv; - expr visit_metavar(expr const & mvar, context const &) { - name const & mvar_name = metavar_name(mvar); - auto it = m_map.find(mvar_name); - if (it == m_map.end()) { - expr r = m_menv->mk_metavar(); - m_map[mvar_name] = r; - return r; - } else { - return it->second; - } - } -public: - move_metavars_fn(metavar_env const & menv):m_menv(menv) {} -}; - -static optional apply_tactic_core(ro_environment const & env, proof_state const & s, - expr th, expr th_type, metavar_env const & new_menv) { - type_checker checker(env); - auto const & p = head(s.get_goals()); - name const & gname = p.first; - goal const & g = p.second; - expr conclusion = th_type; - buffer mvars; - unsigned i = 0; - while (is_pi(conclusion)) { - expr mvar = new_menv->mk_metavar(); - mvars.push_back(mvar); - conclusion = instantiate(abst_body(conclusion), mvar, new_menv); - i++; - } - optional subst = fo_unify(conclusion, g.get_conclusion()); - if (!subst) { - return none_proof_state(); - } - th_type = apply(*subst, th_type); - th = apply(*subst, th); - arg_list alist; - unsigned new_goal_idx = 1; - buffer> new_goals_buf; - for (auto const & mvar : mvars) { - expr mvar_subst = apply(*subst, mvar); - if (mvar_subst != mvar) { - alist = cons(mk_pair(some_expr(mvar_subst), optional()), alist); - th_type = instantiate(abst_body(th_type), mvar_subst, new_menv); - } else { - expr arg_type = abst_domain(th_type); - if (checker.is_flex_proposition(arg_type, context(), new_menv)) { - name new_gname(gname, new_goal_idx); - new_goal_idx++; - hypotheses hs = g.get_hypotheses(); - update_hypotheses_fn add_hypothesis(hs); - hypotheses extra_hs; - while (is_pi(arg_type)) { - expr d = abst_domain(arg_type); - name n = arg_to_hypothesis_name(abst_name(arg_type), d, env, context(), new_menv); - n = add_hypothesis(n, d); - extra_hs.emplace_front(n, d); - arg_type = instantiate(abst_body(arg_type), mk_constant(n, d), new_menv); - } - alist = cons(mk_pair(none_expr(), some(proposition_arg(new_gname, extra_hs))), alist); - new_goals_buf.emplace_back(new_gname, goal(add_hypothesis.get_hypotheses(), arg_type)); - th_type = instantiate(abst_body(th_type), mk_constant(new_gname, arg_type), new_menv); - } else { - // we have to create a new metavar in menv - // since we do not have a substitution for mvar, and - // it is not a proposition - /// expr new_m = new_menv->mk_metavar(context(), some_expr(arg_type)); - alist = cons(mk_pair(some_expr(mvar), optional()), alist); - th_type = instantiate(abst_body(th_type), mvar, new_menv); - } - } - } - proof_builder pb = s.get_proof_builder(); - proof_builder new_pb = mk_apply_tac_proof_builder(pb, gname, th, alist); - goals new_gs = to_list(new_goals_buf.begin(), new_goals_buf.end(), tail(s.get_goals())); - return some(proof_state(precision::Over, new_gs, new_menv, new_pb, s.get_cex_builder())); -} - - -static optional apply_tactic(ro_environment const & env, proof_state const & s, - expr th, optional const & th_type) { - precision prec = s.get_precision(); - if ((prec != precision::Precise && prec != precision::Over) || empty(s.get_goals())) { - // it is pointless to apply this tactic, since it will produce UnderOver - return none_proof_state(); - } - if (th_type) { - metavar_env new_menv = s.get_menv().copy(); - return apply_tactic_core(env, s, th, *th_type, new_menv); - } else { - metavar_env tmp_menv; - type_checker checker(env); - auto const & p = head(s.get_goals()); - goal const & g = p.second; - buffer ucs; - th = apply_tactic_preprocessor_fn(env, tmp_menv, g.get_hypotheses())(th); - expr th_type_inferred = checker.check(th, context(), tmp_menv, ucs); - elaborator elb(env, tmp_menv, ucs.size(), ucs.data()); - try { - while (true) { - metavar_env new_tmp_menv = elb.next(); - metavar_env new_menv = s.get_menv().copy(); - move_metavars_fn move(new_menv); - expr new_th = move(new_tmp_menv->instantiate_metavars(th)); - expr new_th_type_inferred = move(new_tmp_menv->instantiate_metavars(th_type_inferred)); - auto r = apply_tactic_core(env, s, new_th, new_th_type_inferred, new_menv); - if (r) - return r; - } - } catch (exception & ex) { - return none_proof_state(); - } - } -} - -tactic apply_tactic(expr const & th) { - return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { - // th may contain placeholder - // TODO(Leo) - return apply_tactic(env, s, th, none_expr()); - }); -} - -tactic apply_tactic(expr const & th, expr const & th_type) { - return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { - return apply_tactic(env, s, th, some_expr(th_type)); - }); -} - -tactic apply_tactic(name const & th_name) { - return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { - optional obj = env->find_object(th_name); - if (obj && (obj->is_theorem() || obj->is_axiom())) - return apply_tactic(env, s, mk_constant(th_name), some_expr(obj->get_type())); - else - return none_proof_state(); - }); -} - -int mk_apply_tactic(lua_State * L) { - if (is_expr(L, 1)) - return push_tactic(L, apply_tactic(to_expr(L, 1))); - else - return push_tactic(L, apply_tactic(to_name_ext(L, 1))); -} - +int mk_apply_tactic(lua_State * L) { return push_tactic(L, apply_tactic(to_expr(L, 1))); } void open_apply_tactic(lua_State * L) { SET_GLOBAL_FUN(mk_apply_tactic, "apply_tac"); } diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index aeead74d0..a9abc95e6 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -1,14 +1,13 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lua.h" #include "library/tactic/tactic.h" namespace lean { -tactic apply_tactic(expr const & th); -tactic apply_tactic(expr const & th, expr const & th_type); -tactic apply_tactic(name const & th_name); +tactic apply_tactic(expr const & e); void open_apply_tactic(lua_State * L); } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index a042fd7f8..33fa14d6a 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -82,7 +82,7 @@ expr goal::mk_meta(name const & n, expr const & type) const { if (is_local(e)) { bool found = false; for (hypothesis const & h : m_hypotheses) { - if (h.second && h.first == e) { + if (mlocal_name(h.first) == mlocal_name(e)) { found = true; break; } @@ -112,6 +112,14 @@ expr goal::mk_meta(name const & n, expr const & type) const { return mk_app(mk_metavar(n, t), args); } +goal goal::instantiate_metavars(substitution const & s) const { + hypotheses hs = map(m_hypotheses, [&](hypothesis const & h) { + return mk_pair(s.instantiate_metavars_wo_jst(h.first), h.second); + }); + expr c = s.instantiate_metavars_wo_jst(m_conclusion); + return goal(hs, c); +} + static bool validate(expr const & r, hypotheses const & hs) { bool failed = false; for_each(r, [&](expr const & e, unsigned) { diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 187605584..4b6df96d8 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -40,6 +40,7 @@ public: and each hypothesis only contains local constants that occur in the previous hypotheses. */ bool validate() const; + goal instantiate_metavars(substitution const & s) const; format pp(environment const & env, formatter const & fmt, options const & opts) const; }; diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 6169a9299..d3724807e 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -146,11 +146,9 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons optional to_proof(proof_state const & s) { if (s.is_proof_final_state()) { - try { - substitution a; - proof_map m; - return some_expr(s.get_pb()(m, a)); - } catch (...) {} + substitution a; + proof_map m; + return some_expr(s.get_pb()(m, a)); } return none_expr(); } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 0d0b08e6e..843d1e6c3 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -15,7 +15,8 @@ Author: Leonardo de Moura #include "library/tactic/cex_builder.h" namespace lean { -typedef list> goals; +typedef std::pair named_goal; +typedef list goals; /** \brief Return the name of the i-th goal, return none if i == 0 or i > size(g) */ optional get_ith_goal_name(goals const & gs, unsigned i); @@ -50,6 +51,8 @@ public: proof_state(s.m_precision, gs, pb, s.m_cex_builder, ngen, s.m_init_locals) {} proof_state(proof_state const & s, goals const & gs, proof_builder const & pb):proof_state(s, gs, pb, s.m_ngen) {} proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_proof_builder) {} + proof_state(proof_state const & s, name_generator const & ngen): + proof_state(s.m_precision, s.m_goals, s.m_proof_builder, s.m_cex_builder, ngen, s.m_init_locals) {} precision get_precision() const { return m_precision; } goals const & get_goals() const { return m_goals; } proof_builder const & get_pb() const { return m_proof_builder; } diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index 4dd71eb65..3b22b80d3 100644 --- a/src/library/tactic/register_module.h +++ b/src/library/tactic/register_module.h @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "library/tactic/proof_builder.h" #include "library/tactic/proof_state.h" #include "library/tactic/tactic.h" -// #include "library/tactic/apply_tactic.h" +#include "library/tactic/apply_tactic.h" // #include "library/tactic/simplify_tactic.h" namespace lean { @@ -19,7 +19,7 @@ inline void open_tactic_module(lua_State * L) { open_proof_builder(L); open_proof_state(L); open_tactic(L); - // open_apply_tactic(L); + open_apply_tactic(L); // open_simplify_tactic(L); } inline void register_tactic_module() { diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 0dff14ea0..e47b94c04 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -84,9 +84,10 @@ tactic trace_tactic(char const * msg) { return trace_tactic(std::string(msg)); } -tactic trace_state_tactic() { +tactic trace_state_tactic(std::string const & fname, std::pair const & pos) { return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state { - diagnostic(env, ios) << s << endl; + diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n" + << s << endl; ios.get_diagnostic_channel().get_stream().flush(); return s; }); @@ -517,7 +518,6 @@ static int mk_now_tactic(lua_State * L) { return push_tactic(L, now_tac static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_tactic()); } static int mk_trace_tactic(lua_State * L) { return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); } static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); } -static int mk_trace_state_tactic(lua_State * L) { return push_tactic(L, trace_state_tactic()); } static int mk_unfold_tactic(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 0) @@ -567,7 +567,6 @@ void open_tactic(lua_State * L) { SET_GLOBAL_FUN(mk_id_tactic, "id_tac"); SET_GLOBAL_FUN(mk_now_tactic, "now_tac"); SET_GLOBAL_FUN(mk_fail_tactic, "fail_tac"); - SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tac"); SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tac"); SET_GLOBAL_FUN(mk_unfold_tactic, "unfold_tac"); SET_GLOBAL_FUN(mk_beta_tactic, "beta_tac"); diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index c5a612bb6..4aecdf409 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -41,7 +41,7 @@ class sstream; tactic trace_tactic(sstream const & msg); tactic trace_tactic(std::string const & msg); /** \brief Return a tactic that just displays the input state in the diagnostic channel. */ -tactic trace_state_tactic(); +tactic trace_state_tactic(std::string const & fname, std::pair const & pos); /** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */ tactic suppress_trace(tactic const & t); /** \brief Return a tactic that performs \c t1 followed by \c t2. */ diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index a2babde6f..5f41ec344 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -46,6 +46,11 @@ optional is_simple_meta(expr const & e, buffer & args) { return some_expr(m); } +bool is_simple_meta(expr const & e) { + buffer args; + return (bool)is_simple_meta(e, args); // NOLINT +} + // Return true if all local constants in \c e are in locals bool context_check(expr const & e, buffer const & locals) { bool failed = false; diff --git a/src/library/unifier.h b/src/library/unifier.h index 7f9b33121..9ea4fe359 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -23,6 +23,8 @@ namespace lean { unsigned get_unifier_max_steps(options const & opts); bool get_unifier_use_exceptions(options const & opts); +bool is_simple_meta(expr const & e); + enum class unify_status { Solved, Failed, Unsupported }; /** \brief Handle the easy-cases: first-order unification, higher-order patterns, identical terms, and terms without metavariables. diff --git a/src/util/lazy_list_fn.h b/src/util/lazy_list_fn.h index b7688cf74..758666c07 100644 --- a/src/util/lazy_list_fn.h +++ b/src/util/lazy_list_fn.h @@ -122,6 +122,22 @@ lazy_list map(lazy_list const & l, F && f, char const * cname = "lazy list }); } +/** + \brief Create a lazy list by applying \c f to the elements of \c l. +*/ +template +lazy_list map2(lazy_list const & l, F && f, char const * cname = "lazy list") { + return mk_lazy_list([=]() { + typename lazy_list::maybe_pair p = l.pull(); + if (!p) { + return typename lazy_list::maybe_pair(); + } else { + check_system(cname); + return some(mk_pair(f(p->first), map2(p->second, f, cname))); + } + }); +} + /** \brief Create a lazy list that contains only the elements of \c l that satisfies \c pred. diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean index 519a41b27..cacc82be7 100644 --- a/tests/lean/run/tactic3.lean +++ b/tests/lean/run/tactic3.lean @@ -1,6 +1,6 @@ import logic theorem tst {A B : Bool} (H1 : A) (H2 : B) : A -:= by [echo "first try", show, now | +:= by [echo "first try", print, now | echo "second try", fail | echo "third try", exact] diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean index 28fee62b1..c211ec1cf 100644 --- a/tests/lean/run/tactic4.lean +++ b/tests/lean/run/tactic4.lean @@ -3,4 +3,4 @@ import logic definition id {A : Type} (a : A) := a theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A -:= by [unfold id, show, exact] +:= by [unfold id, print, exact] diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean index 668df0a93..2c3b589a1 100644 --- a/tests/lean/run/tactic5.lean +++ b/tests/lean/run/tactic5.lean @@ -3,4 +3,4 @@ import logic definition id {A : Type} (a : A) := a theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A -:= by [!(unfold id, show), exact] +:= by [!(unfold id, print), exact] diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean new file mode 100644 index 000000000..88fc108ee --- /dev/null +++ b/tests/lean/run/tactic7.lean @@ -0,0 +1,4 @@ +import logic + +theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A +:= by (print, apply and_intro, print, exact, apply and_intro, print, !exact) diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean new file mode 100644 index 000000000..dd75d7bda --- /dev/null +++ b/tests/lean/run/tactic8.lean @@ -0,0 +1,7 @@ +import logic + +theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A +:= by (apply and_intro, + show A, from H1, + show B ∧ A, from and_intro H2 H1) +check @tst \ No newline at end of file