From 3188c4cbcfea7c6a9d76da8752b6f1d04c8fe75e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 1 Sep 2017 14:00:17 +0200
Subject: [PATCH] refactor(library/tactic/user_attribute,init/meta/attribute):
 merge `caching_user_attribute` into `user_attribute`

The inheritance-based approach doesn't scale to a second subclass for parameterized attributes
---
 library/init/meta/attribute.lean              | 39 +++++++++-------
 library/init/meta/coinductive_predicates.lean |  2 +-
 library/init/meta/simp_tactic.lean            | 12 +++--
 library/init/meta/smt/ematch.lean             | 29 ++++++------
 library/init/meta/smt/rsimp.lean              |  7 +--
 src/library/constants.cpp                     |  4 --
 src/library/constants.h                       |  1 -
 src/library/constants.txt                     |  1 -
 src/library/tactic/smt/smt_state.cpp          |  9 ++--
 src/library/tactic/user_attribute.cpp         | 44 +++++++++----------
 src/library/tactic/user_attribute.h           |  3 +-
 tests/lean/caching_user_attribute.lean        | 22 ++++++----
 tests/lean/run/check_constants.lean           |  1 -
 tests/lean/run/eval_attr_cache.lean           | 15 ++++---
 tests/lean/slow_error.lean                    |  2 +-
 tests/lean/slow_error.lean.expected.out       |  2 +-
 16 files changed, 99 insertions(+), 94 deletions(-)

diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean
index 031381a095..6ae6c8ed74 100644
--- a/library/init/meta/attribute.lean
+++ b/library/init/meta/attribute.lean
@@ -9,9 +9,16 @@ import init.meta.tactic init.meta.rb_map init.meta.has_reflect
 meta constant attribute.get_instances : name → tactic (list name)
 meta constant attribute.fingerprint : name → tactic nat
 
-meta structure user_attribute :=
-(name         : name)
-(descr        : string)
+meta structure user_attribute_cache_cfg (cache_ty : Type) :=
+(mk_cache     : list name → tactic cache_ty)
+(dependencies : list name)
+
+meta def user_attribute.dflt_cache_cfg : tactic unit :=
+tactic.exact `(⟨λ _, pure (), []⟩ : user_attribute_cache_cfg unit)
+
+meta structure user_attribute (cache_ty : Type := unit) :=
+(name          : name)
+(descr         : string)
 /- Optional handler that will be called after the attribute has been applied to a declaration.
    Failing the tactic will fail the entire `attribute/def/...` command, i.e. the attribute will
    not be applied after all.
@@ -20,33 +27,35 @@ meta structure user_attribute :=
 (after_set    : option (Π (decl : _root_.name) (prio : nat) (persistent : bool), command) := none)
 /- Optional handler that will be called before the attribute is removed from a declaration. -/
 (before_unset : option (Π (decl : _root_.name) (persistent : bool), command) := none)
+(cache_cfg     : user_attribute_cache_cfg cache_ty . user_attribute.dflt_cache_cfg)
 
 /- Registers a new user-defined attribute. The argument must be the name of a definition of type
    `user_attribute` or a sub-structure. -/
 meta def attribute.register (decl : name) : command :=
 tactic.set_basic_attribute ``user_attribute decl tt
 
-meta structure caching_user_attribute (α : Type) extends user_attribute :=
-(mk_cache     : list _root_.name → tactic α)
-(dependencies : list _root_.name)
+meta constant user_attribute.get_cache {α β : Type} (attr : user_attribute α β) : tactic α
 
-meta constant caching_user_attribute.get_cache : Π {α : Type}, caching_user_attribute α → tactic α
 
 open tactic
 
 meta def register_attribute := attribute.register
 
+meta def get_attribute_cache_dyn {α : Type} [reflected α] (name : name) : tactic α :=
+let attr : pexpr := expr.const name [] in
+do e ← to_expr ``(user_attribute.get_cache %%attr),
+   t ← eval_expr (tactic α) e,
+   t
+
 meta def mk_name_set_attr (attr_name : name) : command :=
-do let t := `(caching_user_attribute name_set),
+do let t := `(user_attribute name_set),
    let v := `({name     := attr_name,
-                 descr    := "name_set attribute",
+               descr    := "name_set attribute",
+               cache_cfg := {
                  mk_cache := λ ns, return (name_set.of_list ns),
-                 dependencies := [] } : caching_user_attribute name_set),
+                 dependencies := []}} : user_attribute name_set),
    add_meta_definition attr_name [] t v,
    register_attribute attr_name
 
