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

chore(*): meta ==> unsafe

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-15 14:59:28 -07:00
parent 5d466b1fd1
commit 0888dee25e
41 changed files with 250 additions and 252 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean4-mode/lean4-syntax.el
View file

@ -8,7 +8,7 @@
(require 'rx)
(defconst lean4-keywords1
'("import" "prelude" "protected" "private" "noncomputable" "definition" "meta" "renaming"
'("import" "prelude" "protected" "private" "noncomputable" "definition" "unsafe" "renaming"
"hiding" "exposing" "parameter" "parameters" "begin" "constant" "constants"
"lemma" "variable" "variables" "theorem" "example" "abbreviation"
"open" "export" "axiom" "axioms" "inductive" "coinductive" "with" "without"

8
library/init/core.lean
View file

@ -84,10 +84,10 @@ reserve infixl `; `:1
universes u v w
/-- Auxiliary meta constant used by the compiler when erasing proofs from code. -/
meta constant lc_proof {α : Prop} : α
/-- Auxiliary meta constant used by the compiler to mark unreachable code. -/
meta constant lc_unreachable {α : Sort u} : α
/-- Auxiliary unsafe constant used by the compiler when erasing proofs from code. -/
unsafe axiom lc_proof {α : Prop} : α
/-- Auxiliary unsafe constant used by the compiler to mark unreachable code. -/
unsafe axiom lc_unreachable {α : Sort u} : α
@[inline] def id {α : Sort u} (a : α) : α := a

2
library/init/io.lean
View file

@ -14,7 +14,7 @@ constant io.real_world : Type
def io : Type → Type := state io.real_world
@[extern "lean_io_unsafe"]
meta constant unsafe_io {α : Type} (fn : io α) : α
constant unsafe_io {α : Type} [inhabited α] (fn : io α) : α
@[extern 4 "lean_io_timeit"]
constant timeit {α : Type} (msg : @& string) (fn : io α) : io α

14
library/init/lean/declaration.lean
View file

@ -41,10 +41,10 @@ structure constant_val :=
(id : name) (lparams : list name) (type : expr)
structure axiom_val extends constant_val :=
(is_meta : bool)
(is_unsafe : bool)
structure definition_val extends constant_val :=
(value : expr) (hints : reducibility_hints) (is_meta : bool)
(value : expr) (hints : reducibility_hints) (is_unsafe : bool)
structure theorem_val extends constant_val :=
(value : task expr)
@ -61,8 +61,8 @@ inductive declaration
| defn_decl (val : definition_val)
| thm_decl (val : theorem_val)
| quot_decl
| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `meta`
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool)
| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `unsafe`
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_unsafe : bool)
/-- The kernel compiles (mutual) inductive declarations (see `inductive_decls`) into a set of
- `declaration.induct_decl` (for each inductive datatype in the mutual declaration),
@ -80,7 +80,7 @@ structure inductive_val extends constant_val :=
(all : list name) -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
(cnstrs : list name) -- List of all constructors for this inductive datatype
(is_rec : bool) -- `tt` iff it is recursive
(is_meta : bool)
(is_unsafe : bool)
(is_reflexive : bool)
structure constructor_val extends constant_val :=
@ -88,7 +88,7 @@ structure constructor_val extends constant_val :=
(cidx : nat) -- Constructor index (i.e., position in the inductive declaration)
(nparams : nat) -- Number of parameters in inductive datatype `induct`
(nfields : nat) -- Number of fields (i.e., arity - nparams)
(is_meta : bool)
(is_unsafe : bool)
/-- Information for reducing a recursor -/
structure recursor_rule :=
@ -104,7 +104,7 @@ structure recursor_val extends constant_val :=
(nminor : nat) -- Number of minor premises
(rules : list recursor_rule) -- A reduction for each constructor
(k : bool) -- It supports K-like reduction
(is_meta : bool)
(is_unsafe : bool)
inductive quot_kind
| type -- `quot`

2
library/init/lean/trace.lean
View file

@ -76,7 +76,7 @@ instance (m) [monad m] : monad_tracer (trace_t m) :=
}
}
meta def trace_t.run {m α} [monad m] (opts : options) (x : trace_t m α) : m (α × trace_map) :=
unsafe def trace_t.run {m α} [monad m] (opts : options) (x : trace_t m α) : m (α × trace_map) :=
do (a, st) ← state_t.run x {opts := opts, roots := mk_rbmap _ _ _, cur_pos := none, cur_traces := []},
pure (a, st.roots)

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

