From d655310ecfe77e1a9326adcf028da4d366b5159a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Oct 2016 16:37:08 -0700
Subject: [PATCH] feat(library/init/meta): rename rsimp* back to dsimp*

---
 library/init/meta/converter.lean        |  4 +--
 library/init/meta/interactive.lean      | 10 +++----
 library/init/meta/simp_tactic.lean      | 37 +++++++++++++++++++------
 src/library/tactic/defeq_simplifier.cpp |  4 +--
 tests/lean/change1.lean                 |  2 +-
 tests/lean/change2.lean                 |  2 +-
 tests/lean/defeq1.lean                  |  2 +-
 tests/lean/defeq_simp1.lean             |  4 +--
 tests/lean/defeq_simp2.lean             |  8 +++---
 tests/lean/defeq_simp3.lean             |  2 +-
 tests/lean/defeq_simp4.lean             |  4 +--
 tests/lean/defeq_simp5.lean             |  2 +-
 tests/lean/run/cases_tac1.lean          |  2 +-
 tests/lean/run/converter.lean           |  6 ++--
 tests/lean/run/dsimp_at1.lean           |  2 +-
 tests/lean/unfold_crash.lean            |  2 +-
 16 files changed, 57 insertions(+), 36 deletions(-)

diff --git a/library/init/meta/converter.lean b/library/init/meta/converter.lean
index eb859e10d4..611b3c5d0d 100644
--- a/library/init/meta/converter.lean
+++ b/library/init/meta/converter.lean
@@ -85,8 +85,8 @@ meta def whnf_core (m : transparency) : conv unit :=
 meta def whnf : conv unit :=
 conv.whnf_core reducible
 
-meta def rsimp : conv unit :=
-λ r e, do s ← simp_lemmas.mk_default, n ← s^.rsimplify e, return ⟨(), n, none⟩
+meta def dsimp : conv unit :=
+λ r e, do s ← simp_lemmas.mk_default, n ← s^.dsimplify e, return ⟨(), n, none⟩
 
 meta def try (c : conv unit) : conv unit :=
 c <|> return ()
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index d9b52bedb0..deb8ff9560 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -295,13 +295,13 @@ do s ← mk_simp_set attr_names hs ids,
    end,
    try tactic.triv, try tactic.reflexivity
 
-private meta def rsimp_hyps : location → tactic unit
+private meta def dsimp_hyps : location → tactic unit
 | []      := skip
-| (h::hs) := get_local h >>= rsimp_at
+| (h::hs) := get_local h >>= dsimp_at
 
-meta def rsimp : location → tactic unit
-| [] := tactic.rsimp
-| hs := rsimp_hyps hs
+meta def dsimp : location → tactic unit
+| [] := tactic.dsimp
+| hs := dsimp_hyps hs
 
 meta def reflexivity : tactic unit :=
 tactic.reflexivity
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 250bd6b9f7..18c5c2d9ea 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -59,14 +59,35 @@ simp_lemmas.rewrite_core reducible
    Fails if no simplifications can be performed. -/
 meta constant simp_lemmas.simplify_core : simp_lemmas → tactic unit → name → expr → tactic (expr × expr)
 
-/- Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
+/- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
    The resulting expression is definitionally equal to the input. -/
-meta constant simp_lemmas.rsimplify_core : transparency → simp_lemmas → expr → tactic expr
+meta constant simp_lemmas.dsimplify_core : transparency → simp_lemmas → expr → tactic expr
 
-meta def simp_lemmas.rsimplify : simp_lemmas → expr → tactic expr :=
-simp_lemmas.rsimplify_core reducible
+meta def simp_lemmas.dsimplify : simp_lemmas → expr → tactic expr :=
+simp_lemmas.dsimplify_core reducible
 
 namespace tactic
+meta constant dsimplify_core
+  (max_steps       : nat)
+  /- If visit_instances = ff, then instance implicit arguments are not visited, but
+     tactic will canonize them. -/
+  (visit_instances : bool)
+  /- (pre e) is invoked before visiting the children of subterm 'e',
+     if it succeeds the result is a new expression that must be definitionally equal to 'e',
+     and a flag indicating whether the new children should be visited or not. -/
+  (pre             : expr → tactic (expr × bool))
+  /- (post e) is invoked after visiting the children of subterm 'e',
+     if it succeeds the result is a new expression that must be definitionally equal to 'e',
+     and a flag indicating whether the new children should be revisited.
+     Remark: if (pre e) returns (some (new_e, ff)), then post is not invoked for new_e. -/
+  (post            : expr → tactic (expr × bool))
+  : expr → tactic expr
+
+meta def dsimplify
+  (pre             : expr → tactic (expr × bool))
+  (post            : expr → tactic (expr × bool))
+  : expr → tactic expr :=
+dsimplify_core 1000000 ff pre post
 
 meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
 do lemmas       ← simp_lemmas.mk_default,
