From 3e757d890a04eaa771e59a785df31766d5eb4552 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Mar 2017 15:42:36 -0800 Subject: [PATCH] feat(library/tactic/intro_tactic): allow '_' in interactive mode as the anonymous name for intros, cases, induction --- library/init/meta/interactive.lean | 12 +++++++----- src/library/tactic/intro_tactic.cpp | 10 +++++----- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 587098c5f4..4ec4c17c5d 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -29,8 +29,10 @@ meta def list_of (p : parser α) := tk "[" *> sep_by "," p <* tk "]" '<|>' (rbp 2), ';' (rbp 1), and ',' (rbp 0). It should be used for any (potentially) trailing expression parameters. -/ meta def texpr := qexpr 2 +/-- Parse an identifier or a '_' -/ +meta def ident_ : parser name := ident <|> tk "_" >> return `_ meta def using_ident := (tk "using" *> ident)? -meta def with_ident_list := (tk "with" *> ident*) <|> return [] +meta def with_ident_list := (tk "with" *> ident_*) <|> return [] meta def without_ident_list := (tk "without" *> ident*) <|> return [] meta def location := (tk "at" *> ident*) <|> return [] meta def qexpr_list := list_of (qexpr 0) @@ -82,7 +84,7 @@ If the goal is an arrow `T → U`, then it puts in the local context either `h:T If the goal is neither a Pi/forall nor starting with a let definition, the tactic `intro` applies the tactic `whnf` until the tactic `intro` can be applied or the goal is not `head-reducible`. -/ -meta def intro : parse ident? → tactic unit +meta def intro : parse ident_? → tactic unit | none := intro1 >> skip | (some h) := tactic.intro h >> skip @@ -90,7 +92,7 @@ meta def intro : parse ident? → tactic unit Similar to `intro` tactic. The tactic `intros` will keep introducing new hypotheses until the goal target is not a Pi/forall or let binder. The variant `intros h_1 ... h_n` introduces `n` new hypotheses using the given identifiers to name them. -/ -meta def intros : parse ident* → tactic unit +meta def intros : parse ident_* → tactic unit | [] := tactic.intros >> skip | hs := intro_lst hs >> skip @@ -496,7 +498,7 @@ meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (cfg : simp_config := {}) : tactic unit := simp_using_hs hs attr_names ids cfg -meta def simp_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) +meta def simp_intros (ids : parse ident_*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := do s ← mk_simp_set attr_names hs wo_ids, match ids with @@ -505,7 +507,7 @@ do s ← mk_simp_set attr_names hs wo_ids, end, try triv >> try (reflexivity reducible) -meta def simph_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) +meta def simph_intros (ids : parse ident_*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := do s ← mk_simp_set attr_names hs wo_ids, match ids with diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp index eb4c2ac7b7..0338ec00b1 100644 --- a/src/library/tactic/intro_tactic.cpp +++ b/src/library/tactic/intro_tactic.cpp @@ -14,11 +14,11 @@ Author: Leonardo de Moura #include "library/tactic/tactic_state.h" namespace lean { -static name mk_aux_name(list & given_names, name const & default_name) { +static name mk_aux_name(local_context const & lctx, list & given_names, name const & default_name) { if (given_names) { name r = head(given_names); given_names = tail(given_names); - return r; + return r == "_" ? lctx.get_unused_name(default_name) : r; } else { return default_name; } @@ -29,7 +29,7 @@ optional intron(environment const & env, options const & opts, metavar_con lean_assert(is_metavar(mvar)); optional g = mctx.find_metavar_decl(mvar); if (!g) return none_expr(); - type_context ctx = mk_type_context_for(env, opts, mctx, g->get_context()); + type_context ctx = mk_type_context_for(env, opts, mctx, g->get_context()); expr type = g->get_type(); type_context::tmp_locals new_locals(ctx); buffer new_Hs; @@ -41,7 +41,7 @@ optional intron(environment const & env, options const & opts, metavar_con } lean_assert(is_pi(type) || is_let(type)); if (is_pi(type)) { - expr H = new_locals.push_local(mk_aux_name(given_names, binding_name(type)), annotated_head_beta_reduce(binding_domain(type)), + expr H = new_locals.push_local(mk_aux_name(ctx.lctx(), given_names, binding_name(type)), annotated_head_beta_reduce(binding_domain(type)), binding_info(type)); type = instantiate(binding_body(type), H); new_Hs.push_back(H); @@ -49,7 +49,7 @@ optional intron(environment const & env, options const & opts, metavar_con } else { lean_assert(is_let(type)); - expr H = new_locals.push_let(mk_aux_name(given_names, let_name(type)), annotated_head_beta_reduce(let_type(type)), let_value(type)); + expr H = new_locals.push_let(mk_aux_name(ctx.lctx(), given_names, let_name(type)), annotated_head_beta_reduce(let_type(type)), let_value(type)); type = instantiate(let_body(type), H); new_Hs.push_back(H); new_Hns.push_back(mlocal_name(H));