diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 457dd337c..bc7b4b43d 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -607,20 +607,6 @@ struct default_converter : public converter { } } - list const & cls_proof_irrel = m_env.cls_proof_irrel(); - if (!is_nil(cls_proof_irrel)) { - // Proof irrelevance support for classes - auto tcs = infer_type(c, t); - auto wcs = whnf(tcs.first, c); - expr t_type = wcs.first; - if (std::any_of(cls_proof_irrel.begin(), cls_proof_irrel.end(), [&](name const & cls_name) { return is_app_of(t_type, cls_name); })) { - auto ccs = infer_type(c, s); - auto cs_prime = tcs.second + wcs.second + ccs.second; - if (is_def_eq(t_type, ccs.first, c, jst, cs_prime)) - return to_bcs(true, cs_prime); - } - } - if (may_reduce_later(t_n, c) || may_reduce_later(s_n, c) || delay_check) { cs = cs + constraint_seq(mk_eq_cnstr(t_n, s_n, jst.get())); return to_bcs(true, cs); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 92a4ee308..1b54a59e7 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -13,9 +13,9 @@ Author: Leonardo de Moura namespace lean { environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, - list const & cls_proof_irrel, std::unique_ptr ext): + std::unique_ptr ext): m_trust_lvl(trust_lvl), m_prop_proof_irrel(prop_proof_irrel), m_eta(eta), m_impredicative(impredicative), - m_cls_proof_irrel(cls_proof_irrel), m_norm_ext(std::move(ext)) {} + m_norm_ext(std::move(ext)) {} environment_extension::~environment_extension() {} @@ -73,13 +73,13 @@ bool environment_id::is_descendant(environment_id const & id) const { environment::environment(header const & h, environment_id const & ancestor, declarations const & d, name_set const & g, extensions const & exts): m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {} -environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list const & cls_proof_irrel): - environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, mk_id_normalizer_extension()) +environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative): + environment(trust_lvl, prop_proof_irrel, eta, impredicative, mk_id_normalizer_extension()) {} -environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list const & cls_proof_irrel, +environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, std::unique_ptr ext): - m_header(std::make_shared(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::move(ext))), + m_header(std::make_shared(trust_lvl, prop_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 9a86b4517..71055ba01 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -45,17 +45,15 @@ class environment_header { bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Prop (aka Type.{0}) 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. - list m_cls_proof_irrel; //!< list of proof irrelevant classes, if we want Id types to be proof irrelevant, we the name 'Id' in this list. std::unique_ptr m_norm_ext; void dealloc(); public: environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, - list const & cls_proof_irrel, std::unique_ptr ext); + std::unique_ptr ext); unsigned trust_lvl() const { return m_trust_lvl; } bool prop_proof_irrel() const { return m_prop_proof_irrel; } bool eta() const { return m_eta; } bool impredicative() const { return m_impredicative; } - list const & cls_proof_irrel() const { return m_cls_proof_irrel; } normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); } }; @@ -115,9 +113,8 @@ class environment { environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext); public: - environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true, - list const & cls_proof_irrel = list()); - environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list const & cls_proof_irrel, + environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true); + environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, std::unique_ptr ext); ~environment(); @@ -133,9 +130,6 @@ public: /** \brief Return true iff the environment assumes proof irrelevance for Type.{0} (i.e., Prop) */ bool prop_proof_irrel() const { return m_header->prop_proof_irrel(); } - /** \brief Return the list of classes marked as proof irrelevant */ - list const & cls_proof_irrel() const { return m_header->cls_proof_irrel(); } - /** \brief Return true iff the environment assumes Eta-reduction */ bool eta() const { return m_header->eta(); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 094751466..4b1fcf36c 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1010,7 +1010,6 @@ DECL_UDATA(environment) static int environment_is_descendant(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_descendant(to_environment(L, 2))); } static int environment_trust_lvl(lua_State * L) { return push_integer(L, to_environment(L, 1).trust_lvl()); } static int environment_prop_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).prop_proof_irrel()); } -static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, to_environment(L, 1).cls_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_add_universe(lua_State * L) { @@ -1032,8 +1031,7 @@ static int mk_bare_environment(lua_State * L) { bool prop_proof_irrel = get_bool_named_param(L, 1, "prop_proof_irrel", true); bool eta = get_bool_named_param(L, 1, "eta", true); bool impredicative = get_bool_named_param(L, 1, "impredicative", true); - list const & cls_proof_irrel = get_list_name_named_param(L, 1, "cls_proof_irrel", list()); - return push_environment(L, environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel)); + return push_environment(L, environment(trust_lvl, prop_proof_irrel, eta, impredicative)); } static unsigned get_trust_lvl(lua_State * L, int i) { unsigned trust_lvl = 0; @@ -1120,7 +1118,6 @@ static const struct luaL_Reg environment_m[] = { {"trust_lvl", safe_function}, {"trust_level", safe_function}, {"prop_proof_irrel", safe_function}, - {"cls_proof_irrel", safe_function}, {"eta", safe_function}, {"impredicative", safe_function}, {"add_universe", safe_function}, diff --git a/src/library/standard_kernel.cpp b/src/library/standard_kernel.cpp index 760ee9512..da4d1fdae 100644 --- a/src/library/standard_kernel.cpp +++ b/src/library/standard_kernel.cpp @@ -18,7 +18,6 @@ environment mk_environment(unsigned trust_lvl) { true /* Type.{0} is proof irrelevant */, true /* Eta */, true /* Type.{0} is impredicative */, - list() /* No type class has proof irrelevance */, /* builtin support for inductive and record datatypes */ compose(std::unique_ptr(new inductive_normalizer_extension()), std::unique_ptr(new record_normalizer_extension()))); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index c06a054f0..9e4f13870 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -131,7 +131,7 @@ public: }; static void tst3() { - environment env(0, true, true, true, list(), std::unique_ptr(new normalizer_extension_tst())); + environment env(0, true, true, true, std::unique_ptr(new normalizer_extension_tst())); expr A = Local("A", Type); expr x = Local("x", A); expr id = Const("id"); diff --git a/tests/lua/hott1.lua b/tests/lua/hott1.lua deleted file mode 100644 index 825b43aef..000000000 --- a/tests/lua/hott1.lua +++ /dev/null @@ -1,43 +0,0 @@ --- Create a HoTT compatible environment. --- That is, --- Type.{0} is predicative --- No proof irrelevance for Type.{0} --- Proof irrelevance for Id types -local env = bare_environment({prop_proof_irrel=false, impredicative=false, cls_proof_irrel={"Id"}}) -assert(not env:prop_proof_irrel()) -assert(not env:impredicative()) -assert(env:cls_proof_irrel():head() == name("Id")) -assert(env:cls_proof_irrel():tail():is_nil()) -local l = mk_param_univ("l") -local U_l = mk_sort(l) -local A = Local("A", U_l) -env = add_decl(env, mk_var_decl("Id", {l}, Pi(A, mk_arrow(A, A, U_l)))) -local Set = mk_sort(mk_level_zero()) -env = add_decl(env, mk_var_decl("N", Set)) -local N = Const("N") -env = add_decl(env, mk_var_decl("a", N)) -env = add_decl(env, mk_var_decl("b", N)) -local a = Const("a") -local b = Const("b") -local Id_z = Const("Id", {mk_level_zero()}) -env = add_decl(env, mk_axiom("H1", Id_z(N, a, b))) -env = add_decl(env, mk_axiom("H2", Id_z(N, a, b))) -local tc = type_checker(env) --- H1 and H2 are definitionally equal since both have type Id.{0} N a b --- and Id is in env:cls_proof_irrel() -assert(tc:is_def_eq(Const("H1"), Const("H2"))) -env = add_decl(env, mk_var_decl("Path", {l}, Pi(A, mk_arrow(A, A, U_l)))) -local Path_z = Const("Path", {mk_level_zero()}) -env = add_decl(env, mk_axiom("H3", Path_z(N, a, b))) -env = add_decl(env, mk_axiom("H4", Path_z(N, a, b))) -local tc = type_checker(env) -assert(tc:is_def_eq(Const("H1"), Const("H2"))) -assert(not tc:is_def_eq(Const("H3"), Const("H4"))) -assert(tc:is_def_eq(tc:check(Const("H3")), tc:check(Const("H4")))) -print("H1 : " .. tostring(tc:check(Const("H1")))) -print("H2 : " .. tostring(tc:check(Const("H2")))) -print("H3 : " .. tostring(tc:check(Const("H3")))) -print("H4 : " .. tostring(tc:check(Const("H4")))) -print("N : " .. tostring(get_formatter_factory()(env)(tc:check(Const("N"))))) --- N : Type.{0} -assert(not tc:is_def_eq(Const("a"), Const("b")))