From 69ed291aab8493a7fb33b52dc2982e2db417761f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Jul 2017 14:05:11 -0700 Subject: [PATCH] refactor(library/init/meta/simp_tactic): `tactic.simp_at` => `tactic.simp_hyp` --- doc/changes.md | 3 +++ library/init/meta/interactive.lean | 17 +++-------------- library/init/meta/simp_tactic.lean | 27 +++++++++------------------ 3 files changed, 15 insertions(+), 32 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index 017845ce31..5c62f3545c 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -88,6 +88,9 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ * `tactic.unfold_projections` => `tactic.unfold_projs_target` * `tactic.unfold_projections_at` => `tactic.unfold_projs_hyp` * `tactic.simp_intros_using`, `tactic.simph_intros_using`, `tactic.simp_intro_lst_using`, `tactic.simph_intro_lst_using` => `tactic.simp_intros` +* `tactic.simp_at` => `tactic.simp_hyp` +* deleted `tactic.simp_at_using` +* deleted `tactic.simph_at` v3.2.0 (18 June 2017) ------------- diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index f04601d452..083ab0e3ad 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -709,20 +709,9 @@ end mk_simp_set namespace interactive open interactive interactive.types expr -private meta def simp_goal (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (u : list name) : tactic unit := -do (new_target, pr) ← target >>= λ t, simplify s u t cfg `eq discharger, - replace_target new_target pr - -private meta def simp_hyp (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (u : list name) (h_name : name) : tactic unit := -do h ← get_local h_name, - h_type ← infer_type h, - (h_new_type, pr) ← simplify s u h_type cfg `eq discharger, - replace_hyp h h_new_type pr, - return () - private meta def simp_hyps (cfg : simp_config) (discharger : tactic unit) (s : simp_lemmas) (u : list name) : list name → tactic unit | [] := skip -| (h::hs) := simp_hyp cfg discharger s u h >> simp_hyps hs +| (h::hs) := do h ← get_local h, simp_hyp s u h cfg discharger, simp_hyps hs meta def simp_core (cfg : simp_config) (discharger : tactic unit) (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) @@ -739,11 +728,11 @@ do (s, u) ← mk_simp_set no_dflt attr_names hs ids, mk_eq_mp pr h >>= tactic.exact >> return tt) <|> (return ff) }, - goal_simplified ← (simp_goal cfg discharger s u >> return tt) <|> (return ff), + goal_simplified ← (simp_target s u cfg discharger >> return tt) <|> (return ff), guard (cfg.fail_if_unchanged = ff ∨ to_remove.length > 0 ∨ goal_simplified) <|> fail "simplify tactic failed to simplify", to_remove.mfor' (λ h, try (clear h)), return () - | (loc.ns []) := simp_goal cfg discharger s u + | (loc.ns []) := simp_target s u cfg discharger | (loc.ns hs) := simp_hyps cfg discharger s u hs end, try tactic.triv, try (tactic.reflexivity reducible) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index faa4ef11a7..561c09d5a0 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -215,14 +215,20 @@ structure simp_config := The parameter `to_unfold` specifies definitions that should be delta-reduced, and projection applications that should be unfolded. -/ -meta constant simplify (s : simp_lemmas) (to_unfold : list name) (e : expr) (cfg : simp_config := {}) (r : name := `eq) +meta constant simplify (s : simp_lemmas) (to_unfold : list name := []) (e : expr) (cfg : simp_config := {}) (r : name := `eq) (discharger : tactic unit := failed) : tactic (expr × expr) -meta def simp_target (S : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit := +meta def simp_target (s : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic unit := do t ← target, - (new_t, pr) ← simplify S to_unfold t cfg `eq discharger, + (new_t, pr) ← simplify s to_unfold t cfg `eq discharger, replace_target new_t pr +meta def simp_hyp (s : simp_lemmas) (to_unfold : list name := []) (h : expr) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic expr := +do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"), + htype ← infer_type h, + (h_new_type, pr) ← simplify s to_unfold htype cfg `eq discharger, + replace_hyp h h_new_type pr + meta constant ext_simplify_core /- The user state type. -/ {α : Type} @@ -319,21 +325,6 @@ step $ simp_intros_aux cfg.to_simp_config cfg.use_hyps to_unfold s (bnot ids.emp end simp_intros -meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr := -do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"), - htype ← infer_type h, - S ← simp_lemmas.mk_default, - S ← S.append extra_lemmas, - (h_new_type, pr) ← simplify S [] htype cfg, - replace_hyp h h_new_type pr - -meta def simp_at_using_hs (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr := -do hs ← collect_ctx_simps, - simp_at h (list.filter (≠ h) hs ++ extra_lemmas) cfg - -meta def simph_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic expr := -simp_at_using_hs h extra_lemmas cfg - meta def mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit := do (lhs, rhs) ← target >>= match_eq, (new_rhs, heq) ← simp_ext lhs,