From 1332fbabd6e70fbe329ffad0e0834e7b6e2b02de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 May 2018 14:00:30 -0700 Subject: [PATCH] feat(library,frontends): remove `sorry` macro Lean4 will not have macros. --- library/init/core.lean | 5 ++ library/init/meta/expr.lean | 5 -- library/init/meta/interactive.lean | 5 -- library/init/meta/tactic.lean | 10 --- src/frontends/lean/definition_cmds.cpp | 2 +- src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/parser.cpp | 2 +- src/library/compiler/vm_compiler.cpp | 4 +- src/library/constants.cpp | 4 + src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/equations_compiler/elim_match.cpp | 5 +- src/library/init_module.cpp | 3 - src/library/noncomputable.cpp | 1 + src/library/sorry.cpp | 85 +++++-------------- src/library/sorry.h | 9 +- src/library/vm/vm_expr.cpp | 12 --- 17 files changed, 47 insertions(+), 109 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index c22494505c..2cc8f4b1e7 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -2229,3 +2229,8 @@ theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true := end aux end classical + +/- Auxiliary axiom used to implement `sorry`. + TODO: add this theorem on-demand. That is, + we should only add it if after the first error. -/ +constant sorry_ax (α : Sort u) (synthetic := tt) : α diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index bac6a9e8c2..804b3962ca 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -171,11 +171,6 @@ const `true [] meta def mk_false : expr := const `false [] -/-- Returns the sorry macro with the given type. -/ -meta constant mk_sorry (type : expr) : expr -/-- Checks whether e is sorry, and returns its type. -/ -meta constant is_sorry (e : expr) : option expr - meta def is_var : expr → bool | (var _) := tt | _ := ff diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 478e931def..f792025e35 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -666,11 +666,6 @@ Tries to solve the current goal using a canonical proof of `true`, or the `refle meta def trivial : tactic unit := tactic.triv <|> fail "trivial tactic failed" -/-- -Closes the main goal using `sorry`. --/ -meta def admit : tactic unit := tactic.admit - /-- `iterate { t }` repeatedly applies tactic `t` until `t` fails. `iterate { t }` always succeeds. diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index a2077df036..fa145752a1 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -930,16 +930,6 @@ do u ← mk_meta_univ, t ← mk_meta_var (expr.sort u), mk_meta_var t -/-- Makes a sorry macro with a meta-variable as its type. -/ -meta def mk_sorry : tactic expr := do -u ← mk_meta_univ, -t ← mk_meta_var (expr.sort u), -return $ expr.mk_sorry t - -/-- Closes the main goal using sorry. -/ -meta def admit : tactic unit := -target >>= exact ∘ expr.mk_sorry - meta def triv : tactic unit := mk_const `trivial >>= exact notation `dec_trivial` := of_as_true (by tactic.triv) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 7d14e061af..7b1a1fea4d 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -673,7 +673,7 @@ static expr elaborate_proof( /* Remark: we need the catch to be able to produce correct line information */ message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, ERROR) .set_exception(ex).report(); - return mk_sorry(final_type, true); + return mk_sorry(*tc, final_type, true); } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 290bff7c1c..4a23877398 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -165,7 +165,7 @@ public: bool try_report(std::exception const & ex); bool try_report(std::exception const & ex, optional const & ref); void report_or_throw(elaborator_exception const & ex); - expr mk_sorry(expr const & type, bool synthetic = true) { return ::lean::mk_sorry(type, synthetic); } + expr mk_sorry(expr const & type, bool synthetic = true) { return ::lean::mk_sorry(m_ctx, type, synthetic); } expr mk_sorry(optional const & expected_type, expr const & ref, bool synthetic = true); expr recoverable_error(optional const & expected_type, expr const & ref, elaborator_exception const & ex); template expr recover_expr_from_exception(optional const & expected_type, expr const & ref, Fn &&); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9fe968dace..e6a893940e 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -229,7 +229,7 @@ void parser::scan() { } expr parser::mk_sorry(pos_info const & p, bool synthetic) { - return save_pos(::lean::mk_sorry(mk_Prop(), synthetic), p); + return save_pos(::lean::mk_app(mk_constant(get_sorry_ax_name()), mk_expr_placeholder(), synthetic ? mk_bool_tt() : mk_bool_ff()), p); } void parser::updt_options() { diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index d34d668ccb..b4bd8a891b 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -229,6 +229,8 @@ class vm_compiler_fn { compile_cnstr(e, bpz, m); } else if (is_internal_proj(fn)) { compile_proj(e, bpz, m); + } else if (is_sorry(e)) { + compile_global(*get_vm_decl(m_env, "sorry"), 0, nullptr, bpz, m); } else { compile_fn_call(e, bpz, m); } @@ -279,8 +281,6 @@ class vm_compiler_fn { emit(mk_expr_instr(get_expr_quote_value(e))); } else if (is_pexpr_quote(e)) { emit(mk_expr_instr(get_pexpr_quote_value(e))); - } else if (is_sorry(e)) { - compile_global(*get_vm_decl(m_env, "sorry"), 0, nullptr, bpz, m); } else { throw exception(sstream() << "code generation failed, unexpected kind of macro has been found: '" << macro_def(e).get_name() << "'"); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 361dcb09dd..51c825c6be 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -208,6 +208,7 @@ name const * g_psigma_fst = nullptr; name const * g_psigma_snd = nullptr; name const * g_singleton = nullptr; name const * g_sizeof = nullptr; +name const * g_sorry_ax = nullptr; name const * g_string = nullptr; name const * g_string_empty = nullptr; name const * g_string_str = nullptr; @@ -453,6 +454,7 @@ void initialize_constants() { g_psigma_snd = new name{"psigma", "snd"}; g_singleton = new name{"singleton"}; g_sizeof = new name{"sizeof"}; + g_sorry_ax = new name{"sorry_ax"}; g_string = new name{"string"}; g_string_empty = new name{"string", "empty"}; g_string_str = new name{"string", "str"}; @@ -699,6 +701,7 @@ void finalize_constants() { delete g_psigma_snd; delete g_singleton; delete g_sizeof; + delete g_sorry_ax; delete g_string; delete g_string_empty; delete g_string_str; @@ -944,6 +947,7 @@ name const & get_psigma_fst_name() { return *g_psigma_fst; } name const & get_psigma_snd_name() { return *g_psigma_snd; } name const & get_singleton_name() { return *g_singleton; } name const & get_sizeof_name() { return *g_sizeof; } +name const & get_sorry_ax_name() { return *g_sorry_ax; } name const & get_string_name() { return *g_string; } name const & get_string_empty_name() { return *g_string_empty; } name const & get_string_str_name() { return *g_string_str; } diff --git a/src/library/constants.h b/src/library/constants.h index d5cbf0477f..7088475867 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -210,6 +210,7 @@ name const & get_psigma_fst_name(); name const & get_psigma_snd_name(); name const & get_singleton_name(); name const & get_sizeof_name(); +name const & get_sorry_ax_name(); name const & get_string_name(); name const & get_string_empty_name(); name const & get_string_str_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index d0970a471c..db3d2e8e27 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -203,6 +203,7 @@ psigma.fst psigma.snd singleton sizeof +sorry_ax string string.empty string.str diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 11e9074ba5..64ad70c338 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -1212,7 +1212,8 @@ struct elim_match_fn { list process_leaf(problem const & P) { if (!P.m_equations) { m_unsolved.push_back(P); - m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true)); + type_context_old ctx = mk_type_context(P); + m_mctx.assign(P.m_goal, mk_sorry(ctx, m_mctx.get_metavar_decl(P.m_goal).get_type(), true)); return list(); } equation const & eqn = head(P.m_equations); @@ -1291,7 +1292,7 @@ struct elim_match_fn { } catch (exception & ex) { if (!m_elab.try_report(ex, some_expr(m_ref))) throw; m_error_during_process = true; - m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true)); + m_mctx.assign(P.m_goal, m_elab.mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true)); } return list(); } diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index b7c5d044d0..6901960a95 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -23,7 +23,6 @@ Author: Leonardo de Moura #include "library/export_decl.h" #include "library/io_state.h" #include "library/idx_metavar.h" -#include "library/sorry.h" #include "library/placeholder.h" #include "library/print.h" #include "library/fingerprint.h" @@ -93,7 +92,6 @@ void initialize_library_module() { initialize_reducible(); initialize_aliases(); initialize_export_decl(); - initialize_sorry(); initialize_class(); initialize_library_util(); initialize_quote(); @@ -143,7 +141,6 @@ void finalize_library_module() { finalize_quote(); finalize_library_util(); finalize_class(); - finalize_sorry(); finalize_export_decl(); finalize_aliases(); finalize_reducible(); diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 9520fc169d..57443d5ed0 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -66,6 +66,7 @@ struct noncomputable_modification : public modification { static bool is_builtin_extra(name const & n) { return n == get_io_core_name() || + n == get_sorry_ax_name() || n == get_monad_io_impl_name() || n == get_monad_io_terminal_impl_name() || n == get_monad_io_file_system_impl_name() || diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp index 457b4538d8..5b576f961d 100644 --- a/src/library/sorry.cpp +++ b/src/library/sorry.cpp @@ -4,81 +4,39 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/sorry.h" #include -#include +#include "kernel/find_fn.h" +#include "kernel/for_each_fn.h" #include "kernel/type_checker.h" #include "kernel/environment.h" -#include "library/module.h" -#include "kernel/for_each_fn.h" -#include "library/kernel_serializer.h" +#include "library/sorry.h" +#include "library/constants.h" +#include "library/util.h" +#include "library/util.h" namespace lean { -static name * g_sorry_name = nullptr; -static std::string * g_sorry_opcode = nullptr; - -class sorry_macro_cell : public macro_definition_cell { - bool m_synthetic; - -public: - sorry_macro_cell(bool synthetic) : m_synthetic(synthetic) {} - - bool is_synthetic() const { return m_synthetic; } - - virtual name get_name() const override { return *g_sorry_name; } - - unsigned int trust_level() const override { return 1; } - - virtual expr check_type(expr const & sry, abstract_type_context & ctx, bool infer_only) const override { - if (!is_sorry(sry)) throw exception("invalid sorry macro"); - auto sort = ctx.whnf(ctx.check(sorry_type(sry), infer_only)); - if (!is_sort(sort)) throw exception("type of sorry macro is not a sort"); - return sorry_type(sry); - } - - virtual optional expand(expr const &, abstract_type_context &) const override { - return {}; - } - - virtual void write(serializer & s) const override { - s.write_string(*g_sorry_opcode); - s.write_bool(m_synthetic); - } -}; - -void initialize_sorry() { - g_sorry_name = new name{"sorry"}; - g_sorry_opcode = new std::string("Sorry"); - - register_macro_deserializer(*g_sorry_opcode, - [] (deserializer & d, unsigned num, expr const * args) { - if (num != 1) throw corrupted_stream_exception(); - bool synthetic = d.read_bool(); - return mk_sorry(args[0], synthetic); - }); +expr mk_sorry(abstract_type_context & ctx, expr const & ty, bool synthetic) { + level u = get_level(ctx, ty); + return mk_app(mk_constant(get_sorry_ax_name(), levels(u)), ty, synthetic ? mk_bool_tt() : mk_bool_ff()); } -void finalize_sorry() { - delete g_sorry_opcode; - delete g_sorry_name; -} - -expr mk_sorry(expr const & ty, bool synthetic) { - return mk_macro(macro_definition(new sorry_macro_cell(synthetic)), 1, &ty); -} bool is_sorry(expr const & e) { - return is_macro(e) && macro_num_args(e) == 1 && dynamic_cast(macro_def(e).raw()); + return is_app_of(e, get_sorry_ax_name()) && get_app_num_args(e) >= 2; } + bool is_synthetic_sorry(expr const & e) { - return is_sorry(e) && static_cast(macro_def(e).raw())->is_synthetic(); + if (!is_sorry(e)) return false; + buffer args; + get_app_args(e, args); + return is_constant(args[1], get_bool_tt_name()); } bool has_synthetic_sorry(expr const & ex) { - return !!find(ex, [] (expr const & e, unsigned) { return is_synthetic_sorry(e); }); + return static_cast(find(ex, [] (expr const & e, unsigned) { return is_synthetic_sorry(e); })); } bool has_sorry(expr const & ex) { - return !!find(ex, [] (expr const & e, unsigned) { return is_sorry(e); }); + return static_cast(find(ex, [] (expr const & e, unsigned) { return is_sorry(e); })); } bool has_sorry(declaration const & decl) { @@ -86,14 +44,17 @@ bool has_sorry(declaration const & decl) { } expr const & sorry_type(expr const & sry) { - return macro_arg(sry, 0); + lean_assert(is_sorry(sry)); + buffer args; + get_app_args(sry, args); + return args[0]; } bool has_sorry(environment const & env) { bool found_sorry = false; env.for_each_declaration([&] (declaration const & decl) { - if (!found_sorry && has_sorry(decl)) found_sorry = true; - }); + if (!found_sorry && has_sorry(decl)) found_sorry = true; + }); return found_sorry; } } diff --git a/src/library/sorry.h b/src/library/sorry.h index bc546e2f95..254c0614b7 100644 --- a/src/library/sorry.h +++ b/src/library/sorry.h @@ -15,11 +15,10 @@ bool has_sorry(declaration const &); bool has_synthetic_sorry(expr const &); /** \brief Returns the sorry macro with the specified type. - * \param synthetic Synthetic macros are created by parser and - * elaborator during error recovery. Non-synthetic macros are - * entered by the user using the `sorry` keyword. - */ -expr mk_sorry(expr const & ty, bool synthetic = false); + \param synthetic Synthetic macros are created by parser and + elaborator during error recovery. Non-synthetic macros are + entered by the user using the `sorry` keyword. */ +expr mk_sorry(abstract_type_context & ctx, expr const & ty, bool synthetic = false); /** \brief Return true iff \c e is a sorry macro. */ bool is_sorry(expr const & e); /** \brief Return true iff \c e is a synthetic sorry macro */ diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index f76ccc49d4..d2f03ec8bf 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -413,15 +413,6 @@ vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) { return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b))); } -vm_obj expr_mk_sorry(vm_obj const & t) { - return to_obj(mk_sorry(to_expr(t))); -} - -vm_obj expr_is_sorry(vm_obj const & e_) { - auto & e = to_expr(e_); - return to_obj(is_sorry(e) ? some(sorry_type(e)) : none_expr()); -} - vm_obj expr_occurs(vm_obj const & e1, vm_obj const & e2) { return mk_vm_bool(occurs(to_expr(e1), to_expr(e2))); } @@ -518,9 +509,6 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name("expr", "is_annotation"), expr_is_annotation); - DECLARE_VM_BUILTIN(name("expr", "mk_sorry"), expr_mk_sorry); - DECLARE_VM_BUILTIN(name("expr", "is_sorry"), expr_is_sorry); - // Not sure if we should expose these or what? DECLARE_VM_BUILTIN(name({"expr", "is_internal_cnstr"}), expr_is_internal_cnstr); DECLARE_VM_BUILTIN(name({"expr", "get_nat_value"}), expr_get_nat_value);