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

refactor(kernel): use m_meta instead of m_trusted

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-31 11:18:00 -07:00
parent e80765daca
commit 3c1ccc9b74
49 changed files with 219 additions and 237 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/declaration.lean
View file

@ -84,7 +84,7 @@ meta def value : declaration → expr
| (thm _ _ _ v) := v | (thm _ _ _ v) := v
| _ := default expr | _ := default expr
meta def is_trusted : declaration → bool meta def is_meta : declaration → bool
| (defn _ _ _ _ _ t) := t | (defn _ _ _ _ _ t) := t
| (cnst _ _ _ t) := t | (cnst _ _ _ t) := t
| _ := tt | _ := tt

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

@ -126,8 +126,8 @@ static environment declare_var(parser & p, environment env,
if (k == variable_kind::Axiom) { if (k == variable_kind::Axiom) {
env = module::add(env, check(env, mk_axiom(full_n, ls, new_type))); env = module::add(env, check(env, mk_axiom(full_n, ls, new_type)));
} else { } else {
bool is_trusted = !meta.m_modifiers.m_is_meta; bool is_meta = meta.m_modifiers.m_is_meta;
env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_trusted))); env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_meta)));
} }
if (meta.m_doc_string) if (meta.m_doc_string)
env = add_doc_string(env, full_n, *meta.m_doc_string); env = add_doc_string(env, full_n, *meta.m_doc_string);

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

@ -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); std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val);
} }
bool use_conv_opt = true; 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 = auto def =
(kind == decl_cmd_kind::Theorem ? (kind == decl_cmd_kind::Theorem ?
mk_theorem(c_real_name, names(lp_names), type, *val) : 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) : (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_trusted))); 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); auto cdef = check(p, new_env, c_name, def, pos);
new_env = module::add(new_env, cdef); 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); finalize_definition(elab, params_buf, type, val, univ_params_buf, modifiers.m_is_meta);
bool use_conv_opt = true; 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 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); auto cdef = check(new_env, def);
new_env = module::add(new_env, cdef); new_env = module::add(new_env, cdef);
check_noncomputable(noncomputable_theory, new_env, decl_name, def.get_name(), modifiers.m_is_noncomputable, check_noncomputable(noncomputable_theory, new_env, decl_name, def.get_name(), modifiers.m_is_noncomputable,

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

@ -705,7 +705,7 @@ public:
parse_result r; parse_result r;
parse(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, 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); post_process(r.m_params, r.m_inds, r.m_intro_rules);
return m_env; return m_env;
} }

4
src/frontends/lean/print_cmd.cpp
View file

@ -88,7 +88,7 @@ static void print_axioms(parser & p, message_builder & out) {
bool has_axioms = false; bool has_axioms = false;
p.env().for_each_declaration([&](declaration const & d) { p.env().for_each_declaration([&](declaration const & d) {
name const & n = d.get_name(); 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; out << n << " : " << d.get_type() << endl;
has_axioms = true; has_axioms = true;
} }
@ -328,7 +328,7 @@ static bool print_constant(parser const & p, message_builder & out, char const *
out << "protected "; out << "protected ";
if (d.is_definition() && is_marked_noncomputable(p.env(), d.get_name())) if (d.is_definition() && is_marked_noncomputable(p.env(), d.get_name()))
out << "noncomputable "; out << "noncomputable ";
if (!d.is_trusted()) if (d.is_meta())
out << "meta "; out << "meta ";
out << kind << " " << to_user_name(p.env(), d.get_name()); 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)) out.get_text_stream().update_options(out.get_text_stream().get_options().update((name {"pp", "binder_types"}), true))

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

@ -1069,8 +1069,8 @@ struct structure_cmd_fn {
level_param_names lnames = names(m_level_names); level_param_names lnames = names(m_level_names);
inductive::intro_rule intro = inductive::mk_intro_rule(m_mk, intro_type); 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)); 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; bool is_meta = m_meta_info.m_modifiers.m_is_meta;
m_env = module::add_inductive(m_env, decl, is_trusted); m_env = module::add_inductive(m_env, decl, is_meta);
name rec_name = inductive::get_elim_name(m_name); name rec_name = inductive::get_elim_name(m_name);
m_env = add_namespace(m_env, m_name); m_env = add_namespace(m_env, m_name);
m_env = add_protected(m_env, rec_name); m_env = add_protected(m_env, rec_name);
@ -1079,7 +1079,7 @@ struct structure_cmd_fn {
add_rec_alias(rec_name); add_rec_alias(rec_name);
m_env = add_structure_declaration_aux(m_env, m_p.get_options(), m_level_names, m_params, 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_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() { 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_value, used_univs);
used_univs = collect_univ_params(decl_type, used_univs); used_univs = collect_univ_params(decl_type, used_univs);
level_param_names decl_lvls = to_level_param_names(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()); 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, check(m_env, new_decl));
if (!m_meta_info.m_modifiers.m_is_meta) 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) { void add_rec_on_alias(name const & n) {
name rec_on_name(m_name, "rec_on"); name rec_on_name(m_name, "rec_on");
declaration rec_on_decl = m_env.get(rec_on_name); 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(), rec_on_decl.get_type(), rec_on_decl.get_value(),
reducibility_hints::mk_abbreviation()); reducibility_hints::mk_abbreviation());
m_env = module::add(m_env, check(m_env, new_decl)); 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); coercion_value = Fun(m_params, Fun(st, coercion_value, m_p), m_p);
name coercion_name = coercion_names[i]; name coercion_name = coercion_names[i];
bool use_conv_opt = false; bool use_conv_opt = false;
declaration coercion_decl = mk_definition_inferring_trusted(m_env, coercion_name, lnames, declaration coercion_decl = mk_definition_inferring_meta(m_env, coercion_name, lnames,
coercion_type, coercion_value, use_conv_opt); coercion_type, coercion_value, use_conv_opt);
m_env = module::add(m_env, check(m_env, coercion_decl)); m_env = module::add(m_env, check(m_env, coercion_decl));
add_alias(coercion_name); add_alias(coercion_name);
m_env = vm_compile(m_env, m_env.get(coercion_name)); m_env = vm_compile(m_env, m_env.get(coercion_name));

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

@ -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 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; environment new_env = env;
bool use_conv_opt = true; bool use_conv_opt = true;
bool is_trusted = false; bool is_meta = true;
auto cd = check(new_env, mk_definition(new_env, n, ls, type, e, use_conv_opt, is_trusted)); 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 = new_env.add(cd);
new_env = add_transient_decl_pos_info(new_env, n, pos); new_env = add_transient_decl_pos_info(new_env, n, pos);
return vm_compile(new_env, new_env.get(n)); return vm_compile(new_env, new_env.get(n));

2
src/kernel/abstract_type_context.h
View file

@ -30,8 +30,6 @@ public:
virtual expr check(expr const & e) { return infer(e); } virtual expr check(expr const & e) { return infer(e); }
virtual optional<expr> is_stuck(expr const &) { return none_expr(); } virtual optional<expr> 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 expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info());
virtual void pop_local(); virtual void pop_local();
virtual bool has_local_pp_name(name const & pp_name); virtual bool has_local_pp_name(name const & pp_name);

