From f3e99286bbcf588f7405e04f10724e96a3be0aab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Aug 2018 12:09:57 -0700 Subject: [PATCH] chore(kernel): remove `certified_declaration` --- src/frontends/lean/decl_cmds.cpp | 2 +- src/frontends/lean/definition_cmds.cpp | 27 +------ src/frontends/lean/structure_cmd.cpp | 6 +- src/frontends/lean/util.cpp | 3 +- src/kernel/environment.cpp | 94 ++++++++++++++++++++-- src/kernel/environment.h | 31 ++----- src/kernel/inductive/inductive.cpp | 16 ++-- src/kernel/quot.cpp | 3 +- src/kernel/type_checker.cpp | 86 -------------------- src/kernel/type_checker.h | 8 -- src/library/aux_definition.cpp | 2 +- src/library/compiler/elim_recursors.cpp | 3 +- src/library/constructions/brec_on.cpp | 4 +- src/library/constructions/cases_on.cpp | 2 +- src/library/constructions/drec.cpp | 2 +- src/library/constructions/has_sizeof.cpp | 6 +- src/library/constructions/injective.cpp | 8 +- src/library/constructions/no_confusion.cpp | 4 +- src/library/constructions/projection.cpp | 2 +- src/library/constructions/rec_on.cpp | 4 +- src/library/derive_attribute.cpp | 6 +- src/library/equations_compiler/util.cpp | 3 +- src/library/inductive_compiler/mutual.cpp | 12 +-- src/library/inductive_compiler/nested.cpp | 17 ++-- src/library/module.cpp | 25 ++---- src/library/module.h | 2 +- src/library/tactic/eval.cpp | 3 +- src/library/tactic/tactic_state.cpp | 5 +- src/library/vm/interaction_state_imp.h | 4 +- 29 files changed, 156 insertions(+), 234 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 147023e514..e27c9c3e7e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -122,7 +122,7 @@ static environment declare_var(parser & p, environment env, expr new_type = Pi(new_params, type); bool is_meta = meta.m_modifiers.m_is_meta; - env = module::add(env, check(env, mk_axiom(full_n, ls, new_type, is_meta))); + env = module::add(env, mk_axiom(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 f5c9c4007a..e51505bbf0 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -171,25 +171,6 @@ static void finalize_definition(elaborator & elab, buffer const & params, lp_names.append(implicit_lp_names); } -static certified_declaration check(parser & p, environment const & env, name const & c_name, declaration const & d, pos_info const & pos) { - try { - time_task _("type checking", p.mk_message(pos, INFORMATION), p.get_options(), c_name); - return ::lean::check(env, d); - } catch (kernel_exception & ex) { - unsigned i = get_pp_indent(p.get_options()); - auto pp_fn = ::lean::mk_pp_ctx(env, p.get_options(), metavar_context(), local_context()); - format msg = format("kernel failed to type check declaration '") + format(c_name) + format("' ") + - format("this is usually due to a buggy tactic or a bug in the builtin elaborator"); - msg += line() + format("elaborated type:"); - msg += nest(i, line() + pp_fn(d.get_type())); - if (d.has_value()) { - msg += line() + format("elaborated value:"); - msg += nest(i, line() + pp_fn(d.get_value())); - } - throw nested_exception(msg, std::current_exception()); - } -} - static bool check_noncomputable(bool ignore_noncomputable, environment const & env, name const & c_name, name const & c_real_name, bool is_noncomputable, std::string const & file_name, pos_info const & pos) { if (ignore_noncomputable) @@ -249,8 +230,7 @@ declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buff 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_meta) : mk_definition(new_env, c_real_name, names(lp_names), type, *val, is_meta))); - auto cdef = check(p, new_env, c_name, def, pos); - new_env = module::add(new_env, cdef); + new_env = module::add(new_env, def); check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, meta.m_modifiers.m_is_noncomputable, p.get_file_name(), pos); @@ -427,7 +407,7 @@ static environment copy_equation_lemmas(environment const & env, buffer co new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args); new_eqn_value = locals.mk_lambda(new_eqn_value); declaration new_decl = mk_theorem(new_eqn_name, lps, new_eqn_type, new_eqn_value); - new_env = module::add(new_env, check(new_env, new_decl)); + new_env = module::add(new_env, new_decl); if (is_rfl_lemma(env, eqn_name)) new_env = mark_rfl_lemma(new_env, new_eqn_name); new_env = add_eqn_lemma(new_env, new_eqn_name); @@ -693,8 +673,7 @@ static void check_example(environment const & decl_env, options const & opts, 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, is_meta); - auto cdef = check(new_env, def); - new_env = module::add(new_env, cdef); + new_env = module::add(new_env, def); check_noncomputable(noncomputable_theory, new_env, decl_name, def.get_name(), modifiers.m_is_noncomputable, pos_provider.get_file_name(), pos_provider.get_some_pos()); } catch (throwable & ex) { diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index bdd4f83e01..ae49c35ebb 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -1153,7 +1153,7 @@ struct structure_cmd_fn { level_param_names decl_lvls = to_level_param_names(used_univs); 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)); + m_env = module::add(m_env, new_decl); if (!m_meta_info.m_modifiers.m_is_meta) m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(), is_private(), decl_name, decl_prv_name, args.size()); m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true); @@ -1167,7 +1167,7 @@ struct structure_cmd_fn { 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)); + m_env = module::add(m_env, new_decl); m_env = set_reducible(m_env, n, reducible_status::Reducible, true); add_alias(n); } @@ -1259,7 +1259,7 @@ struct structure_cmd_fn { name coercion_name = coercion_names[i]; declaration coercion_decl = mk_definition_inferring_meta(m_env, coercion_name, lnames, coercion_type, coercion_value); - m_env = module::add(m_env, check(m_env, coercion_decl)); + m_env = module::add(m_env, coercion_decl); add_alias(coercion_name); m_env = vm_compile(m_env, m_env.get(coercion_name)); if (!m_private_parents[i]) { diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index bbaa6f9ccc..7bc5ea5d5c 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -479,8 +479,7 @@ 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 is_meta = true; - auto cd = check(new_env, mk_definition(new_env, n, ls, type, e, is_meta)); - new_env = new_env.add(cd); + new_env = new_env.add(mk_definition(new_env, n, ls, type, e, is_meta)); 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/environment.cpp b/src/kernel/environment.cpp index a44b3cef54..b1e9b1cbe7 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #include #include -#include +#include "runtime/sstream.h" #include "runtime/thread.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" @@ -63,11 +63,89 @@ environment environment::add_quot() const { return new_env; } -environment environment::add(certified_declaration const & d) const { - name const & n = d.get_declaration().get_name(); - if (find(n)) - throw already_declared_exception(*this, n); - return environment(*this, insert(m_declarations, n, d.get_declaration())); +static void check_no_metavar(environment const & env, name const & n, expr const & e) { + if (has_metavar(e)) + throw declaration_has_metavars_exception(env, n, e); +} + +static void check_no_fvar(environment const & env, name const & n, expr const & e) { + if (has_fvar(e)) + throw declaration_has_free_vars_exception(env, n, e); +} + +void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e) { + check_no_metavar(env, n, e); + check_no_fvar(env, n, e); +} + +static void check_name(environment const & env, name const & n) { + if (env.find(n)) + throw already_declared_exception(env, n); +} + +static void check_duplicated_univ_params(environment const & env, declaration const & d) { + level_param_names ls = d.get_univ_params(); + while (!is_nil(ls)) { + auto const & p = head(ls); + ls = tail(ls); + if (std::find(ls.begin(), ls.end(), p) != ls.end()) { + throw kernel_exception(env, sstream() << "failed to add declaration to environment, " + << "duplicate universe level parameter: '" + << p << "'"); + } + } +} + +static void check_definition_value(environment const & env, declaration const & d, type_checker & checker) { + check_no_metavar_no_fvar(env, d.get_name(), d.get_value()); + expr val_type = checker.check(d.get_value(), d.get_univ_params()); + if (!checker.is_def_eq(val_type, d.get_type())) { + throw definition_type_mismatch_exception(env, d, val_type); + } +} + +static void check_definition_value(environment const & env, declaration const & d) { + bool memoize = true; bool non_meta_only = !d.is_meta(); + type_checker checker(env, memoize, non_meta_only); + if (d.has_value()) { + check_definition_value(env, d, checker); + } +} + +static void check_declaration_type(environment const & env, declaration const & d, type_checker & checker) { + check_no_metavar_no_fvar(env, d.get_name(), d.get_type()); + check_duplicated_univ_params(env, d); + expr sort = checker.check(d.get_type(), d.get_univ_params()); + checker.ensure_sort(sort, d.get_type()); +} + +static void check_declaration_type(environment const & env, declaration const & d) { + bool memoize = true; bool non_meta_only = !d.is_meta(); + type_checker checker(env, memoize, non_meta_only); + check_declaration_type(env, d, checker); +} + +environment environment::add_defn_thm_axiom(declaration const & d, bool check) const { + if (check) { + bool memoize = true; bool non_meta_only = !d.is_meta(); + check_name(*this, d.get_name()); + type_checker checker(*this, memoize, non_meta_only); + check_declaration_type(*this, d, checker); + if (d.has_value()) { + check_definition_value(*this, d, checker); + } + } + return environment(*this, insert(m_declarations, d.get_name(), d)); +} + +environment environment::add(declaration const & d, bool check) const { + switch (d.kind()) { + case declaration_kind::Axiom: case declaration_kind::Definition: case declaration_kind::Theorem: + return add_defn_thm_axiom(d, check); + default: + // NOT IMPLEMENTED YET. + lean_unreachable(); + } } environment environment::add_meta(buffer const & ds, bool check) const { @@ -77,13 +155,13 @@ environment environment::add_meta(buffer const & ds, bool check) co /* Check declarations header, and add them to new_env.m_declarations */ for (declaration const & d : ds) { if (check) - check_decl_type(new_env, d); + check_declaration_type(new_env, d); new_env.m_declarations.insert(d.get_name(), d); } /* Check actual definitions */ if (check) { for (declaration const & d : ds) { - check_decl_value(new_env, d); + check_definition_value(new_env, d); } } return new_env; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 1966a387eb..85f111f01f 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -77,6 +77,8 @@ class environment { m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_declarations(ds), m_extensions(env.m_extensions) {} environment(environment const & env, extensions const & exts): m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_declarations(env.m_declarations), m_extensions(exts) {} + + environment add_defn_thm_axiom(declaration const & d, bool check) const; public: environment(unsigned trust_lvl = 0); environment(unsigned trust_lvl, std::unique_ptr ext); @@ -100,11 +102,8 @@ public: /** \brief Return declaration with name \c n. Throws and exception if declaration does not exist in this environment. */ declaration get(name const & n) const; - /** \brief Extends the current environment with the given (certified) declaration - This method throws an exception if: - - The declaration was certified in an environment which is not an ancestor of this one. - - The environment already contains a declaration with the given name. */ - environment add(certified_declaration const & d) const; + /** \brief Extends the current environment with the given declaration */ + environment add(declaration const & d, bool check = true) const; /** \brief Add a sequence of (possibly mutually recursive) meta declarations. The type checking occurs in two phases: @@ -152,26 +151,8 @@ public: } }; +void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e); + void initialize_environment(); void finalize_environment(); - -class name_generator; - -/** \brief A certified declaration is one that has been type checked. - Only the type_checker class can create certified declarations. */ -class certified_declaration { - friend class certify_unchecked; - friend certified_declaration check(environment const & env, declaration const & d); - declaration m_declaration; - certified_declaration(declaration const & d):m_declaration(d) {} -public: - /** \brief Return the id of the environment that was used to type check this declaration. */ - declaration const & get_declaration() const { return m_declaration; } - /** \brief Certifies a declaration without type-checking. - - \remark This method throws an excetion if trust_lvl() == 0 - It is only used when importing pre-compiled .olean files and for inductive definitions, and trust_lvl() > 0. */ - static certified_declaration certify(environment const & env, declaration const & d); - static certified_declaration certify_or_check(environment const & env, declaration const & d); -}; } diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 67674c1339..949a160bf0 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -188,7 +188,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(certified_declaration::certify_or_check(env, mk_axiom(n, ls, t, m_is_meta))); + return env.add(mk_axiom(n, ls, t, m_is_meta)); } environment certified_inductive_decl::add_core(environment const & env, bool update_ext_only) const { @@ -323,8 +323,8 @@ struct add_inductive_fn { /** \brief Add all datatype declarations to environment. */ void declare_inductive_type() { - m_env = m_env.add(check(m_env, mk_axiom(m_decl.m_name, m_decl.m_level_params, m_decl.m_type, - m_is_meta))); + m_env = m_env.add(mk_axiom(m_decl.m_name, m_decl.m_level_params, m_decl.m_type, + m_is_meta)); updt_type_checker(); } @@ -433,9 +433,9 @@ struct add_inductive_fn { /** \brief Add all introduction rules (aka constructors) to environment. */ void declare_intro_rules() { for (auto ir : m_decl.m_intro_rules) { - m_env = m_env.add(check(m_env, mk_axiom(intro_rule_name(ir), - m_decl.m_level_params, intro_rule_type(ir), - m_is_meta))); + m_env = m_env.add(mk_axiom(intro_rule_name(ir), + m_decl.m_level_params, intro_rule_type(ir), + m_is_meta)); } updt_type_checker(); } @@ -646,8 +646,8 @@ struct add_inductive_fn { // parameters 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_axiom(get_elim_name(), get_elim_level_param_names(), elim_ty, - m_is_meta))); + m_env = m_env.add(mk_axiom(get_elim_name(), get_elim_level_param_names(), elim_ty, + m_is_meta)); return elim_ty; } diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp index fb4a331bc7..ce3c3fe444 100644 --- a/src/kernel/quot.cpp +++ b/src/kernel/quot.cpp @@ -19,8 +19,7 @@ name * quot_consts::g_quot_ind = nullptr; name * quot_consts::g_quot_mk = nullptr; static environment add_constant(environment const & env, name const & n, std::initializer_list lvls, expr const & type) { - auto cd = check(env, mk_axiom(n, level_param_names(lvls), type)); - return env.add(cd); + return env.add(mk_axiom(n, level_param_names(lvls), type)); } static void check_eq_type(environment const & env) { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 4b41fc3e64..7ba0c00081 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -803,92 +803,6 @@ type_checker::type_checker(environment const & env, local_ctx const & lctx, bool type_checker::~type_checker() {} -static void check_no_metavar(environment const & env, name const & n, expr const & e) { - if (has_metavar(e)) - throw declaration_has_metavars_exception(env, n, e); -} - -static void check_no_fvar(environment const & env, name const & n, expr const & e) { - if (has_fvar(e)) - throw declaration_has_free_vars_exception(env, n, e); -} - -void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e) { - check_no_metavar(env, n, e); - check_no_fvar(env, n, e); -} - -static void check_name(environment const & env, name const & n) { - if (env.find(n)) - throw already_declared_exception(env, n); -} - -static void check_duplicated_params(environment const & env, declaration const & d) { - level_param_names ls = d.get_univ_params(); - while (!is_nil(ls)) { - auto const & p = head(ls); - ls = tail(ls); - if (std::find(ls.begin(), ls.end(), p) != ls.end()) { - throw kernel_exception(env, sstream() << "failed to add declaration to environment, " - << "duplicate universe level parameter: '" - << p << "'"); - } - } -} - -static void check_definition(environment const & env, declaration const & d, type_checker & checker) { - check_no_metavar_no_fvar(env, d.get_name(), d.get_value()); - expr val_type = checker.check(d.get_value(), d.get_univ_params()); - if (!checker.is_def_eq(val_type, d.get_type())) { - throw definition_type_mismatch_exception(env, d, val_type); - } -} - -static void check_decl_type(environment const & env, declaration const & d, type_checker & checker) { - check_no_metavar_no_fvar(env, d.get_name(), d.get_type()); - check_name(env, d.get_name()); - check_duplicated_params(env, d); - expr sort = checker.check(d.get_type(), d.get_univ_params()); - checker.ensure_sort(sort, d.get_type()); -} - -void check_decl_type(environment const & env, declaration const & d) { - bool memoize = true; bool non_meta_only = !d.is_meta(); - type_checker checker(env, memoize, non_meta_only); - check_decl_type(env, d, checker); -} - -void check_decl_value(environment const & env, declaration const & d) { - bool memoize = true; bool non_meta_only = !d.is_meta(); - type_checker checker(env, memoize, non_meta_only); - if (d.has_value()) { - check_definition(env, d, checker); - } -} - -certified_declaration check(environment const & env, declaration const & d) { - bool memoize = true; bool non_meta_only = !d.is_meta(); - type_checker checker(env, memoize, non_meta_only); - check_decl_type(env, d, checker); - if (d.has_value()) { - check_definition(env, d, checker); - } - return certified_declaration(d); -} - -certified_declaration certified_declaration::certify(environment const & env, declaration const & d) { - if (env.trust_lvl() == 0) - throw kernel_exception(env, "environment trust level does not allow users to add declarations that were not type checked"); - return certified_declaration(d); -} - -certified_declaration certified_declaration::certify_or_check(environment const & env, declaration const & d) { - if (env.trust_lvl() == 0) - return check(env, d); - else - return certify(env, d); -} - void initialize_type_checker() { g_id_delta = new name("id_delta"); g_dont_care = new expr(mk_const("dontcare")); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index b30d7eb6c0..c32d662b99 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -133,14 +133,6 @@ public: } }; -void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e); -void check_decl_type(environment const & env, declaration const & d); -void check_decl_value(environment const & env, declaration const & d); - -/** \brief Type check the given declaration, and return a certified declaration if it is type correct. - Throw an exception if the declaration is type incorrect. */ -certified_declaration check(environment const & env, declaration const & d); - void initialize_type_checker(); void finalize_type_checker(); } diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index 9dd2152aa2..66966fa1cc 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -168,7 +168,7 @@ struct mk_aux_definition_fn : public closure_helper { } else { d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, *is_meta); } - environment new_env = module::add(env, check(env, d)); + environment new_env = module::add(env, d); buffer ls; get_level_closure(ls); buffer ps; diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp index de741e8ae9..d625e75bf6 100644 --- a/src/library/compiler/elim_recursors.cpp +++ b/src/library/compiler/elim_recursors.cpp @@ -35,8 +35,7 @@ protected: bool meta = true; /* We add declaration as an axiom to make sure we can infer the type of the resultant expression. */ - declaration new_decl = mk_axiom(n, ps, type, meta); - m_env = m_env.add(check(m_env, new_decl)); + m_env = m_env.add(mk_axiom(n, ps, type, meta)); return mk_constant(n, param_names_to_levels(ps)); } diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 798741237f..04b3218af9 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -147,7 +147,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow 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)); + environment new_env = module::add(env, new_d); new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true); return add_protected(new_env, below_name); } @@ -326,7 +326,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) 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)); + environment new_env = module::add(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); return add_protected(new_env, brec_on_name); diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index b483480df4..b155753671 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -113,7 +113,7 @@ environment mk_cases_on(environment const & env, name const & n) { 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)); + environment new_env = module::add(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); return add_protected(new_env, cases_on_name); diff --git a/src/library/constructions/drec.cpp b/src/library/constructions/drec.cpp index 8f0a0c9a4a..3ed8aca647 100644 --- a/src/library/constructions/drec.cpp +++ b/src/library/constructions/drec.cpp @@ -198,7 +198,7 @@ struct mk_drec_fn { 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)); + environment new_env = module::add(env, new_d); new_env = set_reducible(new_env, drec_name, reducible_status::Reducible, true); new_env = add_aux_recursor(new_env, drec_name); return add_protected(new_env, drec_name); diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp index 14f146b1f5..927af0bb88 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_meta(m_env, sizeof_name, lp_names, sizeof_type, sizeof_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, sizeof_name, lp_names, sizeof_type, sizeof_val)); 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_meta(m_env, has_sizeof_name, lp_names, has_sizeof_type, has_sizeof_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, has_sizeof_name, lp_names, has_sizeof_type, has_sizeof_val)); 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_meta(m_env, dsimp_rule_name, lp_names, dsimp_rule_type, dsimp_rule_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, dsimp_rule_name, lp_names, dsimp_rule_type, dsimp_rule_val)); 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 6abf9d9a2f..b5fcce0038 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_meta(env, inj_arrow_name, - cons(P_lp_name, d.get_univ_params()), inj_arrow_type, inj_arrow_val))); + environment new_env = module::add(env, mk_definition_inferring_meta(env, inj_arrow_name, + cons(P_lp_name, d.get_univ_params()), inj_arrow_type, inj_arrow_val)); 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_meta(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val))); + env = module::add(env, mk_definition_inferring_meta(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val)); 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_meta(env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value))); + env = module::add(env, mk_definition_inferring_meta(env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value)); } } return env; diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 6790babd92..5b46bcd862 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -124,7 +124,7 @@ optional mk_no_confusion_type(environment const & env, name const & 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)); + environment new_env = module::add(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)); } @@ -234,7 +234,7 @@ environment mk_no_confusion(environment const & env, name const & n) { expr no_confusion_val = Fun(args, eq_rec); 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 = module::add(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); return add_protected(new_env, no_confusion_name); diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 080ed30298..83515b8217 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -122,7 +122,7 @@ environment mk_projections(environment const & env, name const & n, buffer proj_val = Fun(proj_args, proj_val); 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 = module::add(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); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index 5bbf89d8b7..c660b1ea68 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_meta(env, rec_on_name, rec_decl.get_univ_params(), - rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation()))); + 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/derive_attribute.cpp b/src/library/derive_attribute.cpp index 762345e92a..93e09bd708 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -122,10 +122,8 @@ static environment derive(environment env, name const & n, exprs const & clss) { tgt = ctx.mk_pi(n_params, tgt); auto inst2 = ctx.mk_lambda(n_params, inst.value()); auto new_n = n + const_name(cls); - auto def = mk_definition(env, new_n, d.get_univ_params(), - ctx.instantiate_mvars(tgt), inst2, d.is_meta()); - auto cdef = check(env, def); - env = module::add(env, cdef); + env = module::add(env, mk_definition(env, new_n, d.get_univ_params(), + ctx.instantiate_mvars(tgt), inst2, d.is_meta())); env = add_instance(env, new_n, LEAN_DEFAULT_PRIORITY, true); env = add_protected(env, new_n); } diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 0f70eb76be..30eab66ce0 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -1068,8 +1068,7 @@ environment mk_smart_unfolding_definition(environment const & env, options const helper_value = locals.mk_lambda(helper_value); try { declaration def = mk_definition(env, mk_smart_unfolding_name_for(n), d.get_univ_params(), d.get_type(), helper_value, true); - auto cdef = check(env, def); - return module::add(env, cdef); + return module::add(env, def); } catch (exception & ex) { throw nested_exception("failed to generate helper declaration for smart unfolding, type error", std::current_exception()); } diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp index d0dfa55094..9aba3afb66 100644 --- a/src/library/inductive_compiler/mutual.cpp +++ b/src/library/inductive_compiler/mutual.cpp @@ -293,7 +293,7 @@ class add_mutual_inductive_decl_fn { << local_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_meta(m_env, local_name(ind), names(m_mut_decl.get_lp_names()), new_ind_type, new_ind_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, local_name(ind), names(m_mut_decl.get_lp_names()), new_ind_type, new_ind_val)); m_tctx.set_env(m_env); } } @@ -327,14 +327,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(local_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_meta(m_env, mk_injective_name(ir_name), lp_names, inj_and_type, inj_and_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, mk_injective_name(ir_name), lp_names, inj_and_type, inj_and_val)); 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_meta(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value)); } m_tctx.set_env(m_env); @@ -358,7 +358,7 @@ class add_mutual_inductive_decl_fn { lean_assert(!has_local(new_ir_val)); lean_trace(name({"inductive_compiler", "mutual", "ir"}), tout() << local_name(ir) << " : " << new_ir_type << "\n";); - m_env = module::add(m_env, check(m_env, mk_definition_inferring_meta(m_env, local_name(ir), names(m_mut_decl.get_lp_names()), new_ir_type, new_ir_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, local_name(ir), names(m_mut_decl.get_lp_names()), new_ir_type, new_ir_val)); m_env = set_pattern_attribute(m_env, local_name(ir)); m_tctx.set_env(m_env); basic_ir_idx++; @@ -638,7 +638,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_meta(m_env, get_dep_recursor(m_env, local_name(ind)), rec_lp_names, rec_type, rec_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, get_dep_recursor(m_env, local_name(ind)), rec_lp_names, rec_type, rec_val)); } void define_cases_on(name const & rec_name, level_param_names const & rec_lp_names, unsigned ind_idx) { @@ -712,7 +712,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_meta(m_env, name(local_name(ind), "cases_on"), rec_lp_names, cases_on_type, cases_on_val))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, name(local_name(ind), "cases_on"), rec_lp_names, cases_on_type, cases_on_val)); } void define_recursors() { diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 647ef8f169..1253aa9c67 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -336,11 +336,11 @@ class add_nested_inductive_decl_fn { assert_no_locals(n, val); declaration d = mk_definition_inferring_meta(m_env, n, names(m_nested_decl.get_lp_names()), ty, val); try { - m_env = module::add(m_env, check(m_env, d)); + m_env = module::add(m_env, d); lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << "\n";); } catch (exception & ex) { lean_trace(name({"inductive_compiler", "nested", "define", "failure"}), tout() << n << " : " << ty << " :=\n" << val << "\n";); - m_env = module::add(m_env, check(m_env, mk_axiom(n, names(m_nested_decl.get_lp_names()), ty))); + m_env = module::add(m_env, mk_axiom(n, names(m_nested_decl.get_lp_names()), ty)); } m_tctx.set_env(m_env); } @@ -354,7 +354,7 @@ class add_nested_inductive_decl_fn { assert_no_locals(n, val); declaration d = mk_definition_inferring_meta(m_env, n, lp_names, ty, val); try { - m_env = module::add(m_env, check(m_env, d)); + m_env = module::add(m_env, d); lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << " :=\n " << val << "\n";); } catch (exception & ex) { lean_trace(name({"inductive_compiler", "nested", "define", "failure"}), tout() << n << " : " << ty << " :=\n " << val << "\n";); @@ -1424,7 +1424,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_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof)); m_tctx.set_env(m_env); m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); } @@ -1462,7 +1462,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_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof)); m_tctx.set_env(m_env); m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); } @@ -1530,7 +1530,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_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, lemma_name, names(m_nested_decl.get_lp_names()), goal, proof)); m_tctx.set_env(m_env); m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); } @@ -2002,14 +2002,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_meta(m_env, inj_name, lp_names, inj_type, inj_val))); + mk_definition_inferring_meta(m_env, inj_name, lp_names, inj_type, inj_val)); 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_meta(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value))); + m_env = module::add(m_env, mk_definition_inferring_meta(m_env, inj_eq_name, lp_names, inj_eq_type, inj_eq_value)); } } } diff --git a/src/library/module.cpp b/src/library/module.cpp index 7c5088c7a5..b2f23d69db 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -284,15 +284,6 @@ void register_module_object_reader(std::string const & k, module_modification_re readers[k] = r; } -struct import_helper { - static environment add_unchecked(environment const & env, declaration const & decl) { - return env.add(certify_or_check(env, decl)); - } - static certified_declaration certify_or_check(environment const & env, declaration const & decl) { - return certified_declaration::certify_or_check(env, decl); - } -}; - struct decl_modification : public modification { LEAN_MODIFICATION("decl") declaration m_decl; @@ -302,8 +293,7 @@ struct decl_modification : public modification { m_decl(decl) {} void perform(environment & env) const override { - // TODO(gabriel): this might be a bit more unsafe here than before - env = import_helper::add_unchecked(env, m_decl); + env = env.add(m_decl, false); } void serialize(serializer & s) const override { @@ -410,14 +400,13 @@ environment update_module_defs(environment const & env, declaration const & d) { } } -environment add(environment const & env, certified_declaration const & d) { +environment add(environment const & env, declaration const & d) { environment new_env = env.add(d); - declaration _d = d.get_declaration(); - if (!check_computable(new_env, _d.get_name())) - new_env = mark_noncomputable(new_env, _d.get_name()); - new_env = update_module_defs(new_env, _d); - new_env = add(new_env, std::make_shared(_d)); - return add_decl_pos_info(new_env, _d.get_name()); + if (!check_computable(new_env, d.get_name())) + new_env = mark_noncomputable(new_env, d.get_name()); + new_env = update_module_defs(new_env, d); + new_env = add(new_env, std::make_shared(d)); + return add_decl_pos_info(new_env, d.get_name()); } environment add_meta(environment const & env, buffer const & ds) { diff --git a/src/library/module.h b/src/library/module.h index c92e421fbb..8205957391 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -136,7 +136,7 @@ environment add(environment const & env, std::shared_ptr con environment add_and_perform(environment const & env, std::shared_ptr const & modif); /** \brief Add the given declaration to the environment, and mark it to be exported. */ -environment add(environment const & env, certified_declaration const & d); +environment add(environment const & env, declaration const & d); environment add_meta(environment const & env, buffer const & ds); /** \brief Return true iff \c n is a definition added to the current module using #module::add */ diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp index 7ef6ec8472..8fa67a9e77 100644 --- a/src/library/tactic/eval.cpp +++ b/src/library/tactic/eval.cpp @@ -32,8 +32,7 @@ static vm_obj eval(expr const & A, expr a, tactic_state const & s) { environment aux_env = S.env(); name eval_aux_name = mk_unused_name(aux_env, "_eval_expr"); try { - auto cd = check(aux_env, mk_definition(aux_env, eval_aux_name, {}, A, a, false)); - aux_env = aux_env.add(cd); + aux_env = aux_env.add(mk_definition(aux_env, eval_aux_name, {}, A, a, false)); } catch (definition_type_mismatch_exception & ex) { expr given_type = ex.get_given_type(); return tactic::mk_exception([=]() { diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index baa4e42aa7..c67b012b87 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -713,7 +713,7 @@ vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) { tactic_state const & s = tactic::to_state(_s); try { declaration d = to_declaration(_d); - environment new_env = module::add(s.env(), check(s.env(), d)); + environment new_env = module::add(s.env(), d); new_env = vm_compile(new_env, d); return tactic::mk_success(set_env(s, new_env)); } catch (throwable & ex) { @@ -793,8 +793,7 @@ format tactic_state::pp() const { environment new_env = ctx.env(); bool is_meta = true; name pp_name("_pp_tactic_state"); - auto cd = check(new_env, mk_definition(new_env, pp_name, {}, type, code, is_meta)); - new_env = new_env.add(cd); + new_env = new_env.add(mk_definition(new_env, pp_name, {}, type, code, is_meta)); new_env = vm_compile(new_env, new_env.get(pp_name)); vm_state S(new_env, get_options()); vm_obj r = S.invoke(pp_name, to_obj(*this)); diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index 9fb39b8cbe..1d29173ff1 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -240,9 +240,7 @@ environment interaction_monad::evaluator::compile(name const & interactio expr interaction_type = m_ctx.infer(interaction); environment new_env = m_ctx.env(); bool is_meta = true; - auto cd = check(new_env, - mk_definition(new_env, interaction_name, {}, interaction_type, interaction, is_meta)); - new_env = new_env.add(cd); + new_env = new_env.add(mk_definition(new_env, interaction_name, {}, interaction_type, interaction, is_meta)); if (provider) { if (auto pos = provider->get_pos_info(interaction)) new_env = add_transient_decl_pos_info(new_env, interaction_name, *pos);