feat(library/init/meta/simp_tactic): add command for creating simp attributes

library/init/meta/simp_tactic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic
+import init.meta.tactic init.meta.attribute init.meta.constructor_tactic
 
 namespace tactic
 open list nat
@@ -28,10 +28,10 @@ meta constant simp_lemmas_erase       : simp_lemmas → list name → simp_lemma
 meta def simp_lemmas_insert_constant : simp_lemmas → name → tactic simp_lemmas :=
 simp_lemmas_insert_constant_core reducible
 
-meta definition mk_simp_lemmas        : tactic simp_lemmas :=
+meta def mk_simp_lemmas        : tactic simp_lemmas :=
 mk_simp_lemmas_core reducible [`simp] [`congr]
 
-meta definition simp_lemmas_add_extra : transparency → simp_lemmas → list expr → tactic simp_lemmas
+meta def simp_lemmas_add_extra : transparency → simp_lemmas → list expr → tactic simp_lemmas
 | m sls []      := return sls
 | m sls (l::ls) := do
   new_sls ← simp_lemmas_insert_core m sls l,
@@ -47,29 +47,29 @@ meta definition simp_lemmas_add_extra : transparency → simp_lemmas → list ex
    Fails if no simplifications can be performed. -/
 meta constant simplify_core : tactic unit → name → simp_lemmas → expr → tactic (expr × expr)
 
-meta definition simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
+meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
 do simp_lemmas  ← mk_simp_lemmas,
    new_lemmas   ← simp_lemmas_add_extra reducible simp_lemmas extra_lemmas,
    e_type       ← infer_type e >>= whnf,
    simplify_core prove_fn `eq new_lemmas e
 
-meta definition simplify_goal (prove_fn : tactic unit) (extra_lemmas : list expr) : tactic unit :=
+meta def simplify_goal (prove_fn : tactic unit) (extra_lemmas : list expr) : tactic unit :=
 do (new_target, Heq) ← target >>= simplify prove_fn extra_lemmas,
    assert `Htarget new_target, swap,
    Ht ← get_local `Htarget,
    mk_app `eq.mpr [Heq, Ht] >>= exact
 
-meta definition simp : tactic unit :=
+meta def simp : tactic unit :=
 simplify_goal failed [] >> try triv
 
-meta definition simp_using (Hs : list expr) : tactic unit :=
+meta def simp_using (Hs : list expr) : tactic unit :=
 simplify_goal failed Hs >> try triv
 
-private meta definition is_equation : expr → bool
+private meta def is_equation : expr → bool
 | (expr.pi n bi d b) := is_equation b
 | e                  := match (expr.is_eq e) with (some a) := tt | none := ff end
 
-private meta definition collect_eqs : list expr → tactic (list expr)
+private meta def collect_eqs : list expr → tactic (list expr)
 | []        := return []
 | (H :: Hs) := do
   Eqs   ← collect_eqs Hs,
@@ -77,10 +77,10 @@ private meta definition collect_eqs : list expr → tactic (list expr)
   return $ if is_equation Htype then H :: Eqs else Eqs
 
 /- Simplify target using all hypotheses in the local context. -/
-meta definition simp_using_hs : tactic unit :=
+meta def simp_using_hs : tactic unit :=
 local_context >>= collect_eqs >>= simp_using
 
