From 4248ad644df01aff502258d28ca347ec6b6d6fb2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Feb 2015 12:23:54 -0800
Subject: [PATCH] fix(frontends/lean): priority expressions parser

---
 src/frontends/lean/decl_cmds.cpp  | 21 +++++++++++++++++++++
 src/frontends/lean/util.cpp       |  7 +++++--
 src/frontends/lean/util.h         |  1 +
 tests/lean/run/priority_test.lean | 19 +++++++++++++++++++
 4 files changed, 46 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/priority_test.lean

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 332552b3e..90aa26b2a 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -21,6 +21,8 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/reducible.h"
 #include "library/coercion.h"
+#include "library/choice.h"
+#include "library/replace_visitor.h"
 #include "library/class.h"
 #include "library/abbreviation.h"
 #include "library/unfold_macros.h"
@@ -298,6 +300,24 @@ struct decl_attributes {
         m_has_multiple_instances = 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> parse_instance_priority(parser & p) {
         if (p.curr_is_token(get_priority_tk())) {
             p.next();
@@ -305,6 +325,7 @@ struct decl_attributes {
             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())
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index d73d640c2..61699b77e 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -452,8 +452,11 @@ environment open_prec_aliases(environment const & env) {
     return overwrite_aliases(env, prec, name());
 }
 
+name get_priority_namespace() {
+    return name("std", "priority");
+}
+
 environment open_priority_aliases(environment const & env) {
-    name prio("std", "priority");
-    return overwrite_aliases(env, prio, name());
+    return overwrite_aliases(env, get_priority_namespace(), name());
 }
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index f946b63bb..33cbfbf1a 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -111,4 +111,5 @@ environment open_num_notation(environment const & env);
 environment open_prec_aliases(environment const & env);
 /** \brief Open 'std.priority' aliases */
 environment open_priority_aliases(environment const & env);
+name get_priority_namespace();
 }
diff --git a/tests/lean/run/priority_test.lean b/tests/lean/run/priority_test.lean
new file mode 100644
index 000000000..5f3732671
--- /dev/null
+++ b/tests/lean/run/priority_test.lean
@@ -0,0 +1,19 @@
+open nat
+
+structure foo [class] :=
+(a : nat) (b : nat)
+
+definition i1 [instance] [priority default+1] : foo :=
+foo.mk 1 1
+
+definition i2 [instance] : foo :=
+foo.mk 2 2
+
+example : foo.a = 1 :=
+rfl
+
+definition i3 [instance] [priority default+2] : foo :=
+foo.mk 3 3
+
+example : foo.a = 3 :=
+rfl