From 3aec70b92c12a70113a6cb3cca1b8bf714eafa1f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Oct 2014 18:34:45 -0700 Subject: [PATCH] feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time --- library/tools/tactic.lean | 2 +- src/library/tactic/exact_tactic.cpp | 52 +++++++++++++++++++---------- 2 files changed, 35 insertions(+), 19 deletions(-) diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 58c3596b3..f3c176797 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -57,7 +57,7 @@ notation `intros` := intro_list expr_list.nil notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_list l opaque definition unfold {B : Type} (b : B) : tactic := builtin -opaque definition exact {B : Type} (b : B) : tactic := builtin +opaque definition exact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin infixl `;`:15 := and_then notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 945a1a8a6..e3cc17caf 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -5,29 +5,45 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/type_checker.h" +#include "library/unifier.h" +#include "library/reducible.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" namespace lean { -tactic exact_tactic(expr const & _e) { - return tactic01([=](environment const & env, io_state const &, proof_state const & s) { - type_checker tc(env); +tactic exact_tactic(elaborate_fn const & elab, expr const & e) { + return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { + name_generator ngen = s.get_ngen(); substitution subst = s.get_subst(); goals const & gs = s.get_goals(); - goal const & g = head(gs); - expr e = subst.instantiate(_e); - auto e_t_cs = tc.infer(e); - expr e_t = subst.instantiate(e_t_cs.first); - expr t = subst.instantiate(g.get_type()); - auto dcs = tc.is_def_eq(e_t, t); - if (dcs.first && !dcs.second && !e_t_cs.second) { - expr new_p = g.abstract(e); - check_has_no_local(new_p, _e, "exact"); - subst.assign(g.get_name(), new_p); - return some(proof_state(s, tail(gs), subst)); - } else { + if (empty(gs)) return none_proof_state(); + goal const & g = head(gs); + expr new_e; + buffer cs; + auto ecs = elab(g, ngen.mk_child(), e); + new_e = ecs.first; + to_buffer(ecs.second, cs); + to_buffer(s.get_postponed(), cs); + unifier_config cfg(ios.get_options()); + unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg); + if (auto p = rseq.pull()) { + substitution new_subst = p->first.first; + constraints new_postponed = p->first.second; + new_e = new_subst.instantiate(new_e); + bool relax_main_opaque = true; + auto tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque); + auto e_t_cs = tc->infer(new_e); + expr t = new_subst.instantiate(g.get_type()); + auto dcs = tc->is_def_eq(e_t_cs.first, t); + if (dcs.first && !dcs.second && !e_t_cs.second) { + expr new_p = g.abstract(new_e); + check_has_no_local(new_p, e, "exact"); + new_subst.assign(g.get_name(), new_p); + return some(proof_state(tail(gs), new_subst, ngen, new_postponed)); + } } + return none_proof_state(); }); } @@ -39,9 +55,9 @@ void initialize_exact_tactic() { name exact_tac_name({"tactic", "exact"}); g_exact_tac_fn = new expr(Const(exact_tac_name)); register_tac(exact_tac_name, - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - // TODO(Leo): use elaborate_fn - return exact_tactic(app_arg(e)); + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument"); + return exact_tactic(fn, get_tactic_expr_expr(app_arg(e))); }); } void finalize_exact_tactic() {