-meta def get_name_set_for_attr (attr_name : name) : tactic name_set :=
-do
-  cnst   ← return (expr.const attr_name []),
-  attr   ← eval_expr (caching_user_attribute name_set) cnst,
-  caching_user_attribute.get_cache attr
+meta def get_name_set_for_attr (name : name) : tactic name_set :=
+get_attribute_cache_dyn name
diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean
index dade07968b..782de855f4 100644
--- a/library/init/meta/coinductive_predicates.lean
+++ b/library/init/meta/coinductive_predicates.lean
@@ -112,7 +112,7 @@ section
 universe u
 
 @[user_attribute]
-meta def monotonicity := { user_attribute . name := `monotonicity, descr := "Monotonicity rules for predicates" }
+meta def monotonicity : user_attribute := { name := `monotonicity, descr := "Monotonicity rules for predicates" }
 
 lemma monotonicity.pi {α : Sort u} {p q : α → Prop} (h : ∀a, implies (p a) (q a)) :
   implies (Πa, p a) (Πa, q a) :=
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index de49e14e52..3e37ae9037 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -335,20 +335,18 @@ meta def to_simp_lemmas : simp_lemmas → list name → tactic simp_lemmas
 | S (n::ns) := do S' ← S.add_simp n, to_simp_lemmas S' ns
 
 meta def mk_simp_attr (attr_name : name) : command :=
