From 6edec4c4e97d8aaccaf8f27f6db3bf03e44666a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 19 Oct 2016 17:23:32 -0700
Subject: [PATCH] feat(library/init/meta/converter): implement conversionals
 using ext_simplify_core

---
 library/init/meta/converter.lean   | 76 +++++++++++++++++++-----------
 library/init/meta/simp_tactic.lean |  4 +-
 tests/lean/run/converter.lean      | 14 ++----
 3 files changed, 55 insertions(+), 39 deletions(-)

diff --git a/library/init/meta/converter.lean b/library/init/meta/converter.lean
index 611b3c5d0d..4f01653955 100644
--- a/library/init/meta/converter.lean
+++ b/library/init/meta/converter.lean
@@ -172,13 +172,7 @@ meta def match_expr (p : pexpr) : conv unit :=
   new_p ← pexpr_to_pattern p,
   tactic.match_pattern new_p e >> return ⟨(), e, none⟩
 
-meta def attr : user_attribute :=
-{ name  := `convsub,
-  descr := "for marking conversionals (conv unit -> conv unit) used by `conv.sub`" }
-
-run_command attribute.register `conv.attr
-
-@[convsub] meta def funext (c : conv unit) : conv unit :=
+meta def funext (c : conv unit) : conv unit :=
 λ r lhs, do
   guard (r = `eq),
   (expr.lam n bi d b) ← return lhs | failed,
@@ -219,31 +213,59 @@ meta def congr_core (c_f c_a : conv unit) : conv unit :=
       return ⟨(), rhs, some pr⟩
   end
 
-@[convsub] meta def congr (c : conv unit) : conv unit :=
+meta def congr (c : conv unit) : conv unit :=
 congr_core c c
 
-meta def subc_core : list name → conv unit → conv unit
-| []      c r e := return ⟨(), e, none⟩
-| (n::ns) c r e := do
-  F ← eval_expr (conv unit → conv unit) (expr.const n []),
-  (F c r e <|> subc_core ns c r e)
-
-/- Try all conversionals F tagged with attribute @[convsub] -/
-meta def subc (c : conv unit) : conv unit :=
+meta def bottom_up (c : conv unit) : conv unit :=
 λ r e, do
-  is ← attribute.get_instances `convsub,
-  subc_core is c r e
+  s ← simp_lemmas.mk_default,
+  (a, new_e, pr) ←
+     ext_simplify_core () default_simplify_config s
+       (λ u, return u)
+       (λ a s r p e, failed)
+       (λ a s r p e, do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, tt))
+       r e,
+  return ⟨(), new_e, some pr⟩
 
-meta def depth_first : conv unit → conv unit
-| c := (subc (depth_first c) >> repeat c)
+meta def top_down (c : conv unit) : conv unit :=
+λ r e, do
+  s ← simp_lemmas.mk_default,
+  (a, new_e, pr) ←
+     ext_simplify_core () default_simplify_config s
+       (λ u, return u)
+       (λ a s r p e, do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, tt))
+       (λ a s r p e, failed)
+       r e,
+  return ⟨(), new_e, some pr⟩
 
-meta def find : conv unit → conv unit
-| c := c <|> subc (find c)
+meta def find (c : conv unit) : conv unit :=
+λ r e, do
+  s ← simp_lemmas.mk_default,
+  (a, new_e, pr) ←
+     ext_simplify_core () default_simplify_config s
+       (λ u, return u)
+       (λ a s r p e,
+         (do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, ff))
+         <|>
+         return ((), e, none, tt))
+       (λ a s r p e, failed)
+       r e,
+  return ⟨(), new_e, some pr⟩
 
-meta def find_pattern : pattern → conv unit → conv unit
-| p c := do
-  matched ← tryb $ match_pattern p,
-  if matched then c else (subc (find_pattern p c))
+meta def find_pattern (pat : pattern) (c : conv unit) : conv unit :=
+λ r e, do
+  s ← simp_lemmas.mk_default,
+  (a, new_e, pr) ←
+     ext_simplify_core () default_simplify_config s
+       (λ u, return u)
+       (λ a s r p e, do
+         matched ← (tactic.match_pattern pat e >> return tt) <|> return ff,
+         if matched
+         then do ⟨u, new_e, pr⟩ ← c r e, return ((), new_e, pr, ff)
+         else return ((), e, none, tt))
+       (λ a s r p e, failed)
+       r e,
+  return ⟨(), new_e, some pr⟩
 
 meta def findp : pexpr → conv unit → conv unit :=
 λ p c r e, do
@@ -261,6 +283,4 @@ do (r, lhs, rhs) ← (target_lhs_rhs <|> fail "conversion failed, target is not
                      new_lhs_fmt^.indent 4)),
    exact pr
 
-/- TODO(Leo): add more primitives and combinators. Example: congruence, etc -/
-
 end conv
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index f29b1eb99d..c3ec820269 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -185,11 +185,11 @@ meta constant ext_simplify_core
        - 'new_e' is a new expression s.t. 'e r new_e'
        - 'new_pr' is a proof for 'e r new_e', If it is none, the proof is assumed to be by reflexivity
        - 'flag'  if tt 'new_e' children should be visited, and 'post' invoked. -/
-  (pre : A → name → simp_lemmas → option expr → expr → tactic (A × expr × option expr × bool))
+  (pre : A → simp_lemmas → name → option expr → expr → tactic (A × expr × option expr × bool))
   /- (post a r s p e) is invoked after visiting the children of subterm 'e',
      The output is similar to (pre a r s p e), but the 'flag' indicates whether
      the new expression should be revisited or not. -/
-  (post : A → name → simp_lemmas → option expr → expr → tactic (A × expr × option expr × bool))
+  (post : A → simp_lemmas  → name → option expr → expr → tactic (A × expr × option expr × bool))
   /- simplification relation -/
   (r : name) :
   expr → tactic (A × expr × expr)
diff --git a/tests/lean/run/converter.lean b/tests/lean/run/converter.lean
index e14dbfd8d6..2b179b42ca 100644
--- a/tests/lean/run/converter.lean
+++ b/tests/lean/run/converter.lean
@@ -39,22 +39,18 @@ by conversion $
 
 constant h : nat → nat → nat
 
-meta def conv.depth : conv unit → conv unit
-| c r e :=
-  (subc (conv.depth c) >> repeat c) r e
-
 lemma ex (a : nat) : (λ a, h (f a (sizeof a)) (g a)) = (λ a, h 0 a) :=
 by conversion $
-   depth_first $
+   bottom_up $
      (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 $
-   depth_first (apply_simp_set `default)
+   bottom_up (apply_simp_set `default)
 
 lemma ex3 (p q r : Prop) : (p ∧ true ∧ p) = p :=
 by conversion $
-   depth_first (apply_propext_simp_set `default)
+   bottom_up (apply_propext_simp_set `default)
 
 print "---------"
 
@@ -62,11 +58,11 @@ lemma ex4 (a b c : nat) : g (g (g (f (f (g (g a)) (g (g a))) a))) = g (g (g (f (
 by conversion $
    findp `(λ x, f (g x) (g x)) $
      trace "found pattern" >> trace_lhs >>
-     depth_first (apply_simp_set `bla)
+     bottom_up (apply_simp_set `bla)
 
 lemma ex5 (a b c : nat) : g (g (g (f (f (g (g a)) (g (g a))) a))) = g (g (g (f (f a a) a))) :=
 by conversion $
    find $
      match_expr `(λ x, f (g x) (g x)) >>
      trace "found pattern" >> trace_lhs >>
-     depth_first (apply_simp_set `bla)
+     bottom_up (apply_simp_set `bla)