From 48c58af9b55e49edb3b2012f7884e0a1901b504d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Jun 2014 18:00:52 -0700
Subject: [PATCH] feat(frontends/lean/parser): allow explicit universe level to
 be provided to aliases and locals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp      | 33 ++++++++++++++++++++++--------
 src/frontends/lean/parser.h        |  1 +
 src/frontends/lean/token_table.cpp |  2 +-
 tests/lean/run/t4.lean             | 13 ++++++++++++
 4 files changed, 40 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/t4.lean

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 031fa305a..f6373a736 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/flet.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/replace_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "library/parser_nested_exception.h"
@@ -162,6 +163,26 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
     return rec_save_pos(deep_copy(e), p);
 }
 
+/** \brief Add \c ls to constants occurring in \c e. */
+expr parser::propagate_levels(expr const & e, levels const & ls) {
+    if (is_nil(ls)) {
+        return e;
+    } else {
+        return replace(e, [&](expr const & e, unsigned) {
+                if (is_constant(e)) {
+                    auto it = m_env.find(const_name(e));
+                    if (it) {
+                        level_param_names const & univ_ps = it->get_univ_params();
+                        levels const & old_ls = const_levels(e);
+                        if (length(old_ls) + length(ls) <= length(univ_ps))
+                            return some_expr(update_constant(e, append(old_ls, ls)));
+                    }
+                }
+                return none_expr();
+            });
+    }
+}
+
 pos_info parser::pos_of(expr const & e, pos_info default_pos) {
     auto it = m_pos_table->find(get_tag(e));
     if (it == m_pos_table->end())
@@ -615,11 +636,7 @@ expr parser::parse_id() {
     name id = get_name_val();
     next();
     auto it1 = m_local_decls.find(id);
-    // locals
-    if (it1 != m_local_decls.end())
-        return copy_with_new_pos(it1->second.first.m_local, p);
     buffer<level> lvl_buffer;
-    auto p_lvl = pos();
     levels ls;
     if (curr_is_token(g_llevel_curly)) {
         next();
@@ -629,6 +646,9 @@ expr parser::parse_id() {
         next();
         ls = to_list(lvl_buffer.begin(), lvl_buffer.end());
     }
+    // locals
+    if (it1 != m_local_decls.end())
+        return copy_with_new_pos(propagate_levels(it1->second.first.m_local, ls), p);
     optional<expr> r;
     // globals
     if (m_env.find(id))
@@ -636,14 +656,11 @@ expr parser::parse_id() {
     // aliases
     auto as = get_alias_exprs(m_env, id);
     if (!is_nil(as)) {
-        if (!is_nil(ls))
-            throw parser_error(sstream() << "explicit universe levels are not supported for overloaded/aliased identifier '" << id << "' "
-                               << "solutions: use a fully qualified name; or use non-overloaded alias", p_lvl);
         buffer<expr> new_as;
         if (r)
             new_as.push_back(*r);
         for (auto const & e : as) {
-            new_as.push_back(copy_with_new_pos(e, p));
+            new_as.push_back(copy_with_new_pos(propagate_levels(e, ls), p));
         }
         r = mk_choice(new_as.size(), new_as.data());
     }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 444d7f5a1..c44ac9e60 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -90,6 +90,7 @@ class parser {
 
     tag get_tag(expr e);
     expr copy_with_new_pos(expr const & e, pos_info p);
+    expr propagate_levels(expr const & e, levels const & ls);
 
     void updt_options();
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 7c41c8828..98cd8c933 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -12,7 +12,7 @@ namespace lean {
 static unsigned g_arrow_prec = 25;
 static unsigned g_max_prec   = std::numeric_limits<unsigned>::max();
 static unsigned g_plus_prec  = 65;
-static unsigned g_cup_prec   = 75;
+static unsigned g_cup_prec   = 60;
 unsigned get_arrow_prec() { return g_arrow_prec; }
 token_table add_command_token(token_table const & s, char const * token) {
     return insert(s, token, token_info(token));
diff --git a/tests/lean/run/t4.lean b/tests/lean/run/t4.lean
new file mode 100644
index 000000000..68c6fb3ff
--- /dev/null
+++ b/tests/lean/run/t4.lean
@@ -0,0 +1,13 @@
+namespace foo
+  definition f.{l} (A : Type.{l}) : Type.{l} := A
+  check f.{1}
+end
+
+variable N : Type.{1}
+section
+  parameter A : Type
+  definition g (a : A) (B : Type) : A := a
+  check g.{2}
+end
+check g.{2 3}
+