44
src/kernel/declaration.cpp
View file

@ -52,7 +52,7 @@ bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_v
bool declaration::is_constant_assumption() const { return !is_definition(); } 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_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_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; } 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; } 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; } 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, declaration mk_definition(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) {
return declaration(new declaration::cell(n, params, t, v, h, trusted)); return declaration(new declaration::cell(n, params, t, v, h, meta));
} }
static unsigned get_max_height(environment const & env, expr const & v) { static unsigned get_max_height(environment const & env, expr const & v) {
unsigned h = 0; 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, 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); 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) { 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)); return declaration(new declaration::cell(n, params, t, v));
} }
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) { 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) { 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, trusted)); 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; bool found = false;
for_each(e, [&](expr const & e, unsigned) { for_each(e, [&](expr const & e, unsigned) {
if (found) return false; if (found) return false;
if (is_constant(e)) { if (is_constant(e)) {
if (auto d = env.find(const_name(e))) { if (auto d = env.find(const_name(e))) {
if (!d->is_trusted()) { if (d->is_meta()) {
found = true; found = true;
return false; return false;
} }
@ -114,20 +114,22 @@ bool use_untrusted(environment const & env, expr const & e) {
return found; 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) { expr const & t, expr const & v, reducibility_hints const & hints) {
bool trusted = !use_untrusted(env, t) && !use_untrusted(env, v); bool meta = use_meta(env, t) || use_meta(env, v);
return mk_definition(n, params, t, v, hints, trusted); 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) { declaration mk_definition_inferring_meta(environment const & env, name const & n, level_param_names const & params,
bool trusted = !use_untrusted(env, t) && !use_untrusted(env, v); expr const & t, expr const & v, bool use_self_opt) {
unsigned h = get_max_height(env, v); bool meta = use_meta(env, t) && use_meta(env, v);
return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), trusted); 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) { declaration mk_constant_assumption_inferring_meta(environment const & env, name const & n,
return mk_constant_assumption(n, params, t, !use_untrusted(env, t)); level_param_names const & params, expr const & t) {
return mk_constant_assumption(n, params, t, use_meta(env, t));
} }
void initialize_declaration() { void initialize_declaration() {

53
src/kernel/declaration.h
View file

@ -76,23 +76,20 @@ class declaration {
bool m_theorem; bool m_theorem;
optional<expr> m_value; // if none, then declaration is actually a postulate optional<expr> m_value; // if none, then declaration is actually a postulate
reducibility_hints m_hints; reducibility_hints m_hints;
/* Definitions are trusted by default, and nested macros are expanded when kernel is instantiated with /* Definitions are non-meta by default. We use this feature to define tactical-definitions. */
trust level 0. When this flag is false, then we do not expand nested macros. We say the bool m_meta;
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;
void dealloc() { delete this; } 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_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, 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_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): 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_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; cell * m_ptr;
explicit declaration(cell * ptr); explicit declaration(cell * ptr);
@ -123,7 +120,7 @@ public:
bool is_theorem() const; bool is_theorem() const;
bool is_constant_assumption() const; bool is_constant_assumption() const;
bool is_trusted() const; bool is_meta() const;
name const & get_name() const; name const & get_name() const;
level_param_names const & get_univ_params() const; level_param_names const & get_univ_params() const;
@ -134,12 +131,12 @@ public:
reducibility_hints const & get_hints() const; reducibility_hints const & get_hints() const;
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, 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, 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_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_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<declaration> none_declaration() { return optional<declaration>(); } inline optional<declaration> none_declaration() { return optional<declaration>(); }
@ -147,27 +144,27 @@ inline optional<declaration> some_declaration(declaration const & o) { return op
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); } inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, 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, 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_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_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 */ /** \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. /** \brief Similar to mk_definition but infer the value of meta flag.
That is, set it to false if \c t or \c v contains a untrusted declaration. */ That is, set it to true if \c t or \c v contains a meta declaration. */
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); 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, 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); expr const & t, expr const & v, bool use_self_opt);
/** \brief Similar to mk_constant_assumption but infer the value of trusted flag. /** \brief Similar to mk_constant_assumption but infer the value of meta flag.
That is, set it to false if \c t or \c v contains a untrusted declaration. */ That is, set it to true if \c t or \c v contains a meta declaration. */
declaration mk_constant_assumption_inferring_trusted(environment const & env, name const & n, declaration mk_constant_assumption_inferring_meta(environment const & env, name const & n,
level_param_names const & params, expr const & t); level_param_names const & params, expr const & t);
void initialize_declaration(); void initialize_declaration();
void finalize_declaration(); void finalize_declaration();

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

@ -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, environment certified_inductive_decl::add_constant(environment const & env, name const & n, level_param_names const & ls,
expr const & t) const { 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 { 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 { environment certified_inductive_decl::add(environment const & env) const {
if (env.trust_lvl() == 0) { 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 { } else {
return add_core(env, false); return add_core(env, false);
} }
@ -256,16 +256,16 @@ struct add_inductive_fn {
elim_info():m_K_target(false) {} elim_info():m_K_target(false) {}
}; };
elim_info m_elim_info; // for datatype being declared elim_info m_elim_info; // for datatype being declared
bool m_is_trusted; bool m_is_meta;
add_inductive_fn(environment env, add_inductive_fn(environment env,
inductive_decl const & decl, inductive_decl const & decl,
bool is_trusted): bool is_meta):
m_env(env), m_name_generator(*g_ind_fresh), m_decl(decl), m_env(env), m_name_generator(*g_ind_fresh), m_decl(decl),
m_tc(new type_checker(m_env, true, false)) { m_tc(new type_checker(m_env, true, false)) {
m_is_not_zero = false; m_is_not_zero = false;
m_levels = param_names_to_levels(decl.m_level_params); 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. */ /** \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. */ /** \brief Add all datatype declarations to environment. */
void declare_inductive_type() { 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_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(); 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))) 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) << ") " throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") "
<< "of '" << n << "' is too big for the corresponding inductive datatype"); << "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); check_positivity(binding_domain(t), n, i);
bool is_rec = (bool)is_rec_argument(binding_domain(t)); // NOLINT bool is_rec = (bool)is_rec_argument(binding_domain(t)); // NOLINT
if (is_rec) if (is_rec)
@ -445,7 +445,7 @@ struct add_inductive_fn {
for (auto ir : m_decl.m_intro_rules) { for (auto ir : m_decl.m_intro_rules) {
m_env = m_env.add(check(m_env, mk_constant_assumption(intro_rule_name(ir), 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_decl.m_level_params, intro_rule_type(ir),
m_is_trusted))); m_is_meta)));
} }
updt_type_checker(); updt_type_checker();
} }
@ -660,7 +660,7 @@ struct add_inductive_fn {
elim_ty = Pi(m_param_consts, elim_ty); elim_ty = Pi(m_param_consts, elim_ty);
elim_ty = infer_implicit(elim_ty, true /* strict */); 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_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; 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, 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, 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_elim_info.m_K_target, m_elim_info.m_indices.size(), to_list(comp_rules),
m_is_trusted); m_is_meta);
} }
pair<environment, certified_inductive_decl> operator()() { pair<environment, certified_inductive_decl> operator()() {
@ -739,10 +739,10 @@ struct add_inductive_fn {
}; };
pair<environment, certified_inductive_decl> pair<environment, certified_inductive_decl>
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)) if (!env.norm_ext().supports(*g_inductive_extension))
throw kernel_exception(env, "environment does not support inductive datatypes"); 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 { bool inductive_normalizer_extension::supports(name const & feature) const {

10
src/kernel/inductive/inductive.h
View file

@ -63,7 +63,7 @@ private:
bool m_K_target; bool m_K_target;
unsigned m_num_indices; unsigned m_num_indices;
list<comp_rule> m_comp_rules; list<comp_rule> m_comp_rules;
bool m_is_trusted; bool m_is_meta;
friend struct add_inductive_fn; friend struct add_inductive_fn;
friend class ::lean::read_certified_inductive_decl_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, 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, expr const & elim_type, inductive_decl const & decl, bool K_target, unsigned nindices,
list<comp_rule> const & crules, bool is_trusted): list<comp_rule> const & crules, bool is_meta):
m_num_ACe(num_ACe), m_elim_prop(elim_prop), m_dep_elim(dep_delim), 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_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_K_target(K_target), m_num_indices(nindices), m_comp_rules(crules),
m_is_trusted(is_trusted) {} m_is_meta(is_meta) {}
public: public:
unsigned get_num_ACe() const { return m_num_ACe; } unsigned get_num_ACe() const { return m_num_ACe; }
bool elim_prop_only() const { return m_elim_prop; } bool elim_prop_only() const { return m_elim_prop; }
@ -88,7 +88,7 @@ public:
bool is_K_target() const { return m_K_target; } bool is_K_target() const { return m_K_target; }
unsigned get_num_indices() const { return m_num_indices; } unsigned get_num_indices() const { return m_num_indices; }
list<comp_rule> get_comp_rules() const { return m_comp_rules; } list<comp_rule> 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" /** \brief Update the environment with this "certified declaration"
\remark If trust_level is 0, then declaration is rechecked. */ \remark If trust_level is 0, then declaration is rechecked. */
@ -99,7 +99,7 @@ public:
pair<environment, certified_inductive_decl> pair<environment, certified_inductive_decl>
add_inductive(environment env, add_inductive(environment env,
inductive_decl const & decl, 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 /** \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. list of all inductive decls that were simultaneously defined with \c n.

21
src/kernel/type_checker.cpp
View file

@ -83,8 +83,8 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) {
<< const_name(e) << "', #" << const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided"); << length(ps) << " expected, #" << length(ls) << " provided");
if (!infer_only) { if (!infer_only) {
if (m_trusted_only && !d.is_trusted()) { if (m_non_meta_only && d.is_meta()) {
throw_kernel_exception(m_env, sstream() << "invalid definition, it uses untrusted declaration '" throw_kernel_exception(m_env, sstream() << "invalid definition, it uses meta declaration '"
<< const_name(e) << "'"); << const_name(e) << "'");
} }
for (level const & l : ls) 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) { expr type_checker::infer_macro(expr const & e, bool infer_only) {
auto def = macro_def(e); auto def = macro_def(e);
auto t = def.check_type(e, *this, infer_only); auto t = def.check_type(e, *this, infer_only);
if (!infer_only && m_trusted_only && def.trust_level() >= m_env.trust_lvl()) { // TODO(Leo): macros will be deleted
throw_kernel_exception(m_env, "declaration contains macro with trust-level higher than the one allowed " // if (!infer_only && m_trusted_only && def.trust_level() >= m_env.trust_lvl()) {
"(possible solution: unfold macro, or increase trust-level)", e); // 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; return t;
} }
@ -709,8 +710,8 @@ bool type_checker::is_def_eq(expr const & t, expr const & s) {
return r; return r;
} }
type_checker::type_checker(environment const & env, bool memoize, bool trusted_only): 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_trusted_only(trusted_only), m_params(nullptr) { 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() {} 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_no_mlocal(env, d.get_name(), d.get_type(), true);
check_name(env, d.get_name()); check_name(env, d.get_name());
check_duplicated_params(env, d); check_duplicated_params(env, d);
bool memoize = true; bool trusted_only = d.is_trusted(); bool memoize = true; bool non_meta_only = !d.is_meta();
type_checker checker(env, memoize, trusted_only); type_checker checker(env, memoize, non_meta_only);
expr sort = checker.check(d.get_type(), d.get_univ_params()); expr sort = checker.check(d.get_type(), d.get_univ_params());
checker.ensure_sort(sort, d.get_type()); checker.ensure_sort(sort, d.get_type());
if (d.is_definition()) { if (d.is_definition()) {

10
src/kernel/type_checker.h
View file

@ -32,7 +32,7 @@ class type_checker : public abstract_type_context {
environment m_env; environment m_env;
name_generator m_name_generator; name_generator m_name_generator;
bool m_memoize; bool m_memoize;
bool m_trusted_only; bool m_non_meta_only;
cache m_infer_type_cache[2]; cache m_infer_type_cache[2];
expr_map<expr> m_whnf_core_cache; expr_map<expr> m_whnf_core_cache;
expr_map<expr> m_whnf_cache; expr_map<expr> m_whnf_cache;
@ -79,8 +79,10 @@ class type_checker : public abstract_type_context {
public: public:
/** \brief Create a type checker for the given environment. /** \brief Create a type checker for the given environment.
memoize: if true, then inferred types are memoized/cached */ memoize: if true, then inferred types are memoized/cached.
type_checker(environment const & env, bool memoize = true, bool trusted_only = true);
*/
type_checker(environment const & env, bool memoize = true, bool non_meta_only = true);
~type_checker(); ~type_checker();
virtual environment const & env() const { return m_env; } virtual environment const & env() const { return m_env; }
@ -101,8 +103,6 @@ public:
expr check_ignore_undefined_universes(expr const & e); expr check_ignore_undefined_universes(expr const & e);
virtual expr check(expr const & t) { return check_ignore_undefined_universes(t); } 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. */ /** \brief Return true iff t is definitionally equal to s. */
virtual bool is_def_eq(expr const & t, expr const & 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. */ /** \brief Return true iff types of \c t and \c s are (may be) definitionally equal. */

15
src/library/aux_definition.cpp
View file

@ -152,7 +152,7 @@ buffer<expr> const & closure_helper::get_norm_closure_params() const {
struct mk_aux_definition_fn : public closure_helper { struct mk_aux_definition_fn : public closure_helper {
mk_aux_definition_fn(type_context_old & ctx):closure_helper(ctx) {} mk_aux_definition_fn(type_context_old & ctx):closure_helper(ctx) {}
pair<environment, expr> operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional<bool> const & is_meta) { pair<environment, expr> operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional<bool> is_meta) {
lean_assert(!is_lemma || is_meta); lean_assert(!is_lemma || is_meta);
lean_assert(!is_lemma || *is_meta == false); lean_assert(!is_lemma || *is_meta == false);
expr new_type = collect(ctx().instantiate_mvars(type)); expr new_type = collect(ctx().instantiate_mvars(type));
@ -161,21 +161,14 @@ struct mk_aux_definition_fn : public closure_helper {
finalize_collection(); finalize_collection();
expr def_type = mk_pi_closure(new_type); expr def_type = mk_pi_closure(new_type);
expr def_value = mk_lambda_closure(new_value); expr def_value = mk_lambda_closure(new_value);
bool untrusted = false; if (!is_meta)
if (is_meta) is_meta = use_meta(env, def_type) || use_meta(env, def_value);
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);
}
declaration d; declaration d;
if (is_lemma) { if (is_lemma) {
d = mk_theorem(c, get_norm_level_names(), def_type, def_value); d = mk_theorem(c, get_norm_level_names(), def_type, def_value);
} else { } else {
bool use_self_opt = true; 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)); environment new_env = module::add(env, check(env, d));
buffer<level> ls; buffer<level> ls;

2
src/library/aux_definition.h
View file

@ -107,7 +107,7 @@ public:
where l_i's and a_j's are the collected dependencies. 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() */ The updated environment is an extension of ctx.env() */
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,

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

@ -33,10 +33,10 @@ protected:
level_param_names ps = to_level_param_names(collect_univ_params(value)); level_param_names ps = to_level_param_names(collect_univ_params(value));
type_checker tc(m_env); type_checker tc(m_env);
expr type = tc.infer(value); expr type = tc.infer(value);
bool trusted = false; bool meta = true;
/* We add declaration as a constant to make sure /* We add declaration as a constant to make sure
we can infer the type of the resultant expression. */ 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)); m_env = m_env.add(check(m_env, new_decl));
return mk_constant(n, param_names_to_levels(ps)); return mk_constant(n, param_names_to_levels(ps));
} }

6
src/library/compiler/preprocess.cpp
View file

@ -164,9 +164,9 @@ class preprocess_fn {
context_cache m_cache; context_cache m_cache;
bool check(declaration const & d, expr const & v) { bool check(declaration const & d, expr const & v) {
bool memoize = true; bool memoize = true;
bool trusted_only = false; bool non_meta_only = false;
type_checker tc(m_env, memoize, trusted_only); type_checker tc(m_env, memoize, non_meta_only);
expr t = tc.check(v, d.get_univ_params()); expr t = tc.check(v, d.get_univ_params());
if (!tc.is_def_eq(d.get_type(), t)) if (!tc.is_def_eq(d.get_type(), t))
throw exception("preprocess failed"); throw exception("preprocess failed");

5
src/library/compiler/rec_fn_macro.cpp
View file

@ -34,10 +34,7 @@ public:
virtual void display(std::ostream & out) const override { out << m_name; } 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 { 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");
}
check_macro(m); check_macro(m);
return macro_arg(m, 0); return macro_arg(m, 0);
} }

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

@ -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_type = Pi(args, Type_result);
expr below_value = Fun(args, rec); expr below_value = Fun(args, rec);
declaration new_d = mk_definition_inferring_trusted(env, below_name, blvls, below_type, below_value, declaration new_d = mk_definition_inferring_meta(env, below_name, blvls, below_type, below_value,
reducibility_hints::mk_abbreviation()); reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, check(env, new_d)); environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true); new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true);
return add_protected(new_env, below_name); 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_type = Pi(args, result_type);
expr brec_on_value = Fun(args, mk_pprod_fst(tc, rec, ind)); 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, declaration new_d = mk_definition_inferring_meta(env, brec_on_name, blps, brec_on_type, brec_on_value,
reducibility_hints::mk_abbreviation()); reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, check(env, new_d)); 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 = set_reducible(new_env, brec_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, brec_on_name); new_env = add_aux_recursor(new_env, brec_on_name);

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