@ -100,8 +100,8 @@ static environment declare_var(parser & p, environment env,
collect_implicit_locals(p, new_ls, new_params, type);
expr new_type = Pi(new_params, type);
bool is_meta = meta.m_modifiers.m_is_meta;
env = module::add(env, mk_axiom(full_n, ls, new_type, is_meta));
bool is_unsafe = meta.m_modifiers.m_is_unsafe;
env = module::add(env, mk_axiom(full_n, ls, new_type, is_unsafe));
if (!ns.is_anonymous()) {
if (meta.m_modifiers.m_is_protected)
@ -283,8 +283,6 @@ static environment variable_cmd(parser & p, cmd_meta const & meta) {
return variable_cmd_core(p, variable_kind::Variable, meta);
}
static environment axiom_cmd(parser & p, cmd_meta const & meta) {
if (meta.m_modifiers.m_is_meta)
throw exception("invalid 'meta' modifier for axiom");
return variable_cmd_core(p, variable_kind::Axiom, meta);
}
static environment constant_cmd(parser & p, cmd_meta const & meta) {
@ -470,8 +468,8 @@ static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {
meta.m_modifiers.m_is_noncomputable = true;
}
}
if (p.curr_is_token(get_meta_tk())) {
meta.m_modifiers.m_is_meta = true;
if (p.curr_is_token(get_unsafe_tk())) {
meta.m_modifiers.m_is_unsafe = true;
p.next();
}
@ -481,7 +479,7 @@ static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {
}
if (p.curr_is_token(get_private_tk()) || p.curr_is_token(get_protected_tk()) || p.curr_is_token(get_noncomputable_tk())
|| p.curr_is_token(get_meta_tk()) || p.curr_is_token(get_mutual_tk())) {
|| p.curr_is_token(get_unsafe_tk()) || p.curr_is_token(get_mutual_tk())) {
throw parser_error("unexpected definition modifier", p.pos());
}
if (p.curr_is_token(get_attribute_tk()) || p.curr_is_token("@[")) {
@ -565,7 +563,7 @@ void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("variables", "declare new variables", variables_cmd));
add_cmd(r, cmd_info("constants", "declare new constants (aka top-level variables)", constants_cmd));
add_cmd(r, cmd_info("axioms", "declare new axioms", axioms_cmd));
add_cmd(r, cmd_info("meta", "add new meta declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("unsafe", "add new unsafe declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("mutual", "add new mutual declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("noncomputable", "add new noncomputable definition", modifiers_cmd, false));
add_cmd(r, cmd_info("private", "add new private declaration", modifiers_cmd, false));

38
src/frontends/lean/decl_util.cpp
View file

@ -398,12 +398,12 @@ struct definition_info {
name m_prefix; // prefix for local names
name m_actual_prefix; // actual prefix used to create kernel declaration names. m_prefix and m_actual_prefix are different for scoped/private declarations.
bool m_is_private{true}; // pattern matching outside of definitions should generate private names
/* m_is_meta_decl == true iff declaration uses `meta` keyword */
bool m_is_meta_decl{false};
/* m_is_meta == true iff the current subexpression can use meta declarations and code.
Remark: a regular (i.e., non meta) declaration provided by the user may contain a meta subexpression (e.g., tactic).
/* m_is_unsafe_decl == true iff declaration uses `unsafe` keyword */
bool m_is_unsafe_decl{false};
/* m_is_unsafe == true iff the current subexpression can use unsafe declarations and code.
Remark: a regular (i.e., safe) declaration provided by the user may contain a unsafe subexpression (e.g., tactic).
*/
bool m_is_meta{false}; // true iff current block
bool m_is_unsafe{false}; // true iff current block
bool m_is_noncomputable{false};
bool m_is_lemma{false};
bool m_aux_lemmas{false};
@ -422,11 +422,11 @@ declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind ki
info.m_actual_prefix = ns;
}
info.m_is_private = modifiers.m_is_private;
info.m_is_meta_decl = modifiers.m_is_meta;
info.m_is_meta = modifiers.m_is_meta;
info.m_is_unsafe_decl = modifiers.m_is_unsafe;
info.m_is_unsafe = modifiers.m_is_unsafe;
info.m_is_noncomputable = modifiers.m_is_noncomputable;
info.m_is_lemma = kind == decl_cmd_kind::Theorem;
info.m_aux_lemmas = kind != decl_cmd_kind::Theorem && !modifiers.m_is_meta;
info.m_aux_lemmas = kind != decl_cmd_kind::Theorem && !modifiers.m_is_unsafe;
info.m_gen_code = !is_extern;
info.m_next_match_idx = 1;
}
@ -451,7 +451,7 @@ equations_header mk_equations_header(names const & ns, names const & actual_ns)
h.m_fn_names = ns;
h.m_fn_actual_names = actual_ns;
h.m_is_private = get_definition_info().m_is_private;
h.m_is_meta = get_definition_info().m_is_meta;
h.m_is_unsafe = get_definition_info().m_is_unsafe;
h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
h.m_is_lemma = get_definition_info().m_is_lemma;
h.m_aux_lemmas = get_definition_info().m_aux_lemmas;
@ -557,25 +557,25 @@ match_definition_scope::match_definition_scope(environment const & env) {
}
}
meta_definition_scope::meta_definition_scope() {
unsafe_definition_scope::unsafe_definition_scope() {
definition_info & info = get_definition_info();
m_old_is_meta = info.m_is_meta;
info.m_is_meta = true;
m_old_is_unsafe = info.m_is_unsafe;
info.m_is_unsafe = true;
}
meta_definition_scope::~meta_definition_scope() {
unsafe_definition_scope::~unsafe_definition_scope() {
definition_info & info = get_definition_info();
info.m_is_meta = m_old_is_meta;
info.m_is_unsafe = m_old_is_unsafe;
}
restore_decl_meta_scope::restore_decl_meta_scope() {
restore_decl_unsafe_scope::restore_decl_unsafe_scope() {
definition_info & info = get_definition_info();
m_old_is_meta = info.m_is_meta;
info.m_is_meta = info.m_is_meta_decl;
m_old_is_unsafe = info.m_is_unsafe;
info.m_is_unsafe = info.m_is_unsafe_decl;
}
restore_decl_meta_scope::~restore_decl_meta_scope() {
restore_decl_unsafe_scope::~restore_decl_unsafe_scope() {
definition_info & info = get_definition_info();
info.m_is_meta = m_old_is_meta;
info.m_is_unsafe = m_old_is_unsafe;
}
}

24
src/frontends/lean/decl_util.h
View file

@ -19,12 +19,12 @@ enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var, Abbrevia
struct decl_modifiers {
bool m_is_private{false};
bool m_is_protected{false};
bool m_is_meta{false};
bool m_is_unsafe{false};
bool m_is_mutual{false};
bool m_is_noncomputable{false};
operator bool() const {
return m_is_private || m_is_protected || m_is_meta || m_is_mutual || m_is_noncomputable;
return m_is_private || m_is_protected || m_is_unsafe || m_is_mutual || m_is_noncomputable;
}
};
@ -90,25 +90,25 @@ public:
name const & get_actual_name() const { return m_actual_name; }
};
/** \brief Auxiliary scope to switch to `meta` mode when processing a
/** \brief Auxiliary scope to switch to `unsafe` mode when processing a
`by tac` in a regular definition.
We need this because we may have a match expression nested
in `tac`, and we should not create equation lemmas for it. */
class meta_definition_scope {
bool m_old_is_meta;
class unsafe_definition_scope {
bool m_old_is_unsafe;
public:
meta_definition_scope();
~meta_definition_scope();
unsafe_definition_scope();
~unsafe_definition_scope();
};
/** \brief Auxiliary scope to switch to the mode specified by the user.
That is, meta if the `meta` keyword was used, and regular otherwise.
That is, unsafe if the `unsafe` keyword was used, and regular otherwise.
We need this because of quoted expressions used in tactics. */
class restore_decl_meta_scope {
bool m_old_is_meta;
class restore_decl_unsafe_scope {
bool m_old_is_unsafe;
public:
restore_decl_meta_scope();
~restore_decl_meta_scope();
restore_decl_unsafe_scope();
~restore_decl_unsafe_scope();
};
/** \brief Return true if the current scope used match-expressions */

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

@ -196,12 +196,12 @@ declare_definition(environment const & env, decl_cmd_kind kind, buffer<name> con
if (env.find(c_real_name)) {
throw exception(sstream() << "invalid definition, a declaration named '" << c_real_name << "' has already been declared");
}
if (val && !meta.m_modifiers.m_is_meta && !type_checker(env).is_prop(type)) {
if (val && !meta.m_modifiers.m_is_unsafe && !type_checker(env).is_prop(type)) {
/* We only abstract nested proofs if the type of the definition is not a proposition */
std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type);
std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val);
}
bool is_meta = meta.m_modifiers.m_is_meta;
bool is_meta = meta.m_modifiers.m_is_unsafe;
auto def =
(kind == decl_cmd_kind::Theorem ?
mk_theorem(c_real_name, names(lp_names), type, *val) :
@ -472,7 +472,7 @@ static void check_example(environment const & decl_env, options const & opts,
buffer<name> univ_params_buf; to_buffer(univ_params, univ_params_buf);
finalize_definition(elab, params_buf, type, val, univ_params_buf);
bool is_meta = modifiers.m_is_meta;
bool is_meta = modifiers.m_is_unsafe;
auto new_env = elab.env();
declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta);
new_env = module::add(new_env, def);
@ -565,7 +565,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
environment new_env = env_n.first;
name c_real_name = env_n.second;
new_env = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
if (!meta.m_modifiers.m_is_meta && (kind == decl_cmd_kind::Definition || kind == decl_cmd_kind::Instance)) {
if (!meta.m_modifiers.m_is_unsafe && (kind == decl_cmd_kind::Definition || kind == decl_cmd_kind::Instance)) {
new_env = mk_smart_unfolding_definition(new_env, p.get_options(), c_real_name);
}
/* Apply attributes last so that they may access any information on the new decl */
@ -620,7 +620,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
bool is_instance = (kind == decl_cmd_kind::Instance);
bool is_abbrev = (kind == decl_cmd_kind::Abbreviation);
name prv_name;
std::tie(fn, val, prv_name) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta, is_abbrev);
std::tie(fn, val, prv_name) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_unsafe, is_abbrev);
// skip elaboration of definitions during reparsing
if (p.get_break_at_pos())

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

@ -721,7 +721,7 @@ public:
}
ind_types.push_back(inductive_type(local_name_p(r.m_inds[i]), Pi(r.m_params, local_type_p(r.m_inds[i])), constructors(cnstrs)));
}
m_env = module::add(m_env, mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_meta));
m_env = module::add(m_env, mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_unsafe));
bool has_eq = has_eq_decls(m_env);
bool has_heq = has_heq_decls(m_env);

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

@ -83,7 +83,7 @@ static void print_axioms(parser & p, message_builder & out) {
bool has_axioms = false;
p.env().for_each_constant([&](constant_info const & info) {
name const & n = info.get_name();
if (info.is_axiom() && !info.is_meta()) {
if (info.is_axiom() && !info.is_unsafe()) {
out << n << " : " << info.get_type() << endl;
has_axioms = true;
}
@ -255,8 +255,8 @@ static bool print_constant(parser const & p, message_builder & out, char const *
print_attributes(p, out, d.get_name());
if (is_protected(p.env(), d.get_name()))
out << "protected ";
if (d.is_meta())
out << "meta ";
if (d.is_unsafe())
out << "unsafe ";
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))
<< " : " << d.get_type();

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

@ -1063,10 +1063,10 @@ struct structure_cmd_fn {
expr structure_type = mk_structure_type();
expr intro_type = mk_intro_type();
names lnames = names(m_level_names);
bool is_meta = m_meta_info.m_modifiers.m_is_meta;
bool is_unsafe = m_meta_info.m_modifiers.m_is_unsafe;
constructor cnstr(m_mk, intro_type);
inductive_type S(m_name, structure_type, constructors(cnstr));
declaration decl = mk_inductive_decl(lnames, nat(m_params.size()), inductive_types(S), is_meta);
declaration decl = mk_inductive_decl(lnames, nat(m_params.size()), inductive_types(S), is_unsafe);
m_env = module::add(m_env, decl);
name rec_name = mk_rec_name(m_name);
m_env = add_namespace(m_env, m_name);
@ -1140,8 +1140,8 @@ struct structure_cmd_fn {
used_univs = collect_univ_params(decl_value, used_univs);
used_univs = collect_univ_params(decl_type, used_univs);
names decl_lvls = to_names(used_univs);
declaration new_decl = mk_definition_inferring_meta(m_env, decl_name, decl_lvls,
decl_type, decl_value, reducibility_hints::mk_abbreviation());
declaration new_decl = mk_definition_inferring_unsafe(m_env, decl_name, decl_lvls,
decl_type, decl_value, reducibility_hints::mk_abbreviation());
m_env = module::add(m_env, new_decl);
m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
}
@ -1151,9 +1151,9 @@ struct structure_cmd_fn {
void add_rec_on_alias(name const & n) {
name rec_on_name(m_name, "rec_on");
constant_info rec_on_decl = m_env.get(rec_on_name);
declaration new_decl = mk_definition_inferring_meta(m_env, n, rec_on_decl.get_lparams(),
rec_on_decl.get_type(), rec_on_decl.get_value(),
reducibility_hints::mk_abbreviation());
declaration new_decl = mk_definition_inferring_unsafe(m_env, n, rec_on_decl.get_lparams(),
rec_on_decl.get_type(), rec_on_decl.get_value(),
reducibility_hints::mk_abbreviation());
m_env = module::add(m_env, new_decl);
m_env = set_reducible(m_env, n, reducible_status::Reducible, true);
add_alias(n);
@ -1244,8 +1244,8 @@ struct structure_cmd_fn {
}
coercion_value = Fun_p(m_params, Fun_p(st, coercion_value));
name coercion_name = coercion_names[i];
declaration coercion_decl = mk_definition_inferring_meta(m_env, coercion_name, lnames,
coercion_type, coercion_value);
declaration coercion_decl = mk_definition_inferring_unsafe(m_env, coercion_name, lnames,
coercion_type, coercion_value);
m_env = module::add(m_env, coercion_decl);
add_alias(coercion_name);
m_env = compile(m_env, m_p.get_options(), coercion_name);

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

@ -102,7 +102,7 @@ void init_token_table(token_table & t) {
char const * commands[] =
{"theorem", "axiom", "axioms", "variable", "protected", "private", "hide",
"definition", "meta", "mutual", "example", "noncomputable", "abbreviation",
"definition", "unsafe", "mutual", "example", "noncomputable", "abbreviation",
"variables", "constant", "constants",
"using_well_founded", "[whnf]",
"end", "namespace", "section", "prelude",

8
src/frontends/lean/tokens.cpp
View file

@ -89,7 +89,7 @@ static name const * g_private_tk = nullptr;
static name const * g_protected_tk = nullptr;
static name const * g_inline_tk = nullptr;
static name const * g_definition_tk = nullptr;
static name const * g_meta_tk = nullptr;
static name const * g_unsafe_tk = nullptr;
static name const * g_mutual_tk = nullptr;
static name const * g_theorem_tk = nullptr;
static name const * g_axiom_tk = nullptr;
@ -215,7 +215,7 @@ void initialize_tokens() {
g_protected_tk = new name{"protected"};
g_inline_tk = new name{"inline"};
g_definition_tk = new name{"definition"};
g_meta_tk = new name{"meta"};
g_unsafe_tk = new name{"unsafe"};
g_mutual_tk = new name{"mutual"};
g_theorem_tk = new name{"theorem"};
g_axiom_tk = new name{"axiom"};
@ -342,7 +342,7 @@ void finalize_tokens() {
delete g_protected_tk;
delete g_inline_tk;
delete g_definition_tk;
delete g_meta_tk;
delete g_unsafe_tk;
delete g_mutual_tk;
delete g_theorem_tk;
delete g_axiom_tk;
@ -468,7 +468,7 @@ name const & get_private_tk() { return *g_private_tk; }
name const & get_protected_tk() { return *g_protected_tk; }
name const & get_inline_tk() { return *g_inline_tk; }
name const & get_definition_tk() { return *g_definition_tk; }
name const & get_meta_tk() { return *g_meta_tk; }
name const & get_unsafe_tk() { return *g_unsafe_tk; }
name const & get_mutual_tk() { return *g_mutual_tk; }
name const & get_theorem_tk() { return *g_theorem_tk; }
name const & get_axiom_tk() { return *g_axiom_tk; }

2
src/frontends/lean/tokens.h
View file

@ -91,7 +91,7 @@ name const & get_private_tk();
name const & get_protected_tk();
name const & get_inline_tk();
name const & get_definition_tk();
name const & get_meta_tk();
name const & get_unsafe_tk();
name const & get_mutual_tk();
name const & get_theorem_tk();
name const & get_axiom_tk();

2
src/frontends/lean/tokens.txt
View file

@ -84,7 +84,7 @@ private private
protected protected
inline inline
definition definition
meta meta
unsafe unsafe
mutual mutual
theorem theorem
axiom axiom

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

@ -183,7 +183,7 @@ environment elab_attribute_cmd(environment env, expr const & cmd) {
cmd_meta to_cmd_meta(environment const & env, expr const & e) {
auto const & data = mdata_data(e);
cmd_meta m(to_decl_attributes(env, mdata_expr(e), false));
m.m_modifiers.m_is_meta = get_bool(data, "meta").value_or(false);
m.m_modifiers.m_is_unsafe = get_bool(data, "unsafe").value_or(false);
m.m_modifiers.m_is_mutual = get_bool(data, "mutual").value_or(false);
m.m_modifiers.m_is_noncomputable = get_bool(data, "noncomputable").value_or(false);
m.m_modifiers.m_is_private = get_bool(data, "private").value_or(false);

88
src/kernel/declaration.cpp
View file

@ -41,19 +41,19 @@ constant_val::constant_val(name const & n, names const & lparams, expr const & t
object_ref(mk_cnstr(0, n, lparams, type)) {
}
axiom_val::axiom_val(name const & n, names const & lparams, expr const & type, bool is_meta):
axiom_val::axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), 1)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(is_meta));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*), static_cast<unsigned char>(is_unsafe));
}
bool axiom_val::is_meta() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)) != 0; }
bool axiom_val::is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)) != 0; }
definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_meta):
definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_unsafe):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), val, hints, 1)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*3, static_cast<unsigned char>(is_meta));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*3, static_cast<unsigned char>(is_unsafe));
}
bool definition_val::is_meta() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*3) != 0; }
bool definition_val::is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*3) != 0; }
theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
@ -71,50 +71,50 @@ recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const &
}
inductive_val::inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
unsigned nindices, names const & all, names const & cnstrs, bool rec, bool meta, bool is_refl):
unsigned nindices, names const & all, names const & cnstrs, bool rec, bool unsafe, bool is_refl):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), nat(nparams), nat(nindices), all, cnstrs, 3)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*5, static_cast<unsigned char>(rec));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*5 + 1, static_cast<unsigned char>(meta));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*5 + 1, static_cast<unsigned char>(unsafe));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*5 + 2, static_cast<unsigned char>(is_refl));
lean_assert(is_meta() == meta);
lean_assert(is_unsafe() == unsafe);
lean_assert(is_rec() == rec);
lean_assert(is_reflexive() == is_refl);
}
constructor_val::constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_meta):
constructor_val::constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), induct, nat(cidx), nat(nparams), nat(nfields), 1)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*5, static_cast<unsigned char>(is_meta));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*5, static_cast<unsigned char>(is_unsafe));
}
recursor_val::recursor_val(name const & n, names const & lparams, expr const & type,
names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
unsigned nminors, recursor_rules const & rules, bool k, bool is_meta):
unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), all, nat(nparams), nat(nindices), nat(nmotives),
nat(nminors), rules, 2)) {
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*7, static_cast<unsigned char>(k));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*7 + 1, static_cast<unsigned char>(is_meta));
cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*7 + 1, static_cast<unsigned char>(is_unsafe));
}
bool declaration::is_meta() const {
bool declaration::is_unsafe() const {
switch (kind()) {
case declaration_kind::Definition: return to_definition_val().is_meta();
case declaration_kind::Axiom: return to_axiom_val().is_meta();
case declaration_kind::Definition: return to_definition_val().is_unsafe();
case declaration_kind::Axiom: return to_axiom_val().is_unsafe();
case declaration_kind::Theorem: return false;
case declaration_kind::Inductive: return inductive_decl(*this).is_meta();
case declaration_kind::Inductive: return inductive_decl(*this).is_unsafe();
case declaration_kind::Quot: return false;
case declaration_kind::MutualDefinition: return true;
}
lean_unreachable();
}
bool use_meta(environment const & env, expr const & e) {
bool use_unsafe(environment const & env, expr const & e) {
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
if (found) return false;
if (is_constant(e)) {
if (auto info = env.find(const_name(e))) {
if (info->is_meta()) {
if (info->is_unsafe()) {
found = true;
return false;
}
@ -141,45 +141,45 @@ static unsigned get_max_height(environment const & env, expr const & v) {
return h;
}
definition_val mk_definition_val(environment const & env, name const & n, names const & params, expr const & t, expr const & v, bool meta) {
definition_val mk_definition_val(environment const & env, name const & n, names const & params, expr const & t, expr const & v, bool unsafe) {
unsigned h = get_max_height(env, v);
return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), meta);
return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), unsafe);
}
declaration mk_definition(name const & n, names const & params, expr const & t, expr const & v,
reducibility_hints const & h, bool meta) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), definition_val(n, params, t, v, h, meta)));
reducibility_hints const & h, bool unsafe) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), definition_val(n, params, t, v, h, unsafe)));
}
declaration mk_definition(environment const & env, name const & n, names const & params, expr const & t,
expr const & v, bool meta) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, meta)));
expr const & v, bool unsafe) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, unsafe)));
}
declaration mk_theorem(name const & n, names const & params, expr const & t, expr const & v) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, params, t, v)));
}
declaration mk_axiom(name const & n, names const & params, expr const & t, bool meta) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), axiom_val(n, params, t, meta)));
declaration mk_axiom(name const & n, names const & params, expr const & t, bool unsafe) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), axiom_val(n, params, t, unsafe)));
}
declaration mk_definition_inferring_meta(environment const & env, name const & n, names const & params,
declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & params,
expr const & t, expr const & v, reducibility_hints const & hints) {
bool meta = use_meta(env, t) || use_meta(env, v);
return mk_definition(n, params, t, v, hints, meta);
bool unsafe = use_unsafe(env, t) || use_unsafe(env, v);
return mk_definition(n, params, t, v, hints, unsafe);
}
declaration mk_definition_inferring_meta(environment const & env, name const & n, names const & params,
declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & params,
expr const & t, expr const & v) {
bool meta = use_meta(env, t) && use_meta(env, v);
bool unsafe = use_unsafe(env, t) && use_unsafe(env, v);
unsigned h = get_max_height(env, v);
return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), meta);
return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), unsafe);
}
declaration mk_axiom_inferring_meta(environment const & env, name const & n,
declaration mk_axiom_inferring_unsafe(environment const & env, name const & n,
names const & params, expr const & t) {
return mk_axiom(n, params, t, use_meta(env, t));
return mk_axiom(n, params, t, use_unsafe(env, t));
}
declaration mk_mutual_definitions(definition_vals const & ds) {
@ -199,13 +199,13 @@ inductive_type::inductive_type(name const & id, expr const & type, constructors
static unsigned inductive_decl_scalar_offset() { return sizeof(object*)*3; }
declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta) {
declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe) {
declaration r(mk_cnstr(static_cast<unsigned>(declaration_kind::Inductive), lparams, nparams, types, 1));
cnstr_set_scalar<unsigned char>(r.raw(), inductive_decl_scalar_offset(), static_cast<unsigned char>(is_meta));
cnstr_set_scalar<unsigned char>(r.raw(), inductive_decl_scalar_offset(), static_cast<unsigned char>(is_unsafe));
return r;
}
bool inductive_decl::is_meta() const { return cnstr_get_scalar<unsigned char>(raw(), inductive_decl_scalar_offset()) != 0; }
bool inductive_decl::is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), inductive_decl_scalar_offset()) != 0; }
// =======================================
// Constant info
@ -245,15 +245,15 @@ reducibility_hints const & constant_info::get_hints() const {
return *g_opaque;
}
bool constant_info::is_meta() const {
bool constant_info::is_unsafe() const {
switch (kind()) {
case constant_info_kind::Axiom: return to_axiom_val().is_meta();
case constant_info_kind::Definition: return to_definition_val().is_meta();
case constant_info_kind::Axiom: return to_axiom_val().is_unsafe();
case constant_info_kind::Definition: return to_definition_val().is_unsafe();
case constant_info_kind::Theorem: return false;
case constant_info_kind::Quot: return false;
case constant_info_kind::Inductive: return to_inductive_val().is_meta();
case constant_info_kind::Constructor: return to_constructor_val().is_meta();
case constant_info_kind::Recursor: return to_recursor_val().is_meta();
case constant_info_kind::Inductive: return to_inductive_val().is_unsafe();
case constant_info_kind::Constructor: return to_constructor_val().is_unsafe();
case constant_info_kind::Recursor: return to_recursor_val().is_unsafe();
}
lean_unreachable();
}

70
src/kernel/declaration.h
View file

@ -80,11 +80,11 @@ public:
/*
structure axiom_val extends constant_val :=
(is_meta : bool)
(is_unsafe : bool)
*/
class axiom_val : public object_ref {
public:
axiom_val(name const & n, names const & lparams, expr const & type, bool is_meta);
axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe);
axiom_val(axiom_val const & other):object_ref(other) {}
axiom_val(axiom_val && other):object_ref(other) {}
axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; }
@ -93,16 +93,16 @@ public:
name const & get_name() const { return to_constant_val().get_name(); }
names const & get_lparams() const { return to_constant_val().get_lparams(); }
expr const & get_type() const { return to_constant_val().get_type(); }
bool is_meta() const;
bool is_unsafe() const;
};
/*
structure definition_val extends constant_val :=
(value : expr) (hints : reducibility_hints) (is_meta : bool)
(value : expr) (hints : reducibility_hints) (is_unsafe : bool)
*/
class definition_val : public object_ref {
public:
definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_meta);
definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_unsafe);
definition_val(definition_val const & other):object_ref(other) {}
definition_val(definition_val && other):object_ref(other) {}
definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
@ -113,7 +113,7 @@ public:
expr const & get_type() const { return to_constant_val().get_type(); }
expr const & get_value() const { return static_cast<expr const &>(cnstr_get_ref(*this, 1)); }
reducibility_hints const & get_hints() const { return static_cast<reducibility_hints const &>(cnstr_get_ref(*this, 2)); }
bool is_meta() const;
bool is_unsafe() const;
};
typedef list_ref<definition_val> definition_vals;
@ -167,8 +167,8 @@ inductive declaration
| defn_decl (val : definition_val)
| thm_decl (val : theorem_val)
| quot_decl (id : name)
| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `meta`
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool)
| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `unsafe`
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_unsafe : bool)
*/
enum class declaration_kind { Axiom, Definition, Theorem, Quot, MutualDefinition, Inductive };
class declaration : public object_ref {
@ -193,7 +193,7 @@ public:
bool is_theorem() const { return kind() == declaration_kind::Theorem; }
bool is_mutual() const { return kind() == declaration_kind::MutualDefinition; }
bool is_inductive() const { return kind() == declaration_kind::Inductive; }
bool is_meta() const;
bool is_unsafe() const;
bool has_value() const { return is_theorem() || is_definition(); }
axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_get_ref(raw(), 0)); }
@ -213,34 +213,34 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
definition_val mk_definition_val(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, bool meta);
definition_val mk_definition_val(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
reducibility_hints const & hints, bool meta = false);
reducibility_hints const & hints, bool unsafe = false);
declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
bool meta = false);
bool unsafe = false);
declaration mk_theorem(name const & n, names const & lparams, expr const & t, expr const & v);
declaration mk_theorem(name const & n, names const & lparams, expr const & t, expr const & v);
declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool meta = false);
declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool unsafe = false);
declaration mk_mutual_definitions(definition_vals const & ds);
declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_meta);
declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe);
declaration mk_quot_decl();
/** \brief Return true iff \c e depends on meta-declarations */
bool use_meta(environment const & env, expr const & e);
/** \brief Return true iff \c e depends on unsafe-declarations */
bool use_unsafe(environment const & env, expr const & e);
/** \brief Similar to mk_definition but infer the value of meta flag.
That is, set it to true if \c t or \c v contains a meta declaration. */
declaration mk_definition_inferring_meta(environment const & env, name const & n, names const & lparams,
/** \brief Similar to mk_definition but infer the value of unsafe flag.
That is, set it to true if \c t or \c v contains a unsafe declaration. */
declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & lparams,
expr const & t, expr const & v, reducibility_hints const & hints);
declaration mk_definition_inferring_meta(environment const & env, name const & n, names const & lparams,
declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & lparams,
expr const & t, expr const & v);
/** \brief Similar to mk_axiom but infer the value of meta flag.
That is, set it to true if \c t or \c v contains a meta declaration. */
declaration mk_axiom_inferring_meta(environment const & env, name const & n,
/** \brief Similar to mk_axiom but infer the value of unsafe flag.
That is, set it to true if \c t or \c v contains a unsafe declaration. */
declaration mk_axiom_inferring_unsafe(environment const & env, name const & n,
names const & lparams, expr const & t);
/** \brief View for manipulating declaration.induct_decl constructor.
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool) */
| induct_decl (lparams : list name) (nparams : nat) (types : list inductive_type) (is_unsafe : bool) */
class inductive_decl : public object_ref {
public:
inductive_decl(inductive_decl const & other):object_ref(other) {}
@ -251,7 +251,7 @@ public:
names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(raw(), 0)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 1)); }
inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_get_ref(raw(), 2)); }
bool is_meta() const;
bool is_unsafe() const;
};
/*
@ -261,13 +261,13 @@ structure inductive_val extends constant_val :=
(all : list name) -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
(cnstrs : list name) -- List of all constructors for this inductive datatype
(is_rec : bool) -- `tt` iff it is recursive
(is_meta : bool)
(is_unsafe : bool)
(is_reflexive : bool)
*/
class inductive_val : public object_ref {
public:
inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
unsigned nindices, names const & all, names const & cnstrs, bool is_rec, bool is_meta, bool is_reflexive);
unsigned nindices, names const & all, names const & cnstrs, bool is_rec, bool is_unsafe, bool is_reflexive);
inductive_val(inductive_val const & other):object_ref(other) {}
inductive_val(inductive_val && other):object_ref(other) {}
inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
@ -279,7 +279,7 @@ public:
names const & get_cnstrs() const { return static_cast<names const &>(cnstr_get_ref(*this, 4)); }
unsigned get_ncnstrs() const { return length(get_cnstrs()); }
bool is_rec() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5) != 0; }
bool is_meta() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5 + 1) != 0; }
bool is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5 + 1) != 0; }
bool is_reflexive() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5 + 2) != 0; }
};
@ -289,11 +289,11 @@ structure constructor_val extends constant_val :=
(cidx : nat) -- Constructor index (i.e., position in the inductive declaration)
(nparams : nat) -- Number of parameters in inductive datatype `induct`
(nfields : nat) -- Number of fields (i.e., arity - nparams)
(is_meta : bool)
(is_unsafe : bool)
*/
class constructor_val : public object_ref {
public:
constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_meta);
constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe);
constructor_val(constructor_val const & other):object_ref(other) {}
constructor_val(constructor_val && other):object_ref(other) {}
constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
@ -303,7 +303,7 @@ public:
unsigned get_cidx() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }
unsigned get_nfields() const { return static_cast<nat const &>(cnstr_get_ref(*this, 4)).get_small_value(); }
bool is_meta() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5) != 0; }
bool is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*5) != 0; }
};
/*
@ -335,13 +335,13 @@ structure recursor_val extends constant_val :=
(nminors : nat) -- Number of minor premises
(rules : list recursor_rule) -- A reduction for each constructor
(k : bool) -- It supports K-like reduction
(is_meta : bool)
(is_unsafe : bool)
*/
class recursor_val : public object_ref {
public:
recursor_val(name const & n, names const & lparams, expr const & type,
names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
unsigned nminors, recursor_rules const & rules, bool k, bool is_meta);
unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe);
recursor_val(recursor_val const & other):object_ref(other) {}
recursor_val(recursor_val && other):object_ref(other) {}
recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
@ -357,7 +357,7 @@ public:
unsigned get_major_idx() const { return get_nparams() + get_nmotives() + get_nminors() + get_nindices(); }
recursor_rules const & get_rules() const { return static_cast<recursor_rules const &>(cnstr_get_ref(*this, 6)); }
bool is_k() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*7) != 0; }
bool is_meta() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*7 + 1) != 0; }
bool is_unsafe() const { return cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*7 + 1) != 0; }
};
enum class quot_kind { Type, Mk, Lift, Ind };
@ -420,7 +420,7 @@ public:
friend bool is_eqp(constant_info const & d1, constant_info const & d2) { return d1.raw() == d2.raw(); }
bool is_meta() const;
bool is_unsafe() const;
bool is_definition() const { return kind() == constant_info_kind::Definition; }
bool is_axiom() const { return kind() == constant_info_kind::Axiom; }