-do let t := `(caching_user_attribute simp_lemmas),
+do let t := `(user_attribute simp_lemmas),
    let v := `({name     := attr_name,
-                 descr    := "simplifier attribute",
+               descr    := "simplifier attribute",
+               cache_cfg := {
                  mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns},
-                 dependencies := [`reducibility] } : caching_user_attribute simp_lemmas),
+                 dependencies := [`reducibility]}} : user_attribute simp_lemmas),
    add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
    attribute.register attr_name
 
 meta def get_user_simp_lemmas (attr_name : name) : tactic simp_lemmas :=
 if attr_name = `default then simp_lemmas.mk_default
-else do
-  cnst   ← return (expr.const attr_name []),
-  attr   ← eval_expr (caching_user_attribute simp_lemmas) cnst,
-  caching_user_attribute.get_cache attr
+else get_attribute_cache_dyn attr_name
 
 meta def join_user_simp_lemmas_core : simp_lemmas → list name → tactic simp_lemmas
 | S []             := return S
diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean
index b47f810550..622f3ac510 100644
--- a/library/init/meta/smt/ematch.lean
+++ b/library/init/meta/smt/ematch.lean
@@ -79,7 +79,7 @@ meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_
   end
 
 meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command :=
-do let t := `(caching_user_attribute hinst_lemmas),
+do let t := `(user_attribute hinst_lemmas),
    let v := `({name     := attr_name,
                descr    := "hinst_lemma attribute",
                after_set := some $ λ n _ _,
@@ -87,8 +87,9 @@ do let t := `(caching_user_attribute hinst_lemmas),
                  fail format!"invalid ematch lemma '{n}'",
                -- allow unsetting
                before_unset := some $ λ _ _, skip,
-               mk_cache := λ ns, to_hinst_lemmas_core reducible as_simp ns hinst_lemmas.mk,
-               dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas),
+               cache_cfg := {
+                 mk_cache := λ ns, to_hinst_lemmas_core reducible as_simp ns hinst_lemmas.mk,
+                 dependencies := [`reducibility]}} : user_attribute hinst_lemmas),
    add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
    attribute.register attr_name
 
@@ -98,7 +99,7 @@ meta def mk_hinst_lemma_attrs_core (as_simp : bool) : list name → command
   (mk_hinst_lemma_attr_core n as_simp >> mk_hinst_lemma_attrs_core ns)
   <|>
   (do type ← infer_type (expr.const n []),
-      let expected := `(caching_user_attribute hinst_lemmas),
+      let expected := `(user_attribute),
       (is_def_eq type expected
        <|> fail format!"failed to create hinst_lemma attribute '{n}', declaration already exists and has different type."),
       mk_hinst_lemma_attrs_core ns)
@@ -111,7 +112,7 @@ meta def merge_hinst_lemma_attrs (m : transparency) (as_simp : bool) : list name
   merge_hinst_lemma_attrs attrs new_hs
 
 /--
-Create a new "cached" attribute (attr_name : caching_user_attribute hinst_lemmas).
+Create a new "cached" attribute (attr_name : user_attribute hinst_lemmas).
 It also creates "cached" attributes for each attr_names and simp_attr_names if they have not been defined
 yet. Moreover, the hinst_lemmas for attr_name will be the union of the lemmas tagged with
     attr_name, attrs_name, and simp_attr_names.
@@ -120,7 +121,7 @@ For the ones in simp_attr_names, we use the left-hand-side of the conclusion as
 meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names : list name) (simp_attr_names : list name) : command :=
 do mk_hinst_lemma_attrs_core ff attr_names,
    mk_hinst_lemma_attrs_core tt simp_attr_names,
-   let t  := `(caching_user_attribute hinst_lemmas),
+   let t  := `(user_attribute hinst_lemmas),
    let v  := `({name     := attr_name,
                 descr    := "hinst_lemma attribute set",
                 after_set := some $ λ n _ _,
@@ -128,19 +129,17 @@ do mk_hinst_lemma_attrs_core ff attr_names,
                   fail format!"invalid ematch lemma '{n}'",
                 -- allow unsetting
                 before_unset := some $ λ _ _, skip,
-                mk_cache := λ ns, do {
-                   hs₁ ← to_hinst_lemmas_core reducible ff ns hinst_lemmas.mk,
-                   hs₂ ← merge_hinst_lemma_attrs reducible ff attr_names hs₁,
-                   merge_hinst_lemma_attrs reducible tt simp_attr_names hs₂},
-                dependencies := [`reducibility] ++ attr_names ++ simp_attr_names } : caching_user_attribute hinst_lemmas),
+                cache_cfg := {
+                  mk_cache := λ ns, do {
+                    hs₁ ← to_hinst_lemmas_core reducible ff ns hinst_lemmas.mk,
+                    hs₂ ← merge_hinst_lemma_attrs reducible ff attr_names hs₁,
+                    merge_hinst_lemma_attrs reducible tt simp_attr_names hs₂},
+                  dependencies := [`reducibility] ++ attr_names ++ simp_attr_names}} : user_attribute hinst_lemmas),
    add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
    attribute.register attr_name
 
 meta def get_hinst_lemmas_for_attr (attr_name : name) : tactic hinst_lemmas :=
-do
-  cnst   ← return (expr.const attr_name []),
-  attr   ← eval_expr (caching_user_attribute hinst_lemmas) cnst,
-  caching_user_attribute.get_cache attr
+get_attribute_cache_dyn attr_name
 
 structure ematch_config :=
 (max_instances  : nat := 10000)
diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean
index c0ddf178c7..814e976ead 100644
--- a/library/init/meta/smt/rsimp.lean
+++ b/library/init/meta/smt/rsimp.lean
@@ -29,9 +29,10 @@ private meta def to_hinst_lemmas (m : transparency) (ex : name_set) : list name
     We say `ex_attr_name` is the "exception set". It is useful for excluding lemmas in `simp_attr_name`
     which are not good or redundant for ematching. -/
 meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name : name) (simp_attr_name : name) (ex_attr_name : name) : command :=
