refactor(frontends/lean): move parse_priority to util

src/frontends/lean/decl_attributes.cpp

@@ -5,14 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/replace_visitor.h"
-#include "library/choice.h"
 #include "library/normalize.h"
 #include "library/reducible.h"
 #include "library/class.h"
 #include "library/relation_manager.h"
 #include "library/user_recursors.h"
 #include "library/coercion.h"
-#include "library/num.h"
 #include "library/simplifier/rewrite_rule_set.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/parser.h"
@@ -44,46 +42,6 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
     m_rewrite                = false;
 }
 
-struct elim_choice_fn : public replace_visitor {
-    name m_prio_ns;
-    elim_choice_fn():m_prio_ns(get_priority_namespace()) {}
-
-    virtual expr visit_macro(expr const & e) {
-        if (is_choice(e)) {
-            for (unsigned i = 0; i < get_num_choices(e); i++) {
-                expr const & c = get_choice(e, i);
-                if (is_constant(c) && const_name(c).get_prefix() == m_prio_ns)
-                    return c;
-            }
-            throw exception("invalid priority expression, it contains overloaded symbols");
-        } else {
-            return replace_visitor::visit_macro(e);
-        }
-    }
-};
-
-optional<unsigned> decl_attributes::parse_instance_priority(parser & p) {
-    if (p.curr_is_token(get_priority_tk())) {
-        p.next();
-        auto pos = p.pos();
-        environment env = open_priority_aliases(open_num_notation(p.env()));
-        parser::local_scope scope(p, env);
-        expr val = p.parse_expr();
-        val = elim_choice_fn()(val);
-        val = normalize(p.env(), val);
-        if (optional<mpz> mpz_val = to_num(val)) {
-            if (!mpz_val->is_unsigned_int())
-                throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos);
-            p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected");
-            return optional<unsigned>(mpz_val->get_unsigned_int());
-        } else {
-            throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
-        }
-    } else {
-        return optional<unsigned>();
-    }
-}
-
 void decl_attributes::parse(buffer<name> const & ns, parser & p) {
     while (true) {
         auto pos = p.pos();
@@ -126,7 +84,7 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
         } else if (p.curr_is_token(get_multiple_instances_tk())) {
             m_has_multiple_instances = true;
             p.next();
-        } else if (auto it = parse_instance_priority(p)) {
+        } else if (auto it = parse_priority(p)) {
             m_priority = *it;
             if (!m_is_instance) {
                 if (ns.empty()) {

src/frontends/lean/decl_attributes.h

@@ -34,9 +34,7 @@ class decl_attributes {
     optional<unsigned> m_priority;
     optional<unsigned> m_unfold_c_hint;
 
-    optional<unsigned> parse_instance_priority(parser & p);
     void parse(name const & n, parser & p);
-
 public:
     decl_attributes(bool is_abbrev = false, bool persistent = true);
     void parse(buffer<name> const & ns, parser & p);

src/frontends/lean/util.cpp

@@ -19,6 +19,8 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/abbreviation.h"
 #include "library/unfold_macros.h"
+#include "library/choice.h"
+#include "library/num.h"
 #include "library/replace_visitor.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
@@ -453,4 +455,45 @@ char const * close_binder_string(binder_info const & bi, bool unicode) {
 expr postprocess(environment const & env, expr const & e) {
     return eta_reduce(expand_abbreviations(env, unfold_untrusted_macros(env, e)));
 }
+
+
+struct elim_choice_fn : public replace_visitor {
+    name m_prio_ns;
+    elim_choice_fn():m_prio_ns(get_priority_namespace()) {}
+
+    virtual expr visit_macro(expr const & e) {
+        if (is_choice(e)) {
+            for (unsigned i = 0; i < get_num_choices(e); i++) {
+                expr const & c = get_choice(e, i);
+                if (is_constant(c) && const_name(c).get_prefix() == m_prio_ns)
+                    return c;
+            }
+            throw exception("invalid priority expression, it contains overloaded symbols");
+        } else {
+            return replace_visitor::visit_macro(e);
+        }
+    }
+};
+
+optional<unsigned> parse_priority(parser & p) {
+    if (p.curr_is_token(get_priority_tk())) {
+        p.next();
+        auto pos = p.pos();
+        environment env = open_priority_aliases(open_num_notation(p.env()));
+        parser::local_scope scope(p, env);
+        expr val = p.parse_expr();
+        val = elim_choice_fn()(val);
+        val = normalize(p.env(), val);
+        if (optional<mpz> mpz_val = to_num(val)) {
+            if (!mpz_val->is_unsigned_int())
+                throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos);
+            p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected");
+            return optional<unsigned>(mpz_val->get_unsigned_int());
+        } else {
+            throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
+        }
+    } else {
+        return optional<unsigned>();
+    }
+}
 }

src/frontends/lean/util.h

@@ -109,4 +109,7 @@ char const * close_binder_string(binder_info const & bi, bool unicode);
 
 /** \brief Cleanup expression after elaboration. */
 expr postprocess(environment const & env, expr const & e);
+
+/** \brief Parse `[priority <num>]`. Return none if current token is not `[priority` */
+optional<unsigned> parse_priority(parser & p);
 }