26
src/kernel/environment.cpp
View file

@ -77,32 +77,32 @@ static void check_constant_val(environment const & env, constant_val const & v,
checker.ensure_sort(sort, v.get_type());
}
static void check_constant_val(environment const & env, constant_val const & v, bool non_meta_only) {
type_checker checker(env, non_meta_only);
static void check_constant_val(environment const & env, constant_val const & v, bool safe_only) {
type_checker checker(env, safe_only);
check_constant_val(env, v, checker);
}
environment environment::add_axiom(declaration const & d, bool check) const {
axiom_val const & v = d.to_axiom_val();
if (check)
check_constant_val(*this, v.to_constant_val(), !d.is_meta());
check_constant_val(*this, v.to_constant_val(), !d.is_unsafe());
return add(constant_info(d));
}
environment environment::add_definition(declaration const & d, bool check) const {
definition_val const & v = d.to_definition_val();
if (v.is_meta()) {
if (v.is_unsafe()) {
/* Meta definition can be recursive.
So, we check the header, add, and then type check the body. */
if (check) {
bool non_meta_only = false;
type_checker checker(*this, non_meta_only);
bool safe_only = false;
type_checker checker(*this, safe_only);
check_constant_val(*this, v.to_constant_val(), checker);
}
environment new_env = add(constant_info(d));
if (check) {
bool non_meta_only = false;
type_checker checker(new_env, non_meta_only);
bool safe_only = false;
type_checker checker(new_env, safe_only);
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))
throw definition_type_mismatch_exception(new_env, d, val_type);
@ -137,10 +137,10 @@ environment environment::add_mutual(declaration const & d, bool check) const {
definition_vals const & vs = d.to_definition_vals();
/* Check declarations header */
if (check) {
bool non_meta_only = false;
type_checker checker(*this, non_meta_only);
bool safe_only = false;
type_checker checker(*this, safe_only);
for (definition_val const & v : vs) {
if (!v.is_meta())
if (!v.is_unsafe())
throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as meta");
check_constant_val(*this, v.to_constant_val(), checker);
}
@ -152,8 +152,8 @@ environment environment::add_mutual(declaration const & d, bool check) const {
}
/* Check actual definitions */
if (check) {
bool non_meta_only = false;
type_checker checker(new_env, non_meta_only);
bool safe_only = false;
type_checker checker(new_env, safe_only);
for (definition_val const & v : vs) {
expr val_type = checker.check(v.get_value(), v.get_lparams());
if (!checker.is_def_eq(val_type, v.get_type()))

22
src/kernel/inductive.cpp
View file

@ -79,7 +79,7 @@ class add_inductive_fn {
local_ctx m_lctx;
names m_lparams;
unsigned m_nparams;
bool m_is_meta;
bool m_is_unsafe;
buffer<inductive_type> m_ind_types;
buffer<unsigned> m_nindices;
level m_result_level;
@ -109,14 +109,14 @@ class add_inductive_fn {
public:
add_inductive_fn(environment const & env, inductive_decl const & decl):
m_env(env), m_ngen(*g_ind_fresh), m_lparams(decl.get_lparams()), m_is_meta(decl.is_meta()) {
m_env(env), m_ngen(*g_ind_fresh), m_lparams(decl.get_lparams()), m_is_unsafe(decl.is_unsafe()) {
if (!decl.get_nparams().is_small())
throw kernel_exception(env, "invalid inductive datatype, number of parameters is too big");
m_nparams = decl.get_nparams().get_small_value();
to_buffer(decl.get_types(), m_ind_types);
}
type_checker tc() { return type_checker(m_env, m_lctx, !m_is_meta); }
type_checker tc() { return type_checker(m_env, m_lctx, !m_is_unsafe); }
/** Return type of the parameter at position `i` */
expr get_param_type(unsigned i) const {
@ -271,7 +271,7 @@ public:
cnstr_names.push_back(constructor_name(cnstr));
}
m_env.add_core(constant_info(inductive_val(n, m_lparams, ind_type.get_type(), m_nparams, m_nindices[idx],
all, names(cnstr_names), rec, m_is_meta, reflexive)));
all, names(cnstr_names), rec, m_is_unsafe, reflexive)));
}
}
@ -369,7 +369,7 @@ public:
throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") "
<< "of '" << n << "' is too big for the corresponding inductive datatype");
}
if (!m_is_meta)
if (!m_is_unsafe)
check_positivity(binding_domain(t), n, i);
expr local = mk_local_decl_for(t);
t = instantiate(binding_body(t), local);
@ -397,7 +397,7 @@ public:
}
lean_assert(arity >= m_nparams);
unsigned nfields = arity - m_nparams;
m_env.add_core(constant_info(constructor_val(n, m_lparams, t, ind_type.get_name(), cidx, m_nparams, nfields, m_is_meta)));
m_env.add_core(constant_info(constructor_val(n, m_lparams, t, ind_type.get_name(), cidx, m_nparams, nfields, m_is_unsafe)));
cidx++;
}
}
@ -694,7 +694,7 @@ public:
names rec_lparams = get_rec_lparams();
m_env.add_core(constant_info(recursor_val(rec_name, rec_lparams, rec_ty, all,
m_nparams, m_nindices[d_idx], nmotives, nminors,
rules, m_K_target, m_is_meta)));
rules, m_K_target, m_is_unsafe)));
}
}
@ -994,7 +994,7 @@ struct elim_nested_inductive_fn {
m_new_types[qhead] = inductive_type(ind_type.get_name(), ind_type.get_type(), constructors(new_cnstrs));
qhead++;
}
declaration aux_decl = mk_inductive_decl(ind_d.get_lparams(), ind_d.get_nparams(), inductive_types(m_new_types), ind_d.is_meta());
declaration aux_decl = mk_inductive_decl(ind_d.get_lparams(), ind_d.get_nparams(), inductive_types(m_new_types), ind_d.is_unsafe());
return elim_nested_inductive_result(m_ngen, m_params, m_nested_aux, aux_decl);
}
};
@ -1071,7 +1071,7 @@ environment environment::add_inductive(declaration const & d) const {
new_env.add_core(constant_info(recursor_val(new_rec_name, rec_info.get_lparams(), new_rec_type,
all_ind_names, rec_val.get_nparams(), rec_val.get_nindices(), rec_val.get_nmotives(),
rec_val.get_nminors(), recursor_rules(new_rules),
rec_val.is_k(), rec_val.is_meta())));
rec_val.is_k(), rec_val.is_unsafe())));
};
for (inductive_type const & ind_type : ind_d.get_types()) {
constant_info ind_info = aux_env.get(ind_type.get_name());
@ -1082,14 +1082,14 @@ environment environment::add_inductive(declaration const & d) const {
new_env.add_core(constant_info(inductive_val(ind_info.get_name(), ind_info.get_lparams(), ind_info.get_type(),
ind_val.get_nparams(), ind_val.get_nindices(),
all_ind_names, ind_val.get_cnstrs(),
ind_val.is_rec(), ind_val.is_meta(), ind_val.is_reflexive())));
ind_val.is_rec(), ind_val.is_unsafe(), ind_val.is_reflexive())));
for (name const & cnstr_name : ind_val.get_cnstrs()) {
constant_info cnstr_info = aux_env.get(cnstr_name);
constructor_val cnstr_val = cnstr_info.to_constructor_val();
expr new_type = res.restore_nested(cnstr_info.get_type(), aux_env);
new_env.add_core(constant_info(constructor_val(cnstr_info.get_name(), cnstr_info.get_lparams(), new_type,
cnstr_val.get_induct(), cnstr_val.get_cidx(), cnstr_val.get_nparams(),
cnstr_val.get_nfields(), cnstr_val.is_meta())));
cnstr_val.get_nfields(), cnstr_val.is_unsafe())));
}
process_rec(mk_rec_name(ind_type.get_name()));
}