@ -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_type = Pi(cases_on_params, rec_type);
expr cases_on_value = Fun(cases_on_params, mk_app(rec_cnst, rec_args)); 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, 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()); reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, check(env, new_d)); 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 = set_reducible(new_env, cases_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, cases_on_name); new_env = add_aux_recursor(new_env, cases_on_name);

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

@ -197,9 +197,9 @@ struct mk_drec_fn {
expr rec_cnst = mk_constant(I_rec_name, lvls); expr rec_cnst = mk_constant(I_rec_name, lvls);
expr drec_value = Fun(drec_params, mk_app(rec_cnst, rec_args)); expr drec_value = Fun(drec_params, mk_app(rec_cnst, rec_args));
name drec_name = mk_drec_name(); name drec_name = mk_drec_name();
declaration new_d = mk_definition_inferring_trusted(env, drec_name, I_rec_decl.get_univ_params(), declaration new_d = mk_definition_inferring_meta(env, drec_name, I_rec_decl.get_univ_params(),
drec_type, drec_value, drec_type, drec_value,
reducibility_hints::mk_abbreviation()); reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, check(env, new_d)); environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, drec_name, reducible_status::Reducible, true); new_env = set_reducible(new_env, drec_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, drec_name); new_env = add_aux_recursor(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]: " << sizeof_name << " : " << sizeof_type << "\n"
<< sizeof_val << "\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 = set_reducible(m_env, sizeof_name, reducible_status::Irreducible, true);
m_env = add_protected(m_env, sizeof_name); 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]: " << has_sizeof_name << " : " << has_sizeof_type << "\n"
<< has_sizeof_val << "\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_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true);
m_env = add_protected(m_env, has_sizeof_name); 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_name << " : " << dsimp_rule_type << "\n"
<< dsimp_rule_val << "\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 = mark_rfl_lemma(m_env, dsimp_rule_name);
m_env = add_eqn_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); 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_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()); 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";); 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, 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))); cons(P_lp_name, d.get_univ_params()), inj_arrow_type, inj_arrow_val, true)));
return new_env; 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_type = mk_injective_type(env, ir_name, ir_type, num_params, lp_names);
expr inj_val = prove_injective(env, inj_type, ind_name); expr inj_val = prove_injective(env, inj_type, ind_name);
lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n " << inj_val << "\n";); 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); env = mk_injective_arrow(env, ir_name);
if (gen_inj_eq && env.find(get_tactic_mk_inj_eq_name())) { if (gen_inj_eq && env.find(get_tactic_mk_inj_eq_name())) {
name inj_eq_name = mk_injective_eq_name(ir_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_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); 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; return env;

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

@ -122,8 +122,8 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
} }
expr no_confusion_type_value = Fun(args, mk_app(cases_on1, outer_cases_on_args)); 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, 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()); reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, check(env, new_d)); environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true); new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true);
return some(add_protected(new_env, no_confusion_type_name)); 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); eq_rec = mk_app(mk_app(eq_rec, rec_type_former, gen, v2, H12), H12);
// //
expr no_confusion_val = Fun(args, eq_rec); 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, declaration new_d = mk_definition_inferring_meta(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
reducibility_hints::mk_abbreviation()); reducibility_hints::mk_abbreviation());
new_env = module::add(new_env, check(new_env, new_d)); 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 = set_reducible(new_env, no_confusion_name, reducible_status::Reducible, true);
new_env = add_no_confusion(new_env, no_confusion_name); new_env = add_no_confusion(new_env, no_confusion_name);

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

