From 2c0472252ea4cb0914b941b3a5a47fe33f7285f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Nov 2014 18:29:48 -0800
Subject: [PATCH] feat(frontends/lean): allow expressions to be used to define
 precedence, closes #335

---
 library/data/subtype.lean                     |  2 +-
 library/general_notation.lean                 |  4 ++
 library/priority.lean                         |  8 ++-
 library/tools/tactic.lean                     |  2 +-
 src/frontends/lean/class.cpp                  |  9 ++++
 src/frontends/lean/notation_cmd.cpp           | 50 +++++++++++++------
 src/library/aliases.cpp                       | 32 ++++++------
 src/library/aliases.h                         |  9 ++--
 tests/lean/inst.lean                          |  1 -
 .../lean/interactive/findp.input.expected.out |  1 +
 tests/lean/slow/path_groupoids.lean           |  9 ++--
 11 files changed, 82 insertions(+), 45 deletions(-)

diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index ead037793..78fc94bc1 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -9,7 +9,7 @@ open decidable
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binders:55 `|` r:(scoped 1 P, subtype P) `}` := r
+notation `{` binders:55 `|` r:(scoped:1 P, subtype P) `}` := r
 
 namespace subtype
   variables {A : Type} {P : A → Prop}
diff --git a/library/general_notation.lean b/library/general_notation.lean
index 41c9f84bd..ca0428be4 100644
--- a/library/general_notation.lean
+++ b/library/general_notation.lean
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: general_notation
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
+import data.num.decl
 
 /- General operations -/
 
@@ -22,6 +23,9 @@ notation `take`   binders `,` r:(scoped f, f) := r
 
 /- Logical operations and relations -/
 
+definition std.prec.max   : num := 1024 -- reflects max precedence used internally
+definition std.prec.arrow : num := 25
+
 reserve prefix `¬`:40
 reserve prefix `~`:40
 reserve infixr `∧`:35
diff --git a/library/priority.lean b/library/priority.lean
index ea309e247..930c7ec62 100644
--- a/library/priority.lean
+++ b/library/priority.lean
@@ -1,6 +1,4 @@
-import data.num
+import data.num.decl
 
-namespace priority
-definition default : num := 1000
-definition max     : num := 4294967295
-end priority
+definition std.priority.default : num := 1000
+definition std.priority.max     : num := 4294967295
diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean
index 89d007014..1479c2f2d 100644
--- a/library/tools/tactic.lean
+++ b/library/tools/tactic.lean
@@ -83,7 +83,7 @@ opaque definition revert_lst (ids : expr_list) : tactic := builtin
 notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
 
 infixl `;`:15 := and_then
-notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r
+notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
 
 definition try         (t : tactic) : tactic := [t | id]
 definition repeat1     (t : tactic) : tactic := t ; repeat t
diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp
index 733e926be..0a9782cdf 100644
--- a/src/frontends/lean/class.cpp
+++ b/src/frontends/lean/class.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 #include "library/reducible.h"
 #include "library/num.h"
+#include "library/aliases.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
@@ -180,10 +181,18 @@ list<name> get_class_instances(environment const & env, name const & c) {
     return ptr_to_list(s.m_instances.find(c));
 }
 