-do let t := `(caching_user_attribute hinst_lemmas),
+do let t := `(user_attribute hinst_lemmas),
    let v := `({name     := attr_name,
-                 descr    := sformat!"hinst_lemma attribute derived from '{simp_attr_name}'",
+               descr    := sformat!"hinst_lemma attribute derived from '{simp_attr_name}'",
+               cache_cfg := {
                  mk_cache := λ ns,
                  let aux := simp_attr_name in
                  let ex_attr := ex_attr_name in
@@ -41,7 +42,7 @@ do let t := `(caching_user_attribute hinst_lemmas),
                    ex   ← get_name_set_for_attr ex_attr,
                    to_hinst_lemmas reducible ex ss hs
                  },
-                 dependencies := [`reducibility, simp_attr_name]} : caching_user_attribute hinst_lemmas),
+                 dependencies := [`reducibility, simp_attr_name]}} : user_attribute hinst_lemmas),
    add_decl (declaration.defn attr_decl_name [] t v reducibility_hints.abbrev ff),
    attribute.register attr_decl_name
 
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 759c0a3441..78d9b83d77 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -27,7 +27,6 @@ name const * g_bool = nullptr;
 name const * g_bool_ff = nullptr;
 name const * g_bool_tt = nullptr;
 name const * g_combinator_K = nullptr;
-name const * g_caching_user_attribute = nullptr;
 name const * g_cast = nullptr;
 name const * g_cast_heq = nullptr;
 name const * g_char = nullptr;
