feat(library,frontends): remove sorry macro

Lean4 will not have macros.

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) : α

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

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.
 

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)

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

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<expr> 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<expr> const & expected_type, expr const & ref, bool synthetic = true);
     expr recoverable_error(optional<expr> const & expected_type, expr const & ref, elaborator_exception const & ex);
     template <class Fn> expr recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn &&);

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

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() << "'");

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

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

src/library/constants.txt

@@ -203,6 +203,7 @@ psigma.fst
 psigma.snd
 singleton
 sizeof
+sorry_ax
 string
 string.empty
 string.str

src/library/equations_compiler/elim_match.cpp

@@ -1212,7 +1212,8 @@ struct elim_match_fn {
     list<lemma> 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<lemma>();
         }
         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<lemma>();
     }

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

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

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 <string>
-#include <kernel/find_fn.h>
+#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<expr> 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<sorry_macro_cell const *>(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<sorry_macro_cell const *>(macro_def(e).raw())->is_synthetic();
+    if (!is_sorry(e)) return false;
+    buffer<expr> 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<bool>(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<bool>(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<expr> 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;
 }
 }

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 */

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