From cf7e60e5a68f796c96e085663a1330f857dd8236 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 May 2015 15:42:42 -0700 Subject: [PATCH] refactor(kernel): remove "opaque" field from kernel declarations see issue #576 --- src/frontends/lean/builtin_cmds.cpp | 3 +-- src/frontends/lean/decl_cmds.cpp | 10 ++++------ src/frontends/lean/migrate_cmd.cpp | 3 +-- src/frontends/lean/structure_cmd.cpp | 9 ++------- src/kernel/declaration.cpp | 20 +++++++++----------- src/kernel/declaration.h | 9 ++++----- src/kernel/default_converter.cpp | 3 +-- src/library/definitional/brec_on.cpp | 6 ++---- src/library/definitional/cases_on.cpp | 3 +-- src/library/definitional/induction_on.cpp | 5 ++--- src/library/definitional/no_confusion.cpp | 6 ++---- src/library/definitional/projection.cpp | 3 +-- src/library/definitional/rec_on.cpp | 4 +--- src/library/kernel_bindings.cpp | 23 ++++++++++------------- src/library/kernel_serializer.cpp | 13 +++++-------- src/library/module.cpp | 1 - src/library/normalize.cpp | 4 ++-- src/library/reducible.cpp | 2 -- src/library/unfold_macros.cpp | 2 +- src/library/update_declaration.cpp | 2 +- src/library/util.cpp | 14 ++------------ src/library/util.h | 5 ----- tests/lean/run/reducible.lean | 4 +--- tests/lua/def1.lua | 12 ++++-------- 24 files changed, 57 insertions(+), 109 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 52d8938f3..625ccd7b3 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -626,12 +626,11 @@ static environment add_abbrev(parser & p, environment const & env, name const & for (name const & l : decl.get_univ_params()) ls.push_back(mk_param_univ(l)); expr value = mk_constant(d, to_list(ls.begin(), ls.end())); - bool opaque = false; name const & ns = get_namespace(env); name full_id = ns + id; p.add_abbrev_index(full_id, d); environment new_env = - module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque))); + module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value))); if (full_id != id) new_env = add_expr_alias_rec(new_env, id, full_id); return new_env; diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 72aa27eef..6ea141570 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -1064,7 +1064,7 @@ class definition_cmd_fn { cd = check(mk_axiom(m_real_name, c_ls, c_type)); } } else { - cd = check(mk_definition(m_env, m_real_name, c_ls, c_type, c_value, m_is_opaque)); + cd = check(mk_definition(m_env, m_real_name, c_ls, c_type, c_value)); } if (!m_is_private) m_p.add_decl_index(m_real_name, m_pos, m_p.get_cmd_token(), c_type); @@ -1176,11 +1176,10 @@ class definition_cmd_fn { aux_values[i] = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, aux_values[i])); } if (is_definition()) { - m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, - m_type, m_value, m_is_opaque))); + m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, m_value))); for (unsigned i = 0; i < aux_values.size(); i++) m_env = module::add(m_env, check(mk_definition(m_env, m_real_aux_names[i], new_ls, - m_aux_types[i], aux_values[i], m_is_opaque))); + m_aux_types[i], aux_values[i]))); } else { m_env = module::add(m_env, check(mk_theorem(m_real_name, new_ls, m_type, m_value))); for (unsigned i = 0; i < aux_values.size(); i++) @@ -1232,8 +1231,7 @@ class definition_cmd_fn { new_ls = append(m_ls, new_ls); m_type = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type)); m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value)); - m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, - m_type, m_value, m_is_opaque))); + m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, m_value))); m_p.cache_definition(m_real_name, pre_type, pre_value, new_ls, m_type, m_value); } } diff --git a/src/frontends/lean/migrate_cmd.cpp b/src/frontends/lean/migrate_cmd.cpp index 661b1d50f..3a25b5be8 100644 --- a/src/frontends/lean/migrate_cmd.cpp +++ b/src/frontends/lean/migrate_cmd.cpp @@ -229,8 +229,7 @@ struct migrate_cmd_fn { else if (d.is_theorem()) m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value))); else - m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls, - new_type, new_value, d.is_opaque()))); + m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls, new_type, new_value))); m_p.add_decl_index(full_name, m_pos, d.is_theorem() ? name("theorem") : name("definition"), new_type); if (short_name != full_name) m_env = add_expr_alias_rec(m_env, short_name, full_name); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 1c679825c..29965dc1c 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -718,12 +718,10 @@ struct structure_cmd_fn { } void add_rec_on_alias(name const & n) { - bool opaque = false; name rec_on_name(m_name, "rec_on"); declaration rec_on_decl = m_env.get(rec_on_name); declaration new_decl = mk_definition(m_env, n, rec_on_decl.get_univ_params(), - rec_on_decl.get_type(), rec_on_decl.get_value(), - opaque); + rec_on_decl.get_type(), rec_on_decl.get_value()); m_env = module::add(m_env, check(m_env, new_decl)); m_env = set_reducible(m_env, n, reducible_status::Reducible); if (optional idx = has_unfold_c_hint(m_env, rec_on_name)) @@ -817,10 +815,7 @@ struct structure_cmd_fn { } coercion_value = Fun(m_params, Fun(st, coercion_value)); name coercion_name = coercion_names[i]; - - bool opaque = false; - declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value, - opaque); + declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value); m_env = module::add(m_env, check(m_env, coercion_decl)); m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible); save_def_info(coercion_name); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index ff21d69ea..68548dbb9 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -18,7 +18,6 @@ struct declaration::cell { optional m_value; // if none, then declaration is actually a postulate // The following fields are only meaningful for definitions (which are not theorems) unsigned m_weight; - bool m_opaque; // The following field affects the convertability checker. // Let f be this definition, then if the following field is true, // then whenever we are checking whether @@ -30,11 +29,11 @@ struct declaration::cell { cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom): m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom), - m_weight(0), m_opaque(true), m_use_conv_opt(false) {} + m_weight(0), m_use_conv_opt(false) {} cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v, - bool opaque, unsigned w, bool use_conv_opt): + unsigned w, bool use_conv_opt): m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm), - m_value(v), m_weight(w), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {} + m_value(v), m_weight(w), m_use_conv_opt(use_conv_opt) {} }; static declaration * g_dummy = nullptr; @@ -58,17 +57,16 @@ level_param_names const & declaration::get_univ_params() const { return m_ptr->m unsigned declaration::get_num_univ_params() const { return length(get_univ_params()); } expr const & declaration::get_type() const { return m_ptr->m_type; } -bool declaration::is_opaque() const { return m_ptr->m_opaque; } expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); } unsigned declaration::get_weight() const { return m_ptr->m_weight; } bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; } declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, - bool opaque, unsigned weight, bool use_conv_opt) { - return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, use_conv_opt)); + unsigned weight, bool use_conv_opt) { + return declaration(new declaration::cell(n, params, t, false, v, weight, use_conv_opt)); } -declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, - bool opaque, bool use_conv_opt) { +declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, + expr const & v, bool use_conv_opt) { unsigned w = 0; for_each(v, [&](expr const & e, unsigned) { if (is_constant(e)) { @@ -78,10 +76,10 @@ declaration mk_definition(environment const & env, name const & n, level_param_n } return true; }); - return mk_definition(n, params, t, v, opaque, w+1, use_conv_opt); + return mk_definition(n, params, t, v, w+1, use_conv_opt); } declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) { - return declaration(new declaration::cell(n, params, t, true, v, true, 0, false)); + return declaration(new declaration::cell(n, params, t, true, v, 0, false)); } declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { return declaration(new declaration::cell(n, params, t, true)); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index b1c8de13a..2f1e86c13 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -50,13 +50,12 @@ public: expr const & get_type() const; expr const & get_value() const; - bool is_opaque() const; unsigned get_weight() const; bool use_conv_opt() const; friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, - expr const & v, bool opaque, bool use_conv_opt); - friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque, + expr const & v, bool use_conv_opt); + friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned weight, bool use_conv_opt); friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); @@ -68,9 +67,9 @@ inline optional some_declaration(declaration const & o) { return op inline optional some_declaration(declaration && o) { return optional(std::forward(o)); } declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, - bool opaque = false, unsigned weight = 0, bool use_conv_opt = true); + unsigned weight = 0, bool use_conv_opt = true); declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, - bool opaque = false, bool use_conv_opt = true); + bool use_conv_opt = true); declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t); diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 3d66840a7..24f84ade7 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -111,8 +111,7 @@ expr default_converter::whnf_core(expr const & e) { bool default_converter::is_opaque(declaration const & d) const { lean_assert(d.is_definition()); if (d.is_theorem()) return true; // theorems are always opaque - if (!d.is_opaque()) return false; // d is a transparent definition - return true; // d is opaque + return false; } /** \brief Expand \c e if it is non-opaque constant with weight >= w */ diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 153ff1ed4..ab3b5de4e 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -141,10 +141,9 @@ static environment mk_below(environment const & env, name const & n, bool ibelow expr below_type = Pi(args, Type_result); expr below_value = Fun(args, rec); - bool opaque = false; bool use_conv_opt = true; declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value, - opaque, use_conv_opt); + use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, below_name, reducible_status::Reducible); if (!ibelow) @@ -328,10 +327,9 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) expr brec_on_type = Pi(args, result_type); expr brec_on_value = Fun(args, mk_pr1(tc, rec, ind)); - bool opaque = false; bool use_conv_opt = true; declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value, - opaque, use_conv_opt); + use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible); if (!ind) diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index 3f353bcac..724a987f2 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -177,10 +177,9 @@ environment mk_cases_on(environment const & env, name const & n) { expr cases_on_type = Pi(cases_on_params, rec_type); expr cases_on_value = Fun(cases_on_params, mk_app(rec_cnst, rec_args)); - bool opaque = false; bool use_conv_opt = true; declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value, - opaque, use_conv_opt); + use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible); new_env = add_unfold_c_hint(new_env, cases_on_name, cases_on_major_idx); diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp index 33a8ee26c..6a8ce3071 100644 --- a/src/library/definitional/induction_on.cpp +++ b/src/library/definitional/induction_on.cpp @@ -24,7 +24,6 @@ environment mk_induction_on(environment const & env, name const & n) { declaration ind_decl = env.get(n); unsigned rec_on_num_univs = rec_on_decl.get_num_univ_params(); unsigned ind_num_univs = ind_decl.get_num_univ_params(); - bool opaque = false; bool use_conv_opt = true; environment new_env = env; if (rec_on_num_univs == ind_num_univs) { @@ -32,7 +31,7 @@ environment mk_induction_on(environment const & env, name const & n) { certified_declaration cdecl = check(new_env, mk_definition(new_env, induction_on_name, rec_on_decl.get_univ_params(), rec_on_decl.get_type(), rec_on_decl.get_value(), - opaque, use_conv_opt)); + use_conv_opt)); new_env = module::add(new_env, cdecl); } else { level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params()); @@ -43,7 +42,7 @@ environment mk_induction_on(environment const & env, name const & n) { certified_declaration cdecl = check(new_env, mk_definition(new_env, induction_on_name, induction_on_univs, induction_on_type, induction_on_value, - opaque, use_conv_opt)); + use_conv_opt)); new_env = module::add(new_env, cdecl); } return add_protected(new_env, induction_on_name); diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index 781ea825c..bda26b668 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -134,10 +134,9 @@ optional mk_no_confusion_type(environment const & env, name const & } expr no_confusion_type_value = Fun(args, mk_app(cases_on1, outer_cases_on_args)); - bool opaque = false; bool use_conv_opt = true; declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, - opaque, use_conv_opt); + use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible); return some(add_protected(new_env, no_confusion_type_name)); @@ -269,10 +268,9 @@ environment mk_no_confusion(environment const & env, name const & n) { } // expr no_confusion_val = Fun(args, eq_rec); - bool opaque = false; bool use_conv_opt = true; declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, - opaque, use_conv_opt); + use_conv_opt); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible); return add_protected(new_env, no_confusion_name); diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 1b2f64ed6..d2e22ad60 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -129,10 +129,9 @@ environment mk_projections(environment const & env, name const & n, buffer expr proj_type = Pi(proj_args, result_type); proj_type = infer_implicit_params(proj_type, nparams, infer_k); expr proj_val = Fun(proj_args, rec_app); - bool opaque = false; bool use_conv_opt = false; declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val, - opaque, use_conv_opt); + use_conv_opt); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, proj_name, reducible_status::Reducible); new_env = add_unfold_c_hint(new_env, proj_name, nparams); diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index f4df0c84a..1925aac4c 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -53,12 +53,10 @@ environment mk_rec_on(environment const & env, name const & n) { expr rec = mk_constant(rec_decl.get_name(), ls); expr rec_on_val = Fun(new_locals, mk_app(rec, locals)); - bool opaque = false; bool use_conv_opt = true; environment new_env = module::add(env, check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), - rec_on_type, rec_on_val, - opaque, use_conv_opt))); + rec_on_type, rec_on_val, use_conv_opt))); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible); new_env = add_unfold_c_hint(new_env, rec_on_name, rec_on_major_idx); return add_protected(new_env, rec_on_name); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 3072978fd..f819e3c4c 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -742,7 +742,6 @@ DECLARATION_PRED(is_definition) DECLARATION_PRED(is_theorem) DECLARATION_PRED(is_axiom) DECLARATION_PRED(is_constant_assumption) -DECLARATION_PRED(is_opaque) DECLARATION_PRED(use_conv_opt) static int declaration_get_name(lua_State * L) { return push_name(L, to_declaration(L, 1).get_name()); } static int declaration_get_params(lua_State * L) { return push_list_name(L, to_declaration(L, 1).get_univ_params()); } @@ -774,37 +773,36 @@ static int mk_theorem(lua_State * L) { else return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4))); } -static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, bool & use_conv_opt) { - opaque = get_bool_named_param(L, idx, "opaque", opaque); +static void get_definition_args(lua_State * L, int idx, unsigned & weight, bool & use_conv_opt) { use_conv_opt = get_bool_named_param(L, idx, "use_conv_opt", use_conv_opt); weight = get_uint_named_param(L, idx, "weight", weight); } static int mk_definition(lua_State * L) { int nargs = lua_gettop(L); - bool opaque = false; unsigned weight = 0; bool use_conv_opt = true; + unsigned weight = 0; bool use_conv_opt = true; if (nargs < 3) { throw exception("mk_definition must have at least 3 arguments"); } else if (is_environment(L, 1)) { if (nargs < 4) { throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment"); } else if (is_expr(L, 3)) { - get_definition_args(L, 5, opaque, weight, use_conv_opt); + get_definition_args(L, 5, weight, use_conv_opt); return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(), - to_expr(L, 3), to_expr(L, 4), opaque, use_conv_opt)); + to_expr(L, 3), to_expr(L, 4), use_conv_opt)); } else { - get_definition_args(L, 6, opaque, weight, use_conv_opt); + get_definition_args(L, 6, weight, use_conv_opt); return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3), - to_expr(L, 4), to_expr(L, 5), opaque, use_conv_opt)); + to_expr(L, 4), to_expr(L, 5), use_conv_opt)); } } else { if (is_expr(L, 2)) { - get_definition_args(L, 4, opaque, weight, use_conv_opt); + get_definition_args(L, 4, weight, use_conv_opt); return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), - to_expr(L, 3), opaque, weight, use_conv_opt)); + to_expr(L, 3), weight, use_conv_opt)); } else { - get_definition_args(L, 5, opaque, weight, use_conv_opt); + get_definition_args(L, 5, weight, use_conv_opt); return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2), - to_expr(L, 3), to_expr(L, 4), opaque, weight, use_conv_opt)); + to_expr(L, 3), to_expr(L, 4), weight, use_conv_opt)); } } } @@ -815,7 +813,6 @@ static const struct luaL_Reg declaration_m[] = { {"is_theorem", safe_function}, {"is_axiom", safe_function}, {"is_constant_assumption", safe_function}, - {"opaque", safe_function}, {"use_conv_opt", safe_function}, {"name", safe_function}, {"univ_params", safe_function}, diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 8d3a286f5..628c9f582 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -282,13 +282,11 @@ serializer & operator<<(serializer & s, declaration const & d) { char k = 0; if (d.is_definition()) { k |= 1; - if (d.is_opaque()) - k |= 2; if (d.use_conv_opt()) - k |= 4; + k |= 2; } if (d.is_theorem() || d.is_axiom()) - k |= 8; + k |= 4; s << k << d.get_name() << d.get_univ_params() << d.get_type(); if (d.is_definition()) { s << d.get_value(); @@ -301,7 +299,7 @@ serializer & operator<<(serializer & s, declaration const & d) { declaration read_declaration(deserializer & d) { char k = d.read_char(); bool has_value = (k & 1) != 0; - bool is_th_ax = (k & 8) != 0; + bool is_th_ax = (k & 4) != 0; name n = read_name(d); level_param_names ps = read_level_params(d); expr t = read_expr(d); @@ -311,9 +309,8 @@ declaration read_declaration(deserializer & d) { return mk_theorem(n, ps, t, v); } else { unsigned w = d.read_unsigned(); - bool is_opaque = (k & 2) != 0; - bool use_conv_opt = (k & 4) != 0; - return mk_definition(n, ps, t, v, is_opaque, w, use_conv_opt); + bool use_conv_opt = (k & 2) != 0; + return mk_definition(n, ps, t, v, w, use_conv_opt); } } else { if (is_th_ax) diff --git a/src/library/module.cpp b/src/library/module.cpp index 9fd917c56..1b7cd3e75 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -409,7 +409,6 @@ struct import_modules_fn { void import_decl(deserializer & d) { declaration decl = read_declaration(d); - lean_assert(!decl.is_definition()); environment env = m_senv.env(); decl = unfold_untrusted_macros(env, decl); if (decl.get_name() == get_sorry_name() && has_sorry(env)) diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 5927d6af6..d195e720d 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -105,7 +105,7 @@ typedef scoped_ext unfold_hint_ext; environment add_unfold_c_hint(environment const & env, name const & n, unsigned idx, bool persistent) { declaration const & d = env.get(n); - if (!d.is_definition() || d.is_opaque()) + if (!d.is_definition()) throw exception("invalid unfold-c hint, declaration must be a non-opaque definition"); return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_c_entry(n, idx), persistent); } @@ -124,7 +124,7 @@ environment erase_unfold_c_hint(environment const & env, name const & n, bool pe environment add_unfold_f_hint(environment const & env, name const & n, bool persistent) { declaration const & d = env.get(n); - if (!d.is_definition() || d.is_opaque()) + if (!d.is_definition()) throw exception("invalid unfold-f hint, declaration must be a non-opaque definition"); return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_f_entry(n), persistent); } diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index db4980780..2bf75b252 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -86,8 +86,6 @@ static void check_declaration(environment const & env, name const & n) { throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition"); if (d.is_theorem()) throw exception(sstream() << "invalid reducible command, '" << n << "' is a theorem"); - if (d.is_opaque()) - throw exception(sstream() << "invalid reducible command, '" << n << "' is an opaque definition"); } environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent) { diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp index 0c5020504..560102537 100644 --- a/src/library/unfold_macros.cpp +++ b/src/library/unfold_macros.cpp @@ -147,7 +147,7 @@ declaration unfold_untrusted_macros(environment const & env, declaration const & } else if (d.is_definition()) { expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl); return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v, - d.is_opaque(), d.get_weight(), d.use_conv_opt()); + d.get_weight(), d.use_conv_opt()); } else if (d.is_axiom()) { return mk_axiom(d.get_name(), d.get_univ_params(), new_t); } else if (d.is_constant_assumption()) { diff --git a/src/library/update_declaration.cpp b/src/library/update_declaration.cpp index b22aa9e2f..f127a51d7 100644 --- a/src/library/update_declaration.cpp +++ b/src/library/update_declaration.cpp @@ -30,7 +30,7 @@ static declaration update_declaration(declaration d, optional if (d.is_theorem()) return mk_theorem(d.get_name(), _ps, _type, _value); else - return mk_definition(d.get_name(), _ps, _type, _value, d.is_opaque(), + return mk_definition(d.get_name(), _ps, _type, _value, d.get_weight(), d.use_conv_opt()); } } diff --git a/src/library/util.cpp b/src/library/util.cpp index b17a1778c..a5f5af7b2 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -21,16 +21,6 @@ bool is_standard(environment const & env) { return env.prop_proof_irrel() && env.impredicative(); } -bool is_def_app(environment const & env, expr const & e) { - if (!is_app(e)) - return false; - expr const & f = get_app_fn(e); - if (!is_constant(f)) - return false; - auto decl = env.find(const_name(f)); - return decl && decl->is_definition() && !decl->is_opaque(); -} - optional unfold_app(environment const & env, expr const & e) { if (!is_app(e)) return none_expr(); @@ -38,7 +28,7 @@ optional unfold_app(environment const & env, expr const & e) { if (!is_constant(f)) return none_expr(); auto decl = env.find(const_name(f)); - if (!decl || !decl->is_definition() || decl->is_opaque()) + if (!decl || !decl->is_definition()) return none_expr(); expr d = instantiate_value_univ_params(*decl, const_levels(f)); buffer args; @@ -191,7 +181,7 @@ optional is_constructor_app_ext(environment const & env, expr const & e) { if (!is_constant(f)) return optional(); auto decl = env.find(const_name(f)); - if (!decl || !decl->is_definition() || decl->is_opaque()) + if (!decl || !decl->is_definition()) return optional(); expr const * it = &decl->get_value(); while (is_lambda(*it)) diff --git a/src/library/util.h b/src/library/util.h index fea668394..3e90bcf88 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -10,11 +10,6 @@ Author: Leonardo de Moura namespace lean { typedef std::unique_ptr type_checker_ptr; - -/** \brief Return true iff \c e is of the form (f ...) where - \c f is a non-opaque constant definition */ -bool is_def_app(environment const & env, expr const & e); - /** \brief If \c e is of the form (f a_1 ... a_n), where \c f is a non-opaque definition, then unfold \c f, and beta reduce. Otherwise, return none. diff --git a/tests/lean/run/reducible.lean b/tests/lean/run/reducible.lean index 88964b453..5a719cb03 100644 --- a/tests/lean/run/reducible.lean +++ b/tests/lean/run/reducible.lean @@ -1,7 +1,7 @@ definition x [reducible] := 10 definition y := 20 definition z [irreducible] := 30 -opaque definition w := 40 +definition w := 40 (* local env = get_env() @@ -24,7 +24,6 @@ opaque definition w := 40 assert(tc:whnf(x) == val_x) assert(tc:whnf(y) == val_y) assert(tc:whnf(z) == z) - assert(tc:whnf(w) == w) -- Only definitions marked as reducible are unfolded local tc = reducible_type_checker(env) assert(tc:whnf(x) == val_x) @@ -37,7 +36,6 @@ opaque definition w := 40 assert(tc:whnf(x) == val_x) assert(tc:whnf(y) == val_y) assert(tc:whnf(z) == val_z) - assert(tc:whnf(w) == w) *) eval [whnf] x diff --git a/tests/lua/def1.lua b/tests/lua/def1.lua index 508fc567f..519cf5703 100644 --- a/tests/lua/def1.lua +++ b/tests/lua/def1.lua @@ -34,33 +34,29 @@ assert(d:use_conv_opt()) assert(d:name() == name("d1")) assert(d:value() == B) local d2 = mk_definition("d2", A, B, nil) -local d3 = mk_definition("d3", A, B, {opaque=false, weight=100, use_conv_opt=false}) -assert(not d3:opaque()) +local d3 = mk_definition("d3", A, B, {weight=100, use_conv_opt=false}) assert(d3:weight() == 100) assert(not d3:use_conv_opt()) local env = bare_environment() local d4 = mk_definition(env, "bool", Type, Prop) assert(d4:weight() == 1) -local d5 = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, use_conv_opt=true}) -assert(not d5:opaque()) +local d5 = mk_definition(env, "bool", Type, Prop, {weight=100, use_conv_opt=true}) assert(d5:weight() == 1) assert(d5:use_conv_opt()) -local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {opaque=true, weight=5}) +local d6 = mk_definition("d6", {"l1", "l2"}, A, B, {weight=5}) assert(d6:type() == A) assert(d6:value() == B) assert(#(d6:univ_params()) == 2) assert(d6:univ_params():head() == name("l1")) assert(d6:univ_params():tail():head() == name("l2")) -assert(d6:opaque()) assert(d6:weight() == 5) -local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {opaque=true, weight=5}) +local d7 = mk_definition(env, "d7", {"l1", "l2"}, A, B, {weight=5}) assert(d7:type() == A) assert(d7:value() == B) assert(d7:weight() == 1) assert(#(d7:univ_params()) == 2) assert(d7:univ_params():head() == name("l1")) assert(d7:univ_params():tail():head() == name("l2")) -assert(d7:opaque()) print("done") assert(not pcall(function() mk_theorem("t1", {max_univ("l1", "l2")}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0))) end)) local l1 = global_univ("l1")