@@ -404,7 +403,6 @@ void initialize_constants() {
     g_bool_ff = new name{"bool", "ff"};
     g_bool_tt = new name{"bool", "tt"};
     g_combinator_K = new name{"combinator", "K"};
-    g_caching_user_attribute = new name{"caching_user_attribute"};
     g_cast = new name{"cast"};
     g_cast_heq = new name{"cast_heq"};
     g_char = new name{"char"};
@@ -782,7 +780,6 @@ void finalize_constants() {
     delete g_bool_ff;
     delete g_bool_tt;
     delete g_combinator_K;
-    delete g_caching_user_attribute;
     delete g_cast;
     delete g_cast_heq;
     delete g_char;
@@ -1159,7 +1156,6 @@ name const & get_bool_name() { return *g_bool; }
 name const & get_bool_ff_name() { return *g_bool_ff; }
 name const & get_bool_tt_name() { return *g_bool_tt; }
 name const & get_combinator_K_name() { return *g_combinator_K; }
-name const & get_caching_user_attribute_name() { return *g_caching_user_attribute; }
 name const & get_cast_name() { return *g_cast; }
 name const & get_cast_heq_name() { return *g_cast_heq; }
 name const & get_char_name() { return *g_char; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 52755138fd..fb5c8bd1c6 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -29,7 +29,6 @@ name const & get_bool_name();
 name const & get_bool_ff_name();
 name const & get_bool_tt_name();
 name const & get_combinator_K_name();
-name const & get_caching_user_attribute_name();
 name const & get_cast_name();
 name const & get_cast_heq_name();
 name const & get_char_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 2fa0ebd2e5..3dadd93166 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -22,7 +22,6 @@ bool
 bool.ff
 bool.tt
 combinator.K
-caching_user_attribute
 cast
 cast_heq
 char
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index e5f3d1622f..9dccf8d592 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -423,10 +423,9 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) {
 
 static hinst_lemmas get_hinst_lemmas(name const & attr_name, tactic_state const & s) {
     auto & S      = get_vm_state();
-    vm_obj attr   = S.get_constant(attr_name);
-    vm_obj r      = caching_user_attribute_get_cache(mk_vm_unit(), attr, to_obj(s));
+    vm_obj r      = user_attribute_get_cache(S, s, attr_name);
     if (tactic::is_result_exception(r))
-        throw exception(sstream() << "failed to initialize sm_state, failed to retrieve attribute '" << attr_name << "'");
+        throw exception(sstream() << "failed to initialize smt_state, failed to retrieve attribute '" << attr_name << "'");
     vm_obj lemmas = tactic::get_result_value(r);
     if (!is_hinst_lemmas(lemmas))
         throw exception(sstream() << "failed to initialize smt_state, attribute '" << attr_name << "' is not a hinst_lemmas");
@@ -436,9 +435,9 @@ static hinst_lemmas get_hinst_lemmas(name const & attr_name, tactic_state const
 static simp_lemmas get_simp_lemmas(name const & attr_name, tactic_state const & s) {
     auto & S      = get_vm_state();
     vm_obj attr   = S.get_constant(attr_name);
-    vm_obj r      = caching_user_attribute_get_cache(mk_vm_unit(), attr, to_obj(s));
+    vm_obj r      = user_attribute_get_cache(S, s, attr_name);
     if (tactic::is_result_exception(r))
-        throw exception(sstream() << "failed to initialize sm_state, failed to retrieve attribute '" << attr_name << "'");
+        throw exception(sstream() << "failed to initialize smt_state, failed to retrieve attribute '" << attr_name << "'");
     vm_obj lemmas = tactic::get_result_value(r);
     if (!is_simp_lemmas(lemmas))
         throw exception(sstream() << "failed to initialize smt_state, attribute '" << attr_name << "' is not a simp_lemmas");
diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp
index 06c8067118..35db5e7efc 100644
--- a/src/library/tactic/user_attribute.cpp
+++ b/src/library/tactic/user_attribute.cpp
@@ -44,29 +44,25 @@ static environment update(environment const & env, user_attr_ext const & ext) {
 
 static environment add_user_attr(environment const & env, name const & d) {
     auto const & ty = env.get(d).get_type();
-    if (!is_constant(ty, get_user_attribute_name()) && !is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
-        throw exception("invalid [user_attribute], must be applied to definition of type user_attribute");
+    if (!is_app_of(ty, get_user_attribute_name(), 2))
+        throw exception("invalid [user_attribute] usage, must be applied to definition of type `user_attribute`");
 
     vm_state vm(env, options());
-    vm_obj o = vm.invoke(d, {});
-    if (is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
-        o = cfield(o, 0);
-    name const & n = to_name(cfield(o, 0));
-    if (n.is_anonymous())
+    vm_obj o = vm.get_constant(d);
+    name const & attr_name = to_name(cfield(o, 0));
+    if (attr_name.is_anonymous())
         throw exception(sstream() << "invalid user_attribute, anonymous attribute names are not allowed");
-    if (is_attribute(env, n))
-        throw exception(sstream() << "an attribute named [" << n << "] has already been registered");
+    if (is_attribute(env, attr_name))
+        throw exception(sstream() << "an attribute named [" << attr_name << "] has already been registered");
     std::string descr = to_string(cfield(o, 1));
     after_set_proc after_set;
     if (!is_none(cfield(o, 2))) {
         after_set = [=](environment const & env, io_state const & ios, name const & n, unsigned prio, bool persistent) {
             vm_state vm(env, ios.get_options());
             scope_vm_state scope(vm);
-            vm_obj o = vm.invoke(d, {});
-            if (is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
-                o = cfield(o, 0);
+            vm_obj o = vm.get_constant(d);
             tactic_state s = mk_tactic_state_for(env, options(), {}, local_context(), mk_true());
-            auto vm_r = vm.invoke(get_some_value(cfield(o, 2)), to_obj(n), to_obj(prio), mk_vm_bool(persistent), to_obj(s));
+            auto vm_r = vm.invoke(get_some_value(cfield(o, 2)), to_obj(n), mk_vm_nat(prio), mk_vm_bool(persistent), to_obj(s));
             tactic::report_exception(vm, vm_r);
             return tactic::to_state(tactic::get_result_state(vm_r)).env();
         };
@@ -76,9 +72,7 @@ static environment add_user_attr(environment const & env, name const & d) {
         before_unset = [=](environment const & env, io_state const & ios, name const & n, bool persistent) {
             vm_state vm(env, ios.get_options());
             scope_vm_state scope(vm);
-            vm_obj o = vm.invoke(d, {});
-            if (is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
-                o = cfield(o, 0);
+            vm_obj o = vm.get_constant(d);
             tactic_state s = mk_tactic_state_for(env, options(), {}, local_context(), mk_true());
             auto vm_r = vm.invoke(get_some_value(cfield(o, 3)), to_obj(n), mk_vm_bool(persistent), to_obj(s));
             tactic::report_exception(vm, vm_r);
@@ -87,7 +81,7 @@ static environment add_user_attr(environment const & env, name const & d) {
     }
 
     user_attr_ext ext = get_extension(env);
-    ext.m_attrs.insert(n, attribute_ptr(new basic_attribute(n, descr.c_str(), after_set, before_unset)));
+    ext.m_attrs.insert(attr_name, attribute_ptr(new basic_attribute(attr_name, descr.c_str(), after_set, before_unset)));
     return update(env, ext);
 }
 
@@ -166,11 +160,12 @@ static bool check_dep_fingerprints(environment const & env, list<name> const & d
     }
 }
 
-vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, vm_obj const & vm_s) {
+vm_obj user_attribute_get_cache_core(vm_obj const &, vm_obj const &, vm_obj const & vm_attr, vm_obj const & vm_s) {
     tactic_state const & s       = tactic::to_state(vm_s);
-    name const & n               = to_name(cfield(cfield(vm_attr, 0), 0));
-    vm_obj const & cache_handler = cfield(vm_attr, 1);
-    list<name> const & deps      = to_list_name(cfield(vm_attr, 2));
+    name const & n               = to_name(cfield(vm_attr, 0));
+    vm_obj const & cache_cfg     = cfield(vm_attr, 4);
+    vm_obj const & cache_handler = cfield(cache_cfg, 0);
+    list<name> const & deps      = to_list_name(cfield(cache_cfg, 1));
     LEAN_TACTIC_TRY;
     environment const & env = s.env();
     attribute const & attr  = get_attribute(env, n);
@@ -222,6 +217,11 @@ vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr,
     LEAN_TACTIC_CATCH(s);
 }
 
+vm_obj user_attribute_get_cache(vm_state & S, tactic_state const & s, name const & attr_name) {
+    vm_obj attr   = S.get_constant(attr_name);
+    return user_attribute_get_cache_core(mk_vm_unit(), mk_vm_unit(), attr, to_obj(s));
+}
+
 vm_obj set_basic_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj const & p, vm_obj const & vm_prio, vm_obj const & vm_s) {
     name const & attr_n    = to_name(vm_attr_n);
     name const & n         = to_name(vm_n);
@@ -273,7 +273,7 @@ vm_obj has_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj const
 void initialize_user_attribute() {
     DECLARE_VM_BUILTIN(name({"attribute", "get_instances"}),            attribute_get_instances);
     DECLARE_VM_BUILTIN(name({"attribute", "fingerprint"}),              attribute_fingerprint);
-    DECLARE_VM_BUILTIN(name({"caching_user_attribute", "get_cache"}),   caching_user_attribute_get_cache);
+    DECLARE_VM_BUILTIN(name({"user_attribute", "get_cache"}),           user_attribute_get_cache_core);
     DECLARE_VM_BUILTIN(name({"tactic",    "set_basic_attribute"}),      set_basic_attribute);
     DECLARE_VM_BUILTIN(name({"tactic",    "unset_attribute"}),          unset_attribute);
     DECLARE_VM_BUILTIN(name({"tactic",    "has_attribute"}),            has_attribute);
diff --git a/src/library/tactic/user_attribute.h b/src/library/tactic/user_attribute.h
index ac63ce63bb..124f233bc8 100644
--- a/src/library/tactic/user_attribute.h
+++ b/src/library/tactic/user_attribute.h
@@ -6,9 +6,10 @@ Author: Sebastian Ullrich
 */
 #pragma once
 #include "library/vm/vm.h"
+#include "library/tactic/tactic_state.h"
 
 namespace lean {
-vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, vm_obj const & vm_s);
+vm_obj user_attribute_get_cache(vm_state & S, tactic_state const & s, name const & attr_name);
 void initialize_user_attribute();
 void finalize_user_attribute();
 }
diff --git a/tests/lean/caching_user_attribute.lean b/tests/lean/caching_user_attribute.lean
index 13f6af35f4..41102f35cc 100644
--- a/tests/lean/caching_user_attribute.lean
+++ b/tests/lean/caching_user_attribute.lean
@@ -1,21 +1,25 @@
 @[user_attribute]
-meta def foo_attr : caching_user_attribute string :=
+meta def foo_attr : user_attribute string :=
 { name     := `foo, descr := "bar",
-  mk_cache := λ ns, return $ string.join (list.map (λ n, to_string n ++ "\n") ns),
-  dependencies := [] }
+  cache_cfg := {
+    mk_cache := λ ns, return $ string.join (list.map (λ n, to_string n ++ "\n") ns),
+    dependencies := []} }
 
 attribute [foo] eq.refl eq.mp
 
 set_option trace.user_attributes_cache true
 
 run_cmd do
-  s : string ← caching_user_attribute.get_cache foo_attr,
+  s : string ← foo_attr.get_cache,
   tactic.trace s,
-  s : string ← caching_user_attribute.get_cache foo_attr,
-  tactic.trace s,
-  tactic.set_basic_attribute `foo ``eq.mpr,
-  s : string ← caching_user_attribute.get_cache foo_attr,
+  s : string ← foo_attr.get_cache,
+  tactic.trace s
+
+attribute [foo] eq.mpr
+
+run_cmd do
+  s : string ← foo_attr.get_cache,
   tactic.trace s,
   tactic.set_basic_attribute `reducible ``eq.mp, -- should not affect [foo] cache
-  s : string ← caching_user_attribute.get_cache foo_attr,
+  s : string ← foo_attr.get_cache,
   tactic.trace s
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
index e2272eead6..f9e12d36af 100644
--- a/tests/lean/run/check_constants.lean
+++ b/tests/lean/run/check_constants.lean
@@ -27,7 +27,6 @@ run_cmd script_check_id `bool
 run_cmd script_check_id `bool.ff
 run_cmd script_check_id `bool.tt
 run_cmd script_check_id `combinator.K
-run_cmd script_check_id `caching_user_attribute
 run_cmd script_check_id `cast
 run_cmd script_check_id `cast_heq
 run_cmd script_check_id `char
diff --git a/tests/lean/run/eval_attr_cache.lean b/tests/lean/run/eval_attr_cache.lean
index 93afefb04b..0ecd8a5fd2 100644
--- a/tests/lean/run/eval_attr_cache.lean
+++ b/tests/lean/run/eval_attr_cache.lean
@@ -1,17 +1,18 @@
 open tactic
 @[user_attribute]
-meta def my_attr : caching_user_attribute (name → bool) :=
+meta def my_attr : user_attribute (name → bool) :=
 { name         := "my_attr",
   descr        := "my attr",
-  mk_cache     := λ ls, do {
-   let c := `(λ n : name, (name.cases_on n ff (λ _ _, to_bool (n ∈ ls)) (λ _ _, ff) : bool)),
-   eval_expr (name → bool) c
-  },
-  dependencies := []
+  cache_cfg := {
+    mk_cache   := λ ls, do {
+      let c := `(λ n : name, (name.cases_on n ff (λ _ _, to_bool (n ∈ ls)) (λ _ _, ff) : bool)),
+      eval_expr (name → bool) c
+    },
+    dependencies := []}
 }
 
 meta def my_tac : tactic unit :=
-do f ← caching_user_attribute.get_cache my_attr,
+do f ← my_attr.get_cache,
    trace (f `foo),
    return ()
 
diff --git a/tests/lean/slow_error.lean b/tests/lean/slow_error.lean
index 6f160ad4c1..a760e3e97e 100644
--- a/tests/lean/slow_error.lean
+++ b/tests/lean/slow_error.lean
@@ -1,4 +1,4 @@
-variable a : caching_user_attribute string
+variable a : user_attribute string
 variable b : string
 
 #check a = b
diff --git a/tests/lean/slow_error.lean.expected.out b/tests/lean/slow_error.lean.expected.out
index 6bcd5537ba..f53e302385 100644
--- a/tests/lean/slow_error.lean.expected.out
+++ b/tests/lean/slow_error.lean.expected.out
@@ -5,4 +5,4 @@ term
 has type
   string
 but is expected to have type
-  caching_user_attribute string
+  (user_attribute string)