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

refactor(frontends/lean): delegate all attribute parsing to decl_attributes

Browse source
This commit is contained in:
Sebastian Ullrich 2016-08-16 13:54:08 -04:00 • committed by Leonardo de Moura
parent e15e085126
commit 751f2d8b02
3 changed files with 25 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/builtin_cmds.cpp
View file

@ -50,6 +50,7 @@ Author: Leonardo de Moura
// #include "frontends/lean/tactic_hint.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parse_table.h"
#include "frontends/lean/decl_attributes.h"
namespace lean {
environment section_cmd(parser & p) {
@ -393,9 +394,16 @@ static environment register_simp_ext_cmd(parser & p) {
environment env = p.env();
name head = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected");
name simp_ext_name = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected");
unsigned prio = LEAN_DEFAULT_PRIORITY;
if (auto oprio = parse_priority(p))
prio = *oprio;
auto pos = p.pos();
decl_attributes attrs;
attrs.parse(p);
if (auto const & entry = head_opt(attrs.get_entries()))
throw parser_error(sstream() << "invalid #register_simp_ext_cmd command, unexpected attribute ["
<< entry->m_attr->get_name() << "]", pos);
if (attrs.get_priority())
prio = *attrs.get_priority();
bool persistent = true;
env = add_simp_extension(env, p.ios(), head, simp_ext_name, prio, persistent);
return env;

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

@ -12,12 +12,12 @@ Author: Leonardo de Moura
namespace lean {
class parser;
class decl_attributes {
private:
public:
struct entry {
attribute const * m_attr;
attr_data_ptr m_params;
};
private:
bool m_persistent;
bool m_parsing_only;
list<entry> m_entries;
@ -26,7 +26,9 @@ public:
decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {}
void parse(parser & p);
environment apply(environment env, io_state const & ios, name const & d) const;
list<entry> const & get_entries() const { return m_entries; }
bool is_parsing_only() const { return m_parsing_only; }
optional<unsigned > get_priority() const { return m_prio; }
operator bool() const { return static_cast<bool>(m_entries); }
};
}

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

@ -22,6 +22,7 @@ Author: Leonardo de Moura
#include "frontends/lean/tokens.h"
#include "frontends/lean/util.h"
#include "frontends/lean/nested_declaration.h"
#include "frontends/lean/decl_attributes.h"
namespace lean {
static std::string parse_symbol(parser & p, char const * msg) {
@ -682,17 +683,18 @@ struct notation_modifiers {
unsigned m_priority;
notation_modifiers():m_parse_only(false), m_priority(LEAN_DEFAULT_NOTATION_PRIORITY) {}
void parse(parser & p) {
while (true) {
if (p.curr_is_token(get_parsing_only_tk())) {
p.next();
p.check_token_next(get_rbracket_tk(), "invalid [parsing_only] attribute, ']' expected");
auto pos = p.pos();
decl_attributes attrs;
attrs.parse(p);
for (auto const & entry : attrs.get_entries()) {
if (entry.m_attr->get_name() == "parsing_only")
m_parse_only = true;
} else if (auto prio = parse_priority(p)) {
m_priority = *prio;
} else {
return;
}
else
throw parser_error(sstream() << "invalid notation: unexpected attribute ["
<< entry.m_attr->get_name() << "]", pos);
}
if (attrs.get_priority())
m_priority = *attrs.get_priority();
}
};