16
src/kernel/type_checker.cpp
View file

@ -81,8 +81,8 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) {
<< const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided");
if (!infer_only) {
if (m_non_meta_only && info.is_meta()) {
throw kernel_exception(env(), sstream() << "invalid declaration, it uses meta declaration '"
if (m_safe_only && info.is_unsafe()) {
throw kernel_exception(env(), sstream() << "invalid declaration, it uses unsafe declaration '"
<< const_name(e) << "'");
}
for (level const & l : ls)
@ -805,7 +805,7 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
if (is_proj(t_n) && is_proj(s_n) && proj_idx(t_n) == proj_idx(s_n) && is_def_eq(proj_expr(t_n), proj_expr(s_n)))
return true;
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
// At this point, t_n and s_n are in weak head normal form (modulo metavariables and proof irrelevance)
if (is_def_eq_app(t_n, s_n))
return true;
@ -845,19 +845,19 @@ expr type_checker::eta_expand(expr const & e) {
return m_lctx.mk_lambda(fvars, r);
}
type_checker::type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only):
type_checker::type_checker(environment const & env, local_ctx const & lctx, bool safe_only):
m_st_owner(true), m_st(new state(env)),
m_lctx(lctx), m_non_meta_only(non_meta_only), m_lparams(nullptr) {
m_lctx(lctx), m_safe_only(safe_only), m_lparams(nullptr) {
}
type_checker::type_checker(state & st, local_ctx const & lctx, bool non_meta_only):
type_checker::type_checker(state & st, local_ctx const & lctx, bool safe_only):
m_st_owner(false), m_st(&st), m_lctx(lctx),
m_non_meta_only(non_meta_only), m_lparams(nullptr) {
m_safe_only(safe_only), m_lparams(nullptr) {
}
type_checker::type_checker(type_checker && src):
m_st_owner(src.m_st_owner), m_st(src.m_st), m_lctx(std::move(src.m_lctx)),
m_non_meta_only(src.m_non_meta_only), m_lparams(src.m_lparams) {
m_safe_only(src.m_safe_only), m_lparams(src.m_lparams) {
src.m_st_owner = false;
}

10
src/kernel/type_checker.h
View file

@ -43,7 +43,7 @@ private:
bool m_st_owner;
state * m_st;
local_ctx m_lctx;
bool m_non_meta_only;
bool m_safe_only;
/* When `m_lparams != nullptr, the `check` method makes sure all level parameters
are in `m_lparams`. */
names const * m_lparams;
@ -88,10 +88,10 @@ private:
expr check_ignore_undefined_universes(expr const & e);
public:
type_checker(state & st, local_ctx const & lctx, bool non_meta_only = true);
type_checker(state & st, bool non_meta_only = true):type_checker(st, local_ctx(), non_meta_only) {}
type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only = true);
type_checker(environment const & env, bool non_meta_only = true):type_checker(env, local_ctx(), non_meta_only) {}
type_checker(state & st, local_ctx const & lctx, bool safe_only = true);
type_checker(state & st, bool safe_only = true):type_checker(st, local_ctx(), safe_only) {}
type_checker(environment const & env, local_ctx const & lctx, bool safe_only = true);
type_checker(environment const & env, bool safe_only = true):type_checker(env, local_ctx(), safe_only) {}
type_checker(type_checker &&);
type_checker(type_checker const &) = delete;
~type_checker();

24
src/library/aux_definition.cpp
View file

@ -150,22 +150,22 @@ buffer<expr> const & closure_helper::get_norm_closure_params() const {
struct mk_aux_definition_fn : public closure_helper {
mk_aux_definition_fn(type_context_old & ctx):closure_helper(ctx) {}
pair<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 == false);
pair<environment, expr> operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional<bool> is_unsafe) {
lean_assert(!is_lemma || is_unsafe);
lean_assert(!is_lemma || *is_unsafe == false);
expr new_type = collect(ctx().instantiate_mvars(type));
expr new_value = collect(ctx().instantiate_mvars(value));
environment env = ctx().env();
finalize_collection();
expr def_type = mk_pi_closure(new_type);
expr def_value = mk_lambda_closure(new_value);
if (!is_meta)
is_meta = use_meta(env, def_type) || use_meta(env, def_value);
if (!is_unsafe)
is_unsafe = use_unsafe(env, def_type) || use_unsafe(env, def_value);
declaration d;
if (is_lemma) {
d = mk_theorem(c, get_norm_level_names(), def_type, def_value);
} else {
d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, *is_meta);
d = mk_definition(env, c, get_norm_level_names(), def_type, def_value, *is_unsafe);
}
environment new_env = module::add(env, d);
buffer<level> ls;
@ -178,26 +178,26 @@ struct mk_aux_definition_fn : public closure_helper {
};
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & type, expr const & value, optional<bool> const & is_meta) {
name const & c, expr const & type, expr const & value, optional<bool> const & is_unsafe) {
type_context_old ctx(env, options(), mctx, lctx, transparency_mode::All);
bool is_lemma = false;
return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_meta);
return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_unsafe);
}
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & value, optional<bool> const & is_meta) {
name const & c, expr const & value, optional<bool> const & is_unsafe) {
type_context_old ctx(env, options(), mctx, lctx, transparency_mode::All);
expr type = ctx.infer(value);
bool is_lemma = false;
return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_meta);
return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_unsafe);
}
pair<environment, expr> mk_aux_lemma(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & type, expr const & value) {
type_context_old ctx(env, options(), mctx, lctx, transparency_mode::All);
bool is_lemma = true;
optional<bool> is_meta(false);
return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_meta);
optional<bool> is_unsafe(false);
return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_unsafe);
}
struct abstract_nested_proofs_fn : public replace_visitor_with_tc {

2
src/library/compiler/compiler.cpp
View file

@ -35,7 +35,7 @@ bool is_codegen_enabled(options const & opts) {
}
static name get_real_name(name const & n) {
if (optional<name> new_n = is_meta_rec_name(n))
if (optional<name> new_n = is_unsafe_rec_name(n))
return *new_n;
else
return n;

2
src/library/compiler/lcnf.cpp
View file

@ -368,7 +368,7 @@ public:
return visit_no_confusion(fn, args, root);
} else if (is_constructor(env(), const_name(fn))) {
return visit_constructor(fn, args, root);
} else if (optional<name> n = is_meta_rec_name(const_name(fn))) {
} else if (optional<name> n = is_unsafe_rec_name(const_name(fn))) {
fn = mk_constant(*n, const_levels(fn));
return visit_app_default(fn, args, root);
} else if (is_quot_primitive(env(), const_name(fn))) {

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

@ -139,8 +139,8 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
expr below_type = lctx.mk_pi(args, Type_result);
expr below_value = lctx.mk_lambda(args, rec);
declaration new_d = mk_definition_inferring_meta(env, below_name, blvls, below_type, below_value,
reducibility_hints::mk_abbreviation());
declaration new_d = mk_definition_inferring_unsafe(env, below_name, blvls, below_type, below_value,
reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, new_d);
new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true);
return add_protected(new_env, below_name);
@ -340,8 +340,8 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
expr brec_on_value = lctx.mk_lambda(args, mk_pprod_fst(tc, rec, ind));
declaration new_d = mk_definition_inferring_meta(env, brec_on_name, blps, brec_on_type, brec_on_value,
reducibility_hints::mk_abbreviation());
declaration new_d = mk_definition_inferring_unsafe(env, brec_on_name, blps, brec_on_type, brec_on_value,
reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, new_d);
new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, brec_on_name);

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

