feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel

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

src/kernel/environment.cpp

@@ -21,8 +21,8 @@ public:
     }
 };
 
-environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension const> ext):
+environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension const> ext):
-    m_trust_lvl(trust_lvl), m_proof_irrel(proof_irrel), m_eta(eta), m_norm_ext(std::move(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::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative):
-    environment(trust_lvl, proof_irrel, eta, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
+    environment(trust_lvl, proof_irrel, eta, impredicative, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
 {}
 
-environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension> ext):
+environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension> ext):
-    m_header(std::make_shared<environment_header>(trust_lvl, proof_irrel, eta, std::move(ext))),
+    m_header(std::make_shared<environment_header>(trust_lvl, proof_irrel, eta, impredicative, std::move(ext))),
     m_extensions(std::make_shared<environment_extensions const>())
 {}
 

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<normalizer_extension const> m_norm_ext;
     void dealloc();
 public:
-    environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension const> ext);
+    environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension const> 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 = 0, bool proof_irrel = true, bool eta = true, bool impredicative = true);
-    environment(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension> ext);
+    environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension> 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(); }
 

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: {

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<environment_trust_lvl>},
     {"proof_irrel",    safe_function<environment_proof_irrel>},
     {"eta",            safe_function<environment_eta>},
+    {"impredicative",  safe_function<environment_impredicative>},
     {"find",           safe_function<environment_find>},
     {"get",            safe_function<environment_get>},
     {"add",            safe_function<environment_add>},

src/tests/kernel/environment.cpp

@@ -125,7 +125,7 @@ public:
 };
 
 static void tst3() {
-    environment env(0, true, true, std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
+    environment env(0, true, true, true, std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
     expr A = Const("A");
     expr x = Const("x");
     expr id = Const("id");