refactor(library/init/meta/simp_tactic): make sure dunfold tactics use name convention used at simp, dsimp, ...

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
 

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
 

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 :=

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)
   <|>

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() {

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

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),