feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed

The idea is to avoid a "tsunami" of error messages when a heavily used
theorem breaks in the beginning of the file

src/frontends/lean/decl_cmds.cpp

@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
+#include "frontends/lean/update_environment_exception.h"
 
 namespace lean {
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
@@ -452,20 +453,23 @@ struct decl_attributes {
         }
         if (m_is_coercion)
             env = add_coercion(env, d, ios, persistent);
-        if (m_is_reducible)
+        auto decl = env.find(d);
-            env = set_reducible(env, d, reducible_status::Reducible, persistent);
+        if (decl && decl->is_definition()) {
-        if (m_is_irreducible)
+            if (m_is_reducible)
-            env = set_reducible(env, d, reducible_status::Irreducible, persistent);
+                env = set_reducible(env, d, reducible_status::Reducible, persistent);
-        if (m_is_semireducible)
+            if (m_is_irreducible)
-            env = set_reducible(env, d, reducible_status::Semireducible, persistent);
+                env = set_reducible(env, d, reducible_status::Irreducible, persistent);
-        if (m_is_quasireducible)
+            if (m_is_semireducible)
-            env = set_reducible(env, d, reducible_status::Quasireducible, persistent);
+                env = set_reducible(env, d, reducible_status::Semireducible, persistent);
+            if (m_is_quasireducible)
+                env = set_reducible(env, d, reducible_status::Quasireducible, persistent);
+            if (m_unfold_c_hint)
+                env = add_unfold_c_hint(env, d, m_unfold_c_hint, persistent);
+        }
         if (m_is_class)
             env = add_class(env, d, persistent);
         if (m_has_multiple_instances)
             env = mark_multiple_instances(env, d, persistent);
-        if (m_unfold_c_hint)
-            env = add_unfold_c_hint(env, d, m_unfold_c_hint, persistent);
         return env;
     }
 };
@@ -768,6 +772,18 @@ class definition_cmd_fn {
     expr              m_pre_type;
     expr              m_pre_value;
 
+    // Checkpoint for processing definition/theorem as axiom in case of
+    // failure
+    optional<expr>        m_type_checkpoint;
+    optional<environment> m_env_checkpoint;
+    buffer<name>          m_ls_buffer_checkpoint;
+
+    void save_checkpoint() {
+        m_type_checkpoint      = m_type;
+        m_env_checkpoint       = m_env;
+        m_ls_buffer_checkpoint = m_ls_buffer;
+    }
+
     bool is_definition() const { return m_kind == Definition || m_kind == Abbreviation || m_kind == LocalAbbreviation; }
     unsigned start_line() const { return m_pos.first; }
     unsigned end_line() const { return m_end_pos.first; }
@@ -796,6 +812,7 @@ class definition_cmd_fn {
             m_p.next();
             auto pos = m_p.pos();
             m_type = m_p.parse_expr();
+            save_checkpoint();
             if (is_curr_with_or_comma_or_bar(m_p)) {
                 m_value = parse_equations(m_p, m_name, m_type, m_aux_decls,
                                           optional<local_environment>(), buffer<expr>(), m_pos);
@@ -814,9 +831,11 @@ class definition_cmd_fn {
             auto pos = m_p.pos();
             if (m_p.curr_is_token(get_colon_tk())) {
                 m_p.next();
-                m_type = m_p.parse_scoped_expr(ps, *lenv);
+                expr type  = m_p.parse_scoped_expr(ps, *lenv);
+                m_type     = Pi(ps, type, m_p);
+                save_checkpoint();
                 if (is_curr_with_or_comma_or_bar(m_p)) {
-                    m_value = parse_equations(m_p, m_name, m_type, m_aux_decls, lenv, ps, m_pos);
+                    m_value = parse_equations(m_p, m_name, type, m_aux_decls, lenv, ps, m_pos);
                 } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
                     check_end_of_theorem(m_p);
                     m_value = m_p.save_pos(mk_expr_placeholder(), pos);
@@ -831,11 +850,12 @@ class definition_cmd_fn {
                                        "(solution: put parentheses around parameters)",
                                        pos);
                 }
-                m_type = m_p.save_pos(mk_expr_placeholder(), m_p.pos());
+                m_type  = m_p.save_pos(mk_expr_placeholder(), m_p.pos());
+                m_type  = Pi(ps, m_type, m_p);
+                save_checkpoint();
                 m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
                 m_value = m_p.parse_scoped_expr(ps, *lenv);
             }
-            m_type  = Pi(ps, m_type, m_p);
             erase_local_binder_info(ps);
             m_value = Fun(ps, m_value, m_p);
         }
@@ -1074,6 +1094,30 @@ class definition_cmd_fn {
         }
     }
 
+    void process_as_axiom() {
+        lean_assert(m_type_checkpoint);
+        m_type      = *m_type_checkpoint;
+        m_env       = *m_env_checkpoint;
+        m_ls_buffer = m_ls_buffer_checkpoint;
+        m_aux_decls.clear();
+        m_real_aux_names.clear();
+
+        expr dummy  = mk_Prop();
+        m_value     = dummy;
+
+        process_locals();
+        mk_real_name();
+
+        bool clear_pre_info      = false;
+        level_param_names new_ls;
+        std::tie(m_type, new_ls) = m_p.elaborate_type(m_type, list<expr>(), clear_pre_info);
+        check_no_metavar(m_env, m_real_name, m_type, true);
+        m_ls = append(m_ls, new_ls);
+        m_type = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
+        m_env = module::add(m_env, check(m_env, mk_axiom(m_real_name, m_ls, m_type)));
+        register_decl(m_name, m_real_name, m_type);
+    }
+
 public:
     definition_cmd_fn(parser & p, def_cmd_kind kind, bool is_opaque, bool is_private, bool is_protected):
         m_p(p), m_env(m_p.env()), m_kind(kind), m_is_opaque(is_opaque),
@@ -1084,11 +1128,24 @@ public:
     }
 
     environment operator()() {
-        parse();
+        try {
-        process_locals();
+            parse();
-        elaborate();
+            process_locals();
-        register_decl();
+            elaborate();
-        return m_env;
+            register_decl();
+            return m_env;
+        } catch (exception & ex) {
+            if (m_type_checkpoint) {
+                try {
+                    process_as_axiom();
+                } catch (exception & ex2) {
+                    ex.rethrow();
+                }
+                throw update_environment_exception(m_env, std::shared_ptr<throwable>(ex.clone()));
+            }
+            ex.rethrow();
+            lean_unreachable();
+        }
     }
 };
 

