max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/meta/tactic): add option for not creating new subgoals at to_expr

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-28 16:46:29 -07:00
parent 6669ff2132
commit 103b5d09b3
2 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/meta/tactic.lean
View file

@ -326,9 +326,8 @@ meta constant subst : expr → tactic unit
the target type. -/
meta constant exact (e : expr) (md := semireducible) : tactic unit
/-- Elaborate the given quoted expression with respect to the current main goal.
If `allow_mvars` is tt, then metavariables are tolerated and become new goals.
If `report_errors` is ff, then errors are reported using position information from q. -/
meta constant to_expr (q : pexpr) (allow_mvars := tt) : tactic expr
If `allow_mvars` is tt, then metavariables are tolerated and become new goals if `subgoals` is tt. -/
meta constant to_expr (q : pexpr) (allow_mvars := tt) (subgoals := tt) : tactic expr
/-- Return true if the given expression is a type class. -/
meta constant is_class : expr → tactic bool
/-- Try to create an instance of the given type class. -/

9
src/library/tactic/elaborate.cpp
View file

@ -20,7 +20,7 @@ expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
vm_obj tactic_to_expr_core(vm_obj const & qe, vm_obj const & relaxed, vm_obj const & _s) {
vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & allow_mvars, vm_obj const & subgoals, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
@ -31,13 +31,12 @@ vm_obj tactic_to_expr_core(vm_obj const & qe, vm_obj const & relaxed, vm_obj con
bool recover_from_errors = false;
elaborator elab(env, s.get_options(), s.decl_name(), mctx, g->get_context(), recover_from_errors);
expr r = elab.elaborate(resolve_names(env, g->get_context(), e));
if (!to_bool(relaxed))
if (!to_bool(allow_mvars))
elab.ensure_no_unassigned_metavars(r);
mctx = elab.mctx();
env = elab.env();
r = mctx.instantiate_mvars(r);
if (to_bool(relaxed) && has_expr_metavar(r)) {
if (to_bool(subgoals) && has_expr_metavar(r)) {
buffer<expr> new_goals;
name_set found;
for_each(r, [&](expr const & e, unsigned) {
@ -64,7 +63,7 @@ vm_obj tactic_to_expr_core(vm_obj const & qe, vm_obj const & relaxed, vm_obj con
void initialize_elaborate() {
g_by_name = new name("by");
register_annotation(*g_by_name);
DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}), tactic_to_expr_core);
DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}), tactic_to_expr);
}
void finalize_elaborate() {