@ -179,8 +179,8 @@ environment mk_cases_on(environment const & env, name const & n) {
expr cases_on_type = lctx.mk_pi(cases_on_params, rec_type);
expr cases_on_value = lctx.mk_lambda(cases_on_params, mk_app(rec_cnst, rec_args));
declaration new_d = mk_definition_inferring_meta(env, cases_on_name, rec_info.get_lparams(), cases_on_type, cases_on_value,
reducibility_hints::mk_abbreviation());
declaration new_d = mk_definition_inferring_unsafe(env, cases_on_name, rec_info.get_lparams(), cases_on_type, cases_on_value,
reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, new_d);
new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, cases_on_name);

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

@ -118,8 +118,8 @@ static optional<environment> mk_no_confusion_type(environment const & env, name
t1 = binding_body(t1);
}
expr no_confusion_type_value = lctx.mk_lambda(args, mk_app(cases_on1, outer_cases_on_args));
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());
declaration new_d = mk_definition_inferring_unsafe(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
reducibility_hints::mk_abbreviation());
environment new_env = module::add(env, new_d);
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible, true);
return some(add_protected(new_env, no_confusion_type_name));
@ -228,8 +228,8 @@ environment mk_no_confusion(environment const & env, name const & n) {
eq_rec = mk_app(mk_app(eq_rec, rec_type_former, gen, v2, H12), H12);
//
expr no_confusion_val = lctx.mk_lambda(args, eq_rec);
declaration new_d = mk_definition_inferring_meta(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
reducibility_hints::mk_abbreviation());
declaration new_d = mk_definition_inferring_unsafe(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
reducibility_hints::mk_abbreviation());
new_env = module::add(new_env, new_d);
new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible, true);
new_env = add_no_confusion(new_env, no_confusion_name);

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

