diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index aa76f89c13..800246b6ec 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -84,7 +84,7 @@ meta def value : declaration → expr | (thm _ _ _ v) := v | _ := default expr -meta def is_trusted : declaration → bool +meta def is_meta : declaration → bool | (defn _ _ _ _ _ t) := t | (cnst _ _ _ t) := t | _ := tt diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 80332af14c..1989d7a8a9 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -126,8 +126,8 @@ static environment declare_var(parser & p, environment env, if (k == variable_kind::Axiom) { env = module::add(env, check(env, mk_axiom(full_n, ls, new_type))); } else { - bool is_trusted = !meta.m_modifiers.m_is_meta; - env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_trusted))); + bool is_meta = meta.m_modifiers.m_is_meta; + env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_meta))); } if (meta.m_doc_string) env = add_doc_string(env, full_n, *meta.m_doc_string); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index e3916febb8..2eb45582b2 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -251,12 +251,12 @@ declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buff std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val); } bool use_conv_opt = true; - bool is_trusted = !meta.m_modifiers.m_is_meta; + bool is_meta = meta.m_modifiers.m_is_meta; auto def = (kind == decl_cmd_kind::Theorem ? mk_theorem(c_real_name, names(lp_names), type, *val) : - (is_abbrev ? mk_definition(c_real_name, names(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_trusted) : - mk_definition(new_env, c_real_name, names(lp_names), type, *val, use_conv_opt, is_trusted))); + (is_abbrev ? mk_definition(c_real_name, names(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_meta) : + mk_definition(new_env, c_real_name, names(lp_names), type, *val, use_conv_opt, is_meta))); auto cdef = check(p, new_env, c_name, def, pos); new_env = module::add(new_env, cdef); @@ -702,9 +702,9 @@ static void check_example(environment const & decl_env, options const & opts, finalize_definition(elab, params_buf, type, val, univ_params_buf, modifiers.m_is_meta); bool use_conv_opt = true; - bool is_trusted = !modifiers.m_is_meta; + bool is_meta = modifiers.m_is_meta; auto new_env = elab.env(); - auto def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, use_conv_opt, is_trusted); + auto def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, use_conv_opt, is_meta); auto cdef = check(new_env, def); new_env = module::add(new_env, cdef); check_noncomputable(noncomputable_theory, new_env, decl_name, def.get_name(), modifiers.m_is_noncomputable, diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 3b9b494b00..1d3b0fb775 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -705,7 +705,7 @@ public: parse_result r; parse(r); m_env = add_inductive_declaration(m_p.env(), m_p.get_options(), m_implicit_infer_map, m_lp_names, r.m_params, - r.m_inds, r.m_intro_rules, !m_meta_info.m_modifiers.m_is_meta); + r.m_inds, r.m_intro_rules, m_meta_info.m_modifiers.m_is_meta); post_process(r.m_params, r.m_inds, r.m_intro_rules); return m_env; } diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 8276f967c8..3e53ad5d32 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -88,7 +88,7 @@ static void print_axioms(parser & p, message_builder & out) { bool has_axioms = false; p.env().for_each_declaration([&](declaration const & d) { name const & n = d.get_name(); - if (!d.is_definition() && !p.env().is_builtin(n) && d.is_trusted()) { + if (!d.is_definition() && !p.env().is_builtin(n) && !d.is_meta()) { out << n << " : " << d.get_type() << endl; has_axioms = true; } @@ -328,7 +328,7 @@ static bool print_constant(parser const & p, message_builder & out, char const * out << "protected "; if (d.is_definition() && is_marked_noncomputable(p.env(), d.get_name())) out << "noncomputable "; - if (!d.is_trusted()) + if (d.is_meta()) out << "meta "; out << kind << " " << to_user_name(p.env(), d.get_name()); out.get_text_stream().update_options(out.get_text_stream().get_options().update((name {"pp", "binder_types"}), true)) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 515dd0836a..80a8785f1f 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -1069,8 +1069,8 @@ struct structure_cmd_fn { level_param_names lnames = names(m_level_names); inductive::intro_rule intro = inductive::mk_intro_rule(m_mk, intro_type); inductive::inductive_decl decl(m_name, lnames, m_params.size(), structure_type, to_list(intro)); - bool is_trusted = !m_meta_info.m_modifiers.m_is_meta; - m_env = module::add_inductive(m_env, decl, is_trusted); + bool is_meta = m_meta_info.m_modifiers.m_is_meta; + m_env = module::add_inductive(m_env, decl, is_meta); name rec_name = inductive::get_elim_name(m_name); m_env = add_namespace(m_env, m_name); m_env = add_protected(m_env, rec_name); @@ -1079,7 +1079,7 @@ struct structure_cmd_fn { add_rec_alias(rec_name); m_env = add_structure_declaration_aux(m_env, m_p.get_options(), m_level_names, m_params, mk_local(m_name, mk_structure_type_no_params()), - mk_local(m_mk, mk_intro_type_no_params()), is_trusted); + mk_local(m_mk, mk_intro_type_no_params()), is_meta); } void declare_projections() { @@ -1146,7 +1146,7 @@ struct structure_cmd_fn { used_univs = collect_univ_params(decl_value, used_univs); used_univs = collect_univ_params(decl_type, used_univs); level_param_names decl_lvls = to_level_param_names(used_univs); - declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls, + declaration new_decl = mk_definition_inferring_meta(m_env, decl_name, decl_lvls, decl_type, decl_value, reducibility_hints::mk_abbreviation()); m_env = module::add(m_env, check(m_env, new_decl)); if (!m_meta_info.m_modifiers.m_is_meta) @@ -1159,7 +1159,7 @@ struct structure_cmd_fn { void add_rec_on_alias(name const & n) { name rec_on_name(m_name, "rec_on"); declaration rec_on_decl = m_env.get(rec_on_name); - declaration new_decl = mk_definition_inferring_trusted(m_env, n, rec_on_decl.get_univ_params(), + declaration new_decl = mk_definition_inferring_meta(m_env, n, rec_on_decl.get_univ_params(), rec_on_decl.get_type(), rec_on_decl.get_value(), reducibility_hints::mk_abbreviation()); m_env = module::add(m_env, check(m_env, new_decl)); @@ -1255,8 +1255,8 @@ struct structure_cmd_fn { coercion_value = Fun(m_params, Fun(st, coercion_value, m_p), m_p); name coercion_name = coercion_names[i]; bool use_conv_opt = false; - declaration coercion_decl = mk_definition_inferring_trusted(m_env, coercion_name, lnames, - coercion_type, coercion_value, use_conv_opt); + declaration coercion_decl = mk_definition_inferring_meta(m_env, coercion_name, lnames, + coercion_type, coercion_value, use_conv_opt); m_env = module::add(m_env, check(m_env, coercion_decl)); add_alias(coercion_name); m_env = vm_compile(m_env, m_env.get(coercion_name)); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index e09ef5b0a4..a1b10340ee 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -515,8 +515,8 @@ void initialize_frontend_lean_util() { environment compile_expr(environment const & env, name const & n, level_param_names const & ls, expr const & type, expr const & e, pos_info const & pos) { environment new_env = env; bool use_conv_opt = true; - bool is_trusted = false; - auto cd = check(new_env, mk_definition(new_env, n, ls, type, e, use_conv_opt, is_trusted)); + bool is_meta = true; + auto cd = check(new_env, mk_definition(new_env, n, ls, type, e, use_conv_opt, is_meta)); new_env = new_env.add(cd); new_env = add_transient_decl_pos_info(new_env, n, pos); return vm_compile(new_env, new_env.get(n)); diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h index fb56f9f674..2d167179d5 100644 --- a/src/kernel/abstract_type_context.h +++ b/src/kernel/abstract_type_context.h @@ -30,8 +30,6 @@ public: virtual expr check(expr const & e) { return infer(e); } virtual optional is_stuck(expr const &) { return none_expr(); } - virtual bool is_trusted_only() const { return false; } - virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); virtual void pop_local(); virtual bool has_local_pp_name(name const & pp_name); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 28c8b09e10..3a960df35a 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -52,7 +52,7 @@ bool declaration::is_definition() const { return static_cast(m_ptr->m_v bool declaration::is_constant_assumption() const { return !is_definition(); } bool declaration::is_axiom() const { return is_constant_assumption() && m_ptr->m_theorem; } bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; } -bool declaration::is_trusted() const { return m_ptr->m_trusted; } +bool declaration::is_meta() const { return m_ptr->m_meta; } name const & declaration::get_name() const { return m_ptr->m_name; } level_param_names const & declaration::get_univ_params() const { return m_ptr->m_params; } @@ -66,8 +66,8 @@ expr const & declaration::get_value() const { reducibility_hints const & declaration::get_hints() const { return m_ptr->m_hints; } declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, - reducibility_hints const & h, bool trusted) { - return declaration(new declaration::cell(n, params, t, v, h, trusted)); + reducibility_hints const & h, bool meta) { + return declaration(new declaration::cell(n, params, t, v, h, meta)); } static unsigned get_max_height(environment const & env, expr const & v) { unsigned h = 0; @@ -83,27 +83,27 @@ static unsigned get_max_height(environment const & env, expr const & v) { } declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, - expr const & v, bool use_self_opt, bool trusted) { + expr const & v, bool use_self_opt, bool meta) { unsigned h = get_max_height(env, v); - return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), trusted); + return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), meta); } 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, v)); } declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { - return declaration(new declaration::cell(n, params, t, true, true)); + return declaration(new declaration::cell(n, params, t, true, false)); } -declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted) { - return declaration(new declaration::cell(n, params, t, false, trusted)); +declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool meta) { + return declaration(new declaration::cell(n, params, t, false, meta)); } -bool use_untrusted(environment const & env, expr const & e) { +bool use_meta(environment const & env, expr const & e) { bool found = false; for_each(e, [&](expr const & e, unsigned) { if (found) return false; if (is_constant(e)) { if (auto d = env.find(const_name(e))) { - if (!d->is_trusted()) { + if (d->is_meta()) { found = true; return false; } @@ -114,20 +114,22 @@ bool use_untrusted(environment const & env, expr const & e) { return found; } -declaration mk_definition_inferring_trusted(environment const & env, name const & n, level_param_names const & params, +declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, reducibility_hints const & hints) { - bool trusted = !use_untrusted(env, t) && !use_untrusted(env, v); - return mk_definition(n, params, t, v, hints, trusted); + bool meta = use_meta(env, t) || use_meta(env, v); + return mk_definition(n, params, t, v, hints, meta); } -declaration mk_definition_inferring_trusted(environment const & env, name const & n, level_param_names const & params, - expr const & t, expr const & v, bool use_self_opt) { - bool trusted = !use_untrusted(env, t) && !use_untrusted(env, v); - unsigned h = get_max_height(env, v); - return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), trusted); + +declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, + expr const & t, expr const & v, bool use_self_opt) { + bool meta = use_meta(env, t) && use_meta(env, v); + unsigned h = get_max_height(env, v); + return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), meta); } -declaration mk_constant_assumption_inferring_trusted(environment const & env, name const & n, - level_param_names const & params, expr const & t) { - return mk_constant_assumption(n, params, t, !use_untrusted(env, t)); + +declaration mk_constant_assumption_inferring_meta(environment const & env, name const & n, + level_param_names const & params, expr const & t) { + return mk_constant_assumption(n, params, t, use_meta(env, t)); } void initialize_declaration() { diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 861200ffeb..8cb576c786 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -76,23 +76,20 @@ class declaration { bool m_theorem; optional m_value; // if none, then declaration is actually a postulate reducibility_hints m_hints; - /* Definitions are trusted by default, and nested macros are expanded when kernel is instantiated with - trust level 0. When this flag is false, then we do not expand nested macros. We say the - associated definitions are "untrusted". We use this feature to define tactical-definitions. - The kernel type checker ensures trusted definitions do not use untrusted ones. */ - bool m_trusted; + /* Definitions are non-meta by default. We use this feature to define tactical-definitions. */ + bool m_meta; void dealloc() { delete this; } - cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool trusted): + cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool meta): m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom), - m_hints(reducibility_hints::mk_opaque()), m_trusted(trusted) {} + m_hints(reducibility_hints::mk_opaque()), m_meta(meta) {} cell(name const & n, level_param_names const & params, expr const & t, expr const & v, - reducibility_hints const & h, bool trusted): + reducibility_hints const & h, bool meta): m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(false), - m_value(v), m_hints(h), m_trusted(trusted) {} + m_value(v), m_hints(h), m_meta(meta) {} cell(name const & n, level_param_names const & params, expr const & t, expr const & v): m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(true), - m_value(v), m_hints(reducibility_hints::mk_opaque()), m_trusted(true) {} + m_value(v), m_hints(reducibility_hints::mk_opaque()), m_meta(false) {} }; cell * m_ptr; explicit declaration(cell * ptr); @@ -123,7 +120,7 @@ public: bool is_theorem() const; bool is_constant_assumption() const; - bool is_trusted() const; + bool is_meta() const; name const & get_name() const; level_param_names const & get_univ_params() const; @@ -134,12 +131,12 @@ public: reducibility_hints const & get_hints() const; friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, - reducibility_hints const & hints, bool trusted); + reducibility_hints const & hints, bool meta); friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, - expr const & v, bool use_conv_opt, bool trusted); + expr const & v, bool use_conv_opt, bool meta); friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &); friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t); - friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted); + friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool meta); }; inline optional none_declaration() { return optional(); } @@ -147,27 +144,27 @@ 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, - reducibility_hints const & hints, bool trusted = true); + reducibility_hints const & hints, bool meta = false); declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v, - bool use_conv_opt = true, bool trusted = true); + bool use_conv_opt = true, bool meta = false); declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v); 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, bool trusted = true); +declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool meta = false); /** \brief Return true iff \c e depends on meta-declarations */ -bool use_untrusted(environment const & env, expr const & e); +bool use_meta(environment const & env, expr const & e); -/** \brief Similar to mk_definition but infer the value of trusted flag. - That is, set it to false if \c t or \c v contains a untrusted declaration. */ -declaration mk_definition_inferring_trusted(environment const & env, name const & n, level_param_names const & params, - expr const & t, expr const & v, reducibility_hints const & hints); -declaration mk_definition_inferring_trusted(environment const & env, name const & n, level_param_names const & params, - expr const & t, expr const & v, bool use_self_opt); -/** \brief Similar to mk_constant_assumption but infer the value of trusted flag. - That is, set it to false if \c t or \c v contains a untrusted declaration. */ -declaration mk_constant_assumption_inferring_trusted(environment const & env, name const & n, - level_param_names const & params, expr const & t); +/** \brief Similar to mk_definition but infer the value of meta flag. + That is, set it to true if \c t or \c v contains a meta declaration. */ +declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, + expr const & t, expr const & v, reducibility_hints const & hints); +declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params, + expr const & t, expr const & v, bool use_self_opt); +/** \brief Similar to mk_constant_assumption but infer the value of meta flag. + That is, set it to true if \c t or \c v contains a meta declaration. */ +declaration mk_constant_assumption_inferring_meta(environment const & env, name const & n, + level_param_names const & params, expr const & t); void initialize_declaration(); void finalize_declaration(); diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 8bf6cc68de..1752261558 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -187,7 +187,7 @@ name get_elim_name(name const & n) { environment certified_inductive_decl::add_constant(environment const & env, name const & n, level_param_names const & ls, expr const & t) const { - return env.add(certify_unchecked::certify_or_check(env, mk_constant_assumption(n, ls, t, m_is_trusted))); + return env.add(certify_unchecked::certify_or_check(env, mk_constant_assumption(n, ls, t, m_is_meta))); } environment certified_inductive_decl::add_core(environment const & env, bool update_ext_only) const { @@ -220,7 +220,7 @@ environment certified_inductive_decl::add_core(environment const & env, bool upd environment certified_inductive_decl::add(environment const & env) const { if (env.trust_lvl() == 0) { - return add_inductive(env, m_decl, m_is_trusted).first; + return add_inductive(env, m_decl, m_is_meta).first; } else { return add_core(env, false); } @@ -256,16 +256,16 @@ struct add_inductive_fn { elim_info():m_K_target(false) {} }; elim_info m_elim_info; // for datatype being declared - bool m_is_trusted; + bool m_is_meta; add_inductive_fn(environment env, inductive_decl const & decl, - bool is_trusted): + bool is_meta): m_env(env), m_name_generator(*g_ind_fresh), m_decl(decl), m_tc(new type_checker(m_env, true, false)) { m_is_not_zero = false; m_levels = param_names_to_levels(decl.m_level_params); - m_is_trusted = is_trusted; + m_is_meta = is_meta; } /** \brief Make sure the latest environment is being used by m_tc. */ @@ -323,7 +323,7 @@ struct add_inductive_fn { /** \brief Add all datatype declarations to environment. */ void declare_inductive_type() { m_env = m_env.add(check(m_env, mk_constant_assumption(m_decl.m_name, m_decl.m_level_params, m_decl.m_type, - m_is_trusted))); + m_is_meta))); updt_type_checker(); } @@ -408,7 +408,7 @@ struct add_inductive_fn { if (!(is_geq(m_it_level, sort_level(s)) || is_zero(m_it_level))) throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") " << "of '" << n << "' is too big for the corresponding inductive datatype"); - if (m_is_trusted) + if (!m_is_meta) check_positivity(binding_domain(t), n, i); bool is_rec = (bool)is_rec_argument(binding_domain(t)); // NOLINT if (is_rec) @@ -445,7 +445,7 @@ struct add_inductive_fn { for (auto ir : m_decl.m_intro_rules) { m_env = m_env.add(check(m_env, mk_constant_assumption(intro_rule_name(ir), m_decl.m_level_params, intro_rule_type(ir), - m_is_trusted))); + m_is_meta))); } updt_type_checker(); } @@ -660,7 +660,7 @@ struct add_inductive_fn { elim_ty = Pi(m_param_consts, elim_ty); elim_ty = infer_implicit(elim_ty, true /* strict */); m_env = m_env.add(check(m_env, mk_constant_assumption(get_elim_name(), get_elim_level_param_names(), elim_ty, - m_is_trusted))); + m_is_meta))); return elim_ty; } @@ -724,7 +724,7 @@ struct add_inductive_fn { return certified_inductive_decl(m_decl.m_num_params + 1 + e.size(), elim_Prop, m_dep_elim, get_elim_level_param_names(), elim_type, m_decl, m_elim_info.m_K_target, m_elim_info.m_indices.size(), to_list(comp_rules), - m_is_trusted); + m_is_meta); } pair operator()() { @@ -739,10 +739,10 @@ struct add_inductive_fn { }; pair -add_inductive(environment env, inductive_decl const & decl, bool is_trusted) { +add_inductive(environment env, inductive_decl const & decl, bool is_meta) { if (!env.norm_ext().supports(*g_inductive_extension)) throw kernel_exception(env, "environment does not support inductive datatypes"); - return add_inductive_fn(env, decl, is_trusted)(); + return add_inductive_fn(env, decl, is_meta)(); } bool inductive_normalizer_extension::supports(name const & feature) const { diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index a3d06afc55..f4fcbb9799 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -63,7 +63,7 @@ private: bool m_K_target; unsigned m_num_indices; list m_comp_rules; - bool m_is_trusted; + bool m_is_meta; friend struct add_inductive_fn; friend class ::lean::read_certified_inductive_decl_fn; @@ -73,11 +73,11 @@ private: certified_inductive_decl(unsigned num_ACe, bool elim_prop, bool dep_delim, level_param_names const & elim_levels, expr const & elim_type, inductive_decl const & decl, bool K_target, unsigned nindices, - list const & crules, bool is_trusted): + list const & crules, bool is_meta): m_num_ACe(num_ACe), m_elim_prop(elim_prop), m_dep_elim(dep_delim), m_elim_levels(elim_levels), m_elim_type(elim_type), m_decl(decl), m_K_target(K_target), m_num_indices(nindices), m_comp_rules(crules), - m_is_trusted(is_trusted) {} + m_is_meta(is_meta) {} public: unsigned get_num_ACe() const { return m_num_ACe; } bool elim_prop_only() const { return m_elim_prop; } @@ -88,7 +88,7 @@ public: bool is_K_target() const { return m_K_target; } unsigned get_num_indices() const { return m_num_indices; } list get_comp_rules() const { return m_comp_rules; } - bool is_trusted() const { return m_is_trusted; } + bool is_meta() const { return m_is_meta; } /** \brief Update the environment with this "certified declaration" \remark If trust_level is 0, then declaration is rechecked. */ @@ -99,7 +99,7 @@ public: pair add_inductive(environment env, inductive_decl const & decl, - bool is_trusted); + bool is_meta); /** \brief If \c n is the name of an inductive declaration in the environment \c env, then return the list of all inductive decls that were simultaneously defined with \c n. diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index abc2d21a73..db61f34d71 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -83,8 +83,8 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) { << const_name(e) << "', #" << length(ps) << " expected, #" << length(ls) << " provided"); if (!infer_only) { - if (m_trusted_only && !d.is_trusted()) { - throw_kernel_exception(m_env, sstream() << "invalid definition, it uses untrusted declaration '" + if (m_non_meta_only && d.is_meta()) { + throw_kernel_exception(m_env, sstream() << "invalid definition, it uses meta declaration '" << const_name(e) << "'"); } for (level const & l : ls) @@ -96,10 +96,11 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) { expr type_checker::infer_macro(expr const & e, bool infer_only) { auto def = macro_def(e); auto t = def.check_type(e, *this, infer_only); - if (!infer_only && m_trusted_only && def.trust_level() >= m_env.trust_lvl()) { - throw_kernel_exception(m_env, "declaration contains macro with trust-level higher than the one allowed " - "(possible solution: unfold macro, or increase trust-level)", e); - } +// TODO(Leo): macros will be deleted +// if (!infer_only && m_trusted_only && def.trust_level() >= m_env.trust_lvl()) { +// throw_kernel_exception(m_env, "declaration contains macro with trust-level higher than the one allowed " +// "(possible solution: unfold macro, or increase trust-level)", e); +// } return t; } @@ -709,8 +710,8 @@ bool type_checker::is_def_eq(expr const & t, expr const & s) { return r; } -type_checker::type_checker(environment const & env, bool memoize, bool trusted_only): - m_env(env), m_name_generator(*g_kernel_fresh), m_memoize(memoize), m_trusted_only(trusted_only), m_params(nullptr) { +type_checker::type_checker(environment const & env, bool memoize, bool non_meta_only): + m_env(env), m_name_generator(*g_kernel_fresh), m_memoize(memoize), m_non_meta_only(non_meta_only), m_params(nullptr) { } type_checker::~type_checker() {} @@ -760,8 +761,8 @@ certified_declaration check(environment const & env, declaration const & d) { check_no_mlocal(env, d.get_name(), d.get_type(), true); check_name(env, d.get_name()); check_duplicated_params(env, d); - bool memoize = true; bool trusted_only = d.is_trusted(); - type_checker checker(env, memoize, trusted_only); + bool memoize = true; bool non_meta_only = !d.is_meta(); + type_checker checker(env, memoize, non_meta_only); expr sort = checker.check(d.get_type(), d.get_univ_params()); checker.ensure_sort(sort, d.get_type()); if (d.is_definition()) { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index cff75574c1..27983fede3 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -32,7 +32,7 @@ class type_checker : public abstract_type_context { environment m_env; name_generator m_name_generator; bool m_memoize; - bool m_trusted_only; + bool m_non_meta_only; cache m_infer_type_cache[2]; expr_map m_whnf_core_cache; expr_map m_whnf_cache; @@ -79,8 +79,10 @@ class type_checker : public abstract_type_context { public: /** \brief Create a type checker for the given environment. - memoize: if true, then inferred types are memoized/cached */ - type_checker(environment const & env, bool memoize = true, bool trusted_only = true); + memoize: if true, then inferred types are memoized/cached. + + */ + type_checker(environment const & env, bool memoize = true, bool non_meta_only = true); ~type_checker(); virtual environment const & env() const { return m_env; } @@ -101,8 +103,6 @@ public: expr check_ignore_undefined_universes(expr const & e); virtual expr check(expr const & t) { return check_ignore_undefined_universes(t); } - virtual bool is_trusted_only() const { return m_trusted_only; } - /** \brief Return true iff t is definitionally equal to s. */ virtual bool is_def_eq(expr const & t, expr const & s); /** \brief Return true iff types of \c t and \c s are (may be) definitionally equal. */ diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index b337e9fdeb..baa9736837 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -152,7 +152,7 @@ buffer const & closure_helper::get_norm_closure_params() const { struct mk_aux_definition_fn : public closure_helper { mk_aux_definition_fn(type_context_old & ctx):closure_helper(ctx) {} - pair operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional const & is_meta) { + pair operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional is_meta) { lean_assert(!is_lemma || is_meta); lean_assert(!is_lemma || *is_meta == false); expr new_type = collect(ctx().instantiate_mvars(type)); @@ -161,21 +161,14 @@ struct mk_aux_definition_fn : public closure_helper { finalize_collection(); expr def_type = mk_pi_closure(new_type); expr def_value = mk_lambda_closure(new_value); - bool untrusted = false; - if (is_meta) - untrusted = *is_meta; - else - untrusted = use_untrusted(env, def_type) || use_untrusted(env, def_value); - if (!untrusted) { - def_type = unfold_untrusted_macros(env, def_type); - def_value = unfold_untrusted_macros(env, def_value); - } + if (!is_meta) + is_meta = use_meta(env, def_type) || use_meta(env, def_value); declaration d; if (is_lemma) { d = mk_theorem(c, get_norm_level_names(), def_type, def_value); } else { bool use_self_opt = true; - d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, use_self_opt, !untrusted); + d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, use_self_opt, *is_meta); } environment new_env = module::add(env, check(env, d)); buffer ls; diff --git a/src/library/aux_definition.h b/src/library/aux_definition.h index 2360817659..140ab2e1e0 100644 --- a/src/library/aux_definition.h +++ b/src/library/aux_definition.h @@ -107,7 +107,7 @@ public: where l_i's and a_j's are the collected dependencies. - If is_meta is none, then function also computes whether the new definition should be tagged as trusted or not. + If is_meta is none, then function also computes whether the new definition should be tagged as meta or not. The updated environment is an extension of ctx.env() */ pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp index 6f533fcf8f..95179aec61 100644 --- a/src/library/compiler/elim_recursors.cpp +++ b/src/library/compiler/elim_recursors.cpp @@ -33,10 +33,10 @@ protected: level_param_names ps = to_level_param_names(collect_univ_params(value)); type_checker tc(m_env); expr type = tc.infer(value); - bool trusted = false; + bool meta = true; /* We add declaration as a constant to make sure we can infer the type of the resultant expression. */ - declaration new_decl = mk_constant_assumption(n, ps, type, trusted); + declaration new_decl = mk_constant_assumption(n, ps, type, meta); m_env = m_env.add(check(m_env, new_decl)); return mk_constant(n, param_names_to_levels(ps)); } diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 1749baa9f8..6a3826fd1e 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -164,9 +164,9 @@ class preprocess_fn { context_cache m_cache; bool check(declaration const & d, expr const & v) { - bool memoize = true; - bool trusted_only = false; - type_checker tc(m_env, memoize, trusted_only); + bool memoize = true; + bool non_meta_only = false; + type_checker tc(m_env, memoize, non_meta_only); expr t = tc.check(v, d.get_univ_params()); if (!tc.is_def_eq(d.get_type(), t)) throw exception("preprocess failed"); diff --git a/src/library/compiler/rec_fn_macro.cpp b/src/library/compiler/rec_fn_macro.cpp index b05dbf2635..33c2b31003 100644 --- a/src/library/compiler/rec_fn_macro.cpp +++ b/src/library/compiler/rec_fn_macro.cpp @@ -34,10 +34,7 @@ public: virtual void display(std::ostream & out) const override { out << m_name; } - virtual expr check_type(expr const & m, abstract_type_context & tc, bool) const override { - if (tc.is_trusted_only()) { - throw exception("rec_fn_macro only allowed in meta definitions"); - } + virtual expr check_type(expr const & m, abstract_type_context & /* tc */, bool) const override { check_macro(m); return macro_arg(m, 0); } diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index bdbe5988f4..5fef98d9c6 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -145,8 +145,8 @@ 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); - declaration new_d = mk_definition_inferring_trusted(env, below_name, blvls, below_type, below_value, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(env, below_name, blvls, below_type, below_value, + reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true); return add_protected(new_env, below_name); @@ -324,8 +324,8 @@ 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_pprod_fst(tc, rec, ind)); - declaration new_d = mk_definition_inferring_trusted(env, brec_on_name, blps, brec_on_type, brec_on_value, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(env, brec_on_name, blps, brec_on_type, brec_on_value, + reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, brec_on_name); diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index 7e963a2e35..214a79289e 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -111,8 +111,8 @@ 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)); - declaration new_d = mk_definition_inferring_trusted(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value, + reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, cases_on_name); diff --git a/src/library/constructions/drec.cpp b/src/library/constructions/drec.cpp index f2b5cfa187..50842be0dd 100644 --- a/src/library/constructions/drec.cpp +++ b/src/library/constructions/drec.cpp @@ -197,9 +197,9 @@ struct mk_drec_fn { expr rec_cnst = mk_constant(I_rec_name, lvls); expr drec_value = Fun(drec_params, mk_app(rec_cnst, rec_args)); name drec_name = mk_drec_name(); - declaration new_d = mk_definition_inferring_trusted(env, drec_name, I_rec_decl.get_univ_params(), - drec_type, drec_value, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(env, drec_name, I_rec_decl.get_univ_params(), + drec_type, drec_value, + reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, drec_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, drec_name); diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp index 5b545ce8e9..f6b95ac311 100644 --- a/src/library/constructions/has_sizeof.cpp +++ b/src/library/constructions/has_sizeof.cpp @@ -233,7 +233,7 @@ class mk_has_sizeof_fn { << "[sizeof]: " << sizeof_name << " : " << sizeof_type << "\n" << sizeof_val << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, sizeof_name, lp_names, sizeof_type, sizeof_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, sizeof_name, lp_names, sizeof_type, sizeof_val, true))); m_env = set_reducible(m_env, sizeof_name, reducible_status::Irreducible, true); m_env = add_protected(m_env, sizeof_name); @@ -263,7 +263,7 @@ class mk_has_sizeof_fn { << "[has_sizeof]: " << has_sizeof_name << " : " << has_sizeof_type << "\n" << has_sizeof_val << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, has_sizeof_name, lp_names, has_sizeof_type, has_sizeof_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, has_sizeof_name, lp_names, has_sizeof_type, has_sizeof_val, true))); m_env = add_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true); m_env = add_protected(m_env, has_sizeof_name); @@ -307,7 +307,7 @@ class mk_has_sizeof_fn { << dsimp_rule_name << " : " << dsimp_rule_type << "\n" << dsimp_rule_val << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, dsimp_rule_name, lp_names, dsimp_rule_type, dsimp_rule_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, dsimp_rule_name, lp_names, dsimp_rule_type, dsimp_rule_val, true))); m_env = mark_rfl_lemma(m_env, dsimp_rule_name); m_env = add_eqn_lemma(m_env, dsimp_rule_name); m_env = add_protected(m_env, dsimp_rule_name); diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp index da2a2ac356..a880d062ec 100644 --- a/src/library/constructions/injective.cpp +++ b/src/library/constructions/injective.cpp @@ -242,8 +242,8 @@ environment mk_injective_arrow(environment const & env, name const & ir_name) { expr inj_arrow_type = tctx.mk_pi(args, tctx.mk_pi(P, mk_arrow(antecedent, P))); expr inj_arrow_val = prove_injective_arrow(env, inj_arrow_type, mk_injective_name(ir_name), d.get_univ_params()); lean_trace(name({"constructions", "injective"}), tout() << inj_arrow_name << " : " << inj_arrow_type << "\n";); - environment new_env = module::add(env, check(env, mk_definition_inferring_trusted(env, inj_arrow_name, - cons(P_lp_name, d.get_univ_params()), inj_arrow_type, inj_arrow_val, true))); + environment new_env = module::add(env, check(env, mk_definition_inferring_meta(env, inj_arrow_name, + cons(P_lp_name, d.get_univ_params()), inj_arrow_type, inj_arrow_val, true))); return new_env; } @@ -286,13 +286,13 @@ environment mk_injective_lemmas(environment const & _env, name const & ind_name, expr inj_type = mk_injective_type(env, ir_name, ir_type, num_params, lp_names); expr inj_val = prove_injective(env, inj_type, ind_name); lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n " << inj_val << "\n";); - env = module::add(env, check(env, mk_definition_inferring_trusted(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val, true))); + env = module::add(env, check(env, mk_definition_inferring_meta(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val, true))); env = mk_injective_arrow(env, ir_name); if (gen_inj_eq && env.find(get_tactic_mk_inj_eq_name())) { name inj_eq_name = mk_injective_eq_name(ir_name); expr inj_eq_type = mk_injective_eq_type(env, ir_name, ir_type, num_params, lp_names); expr inj_eq_value = prove_injective_eq(env, inj_eq_type, inj_eq_name); - env = module::add(env, check(env, mk_definition_inferring_trusted(env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value, true))); + env = module::add(env, check(env, mk_definition_inferring_meta(env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value, true))); } } return env; diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index e5088bf8b1..9186eb84e4 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -122,8 +122,8 @@ 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)); - declaration new_d = mk_definition_inferring_trusted(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, + reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true); return some(add_protected(new_env, no_confusion_type_name)); @@ -232,8 +232,8 @@ environment mk_no_confusion(environment const & env, name const & n) { eq_rec = mk_app(mk_app(eq_rec, rec_type_former, gen, v2, H12), H12); // expr no_confusion_val = Fun(args, eq_rec); - declaration new_d = mk_definition_inferring_trusted(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val, + reducibility_hints::mk_abbreviation()); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible, true); new_env = add_no_confusion(new_env, no_confusion_name); diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 203fa54080..565cbbced3 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -261,8 +261,8 @@ environment mk_projections(environment const & env, name const & n, buffer nparams + i, lvl_params, mtype, mval, proj_args.back()); proj_val = Fun(proj_args, proj_val); } - declaration new_d = mk_definition_inferring_trusted(env, proj_name, lvl_params, proj_type, proj_val, - reducibility_hints::mk_abbreviation()); + declaration new_d = mk_definition_inferring_meta(env, proj_name, lvl_params, proj_type, proj_val, + reducibility_hints::mk_abbreviation()); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true); new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit); diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index 9b2437c7e6..b4aef78aae 100644 --- a/src/library/constructions/rec_on.cpp +++ b/src/library/constructions/rec_on.cpp @@ -56,8 +56,8 @@ environment mk_rec_on(environment const & env, name const & n) { expr rec_on_val = Fun(new_locals, mk_app(rec, locals)); environment new_env = module::add(env, - check(env, mk_definition_inferring_trusted(env, rec_on_name, rec_decl.get_univ_params(), - rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation()))); + check(env, mk_definition_inferring_meta(env, rec_on_name, rec_decl.get_univ_params(), + rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation()))); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, rec_on_name); return add_protected(new_env, rec_on_name); diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp index bced15c2c9..f4d1e210d8 100644 --- a/src/library/equations_compiler/unbounded_rec.cpp +++ b/src/library/equations_compiler/unbounded_rec.cpp @@ -159,8 +159,8 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab, fn = helper.mk_lambda_closure(fn); bool use_self_opt = true; - bool trusted = false; - declaration d = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, trusted); + bool is_meta = true; + declaration d = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, is_meta); env = module::add(env, check(env, d)); expr result_fn = mk_app(mk_constant(fn_name, levels(closure_lvl_params)), closure_params); diff --git a/src/library/export.cpp b/src/library/export.cpp index 61a14a3608..e5417dbfcb 100644 --- a/src/library/export.cpp +++ b/src/library/export.cpp @@ -219,7 +219,7 @@ class exporter { void export_declaration(declaration d) { // do not export meta declarations - if (!d.is_trusted()) return; + if (d.is_meta()) return; if (is_quotient_decl(m_env, d.get_name())) return export_quotient(); diff --git a/src/library/inductive_compiler/add_decl.cpp b/src/library/inductive_compiler/add_decl.cpp index d389b13a9c..3ef784317a 100644 --- a/src/library/inductive_compiler/add_decl.cpp +++ b/src/library/inductive_compiler/add_decl.cpp @@ -17,16 +17,16 @@ environment add_inductive_declaration(environment const & old_env, options const name_map implicit_infer_map, buffer const & lp_names, buffer const & params, buffer const & inds, buffer > const & intro_rules, - bool is_trusted) { + bool is_meta) { name_generator ngen(*g_inductive_compiler_fresh); ginductive_decl decl(old_env, 0, lp_names, params, inds, intro_rules); - environment env = add_inner_inductive_declaration(old_env, ngen, opts, implicit_infer_map, decl, is_trusted); + environment env = add_inner_inductive_declaration(old_env, ngen, opts, implicit_infer_map, decl, is_meta); return env; } environment add_structure_declaration_aux(environment const & old_env, options const &, buffer const & lp_names, buffer const & params, expr const & ind, expr const & intro_rule, - bool is_trusted) { + bool is_meta) { buffer inds; inds.push_back(ind); @@ -37,7 +37,7 @@ environment add_structure_declaration_aux(environment const & old_env, options c ginductive_decl decl(old_env, 0, lp_names, params, inds, intro_rules); environment env = old_env; - if (is_trusted && mlocal_name(ind) != get_has_sizeof_name()) + if (!is_meta && mlocal_name(ind) != get_has_sizeof_name()) env = mk_has_sizeof(env, mlocal_name(ind)); return register_ginductive_decl(env, decl, ginductive_kind::BASIC); diff --git a/src/library/inductive_compiler/add_decl.h b/src/library/inductive_compiler/add_decl.h index 5cc0f9ad1e..3c34746c83 100644 --- a/src/library/inductive_compiler/add_decl.h +++ b/src/library/inductive_compiler/add_decl.h @@ -13,11 +13,11 @@ environment add_inductive_declaration(environment const & env, options const & o name_map implicit_infer_map, buffer const & lp_names, buffer const & params, buffer const & inds, buffer > const & intro_rules, - bool is_trusted); + bool is_meta); environment add_structure_declaration_aux(environment const & env, options const & opts, buffer const & lp_names, buffer const & params, expr const & ind, expr const & intro_rule, - bool is_trusted); + bool is_meta); void initialize_inductive_compiler_add_decl(); void finalize_inductive_compiler_add_decl(); diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index b2819267bb..ef2c0da023 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -70,7 +70,7 @@ class add_basic_inductive_decl_fn { options const & m_opts; name_map const & m_implicit_infer_map; ginductive_decl const & m_decl; - bool m_is_trusted; + bool m_is_meta; void mk_basic_aux_decls() { name ind_name = mlocal_name(m_decl.get_inds()[0]); @@ -110,7 +110,7 @@ class add_basic_inductive_decl_fn { m_env = mk_binduction_on(m_env, ind_name); } - if (m_is_trusted) + if (!m_is_meta) m_env = mk_has_sizeof(m_env, ind_name); } @@ -134,13 +134,13 @@ class add_basic_inductive_decl_fn { lean_trace(name({"inductive_compiler", "basic", "irs"}), tout() << mlocal_name(ir) << " : " << new_ir_type << "\n";); } inductive_decl kdecl(mlocal_name(ind), names(lp_names), params.size(), new_ind_type, to_list(new_intro_rules)); - m_env = module::add_inductive(m_env, kdecl, m_is_trusted); + m_env = module::add_inductive(m_env, kdecl, m_is_meta); } public: add_basic_inductive_decl_fn(environment const & env, options const & opts, name_map implicit_infer_map, - ginductive_decl const & decl, bool is_trusted): - m_env(env), m_opts(opts), m_implicit_infer_map(implicit_infer_map), m_decl(decl), m_is_trusted(is_trusted) {} + ginductive_decl const & decl, bool is_meta): + m_env(env), m_opts(opts), m_implicit_infer_map(implicit_infer_map), m_decl(decl), m_is_meta(is_meta) {} environment operator()() { send_to_kernel(); @@ -150,8 +150,8 @@ public: }; environment add_basic_inductive_decl(environment const & env, options const & opts, name_map implicit_infer_map, - ginductive_decl const & decl, bool is_trusted) { - return add_basic_inductive_decl_fn(env, opts, implicit_infer_map, decl, is_trusted)(); + ginductive_decl const & decl, bool is_meta) { + return add_basic_inductive_decl_fn(env, opts, implicit_infer_map, decl, is_meta)(); } void initialize_inductive_compiler_basic() { diff --git a/src/library/inductive_compiler/basic.h b/src/library/inductive_compiler/basic.h index 2a00f5ea23..4f8b931c5b 100644 --- a/src/library/inductive_compiler/basic.h +++ b/src/library/inductive_compiler/basic.h @@ -12,7 +12,7 @@ Author: Daniel Selsam namespace lean { environment add_basic_inductive_decl(environment const & env, options const & opts, name_map implicit_infer_map, - ginductive_decl const & decl, bool is_trusted); + ginductive_decl const & decl, bool is_meta); void initialize_inductive_compiler_basic(); void finalize_inductive_compiler_basic(); diff --git a/src/library/inductive_compiler/compiler.cpp b/src/library/inductive_compiler/compiler.cpp index bf8a1c9c2c..6eca5d5c3d 100644 --- a/src/library/inductive_compiler/compiler.cpp +++ b/src/library/inductive_compiler/compiler.cpp @@ -19,20 +19,20 @@ Author: Daniel Selsam namespace lean { environment add_inner_inductive_declaration(environment const & env, name_generator & ngen, options const & opts, name_map implicit_infer_map, - ginductive_decl & decl, bool is_trusted) { + ginductive_decl & decl, bool is_meta) { lean_assert(decl.get_inds().size() == decl.get_intro_rules().size()); - if (is_trusted) { + if (!is_meta) { if (optional new_env = add_nested_inductive_decl(env, ngen, opts, implicit_infer_map, decl, - is_trusted)) { + is_meta)) { return register_ginductive_decl(*new_env, decl, ginductive_kind::NESTED); } } if (decl.is_mutual()) { - return register_ginductive_decl(add_mutual_inductive_decl(env, ngen, opts, implicit_infer_map, decl, is_trusted), + return register_ginductive_decl(add_mutual_inductive_decl(env, ngen, opts, implicit_infer_map, decl, is_meta), decl, ginductive_kind::MUTUAL); } else { lean_assert(!decl.is_mutual()); - return register_ginductive_decl(add_basic_inductive_decl(env, opts, implicit_infer_map, decl, is_trusted), + return register_ginductive_decl(add_basic_inductive_decl(env, opts, implicit_infer_map, decl, is_meta), decl, ginductive_kind::BASIC); } } diff --git a/src/library/inductive_compiler/compiler.h b/src/library/inductive_compiler/compiler.h index 5948acbfd3..42c02dc4e6 100644 --- a/src/library/inductive_compiler/compiler.h +++ b/src/library/inductive_compiler/compiler.h @@ -13,7 +13,7 @@ Author: Daniel Selsam namespace lean { environment add_inner_inductive_declaration(environment const & env, name_generator & ngen, options const & opts, name_map implicit_infer_map, - ginductive_decl & decl, bool is_trusted); + ginductive_decl & decl, bool is_meta); void initialize_inductive_compiler(); void finalize_inductive_compiler(); diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp index ad5e4c36c1..82099fb37f 100644 --- a/src/library/inductive_compiler/mutual.cpp +++ b/src/library/inductive_compiler/mutual.cpp @@ -38,7 +38,7 @@ class add_mutual_inductive_decl_fn { options const & m_opts; name_map m_implicit_infer_map; ginductive_decl const & m_mut_decl; - bool m_is_trusted; + bool m_is_meta; ginductive_decl m_basic_decl; name m_basic_ind_name; @@ -293,7 +293,7 @@ class add_mutual_inductive_decl_fn { << mlocal_name(ind) << " : " << new_ind_type << " :=\n " << new_ind_val << "\n";); lean_assert(!has_local(new_ind_type)); lean_assert(!has_local(new_ind_val)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, mlocal_name(ind), names(m_mut_decl.get_lp_names()), new_ind_type, new_ind_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, mlocal_name(ind), names(m_mut_decl.get_lp_names()), new_ind_type, new_ind_val, true))); m_tctx.set_env(m_env); } } @@ -347,7 +347,7 @@ class add_mutual_inductive_decl_fn { << sizeof_name << " : " << sizeof_type << " :=\n " << sizeof_val << "\n";); lean_assert(!has_local(sizeof_type)); lean_assert(!has_local(sizeof_val)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, sizeof_name, names(m_mut_decl.get_lp_names()), sizeof_type, sizeof_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, sizeof_name, names(m_mut_decl.get_lp_names()), sizeof_type, sizeof_val, true))); m_env = add_protected(m_env, sizeof_name); m_tctx.set_env(m_env); @@ -368,7 +368,7 @@ class add_mutual_inductive_decl_fn { << has_sizeof_name << " : " << has_sizeof_type << " :=\n " << has_sizeof_val << "\n";); lean_assert(!has_local(has_sizeof_type)); lean_assert(!has_local(has_sizeof_val)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, has_sizeof_name, names(m_mut_decl.get_lp_names()), has_sizeof_type, has_sizeof_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, has_sizeof_name, names(m_mut_decl.get_lp_names()), has_sizeof_type, has_sizeof_val, true))); m_env = add_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true); m_env = add_protected(m_env, sizeof_name); m_tctx.set_env(m_env); @@ -421,7 +421,7 @@ class add_mutual_inductive_decl_fn { lean_trace(name({"inductive_compiler", "mutual", "sizeof"}), tout() << dsimp_rule_name << " : " << dsimp_rule_type << " :=\n " << dsimp_rule_val << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, dsimp_rule_name, names(m_mut_decl.get_lp_names()), dsimp_rule_type, dsimp_rule_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, dsimp_rule_name, names(m_mut_decl.get_lp_names()), dsimp_rule_type, dsimp_rule_val, true))); m_env = mark_rfl_lemma(m_env, dsimp_rule_name); m_env = add_eqn_lemma(m_env, dsimp_rule_name); m_env = add_protected(m_env, dsimp_rule_name); @@ -468,14 +468,14 @@ class add_mutual_inductive_decl_fn { expr inj_and_type = mk_injective_type(m_env, ir_name, ir_type, num_params, lp_names); expr inj_and_val = mk_constant(mk_injective_name(mlocal_name(m_basic_decl.get_intro_rule(0, basic_ir_idx))), m_mut_decl.get_levels()); lean_trace(name({"inductive_compiler", "mutual", "injective"}), tout() << mk_injective_name(ir_name) << " : " << inj_and_type << " :=\n " << inj_and_val << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, mk_injective_name(ir_name), lp_names, inj_and_type, inj_and_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, mk_injective_name(ir_name), lp_names, inj_and_type, inj_and_val, true))); m_env = mk_injective_arrow(m_env, ir_name); if (m_env.find(get_tactic_mk_inj_eq_name())) { name inj_eq_name = mk_injective_eq_name(ir_name); expr inj_eq_type = mk_injective_eq_type(m_env, ir_name, ir_type, num_params, lp_names); expr inj_eq_value = prove_injective_eq(m_env, inj_eq_type, inj_eq_name); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value, true))); } m_tctx.set_env(m_env); @@ -499,7 +499,7 @@ class add_mutual_inductive_decl_fn { lean_assert(!has_local(new_ir_val)); lean_trace(name({"inductive_compiler", "mutual", "ir"}), tout() << mlocal_name(ir) << " : " << new_ir_type << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, mlocal_name(ir), names(m_mut_decl.get_lp_names()), new_ir_type, new_ir_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, mlocal_name(ir), names(m_mut_decl.get_lp_names()), new_ir_type, new_ir_val, true))); m_env = set_pattern_attribute(m_env, mlocal_name(ir)); m_tctx.set_env(m_env); basic_ir_idx++; @@ -779,7 +779,7 @@ class add_mutual_inductive_decl_fn { lean_assert(!has_local(rec_type)); lean_assert(!has_local(rec_val)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, get_dep_recursor(m_env, mlocal_name(ind)), rec_lp_names, rec_type, rec_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, get_dep_recursor(m_env, mlocal_name(ind)), rec_lp_names, rec_type, rec_val, true))); } void define_cases_on(name const & rec_name, level_param_names const & rec_lp_names, unsigned ind_idx) { @@ -853,7 +853,7 @@ class add_mutual_inductive_decl_fn { lean_assert(!has_local(cases_on_type)); lean_assert(!has_local(cases_on_val)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, name(mlocal_name(ind), "cases_on"), rec_lp_names, cases_on_type, cases_on_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, name(mlocal_name(ind), "cases_on"), rec_lp_names, cases_on_type, cases_on_val, true))); } void define_recursors() { @@ -876,9 +876,9 @@ class add_mutual_inductive_decl_fn { public: add_mutual_inductive_decl_fn(environment const & env, name_generator & ngen, options const & opts, name_map const & implicit_infer_map, ginductive_decl const & mut_decl, - bool is_trusted): + bool is_meta): m_env(env), m_ngen(ngen), m_opts(opts), m_implicit_infer_map(implicit_infer_map), - m_mut_decl(mut_decl), m_is_trusted(is_trusted), + m_mut_decl(mut_decl), m_is_meta(is_meta), m_basic_decl(m_mut_decl.get_nest_depth() + 1, m_mut_decl.get_lp_names(), m_mut_decl.get_params(), m_mut_decl.get_ir_offsets()), m_tctx(env, opts) {} @@ -895,7 +895,7 @@ public: compute_idx_to_ir_range(); try { - m_env = add_inner_inductive_declaration(m_env, m_ngen, m_opts, m_implicit_infer_map, m_basic_decl, m_is_trusted); + m_env = add_inner_inductive_declaration(m_env, m_ngen, m_opts, m_implicit_infer_map, m_basic_decl, m_is_meta); } catch (exception & ex) { throw nested_exception(sstream() << "mutually inductive types compiled to invalid basic inductive type", ex); } @@ -912,8 +912,8 @@ public: environment add_mutual_inductive_decl(environment const & env, name_generator & ngen, options const & opts, name_map const & implicit_infer_map, - ginductive_decl & mut_decl, bool is_trusted) { - return add_mutual_inductive_decl_fn(env, ngen, opts, implicit_infer_map, mut_decl, is_trusted)(); + ginductive_decl & mut_decl, bool is_meta) { + return add_mutual_inductive_decl_fn(env, ngen, opts, implicit_infer_map, mut_decl, is_meta)(); } void initialize_inductive_compiler_mutual() { diff --git a/src/library/inductive_compiler/mutual.h b/src/library/inductive_compiler/mutual.h index efb4c6b01d..f05162aa26 100644 --- a/src/library/inductive_compiler/mutual.h +++ b/src/library/inductive_compiler/mutual.h @@ -12,7 +12,7 @@ Author: Daniel Selsam namespace lean { environment add_mutual_inductive_decl(environment const & env, name_generator & ngen, options const & opts, name_map const & implicit_infer_map, - ginductive_decl & mut_decl, bool is_trusted); + ginductive_decl & mut_decl, bool is_meta); void initialize_inductive_compiler_mutual(); void finalize_inductive_compiler_mutual(); diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 14b17116cc..ea8f53a012 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -87,7 +87,7 @@ class add_nested_inductive_decl_fn { name_map m_implicit_infer_map; // Note(dhs): m_nested_decl is morally const, but we make it non-const to pass around sizeof_lemmas ginductive_decl & m_nested_decl; - bool m_is_trusted; + bool m_is_meta; ginductive_decl m_inner_decl; type_context_old m_tctx; @@ -277,7 +277,7 @@ class add_nested_inductive_decl_fn { void add_inner_decl() { try { - m_env = add_inner_inductive_declaration(m_env, m_ngen, m_opts, m_implicit_infer_map, m_inner_decl, m_is_trusted); + m_env = add_inner_inductive_declaration(m_env, m_ngen, m_opts, m_implicit_infer_map, m_inner_decl, m_is_meta); } catch (exception & ex) { throw nested_exception(sstream() << "nested inductive type compiled to invalid inductive type", ex); } @@ -370,7 +370,7 @@ class add_nested_inductive_decl_fn { void define_theorem(name const & n, expr const & ty, expr const & val) { assert_no_locals(n, ty); assert_no_locals(n, val); - declaration d = mk_definition_inferring_trusted(m_env, n, names(m_nested_decl.get_lp_names()), ty, val, true); + declaration d = mk_definition_inferring_meta(m_env, n, names(m_nested_decl.get_lp_names()), ty, val, true); try { m_env = module::add(m_env, check(m_env, d)); lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << "\n";); @@ -388,7 +388,7 @@ class add_nested_inductive_decl_fn { void define(name const & n, expr const & ty, expr const & val, level_param_names const & lp_names) { assert_no_locals(n, ty); assert_no_locals(n, val); - declaration d = mk_definition_inferring_trusted(m_env, n, lp_names, ty, val, true); + declaration d = mk_definition_inferring_meta(m_env, n, lp_names, ty, val, true); try { m_env = module::add(m_env, check(m_env, d)); lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << " :=\n " << val << "\n";); @@ -817,7 +817,7 @@ class add_nested_inductive_decl_fn { << has_sizeof_name << " : " << has_sizeof_type << " :=\n " << has_sizeof_val << "\n";); lean_assert(!has_local(has_sizeof_type)); lean_assert(!has_local(has_sizeof_val)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, has_sizeof_name, names(m_nested_decl.get_lp_names()), has_sizeof_type, has_sizeof_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, has_sizeof_name, names(m_nested_decl.get_lp_names()), has_sizeof_type, has_sizeof_val, true))); m_env = add_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true); m_env = add_protected(m_env, sizeof_name); m_tctx.set_env(m_env); @@ -897,7 +897,7 @@ class add_nested_inductive_decl_fn { lean_trace(name({"inductive_compiler", "nested", "sizeof"}), tout() << sizeof_spec_name << " : " << sizeof_spec_type << " :=\n " << sizeof_spec_val << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, sizeof_spec_name, names(m_nested_decl.get_lp_names()), sizeof_spec_type, sizeof_spec_val, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, sizeof_spec_name, names(m_nested_decl.get_lp_names()), sizeof_spec_type, sizeof_spec_val, true))); lean_trace(name({"inductive_compiler", "nested", "sizeof"}), tout() << "[defined]: " << sizeof_spec_name << "\n";); m_env = add_eqn_lemma(m_env, sizeof_spec_name); @@ -1667,7 +1667,7 @@ class add_nested_inductive_decl_fn { args.push_back(to_obj(mk_primitive_name(fn_type::UNPACK_PACK))); args.push_back(to_obj(mk_primitive_name(fn_type::UNPACK))); expr proof = prove_pack_injective(lemma_name, goal, mk_primitive_name(fn_type::UNPACK), mk_primitive_name(fn_type::UNPACK_PACK)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof, true))); m_tctx.set_env(m_env); m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); } @@ -1721,7 +1721,7 @@ class add_nested_inductive_decl_fn { args.push_back(to_obj(mk_nested_name(fn_type::UNPACK_PACK, nest_idx))); args.push_back(to_obj(mk_nested_name(fn_type::UNPACK, nest_idx))); expr proof = prove_pack_injective(lemma_name, goal, mk_nested_name(fn_type::UNPACK, nest_idx), mk_nested_name(fn_type::UNPACK_PACK, nest_idx)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof, true))); m_tctx.set_env(m_env); m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); } @@ -1818,7 +1818,7 @@ class add_nested_inductive_decl_fn { args.push_back(to_obj(mk_pi_name(fn_type::UNPACK_PACK))); args.push_back(to_obj(mk_pi_name(fn_type::UNPACK))); expr proof = prove_pack_injective(lemma_name, goal, mk_pi_name(fn_type::UNPACK), mk_pi_name(fn_type::UNPACK_PACK)); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof, true))); m_tctx.set_env(m_env); m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); } @@ -2291,13 +2291,13 @@ class add_nested_inductive_decl_fn { expr inj_val = prove_nested_injective(inj_type, m_inj_lemmas, inj_arrow_name); m_env = module::add(m_env, check(m_env, - mk_definition_inferring_trusted(m_env, inj_name, lp_names, inj_type, inj_val, true))); + mk_definition_inferring_meta(m_env, inj_name, lp_names, inj_type, inj_val, true))); m_env = mk_injective_arrow(m_env, ir_name); if (m_env.find(get_tactic_mk_inj_eq_name())) { name inj_eq_name = mk_injective_eq_name(ir_name); expr inj_eq_type = mk_injective_eq_type(m_env, ir_name, ir_type, num_params, lp_names); expr inj_eq_value = prove_injective_eq(m_env, inj_eq_type, inj_eq_name); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value, true))); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value, true))); } } } @@ -2307,9 +2307,9 @@ class add_nested_inductive_decl_fn { public: add_nested_inductive_decl_fn(environment const & env, name_generator & ngen, options const & opts, name_map const & implicit_infer_map, - ginductive_decl & nested_decl, bool is_trusted): + ginductive_decl & nested_decl, bool is_meta): m_env(env), m_ngen(ngen), m_opts(opts), m_implicit_infer_map(implicit_infer_map), - m_nested_decl(nested_decl), m_is_trusted(is_trusted), + m_nested_decl(nested_decl), m_is_meta(is_meta), m_inner_decl(m_nested_decl.get_nest_depth() + 1, m_nested_decl.get_lp_names(), m_nested_decl.get_params(), m_nested_decl.get_num_indices(), m_nested_decl.get_ir_offsets()), m_tctx(env, opts, transparency_mode::Semireducible) { } @@ -2347,8 +2347,8 @@ public: optional add_nested_inductive_decl(environment const & env, name_generator & ngen, options const & opts, name_map const & implicit_infer_map, - ginductive_decl & decl, bool is_trusted) { - return add_nested_inductive_decl_fn(env, ngen, opts, implicit_infer_map, decl, is_trusted)(); + ginductive_decl & decl, bool is_meta) { + return add_nested_inductive_decl_fn(env, ngen, opts, implicit_infer_map, decl, is_meta)(); } void initialize_inductive_compiler_nested() { diff --git a/src/library/inductive_compiler/nested.h b/src/library/inductive_compiler/nested.h index 49ea22ad0f..de3d655ae1 100644 --- a/src/library/inductive_compiler/nested.h +++ b/src/library/inductive_compiler/nested.h @@ -12,7 +12,7 @@ Author: Daniel Selsam namespace lean { optional add_nested_inductive_decl(environment const & env, name_generator & ngen, options const & opts, name_map const & implicit_infer_map, - ginductive_decl & decl, bool is_trusted); + ginductive_decl & decl, bool is_meta); void initialize_inductive_compiler_nested(); void finalize_inductive_compiler_nested(); diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 678168cdd8..030d9a130c 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -231,7 +231,7 @@ serializer & operator<<(serializer & s, declaration const & d) { k |= 1; if (d.is_theorem() || d.is_axiom()) k |= 2; - if (d.is_trusted()) + if (d.is_meta()) k |= 4; s << k << d.get_name() << d.get_univ_params() << d.get_type(); if (d.is_definition()) { @@ -246,7 +246,7 @@ declaration read_declaration(deserializer & d) { char k = d.read_char(); bool has_value = (k & 1) != 0; bool is_th_ax = (k & 2) != 0; - bool is_trusted = (k & 4) != 0; + bool is_meta = (k & 4) != 0; name n = read_name(d); level_param_names ps = read_level_params(d); expr t = read_expr(d); @@ -256,13 +256,13 @@ declaration read_declaration(deserializer & d) { return mk_theorem(n, ps, t, v); } else { reducibility_hints hints = read_hints(d); - return mk_definition(n, ps, t, v, hints, is_trusted); + return mk_definition(n, ps, t, v, hints, is_meta); } } else { if (is_th_ax) return mk_axiom(n, ps, t); else - return mk_constant_assumption(n, ps, t, is_trusted); + return mk_constant_assumption(n, ps, t, is_meta); } } @@ -308,7 +308,7 @@ inductive_decl read_inductive_decl(deserializer & d) { serializer & operator<<(serializer & s, certified_inductive_decl const & d) { s << d.get_num_ACe() << d.elim_prop_only() << d.has_dep_elim() << d.get_elim_levels() << d.get_elim_type() << d.get_decl() - << d.is_K_target() << d.get_num_indices() << d.is_trusted(); + << d.is_K_target() << d.get_num_indices() << d.is_meta(); write_list(s, d.get_comp_rules()); return s; } @@ -324,10 +324,10 @@ public: inductive_decl decl = read_inductive_decl(d); bool K = d.read_bool(); unsigned nind = d.read_unsigned(); - bool is_trusted = d.read_bool(); + bool is_meta = d.read_bool(); auto rs = read_list(d, read_comp_rule); return certified_inductive_decl(nACe, elim_prop, dep_elim, ls, elim_type, decl, - K, nind, rs, is_trusted); + K, nind, rs, is_meta); } }; diff --git a/src/library/module.cpp b/src/library/module.cpp index 5137e8bf9c..1d42e7f04d 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -373,7 +373,7 @@ struct inductive_modification : public modification { d.m_intro_rules = map(d.m_intro_rules, [&](inductive::intro_rule const & r) { return unfold_untrusted_macros(env, r); }); - env = add_inductive(env, d, m_decl.is_trusted()).first; + env = add_inductive(env, d, m_decl.is_meta()).first; } else { env = m_decl.add(env); } @@ -464,8 +464,8 @@ using inductive::certified_inductive_decl; environment add_inductive(environment env, inductive::inductive_decl const & decl, - bool is_trusted) { - pair r = inductive::add_inductive(env, decl, is_trusted); + bool is_meta) { + pair r = inductive::add_inductive(env, decl, is_meta); environment new_env = r.first; certified_inductive_decl cidecl = r.second; module_ext ext = get_extension(env); diff --git a/src/library/module.h b/src/library/module.h index 3c00b2f4af..801a03f8d3 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -149,7 +149,7 @@ bool is_definition(environment const & env, name const & n); /** \brief Add the given inductive declaration to the environment, and mark it to be exported. */ environment add_inductive(environment env, inductive::inductive_decl const & decl, - bool is_trusted); + bool is_meta); /** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */ environment declare_quotient(environment const & env); diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 57443d5ed0..c34311573a 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -80,7 +80,7 @@ static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, n if (ext.m_noncomputable.contains(n)) return true; declaration const & d = env.get(n); - if (!d.is_trusted()) { + if (d.is_meta()) { return false; /* ignore nontrusted definitions */ } else if (d.is_axiom() && !tc.is_prop(d.get_type())) { return true; diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 2f50756807..d35fcbf7d9 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -796,9 +796,9 @@ format tactic_state::pp() const { expr type = ctx.infer(code); environment new_env = ctx.env(); bool use_conv_opt = true; - bool is_trusted = false; + bool is_meta = true; name pp_name("_pp_tactic_state"); - auto cd = check(new_env, mk_definition(new_env, pp_name, {}, type, code, use_conv_opt, is_trusted)); + auto cd = check(new_env, mk_definition(new_env, pp_name, {}, type, code, use_conv_opt, is_meta)); new_env = new_env.add(cd); new_env = vm_compile(new_env, new_env.get(pp_name)); vm_state S(new_env, get_options()); diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp index e003a56273..7a1b7ab76e 100644 --- a/src/library/unfold_macros.cpp +++ b/src/library/unfold_macros.cpp @@ -69,15 +69,9 @@ expr unfold_all_macros(environment const & env, expr const & e) { return unfold_untrusted_macros(env, e, {}); } -static bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) { -#if defined(LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL) - if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) return false; -#endif - if (!d.is_trusted()) - return false; - if (contains_untrusted_macro(trust_lvl, d.get_type())) - return true; - return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(trust_lvl, d.get_value()); +static bool contains_untrusted_macro(unsigned /* trust_lvl */, declaration const & /* d */) { + /* TODO(Leo): macros will be deleted */ + return false; } declaration unfold_untrusted_macros(environment const & env, declaration const & d, optional const & trust_lvl) { @@ -89,7 +83,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.get_hints(), d.is_trusted()); + d.get_hints(), d.is_meta()); } 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 f0d7eda218..f11fea3bce 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.get_hints(), d.is_trusted()); + return mk_definition(d.get_name(), _ps, _type, _value, d.get_hints(), d.is_meta()); } } diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index 5959173e0f..07fecce3dd 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -236,10 +236,10 @@ environment interaction_monad::evaluator::compile(name const & interactio expr interaction_type = m_ctx.infer(interaction); environment new_env = m_ctx.env(); bool use_conv_opt = true; - bool is_trusted = false; + bool is_meta = true; auto cd = check(new_env, mk_definition(new_env, interaction_name, {}, interaction_type, interaction, use_conv_opt, - is_trusted)); + is_meta)); new_env = new_env.add(cd); if (provider) { if (auto pos = provider->get_pos_info(interaction)) diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp index b4facc56a2..5bf7500a70 100644 --- a/src/library/vm/vm_declaration.cpp +++ b/src/library/vm/vm_declaration.cpp @@ -60,16 +60,16 @@ vm_obj to_obj(declaration const & n) { } vm_obj declaration_defn(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value, - vm_obj const & hints, vm_obj const & trusted) { - return to_obj(mk_definition(to_name(n), to_names(ls), to_expr(type), to_expr(value), to_reducibility_hints(hints), to_bool(trusted))); + vm_obj const & hints, vm_obj const & meta) { + return to_obj(mk_definition(to_name(n), to_names(ls), to_expr(type), to_expr(value), to_reducibility_hints(hints), to_bool(meta))); } vm_obj declaration_thm(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value) { return to_obj(mk_theorem(to_name(n), to_names(ls), to_expr(type), to_expr(value))); } -vm_obj declaration_cnst(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & trusted) { - return to_obj(mk_constant_assumption(to_name(n), to_names(ls), to_expr(type), to_bool(trusted))); +vm_obj declaration_cnst(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & meta) { + return to_obj(mk_constant_assumption(to_name(n), to_names(ls), to_expr(type), to_bool(meta))); } vm_obj declaration_ax(vm_obj const & n, vm_obj const & ls, vm_obj const & type) { @@ -89,11 +89,11 @@ unsigned declaration_cases_on(vm_obj const & o, buffer & data) { } else if (d.is_definition()) { data.push_back(to_obj(d.get_value())); data.push_back(to_obj(d.get_hints())); - data.push_back(mk_vm_bool(d.is_trusted())); + data.push_back(mk_vm_bool(d.is_meta())); return 0; } else { lean_assert(d.is_constant_assumption()); - data.push_back(mk_vm_bool(d.is_trusted())); + data.push_back(mk_vm_bool(d.is_meta())); return 2; } } diff --git a/src/shell/leandoc.cpp b/src/shell/leandoc.cpp index 50a0822624..e8b8d30330 100644 --- a/src/shell/leandoc.cpp +++ b/src/shell/leandoc.cpp @@ -67,7 +67,7 @@ static void print_constant(std::ostream & out, environment const & env, formatte format r; if (is_protected(env, d.get_name())) add_string(r, "protected"); - if (!d.is_trusted()) + if (d.is_meta()) add_string(r, "meta"); if (d.is_definition() && is_marked_noncomputable(env, d.get_name())) add_string(r, "noncomputable");