@ -261,8 +261,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
nparams + i, lvl_params, mtype, mval, proj_args.back()); nparams + i, lvl_params, mtype, mval, proj_args.back());
proj_val = Fun(proj_args, proj_val); proj_val = Fun(proj_args, proj_val);
} }
declaration new_d = mk_definition_inferring_trusted(env, proj_name, lvl_params, proj_type, proj_val, declaration new_d = mk_definition_inferring_meta(env, proj_name, lvl_params, proj_type, proj_val,
reducibility_hints::mk_abbreviation()); reducibility_hints::mk_abbreviation());
new_env = module::add(new_env, check(new_env, new_d)); 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 = 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); new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit);

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)); expr rec_on_val = Fun(new_locals, mk_app(rec, locals));
environment new_env = module::add(env, environment new_env = module::add(env,
check(env, mk_definition_inferring_trusted(env, rec_on_name, rec_decl.get_univ_params(), 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()))); 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 = set_reducible(new_env, rec_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, rec_on_name); new_env = add_aux_recursor(new_env, rec_on_name);
return add_protected(new_env, rec_on_name); return add_protected(new_env, rec_on_name);

4
src/library/equations_compiler/unbounded_rec.cpp
View file

@ -159,8 +159,8 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
fn = helper.mk_lambda_closure(fn); fn = helper.mk_lambda_closure(fn);
bool use_self_opt = true; bool use_self_opt = true;
bool trusted = false; bool is_meta = true;
declaration d = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, trusted); declaration d = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, is_meta);
env = module::add(env, check(env, d)); env = module::add(env, check(env, d));
expr result_fn = mk_app(mk_constant(fn_name, levels(closure_lvl_params)), closure_params); expr result_fn = mk_app(mk_constant(fn_name, levels(closure_lvl_params)), closure_params);

