From 998f90b849e2c47f496fa58d4e0fd5ae0398071c Mon Sep 17 00:00:00 2001 From: Jared Roesch Date: Thu, 11 May 2017 11:37:57 -0700 Subject: [PATCH] feat(library/init/meta/interactive): add support for location wildcards This allows users to now use to apply a tactic in all hypotheses as well as the goal, we add support for all interactive tactics using location: rewrite, simp, dsimp, unfold, and delta including each tactics many variants. --- library/init/meta/interactive.lean | 80 ++++++++++++++++++++++-------- 1 file changed, 60 insertions(+), 20 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index f9cb99ff8d..f5e67bb88a 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -20,6 +20,18 @@ namespace interactive to the tactic. -/ @[reducible] meta def parse {α : Type} [has_reflect α] (p : parser α) : Type := α +inductive loc : Type +| wildcard : loc +| ns : list name → loc + +def loc.empty := loc.ns [] + +meta instance : has_reflect loc := +fun l, match l with +| loc.wildcard := ```(_) +| loc.ns xs := ```(_) +end + namespace types variables {α β : Type} @@ -37,7 +49,7 @@ 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 without_ident_list := (tk "without" *> ident*) <|> return [] -meta def location := (tk "at" *> ident*) <|> return [] +meta def location := (tk "at" *> (tk "*" *> pure loc.wildcard <|> (loc.ns <$> ident*))) <|> return loc.empty meta def qexpr_list := list_of (qexpr 0) meta def opt_qexpr_list := qexpr_list <|> return [] meta def qexpr_list_or_texpr := qexpr_list <|> list.ret <$> texpr @@ -345,10 +357,14 @@ meta def rw_rules : parser rw_rules_t := <*> (some <$> cur_pos <* set_goal_info_pos (tk "]"))) <|> rw_rules_t.mk <$> (list.ret <$> rw_rule_p texpr) <*> return none -private meta def rw_core (m : transparency) (rs : parse rw_rules) (loc : parse location) : tactic unit := -match loc with -| [] := rw_goal m rs.rules -| hs := rw_hyps m rs.rules hs +private meta def rw_core (m : transparency) (rs : parse rw_rules) (loca : parse location) : tactic unit := +match loca with +| loc.wildcard := +do ls ← local_context, + let ls_names := list.map (fun (l : expr), l.local_pp_name) ls, + ls_names.mfor' (fun loc, try $ rw_hyp m rs.rules loc) +| loc.ns [] := rw_goal m rs.rules +| loc.ns hs := rw_hyps m rs.rules hs end >> try (reflexivity reducible) >> (returnopt rs.end_pos >>= save_info <|> skip) @@ -666,12 +682,18 @@ private meta def simp_hyps (cfg : simp_config) : simp_lemmas → list name → t | s [] := skip | s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs -private meta def simp_core (cfg : simp_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (loc : list name) : tactic unit := +private meta def simp_core (cfg : simp_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (locat : loc) : tactic unit := do s ← mk_simp_set attr_names hs ids, s ← s.append ctx, - match loc : _ → tactic unit with - | [] := simp_goal cfg s - | _ := simp_hyps cfg s loc + match locat : _ → tactic unit with + | loc.wildcard := + do ls ← local_context, + let loc_names := ls.map (fun l, l.local_pp_name), + revert_lst ls, + simp_intro_aux cfg ff s ff loc_names, + return () + | (loc.ns []) := simp_goal cfg s + | (loc.ns hs) := simp_hyps cfg s hs end, try tactic.triv, try (tactic.reflexivity reducible) @@ -692,9 +714,9 @@ It has many variants. - `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`. -/ -meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) +meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (locat : parse location) (cfg : simp_config := {}) : tactic unit := -simp_core cfg [] hs attr_names ids loc +simp_core cfg [] hs attr_names ids locat /-- Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules. @@ -702,7 +724,7 @@ Similar to the `simp` tactic, but adds all applicable hypotheses as simplificati meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := do ctx ← collect_ctx_simps, - simp_core cfg ctx hs attr_names ids [] + simp_core cfg ctx hs attr_names ids (loc.ns []) meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := @@ -732,8 +754,14 @@ private meta def dsimp_hyps (s : simp_lemmas) : list name → tactic unit | (h::hs) := get_local h >>= dsimp_at_core s meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : parse location → tactic unit -| [] := do s ← mk_simp_set attr_names es ids, tactic.dsimp_core s -| hs := do s ← mk_simp_set attr_names es ids, dsimp_hyps s hs +| (loc.ns []) := do s ← mk_simp_set attr_names es ids, tactic.dsimp_core s +| (loc.ns hs) := do s ← mk_simp_set attr_names es ids, dsimp_hyps s hs +| (loc.wildcard) := +do ls ← local_context, + n ← revert_lst ls, + s ← mk_simp_set attr_names es ids, + tactic.dsimp_core s, + intron n /-- This tactic applies to a goal that has the form `t ~ u` where `~` is a reflexive relation. @@ -794,8 +822,13 @@ private meta def dunfold_hyps : list name → list name → tactic unit | cs (h::hs) := get_local h >>= dunfold_at cs >> dunfold_hyps cs hs meta def dunfold : parse ident* → parse location → tactic unit -| cs [] := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs -| cs hs := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs hs +| cs (loc.ns []) := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs +| cs (loc.ns hs) := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs hs +| cs (loc.wildcard) :=do ls ← tactic.local_context, + n ← revert_lst ls, + new_cs ← to_qualified_names cs, + tactic.dunfold new_cs, + intron n /- TODO(Leo): add support for non-refl lemmas -/ meta def unfold : parse ident* → parse location → tactic unit := @@ -806,8 +839,9 @@ private meta def dunfold_hyps_occs : name → occurrences → list name → tact | c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs meta def dunfold_occs : parse ident → parse location → list nat → tactic unit -| c [] ps := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c -| c hs ps := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs +| c (loc.ns []) ps := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c +| c (loc.ns hs) ps := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs +| c (loc.wildcard) ps := sorry /- TODO(Leo): add support for non-refl lemmas -/ meta def unfold_occs : parse ident → parse location → list nat → tactic unit := @@ -818,8 +852,14 @@ private meta def delta_hyps : list name → list name → tactic unit | cs (h::hs) := get_local h >>= delta_at cs >> dunfold_hyps cs hs meta def delta : parse ident* → parse location → tactic unit -| cs [] := do new_cs ← to_qualified_names cs, tactic.delta new_cs -| cs hs := do new_cs ← to_qualified_names cs, delta_hyps new_cs hs +| cs (loc.ns []) := do new_cs ← to_qualified_names cs, tactic.delta new_cs +| cs (loc.ns hs) := do new_cs ← to_qualified_names cs, delta_hyps new_cs hs +| cs (loc.wildcard) := +do ls ← tactic.local_context, + n ← revert_lst ls, + new_cs ← to_qualified_names cs, + tactic.delta new_cs, + intron n meta def apply_opt_param : tactic unit := tactic.apply_opt_param