@ -98,7 +98,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
proj_type = infer_implicit_params(proj_type, nparams, infer_kinds[i]);
expr proj_val = mk_proj(n, i, c);
proj_val = lctx.mk_lambda(proj_args, proj_val);
declaration new_d = mk_definition_inferring_meta(env, proj_name, lvl_params, proj_type, proj_val,
declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
reducibility_hints::mk_abbreviation());
new_env = module::add(new_env, new_d);
new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);

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

@ -55,8 +55,8 @@ environment mk_rec_on(environment const & env, name const & n) {
expr rec_on_val = lctx.mk_lambda(new_locals, mk_app(rec, locals));
environment new_env = module::add(env,
mk_definition_inferring_meta(env, rec_on_name, rec_info.get_lparams(),
rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation()));
mk_definition_inferring_unsafe(env, rec_on_name, rec_info.get_lparams(),
rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation()));
new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible, true);
new_env = add_aux_recursor(new_env, rec_on_name);
return add_protected(new_env, rec_on_name);

2
src/library/derive_attribute.cpp
View file

@ -126,7 +126,7 @@ static environment derive(environment env, options const & opts, name const & n,
auto inst2 = ctx.mk_lambda(params, inst.value());
auto new_n = n + const_name(cls);
env = module::add(env, mk_definition(env, new_n, d.get_lparams(),
ctx.instantiate_mvars(tgt), inst2, d.is_meta()));
ctx.instantiate_mvars(tgt), inst2, d.is_unsafe()));
env = add_instance(env, new_n, LEAN_DEFAULT_PRIORITY, true);
env = add_protected(env, new_n);
env = compile(env, opts, new_n);