2
src/library/export.cpp
View file

@ -219,7 +219,7 @@ class exporter {
void export_declaration(declaration d) { void export_declaration(declaration d) {
// do not export meta declarations // do not export meta declarations
if (!d.is_trusted()) return; if (d.is_meta()) return;
if (is_quotient_decl(m_env, d.get_name())) if (is_quotient_decl(m_env, d.get_name()))
return export_quotient(); return export_quotient();

8
src/library/inductive_compiler/add_decl.cpp
View file

@ -17,16 +17,16 @@ environment add_inductive_declaration(environment const & old_env, options const
name_map<implicit_infer_kind> implicit_infer_map, name_map<implicit_infer_kind> implicit_infer_map,
buffer<name> const & lp_names, buffer<expr> const & params, buffer<name> const & lp_names, buffer<expr> const & params,
buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules,
bool is_trusted) { bool is_meta) {
name_generator ngen(*g_inductive_compiler_fresh); name_generator ngen(*g_inductive_compiler_fresh);
ginductive_decl decl(old_env, 0, lp_names, params, inds, intro_rules); 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; return env;
} }
environment add_structure_declaration_aux(environment const & old_env, options const &, buffer <name> const & lp_names, environment add_structure_declaration_aux(environment const & old_env, options const &, buffer <name> const & lp_names,
buffer <expr> const & params, expr const & ind, expr const & intro_rule, buffer <expr> const & params, expr const & ind, expr const & intro_rule,
bool is_trusted) { bool is_meta) {
buffer<expr> inds; buffer<expr> inds;
inds.push_back(ind); 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); ginductive_decl decl(old_env, 0, lp_names, params, inds, intro_rules);
environment env = old_env; 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)); env = mk_has_sizeof(env, mlocal_name(ind));
return register_ginductive_decl(env, decl, ginductive_kind::BASIC); return register_ginductive_decl(env, decl, ginductive_kind::BASIC);

4
src/library/inductive_compiler/add_decl.h
View file

@ -13,11 +13,11 @@ environment add_inductive_declaration(environment const & env, options const & o
name_map<implicit_infer_kind> implicit_infer_map, name_map<implicit_infer_kind> implicit_infer_map,
buffer<name> const & lp_names, buffer<expr> const & params, buffer<name> const & lp_names, buffer<expr> const & params,
buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules,
bool is_trusted); bool is_meta);
environment add_structure_declaration_aux(environment const & env, options const & opts, buffer <name> const & lp_names, environment add_structure_declaration_aux(environment const & env, options const & opts, buffer <name> const & lp_names,
buffer <expr> const & params, expr const & ind, expr const & intro_rule, buffer <expr> const & params, expr const & ind, expr const & intro_rule,
bool is_trusted); bool is_meta);
void initialize_inductive_compiler_add_decl(); void initialize_inductive_compiler_add_decl();
void finalize_inductive_compiler_add_decl(); void finalize_inductive_compiler_add_decl();

14
src/library/inductive_compiler/basic.cpp
View file

