From 0888dee25e2fd53d4c3e621fd10c6775e945a01c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Mar 2019 14:59:28 -0700 Subject: [PATCH] chore(*): `meta` ==> `unsafe` --- lean4-mode/lean4-syntax.el | 2 +- library/init/core.lean | 8 +- library/init/io.lean | 2 +- library/init/lean/declaration.lean | 14 +-- library/init/lean/trace.lean | 2 +- src/frontends/lean/decl_cmds.cpp | 14 ++- src/frontends/lean/decl_util.cpp | 38 ++++---- src/frontends/lean/decl_util.h | 24 ++--- src/frontends/lean/definition_cmds.cpp | 10 +-- src/frontends/lean/inductive_cmds.cpp | 2 +- src/frontends/lean/print_cmd.cpp | 6 +- src/frontends/lean/structure_cmd.cpp | 18 ++-- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 8 +- src/frontends/lean/tokens.h | 2 +- src/frontends/lean/tokens.txt | 2 +- src/frontends/lean/vm_elaborator.cpp | 2 +- src/kernel/declaration.cpp | 88 +++++++++---------- src/kernel/declaration.h | 70 +++++++-------- src/kernel/environment.cpp | 26 +++--- src/kernel/inductive.cpp | 22 ++--- src/kernel/type_checker.cpp | 16 ++-- src/kernel/type_checker.h | 10 +-- src/library/aux_definition.cpp | 24 ++--- src/library/compiler/compiler.cpp | 2 +- src/library/compiler/lcnf.cpp | 2 +- src/library/constructions/brec_on.cpp | 8 +- src/library/constructions/cases_on.cpp | 4 +- src/library/constructions/no_confusion.cpp | 8 +- src/library/constructions/projection.cpp | 2 +- src/library/constructions/rec_on.cpp | 4 +- src/library/derive_attribute.cpp | 2 +- src/library/equations_compiler/compiler.cpp | 18 ++-- src/library/equations_compiler/elim_match.cpp | 2 +- src/library/equations_compiler/equations.cpp | 6 +- src/library/equations_compiler/equations.h | 2 +- .../equations_compiler/structural_rec.cpp | 2 +- src/library/equations_compiler/util.cpp | 2 +- src/library/util.cpp | 10 +-- src/library/util.h | 12 +-- src/runtime/io.cpp | 4 +- 41 files changed, 250 insertions(+), 252 deletions(-) diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index a978b11bd6..35cd6e1ce8 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -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" diff --git a/library/init/core.lean b/library/init/core.lean index 4a185b6719..d6d74c68af 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -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 diff --git a/library/init/io.lean b/library/init/io.lean index a75b5783c0..cca8ef8434 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -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 α diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean index 5ceeed89e9..08b8814210 100644 --- a/library/init/lean/declaration.lean +++ b/library/init/lean/declaration.lean @@ -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` diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 1d4f28a442..07d237b0f5 100644 --- a/library/init/lean/trace.lean +++ b/library/init/lean/trace.lean @@ -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) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index ace4c804dd..34db74970c 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -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)); diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 25a36b66a9..a030ed8abe 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -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; } } diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index 0108cd9820..5523a80597 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -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 */ diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 0bcf49a247..93f9181648 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -196,12 +196,12 @@ declare_definition(environment const & env, decl_cmd_kind kind, buffer 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 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()) diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 6da85db235..3e7166f6d1 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -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); diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index a271874b20..edbd6fc7f9 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -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(); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 56bda6b36e..4b77362270 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index e695af2171..8fa9c48a05 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -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", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 9fc5c3bb46..03033b51fa 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 37bd6874dd..2bbf00db7e 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -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(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 797697519e..bd10b3b463 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -84,7 +84,7 @@ private private protected protected inline inline definition definition -meta meta +unsafe unsafe mutual mutual theorem theorem axiom axiom diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index d87ed27c77..ae408ce606 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -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); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index e8e619eb05..b21bb52a33 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -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(raw(), sizeof(object*), static_cast(is_meta)); + cnstr_set_scalar(raw(), sizeof(object*), static_cast(is_unsafe)); } -bool axiom_val::is_meta() const { return cnstr_get_scalar(raw(), sizeof(object*)) != 0; } +bool axiom_val::is_unsafe() const { return cnstr_get_scalar(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(raw(), sizeof(object*)*3, static_cast(is_meta)); + cnstr_set_scalar(raw(), sizeof(object*)*3, static_cast(is_unsafe)); } -bool definition_val::is_meta() const { return cnstr_get_scalar(raw(), sizeof(object*)*3) != 0; } +bool definition_val::is_unsafe() const { return cnstr_get_scalar(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(raw(), sizeof(object*)*5, static_cast(rec)); - cnstr_set_scalar(raw(), sizeof(object*)*5 + 1, static_cast(meta)); + cnstr_set_scalar(raw(), sizeof(object*)*5 + 1, static_cast(unsafe)); cnstr_set_scalar(raw(), sizeof(object*)*5 + 2, static_cast(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(raw(), sizeof(object*)*5, static_cast(is_meta)); + cnstr_set_scalar(raw(), sizeof(object*)*5, static_cast(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(raw(), sizeof(object*)*7, static_cast(k)); - cnstr_set_scalar(raw(), sizeof(object*)*7 + 1, static_cast(is_meta)); + cnstr_set_scalar(raw(), sizeof(object*)*7 + 1, static_cast(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(declaration_kind::Definition), definition_val(n, params, t, v, h, meta))); + reducibility_hints const & h, bool unsafe) { + return declaration(mk_cnstr(static_cast(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(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, meta))); + expr const & v, bool unsafe) { + return declaration(mk_cnstr(static_cast(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(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(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(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(declaration_kind::Inductive), lparams, nparams, types, 1)); - cnstr_set_scalar(r.raw(), inductive_decl_scalar_offset(), static_cast(is_meta)); + cnstr_set_scalar(r.raw(), inductive_decl_scalar_offset(), static_cast(is_unsafe)); return r; } -bool inductive_decl::is_meta() const { return cnstr_get_scalar(raw(), inductive_decl_scalar_offset()) != 0; } +bool inductive_decl::is_unsafe() const { return cnstr_get_scalar(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(); } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 2fc3e82fc8..eb97dac981 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -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(cnstr_get_ref(*this, 1)); } reducibility_hints const & get_hints() const { return static_cast(cnstr_get_ref(*this, 2)); } - bool is_meta() const; + bool is_unsafe() const; }; typedef list_ref 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(cnstr_get_ref(raw(), 0)); } @@ -213,34 +213,34 @@ inline optional none_declaration() { return optional() inline optional some_declaration(declaration const & o) { return optional(o); } inline optional some_declaration(declaration && o) { return optional(std::forward(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(cnstr_get_ref(raw(), 0)); } nat const & get_nparams() const { return static_cast(cnstr_get_ref(raw(), 1)); } inductive_types const & get_types() const { return static_cast(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(cnstr_get_ref(*this, 4)); } unsigned get_ncnstrs() const { return length(get_cnstrs()); } bool is_rec() const { return cnstr_get_scalar(raw(), sizeof(object*)*5) != 0; } - bool is_meta() const { return cnstr_get_scalar(raw(), sizeof(object*)*5 + 1) != 0; } + bool is_unsafe() const { return cnstr_get_scalar(raw(), sizeof(object*)*5 + 1) != 0; } bool is_reflexive() const { return cnstr_get_scalar(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(cnstr_get_ref(*this, 2)).get_small_value(); } unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 3)).get_small_value(); } unsigned get_nfields() const { return static_cast(cnstr_get_ref(*this, 4)).get_small_value(); } - bool is_meta() const { return cnstr_get_scalar(raw(), sizeof(object*)*5) != 0; } + bool is_unsafe() const { return cnstr_get_scalar(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(cnstr_get_ref(*this, 6)); } bool is_k() const { return cnstr_get_scalar(raw(), sizeof(object*)*7) != 0; } - bool is_meta() const { return cnstr_get_scalar(raw(), sizeof(object*)*7 + 1) != 0; } + bool is_unsafe() const { return cnstr_get_scalar(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; } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index f36b234738..f21b493e6f 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -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())) diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index de3cbfba56..d058dae40e 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -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 m_ind_types; buffer 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())); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 72a2934c13..50ab706531 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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; } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 87629ae3a9..0e959b3290 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -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(); diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index 826675f4f5..afd4317888 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -150,22 +150,22 @@ buffer const & closure_helper::get_norm_closure_params() const { struct mk_aux_definition_fn : public closure_helper { mk_aux_definition_fn(type_context_old & ctx):closure_helper(ctx) {} - pair operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional is_meta) { - lean_assert(!is_lemma || is_meta); - lean_assert(!is_lemma || *is_meta == false); + pair operator()(name const & c, expr const & type, expr const & value, bool is_lemma, optional 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 ls; @@ -178,26 +178,26 @@ struct mk_aux_definition_fn : public closure_helper { }; pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - name const & c, expr const & type, expr const & value, optional const & is_meta) { + name const & c, expr const & type, expr const & value, optional 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 mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - name const & c, expr const & value, optional const & is_meta) { + name const & c, expr const & value, optional 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 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 is_meta(false); - return mk_aux_definition_fn(ctx)(c, type, value, is_lemma, is_meta); + optional 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 { diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 43f0a203d9..3750934b03 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -35,7 +35,7 @@ bool is_codegen_enabled(options const & opts) { } static name get_real_name(name const & n) { - if (optional new_n = is_meta_rec_name(n)) + if (optional new_n = is_unsafe_rec_name(n)) return *new_n; else return n; diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 5fd6fabd57..882494bbc4 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -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 n = is_meta_rec_name(const_name(fn))) { + } else if (optional 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))) { diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index ec547d36f5..c71d87375f 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -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); diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index a3d1e5ecc0..58fad59ae5 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -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); diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index ba4e082eb4..8801d0a2f1 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -118,8 +118,8 @@ static optional 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); diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 7ec96f810f..69c8dca89d 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -98,7 +98,7 @@ environment mk_projections(environment const & env, name const & n, buffer 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); diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index 9f72308160..f5f3062056 100644 --- a/src/library/constructions/rec_on.cpp +++ b/src/library/constructions/rec_on.cpp @@ -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); diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index a7485f2f71..96bb4c6b7f 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -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); diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index 34ddd77086..210dbe6475 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -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; diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 63529fdf8e..9ce092cb31 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -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(R.m_counter_examples, [&] (list const & e) { return mk_app(fn, e); }); diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index 77d0917b87..d5c5139694 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -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); diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h index b8fb2b1992..cedc88c347 100644 --- a/src/library/equations_compiler/equations.h +++ b/src/library/equations_compiler/equations.h @@ -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, diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index c7a451172e..47ba2899d4 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -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; diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 8598211fa0..09de7fb61c 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -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 aux_info = env.find(meta_aux_fn_name)) { diff --git a/src/library/util.cpp b/src/library/util.cpp index 2e53821fff..d806f55e24 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -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 is_meta_rec_name(name const & n) { - if (!n.is_atomic() && n.is_string() && n.get_string() == g_meta_rec_prefix) { +optional is_unsafe_rec_name(name const & n) { + if (!n.is_atomic() && n.is_string() && n.get_string() == g_unsafe_rec_prefix) { return optional(n.get_prefix()); } else { return optional(); diff --git a/src/library/util.h b/src/library/util.h index 633808116d..c147494f79 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -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 is_meta_rec_name(name const & n); +/** Return some(n') if \c n is a name created using mk_unsafe_rec_name(n') */ +optional is_unsafe_rec_name(name const & n); /** Convert an expression representing a `name` literal into a `name` object. */ optional name_lit_to_name(expr const & name_lit); diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index d79e235186..bad8d978c3 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -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);