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

feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware

Browse source
This commit is contained in:
Sebastian Ullrich 2016-08-16 17:51:33 -04:00 • committed by Leonardo de Moura
parent cd77f7167e
commit ca8be3857c
29 changed files with 428 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/init/meta/attribute.lean Normal file
View file

@ -0,0 +1,14 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
prelude
import init.meta.environment
meta_constant attribute.get_instances : environment → name → list name
/- The structure of a user-defined attribute. To declare a new attribute, define an instance of this
structure and annotate it with the (built-in) [user_attribute] attribute. -/
structure user_attribute :=
(descr : string)

2
library/init/meta/default.lean
View file

@ -5,7 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import init.meta.name init.meta.options init.meta.format init.meta.rb_map
import init.meta.level init.meta.expr init.meta.environment
import init.meta.level init.meta.expr init.meta.environment init.meta.attribute
import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic
import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics

4
src/frontends/lean/decl_attributes.cpp
View file

@ -36,10 +36,10 @@ void decl_attributes::parse(parser & p) {
throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
}
} else {
if (!is_attribute(name))
if (!is_attribute(p.env(), name))
throw parser_error(sstream() << "unknown attribute [" << name << "]", pos);
auto const & attr = get_attribute(name);
auto const & attr = get_attribute(p.env(), name);
for (auto const & entry : m_entries) {
if (are_incompatible(*entry.m_attr, attr)) {
throw parser_error(sstream() << "invalid attribute [" << name

7
src/frontends/lean/old_attributes.cpp
View file

@ -8,9 +8,10 @@ Author: Leonardo de Moura
namespace lean {
void initialize_old_attributes() {
register_attribute(basic_attribute("elim", "elimination rule that is eagerly applied by blast grinder"));
register_attribute(basic_attribute("no_pattern", "do not consider terms containing this declaration in the pattern inference procedure"));
register_attribute(basic_attribute("forward", "forward chaining"));
register_system_attribute(basic_attribute("elim", "elimination rule that is eagerly applied by blast grinder"));
register_system_attribute(basic_attribute("no_pattern",
"do not consider terms containing this declaration in the pattern inference procedure"));
register_system_attribute(basic_attribute("forward", "forward chaining"));
}
void finalize_old_attributes() {}
}

4
src/frontends/lean/pattern_attribute.cpp
View file

@ -12,8 +12,8 @@ bool has_pattern_attribute(environment const & env, name const & d) {
}
void initialize_pattern_attribute() {
register_attribute(basic_attribute("pattern", "mark that a definition can be used in a pattern"
"(remark: the dependent pattern matching compiler will unfold the definition)"));
register_system_attribute(basic_attribute("pattern", "mark that a definition can be used in a pattern"
"(remark: the dependent pattern matching compiler will unfold the definition)"));
}
void finalize_pattern_attribute() {

8
src/frontends/lean/print_cmd.cpp
View file

@ -248,7 +248,7 @@ static void print_attributes(parser const & p, name const & n) {
environment const & env = p.env();
std::ostream & out = p.ios().get_regular_stream();
buffer<attribute const *> attrs;
get_attributes(attrs);
get_attributes(p.env(), attrs);
std::sort(attrs.begin(), attrs.end(), [](attribute const * a1, attribute const * a2) {
return a1->get_name() < a2->get_name();
});
@ -621,7 +621,7 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token_or_id(get_attributes_tk())) {
p.next();
buffer<attribute const *> attrs;
get_attributes(attrs);
get_attributes(p.env(), attrs);
std::sort(attrs.begin(), attrs.end(), [](attribute const * a1, attribute const * a2) {
return a1->get_name() < a2->get_name();
});
@ -671,9 +671,9 @@ environment print_cmd(parser & p) {
else if (name == "light") {
// print_light_rules(p);
} else {
if (!is_attribute(name))
if (!is_attribute(p.env(), name))
throw parser_error(sstream() << "unknown attribute [" << name << "]", pos);
auto const & attr = get_attribute(name);
auto const & attr = get_attribute(p.env(), name);
print_attribute(p, attr);
}
} else if (print_polymorphic(p)) {

14
src/library/abbreviation.cpp
View file

@ -116,11 +116,15 @@ void initialize_abbreviation() {
g_class_name = new name("abbreviation");
g_key = new std::string("ABBREV");
abbrev_ext::initialize();
register_attribute(basic_attribute("parsing_only", "parsing-only abbreviation", [](environment const & env, io_state const &, name const & d, unsigned, bool) {
if (!is_abbreviation(env, d))
throw exception(sstream() << "invalid '[parsing_only]' attribute, " << d << " is not an abbreviation");
return env;
}));
register_system_attribute(basic_attribute("parsing_only", "parsing-only abbreviation",
[](environment const & env, io_state const &, name const & d, unsigned,
bool) {
if (!is_abbreviation(env, d))
throw exception(
sstream() << "invalid '[parsing_only]' attribute, " << d
<< " is not an abbreviation");
return env;
}));
}
void finalize_abbreviation() {

91
src/library/attribute_manager.cpp
View file

@ -15,29 +15,47 @@ Author: Leonardo de Moura
namespace lean {
static name_map<attribute_ptr> * g_attributes;
static name_map<attribute_ptr> * g_system_attributes;
static std::unique_ptr<user_attribute_ext> g_user_attribute_ext;
name_map<attribute_ptr> user_attribute_ext::get_attributes(environment const &) {
return {};
}
void set_user_attribute_ext(std::unique_ptr<user_attribute_ext> ext) {
g_user_attribute_ext = std::move(ext);
}
static std::vector<pair<name, name>> * g_incomp = nullptr;
static std::string * g_key = nullptr;
void register_attribute(attribute_ptr attr) {
lean_assert(!is_attribute(attr->get_name()));
(*g_attributes)[attr->get_name()] = attr;
static bool is_system_attribute(name const & attr) {
return g_system_attributes->find(attr) != nullptr;
}
void register_system_attribute(attribute_ptr attr) {
lean_assert(!is_system_attribute(attr->get_name()));
(*g_system_attributes)[attr->get_name()] = attr;
}
bool is_attribute(name const & attr) {
return g_attributes->find(attr) != nullptr;
bool is_attribute(environment const & env, name const & attr) {
return is_system_attribute(attr) || g_user_attribute_ext->get_attributes(env).find(attr) != nullptr;
}
[[ noreturn ]] void throw_unknown_attribute(name const & attr) {
throw exception(sstream() << "unknown attribute '" << attr << "'");
}
attribute const & get_attribute(name const & attr) {
auto it = g_attributes->find(attr);
attribute const & get_system_attribute(name const & attr) {
auto it = g_system_attributes->find(attr);
if (it)
return **it;
throw_unknown_attribute(attr);
throw exception(sstream() << "unknown system attribute '" << attr << "'");
}
attribute const & get_attribute(environment const & env, name const & attr) {
auto it = g_system_attributes->find(attr);
if (it)
return **it;
it = g_user_attribute_ext->get_attributes(env).find(attr);
if (it)
return **it;
throw exception(sstream() << "unknown attribute '" << attr << "'");
}
struct attr_record {
@ -64,7 +82,7 @@ struct attr_record_cmp {
};
struct attr_entry {
name m_attr;
name m_attr;
unsigned m_prio;
attr_record m_record;
@ -92,12 +110,20 @@ struct attr_config {
static void write_entry(serializer & s, entry const & e) {
s << e.m_attr << e.m_prio << e.m_record.m_decl;
lean_assert(e.m_record.m_data);
get_attribute(e.m_attr).write_entry(s, *e.m_record.m_data);
if (is_system_attribute(e.m_attr))
get_system_attribute(e.m_attr).write_entry(s, *e.m_record.m_data);
else
// dispatch over the extension, since we can't call get_attribute without an env
g_user_attribute_ext->write_entry(s, *e.m_record.m_data);
}
static entry read_entry(deserializer & d) {
entry e;
d >> e.m_attr >> e.m_prio >> e.m_record.m_decl;
e.m_record.m_data = get_attribute(e.m_attr).read_entry(d);
if (is_system_attribute(e.m_attr))
e.m_record.m_data = get_system_attribute(e.m_attr).read_entry(d);
else
// dispatch over the extension, since we can't call get_attribute without an env
e.m_record.m_data = g_user_attribute_ext->read_entry(d);
return e;
}
static optional<unsigned> get_fingerprint(entry const & e) {
@ -156,8 +182,8 @@ void indices_attribute_data::parse(abstract_parser & p) {
}
void register_incompatible(char const * attr1, char const * attr2) {
lean_assert(is_attribute(attr1));
lean_assert(is_attribute(attr2));
lean_assert(is_system_attribute(attr1));
lean_assert(is_system_attribute(attr2));
name s1(attr1);
name s2(attr2);
if (s1 > s2)
@ -165,18 +191,21 @@ void register_incompatible(char const * attr1, char const * attr2) {
g_incomp->emplace_back(s1, s2);
}
void get_attributes(buffer<attribute const *> & r) {
g_attributes->for_each([&](name const &, attribute_ptr const & attr) {
void get_attributes(environment const & env, buffer<attribute const *> & r) {
g_system_attributes->for_each([&](name const &, attribute_ptr const & attr) {
r.push_back(&*attr);
});
g_user_attribute_ext->get_attributes(env).for_each([&](name const &, attribute_ptr const & attr) {
r.push_back(&*attr);
});
}
bool has_attribute(environment const & env, char const * attr, name const & d) {
return static_cast<bool>(get_attribute(attr).get(env, d));
return static_cast<bool>(get_attribute(env, attr).get(env, d));
}
void get_attribute_instances(environment const & env, char const * attr, buffer<name> & r) {
return get_attribute(attr).get_instances(env, r);
return get_attribute(env, attr).get_instances(env, r);
}
priority_queue<name, name_quick_cmp> get_attribute_instances_by_prio(environment const & env, name const & attr) {
@ -188,14 +217,14 @@ priority_queue<name, name_quick_cmp> get_attribute_instances_by_prio(environment
environment set_attribute(environment const & env, io_state const & ios, char const * name,
lean::name const & d, unsigned prio, list<unsigned> const & params, bool persistent) {
auto const & attr = get_attribute(name);
auto const & attr = get_attribute(env, name);
lean_assert(dynamic_cast<indices_attribute const *>(&attr));
return static_cast<indices_attribute const &>(attr).set(env, ios, d, prio, {params}, persistent);
}
environment set_attribute(environment const & env, io_state const & ios, char const * name, lean::name const & d,
unsigned prio, bool persistent) {
auto const & attr = get_attribute(name);
auto const & attr = get_attribute(env, name);
lean_assert(dynamic_cast<basic_attribute const *>(&attr));
return static_cast<basic_attribute const &>(attr).set(env, ios, d, prio, persistent);
}
@ -205,11 +234,11 @@ environment set_attribute(environment const & env, io_state const & ios, char co
}
unsigned get_attribute_prio(environment const & env, name const & attr, name const & d) {
return get_attribute(attr).get_prio(env, d);
return get_attribute(env, attr).get_prio(env, d);
}
list<unsigned> get_attribute_params(environment const & env, name const & attr, name const & d) {
if (auto attribute = dynamic_cast<indices_attribute const *>(&get_attribute(attr))) {
if (auto attribute = dynamic_cast<indices_attribute const *>(&get_attribute(env, attr))) {
auto data = attribute->get_data(env, d);
lean_assert(data);
return data->m_idxs;
@ -226,9 +255,10 @@ bool are_incompatible(attribute const & attr1, attribute const & attr2) {
}
void initialize_attribute_manager() {
g_attributes = new name_map<attribute_ptr>();
g_incomp = new std::vector<pair<name, name>>();
g_key = new std::string("ATTR");
g_system_attributes = new name_map<attribute_ptr>();
g_user_attribute_ext.reset(new user_attribute_ext());
g_incomp = new std::vector<pair<name, name>>();
g_key = new std::string("ATTR");
attribute_ext::initialize();
}
@ -236,6 +266,7 @@ void finalize_attribute_manager() {
attribute_ext::finalize();
delete g_key;
delete g_incomp;
delete g_attributes;
g_user_attribute_ext.release();
delete g_system_attributes;
}
}

31
src/library/attribute_manager.h
View file

@ -100,9 +100,9 @@ protected:
return attr_data_ptr(data);
}
public:
typed_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
typed_attribute(name const & id, char const * descr, on_set_proc on_set) : attribute(id, descr),
m_on_set(on_set) {}
typed_attribute(char const * id, char const * descr) : typed_attribute(id, descr, {}) {}
typed_attribute(name const & id, char const * descr) : typed_attribute(id, descr, {}) {}
virtual attr_data_ptr parse_data(abstract_parser & p) const final override {
auto data = new Data;
@ -155,20 +155,31 @@ template class typed_attribute<indices_attribute_data>;
/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
typedef typed_attribute<indices_attribute_data> indices_attribute;
void register_attribute(attribute_ptr);
attribute const & get_attribute(name const & attr);
void get_attributes(buffer<attribute const *> &);
class user_attribute_ext {
public:
virtual name_map<attribute_ptr> get_attributes(environment const & env);
virtual void write_entry(serializer &, attr_data const &) {}
virtual attr_data_ptr read_entry(deserializer &) {
return attr_data_ptr(new attr_data);
}
};
/** \brief Register the user_attribute handlers, if included in the compilation */
void set_user_attribute_ext(std::unique_ptr<user_attribute_ext>);
void register_system_attribute(attribute_ptr);
template<typename Attribute>
void register_attribute(Attribute attr) {
register_attribute(attribute_ptr(new Attribute(attr)));
void register_system_attribute(Attribute attr) {
register_system_attribute(attribute_ptr(new Attribute(attr)));
}
void register_incompatible(char const * attr1, char const * attr2);
// TODO(sullrich): all of these should become members of/return attribute or a subclass
bool is_attribute(name const & attr);
bool is_attribute(environment const & env, name const & attr);
attribute const & get_attribute(environment const & env, name const & attr);
attribute const & get_system_attribute(name const & attr);
void get_attributes(environment const & env, buffer<attribute const *> &);
// TODO(sullrich): all of these should become members of/return attribute or a subclass
environment set_attribute(environment const & env, io_state const & ios, char const * attr,
name const & d, unsigned prio, list<unsigned> const & params, bool persistent);
environment set_attribute(environment const & env, io_state const & ios, char const * attr,

16
src/library/class.cpp
View file

@ -320,13 +320,17 @@ void initialize_class() {
g_key = new std::string("class");
class_ext::initialize();
register_attribute(basic_attribute("class", "type class", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_class(env, d, persistent);
}));
register_system_attribute(basic_attribute("class", "type class",
[](environment const & env, io_state const &, name const & d, unsigned,
bool persistent) {
return add_class(env, d, persistent);
}));
register_attribute(basic_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
return add_instance(env, d, prio, persistent);
}));
register_system_attribute(basic_attribute("instance", "type class instance",
[](environment const & env, io_state const &, name const & d,
unsigned prio, bool persistent) {
return add_instance(env, d, prio, persistent);
}));
}
void finalize_class() {

15
src/library/compiler/inliner.cpp
View file

@ -21,12 +21,15 @@ bool is_inline(environment const & env, name const & n) {
}
void initialize_inliner() {
register_attribute(basic_attribute("inline", "mark definition to always be inlined", [](environment const & env, io_state const &, name const & d, unsigned, bool) {
auto decl = env.get(d);
if (!decl.is_definition() || decl.is_theorem())
throw exception("invalid 'inline' use, only definitions can be marked as inline");
return env;
}));
register_system_attribute(basic_attribute("inline", "mark definition to always be inlined",
[](environment const & env, io_state const &, name const & d, unsigned,
bool) {
auto decl = env.get(d);
if (!decl.is_definition() || decl.is_theorem())
throw exception(
"invalid 'inline' use, only definitions can be marked as inline");
return env;
}));
}
void finalize_inliner() {

4
src/library/constants.cpp
View file

@ -323,6 +323,7 @@ name const * g_unification_constraint = nullptr;
name const * g_unification_constraint_mk = nullptr;
name const * g_unit = nullptr;
name const * g_unit_star = nullptr;
name const * g_user_attribute = nullptr;
name const * g_weak_order = nullptr;
name const * g_well_founded = nullptr;
name const * g_xor = nullptr;
@ -651,6 +652,7 @@ void initialize_constants() {
g_unification_constraint_mk = new name{"unification_constraint", "mk"};
g_unit = new name{"unit"};
g_unit_star = new name{"unit", "star"};
g_user_attribute = new name{"user_attribute"};
g_weak_order = new name{"weak_order"};
g_well_founded = new name{"well_founded"};
g_xor = new name{"xor"};
@ -980,6 +982,7 @@ void finalize_constants() {
delete g_unification_constraint_mk;
delete g_unit;
delete g_unit_star;
delete g_user_attribute;
delete g_weak_order;
delete g_well_founded;
delete g_xor;
@ -1308,6 +1311,7 @@ name const & get_unification_constraint_name() { return *g_unification_constrain
name const & get_unification_constraint_mk_name() { return *g_unification_constraint_mk; }
name const & get_unit_name() { return *g_unit; }
name const & get_unit_star_name() { return *g_unit_star; }
name const & get_user_attribute_name() { return *g_user_attribute; }
name const & get_weak_order_name() { return *g_weak_order; }
name const & get_well_founded_name() { return *g_well_founded; }
name const & get_xor_name() { return *g_xor; }

1
src/library/constants.h
View file

@ -325,6 +325,7 @@ name const & get_unification_constraint_name();
name const & get_unification_constraint_mk_name();
name const & get_unit_name();
name const & get_unit_star_name();
name const & get_user_attribute_name();
name const & get_weak_order_name();
name const & get_well_founded_name();
name const & get_xor_name();

1
src/library/constants.txt
View file

@ -318,6 +318,7 @@ unification_constraint
unification_constraint.mk
unit
unit.star
user_attribute
weak_order
well_founded
xor

12
src/library/init_module.cpp
View file

@ -67,9 +67,15 @@ namespace lean {
void initialize_library_core_module() {
initialize_constants();
initialize_trace();
initialize_module();
initialize_scoped_ext();
initialize_attribute_manager();
}
void finalize_library_core_module() {
finalize_attribute_manager();
finalize_scoped_ext();
finalize_module();
finalize_trace();
finalize_constants();
}
@ -98,11 +104,8 @@ void initialize_library_module() {
initialize_annotation();
initialize_quote();
initialize_explicit();
initialize_module();
initialize_protected();
initialize_private();
initialize_scoped_ext();
initialize_attribute_manager();
initialize_reducible();
initialize_aliases();
initialize_export_decl();
@ -160,10 +163,8 @@ void finalize_library_module() {
finalize_export_decl();
finalize_aliases();
finalize_reducible();
finalize_scoped_ext();
finalize_private();
finalize_protected();
finalize_module();
finalize_explicit();
finalize_quote();
finalize_annotation();
@ -179,7 +180,6 @@ void finalize_library_module() {
finalize_placeholder();
finalize_print();
finalize_fingerprint();
finalize_attribute_manager();
finalize_metavar_context();
finalize_local_context();

9
src/library/normalize.cpp
View file

@ -49,9 +49,12 @@ bool has_constructor_hint(environment const & env, name const & d) {
}
void initialize_normalize() {
register_attribute(indices_attribute("unfold", "unfold definition when the given positions are constructors"));
register_attribute(basic_attribute("unfold_full", "instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied"));
register_attribute(basic_attribute("constructor", "instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator"));
register_system_attribute(
indices_attribute("unfold", "unfold definition when the given positions are constructors"));
register_system_attribute(basic_attribute("unfold_full",
"instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied"));
register_system_attribute(basic_attribute("constructor",
"instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator"));
}
void finalize_normalize() {

10
src/library/reducible.cpp
View file

@ -36,7 +36,7 @@ template class typed_attribute<reducibility_attribute_data>;
typedef typed_attribute<reducibility_attribute_data> reducibility_attribute;
static reducibility_attribute const & get_reducibility_attribute() {
return static_cast<reducibility_attribute const &>(get_attribute("reducibility"));
return static_cast<reducibility_attribute const &>(get_system_attribute("reducibility"));
}
class proxy_attribute : public basic_attribute {
@ -70,11 +70,11 @@ public:
};
void initialize_reducible() {
register_attribute(reducibility_attribute("reducibility", "internal attribute for storing reducibility"));
register_system_attribute(reducibility_attribute("reducibility", "internal attribute for storing reducibility"));
register_attribute(proxy_attribute("reducible", "reducible", reducible_status::Reducible));
register_attribute(proxy_attribute("semireducible", "semireducible", reducible_status::Semireducible));
register_attribute(proxy_attribute("irreducible", "irreducible", reducible_status::Irreducible));
register_system_attribute(proxy_attribute("reducible", "reducible", reducible_status::Reducible));
register_system_attribute(proxy_attribute("semireducible", "semireducible", reducible_status::Semireducible));
register_system_attribute(proxy_attribute("irreducible", "irreducible", reducible_status::Irreducible));
register_incompatible("reducible", "semireducible");
register_incompatible("reducible", "irreducible");

32
src/library/relation_manager.cpp
View file

@ -325,21 +325,29 @@ is_relation_pred mk_is_relation_pred(environment const & env) {
void initialize_relation_manager() {
g_key = new std::string("REL");
rel_ext::initialize();
register_attribute(basic_attribute("refl", "reflexive relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_refl(env, d, persistent);
}));
register_system_attribute(basic_attribute("refl", "reflexive relation",
[](environment const & env, io_state const &, name const & d, unsigned,
bool persistent) {
return add_refl(env, d, persistent);
}));
register_attribute(basic_attribute("symm", "symmetric relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_symm(env, d, persistent);
}));
register_system_attribute(basic_attribute("symm", "symmetric relation",
[](environment const & env, io_state const &, name const & d, unsigned,
bool persistent) {
return add_symm(env, d, persistent);
}));
register_attribute(basic_attribute("trans", "transitive relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_trans(env, d, persistent);
}));
register_system_attribute(basic_attribute("trans", "transitive relation",
[](environment const & env, io_state const &, name const & d, unsigned,
bool persistent) {
return add_trans(env, d, persistent);
}));
register_attribute(basic_attribute("subst", "substitution", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_subst(env, d, persistent);
}));
register_system_attribute(basic_attribute("subst", "substitution",
[](environment const & env, io_state const &, name const & d, unsigned,
bool persistent) {
return add_subst(env, d, persistent);
}));
}
void finalize_relation_manager() {

23
src/library/tactic/backward/backward_lemmas.cpp
View file

@ -163,16 +163,19 @@ vm_obj tactic_backward_lemmas_find(vm_obj const & lemmas, vm_obj const & h, vm_o
void initialize_backward_lemmas() {
register_trace_class(name{"tactic", "back_chaining"});
register_attribute(intro_attribute("intro", "introduction rule for backward chaining", [](environment const & env, io_state const & ios, name const & c, unsigned, intro_attr_data data, bool) {
if (data.m_eager)
return env; // FIXME: support old blast attributes
aux_type_context ctx(env, ios.get_options());
auto index = get_backward_target(ctx, c);
if (!index || index->kind() != expr_kind::Constant)
throw exception(sstream() << "invalid [intro] attribute for '" << c
<< "', head symbol of resulting type must be a constant");
return env;
}));
register_system_attribute(intro_attribute("intro", "introduction rule for backward chaining",
[](environment const & env, io_state const & ios, name const & c,
unsigned, intro_attr_data data, bool) {
if (data.m_eager)
return env; // FIXME: support old blast attributes
aux_type_context ctx(env, ios.get_options());
auto index = get_backward_target(ctx, c);
if (!index || index->kind() != expr_kind::Constant)
throw exception(
sstream() << "invalid [intro] attribute for '" << c
<< "', head symbol of resulting type must be a constant");
return env;
}));
DECLARE_VM_BUILTIN(name({"tactic", "mk_back_lemmas_core"}), tactic_mk_backward_lemmas);
DECLARE_VM_BUILTIN(name({"tactic", "back_lemmas_insert_core"}), tactic_backward_lemmas_insert);
DECLARE_VM_BUILTIN(name({"tactic", "back_lemmas_find"}), tactic_backward_lemmas_find);

2
src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
View file

@ -146,7 +146,7 @@ void initialize_defeq_simp_lemmas() {
defeq_simp_lemmas_ext::initialize();
register_attribute(basic_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma));
register_system_attribute(basic_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma));
}
void finalize_defeq_simp_lemmas() {

4
src/library/tactic/simplifier/simp_lemmas.cpp
View file

@ -671,8 +671,8 @@ void initialize_simp_lemmas() {
DECLARE_VM_BUILTIN(name({"tactic", "mk_empy_simp_lemmas"}), tactic_mk_empty_simp_lemmas);
DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_insert_core"}), tactic_simp_lemmas_insert);
register_attribute(basic_attribute("simp", "simplification lemma", on_add_simp_lemma));
register_attribute(basic_attribute("congr", "congruence lemma", on_add_congr_lemma));
register_system_attribute(basic_attribute("simp", "simplification lemma", on_add_simp_lemma));
register_system_attribute(basic_attribute("congr", "congruence lemma", on_add_congr_lemma));
}
void finalize_simp_lemmas() {

2
src/library/unification_hint.cpp
View file

@ -204,7 +204,7 @@ void initialize_unification_hint() {
unification_hint_ext::initialize();
register_attribute(basic_attribute("unify", "unification hint", add_unification_hint));
register_system_attribute(basic_attribute("unify", "unification hint", add_unification_hint));
}
void finalize_unification_hint() {

13
src/library/user_recursors.cpp
View file

@ -344,11 +344,14 @@ has_recursors_pred::has_recursors_pred(environment const & env):
void initialize_user_recursors() {
g_key = new std::string("UREC");
recursor_ext::initialize();
register_attribute(indices_attribute("recursor", "user defined recursor", [](environment const & env, io_state const &, name const & n, unsigned, indices_attribute_data const & data, bool persistent) {
if (data.m_idxs && tail(data.m_idxs))
throw exception(sstream() << "invalid [recursor] declaration, expected at most one parameter");
return add_user_recursor(env, n, head_opt(data.m_idxs), persistent);
}));
register_system_attribute(indices_attribute("recursor", "user defined recursor",
[](environment const & env, io_state const &, name const & n, unsigned,
indices_attribute_data const & data, bool persistent) {
if (data.m_idxs && tail(data.m_idxs))
throw exception(sstream()
<< "invalid [recursor] declaration, expected at most one parameter");
return add_user_recursor(env, n, head_opt(data.m_idxs), persistent);
}));
}
void finalize_user_recursors() {

2
src/library/vm/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp init_module.cpp)
vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp user_attribute.cpp init_module.cpp)

3
src/library/vm/init_module.cpp
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_environment.h"
#include "library/vm/user_attribute.h"
namespace lean {
void initialize_vm_core_module() {
@ -37,8 +38,10 @@ void initialize_vm_core_module() {
initialize_vm_exceptional();
initialize_vm_declaration();
initialize_vm_environment();
initialize_user_attribute();
}
void finalize_vm_core_module() {
finalize_user_attribute();
finalize_vm_environment();
finalize_vm_declaration();
finalize_vm_exceptional();

105
src/library/vm/user_attribute.cpp Normal file
View file

@ -0,0 +1,105 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sebastian Ullrich
*/
#include <string>
#include "library/attribute_manager.h"
#include "library/constants.h"
#include "library/scoped_ext.h"
#include "library/vm/vm_environment.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_string.h"
#include "util/sstream.h"
namespace lean {
static std::string * g_key = nullptr;
struct user_attr_data : public attr_data {
// to be filled
void write(serializer &) const {
lean_unreachable();
}
void read(deserializer &) {
lean_unreachable();
}
};
class user_attribute : public typed_attribute<user_attr_data> {
public:
user_attribute(name const & id, char const * descr) : typed_attribute(id, descr) {}
};
typedef name_map<attribute_ptr> user_attribute_state;
struct user_attribute_config {
typedef name entry;
typedef user_attribute_state state;
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
if (is_attribute(env, e))
throw exception(sstream() << "an attribute named [" << e << "] has already been registered");
auto const & ty = env.get(e).get_type();
if (!is_constant(ty, get_user_attribute_name()))
throw exception("malformed [user_attribute] application, definition must be an instance of user_attribute");
vm_state vm(env);
vm_decl const & vm_decl = *vm.get_decl(e);
vm_obj const & o = vm.invoke(e, {});
std::string descr = to_string(o);
s.insert(e, attribute_ptr(new user_attribute(e, descr.c_str())));
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e;
}
static entry read_entry(deserializer & d) {
name e;
d >> e;
return e;
}
static optional<unsigned> get_fingerprint(entry const & e) {
return some(e.hash());
}
};
typedef scoped_ext<user_attribute_config> scope_ext;
class actual_user_attribute_ext : public user_attribute_ext {
public:
virtual name_map<attribute_ptr> get_attributes(environment const & env) override {
return scope_ext::get_state(env);
}
};
static vm_obj attribute_get_instances(vm_obj const & vm_env, vm_obj const & vm_n) {
auto const & env = to_env(vm_env);
buffer<name> b;
get_attribute(env, to_name(vm_n)).get_instances(env, b);
return to_obj(b);
}
void initialize_user_attribute() {
DECLARE_VM_BUILTIN(name({"attribute", "get_instances"}), attribute_get_instances);
g_key = new std::string("USR_ATTR");
scope_ext::initialize();
register_system_attribute(basic_attribute("user_attribute", "declare user-defined attribute",
[](environment const & env, io_state const & ios, name const & d, unsigned,
bool persistent) {
return scope_ext::add_entry(env, ios, d, persistent);
}));
set_user_attribute_ext(std::unique_ptr<user_attribute_ext>(new actual_user_attribute_ext));
}
void finalize_user_attribute() {
scope_ext::finalize();
delete g_key;
}
}

12
src/library/vm/user_attribute.h Normal file
View file

@ -0,0 +1,12 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sebastian Ullrich
*/
#pragma once
namespace lean {
void initialize_user_attribute();
void finalize_user_attribute();
}

38
tests/lean/user_attribute.lean Normal file
View file

@ -0,0 +1,38 @@
attribute [user_attribute]
definition foo := ⦃user_attribute, descr := "bar"⦄
print attributes
attribute [foo] eq.refl
print [foo]
print eq.refl
-- compound names
attribute [user_attribute]
definition foo.baz := ⦃user_attribute, descr := "bar"⦄
print attributes
attribute [foo.baz] eq.refl
print [foo.baz]
print eq.refl
-- can't redeclare attributes
attribute [user_attribute]
definition reducible := ⦃user_attribute, descr := "bar"⦄
-- wrong type
attribute [user_attribute]
definition bar := "bar"
section
variable x : string
attribute [user_attribute]
definition bar := ⦃user_attribute, descr := x⦄
end

64
tests/lean/user_attribute.lean.expected.out Normal file
View file

@ -0,0 +1,64 @@
[class] type class
[congr] congruence lemma
[constructor] instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator
[defeq] defeq simp lemma
[elim] elimination rule that is eagerly applied by blast grinder
[foo] bar
[forward] forward chaining
[inline] mark definition to always be inlined
[instance] type class instance
[intro] introduction rule for backward chaining
[irreducible] irreducible
[no_pattern] do not consider terms containing this declaration in the pattern inference procedure
[parsing_only] parsing-only abbreviation
[pattern] mark that a definition can be used in a pattern(remark: the dependent pattern matching compiler will unfold the definition)
[recursor] user defined recursor
[reducibility] internal attribute for storing reducibility
[reducible] reducible
[refl] reflexive relation
[semireducible] semireducible
[simp] simplification lemma
[subst] substitution
[symm] symmetric relation
[trans] transitive relation
[unfold] unfold definition when the given positions are constructors
[unfold_full] instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied
[unify] unification hint
[user_attribute] declare user-defined attribute
eq.refl
attribute [foo, refl]
constructor eq.refl : ∀ {A : Type} (a : A), a = a
[class] type class
[congr] congruence lemma
[constructor] instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator
[defeq] defeq simp lemma
[elim] elimination rule that is eagerly applied by blast grinder
[foo] bar
[foo.baz] bar
[forward] forward chaining
[inline] mark definition to always be inlined
[instance] type class instance
[intro] introduction rule for backward chaining
[irreducible] irreducible
[no_pattern] do not consider terms containing this declaration in the pattern inference procedure
[parsing_only] parsing-only abbreviation
[pattern] mark that a definition can be used in a pattern(remark: the dependent pattern matching compiler will unfold the definition)
[recursor] user defined recursor
[reducibility] internal attribute for storing reducibility
[reducible] reducible
[refl] reflexive relation
[semireducible] semireducible
[simp] simplification lemma
[subst] substitution
[symm] symmetric relation
[trans] transitive relation
[unfold] unfold definition when the given positions are constructors
[unfold_full] instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied
[unify] unification hint
[user_attribute] declare user-defined attribute
eq.refl
attribute [foo, foo.baz, refl]
constructor eq.refl : ∀ {A : Type} (a : A), a = a
user_attribute.lean:25:0: error: an attribute named [reducible] has already been registered
user_attribute.lean:30:0: error: malformed [user_attribute] application, definition must be an instance of user_attribute
user_attribute.lean:36:2: error: malformed [user_attribute] application, definition must be an instance of user_attribute