@ -70,7 +70,7 @@ class add_basic_inductive_decl_fn {
options const & m_opts; options const & m_opts;
name_map<implicit_infer_kind> const & m_implicit_infer_map; name_map<implicit_infer_kind> const & m_implicit_infer_map;
ginductive_decl const & m_decl; ginductive_decl const & m_decl;
bool m_is_trusted; bool m_is_meta;
void mk_basic_aux_decls() { void mk_basic_aux_decls() {
name ind_name = mlocal_name(m_decl.get_inds()[0]); 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); 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); 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";); 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)); 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: public:
add_basic_inductive_decl_fn(environment const & env, options const & opts, name_map<implicit_infer_kind> implicit_infer_map, add_basic_inductive_decl_fn(environment const & env, options const & opts, name_map<implicit_infer_kind> implicit_infer_map,
ginductive_decl const & decl, bool 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_trusted(is_trusted) {} m_env(env), m_opts(opts), m_implicit_infer_map(implicit_infer_map), m_decl(decl), m_is_meta(is_meta) {}
environment operator()() { environment operator()() {
send_to_kernel(); send_to_kernel();
@ -150,8 +150,8 @@ public:
}; };
environment add_basic_inductive_decl(environment const & env, options const & opts, name_map<implicit_infer_kind> implicit_infer_map, environment add_basic_inductive_decl(environment const & env, options const & opts, name_map<implicit_infer_kind> implicit_infer_map,
ginductive_decl const & decl, bool is_trusted) { ginductive_decl const & decl, bool is_meta) {
return add_basic_inductive_decl_fn(env, opts, implicit_infer_map, decl, is_trusted)(); return add_basic_inductive_decl_fn(env, opts, implicit_infer_map, decl, is_meta)();
} }
void initialize_inductive_compiler_basic() { void initialize_inductive_compiler_basic() {

2
src/library/inductive_compiler/basic.h
View file

@ -12,7 +12,7 @@ Author: Daniel Selsam
namespace lean { namespace lean {
environment add_basic_inductive_decl(environment const & env, options const & opts, environment add_basic_inductive_decl(environment const & env, options const & opts,
name_map<implicit_infer_kind> implicit_infer_map, name_map<implicit_infer_kind> implicit_infer_map,
ginductive_decl const & decl, bool is_trusted); ginductive_decl const & decl, bool is_meta);
void initialize_inductive_compiler_basic(); void initialize_inductive_compiler_basic();
void finalize_inductive_compiler_basic(); void finalize_inductive_compiler_basic();

10
src/library/inductive_compiler/compiler.cpp
View file

@ -19,20 +19,20 @@ Author: Daniel Selsam
namespace lean { namespace lean {
environment add_inner_inductive_declaration(environment const & env, name_generator & ngen, options const & opts, environment add_inner_inductive_declaration(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> implicit_infer_map, name_map<implicit_infer_kind> 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()); lean_assert(decl.get_inds().size() == decl.get_intro_rules().size());
if (is_trusted) { if (!is_meta) {
if (optional<environment> new_env = add_nested_inductive_decl(env, ngen, opts, implicit_infer_map, decl, if (optional<environment> 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); return register_ginductive_decl(*new_env, decl, ginductive_kind::NESTED);
} }
} }
if (decl.is_mutual()) { 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); decl, ginductive_kind::MUTUAL);
} else { } else {
lean_assert(!decl.is_mutual()); 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); decl, ginductive_kind::BASIC);
} }
} }

2
src/library/inductive_compiler/compiler.h
View file

@ -13,7 +13,7 @@ Author: Daniel Selsam
namespace lean { namespace lean {
environment add_inner_inductive_declaration(environment const & env, name_generator & ngen, options const & opts, environment add_inner_inductive_declaration(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> implicit_infer_map, name_map<implicit_infer_kind> implicit_infer_map,
ginductive_decl & decl, bool is_trusted); ginductive_decl & decl, bool is_meta);
void initialize_inductive_compiler(); void initialize_inductive_compiler();
void finalize_inductive_compiler(); void finalize_inductive_compiler();

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

@ -38,7 +38,7 @@ class add_mutual_inductive_decl_fn {
options const & m_opts; options const & m_opts;
name_map<implicit_infer_kind> m_implicit_infer_map; name_map<implicit_infer_kind> m_implicit_infer_map;
ginductive_decl const & m_mut_decl; ginductive_decl const & m_mut_decl;
bool m_is_trusted; bool m_is_meta;
ginductive_decl m_basic_decl; ginductive_decl m_basic_decl;
name m_basic_ind_name; 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";); << mlocal_name(ind) << " : " << new_ind_type << " :=\n " << new_ind_val << "\n";);
lean_assert(!has_local(new_ind_type)); lean_assert(!has_local(new_ind_type));
lean_assert(!has_local(new_ind_val)); 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); m_tctx.set_env(m_env);
} }
} }
@ -347,7 +347,7 @@ class add_mutual_inductive_decl_fn {
<< sizeof_name << " : " << sizeof_type << " :=\n " << sizeof_val << "\n";); << sizeof_name << " : " << sizeof_type << " :=\n " << sizeof_val << "\n";);
lean_assert(!has_local(sizeof_type)); lean_assert(!has_local(sizeof_type));
lean_assert(!has_local(sizeof_val)); 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_env = add_protected(m_env, sizeof_name);
m_tctx.set_env(m_env); 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";); << has_sizeof_name << " : " << has_sizeof_type << " :=\n " << has_sizeof_val << "\n";);
lean_assert(!has_local(has_sizeof_type)); lean_assert(!has_local(has_sizeof_type));
lean_assert(!has_local(has_sizeof_val)); 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_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true);
m_env = add_protected(m_env, sizeof_name); m_env = add_protected(m_env, sizeof_name);
m_tctx.set_env(m_env); m_tctx.set_env(m_env);
@ -421,7 +421,7 @@ class add_mutual_inductive_decl_fn {
lean_trace(name({"inductive_compiler", "mutual", "sizeof"}), tout() lean_trace(name({"inductive_compiler", "mutual", "sizeof"}), tout()
<< dsimp_rule_name << " : " << dsimp_rule_type << " :=\n " << dsimp_rule_val << "\n";); << 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 = mark_rfl_lemma(m_env, dsimp_rule_name);
m_env = add_eqn_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); 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_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()); 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";); 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); m_env = mk_injective_arrow(m_env, ir_name);
if (m_env.find(get_tactic_mk_inj_eq_name())) { if (m_env.find(get_tactic_mk_inj_eq_name())) {
name inj_eq_name = mk_injective_eq_name(ir_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_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); 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); m_tctx.set_env(m_env);
@ -499,7 +499,7 @@ class add_mutual_inductive_decl_fn {
lean_assert(!has_local(new_ir_val)); lean_assert(!has_local(new_ir_val));
lean_trace(name({"inductive_compiler", "mutual", "ir"}), tout() << mlocal_name(ir) << " : " << new_ir_type << "\n";); 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_env = set_pattern_attribute(m_env, mlocal_name(ir));
m_tctx.set_env(m_env); m_tctx.set_env(m_env);
basic_ir_idx++; basic_ir_idx++;
@ -779,7 +779,7 @@ class add_mutual_inductive_decl_fn {
lean_assert(!has_local(rec_type)); lean_assert(!has_local(rec_type));
lean_assert(!has_local(rec_val)); 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) { 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_type));
lean_assert(!has_local(cases_on_val)); 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() { void define_recursors() {
@ -876,9 +876,9 @@ class add_mutual_inductive_decl_fn {
public: public:
add_mutual_inductive_decl_fn(environment const & env, name_generator & ngen, options const & opts, add_mutual_inductive_decl_fn(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> const & implicit_infer_map, ginductive_decl const & mut_decl, name_map<implicit_infer_kind> 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_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_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) {} m_tctx(env, opts) {}
@ -895,7 +895,7 @@ public:
compute_idx_to_ir_range(); compute_idx_to_ir_range();
try { 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) { } catch (exception & ex) {
throw nested_exception(sstream() << "mutually inductive types compiled to invalid basic inductive type", 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, environment add_mutual_inductive_decl(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> const & implicit_infer_map, name_map<implicit_infer_kind> const & implicit_infer_map,
ginductive_decl & mut_decl, bool is_trusted) { ginductive_decl & mut_decl, bool is_meta) {
return add_mutual_inductive_decl_fn(env, ngen, opts, implicit_infer_map, mut_decl, is_trusted)(); return add_mutual_inductive_decl_fn(env, ngen, opts, implicit_infer_map, mut_decl, is_meta)();
} }
void initialize_inductive_compiler_mutual() { void initialize_inductive_compiler_mutual() {

2
src/library/inductive_compiler/mutual.h
View file

@ -12,7 +12,7 @@ Author: Daniel Selsam
namespace lean { namespace lean {
environment add_mutual_inductive_decl(environment const & env, name_generator & ngen, options const & opts, environment add_mutual_inductive_decl(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> const & implicit_infer_map, name_map<implicit_infer_kind> const & implicit_infer_map,
ginductive_decl & mut_decl, bool is_trusted); ginductive_decl & mut_decl, bool is_meta);
void initialize_inductive_compiler_mutual(); void initialize_inductive_compiler_mutual();
void finalize_inductive_compiler_mutual(); void finalize_inductive_compiler_mutual();

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

@ -87,7 +87,7 @@ class add_nested_inductive_decl_fn {
name_map<implicit_infer_kind> m_implicit_infer_map; name_map<implicit_infer_kind> m_implicit_infer_map;
// Note(dhs): m_nested_decl is morally const, but we make it non-const to pass around sizeof_lemmas // Note(dhs): m_nested_decl is morally const, but we make it non-const to pass around sizeof_lemmas
ginductive_decl & m_nested_decl; ginductive_decl & m_nested_decl;
bool m_is_trusted; bool m_is_meta;
ginductive_decl m_inner_decl; ginductive_decl m_inner_decl;
type_context_old m_tctx; type_context_old m_tctx;
@ -277,7 +277,7 @@ class add_nested_inductive_decl_fn {
void add_inner_decl() { void add_inner_decl() {
try { 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) { } catch (exception & ex) {
throw nested_exception(sstream() << "nested inductive type compiled to invalid inductive type", 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) { void define_theorem(name const & n, expr const & ty, expr const & val) {
assert_no_locals(n, ty); assert_no_locals(n, ty);
assert_no_locals(n, val); 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 { try {
m_env = module::add(m_env, check(m_env, d)); m_env = module::add(m_env, check(m_env, d));
lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << "\n";); 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) { 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, ty);
assert_no_locals(n, val); 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 { try {
m_env = module::add(m_env, check(m_env, d)); m_env = module::add(m_env, check(m_env, d));
lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << " :=\n " << val << "\n";); 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";); << has_sizeof_name << " : " << has_sizeof_type << " :=\n " << has_sizeof_val << "\n";);
lean_assert(!has_local(has_sizeof_type)); lean_assert(!has_local(has_sizeof_type));
lean_assert(!has_local(has_sizeof_val)); 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_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true);
m_env = add_protected(m_env, sizeof_name); m_env = add_protected(m_env, sizeof_name);
m_tctx.set_env(m_env); m_tctx.set_env(m_env);
@ -897,7 +897,7 @@ class add_nested_inductive_decl_fn {
lean_trace(name({"inductive_compiler", "nested", "sizeof"}), tout() lean_trace(name({"inductive_compiler", "nested", "sizeof"}), tout()
<< sizeof_spec_name << " : " << sizeof_spec_type << " :=\n " << sizeof_spec_val << "\n";); << 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";); lean_trace(name({"inductive_compiler", "nested", "sizeof"}), tout() << "[defined]: " << sizeof_spec_name << "\n";);
m_env = add_eqn_lemma(m_env, sizeof_spec_name); 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_PACK)));
args.push_back(to_obj(mk_primitive_name(fn_type::UNPACK))); 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)); 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_tctx.set_env(m_env);
m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); 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_PACK, nest_idx)));
args.push_back(to_obj(mk_nested_name(fn_type::UNPACK, 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)); 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_tctx.set_env(m_env);
m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); 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_PACK)));
args.push_back(to_obj(mk_pi_name(fn_type::UNPACK))); 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)); 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_tctx.set_env(m_env);
m_inj_lemmas = add(m_tctx, m_inj_lemmas, lemma_name, LEAN_DEFAULT_PRIORITY); 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); expr inj_val = prove_nested_injective(inj_type, m_inj_lemmas, inj_arrow_name);
m_env = module::add(m_env, m_env = module::add(m_env,
check(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); m_env = mk_injective_arrow(m_env, ir_name);
if (m_env.find(get_tactic_mk_inj_eq_name())) { if (m_env.find(get_tactic_mk_inj_eq_name())) {
name inj_eq_name = mk_injective_eq_name(ir_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_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); 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: public:
add_nested_inductive_decl_fn(environment const & env, name_generator & ngen, options const & opts, add_nested_inductive_decl_fn(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> const & implicit_infer_map, name_map<implicit_infer_kind> 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_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_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_nested_decl.get_num_indices(), m_nested_decl.get_ir_offsets()),
m_tctx(env, opts, transparency_mode::Semireducible) { } m_tctx(env, opts, transparency_mode::Semireducible) { }
@ -2347,8 +2347,8 @@ public:
optional<environment> add_nested_inductive_decl(environment const & env, name_generator & ngen, options const & opts, optional<environment> add_nested_inductive_decl(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> const & implicit_infer_map, name_map<implicit_infer_kind> const & implicit_infer_map,
ginductive_decl & decl, bool is_trusted) { ginductive_decl & decl, bool is_meta) {
return add_nested_inductive_decl_fn(env, ngen, opts, implicit_infer_map, decl, is_trusted)(); return add_nested_inductive_decl_fn(env, ngen, opts, implicit_infer_map, decl, is_meta)();
} }
void initialize_inductive_compiler_nested() { void initialize_inductive_compiler_nested() {

2
src/library/inductive_compiler/nested.h
View file

@ -12,7 +12,7 @@ Author: Daniel Selsam
namespace lean { namespace lean {
optional<environment> add_nested_inductive_decl(environment const & env, name_generator & ngen, options const & opts, optional<environment> add_nested_inductive_decl(environment const & env, name_generator & ngen, options const & opts,
name_map<implicit_infer_kind> const & implicit_infer_map, name_map<implicit_infer_kind> const & implicit_infer_map,
ginductive_decl & decl, bool is_trusted); ginductive_decl & decl, bool is_meta);
void initialize_inductive_compiler_nested(); void initialize_inductive_compiler_nested();
void finalize_inductive_compiler_nested(); void finalize_inductive_compiler_nested();

14
src/library/kernel_serializer.cpp
View file

@ -231,7 +231,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
k |= 1; k |= 1;
if (d.is_theorem() || d.is_axiom()) if (d.is_theorem() || d.is_axiom())
k |= 2; k |= 2;
if (d.is_trusted()) if (d.is_meta())
k |= 4; k |= 4;
s << k << d.get_name() << d.get_univ_params() << d.get_type(); s << k << d.get_name() << d.get_univ_params() << d.get_type();
if (d.is_definition()) { if (d.is_definition()) {
@ -246,7 +246,7 @@ declaration read_declaration(deserializer & d) {
char k = d.read_char(); char k = d.read_char();
bool has_value = (k & 1) != 0; bool has_value = (k & 1) != 0;
bool is_th_ax = (k & 2) != 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); name n = read_name(d);
level_param_names ps = read_level_params(d); level_param_names ps = read_level_params(d);
expr t = read_expr(d); expr t = read_expr(d);
@ -256,13 +256,13 @@ declaration read_declaration(deserializer & d) {
return mk_theorem(n, ps, t, v); return mk_theorem(n, ps, t, v);
} else { } else {
reducibility_hints hints = read_hints(d); 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 { } else {
if (is_th_ax) if (is_th_ax)
return mk_axiom(n, ps, t); return mk_axiom(n, ps, t);
else 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) { serializer & operator<<(serializer & s, certified_inductive_decl const & d) {
s << d.get_num_ACe() << d.elim_prop_only() << d.has_dep_elim() 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.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<certified_inductive_decl::comp_rule>(s, d.get_comp_rules()); write_list<certified_inductive_decl::comp_rule>(s, d.get_comp_rules());
return s; return s;
} }
@ -324,10 +324,10 @@ public:
inductive_decl decl = read_inductive_decl(d); inductive_decl decl = read_inductive_decl(d);
bool K = d.read_bool(); bool K = d.read_bool();
unsigned nind = d.read_unsigned(); unsigned nind = d.read_unsigned();
bool is_trusted = d.read_bool(); bool is_meta = d.read_bool();
auto rs = read_list<certified_inductive_decl::comp_rule>(d, read_comp_rule); auto rs = read_list<certified_inductive_decl::comp_rule>(d, read_comp_rule);
return certified_inductive_decl(nACe, elim_prop, dep_elim, ls, elim_type, decl, return certified_inductive_decl(nACe, elim_prop, dep_elim, ls, elim_type, decl,
K, nind, rs, is_trusted); K, nind, rs, is_meta);
} }
}; };

6
src/library/module.cpp
View file

@ -373,7 +373,7 @@ struct inductive_modification : public modification {
d.m_intro_rules = map(d.m_intro_rules, [&](inductive::intro_rule const & r) { d.m_intro_rules = map(d.m_intro_rules, [&](inductive::intro_rule const & r) {
return unfold_untrusted_macros(env, 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 { } else {
env = m_decl.add(env); env = m_decl.add(env);
} }
@ -464,8 +464,8 @@ using inductive::certified_inductive_decl;
environment add_inductive(environment env, environment add_inductive(environment env,
inductive::inductive_decl const & decl, inductive::inductive_decl const & decl,
bool is_trusted) { bool is_meta) {
pair<environment, certified_inductive_decl> r = inductive::add_inductive(env, decl, is_trusted); pair<environment, certified_inductive_decl> r = inductive::add_inductive(env, decl, is_meta);
environment new_env = r.first; environment new_env = r.first;
certified_inductive_decl cidecl = r.second; certified_inductive_decl cidecl = r.second;
module_ext ext = get_extension(env); module_ext ext = get_extension(env);

2
src/library/module.h
View file

@ -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. */ /** \brief Add the given inductive declaration to the environment, and mark it to be exported. */
environment add_inductive(environment env, environment add_inductive(environment env,
inductive::inductive_decl const & decl, 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. */ /** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */
environment declare_quotient(environment const & env); environment declare_quotient(environment const & env);

2
src/library/noncomputable.cpp
View file

@ -80,7 +80,7 @@ static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, n
if (ext.m_noncomputable.contains(n)) if (ext.m_noncomputable.contains(n))
return true; return true;
declaration const & d = env.get(n); declaration const & d = env.get(n);
if (!d.is_trusted()) { if (d.is_meta()) {
return false; /* ignore nontrusted definitions */ return false; /* ignore nontrusted definitions */
} else if (d.is_axiom() && !tc.is_prop(d.get_type())) { } else if (d.is_axiom() && !tc.is_prop(d.get_type())) {
return true; return true;

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

@ -796,9 +796,9 @@ format tactic_state::pp() const {
expr type = ctx.infer(code); expr type = ctx.infer(code);
environment new_env = ctx.env(); environment new_env = ctx.env();
bool use_conv_opt = true; bool use_conv_opt = true;
bool is_trusted = false; bool is_meta = true;
name pp_name("_pp_tactic_state"); 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 = new_env.add(cd);
new_env = vm_compile(new_env, new_env.get(pp_name)); new_env = vm_compile(new_env, new_env.get(pp_name));
vm_state S(new_env, get_options()); vm_state S(new_env, get_options());

14
src/library/unfold_macros.cpp
View file

@ -69,15 +69,9 @@ expr unfold_all_macros(environment const & env, expr const & e) {
return unfold_untrusted_macros(env, e, {}); return unfold_untrusted_macros(env, e, {});
} }
static bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) { static bool contains_untrusted_macro(unsigned /* trust_lvl */, declaration const & /* d */) {
#if defined(LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL) /* TODO(Leo): macros will be deleted */
if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) return false; 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());
} }
declaration unfold_untrusted_macros(environment const & env, declaration const & d, optional<unsigned> const & trust_lvl) { declaration unfold_untrusted_macros(environment const & env, declaration const & d, optional<unsigned> const & trust_lvl) {
@ -89,7 +83,7 @@ declaration unfold_untrusted_macros(environment const & env, declaration const &
} else if (d.is_definition()) { } else if (d.is_definition()) {
expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl); 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, 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()) { } else if (d.is_axiom()) {
return mk_axiom(d.get_name(), d.get_univ_params(), new_t); return mk_axiom(d.get_name(), d.get_univ_params(), new_t);
} else if (d.is_constant_assumption()) { } else if (d.is_constant_assumption()) {

2
src/library/update_declaration.cpp
View file

@ -30,7 +30,7 @@ static declaration update_declaration(declaration d, optional<level_param_names>
if (d.is_theorem()) if (d.is_theorem())
return mk_theorem(d.get_name(), _ps, _type, _value); return mk_theorem(d.get_name(), _ps, _type, _value);
else 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());
} }
} }

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

@ -236,10 +236,10 @@ environment interaction_monad<State>::evaluator::compile(name const & interactio
expr interaction_type = m_ctx.infer(interaction); expr interaction_type = m_ctx.infer(interaction);
environment new_env = m_ctx.env(); environment new_env = m_ctx.env();
bool use_conv_opt = true; bool use_conv_opt = true;
bool is_trusted = false; bool is_meta = true;
auto cd = check(new_env, auto cd = check(new_env,
mk_definition(new_env, interaction_name, {}, interaction_type, interaction, use_conv_opt, mk_definition(new_env, interaction_name, {}, interaction_type, interaction, use_conv_opt,
is_trusted)); is_meta));
new_env = new_env.add(cd); new_env = new_env.add(cd);
if (provider) { if (provider) {
if (auto pos = provider->get_pos_info(interaction)) if (auto pos = provider->get_pos_info(interaction))

12
src/library/vm/vm_declaration.cpp
View file

@ -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 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) { 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(trusted))); 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) { 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))); 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) { 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(trusted))); 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) { 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<vm_obj> & data) {
} else if (d.is_definition()) { } else if (d.is_definition()) {
data.push_back(to_obj(d.get_value())); data.push_back(to_obj(d.get_value()));
data.push_back(to_obj(d.get_hints())); 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; return 0;
} else { } else {
lean_assert(d.is_constant_assumption()); 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; return 2;
} }
} }

2
src/shell/leandoc.cpp
View file

@ -67,7 +67,7 @@ static void print_constant(std::ostream & out, environment const & env, formatte
format r; format r;
if (is_protected(env, d.get_name())) if (is_protected(env, d.get_name()))
add_string(r, "protected"); add_string(r, "protected");
if (!d.is_trusted()) if (d.is_meta())
add_string(r, "meta"); add_string(r, "meta");
if (d.is_definition() && is_marked_noncomputable(env, d.get_name())) if (d.is_definition() && is_marked_noncomputable(env, d.get_name()))
add_string(r, "noncomputable"); add_string(r, "noncomputable");