@@ -86,15 +107,15 @@ simplify_goal failed [] >> try triv >> try reflexivity
 meta def simp_using (Hs : list expr) : tactic unit :=
 simplify_goal failed Hs >> try triv
 
-meta def rsimp : tactic unit :=
+meta def dsimp : tactic unit :=
 do S ← simp_lemmas.mk_default,
-   target >>= S^.rsimplify >>= change
+   target >>= S^.dsimplify >>= change
 
-meta def rsimp_at (H : expr) : tactic unit :=
+meta def dsimp_at (H : expr) : tactic unit :=
 do num_reverted : ℕ ← revert H,
    (expr.pi n bi d b : expr) ← target | failed,
    S      ← simp_lemmas.mk_default,
-   H_simp ← S^.rsimplify d,
+   H_simp ← S^.dsimplify d,
    change $ expr.pi n bi H_simp b,
    intron num_reverted
 
diff --git a/src/library/tactic/defeq_simplifier.cpp b/src/library/tactic/defeq_simplifier.cpp
index e87e48a404..34a504fb0d 100644
--- a/src/library/tactic/defeq_simplifier.cpp
+++ b/src/library/tactic/defeq_simplifier.cpp
@@ -303,7 +303,7 @@ expr defeq_simplify(type_context & ctx, simp_lemmas const & simp_lemmas, expr co
     return defeq_simplify_fn(ctx, simp_lemmas)(e);
 }
 
