diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 06c7c4c03..4ca0c3084 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -21,8 +21,8 @@ public: } }; -environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr ext): - m_trust_lvl(trust_lvl), m_proof_irrel(proof_irrel), m_eta(eta), m_norm_ext(std::move(ext)) {} +environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr ext): + m_trust_lvl(trust_lvl), m_proof_irrel(proof_irrel), m_eta(eta), m_impredicative(impredicative), m_norm_ext(std::move(ext)) {} environment_extension::~environment_extension() {} @@ -45,12 +45,12 @@ bool environment_id::is_descendant(environment_id const & id) const { 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(unsigned trust_lvl, bool proof_irrel, bool eta): - environment(trust_lvl, proof_irrel, eta, std::unique_ptr(new noop_normalizer_extension())) +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())) {} -environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr ext): - m_header(std::make_shared(trust_lvl, proof_irrel, eta, std::move(ext))), +environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr ext): + m_header(std::make_shared(trust_lvl, proof_irrel, eta, impredicative, std::move(ext))), m_extensions(std::make_shared()) {} diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 0a83e3229..600477bd8 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -46,13 +46,15 @@ class environment_header { unsigned m_trust_lvl; //!the given one. bool m_proof_irrel; //!< true if the kernel assumes proof irrelevance bool m_eta; //!< true if the kernel uses eta-reduction in convertability checks + bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool. std::unique_ptr m_norm_ext; void dealloc(); public: - environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr ext); + environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr ext); unsigned trust_lvl() const { return m_trust_lvl; } bool proof_irrel() const { return m_proof_irrel; } bool eta() const { return m_eta; } + bool impredicative() const { return m_impredicative; } normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); } }; @@ -104,8 +106,8 @@ class environment { environment(header const & h, environment_id const & id, definitions const & d, extensions const & ext); public: - environment(unsigned trust_lvl = 0, bool proof_irrel = true, bool eta = true); - environment(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr ext); + environment(unsigned trust_lvl = 0, bool proof_irrel = true, bool eta = true, bool impredicative = true); + environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr ext); ~environment(); /** \brief Return the environment unique identifier. */ @@ -123,6 +125,9 @@ public: /** \brief Return true iff the environment assumes Eta-reduction */ bool eta() const { return m_header->eta(); } + /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop/Bool */ + bool impredicative() const { return m_header->impredicative(); } + /** \brief Return reference to the normalizer extension associatied with this environment. */ normalizer_extension const & norm_ext() const { return m_header->norm_ext(); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index d5ef932da..27a64f099 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -382,7 +382,10 @@ struct type_checker::imp { expr t1 = ensure_sort(infer_type_core(binder_domain(e), infer_only), binder_domain(e)); auto b = open_binder_body(e); expr t2 = ensure_sort(infer_type_core(b.first, infer_only), binder_body(e)); - r = mk_sort(mk_imax(sort_level(t1), sort_level(t2))); + if (m_env.impredicative()) + r = mk_sort(mk_imax(sort_level(t1), sort_level(t2))); + else + r = mk_sort(mk_max(sort_level(t1), sort_level(t2))); break; } case expr_kind::App: { diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index d5f7de37f..28bee5176 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -851,6 +851,7 @@ static int environment_is_descendant(lua_State * L) { return push_boolean(L, to_ static int environment_trust_lvl(lua_State * L) { return push_integer(L, to_environment(L, 1).trust_lvl()); } static int environment_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).proof_irrel()); } static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); } +static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); } static int environment_find(lua_State * L) { return push_optional_definition(L, to_environment(L, 1).find(to_name_ext(L, 2))); } static int environment_get(lua_State * L) { return push_definition(L, to_environment(L, 1).get(to_name_ext(L, 2))); } static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); } @@ -865,6 +866,7 @@ static const struct luaL_Reg environment_m[] = { {"trust_lvl", safe_function}, {"proof_irrel", safe_function}, {"eta", safe_function}, + {"impredicative", safe_function}, {"find", safe_function}, {"get", safe_function}, {"add", safe_function}, diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 3f6bc98ed..f2e925642 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -125,7 +125,7 @@ public: }; static void tst3() { - environment env(0, true, true, std::unique_ptr(new normalizer_extension_tst())); + environment env(0, true, true, true, std::unique_ptr(new normalizer_extension_tst())); expr A = Const("A"); expr x = Const("x"); expr id = Const("id");