From 9c760132e25455e5d108959a320c88fa401d444c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 May 2014 16:07:31 -0700 Subject: [PATCH] feat(kernel): add global levels to environment Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 21 ++++++--- src/kernel/environment.h | 12 +++++- src/kernel/level.cpp | 86 ++++++++++++++++++++++++------------- src/kernel/level.h | 38 ++++++++++------ src/kernel/type_checker.cpp | 8 +++- src/kernel/type_checker.h | 2 +- 6 files changed, 113 insertions(+), 54 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 4ca0c3084..ab27c5316 100644 --- a/src/kernel/environment.cpp +++ b/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): - m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_extensions(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_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(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= 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); } } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 600477bd8..8235095a9 100644 --- a/src/kernel/environment.h +++ b/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: diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 370d1e44e..df70464ef 100644 --- a/src/kernel/level.cpp +++ b/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(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 get_undef_param(level const & l, param_names const & ps) { - if (!has_param(l)) - return optional(); +void for_each_level_fn::apply(level const & l) { + if (!m_f(l)) + 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 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 it; - else - 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(param_id(l)); - else - return optional(); - case level_kind::Zero: case level_kind::Meta: case level_kind::Global: - lean_unreachable(); // LCOV_EXCL_LINE + 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 } +optional get_undef_param(level const & l, param_names const & ps) { + optional 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 get_undef_global(level const & l, environment const & env) { + optional 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 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 get_undef_param(level_cnstrs const & cs, param_names const & ps) return optional(); } +optional 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(); +} + 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 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) { diff --git a/src/kernel/level.h b/src/kernel/level.h index e2f7e9b83..d31da8a00 100644 --- a/src/kernel/level.h +++ b/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 l == succ(arg), 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 param_names; +/** \brief Functional for applying F to each level expressions. */ +class for_each_level_fn { + std::function m_f; // NOLINT + void apply(level const & l); +public: + template for_each_level_fn(F const & f):m_f(f) {} + void operator()(level const & l) { return apply(l); } +}; +template void for_each(level const & l, F const & f) { return for_each_level_fn(f)(l); } -/** - \brief If \c cs contains a parameter that is not in \c param_names, then return it. - Otherwise, return none. -*/ -optional get_undef_param(level_cnstrs const & cs, param_names const & ps); - -/** - \brief Functional for applying F to the level expressions. -*/ +/** \brief Functional for applying F to the level expressions. */ class replace_level_fn { std::function(level const &)> m_f; level apply(level const & l); @@ -187,10 +186,21 @@ public: template replace_level_fn(F const & f):m_f(f) {} level operator()(level const & l) { return apply(l); } }; +template level replace(level const & l, F const & f) { return replace_level_fn(f)(l); } -template level replace(level const & l, F const & f) { - return replace_level_fn(f)(l); -} +typedef list param_names; + +/** \brief If \c l contains a global that is not in \c env, then return it. Otherwise, return none. */ +optional 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 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 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 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. diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 27a64f099..4c7cd3440 100644 --- a/src/kernel/type_checker.cpp +++ b/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 && 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 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); } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 499a4db10..1f0adcb85 100644 --- a/src/kernel/type_checker.h +++ b/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. */