feat(frontends/lean): add 'sorry'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/emacs/lean-mode.el

@@ -50,6 +50,7 @@
     ("\\_<\\(variables\\|parameters\\)\\_>[ \t\(\{\[]*\\([^:]*\\)" (2 'font-lock-function-name-face))
     ("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
     ("\\_<_\\_>" . 'font-lock-preprocessor-face)
+    ("\\_<sorry\\_>" . 'font-lock-warning-face)
     ;;
     )
   '("\\.lean$")                    ;; files for which to activate this mode

src/frontends/lean/CMakeLists.txt

@@ -5,6 +5,6 @@ interactive.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
 dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp
 class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
-structure_cmd.cpp)
+structure_cmd.cpp sorry.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_exprs.cpp

@@ -362,6 +362,10 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co
     return r;
 }
 
+static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.mk_sorry(pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -383,6 +387,7 @@ parse_table init_nud_table() {
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
+    r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
     r = r.add({transition("including", mk_ext_action(parse_including_expr))}, x0);
     return r;
 }

src/frontends/lean/decl_cmds.cpp

@@ -187,7 +187,6 @@ struct decl_modifiers {
 environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     name n = p.check_id_next("invalid declaration, identifier expected");
     check_atomic(n);
-    environment env = p.env();
     decl_modifiers modifiers;
     name real_n; // real name for this declaration
     modifiers.m_is_opaque = _is_opaque;
@@ -203,14 +202,6 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         modifiers.parse(p);
         if (is_theorem && !modifiers.m_is_opaque)
             throw exception("invalid theorem declaration, theorems cannot be transparent");
-        if (modifiers.m_is_private) {
-            auto env_n = add_private_name(env, n, optional<unsigned>(hash(p.pos().first, p.pos().second)));
-            env    = env_n.first;
-            real_n = env_n.second;
-        } else {
-            name const & ns = get_namespace(env);
-            real_n     = ns + n;
-        }
 
         if (p.curr_is_token(g_assign)) {
             auto pos = p.pos();
@@ -249,9 +240,24 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
             type  = Pi(ps, type, p);
             value = Fun(ps, value, p);
         }
+
         update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
     }
+
+    if (p.used_sorry())
+        p.declare_sorry();
+    environment env = p.env();
+
+    if (modifiers.m_is_private) {
+        auto env_n = add_private_name(env, n, optional<unsigned>(hash(p.pos().first, p.pos().second)));
+        env    = env_n.first;
+        real_n = env_n.second;
+    } else {
+        name const & ns = get_namespace(env);
+        real_n     = ns + n;
+    }
+
     if (in_section(env)) {
         buffer<expr> section_ps;
         collect_section_locals(type, value, p, section_ps);

src/frontends/lean/parser.cpp

@@ -37,6 +37,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/pp_options.h"
+#include "frontends/lean/sorry.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -91,6 +92,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_num_threads = num_threads;
     m_no_undef_id_error    = false;
     m_found_errors = false;
+    m_used_sorry = false;
     updt_options();
     m_next_tag_idx = 0;
     m_curr = scanner::token_kind::Identifier;
@@ -107,6 +109,20 @@ parser::~parser() {
     } catch (...) {}
 }
 
+expr parser::mk_sorry(pos_info const & p) {
+    m_used_sorry = true;
+    {
+        flycheck_warning wrn(regular_stream());
+        regular_stream() << get_stream_name() << ":" << p.first << ":" << p.second << ": warning using 'sorry'" << endl;
+    }
+    return get_sorry_constant();
+}
+
+void parser::declare_sorry() {
+    m_used_sorry = true;
+    m_env = ::lean::declare_sorry(m_env);
+}
+
 bool parser::has_tactic_decls() {
     if (!m_has_tactic_decls)
         m_has_tactic_decls = ::lean::has_tactic_decls(m_env);

src/frontends/lean/parser.h

@@ -57,6 +57,7 @@ class parser {
     pos_info                m_last_script_pos;
     unsigned                m_next_tag_idx;
     bool                    m_found_errors;
+    bool                    m_used_sorry;
     pos_info_table_ptr      m_pos_table;
     // By default, when the parser finds a unknown identifier, it signs an error.
     // When the following flag is true, it creates a constant.
@@ -270,6 +271,10 @@ public:
     std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls,
                                                                       name const & n, expr const & t, expr const & v, bool is_opaque);
 
+    expr mk_sorry(pos_info const & p);
+    bool used_sorry() const { return m_used_sorry; }
+    void declare_sorry();
+
     parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }
 
     /** parse all commands in the input stream */

src/frontends/lean/sorry.cpp

@@ -0,0 +1,35 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/type_checker.h"
+#include "kernel/environment.h"
+#include "library/module.h"
+
+namespace lean {
+static name g_sorry_name("sorry");
+static expr g_sorry(mk_constant(g_sorry_name));
+static name  g_l("l");
+static expr  g_sorry_type(mk_pi("A", mk_sort(mk_param_univ(g_l)), mk_var(0), binder_info(true)));
+
+bool has_sorry(environment const & env) {
+    auto decl = env.find(g_sorry_name);
+    return decl && decl->get_type() != g_sorry_type;
+}
+
+environment declare_sorry(environment const & env) {
+    if (auto decl = env.find(g_sorry_name)) {
+        if (decl->get_type() != g_sorry_type)
+            throw exception("failed to declare 'sorry', environment already has an object named 'sorry'");
+        return env;
+    } else {
+        return module::add(env, check(env, mk_var_decl(g_sorry_name, list<name>(g_l), g_sorry_type)));
+    }
+}
+
+expr const & get_sorry_constant() {
+    return g_sorry;
+}
+}

src/frontends/lean/sorry.h

@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Return true iff the given environment has <tt>sorry.{l} : Pi {A : Type.{l}}, A</tt> */
+bool has_sorry(environment const & env);
+
+/** \brief Declare <tt>sorry.{l} : Pi {A : Type.{l}}, A</tt> in the given environment if it doesn't already contain it.
+    Throw an exception if the environment already contains a declaration named \c sorry. */
+environment declare_sorry(environment const & env);
+
+/** \brief Return the constant \c sorry */
+expr const & get_sorry_constant();
+}

src/frontends/lean/token_table.cpp

@@ -69,7 +69,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec},
          {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec}, {"including", 0},
+         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",

tests/lean/crash.lean.expected.out

@@ -1,6 +1,6 @@
 crash.lean:8:12: error: type mismatch at application
   have H' : not P, from H,
-  ?M_1 P H
+  ?M_1
 term
   H
 is expected of type

tests/lean/run/elab_bug1.lean

@@ -11,9 +11,6 @@ using function
 
 namespace congruence
 
--- TODO: delete this
-axiom sorry {P : Prop} : P
-
 -- TODO: move this somewhere else
 abbreviation reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x
 

tests/lean/run/sorry.lean

@@ -0,0 +1,7 @@
+import logic
+
+definition b : Prop :=
+sorry
+
+theorem tst : true = false :=
+sorry

tests/lean/run/univ2.lean

@@ -6,6 +6,5 @@ hypothesis unfold : I → F I
 hypothesis fold   : F I → I
 hypothesis iso1 : ∀x, fold (unfold x) = x
 
-variable sorry {A : Type} : A
 theorem iso2 : ∀x, fold (unfold x) = x
 := sorry