src/frontends/lean/parser.cpp

@@ -46,6 +46,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/parse_rewrite_tactic.h"
+#include "frontends/lean/update_environment_exception.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -264,7 +265,7 @@ void parser::throw_parser_exception(char const * msg, pos_info p) {
     throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second);
 }
 
-void parser::throw_nested_exception(throwable & ex, pos_info p) {
+void parser::throw_nested_exception(throwable const & ex, pos_info p) {
     throw parser_nested_exception(std::shared_ptr<throwable>(ex.clone()),
                                   std::make_shared<parser_pos_provider>(m_pos_table, get_stream_name(), p));
 }
@@ -278,7 +279,12 @@ if (m_use_exceptions) { ThrowError ; }
 
 void parser::protected_call(std::function<void()> && f, std::function<void()> && sync) {
     try {
-        f();
+        try {
+            f();
+        } catch (update_environment_exception & ex) {
+            m_env = ex.get_env();
+            ex.get_exception().rethrow();
+        }
     } catch (parser_exception & ex) {
         CATCH(flycheck_error err(regular_stream()); regular_stream() << ex.what() << endl,
               throw);

src/frontends/lean/parser.h

@@ -146,7 +146,7 @@ class parser {
     void display_error(throwable const & ex);
     void display_error(script_exception const & ex);
     void throw_parser_exception(char const * msg, pos_info p);
-    void throw_nested_exception(throwable & ex, pos_info p);
+    void throw_nested_exception(throwable const & ex, pos_info p);
 
     void sync_command();
     void protected_call(std::function<void()> && f, std::function<void()> && sync);

src/frontends/lean/update_environment_exception.h

@@ -0,0 +1,33 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <memory>
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Auxiliary exception that stores the "real" exception, and a new
+    environment that should replace the one in the parser.
+    This is a trick to simulate commands that had "partial success".
+    Example: we may have failed to type check a proof, but we may have succeeded
+    in checking the theorem's type. So, we may store the theorem as an axiom, and
+    continue. This feature is useful to avoid a cascade of error messages when
+    a heavily useful theorem is broken in the beginning of the file.
+*/
+class update_environment_exception : public exception {
+    environment                m_env;
+    std::shared_ptr<throwable> m_exception;
+public:
+    update_environment_exception(environment const & env, std::shared_ptr<throwable> const & ex):
+        exception("exception"), m_env(env), m_exception(ex) {}
+    virtual ~update_environment_exception() {}
+    virtual throwable * clone() const { return new update_environment_exception(m_env, m_exception); }
+    virtual void rethrow() const { throw *this; }
+    virtual char const * what() const noexcept { return m_exception->what(); }
+    throwable const & get_exception() const { return *(m_exception.get()); }
+    environment const & get_env() const { return m_env; }
+};
+}

tests/lean/bad_eqns.lean

@@ -1,15 +1,15 @@
 open nat
 
-definition foo : nat → nat
+definition foo1 : nat → nat
-| foo (0 + x) := x
+| foo1 (0 + x) := x
 
-definition foo : nat → nat → nat
+definition foo2 : nat → nat → nat
-| foo 0 _   := 0
+| foo2 0 _   := 0
-| foo x ⌞y⌟ := x
+| foo2 x ⌞y⌟ := x
 
-definition foo : nat → nat → nat
+definition foo3 : nat → nat → nat
-| foo 0   _ := 0
+| foo3 0   _ := 0
-| foo ⌞x⌟ x := x
+| foo3 ⌞x⌟ x := x
 
 inductive tree (A : Type) :=
 | node   : tree_list A → tree A

tests/lean/bad_eqns.lean.expected.out

@@ -1,9 +1,9 @@
 bad_eqns.lean:4:2: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
   0 + x
 in the following equation left-hand-side
-  foo (0 + x)
+  foo1 (0 + x)
 bad_eqns.lean:8:2: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
-  foo x y
+  foo2 x y
-bad_eqns.lean:10:11: error: invalid recursive equations for 'foo', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
+bad_eqns.lean:10:11: error: invalid recursive equations for 'foo3', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
 bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions
 bad_eqns.lean:34:11: error: invalid recursive equations, failed to find recursive arguments that are structurally smaller (possible solution: use well-founded recursion)

tests/lean/bug1.lean

@@ -5,19 +5,19 @@ infixl `∧`:25 := and
 constant a : bool
 
 -- Error
-theorem and_intro (p q : bool) (H1 : p) (H2 : q) : a
+theorem and_intro1 (p q : bool) (H1 : p) (H2 : q) : a
 := fun (c : bool) (H : p -> q -> c), H H1 H2
 
 -- Error
-theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ p
+theorem and_intro2 (p q : bool) (H1 : p) (H2 : q) : p ∧ p
 := fun (c : bool) (H : p -> q -> c), H H1 H2
 
 -- Error
-theorem and_intro (p q : bool) (H1 : p) (H2 : q) : q ∧ p
+theorem and_intro3 (p q : bool) (H1 : p) (H2 : q) : q ∧ p
 := fun (c : bool) (H : p -> q -> c), H H1 H2
 
 -- Correct
-theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
+theorem and_intro4 (p q : bool) (H1 : p) (H2 : q) : p ∧ q
 := fun (c : bool) (H : p -> q -> c), H H1 H2
 
-check and_intro
+check and_intro4

tests/lean/bug1.lean.expected.out

@@ -1,19 +1,19 @@
-bug1.lean:9:7: error: type mismatch at definition 'and_intro', has type
+bug1.lean:9:7: error: type mismatch at definition 'and_intro1', has type
   ∀ (p q : bool),
     p → q → (∀ (c : bool), (p → q → c) → c)
 but is expected to have type
   ∀ (p q : bool),
     p → q → a
-bug1.lean:13:7: error: type mismatch at definition 'and_intro', has type
+bug1.lean:13:7: error: type mismatch at definition 'and_intro2', has type
   ∀ (p q : bool),
     p → q → (∀ (c : bool), (p → q → c) → c)
 but is expected to have type
   ∀ (p q : bool),
     p → q → p ∧ p
-bug1.lean:17:7: error: type mismatch at definition 'and_intro', has type
+bug1.lean:17:7: error: type mismatch at definition 'and_intro3', has type
   ∀ (p q : bool),
     p → q → (∀ (c : bool), (p → q → c) → c)
 but is expected to have type
   ∀ (p q : bool),
     p → q → q ∧ p
-and_intro : ∀ (p q : bool), p → q → p ∧ q
+and_intro4 : ∀ (p q : bool), p → q → p ∧ q

tests/lean/gen_bug.lean

@@ -11,7 +11,7 @@ begin
   apply (heq.symm H),
 end
 
-theorem tst (A B : Type) (a : A) (b : B) : a == b → b == a :=
+theorem tst2 (A B : Type) (a : A) (b : B) : a == b → b == a :=
 begin
   generalize a,
   generalize b,

tests/lean/interactive/num2.input.expected.out

@@ -7,6 +7,7 @@ pos_num.size|pos_num → pos_num
 pos_num.bit0|pos_num → pos_num
 pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
+pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
 pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
@@ -20,6 +21,7 @@ pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos
 pos_num.pred|pos_num → pos_num
 pos_num.mul|pos_num → pos_num → pos_num
 pos_num.no_confusion_type|Type → pos_num → pos_num → Type
+pos_num.num_bits|pos_num → pos_num
 pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.lt|pos_num → pos_num → bool
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
@@ -36,6 +38,7 @@ pos_num.size|pos_num → pos_num
 pos_num.bit0|pos_num → pos_num
 pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
+pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
 pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
@@ -61,6 +64,7 @@ pos_num.size|pos_num → pos_num
 pos_num.bit0|pos_num → pos_num
 pos_num.is_inhabited|inhabited pos_num
 pos_num.is_one|pos_num → bool
+pos_num.inc|pos_num → pos_num
 pos_num.ibelow|pos_num → Prop
 pos_num.binduction_on|Π (n : pos_num), (Π (n : pos_num), pos_num.ibelow n → ?C n) → ?C n
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n

tests/lean/unique_instances.lean

@@ -6,5 +6,5 @@ theorem tst (A : Type) (H₁ : inhabited A) (H₂ : inhabited A) : inhabited (A
 _
 
 set_option class.unique_instances false
-theorem tst (A : Type) (H₁ : inhabited A) (H₂ : inhabited A) : inhabited (A × A) :=
+theorem tst2 (A : Type) (H₁ : inhabited A) (H₂ : inhabited A) : inhabited (A × A) :=
 _