-vm_obj simp_lemmas_rsimplify_core(vm_obj const & m, vm_obj const & _lemmas, vm_obj const & e, vm_obj const & s0) {
+vm_obj simp_lemmas_dsimplify_core(vm_obj const & m, vm_obj const & _lemmas, vm_obj const & e, vm_obj const & s0) {
     type_context ctx = mk_type_context_for(s0, m);
     tactic_state const & s    = to_tactic_state(s0);
     LEAN_TACTIC_TRY;
@@ -320,7 +320,7 @@ expr defeq_simplify(type_context & ctx, expr const & e) {
 
 /* Setup and teardown */
 void initialize_defeq_simplifier() {
-    DECLARE_VM_BUILTIN(name({"simp_lemmas", "rsimplify_core"}), simp_lemmas_rsimplify_core);
+    DECLARE_VM_BUILTIN(name({"simp_lemmas", "dsimplify_core"}), simp_lemmas_dsimplify_core);
 
     register_trace_class("defeq_simplifier");
     register_trace_class(name({"defeq_simplifier", "canonize"}));
diff --git a/tests/lean/change1.lean b/tests/lean/change1.lean
index e6e84fb714..090e2fc4e1 100644
--- a/tests/lean/change1.lean
+++ b/tests/lean/change1.lean
@@ -9,7 +9,7 @@ by do intro `Heq,
       t  ← target,
       trace_state,
       s ← simp_lemmas.mk_default,
-      t' ← s^.rsimplify t,
+      t' ← s^.dsimplify t,
       change t',
       trace "---- after change ----",
       trace_state,
diff --git a/tests/lean/change2.lean b/tests/lean/change2.lean
index 5a98722524..6263df656b 100644
--- a/tests/lean/change2.lean
+++ b/tests/lean/change2.lean
@@ -8,7 +8,7 @@ example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
 by do intro `Heq,
       get_local `a >>= subst,
       trace_state,
-      rsimp,
+      dsimp,
       trace "---- after dsimp ----",
       trace_state,
       t ← target,
diff --git a/tests/lean/defeq1.lean b/tests/lean/defeq1.lean
index 0f147990ad..63c3dacfa3 100644
--- a/tests/lean/defeq1.lean
+++ b/tests/lean/defeq1.lean
@@ -9,6 +9,6 @@ example (n m : nat) (H : succ (succ n) = succ m) : true :=
 by do H  ← get_local `H,
       t  ← infer_type H,
       s  ← simp_lemmas.mk_default,
-      t' ← s^.rsimplify t,
+      t' ← s^.dsimplify t,
       trace t',
       exact (expr.const `trivial [])
diff --git a/tests/lean/defeq_simp1.lean b/tests/lean/defeq_simp1.lean
index 43a015a6f0..6413421877 100644
--- a/tests/lean/defeq_simp1.lean
+++ b/tests/lean/defeq_simp1.lean
@@ -9,14 +9,14 @@ open tactic
 example (a b : nat) (H : @add nat (id (id nat.has_add)) a b = @add nat nat_has_add2 a b) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 
 example (a b : nat) (H : (λ x : nat, @add nat (id (id nat.has_add)) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 attribute [reducible]
diff --git a/tests/lean/defeq_simp2.lean b/tests/lean/defeq_simp2.lean
index 7c05d584fe..9de0a75598 100644
--- a/tests/lean/defeq_simp2.lean
+++ b/tests/lean/defeq_simp2.lean
@@ -10,7 +10,7 @@ axiom foo3 (n : nat) : n ≥ 0
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 set_option defeq_simplify.canonize_proofs true
@@ -20,7 +20,7 @@ constant x1 : nat -- update the environment to force defeq_canonize cache to be
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 constant x2 : nat -- update the environment to force defeq_canonize cache to be reset
@@ -28,12 +28,12 @@ constant x2 : nat -- update the environment to force defeq_canonize cache to be
 example (a b : nat) (H : f a (id (id (id (foo1 a)))) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 -- Example that does not work
 example (a b : nat) (H : (λ x, f x (id (id (id (foo1 x))))) = (λ x, f x (foo2 x))) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
diff --git a/tests/lean/defeq_simp3.lean b/tests/lean/defeq_simp3.lean
index 79a5fbc417..188622f426 100644
--- a/tests/lean/defeq_simp3.lean
+++ b/tests/lean/defeq_simp3.lean
@@ -12,5 +12,5 @@ set_option pp.all true
 example (a b : nat) (H : (λ x : nat, @add nat nat_has_add2 a x) = (λ x : nat, @add nat (nat_has_add3 x) a b)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
diff --git a/tests/lean/defeq_simp4.lean b/tests/lean/defeq_simp4.lean
index d7caff17d9..948ac4bb46 100644
--- a/tests/lean/defeq_simp4.lean
+++ b/tests/lean/defeq_simp4.lean
@@ -16,8 +16,8 @@ set_option pp.all true
 example (a b : nat) (H : (λ x : nat, @add nat (nat_has_add3 x) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   trace "---------",
   -- The following should work
-  get_local `H >>= infer_type >>= s^.rsimplify >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= s^.dsimplify >>= trace,
   constructor
diff --git a/tests/lean/defeq_simp5.lean b/tests/lean/defeq_simp5.lean
index 50cc38c268..5018144a5b 100644
--- a/tests/lean/defeq_simp5.lean
+++ b/tests/lean/defeq_simp5.lean
@@ -17,5 +17,5 @@ example (a b : nat)
              (λ x y : nat, @add nat (nat_has_add3 y) a x)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
diff --git a/tests/lean/run/cases_tac1.lean b/tests/lean/run/cases_tac1.lean
index 6878bcebb1..7927ee8d7a 100644
--- a/tests/lean/run/cases_tac1.lean
+++ b/tests/lean/run/cases_tac1.lean
@@ -25,7 +25,7 @@ by do
   w ← get_local `w,
   cases_using w [`n', `hw, `tw],
   trace_state,
-  rsimp,
+  dsimp,
   Heq1 ← intro1,
   Heq2 ← intro1,
   subst Heq1, subst Heq2,
diff --git a/tests/lean/run/converter.lean b/tests/lean/run/converter.lean
index b1d47d3628..e14dbfd8d6 100644
--- a/tests/lean/run/converter.lean
+++ b/tests/lean/run/converter.lean
@@ -17,7 +17,7 @@ by conversion $
   whnf >>
   trace_lhs >>
   apply_simp_set `bla >>
-  rsimp >>
+  dsimp >>
   trace "after defeq simplifier" >>
   trace_lhs >>
   change `(f a a) >>
@@ -34,7 +34,7 @@ by conversion $
   funext $ do
     trace_lhs,
     apply_simp_set `bla,
-    rsimp,
+    dsimp,
     apply_simp_set `foo
 
 constant h : nat → nat → nat
@@ -46,7 +46,7 @@ meta def conv.depth : conv unit → conv unit
 lemma ex (a : nat) : (λ a, h (f a (sizeof a)) (g a)) = (λ a, h 0 a) :=
 by conversion $
    depth_first $
-     (apply_simp_set `foo <|> apply_simp_set `bla <|> rsimp)
+     (apply_simp_set `foo <|> apply_simp_set `bla <|> dsimp)
 
 lemma ex2 {A : Type} [comm_group A] (a b : A) : b * 1 * a = a * b :=
 by conversion $
diff --git a/tests/lean/run/dsimp_at1.lean b/tests/lean/run/dsimp_at1.lean
index 58ddd726b3..1e077afe19 100644
--- a/tests/lean/run/dsimp_at1.lean
+++ b/tests/lean/run/dsimp_at1.lean
@@ -8,6 +8,6 @@ noncomputable definition f (z : A) : A := z
 definition foo (z₁ z₂ : A) : f z₁ = f z₂ → z₁ = z₂ :=
 by do H ← intro `H,
       trace_state,
-      rsimp_at H,
+      dsimp_at H,
       trace_state,
       assumption
diff --git a/tests/lean/unfold_crash.lean b/tests/lean/unfold_crash.lean
index ba378adf39..c46021fcb3 100644
--- a/tests/lean/unfold_crash.lean
+++ b/tests/lean/unfold_crash.lean
@@ -5,6 +5,6 @@ example (a b : nat) : a = succ b → a = b + 1 :=
 by do
   H ← intro `H,
   try (unfold_at [`nat.succ] H),
-  unfold [`add], rsimp, unfold [`nat.add],
+  unfold [`add], dsimp, unfold [`nat.add],
   trace_state,
   assumption