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

feat(frontends/lean/decl_attributes): add 'default_priority' attribute

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-01 13:27:08 -07:00
parent 837915f06b
commit 95ffdca3f7
3 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "library/attribute_manager.h"
#include "library/constants.h"
#include "library/normalize.h"
@ -15,6 +16,15 @@ Author: Leonardo de Moura
#include "frontends/lean/util.h"
namespace lean {
// ==========================================
// configuration options
static name * g_default_priority = nullptr;
unsigned get_default_priority(options const & opts) {
return opts.get_unsigned(*g_default_priority, LEAN_DEFAULT_PRIORITY);
}
// ==========================================
void decl_attributes::parse_core(parser & p, bool compact) {
while (true) {
auto pos = p.pos();
@ -111,7 +121,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
<< "]: no prior declaration on " << d);
env = entry.m_attr->unset(env, ios, d, m_persistent);
} else {
unsigned prio = m_prio ? *m_prio : LEAN_DEFAULT_PRIORITY;
unsigned prio = m_prio ? *m_prio : get_default_priority(ios.get_options());
env = entry.m_attr->set_untyped(env, ios, d, prio, entry.m_params, m_persistent);
}
}
@ -132,4 +142,12 @@ bool decl_attributes::has_class() const {
return false;
}
void initialize_decl_attributes() {
g_default_priority = new name{"default_priority"};
register_unsigned_option(*g_default_priority, LEAN_DEFAULT_PRIORITY, "default priority for attributes");
}
void finalize_decl_attributes() {
delete g_default_priority;
}
}

3
src/frontends/lean/decl_attributes.h
View file

@ -39,4 +39,7 @@ public:
bool has_class() const;
operator bool() const { return static_cast<bool>(m_entries); }
};
void initialize_decl_attributes();
void finalize_decl_attributes();
}

3
src/frontends/lean/init_module.cpp
View file

@ -24,9 +24,11 @@ Author: Leonardo de Moura
#include "frontends/lean/match_expr.h"
#include "frontends/lean/notation_cmd.h"
#include "frontends/lean/tactic_notation.h"
#include "frontends/lean/decl_attributes.h"
namespace lean {
void initialize_frontend_lean_module() {
initialize_decl_attributes();
initialize_prenum();
initialize_tokens();
initialize_token_table();
@ -69,5 +71,6 @@ void finalize_frontend_lean_module() {
finalize_token_table();
finalize_tokens();
finalize_prenum();
finalize_decl_attributes();
}
}