From fa79b214b831179b51ebcab6edcee6881e2a0dc4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Mar 2015 16:17:01 -0800 Subject: [PATCH] fix(frontends/lean): allow 'attribute [priority ...]' --- src/frontends/lean/decl_cmds.cpp | 32 +++++++++++++++++++++++++----- src/library/class.cpp | 12 +++++++++-- src/library/class.h | 4 +++- tests/lean/run/priority_test2.lean | 15 ++++++++++++++ 4 files changed, 55 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index d8281206c2..e44df8cbb0 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -297,7 +297,8 @@ struct decl_attributes { optional m_priority; optional m_unfold_c_hint; - decl_attributes(bool def_only = true, bool is_abbrev = false):m_priority() { + decl_attributes(bool def_only = true, bool is_abbrev = false): + m_priority() { m_def_only = def_only; m_is_abbrev = is_abbrev; m_is_instance = false; @@ -350,7 +351,7 @@ struct decl_attributes { } } - void parse(parser & p) { + void parse(buffer const & ns, parser & p) { while (true) { auto pos = p.pos(); if (p.curr_is_token(get_instance_tk())) { @@ -389,8 +390,18 @@ struct decl_attributes { p.next(); } else if (auto it = parse_instance_priority(p)) { m_priority = *it; - if (!m_is_instance) - throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]'", pos); + if (!m_is_instance) { + if (ns.empty()) { + throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]'", pos); + } else { + for (name const & n : ns) { + if (!is_instance(p.env(), n)) + throw parser_error(sstream() << "invalid '[priority]' attribute, declaration '" << n + << "' must be marked as an '[instance]'", pos); + } + m_is_instance = true; + } + } } else if (p.curr_is_token(get_parsing_only_tk())) { if (!m_is_abbrev) throw parser_error("invalid '[parsing-only]' attribute, only abbreviations can be " @@ -410,6 +421,17 @@ struct decl_attributes { } } + void parse(name const & n, parser & p) { + buffer ns; + ns.push_back(n); + parse(ns, p); + } + + void parse(parser & p) { + buffer ns; + parse(ns, p); + } + environment apply(environment env, io_state const & ios, name const & d, bool persistent) { if (m_is_instance) { if (m_priority) { @@ -1113,7 +1135,7 @@ static environment attribute_cmd_core(parser & p, bool persistent) { } bool decl_only = false; decl_attributes attributes(decl_only); - attributes.parse(p); + attributes.parse(ds, p); environment env = p.env(); for (name const & d : ds) env = attributes.apply(env, p.ios(), d, persistent); diff --git a/src/library/class.cpp b/src/library/class.cpp index ab2cd78ecb..38ba73d0c3 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -46,6 +46,10 @@ struct class_state { return LEAN_INSTANCE_DEFAULT_PRIORITY; } + bool is_instance(name const & i) const { + return m_priorities.contains(i); + } + bool try_multiple_instances(name const & c) const { return m_multiple.contains(c); } @@ -73,8 +77,7 @@ struct class_state { auto lst = filter(*it, [&](name const & i1) { return i1 != i; }); m_instances.insert(c, insert(i, p, lst)); } - if (p != LEAN_INSTANCE_DEFAULT_PRIORITY) - m_priorities.insert(i, p); + m_priorities.insert(i, p); } void add_multiple(name const & c) { @@ -215,6 +218,11 @@ bool is_class(environment const & env, name const & c) { return s.m_instances.contains(c); } +bool is_instance(environment const & env, name const & i) { + class_state const & s = class_ext::get_state(env); + return s.is_instance(i); +} + list get_class_instances(environment const & env, name const & c) { class_state const & s = class_ext::get_state(env); return ptr_to_list(s.m_instances.find(c)); diff --git a/src/library/class.h b/src/library/class.h index 9832cc3fa1..7149f03275 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -13,8 +13,10 @@ environment add_class(environment const & env, name const & n, bool persistent = environment add_instance(environment const & env, name const & n, bool persistent = true); /** \brief Add a new 'class instance' to the environment. */ environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent); -/** \brief Return true iff \c c was declared with \c add_class . */ +/** \brief Return true iff \c c was declared with \c add_class. */ bool is_class(environment const & env, name const & c); +/** \brief Return true iff \c i was declared with \c add_instance. */ +bool is_instance(environment const & env, name const & i); /** \brief Return the instances of the given class. */ list get_class_instances(environment const & env, name const & c); /** \brief Return the classes in the given environment. */ diff --git a/tests/lean/run/priority_test2.lean b/tests/lean/run/priority_test2.lean index a4fc774a19..b3e7cf6c25 100644 --- a/tests/lean/run/priority_test2.lean +++ b/tests/lean/run/priority_test2.lean @@ -26,3 +26,18 @@ foo.mk 4 4 example : foo.a = 3 := rfl + +attribute i4 [priority default+2] + +example : foo.a = 4 := +rfl + +attribute i1 [priority default+3] + +example : foo.a = 1 := +rfl + +attribute i2 [instance] [priority default+4] + +example : foo.a = 2 := +rfl