From abef98c772fd606d85ec0a37822dc1b7cd8914d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Jul 2017 21:36:17 -0700 Subject: [PATCH] refactor(library/init/meta/simp_tactic): make sure `dunfold` tactics use name convention used at `simp`, `dsimp`, ... --- library/init/meta/declaration.lean | 4 ++++ library/init/meta/interactive.lean | 6 +++--- library/init/meta/simp_tactic.lean | 19 ++++++++++++------- library/init/meta/well_founded_tactics.lean | 6 +++--- src/library/tactic/unfold_tactic.cpp | 8 ++++---- tests/lean/unfold1.lean | 4 ++-- tests/lean/unfold_crash.lean | 4 ++-- 7 files changed, 30 insertions(+), 21 deletions(-) diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index e664038bcb..fc75f7bbae 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -121,6 +121,10 @@ meta def to_definition : declaration → declaration | (ax n ls t) := thm n ls t (task.pure (default expr)) | d := d +meta def is_definition : declaration → bool +| (defn _ _ _ _ _ _) := tt +| _ := ff + /-- Instantiate a universe polymorphic declaration type with the given universes. -/ meta constant instantiate_type_univ_params : declaration → list level → option expr diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index ce5c196f87..8c37082dd1 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -906,16 +906,16 @@ private meta def to_qualified_names : list name → tactic (list name) private meta def dunfold_hyps (cs : list name) (cfg : dunfold_config) : list name → tactic unit | [] := skip -| (h::hs) := do h' ← get_local h, dunfold_at cs h' cfg, dunfold_hyps hs +| (h::hs) := do h' ← get_local h, dunfold_hyp cs h' cfg, dunfold_hyps hs meta def dunfold (cs : parse ident*) (l : parse location) (cfg : dunfold_config := {}) : tactic unit := match l with -| (loc.ns []) := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs cfg +| (loc.ns []) := do new_cs ← to_qualified_names cs, dunfold_target new_cs cfg | (loc.ns hs) := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs cfg hs | (loc.wildcard) := do ls ← tactic.local_context, n ← revert_lst ls, new_cs ← to_qualified_names cs, - tactic.dunfold new_cs cfg, + dunfold_target new_cs cfg, intron n end diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 561c09d5a0..0398a796fb 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -129,19 +129,23 @@ do s ← get_simp_lemmas_or_default s, revert_and_transform (λ e, s.dsimplify u (@has_add.add nat nat.has_add a b) -/ -/-- If `e` is a projection application, try to unfold it, otherwise fail. -/ -meta constant dunfold_expr (e : expr) (md := transparency.instances) : tactic expr +/-- Tries to unfold `e` if it is a constant or a constant application. + Remark: this is not a recursive procedure. -/ +meta constant dunfold_head (e : expr) (md := transparency.instances) : tactic expr structure dunfold_config extends dsimp_config := (md := transparency.instances) -meta constant dunfold_core (cs : list name) (e : expr) (cfg : dunfold_config := {}) : tactic expr +/- Remark: in principle, dunfold can be implemented on top of dsimp. We don't do it for + performance reasons. -/ -meta def dunfold (cs : list name) (cfg : dunfold_config := {}) : tactic unit := -do t ← target, dunfold_core cs t cfg >>= unsafe_change +meta constant dunfold (cs : list name) (e : expr) (cfg : dunfold_config := {}) : tactic expr -meta def dunfold_at (cs : list name) (h : expr) (cfg : dunfold_config := {}) : tactic unit := -revert_and_transform (λ e, dunfold_core cs e cfg) h +meta def dunfold_target (cs : list name) (cfg : dunfold_config := {}) : tactic unit := +do t ← target, dunfold cs t cfg >>= unsafe_change + +meta def dunfold_hyp (cs : list name) (h : expr) (cfg : dunfold_config := {}) : tactic unit := +revert_and_transform (λ e, dunfold cs e cfg) h structure delta_config := (max_steps := simp.default_max_steps) @@ -176,6 +180,7 @@ revert_and_transform (λ e, delta cs e cfg) h structure unfold_proj_config extends dsimp_config := (md := transparency.instances) +/-- If `e` is a projection application, try to unfold it, otherwise fail. -/ meta constant unfold_proj (e : expr) (md := transparency.instances) : tactic expr meta def unfold_projs (e : expr) (cfg : unfold_proj_config := {}) : tactic expr := diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean index 7f8e0391fa..1423e006de 100644 --- a/library/init/meta/well_founded_tactics.lean +++ b/library/init/meta/well_founded_tactics.lean @@ -36,7 +36,7 @@ meta def clear_internals : tactic unit := local_context >>= clear_wf_rec_goal_aux meta def unfold_wf_rel : tactic unit := -dunfold [``has_well_founded.r] {fail_if_unchanged := ff} +dunfold_target [``has_well_founded.r] {fail_if_unchanged := ff} meta def is_psigma_mk : expr → tactic (expr × expr) | `(psigma.mk %%a %%b) := return (a, b) @@ -57,7 +57,7 @@ meta def process_lex : tactic unit → tactic unit tac private meta def unfold_sizeof_measure : tactic unit := -dunfold [``sizeof_measure, ``measure, ``inv_image] {fail_if_unchanged := ff} +dunfold_target [``sizeof_measure, ``measure, ``inv_image] {fail_if_unchanged := ff} private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas | s [] := return s @@ -77,7 +77,7 @@ e.mfold simp_lemmas.mk $ λ c d s, private meta def unfold_sizeof_loop : tactic unit := do - dunfold [``sizeof, ``has_sizeof.sizeof] {fail_if_unchanged := ff}, + dunfold_target [``sizeof, ``has_sizeof.sizeof] {fail_if_unchanged := ff}, S ← target >>= collect_sizeof_lemmas, (simp_target S >> unfold_sizeof_loop) <|> diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index 17c41f8b5b..9582ad00e5 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -110,7 +110,7 @@ public: } }; -vm_obj tactic_dunfold_core(vm_obj const & cs, vm_obj const & _e, vm_obj const & _cfg, vm_obj const & _s) { +vm_obj tactic_dunfold(vm_obj const & cs, vm_obj const & _e, vm_obj const & _cfg, vm_obj const & _s) { expr const & e = to_expr(_e); tactic_state const & s = tactic::to_state(_s); defeq_can_state dcs = s.dcs(); @@ -134,7 +134,7 @@ vm_obj tactic_dunfold_core(vm_obj const & cs, vm_obj const & _e, vm_obj const & } } -vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & m, vm_obj const & _s) { +vm_obj tactic_dunfold_head(vm_obj const & _e, vm_obj const & m, vm_obj const & _s) { expr const & e = to_expr(_e); tactic_state const & s = tactic::to_state(_s); try { @@ -166,8 +166,8 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & m, vm_obj const & _ void initialize_unfold_tactic() { DECLARE_VM_BUILTIN(name({"tactic", "unfold_proj"}), tactic_unfold_projection); - DECLARE_VM_BUILTIN(name({"tactic", "dunfold_core"}), tactic_dunfold_core); - DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}), tactic_dunfold_expr); + DECLARE_VM_BUILTIN(name({"tactic", "dunfold"}), tactic_dunfold); + DECLARE_VM_BUILTIN(name({"tactic", "dunfold_head"}), tactic_dunfold_head); } void finalize_unfold_tactic() { diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean index a195f2c287..7784ddccdd 100644 --- a/tests/lean/unfold1.lean +++ b/tests/lean/unfold1.lean @@ -9,10 +9,10 @@ example (l : list nat) : list.append l [] = l := by do get_local `l >>= λ H, induction H [`h, `t, `iH], -- - dunfold [`list.append], + dunfold_target [`list.append], trace_state, trace "------", reflexivity, - dunfold [`list.append], + dunfold_target [`list.append], trace_state, rewriteH `iH diff --git a/tests/lean/unfold_crash.lean b/tests/lean/unfold_crash.lean index 18a14db2f5..1155aee4f1 100644 --- a/tests/lean/unfold_crash.lean +++ b/tests/lean/unfold_crash.lean @@ -4,8 +4,8 @@ open nat tactic example (a b : nat) : a = succ b → a = b + 1 := by do H ← intro `H, - try (dunfold_at [`nat.succ] H), - dunfold [`add, `has_add.add, `has_one.one, `nat.add, `one], + try (dunfold_hyp [`nat.succ] H), + dunfold_target [`add, `has_add.add, `has_one.one, `nat.add, `one], trace_state, t ← target, expected ← to_expr ```(a = succ b),