max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(init/meta/attribute): rename user_attribute.set_param to user_attribute.set

Browse source 
Setting the parameter value really is a side effect of setting the whole attribute
This commit is contained in:
Sebastian Ullrich 2017-09-14 18:46:05 +02:00
parent 928e982565
commit 7ff06b2184
4 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/changes.md
View file

@ -137,7 +137,7 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
`⟨h1, h2⟩`. This change is motivated by the previous one. Without it, `and.intro h1 h2` would be
pretty printed as `{left := h1, right := h2}`.
* User attributes can no longer be set with `set_basic_attribute`. You need to use `user_attribute.set_param` now.
* User attributes can no longer be set with `set_basic_attribute`. You need to use `user_attribute.set` now.
*API name changes*

6
library/init/meta/attribute.lean
View file

@ -47,15 +47,15 @@ meta def user_attribute.parse_reflect {α β : Type} (attr : user_attribute α
meta constant user_attribute.get_param_untyped {α β : Type} (attr : user_attribute α β) (decl : name)
: tactic expr
meta constant user_attribute.set_param_untyped {α β : Type} [reflected β] (attr : user_attribute α β) (decl : name)
meta constant user_attribute.set_untyped {α β : Type} [reflected β] (attr : user_attribute α β) (decl : name)
(val : expr) (persistent : bool) (prio : option nat := none) : tactic unit
meta def user_attribute.get_param {α β : Type} [reflected β] (attr : user_attribute α β) (n : name) : tactic β :=
attr.get_param_untyped n >>= tactic.eval_expr β
meta def user_attribute.set_param {α β : Type} [reflected β] (attr : user_attribute α β) (n : name)
meta def user_attribute.set {α β : Type} [reflected β] (attr : user_attribute α β) (n : name)
(val : β) (persistent : bool) (prio : option nat := none) : tactic unit :=
attr.set_param_untyped n (attr.reflect_param val) persistent prio
attr.set_untyped n (attr.reflect_param val) persistent prio
open tactic

14
src/library/tactic/user_attribute.cpp
View file

@ -93,11 +93,11 @@ vm_obj user_attribute_get_param_untyped(vm_obj const &, vm_obj const &, vm_obj c
LEAN_TACTIC_CATCH(s);
}
vm_obj user_attribute_set_param_untyped(expr const & beta, name const & attr_n, name const & n, expr const & val,
vm_obj user_attribute_set_untyped(expr const & beta, name const & attr_n, name const & n, expr const & val,
bool persistent, unsigned prio, tactic_state const & s) {
type_context ctx(s.env(), s.get_options());
if (!ctx.is_def_eq(beta, ctx.infer(val))) {
return tactic::mk_exception(sstream() << "set_param_untyped failed, '" << val << "' is not of type '" << beta << "'", s);
return tactic::mk_exception(sstream() << "set_untyped failed, '" << val << "' is not of type '" << beta << "'", s);
}
LEAN_TACTIC_TRY;
attribute const & attr = get_attribute(s.env(), attr_n);
@ -105,15 +105,15 @@ vm_obj user_attribute_set_param_untyped(expr const & beta, name const & attr_n,
environment new_env = user_attr->set(s.env(), get_global_ios(), n, prio, user_attribute_data(val), persistent);
return tactic::mk_success(set_env(s, new_env));
} else {
return tactic::mk_exception(sstream() << "set_param_untyped failed, '" << attr_n << "' is not a user attribute", s);
return tactic::mk_exception(sstream() << "set_untyped failed, '" << attr_n << "' is not a user attribute", s);
}
LEAN_TACTIC_CATCH(s);
}
vm_obj user_attribute_set_param_untyped(unsigned DEBUG_CODE(num), vm_obj const * args) {
vm_obj user_attribute_set_untyped(unsigned DEBUG_CODE(num), vm_obj const * args) {
lean_assert(num == 9);
unsigned prio = is_none(args[7]) ? LEAN_DEFAULT_PRIORITY : to_unsigned(get_some_value(args[7]));
return user_attribute_set_param_untyped(to_expr(args[2]), to_name(cfield(args[3], 0)), to_name(args[4]),
return user_attribute_set_untyped(to_expr(args[2]), to_name(cfield(args[3], 0)), to_name(args[4]),
to_expr(args[5]), to_bool(args[6]), prio, tactic::to_state(args[8]));
}
@ -350,8 +350,8 @@ void initialize_user_attribute() {
DECLARE_VM_BUILTIN(name({"attribute", "fingerprint"}), attribute_fingerprint);
DECLARE_VM_BUILTIN(name({"user_attribute", "get_cache"}), user_attribute_get_cache_core);
DECLARE_VM_BUILTIN(name({"user_attribute", "get_param_untyped"}), user_attribute_get_param_untyped);
declare_vm_builtin(name({"user_attribute", "set_param_untyped"}), "user_attribute_set_param_untyped",
9, user_attribute_set_param_untyped);
declare_vm_builtin(name({"user_attribute", "set_untyped"}), "user_attribute_set_untyped",
9, user_attribute_set_untyped);
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);

2
tests/lean/caching_user_attribute.lean
View file

@ -14,7 +14,7 @@ run_cmd do
tactic.trace s,
s : string ← foo_attr.get_cache,
tactic.trace s,
foo_attr.set_param `eq.mpr () tt,
foo_attr.set `eq.mpr () tt,
s : string ← foo_attr.get_cache,
tactic.trace s,
tactic.set_basic_attribute `reducible ``eq.mp, -- should not affect [foo] cache