max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(kernel): remove certified_declaration

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-22 12:09:57 -07:00
parent d64a49a7da
commit f3e99286bb
29 changed files with 156 additions and 234 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/decl_cmds.cpp
View file

@ -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);

27
src/frontends/lean/definition_cmds.cpp
View file

@ -171,25 +171,6 @@ static void finalize_definition(elaborator & elab, buffer<expr> 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<name> 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) {

6
src/frontends/lean/structure_cmd.cpp
View file

@ -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]) {

3
src/frontends/lean/util.cpp
View file

@ -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));
}

94
src/kernel/environment.cpp
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#include <utility>
#include <vector>
#include <limits>
#include <util/task_builder.h>
#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<declaration> const & ds, bool check) const {
@ -77,13 +155,13 @@ environment environment::add_meta(buffer<declaration> 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;

31
src/kernel/environment.h
View file

@ -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<normalizer_extension> 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);
};
}

16
src/kernel/inductive/inductive.cpp
View file

@ -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;
}

3
src/kernel/quot.cpp
View file

@ -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<name> 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) {

86
src/kernel/type_checker.cpp
View file

@ -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"));

8
src/kernel/type_checker.h
View file

@ -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();
}

2
src/library/aux_definition.cpp
View file

@ -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<level> ls;
get_level_closure(ls);
buffer<expr> ps;

3
src/library/compiler/elim_recursors.cpp
View file

@ -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));
}

4
src/library/constructions/brec_on.cpp
View file

@ -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);

2
src/library/constructions/cases_on.cpp
View file

@ -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);

2
src/library/constructions/drec.cpp
View file

@ -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);

6
src/library/constructions/has_sizeof.cpp
View file

@ -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);

8
src/library/constructions/injective.cpp
View file

@ -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;

4
src/library/constructions/no_confusion.cpp
View file

@ -124,7 +124,7 @@ optional<environment> 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);

2
src/library/constructions/projection.cpp
View file

@ -122,7 +122,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
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);

4
src/library/constructions/rec_on.cpp
View file

@ -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);

6
src/library/derive_attribute.cpp
View file

@ -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);
}

3
src/library/equations_compiler/util.cpp
View file

@ -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());
}

12
src/library/inductive_compiler/mutual.cpp
View file

@ -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() {

17
src/library/inductive_compiler/nested.cpp
View file

@ -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));
}
}
}

25
src/library/module.cpp
View file

@ -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<decl_modification>(_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<decl_modification>(d));
return add_decl_pos_info(new_env, d.get_name());
}
environment add_meta(environment const & env, buffer<declaration> const & ds) {

2
src/library/module.h
View file

@ -136,7 +136,7 @@ environment add(environment const & env, std::shared_ptr<modification const> con
environment add_and_perform(environment const & env, std::shared_ptr<modification const> 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<declaration> const & ds);
/** \brief Return true iff \c n is a definition added to the current module using #module::add */

3
src/library/tactic/eval.cpp
View file

@ -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([=]() {

5
src/library/tactic/tactic_state.cpp
View file

@ -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));

4
src/library/vm/interaction_state_imp.h
View file

@ -240,9 +240,7 @@ environment interaction_monad<State>::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);