-meta definition simp_core_at (prove_fn : tactic unit) (extra_lemmas : list expr) (H : expr) : tactic unit :=
+meta def simp_core_at (prove_fn : tactic unit) (extra_lemmas : list expr) (H : expr) : tactic unit :=
 do when (expr.is_local_constant H = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
    Htype ← infer_type H,
    (new_Htype, Heq) ← simplify prove_fn extra_lemmas Htype,
@@ -88,20 +88,40 @@ do when (expr.is_local_constant H = ff) (fail "tactic simp_at failed, the given
    mk_app `eq.mp [Heq, H] >>= exact,
    try $ clear H
 
-meta definition simp_at : expr → tactic unit :=
+meta def simp_at : expr → tactic unit :=
 simp_core_at failed []
 
-meta definition simp_at_using (Hs : list expr) : expr → tactic unit :=
+meta def simp_at_using (Hs : list expr) : expr → tactic unit :=
 simp_core_at failed Hs
 
-meta definition simp_at_using_hs (H : expr) : tactic unit :=
+meta def simp_at_using_hs (H : expr) : tactic unit :=
 do Hs ← local_context >>= collect_eqs,
    simp_core_at failed (filter (ne H) Hs) H
 
-meta definition mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit :=
+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,
    unify rhs new_rhs,
    exact Heq
 
+/- Simp attribute support -/
+
+meta def to_simp_lemmas : simp_lemmas → list name → tactic simp_lemmas
+| S []      := return S
+| S (n::ns) := do S' ← simp_lemmas_insert_constant S n, to_simp_lemmas S' ns
+
 end tactic
+
+open tactic
+
+meta def mk_simp_attr (attr_name : name) : command :=
+do t ← to_expr `(caching_user_attribute),
+   a ← attr_name^.to_expr,
+   v ← to_expr `({ caching_user_attribute .
+                   name     := %%a,
+                   descr    := "simplifier attribute",
+                   cache    := simp_lemmas,
+                   mk_cache := λ ns, do {S₀ ← tactic.mk_empty_simp_lemmas, tactic.to_simp_lemmas S₀ ns},
+                   dependencies := [`reducible] }),
+   add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
+   attribute.register attr_name

library/init/meta/tactic.lean

@@ -645,15 +645,32 @@ meta definition generalizes : list expr → tactic unit
 meta definition refine (e : pexpr) : tactic unit :=
 do tgt : expr ← target,
    to_expr `((%%e : %%tgt)) >>= exact
+end tactic
 
-meta definition expr_of_nat : nat → tactic expr
+open tactic
+
+meta definition nat.to_expr : nat → tactic expr
 | n :=
   if n = 0 then to_expr `(0)
   else if n = 1 then to_expr `(1)
   else do
-    r : expr ← expr_of_nat (n / 2),
+    r : expr ← nat.to_expr (n / 2),
     if n % 2 = 0 then to_expr `(bit0 %%r)
     else to_expr `(bit1 %%r)
 
+meta definition char.to_expr : char → tactic expr
+| ⟨n, pr⟩ := do e ← n^.to_expr, to_expr `(char.of_nat %%e)
+
+meta definition string.to_expr : string → tactic expr
+| []      := to_expr `(string.empty)
+| (c::cs) := do e ← c^.to_expr, es ← string.to_expr cs, to_expr `(string.str %%e %%es)
+
+meta definition unsigned.to_expr : unsigned → tactic expr
+| ⟨n, pr⟩ := do e ← n^.to_expr, to_expr `(unsigned.of_nat %%e)
+
+meta definition name.to_expr : name → tactic expr
+| name.anonymous        := to_expr `(name.anonymous)
+| (name.mk_string s n)  := do es ← s^.to_expr, en ← name.to_expr n, to_expr `(name.mk_string %%es %%en)
+| (name.mk_numeral i n) := do is ← i^.to_expr, en ← name.to_expr n, to_expr `(name.mk_string %%is %%en)
+
 notation `command`:max := tactic unit
-end tactic

src/library/tactic/tactic_state.cpp

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_option.h"
+#include "library/compiler/vm_compiler.h"
 #include "library/tactic/tactic_state.h"
 
 #ifndef LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS
@@ -563,10 +564,12 @@ vm_obj tactic_instantiate_mvars(vm_obj const & e, vm_obj const & _s) {
     return mk_tactic_success(to_obj(r), set_mctx(s, mctx));
 }
 
-vm_obj tactic_add_decl(vm_obj const & d, vm_obj const & _s) {
+vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) {
     tactic_state const & s  = to_tactic_state(_s);
     try {
-        environment new_env = module::add(s.env(), check(s.env(), to_declaration(d)));
+        declaration d       = to_declaration(_d);
+        environment new_env = module::add(s.env(), check(s.env(), d));
+        new_env = vm_compile(new_env, d);
         return mk_tactic_success(set_env(s, new_env));
     } catch (throwable & ex) {
         return mk_tactic_exception(ex, s);