feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_cmds.cpp

@@ -4,18 +4,35 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/sstream.h"
 #include "library/io_state_stream.h"
+#include "library/scoped_ext.h"
+#include "library/aliases.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
 static name g_raw("raw");
+static void check_atomic(name const & n) {
+    if (!n.is_atomic())
+        throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
+}
 
 environment universe_cmd(parser & p) {
     if (p.curr_is_identifier()) {
-        // TODO(Leo): take namespace and scopes into account
         name n = p.get_name_val();
+        check_atomic(n);
         p.next();
-        return p.env().add_universe(n);
+        environment env = p.env();
+        if (in_section(env)) {
+            p.add_local_level(n, mk_param_univ(n));
+        } else {
+            name const & ns = get_namespace(env);
+            name full_n  = ns + n;
+            env = env.add_universe(full_n);
+            if (!ns.is_anonymous())
+                env = add_alias(env, n, mk_global_univ(full_n));
+        }
+        return env;
     } else {
         throw parser_error("invalid universe declaration, identifier expected", p.cmd_pos());
     }
@@ -35,10 +52,35 @@ environment print_cmd(parser & p) {
     return p.env();
 }
 
+environment section_cmd(parser & p) {
+    p.push_local_scope();
+    return push_scope(p.env(), p.ios());
+}
+
+environment namespace_cmd(parser & p) {
+    if (p.curr_is_identifier()) {
+        name n = p.get_name_val();
+        check_atomic(n);
+        p.next();
+        return push_scope(p.env(), p.ios(), n);
+    } else {
+        throw parser_error("invalid namespace declaration, identifier expected", p.cmd_pos());
+    }
+}
+
+environment end_scoped_cmd(parser & p) {
+    if (in_section(p.env()))
+        p.pop_local_scope();
+    return pop_scope(p.env());
+}
+
 cmd_table init_cmd_table() {
     cmd_table r;
-    add_cmd(r, cmd_info("print",    "print a string", print_cmd));
-    add_cmd(r, cmd_info("universe", "declare a global universe level", universe_cmd));
+    add_cmd(r, cmd_info("print",     "print a string", print_cmd));
+    add_cmd(r, cmd_info("universe",  "declare a global universe level", universe_cmd));
+    add_cmd(r, cmd_info("section",   "open a new section", section_cmd));
+    add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd));
+    add_cmd(r, cmd_info("end",       "close the current namespace/section", end_scoped_cmd));
     return r;
 }
 

src/frontends/lean/builtin_exprs.cpp

@@ -19,7 +19,7 @@ static expr parse_Type(parser & p, unsigned, expr const *) {
         p.check_token_next(g_rcurly, "invalid Type expression, '}' expected");
         return mk_sort(l);
     } else {
-        return mk_sort(p.mk_new_level_param());
+        return p.mk_Type();
     }
 }
 

src/frontends/lean/parser.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "util/script_exception.h"
 #include "util/sstream.h"
+#include "util/flet.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
@@ -42,6 +43,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_env(env), m_ios(ios), m_ss(ss),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name), m_pos_table(std::make_shared<pos_info_table>()) {
+    m_type_use_placeholder = true;
     m_found_errors = false;
     updt_options();
     m_next_tag_idx = 0;
@@ -193,13 +195,31 @@ expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
     return save_pos(::lean::mk_app(fn, arg), p);
 }
 
