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

refactor(library/attribute_manager): parse attribute data from pexpr instead of abstract_parser

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-15 19:15:39 +01:00 • committed by Leonardo de Moura
parent 03456ab752
commit a6ac98966a
7 changed files with 64 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "library/class.h"
#include "library/num.h"
#include "library/vm/vm_nat.h"
#include "library/sorry.h"
#include "frontends/lean/decl_attributes.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
@ -71,7 +72,19 @@ void decl_attributes::parse_core(parser & p, bool compact) {
}
}
}
auto data = deleted ? attr_data_ptr() : attr.parse_data(p);
attr_data_ptr data;
if (deleted) {
data = attr_data_ptr();
} else {
expr e = mk_const(id);
while (!p.curr_is_token("]") && !p.curr_is_token(",")) {
expr arg = p.parse_expr();
if (has_sorry(arg))
break;
e = mk_app(e, arg);
}
attr.parse_data(e);
}
m_entries = cons({&attr, data}, m_entries);
if (id == "parsing_only")
m_parsing_only = true;

1
src/kernel/expr.h
View file

@ -224,6 +224,7 @@ expr mk_Type();
// Accessors
inline literal const & lit_value(expr const & e) { lean_assert(is_lit(e)); return static_cast<literal const &>(cnstr_get_ref(e, 0)); }
inline bool is_nat_lit(expr const & e) { return is_lit(e) && lit_value(e).kind() == literal_kind::Nat; }
inline bool is_string_lit(expr const & e) { return is_lit(e) && lit_value(e).kind() == literal_kind::String; }
expr const & lit_type(expr const & e);
inline kvmap const & mdata_data(expr const & e) { lean_assert(is_mdata(e)); return static_cast<kvmap const &>(cnstr_get_ref(e, 0)); }
inline expr const & mdata_expr(expr const & e) { lean_assert(is_mdata(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }

13
src/library/attribute_manager.cpp
View file

@ -207,15 +207,18 @@ priority_queue<name, name_quick_cmp> attribute::get_instances_by_prio(environmen
return q;
}
attr_data_ptr attribute::parse_data(abstract_parser &) const {
attr_data_ptr attribute::parse_data(expr const &) const {
return get_default_attr_data();
}
void indices_attribute_data::parse(abstract_parser & p) {
void indices_attribute_data::parse(const expr & e) {
buffer<expr> args; get_app_args(e, args);
buffer<unsigned> vs;
while (p.curr_is_numeral()) {
auto pos = p.pos();
unsigned v = p.parse_small_nat();
for (expr const & arg : args) {
auto pos = get_pos_info_provider()->get_pos_info_or_some(arg);
if (!is_nat_lit(unwrap_pos(arg)))
throw parser_error("numeral expected", pos);
unsigned v = lit_value(unwrap_pos(arg)).get_nat().get_small_value();
if (v == 0)
throw parser_error("invalid attribute parameter, value must be positive", pos);
vs.push_back(v - 1);

10
src/library/attribute_manager.h
View file

@ -21,7 +21,7 @@ struct attr_data {
virtual unsigned hash() const {
return 0;
}
virtual void parse(abstract_parser &) {}
virtual void parse(expr const &) {}
virtual void print(std::ostream &) {}
virtual ~attr_data() {}
};
@ -65,7 +65,7 @@ public:
unsigned get_prio(environment const &, name const &) const;
virtual void get_instances(environment const &, buffer<name> &) const;
priority_queue<name, name_quick_cmp> get_instances_by_prio(environment const &) const;
virtual attr_data_ptr parse_data(abstract_parser &) const;
virtual attr_data_ptr parse_data(expr const &) const;
virtual environment unset(environment env, io_state const & ios, name const & n, bool persistent) const;
};
@ -125,9 +125,9 @@ public:
typed_attribute(name const & id, char const * descr, after_set_proc after_set = {}, before_unset_proc before_unset = {}) :
attribute(id, descr, after_set, before_unset) {}
virtual attr_data_ptr parse_data(abstract_parser & p) const override {
virtual attr_data_ptr parse_data(expr const & e) const override {
auto data = new Data;
data->parse(p);
data->parse(e);
return attr_data_ptr(data);
}
@ -197,7 +197,7 @@ struct indices_attribute_data : public attr_data {
void read(deserializer & d) {
m_idxs = read_list<unsigned>(d);
}
void parse(abstract_parser & p) override;
void parse(expr const &) override;
virtual void print(std::ostream & out) override {
for (auto p : m_idxs) {
out << " " << p + 1;

8
src/library/compiler/export_attribute.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "library/attribute_manager.h"
#include "library/constants.h"
#include "library/util.h"
namespace lean {
struct export_attr_data : public attr_data {
@ -14,7 +15,12 @@ struct export_attr_data : public attr_data {
export_attr_data() {}
virtual unsigned hash() const override { return m_id.hash(); }
virtual void parse(abstract_parser & p) override { m_id = p.parse_name(); }
virtual void parse(expr const & e) override {
buffer<expr> args; get_app_args(e, args);
if (args.size() != 1 || !is_const(extract_mdata(args[0])))
throw parser_error("constant expected", get_pos_info_provider()->get_pos_info_or_some(e));
m_id = const_name(extract_mdata(args[0]));
}
virtual void print(std::ostream & out) override { out << " " << m_id; }
void write(serializer & s) const { s << m_id; }
void read(deserializer & d) { m_id = read_name(d); }

40
src/library/compiler/extern_attribute.cpp
View file

@ -74,39 +74,51 @@ struct extern_attr_data : public attr_data {
- `@[extern cpp "foo" llvm adhoc]`
- `@[extern 2 cpp "io_prim_println"]
*/
virtual void parse(abstract_parser & p) override {
virtual void parse(expr const & e) override {
buffer<expr> args; get_app_args(e, args);
auto it = args.begin();
buffer<extern_entry> entries;
optional<unsigned> arity;
if (p.curr_is_token("]") || p.curr_is_token(",")) {
if (it == args.end()) {
// - `@[extern]`
entries.push_back(mk_adhoc_ext_entry("all"));
m_value = mk_extern_attr_data_value(arity, entries);
return;
}
if (p.curr_is_numeral()) {
arity = p.parse_small_nat();
expr arg = unwrap_pos(*it);
if (is_nat_lit(arg)) {
arity = lit_value(arg).get_nat().get_small_value();
it++;
}
if (p.curr_is_string()) {
if (it != args.end() && is_string_lit(arg = unwrap_pos(*it))) {
// - `@[extern "level_hash"]`
// - `@[extern 2 "level_hash"]`
std::string lit = p.parse_string_lit();
std::string lit = lit_value(arg).get_string().to_std_string();
entries.push_back(mk_std_ext_entry("all", lit.c_str()));
m_value = mk_extern_attr_data_value(arity, entries);
return;
}
while (p.curr_is_name()) {
name backend = p.parse_name();
if (p.curr_is_token_or_id("inline")) {
p.next();
std::string fn = p.parse_string_lit();
while (it != args.end()) {
arg = extract_mdata(*it);
if (!is_const(arg))
throw parser_error("constant expected", get_pos_info_provider()->get_pos_info_or_some(*it));
name backend = const_name(arg);
it++;
if (it != args.end() && is_const(extract_mdata(*it), "inline")) {
it++;
if (it == args.end() || !is_string_lit(arg = extract_mdata(*it)))
throw parser_error("string literal expected", get_pos_info_provider()->get_pos_info_or_some(*it));
std::string fn = lit_value(arg).get_string().to_std_string();
entries.push_back(mk_inline_ext_entry(backend, fn.c_str()));
} else if (p.curr_is_token("adhoc")) {
p.next();
} else if (it != args.end() && is_const(extract_mdata(*it), "adhoc")) {
entries.push_back(mk_adhoc_ext_entry(backend));
} else {
std::string fn = p.parse_string_lit();
if (it == args.end() || !is_string_lit(arg = extract_mdata(*it)))
throw parser_error("string literal expected", get_pos_info_provider()->get_pos_info_or_some(*it));
std::string fn = lit_value(arg).get_string().to_std_string();
entries.push_back(mk_std_ext_entry(backend, fn.c_str()));
}
it++;
}
m_value = mk_extern_attr_data_value(arity, entries);
}

10
src/library/derive_attribute.cpp
View file

@ -38,13 +38,9 @@ struct exprs_attribute_data : public attr_data {
void read(deserializer & d) {
m_args = read_exprs(d);
}
void parse(abstract_parser & p) override {
while (!p.curr_is_token("]") && !p.curr_is_token(",")) {
expr e = p.parse_expr(10000);
if (has_sorry(e))
break;
m_args = cons(e, m_args);
}
void parse(expr const & e) override {
buffer<expr> args; get_app_args(e, args);
m_args = exprs(args);
}
virtual void print(std::ostream & out) override {
out << "<>";