feat(kernel): add global levels to environment

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

src/kernel/environment.cpp

@@ -42,8 +42,8 @@ bool environment_id::is_descendant(environment_id const & id) const {
     return false;
 }
 
-environment::environment(header const & h, environment_id const & ancestor, definitions const & d, extensions const & exts):
+environment::environment(header const & h, environment_id const & ancestor, definitions const & d, name_set const & g, extensions const & exts):
-    m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_extensions(exts) {}
+    m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_global_levels(g), m_extensions(exts) {}
 
 environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative):
     environment(trust_lvl, proof_irrel, eta, impredicative, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
@@ -78,7 +78,18 @@ environment environment::add(certified_definition const & d) const {
     name const & n = d.get_definition().get_name();
     if (find(n))
         throw_already_declared(*this, n);
-    return environment(m_header, m_id, insert(m_definitions, n, d.get_definition()), m_extensions);
+    return environment(m_header, m_id, insert(m_definitions, n, d.get_definition()), m_global_levels, m_extensions);
+}
+
+environment environment::add_global_level(name const & n) const {
+    if (m_global_levels.contains(n))
+        throw_kernel_exception(*this,
+                               "invalid global universe level declaration, environment already contains a universe level with the given name");
+    return environment(m_header, m_id, m_definitions, insert(m_global_levels, n), m_extensions);
+}
+
+bool environment::is_global_level(name const & n) const {
+    return m_global_levels.contains(n);
 }
 
 environment environment::replace(certified_definition const & t) const {
@@ -94,7 +105,7 @@ environment environment::replace(certified_definition const & t) const {
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the new declaration is not a theorem");
     if (ax->get_type() != t.get_definition().get_type())
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same type");
-    return environment(m_header, m_id, insert(m_definitions, n, t.get_definition()), m_extensions);
+    return environment(m_header, m_id, insert(m_definitions, n, t.get_definition()), m_global_levels, m_extensions);
 }
 
 class extension_manager {
@@ -147,6 +158,6 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
     if (id >= new_exts->size())
         new_exts->resize(id+1);
     (*new_exts)[id] = ext;
-    return environment(m_header, m_id, m_definitions, new_exts);
+    return environment(m_header, m_id, m_definitions, m_global_levels, new_exts);
 }
 }

src/kernel/environment.h

@@ -101,9 +101,10 @@ class environment {
     header         m_header;
     environment_id m_id;
     definitions    m_definitions;
+    name_set       m_global_levels;
     extensions     m_extensions;
 
-    environment(header const & h, environment_id const & id, definitions const & d, extensions const & ext);
+    environment(header const & h, environment_id const & id, definitions const & d, name_set const & global_levels, extensions const & ext);
 
 public:
     environment(unsigned trust_lvl = 0, bool proof_irrel = true, bool eta = true, bool impredicative = true);
@@ -137,6 +138,15 @@ public:
     /** \brief Return definition with name \c n. Throws and exception if definition does not exist in this environment. */
     definition get(name const & n) const;
 
+    /**
+        \brief Add a new global universe level with name \c n
+        This method throws an exception if the environment already contains a level named \c n.
+    */
+    environment add_global_level(name const & n) const;
+
+    /** \brief Return true iff the environment has a universe level named \c n. */
+    bool is_global_level(name const & n) const;
+
     /**
        \brief Extends the current environment with the given (certified) definition
        This method throws an exception if:

src/kernel/level.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "util/object_serializer.h"
 #include "util/interrupt.h"
 #include "kernel/level.h"
+#include "kernel/environment.h"
 
 namespace lean {
 level_cell const & to_cell(level const & l) {
@@ -94,7 +95,7 @@ level const & imax_rhs(level const & l) { lean_assert(is_imax(l)); return to_max
 struct level_param_core : public level_cell {
     name m_id;
     level_param_core(level_kind k, name const & id):
-        level_cell(k, hash(id.hash(), is_param ? 11u : 13u)),
+        level_cell(k, hash(id.hash(), static_cast<unsigned>(k))),
         m_id(id) {
         lean_assert(k == level_kind::Meta || k == level_kind::Param || k == level_kind::Global);
     }
@@ -427,28 +428,56 @@ bool has_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](l
 bool has_meta(level_cnstr const & c) { return has_meta(c.first) || has_meta(c.second); }
 bool has_meta(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_meta(c); }); }
 
-static optional<name> get_undef_param(level const & l, param_names const & ps) {
+void for_each_level_fn::apply(level const & l) {
-    if (!has_param(l))
+    if (!m_f(l))
-        return optional<name>();
+        return;
+    switch (l.kind()) {
+    case level_kind::Succ:                          apply(succ_of(l)); break;
+    case level_kind::Max: case level_kind::IMax:    apply(to_max_core(l).m_lhs); apply(to_max_core(l).m_rhs); break;
+    case level_kind::Zero: case level_kind::Param:
+    case level_kind::Meta: case level_kind::Global: break;
+    }
+}
+
+level replace_level_fn::apply(level const & l) {
+    optional<level> r = m_f(l);
+    if (r)
+        return *r;
     switch (l.kind()) {
     case level_kind::Succ:
-        return get_undef_param(succ_of(l), ps);
+        return update_succ(l, apply(succ_of(l)));
     case level_kind::Max: case level_kind::IMax:
-        if (auto it = get_undef_param(to_max_core(l).m_lhs, ps))
+        return update_max(l, apply(to_max_core(l).m_lhs), apply(to_max_core(l).m_rhs));
-            return it;
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta: case level_kind::Global:
-        else
+        return l;
-            return get_undef_param(to_max_core(l).m_rhs, ps);
-    case level_kind::Param:
-        if (std::find(ps.begin(), ps.end(), param_id(l)) == ps.end())
-            return optional<name>(param_id(l));
-        else
-            return optional<name>();
-    case level_kind::Zero: case level_kind::Meta: case level_kind::Global:
-        lean_unreachable(); // LCOV_EXCL_LINE
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+optional<name> get_undef_param(level const & l, param_names const & ps) {
+    optional<name> r;
+    for_each(l, [&](level const & l) {
+            if (!has_param(l))
+                return false;
+            if (l.kind() == level_kind::Param && std::find(ps.begin(), ps.end(), param_id(l)) != ps.end())
+                r = param_id(l);
+            return true;
+        });
+    return r;
+}
+
+optional<name> get_undef_global(level const & l, environment const & env) {
+    optional<name> r;
+    for_each(l, [&](level const & l) {
+            if (!has_global(l))
+                return false;
+            if (l.kind() == level_kind::Global && env.is_global_level(global_id(l)))
+                r = global_id(l);
+            return true;
+        });
+    return r;
+}
+
 optional<name> get_undef_param(level_cnstrs const & cs, param_names const & ps) {
     for (auto const & c : cs) {
         if (auto it = get_undef_param(c.first, ps))
@@ -459,6 +488,16 @@ optional<name> get_undef_param(level_cnstrs const & cs, param_names const & ps)
     return optional<name>();
 }
 
+optional<name> get_undef_global(level_cnstrs const & cs, environment const & env) {
+    for (auto const & c : cs) {
+        if (auto it = get_undef_global(c.first, env))
+            return it;
+        if (auto it = get_undef_global(c.second, env))
+            return it;
+    }
+    return optional<name>();
+}
+
 level update_succ(level const & l, level const & new_arg) {
     if (is_eqp(succ_of(l), new_arg))
         return l;
@@ -475,21 +514,6 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs)
         return mk_imax(new_lhs, new_rhs);
 }
 
-level replace_level_fn::apply(level const & l) {
-    optional<level> r = m_f(l);
-    if (r)
-        return *r;
-    switch (l.kind()) {
-    case level_kind::Succ:
-        return update_succ(l, apply(succ_of(l)));
-    case level_kind::Max: case level_kind::IMax:
-        return update_max(l, apply(to_max_core(l).m_lhs), apply(to_max_core(l).m_rhs));
-    case level_kind::Zero: case level_kind::Param: case level_kind::Meta: case level_kind::Global:
-        return l;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
 level instantiate(level const & l, param_names const & ps, levels const & ls) {
     lean_assert(length(ps) == length(ls));
     return replace(l, [=](level const & l) {

src/kernel/level.h

@@ -124,7 +124,6 @@ bool has_global(level const & l);
 /** \brief Return true iff \c l contains parameters */
 bool has_param(level const & l);
 
-
 /**
    \brief Return a new level expression based on <tt>l == succ(arg)</tt>, where \c arg is replaced with
    \c new_arg.
@@ -169,17 +168,17 @@ bool has_global(level_cnstrs const & cs);
 bool has_meta(level_cnstr const & c);
 bool has_meta(level_cnstrs const & cs);
 
-typedef list<name> param_names;
+/** \brief Functional for applying <tt>F</tt> to each level expressions. */
+class for_each_level_fn {
+    std::function<bool(level const &)>  m_f; // NOLINT
+    void apply(level const & l);
+public:
+    template<typename F> for_each_level_fn(F const & f):m_f(f) {}
+    void operator()(level const & l) { return apply(l); }
+};
+template<typename F> void for_each(level const & l, F const & f) { return for_each_level_fn(f)(l); }
 
-/**
+/** \brief Functional for applying <tt>F</tt> to the level expressions. */
-   \brief If \c cs contains a parameter that is not in \c param_names, then return it.
-   Otherwise, return none.
-*/
-optional<name> get_undef_param(level_cnstrs const & cs, param_names const & ps);
-
-/**
-   \brief Functional for applying <tt>F</tt> to the level expressions.
-*/
 class replace_level_fn {
     std::function<optional<level>(level const &)>  m_f;
     level apply(level const & l);
@@ -187,10 +186,21 @@ public:
     template<typename F> replace_level_fn(F const & f):m_f(f) {}
     level operator()(level const & l) { return apply(l); }
 };
+template<typename F> level replace(level const & l, F const & f) { return replace_level_fn(f)(l); }
 
-template<typename F> level replace(level const & l, F const & f) {
+typedef list<name> param_names;
-    return replace_level_fn(f)(l);
+
-}
+/** \brief If \c l contains a global that is not in \c env, then return it. Otherwise, return none. */
+optional<name> get_undef_global(level const & l, environment const & env);
+
+/** \brief If \c l contains a parameter that is not in \c ps, then return it. Otherwise, return none. */
+optional<name> get_undef_param(level const & l, param_names const & ps);
+
+/** \brief If \c cs contains a global that is not in \c env, then return it. Otherwise, return none. */
+optional<name> get_undef_global(level_cnstrs const & cs, environment const & env);
+
+/** \brief If \c cs contains a parameter that is not in \c ps, then return it. Otherwise, return none. */
+optional<name> get_undef_param(level_cnstrs const & cs, param_names const & ps);
 
 /**
     \brief Instantiate the universe level parameters \c ps occurring in \c l with the levels \c ls.

src/kernel/type_checker.cpp

@@ -75,6 +75,7 @@ struct type_checker::imp {
     bool                       m_memoize;
     // temp flag
     bool                       m_cnstrs_enabled;
+    param_names                m_params;
 
     imp(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr<converter> && conv, bool memoize):
         m_env(env), m_gen(g), m_chandler(h), m_conv(std::move(conv)), m_conv_ctx(*this), m_tc_ctx(*this),
@@ -426,7 +427,10 @@ struct type_checker::imp {
     }
 
     expr infer_type(expr const & e) { return infer_type_core(e, true); }
-    expr check(expr const & e) { return infer_type_core(e, false); }
+    expr check(expr const & e, param_names const & ps) {
+        flet<param_names> updt(m_params, ps);
+        return infer_type_core(e, false);
+    }
     bool is_conv(expr const & t, expr const & s) { return m_conv->is_conv(t, s, m_conv_ctx); }
     bool is_def_eq(expr const & t, expr const & s) { return m_conv->is_def_eq(t, s, m_conv_ctx); }
     expr whnf(expr const & t) { return m_conv->whnf(t, m_conv_ctx); }
@@ -442,7 +446,7 @@ type_checker::type_checker(environment const & env, name_generator const & g, st
 
 type_checker::~type_checker() {}
 expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); }
-expr type_checker::check(expr const & t) { return m_ptr->check(t); }
+expr type_checker::check(expr const & t, param_names const & ps) { return m_ptr->check(t, ps); }
 bool type_checker::is_conv(expr const & t, expr const & s) { return m_ptr->is_conv(t, s); }
 bool type_checker::is_def_eq(expr const & t, expr const & s) { return m_ptr->is_def_eq(t, s); }
 bool type_checker::is_prop(expr const & t) { return m_ptr->is_prop(t); }

src/kernel/type_checker.h

@@ -84,7 +84,7 @@ public:
        The result is meaningful only if the constraints sent to the
        constraint handler can be solved.
     */
-    expr check(expr const & t);
+    expr check(expr const & t, param_names const & ps = param_names());
     /** \brief Return true iff t is convertible to s. */
     bool is_conv(expr const & t, expr const & s);
     /** \brief Return true iff t is definitionally equal to s. */