From 66a59d5b519148c5c0db812b2f46f6eaf68fb811 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Aug 2015 18:01:40 -0700
Subject: [PATCH] feat(frontends/lean/util): remove hack that overrides
 priority namespace

closes #789
---
 src/frontends/lean/util.cpp           | 35 +++++----------------------
 tests/lean/inst.lean                  |  2 +-
 tests/lean/run/notation_priority.lean |  6 ++---
 tests/lean/run/priority_test.lean     |  4 +--
 tests/lean/run/priority_test2.lean    | 12 ++++-----
 5 files changed, 18 insertions(+), 41 deletions(-)

diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 1677d559f..c4306b20a 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -429,14 +429,6 @@ 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) {
-    return overwrite_aliases(env, get_priority_namespace(), name());
-}
-
 char const * open_binder_string(binder_info const & bi, bool unicode) {
     if (bi.is_implicit()) return "{";
     else if (bi.is_inst_implicit()) return "[";
@@ -457,33 +449,18 @@ 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()));
+        environment env = open_num_notation(p.env());
         parser::local_scope scope(p, env);
         expr val = p.parse_expr();
-        val = elim_choice_fn()(val);
+        for_each(val, [](expr const & e, unsigned) {
+                if (is_choice(e))
+                    throw exception("invalid priority expression, it contains overloaded symbols");
+                return true;
+            });
         val = normalize(p.env(), val);
         if (optional<mpz> mpz_val = to_num(val)) {
             if (!mpz_val->is_unsigned_int())
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 0410953b2..441d6d555 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -8,7 +8,7 @@ definition val {A : Type} (c : C A) : A :=
 C.rec (λa, a) c
 
 constant magic (A : Type) : A
-definition C_magic [instance] [priority max] (A : Type) : C A :=
+definition C_magic [instance] [priority std.priority.max] (A : Type) : C A :=
 C.mk (magic A)
 
 definition C_prop [instance] : C Prop :=
diff --git a/tests/lean/run/notation_priority.lean b/tests/lean/run/notation_priority.lean
index b9274af24..9ffaa104d 100644
--- a/tests/lean/run/notation_priority.lean
+++ b/tests/lean/run/notation_priority.lean
@@ -13,15 +13,15 @@ example : a + b = f a b := rfl
 infix [priority 15] + := g
 example : a + b = g a b := rfl
 
-infix [priority default+1] + := f
+infix [priority std.priority.default+1] + := f
 infix + := g
 example : a + b = f a b := rfl
-infix [priority default+2] + := g
+infix [priority std.priority.default+2] + := g
 example : a + b = g a b := rfl
 
 infix + := f
 infix + := g
 example : a + b = f a b := rfl
 
-infix [priority default+1] + := g
+infix [priority std.priority.default+1] + := g
 example : a + b = g a b := rfl
diff --git a/tests/lean/run/priority_test.lean b/tests/lean/run/priority_test.lean
index 5f3732671..68b195982 100644
--- a/tests/lean/run/priority_test.lean
+++ b/tests/lean/run/priority_test.lean
@@ -3,7 +3,7 @@ open nat
 structure foo [class] :=
 (a : nat) (b : nat)
 
-definition i1 [instance] [priority default+1] : foo :=
+definition i1 [instance] [priority std.priority.default+1] : foo :=
 foo.mk 1 1
 
 definition i2 [instance] : foo :=
@@ -12,7 +12,7 @@ foo.mk 2 2
 example : foo.a = 1 :=
 rfl
 
-definition i3 [instance] [priority default+2] : foo :=
+definition i3 [instance] [priority std.priority.default+2] : foo :=
 foo.mk 3 3
 
 example : foo.a = 3 :=
diff --git a/tests/lean/run/priority_test2.lean b/tests/lean/run/priority_test2.lean
index b3e7cf6c2..05f9121c4 100644
--- a/tests/lean/run/priority_test2.lean
+++ b/tests/lean/run/priority_test2.lean
@@ -3,13 +3,13 @@ open nat
 structure foo [class] :=
 (a : nat) (b : nat)
 
-definition i1 [instance] [priority default-2] : foo :=
+definition i1 [instance] [priority std.priority.default-2] : foo :=
 foo.mk 1 1
 
 example : foo.a = 1 :=
 rfl
 
-definition i2 [instance] [priority default-1] : foo :=
+definition i2 [instance] [priority std.priority.default-1] : foo :=
 foo.mk 2 2
 
 example : foo.a = 2 :=
@@ -21,23 +21,23 @@ foo.mk 3 3
 example : foo.a = 3 :=
 rfl
 
-definition i4 [instance] [priority default-1] : foo :=
+definition i4 [instance] [priority std.priority.default-1] : foo :=
 foo.mk 4 4
 
 example : foo.a = 3 :=
 rfl
 
-attribute i4 [priority default+2]
+attribute i4 [priority std.priority.default+2]
 
 example : foo.a = 4 :=
 rfl
 
-attribute i1 [priority default+3]
+attribute i1 [priority std.priority.default+3]
 
 example : foo.a = 1 :=
 rfl
 
-attribute i2 [instance] [priority default+4]
+attribute i2 [instance] [priority std.priority.default+4]
 
 example : foo.a = 2 :=
 rfl