+static environment open_priority_namespace(parser & p) {
+    name prio("std", "priority");
+    environment env = using_namespace(p.env(), p.ios(), prio);
+    return overwrite_aliases(env, prio, name());
+}
+
 optional<unsigned> parse_instance_priority(parser & p) {
     if (p.curr_is_token(get_priority_tk())) {
         p.next();
         auto pos = p.pos();
+        environment env = open_priority_namespace(p);
+        parser::local_scope scope(p, env);
         expr val = p.parse_expr();
         val = type_checker(p.env()).whnf(val).first;
         if (optional<mpz> mpz_val = to_num(val)) {
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 2b99780a8..e1d9e5b38 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -13,6 +13,8 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "library/scoped_ext.h"
 #include "library/explicit.h"
+#include "library/num.h"
+#include "library/aliases.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 
@@ -30,22 +32,42 @@ static std::string parse_symbol(parser & p, char const * msg) {
     return n.to_string();
 }
 
-static optional<unsigned> parse_optional_precedence(parser & p) {
+static environment open_prec_namespace(parser & p) {
+    name prec("std", "prec");
+    environment env = using_namespace(p.env(), p.ios(), prec);
+    return overwrite_aliases(env, prec, name());
+}
+
+static unsigned parse_precedence_core(parser & p) {
+    auto pos = p.pos();
     if (p.curr_is_numeral()) {
-        return optional<unsigned>(p.parse_small_nat());
-    } else if (p.curr_is_token_or_id(get_max_tk())) {
+        return p.parse_small_nat();
+    } else {
+        environment env = open_prec_namespace(p);
+        parser::local_scope scope(p, env);
+        expr val = p.parse_expr(get_max_prec());
+        val = type_checker(p.env()).whnf(val).first;
+        if (optional<mpz> mpz_val = to_num(val)) {
+            if (!mpz_val->is_unsigned_int())
+                throw parser_error("invalid 'precedence', argument does not fit in a machine integer", pos);
+            return mpz_val->get_unsigned_int();
+        } else {
+            throw parser_error("invalid 'precedence', argument does not evaluate to a numeral", pos);
+        }
+    }
+}
+
+static optional<unsigned> parse_optional_precedence(parser & p) {
+    if (p.curr_is_token(get_colon_tk())) {
         p.next();
-        return optional<unsigned>(get_max_prec());
+        return some(parse_precedence_core(p));
     } else {
         return optional<unsigned>();
     }
 }
 
-static unsigned parse_precedence(parser & p, char const * msg) {
-    auto r = parse_optional_precedence(p);
-    if (!r)
-        throw parser_error(msg, p.pos());
-    return *r;
+static unsigned parse_precedence(parser & p) {
+    return parse_precedence_core(p);
 }
 
 LEAN_THREAD_VALUE(bool, g_allow_local, false);
@@ -108,7 +130,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
             throw parser_error("invalid notation declaration, invalid ':' occurrence "
                                "(declaration matches reserved notation)", p.pos());
         p.next();
-        prec = parse_precedence(p, "invalid notation declaration, numeral or 'max' expected");
+        prec = parse_precedence(p);
     }
 
     if (prec && k == mixfix_kind::infixr && *prec == 0)
@@ -224,7 +246,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
         p.next();
         if (p.curr_is_token(get_colon_tk())) {
             p.next();
-            unsigned prec = parse_precedence(p, "invalid notation declaration, precedence (small numeral) expected");
+            unsigned prec = parse_precedence(p);
             auto old_prec = get_precedence(get_token_table(env), tkcs);
             if (!old_prec || prec != *old_prec)
                 new_tokens.push_back(token_entry(tkcs, prec));
@@ -287,7 +309,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
     if (p.curr_is_token(get_colon_tk())) {
         p.next();
         if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) {
-            unsigned prec = parse_precedence(p, "invalid notation declaration, small numeral expected");
+            unsigned prec = parse_precedence(p);
             return mk_expr_action(prec);
         } else if (p.curr_is_token_or_id(get_prev_tk())) {
             p.next();
@@ -392,7 +414,7 @@ static optional<pair<action, parse_table>> find_next(optional<parse_table> const
 static unsigned parse_binders_rbp(parser & p) {
     if (p.curr_is_token(get_colon_tk())) {
         p.next();
-        return parse_precedence(p, "invalid binder/binders, precedence expected");
+        return parse_precedence(p);
     } else {
         return 0;
     }
@@ -695,7 +717,7 @@ static environment reserve_cmd(parser & p) {
 static environment precedence_cmd(parser & p) {
     std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected");
     p.check_token_next(get_colon_tk(), "invalid precedence declaration, ':' expected");
-    unsigned prec = parse_precedence(p, "invalid precedence declaration, numeral or 'max' expected");
+    unsigned prec = parse_precedence(p);
     return add_user_token(p.env(), tk.c_str(), prec);
 }
 
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 0fa8bb784..26fa44a57 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -32,9 +32,9 @@ struct aliases_ext : public environment_extension {
         name_map<name>        m_inv_level_aliases;
         state():m_in_context(false) {}
 
-        void add_expr_alias(name const & a, name const & e) {
+        void add_expr_alias(name const & a, name const & e, bool overwrite) {
             auto it = m_aliases.find(a);
-            if (it)
+            if (it && !overwrite)
                 m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
             else
                 m_aliases.insert(a, to_list(e));
@@ -45,8 +45,8 @@ struct aliases_ext : public environment_extension {
     state       m_state;
     list<state> m_scopes;
 
-    void add_expr_alias(name const & a, name const & e) {
-        m_state.add_expr_alias(a, e);
+    void add_expr_alias(name const & a, name const & e, bool overwrite) {
+        m_state.add_expr_alias(a, e, overwrite);
     }
 
     void add_level_alias(name const & a, name const & l) {
@@ -57,25 +57,25 @@ struct aliases_ext : public environment_extension {
         m_state.m_inv_level_aliases.insert(l, a);
     }
 
-    list<state> add_expr_alias_rec_core(list<state> const & scopes, name const & a, name const & e) {
+    list<state> add_expr_alias_rec_core(list<state> const & scopes, name const & a, name const & e, bool overwrite) {
         if (empty(scopes)) {
             return scopes;
         } else {
             state s = head(scopes);
-            s.add_expr_alias(a, e);
+            s.add_expr_alias(a, e, overwrite);
             if (s.m_in_context) {
-                return cons(s, add_expr_alias_rec_core(tail(scopes), a, e));
+                return cons(s, add_expr_alias_rec_core(tail(scopes), a, e, overwrite));
             } else {
                 return cons(s, tail(scopes));
             }
         }
     }
 
-    void add_expr_alias_rec(name const & a, name const & e) {
+    void add_expr_alias_rec(name const & a, name const & e, bool overwrite = false) {
         if (m_state.m_in_context) {
-            m_scopes = add_expr_alias_rec_core(m_scopes, a, e);
+            m_scopes = add_expr_alias_rec_core(m_scopes, a, e, overwrite);
         } else {
-            add_expr_alias(a, e);
+            add_expr_alias(a, e, overwrite);
         }
     }
 
@@ -138,15 +138,15 @@ static environment update(environment const & env, aliases_ext const & ext) {
     return env.update(g_ext->m_ext_id, std::make_shared<aliases_ext>(ext));
 }
 
-environment add_expr_alias(environment const & env, name const & a, name const & e) {
+environment add_expr_alias(environment const & env, name const & a, name const & e, bool overwrite) {
     aliases_ext ext = get_extension(env);
-    ext.add_expr_alias(a, e);
+    ext.add_expr_alias(a, e, overwrite);
     return update(env, ext);
 }
 
-environment add_expr_alias_rec(environment const & env, name const & a, name const & e) {
+environment add_expr_alias_rec(environment const & env, name const & a, name const & e, bool overwrite) {
     aliases_ext ext = get_extension(env);
-    ext.add_expr_alias_rec(a, e);
+    ext.add_expr_alias_rec(a, e, overwrite);
     return update(env, ext);
 }
 
@@ -187,14 +187,14 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
 }
 
 environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
-                        unsigned num_exceptions, name const * exceptions) {
+                        unsigned num_exceptions, name const * exceptions, bool overwrite) {
     aliases_ext ext = get_extension(env);
     env.for_each_declaration([&](declaration const & d) {
             if (!is_protected(env, d.get_name()) &&
                 is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
                 name a        = d.get_name().replace_prefix(prefix, new_prefix);
                 if (!a.is_anonymous())
-                    ext.add_expr_alias(a, d.get_name());
+                    ext.add_expr_alias(a, d.get_name(), overwrite);
             }
         });
     env.for_each_universe([&](name const & u) {
diff --git a/src/library/aliases.h b/src/library/aliases.h
index aca2e0b12..affbfb88a 100644
--- a/src/library/aliases.h
+++ b/src/library/aliases.h
@@ -11,12 +11,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \brief Add the alias \c a for \c e. */
-environment add_expr_alias(environment const & env, name const & a, name const & e);
+environment add_expr_alias(environment const & env, name const & a, name const & e, bool overwrite = false);
 /**
    \brief Add alias \c a for \c e, and also add it to all parent scopes
    until in a namespace scope.
 */
-environment add_expr_alias_rec(environment const & env, name const & a, name const & e);
+environment add_expr_alias_rec(environment const & env, name const & a, name const & e, bool overwrite = false);
 
 /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */
 optional<name> is_expr_aliased(environment const & env, name const & t);
@@ -48,7 +48,10 @@ optional<name> get_level_alias(environment const & env, name const & n);
    \remark \c new_prefix may be the anonymous name.
 */
 environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
-                        unsigned num_exceptions = 0, name const * exceptions = nullptr);
+                        unsigned num_exceptions = 0, name const * exceptions = nullptr, bool overwrite = false);
+inline environment overwrite_aliases(environment const & env, name const & prefix, name const & new_prefix) {
+    return add_aliases(env, prefix, new_prefix, 0, nullptr, true);
+}
 
 bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions);
 
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 6a87d2a70..b5d6dbda8 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,5 +1,4 @@
 import logic data.prod priority
-open priority
 set_option pp.notation false
 
 inductive C [class] (A : Type) :=
diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index a6c26e522..ced012280 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -5,6 +5,7 @@ false|Prop
 false.rec|Π (C : Type), false → C
 false_elim|false → ?c
 false.rec_on|Π (C : Type), false → C
+false.cases_on|Π (C : Type), false → C
 false.induction_on|∀ (C : Prop), false → C
 not_false_trivial|¬ false
 true_ne_false|¬ true = false
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 14e7f4769..9f276d2d6 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -2,13 +2,14 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 -- Ported from Coq HoTT
+import general_notation
 
 notation `assume` binders `,` r:(scoped f, f) := r
 notation `take`   binders `,` r:(scoped f, f) := r
 
 definition id {A : Type} (a : A) := a
 definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
-infixl `∘`:60 := compose
+infixr ∘ := compose
 
 -- Path
 -- ----
@@ -17,7 +18,7 @@ set_option unifier.max_steps 100000
 inductive path {A : Type} (a : A) : A → Type :=
 idpath : path a a
 definition idpath := @path.idpath
-infix `≈`:50 := path
+infix `≈` := path
 -- TODO: is this right?
 notation x `≈`:50 y `:>`:0 A:0 := @path A x y
 notation `idp`:max := idpath _     -- TODO: can we / should we use `1`?
@@ -32,7 +33,7 @@ path.rec (λu, u) q p
 definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
 path.rec (idpath x) p
 
-infixl `⬝`:75 := concat
+infixl `⬝` := concat
 postfix `^`:100 := inverse
 
 -- In Coq, these are not needed, because concat and inv are kept transparent
@@ -201,7 +202,7 @@ definition ap01 := ap
 definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
 Πx : A, f x ≈ g x
 
-infix `∼`:50 := pointwise_paths
+infix `∼` := pointwise_paths
 
 definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g :=
 λx, path.rec_on H idp