From a6ac98966aeed647da32cd88d7c71ca2b6307fba Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 Feb 2019 19:15:39 +0100 Subject: [PATCH] refactor(library/attribute_manager): parse attribute data from pexpr instead of abstract_parser --- src/frontends/lean/decl_attributes.cpp | 15 ++++++++- src/kernel/expr.h | 1 + src/library/attribute_manager.cpp | 13 +++++--- src/library/attribute_manager.h | 10 +++--- src/library/compiler/export_attribute.cpp | 8 ++++- src/library/compiler/extern_attribute.cpp | 40 +++++++++++++++-------- src/library/derive_attribute.cpp | 10 ++---- 7 files changed, 64 insertions(+), 33 deletions(-) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 1847e8d55d..e296c09336 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -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; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 919b44c4be..1bbff6a00c 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -224,6 +224,7 @@ expr mk_Type(); // Accessors inline literal const & lit_value(expr const & e) { lean_assert(is_lit(e)); return static_cast(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(cnstr_get_ref(e, 0)); } inline expr const & mdata_expr(expr const & e) { lean_assert(is_mdata(e)); return static_cast(cnstr_get_ref(e, 1)); } diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 91c2782f65..3e7615fab6 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -207,15 +207,18 @@ priority_queue 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 args; get_app_args(e, args); buffer 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); diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index bf86cab086..bf88283558 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -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 &) const; priority_queue 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(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; diff --git a/src/library/compiler/export_attribute.cpp b/src/library/compiler/export_attribute.cpp index b712d28158..21827218a9 100644 --- a/src/library/compiler/export_attribute.cpp +++ b/src/library/compiler/export_attribute.cpp @@ -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 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); } diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp index 7dd95c6691..e2b57092bb 100644 --- a/src/library/compiler/extern_attribute.cpp +++ b/src/library/compiler/extern_attribute.cpp @@ -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 args; get_app_args(e, args); + auto it = args.begin(); buffer entries; optional 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); } diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index 5e80e4566a..a7485f2f71 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -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 args; get_app_args(e, args); + m_args = exprs(args); } virtual void print(std::ostream & out) override { out << "<>";