-void parser::add_local_entry(name const & n, expr const & e) {
+void parser::push_local_scope() {
+    m_local_level_decls.push();
+    m_local_decls.push();
+}
+
+void parser::pop_local_scope() {
+    m_local_level_decls.pop();
+    m_local_decls.pop();
+}
+
+void parser::add_local_level(name const & n, level const & l) {
+    if (m_env.is_universe(n))
+        throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
+    if (m_local_level_decls.contains(n))
+        throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
+    m_local_level_decls.insert(n, local_level_entry(l, m_local_level_decls.size()));
+}
+
+void parser::add_local_expr(name const & n, expr const & e) {
     m_local_decls.insert(n, local_entry(e, m_local_decls.size()));
 }
 
-void parser::add_local_decl(expr const & e) {
+void parser::add_local(expr const & e) {
     lean_assert(is_local(e));
-    add_local_entry(local_pp_name(e), e);
+    add_local_expr(local_pp_name(e), e);
 }
 
 /** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
@@ -214,6 +234,7 @@ static name g_period(".");
 static name g_colon(":");
 static name g_lparen("(");
 static name g_rparen(")");
+static name g_llevel_curly(".{");
 static name g_lcurly("{");
 static name g_rcurly("}");
 static name g_lbracket("[");
@@ -282,7 +303,9 @@ level parser::parse_level_id() {
         return it->second.first;
     if (m_env.is_universe(id))
         return mk_global_univ(id);
-    throw parser_error(sstream() << "unknown level '" << id << "'", p);
+    if (auto it = get_alias_level(m_env, id))
+        return *it;
+    throw parser_error(sstream() << "unknown universe '" << id << "'", p);
 }
 
 level parser::parse_level_nud() {
@@ -332,9 +355,21 @@ level parser::parse_level(unsigned rbp) {
     return left;
 }
 
-level parser::mk_new_level_param() {
-    // TODO(Leo)
-    return level();
+expr parser::mk_Type() {
+    if (m_type_use_placeholder) {
+        return mk_sort(mk_level_placeholder());
+    } else {
+        unsigned i = 1;
+        name l("l");
+        name r = l.append_after(i);
+        while (m_local_level_decls.contains(r) || m_env.is_universe(r)) {
+            i++;
+            r = l.append_after(i);
+        }
+        level lvl = mk_param_univ(r);
+        add_local_level(r, lvl);
+        return mk_sort(lvl);
+    }
 }
 
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
@@ -394,7 +429,7 @@ void parser::parse_binder_block(buffer<parameter> & r, binder_info const & bi) {
     for (auto p : names) {
         expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
         expr local = mk_local(p.second, p.second, arg_type);
-        add_local_decl(local);
+        add_local(local);
         r.push_back(parameter(p.first, local, bi));
     }
 }
@@ -542,21 +577,41 @@ expr parser::parse_id() {
     // locals
     if (it1 != m_local_decls.end())
         return copy_with_new_pos(it1->second.first, p);
+    buffer<level> lvl_buffer;
+    auto p_lvl = pos();
+    levels ls;
+    if (curr_is_token(g_llevel_curly)) {
+        next();
+        while (!curr_is_token(g_rcurly)) {
+            lvl_buffer.push_back(parse_level());
+        }
+        next();
+        ls = to_list(lvl_buffer.begin(), lvl_buffer.end());
+    }
+    optional<expr> r;
     // globals
     if (m_env.find(id))
-        return save_pos(mk_constant(id), p);
+        r = save_pos(mk_constant(id, ls), p);
     // private globals
-    if (auto prv_id = user_to_hidden_name(m_env, id))
-        return save_pos(mk_constant(*prv_id), p);
+    else if (auto prv_id = user_to_hidden_name(m_env, id))
+        r = save_pos(mk_constant(*prv_id, ls), p);
     // 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;
-        for (auto const & e : as)
+        if (r)
+            new_as.push_back(*r);
+        for (auto const & e : as) {
             new_as.push_back(copy_with_new_pos(e, p));
-        return mk_choice(new_as.size(), new_as.data());
+        }
+        r = mk_choice(new_as.size(), new_as.data());
     }
-    throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
+    if (!r)
+        throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
+    return *r;
 }
 
 expr parser::parse_numeral_expr() {
@@ -621,14 +676,14 @@ expr parser::parse_expr(unsigned rbp) {
 expr parser::parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp) {
     local_decls::mk_scope scope(m_local_decls);
     for (unsigned i = 0; i < num_locals; i++)
-        add_local_decl(locals[i]);
+        add_local(locals[i]);
     return parse_expr(rbp);
 }
 
 expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp) {
     local_decls::mk_scope scope(m_local_decls);
     for (unsigned i = 0; i < num_params; i++)
-        add_local_decl(ps[i].m_local);
+        add_local(ps[i].m_local);
     return parse_expr(rbp);
 }
 
@@ -658,6 +713,8 @@ tactic parser::parse_tactic(unsigned /* rbp */) {
 
 void parser::parse_command() {
     lean_assert(curr() == scanner::token_kind::CommandKeyword);
+    flet<bool> save1(m_type_use_placeholder, m_type_use_placeholder);
+    m_last_cmd_pos = pos();
     name const & cmd_name = get_token_info().value();
     if (auto it = cmds().find(cmd_name)) {
         next();

src/frontends/lean/parser.h

@@ -64,10 +64,10 @@ class parser {
     unsigned                m_next_tag_idx;
     bool                    m_found_errors;
     pos_info_table_ptr      m_pos_table;
-
-    enum class scope_kind { Scope, Namespace, Structure };
-    std::vector<name>       m_namespace_prefixes;
-    std::vector<scope_kind> m_scope_kinds;
+    // If m_type_use_placeholder is true, then the token Type is parsed as Type.{_}.
+    // if it is false, then it is parsed as Type.{l} where l is a fresh parameter,
+    // and is automatically inserted into m_local_level_decls.
+    bool                    m_type_use_placeholder;
 
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
@@ -100,9 +100,6 @@ class parser {
     /** \brief Return true if the current token is a keyword named \c tk or an identifier named \c tk */
     bool curr_is_token_or_id(name const & tk) const;
 
-    void add_local_entry(name const & n, expr const & e);
-    void add_local_decl(expr const & t);
-
     unsigned curr_level_lbp() const;
     level parse_max_imax(bool is_max);
     level parse_level_id();
@@ -140,7 +137,6 @@ public:
     unsigned parse_small_nat();
 
     level parse_level(unsigned rbp = 0);
-    level mk_new_level_param();
 
     parameter parse_binder();
     void parse_binders(buffer<parameter> & r);
@@ -154,6 +150,25 @@ public:
 
     tactic parse_tactic(unsigned rbp = 0);
 
+    void push_local_scope();
+    void pop_local_scope();
+    void add_local_level(name const & n, level const & l);
+    void add_local_expr(name const & n, expr const & e);
+    void add_local(expr const & t);
+    /**
+       \brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
+       it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
+       automalically infer a universe level expression for '_'. When <tt>set_type_use_placeholder(false)</tt>,
+       then it returns <tt>'Type.{l}'</tt>, where \c l is a fresh universe level parameter.
+       The new parameter is automatically added to \c m_local_level_decls.
+
+       \remark When the parse is created the flag is set to false.
+       \remark Before parsing a command, the parser automatically "caches" the current value, and
+       restores it after the command is parsed (or aborted).
+    */
+    void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; }
+    expr mk_Type();
+
     /** \brief Return the current position information */
     pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
     expr save_pos(expr e, pos_info p);

src/library/aliases.cpp

@@ -15,34 +15,78 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/aliases.h"
 #include "library/placeholder.h"
+#include "library/scoped_ext.h"
 
 namespace lean {
+struct aliases_ext;
+static aliases_ext const & get_extension(environment const & env);
+static environment update(environment const & env, aliases_ext const & ext);
+
 struct aliases_ext : public environment_extension {
-    rb_map<name, list<expr>, name_quick_cmp>  m_aliases;
-    rb_map<expr, name,       expr_quick_cmp>  m_inv_aliases;
-    rb_map<name, level,      name_quick_cmp>  m_level_aliases;
-    rb_map<level, name,      level_quick_cmp> m_inv_level_aliases;
+    struct state {
+        rb_map<name, list<expr>, name_quick_cmp>  m_aliases;
+        rb_map<expr, name,       expr_quick_cmp>  m_inv_aliases;
+        rb_map<name, level,      name_quick_cmp>  m_level_aliases;
+        rb_map<level, name,      level_quick_cmp> m_inv_level_aliases;
+    };
+    state       m_state;
+    list<state> m_scopes;
+
     void add_alias(name const & a, expr const & e) {
-        auto it = m_aliases.find(a);
+        auto it = m_state.m_aliases.find(a);
         if (it)
-            m_aliases.insert(a, list<expr>(e, *it));
+            m_state.m_aliases.insert(a, list<expr>(e, *it));
         else
-            m_aliases.insert(a, list<expr>(e));
-        m_inv_aliases.insert(e, a);
+            m_state.m_aliases.insert(a, list<expr>(e));
+        m_state.m_inv_aliases.insert(e, a);
     }
 
     void add_alias(name const & a, level const & l) {
-        auto it = m_level_aliases.find(a);
+        auto it = m_state.m_level_aliases.find(a);
         if (it)
             throw exception(sstream() << "universe level alias '" << a << "' shadows existing alias");
-        m_level_aliases.insert(a, l);
-        m_inv_level_aliases.insert(l, a);
+        m_state.m_level_aliases.insert(a, l);
+        m_state.m_inv_level_aliases.insert(l, a);
+    }
+
+    void push() {
+        m_scopes = list<state>(m_state, m_scopes);
+    }
+
+    void pop() {
+        m_state  = head(m_scopes);
+        m_scopes = tail(m_scopes);
+    }
+
+    static environment using_namespace(environment const & env, io_state const &, name const &) {
+        // do nothing, aliases are treated in a special way in the frontend.
+        return env;
+    }
+
+    static environment push_scope(environment const & env) {
+        aliases_ext ext = get_extension(env);
+        ext.push();
+        environment new_env = update(env, ext);
+        if (!in_section(new_env))
+            new_env = add_aliases(new_env, get_namespace(new_env), name());
+        return new_env;
+    }
+
+    static environment pop_scope(environment const & env) {
+        aliases_ext ext = get_extension(env);
+        ext.pop();
+        return update(env, ext);
     }
 };
 
+static name g_aliases("aliases");
+
 struct aliases_ext_reg {
     unsigned m_ext_id;
-    aliases_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<aliases_ext>()); }
+    aliases_ext_reg() {
+        register_scoped_ext(g_aliases, aliases_ext::using_namespace, aliases_ext::push_scope, aliases_ext::pop_scope);
+        m_ext_id = environment::register_extension(std::make_shared<aliases_ext>());
+    }
 };
 static aliases_ext_reg g_ext;
 static aliases_ext const & get_extension(environment const & env) {
@@ -59,12 +103,12 @@ environment add_alias(environment const & env, name const & a, expr const & e) {
 }
 
 optional<name> is_aliased(environment const & env, expr const & t) {
-    auto it = get_extension(env).m_inv_aliases.find(t);
+    auto it = get_extension(env).m_state.m_inv_aliases.find(t);
     return it ? optional<name>(*it) : optional<name>();
 }
 
 list<expr> get_alias_exprs(environment const & env, name const & n) {
-    auto it = get_extension(env).m_aliases.find(n);
+    auto it = get_extension(env).m_state.m_aliases.find(n);
     return it ? *it : list<expr>();
 }
 
@@ -77,12 +121,12 @@ environment add_alias(environment const & env, name const & a, level const & l)
 }
 
 optional<name> is_aliased(environment const & env, level const & l) {
-    auto it = get_extension(env).m_inv_level_aliases.find(l);
+    auto it = get_extension(env).m_state.m_inv_level_aliases.find(l);
     return it ? optional<name>(*it) : optional<name>();
 }
 
 optional<level> get_alias_level(environment const & env, name const & n) {
-    auto it = get_extension(env).m_level_aliases.find(n);
+    auto it = get_extension(env).m_state.m_level_aliases.find(n);
     return it ? some_level(*it) : optional<level>();
 }
 

tests/lean/t3.lean

@@ -0,0 +1,37 @@
+universe u
+print raw Type.{u}
+namespace tst
+  universe v
+  print raw Type.{v}
+  print raw Type.{tst.v}
+end
+print raw Type.{tst.v}
+print raw Type.{v}  -- Error: alias 'v' is not available anymore
+section
+  universe z        -- Remark: this is a local universe
+  print raw Type.{z}
+end
+print raw Type.{z}  -- Error: local universe 'z' is gone
+section
+  namespace foo -- Error: we cannot create a namespace inside a section
+end
+namespace tst
+  print raw Type.{v} -- Remark: alias 'v' is available again
+  print raw Type.{u}
+  namespace foo
+    universe U
+  end
+end
+print raw Type.{tst.foo.U}
+namespace tst.foo    -- Error: we cannot use qualified names in declarations
+universe full.name.U -- Error: we cannot use qualified names in declarations
+namespace tst
+  namespace foo
+    print raw Type.{v}  -- Remark: alias 'v' for 'tst.v' is available again
+    print raw Type.{U}  -- Remark: alias 'U' for 'tst.foo.U' is available again
+  end
+end
+namespace bla
+  universe u -- Error: we cannot shadow universe levels
+end
+print raw Type.{bla.u} -- Error: we failed to declare bla.u

tests/lean/t3.lean.expected.out

@@ -0,0 +1,17 @@
+Type.{u}
+Type.{tst.v}
+Type.{tst.v}
+Type.{tst.v}
+t3.lean:9:16: error: unknown universe 'v'
+Type.{z}
+t3.lean:14:16: error: unknown universe 'z'
+t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section
+Type.{tst.v}
+Type.{u}
+Type.{tst.foo.U}
+t3.lean:26:0: error: invalid declaration name 'tst.foo', identifier must be atomic
+t3.lean:27:1: error: invalid declaration name 'full.name.U', identifier must be atomic
+Type.{tst.v}
+Type.{tst.foo.U}
+t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level
+t3.lean:37:16: error: unknown universe 'bla.u'