18
src/library/equations_compiler/compiler.cpp
View file

@ -38,11 +38,11 @@ static eqn_compiler_result compile_equations_core(environment & env, elaborator
trace_compiler(tout() << "nested recursion: " << has_nested_rec(eqns) << "\n";);
trace_compiler(tout() << "using_well_founded: " << is_wf_equations(eqns) << "\n";);
equations_header const & header = get_equations_header(eqns);
lean_assert(header.m_is_meta || !has_nested_rec(eqns));
lean_assert(header.m_is_unsafe || !has_nested_rec(eqns));
if (header.m_is_meta) {
if (header.m_is_unsafe) {
if (is_wf_equations(eqns)) {
throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion");
throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for unsafe definitions, since they can use unbounded recursion");
}
return unbounded_rec(env, elab, mctx, lctx, eqns);
}
@ -352,7 +352,7 @@ static expr compile_equations_main(environment & env, elaborator & elab,
expr eqns = eta_expand_rec_apps_fn(ctx)(_eqns);
equations_header const & header = get_equations_header(eqns);
eqn_compiler_result r;
if (!header.m_is_meta && has_nested_rec(eqns)) {
if (!header.m_is_unsafe && has_nested_rec(eqns)) {
r = pull_nested_rec_fn(env, elab, mctx, lctx)(eqns);
} else {
r = compile_equations_core(env, elab, mctx, lctx, eqns);
@ -374,7 +374,7 @@ static expr compile_equations_main(environment & env, elaborator & elab,
expr compile_equations(environment & env, elaborator & elab, metavar_context & mctx, local_context const & lctx, expr const & eqns) {
equations_header const & header = get_equations_header(eqns);
type_context_old ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
if (!header.m_is_meta &&
if (!header.m_is_unsafe &&
!header.m_is_lemma &&
!header.m_is_noncomputable &&
/* Remark: we don't need special compilation scheme for non recursive equations */
@ -383,15 +383,15 @@ expr compile_equations(environment & env, elaborator & elab, metavar_context & m
equations_header new_header = header;
new_header.m_gen_code = false;
expr result = compile_equations_main(env, elab, mctx, lctx, update_equations(eqns, new_header), true);
/* Then, we compile the equations again using `meta` and generate code.
/* Then, we compile the equations again using `unsafe` and generate code.
The motivations are:
- Clear execution cost semantics for recursive functions.
- Auxiliary meta definition may assist recursive definition unfolding in the type_context_old object.
- Auxiliary unsafe definition may assist recursive definition unfolding in the type_context_old object.
*/
equations_header aux_header = header;
aux_header.m_is_meta = true;
aux_header.m_is_unsafe = true;
aux_header.m_aux_lemmas = false;
aux_header.m_fn_actual_names = map(header.m_fn_actual_names, mk_meta_rec_name);
aux_header.m_fn_actual_names = map(header.m_fn_actual_names, mk_unsafe_rec_name);
expr aux_eqns = remove_wf_annotation_from_equations(update_equations(eqns, aux_header));
compile_equations_main(env, elab, mctx, lctx, aux_eqns, false);
return result;

2
src/library/equations_compiler/elim_match.cpp
View file

@ -1291,7 +1291,7 @@ eqn_compiler_result mk_nonrec(environment & env, elaborator & elab, metavar_cont
local_context const & lctx, expr const & eqns) {
equations_header header = get_equations_header(eqns);
auto R = elim_match(env, elab, mctx, lctx, eqns);
if (header.m_is_meta || header.m_is_lemma) {
if (header.m_is_unsafe || header.m_is_lemma) {
/* Do not generate auxiliary equation or equational lemmas */
auto fn = mk_constant(head(header.m_fn_names));
auto counter_examples = map2<expr>(R.m_counter_examples, [&] (list<expr> const & e) { return mk_app(fn, e); });

6
src/library/equations_compiler/equations.cpp
View file

@ -40,7 +40,7 @@ bool operator==(equations_header const & h1, equations_header const & h2) {
h1.m_fn_actual_names == h2.m_fn_actual_names &&
h1.m_is_private == h2.m_is_private &&
h1.m_is_lemma == h2.m_is_lemma &&
h1.m_is_meta == h2.m_is_meta &&
h1.m_is_unsafe == h2.m_is_unsafe &&
h1.m_is_noncomputable == h2.m_is_noncomputable &&
h1.m_aux_lemmas == h2.m_aux_lemmas &&
h1.m_prev_errors == h2.m_prev_errors &&
@ -154,7 +154,7 @@ equations_header get_equations_header(expr const & e) {
h.m_num_fns = get_nat(m, name(*g_equations_name, "num_fns"))->get_small_value();
h.m_is_private = *get_bool(m, name(*g_equations_name, "is_private"));
h.m_is_lemma = *get_bool(m, name(*g_equations_name, "is_lemma"));
h.m_is_meta = *get_bool(m, name(*g_equations_name, "is_meta"));
h.m_is_unsafe = *get_bool(m, name(*g_equations_name, "is_unsafe"));
h.m_is_noncomputable = *get_bool(m, name(*g_equations_name, "is_noncomputable"));
h.m_aux_lemmas = *get_bool(m, name(*g_equations_name, "aux_lemmas"));
h.m_prev_errors = *get_bool(m, name(*g_equations_name, "prev_errors"));
@ -196,7 +196,7 @@ expr mk_equations(equations_header const & h, unsigned num_eqs, expr const * eqs
m = set_nat(m, name(*g_equations_name, "num_fns"), h.m_num_fns);
m = set_bool(m, name(*g_equations_name, "is_private"), h.m_is_private);
m = set_bool(m, name(*g_equations_name, "is_lemma"), h.m_is_lemma);
m = set_bool(m, name(*g_equations_name, "is_meta"), h.m_is_meta);
m = set_bool(m, name(*g_equations_name, "is_unsafe"), h.m_is_unsafe);
m = set_bool(m, name(*g_equations_name, "is_noncomputable"), h.m_is_noncomputable);
m = set_bool(m, name(*g_equations_name, "aux_lemmas"), h.m_aux_lemmas);
m = set_bool(m, name(*g_equations_name, "prev_errors"), h.m_prev_errors);

2
src/library/equations_compiler/equations.h
View file

@ -43,7 +43,7 @@ struct equations_header {
names m_fn_actual_names; /* Full qualified name and/or private name */
bool m_is_private{false}; /* if true, it must be a private definition */
bool m_is_lemma{false}; /* if true, equations are defining a lemma */
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
bool m_is_unsafe{false}; /* the auxiliary declarations should be tagged as unsafe */
bool m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */
bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */
/* m_prev_errors is true when errors have already being found processing the file,

2
src/library/equations_compiler/structural_rec.cpp
View file

@ -701,7 +701,7 @@ struct structural_rec_fn {
brec_on_args.push_back(F);
expr new_fn = ctx.mk_lambda(fn_args, mk_app(mk_app(brec_on_fn, brec_on_args), extra_args));
lean_trace("eqn_compiler", tout() << "result:\n" << new_fn << "\ntype:\n" << ctx.infer(new_fn) << "\n";);
if (m_header.m_is_meta) {
if (m_header.m_is_unsafe) {
/* We don't create auxiliary definitions for meta-definitions because we don't create lemmas
for them. */
return new_fn;

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

@ -498,7 +498,7 @@ environment mk_smart_unfolding_definition(environment const & env, options const
return env;
}
name meta_aux_fn_name = mk_meta_rec_name(fn_name);
name meta_aux_fn_name = mk_unsafe_rec_name(fn_name);
expr helper_value;
if (optional<constant_info> aux_info = env.find(meta_aux_fn_name)) {

10
src/library/util.cpp
View file

@ -991,14 +991,14 @@ name get_dep_cases_on(environment const &, name const & n) {
return name(n, "cases_on");
}
static char const * g_meta_rec_prefix = "_meta_rec";
static char const * g_unsafe_rec_prefix = "_unsafe_rec";
name mk_meta_rec_name(name const & n) {
return name(n, g_meta_rec_prefix);
name mk_unsafe_rec_name(name const & n) {
return name(n, g_unsafe_rec_prefix);
}
optional<name> is_meta_rec_name(name const & n) {
if (!n.is_atomic() && n.is_string() && n.get_string() == g_meta_rec_prefix) {
optional<name> is_unsafe_rec_name(name const & n) {
if (!n.is_atomic() && n.is_string() && n.get_string() == g_unsafe_rec_prefix) {
return optional<name>(n.get_prefix());
} else {
return optional<name>();

12
src/library/util.h
View file

@ -299,13 +299,13 @@ name get_dep_recursor(environment const & env, name const & n);
even if \c n is an inductive predicate. */
name get_dep_cases_on(environment const & env, name const & n);
/** We generate auxiliary meta definitions for regular recursive definitions.
The auxiliary meta definition has a clear runtime cost execution model, and
we use it in the VM. This function returns an auxiliary meta definition for the given name. */
name mk_meta_rec_name(name const & n);
/** We generate auxiliary unsafe definitions for regular recursive definitions.
The auxiliary unsafe definition has a clear runtime cost execution model, and
we use it in the VM and code generators. This function returns an auxiliary unsafe definition for the given name. */
name mk_unsafe_rec_name(name const & n);
/** Return some(n') if \c n is a name created using mk_meta_rec_name(n') */
optional<name> is_meta_rec_name(name const & n);
/** Return some(n') if \c n is a name created using mk_unsafe_rec_name(n') */
optional<name> is_unsafe_rec_name(name const & n);
/** Convert an expression representing a `name` literal into a `name` object. */
optional<name> name_lit_to_name(expr const & name_lit);

4
src/runtime/io.cpp
View file

@ -67,8 +67,8 @@ extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg /* h */, obj_arg /* w
lean_unreachable();
}
/* unsafe_io {α : Type} (fn : io α) : α */
extern "C" obj_res lean_io_unsafe(obj_arg, obj_arg fn) {
/* constant unsafe_io {α : Type} [inhabited α] (fn : io α) : α */
extern "C" obj_res lean_io_unsafe(obj_arg, obj_arg, obj_arg fn) {
object * r = apply_1(fn, REAL_WORLD);
object * a = cnstr_get(r, 0);
inc(a); dec(r);