From b88b98ac22592c8e06b617e0f101fda33fbb4739 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Mar 2015 14:47:21 -0700 Subject: [PATCH] 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 | 95 +++++++++++++++---- src/frontends/lean/parser.cpp | 10 +- src/frontends/lean/parser.h | 2 +- .../lean/update_environment_exception.h | 33 +++++++ tests/lean/bad_eqns.lean | 16 ++-- tests/lean/bad_eqns.lean.expected.out | 6 +- tests/lean/bug1.lean | 10 +- tests/lean/bug1.lean.expected.out | 8 +- tests/lean/gen_bug.lean | 2 +- .../lean/interactive/num2.input.expected.out | 4 + tests/lean/unique_instances.lean | 2 +- 11 files changed, 144 insertions(+), 44 deletions(-) create mode 100644 src/frontends/lean/update_environment_exception.h diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 5ece80edf..bed54b9e2 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/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) - env = set_reducible(env, d, reducible_status::Reducible, persistent); - if (m_is_irreducible) - env = set_reducible(env, d, reducible_status::Irreducible, persistent); - if (m_is_semireducible) - env = set_reducible(env, d, reducible_status::Semireducible, persistent); - if (m_is_quasireducible) - env = set_reducible(env, d, reducible_status::Quasireducible, persistent); + auto decl = env.find(d); + if (decl && decl->is_definition()) { + if (m_is_reducible) + env = set_reducible(env, d, reducible_status::Reducible, persistent); + if (m_is_irreducible) + env = set_reducible(env, d, reducible_status::Irreducible, persistent); + if (m_is_semireducible) + 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 m_type_checkpoint; + optional m_env_checkpoint; + buffer 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(), buffer(), 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(), 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(); - process_locals(); - elaborate(); - register_decl(); - return m_env; + try { + parse(); + process_locals(); + elaborate(); + 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(ex.clone())); + } + ex.rethrow(); + lean_unreachable(); + } } }; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 60eead443..267ccd81e 100644 --- a/src/frontends/lean/parser.cpp +++ b/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(ex.clone()), std::make_shared(m_pos_table, get_stream_name(), p)); } @@ -278,7 +279,12 @@ if (m_use_exceptions) { ThrowError ; } void parser::protected_call(std::function && f, std::function && 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); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 57277301b..659de73a4 100644 --- a/src/frontends/lean/parser.h +++ b/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 && f, std::function && sync); diff --git a/src/frontends/lean/update_environment_exception.h b/src/frontends/lean/update_environment_exception.h new file mode 100644 index 000000000..4cc8124fa --- /dev/null +++ b/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 +#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 m_exception; +public: + update_environment_exception(environment const & env, std::shared_ptr 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; } +}; +} diff --git a/tests/lean/bad_eqns.lean b/tests/lean/bad_eqns.lean index f437578ab..640a59f3a 100644 --- a/tests/lean/bad_eqns.lean +++ b/tests/lean/bad_eqns.lean @@ -1,15 +1,15 @@ open nat -definition foo : nat → nat -| foo (0 + x) := x +definition foo1 : nat → nat +| foo1 (0 + x) := x -definition foo : nat → nat → nat -| foo 0 _ := 0 -| foo x ⌞y⌟ := x +definition foo2 : nat → nat → nat +| foo2 0 _ := 0 +| foo2 x ⌞y⌟ := x -definition foo : nat → nat → nat -| foo 0 _ := 0 -| foo ⌞x⌟ x := x +definition foo3 : nat → nat → nat +| foo3 0 _ := 0 +| foo3 ⌞x⌟ x := x inductive tree (A : Type) := | node : tree_list A → tree A diff --git a/tests/lean/bad_eqns.lean.expected.out b/tests/lean/bad_eqns.lean.expected.out index 36fb4ce97..c0551e047 100644 --- a/tests/lean/bad_eqns.lean.expected.out +++ b/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 -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 + foo2 x y +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) diff --git a/tests/lean/bug1.lean b/tests/lean/bug1.lean index 9439574e2..7bdbf1364 100644 --- a/tests/lean/bug1.lean +++ b/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 diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out index 778e130ba..6f19cf6b8 100644 --- a/tests/lean/bug1.lean.expected.out +++ b/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 diff --git a/tests/lean/gen_bug.lean b/tests/lean/gen_bug.lean index d87b1ed95..66e30f565 100644 --- a/tests/lean/gen_bug.lean +++ b/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, diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out index f908cb9ab..a9616bb94 100644 --- a/tests/lean/interactive/num2.input.expected.out +++ 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 diff --git a/tests/lean/unique_instances.lean b/tests/lean/unique_instances.lean index 86bcf3378..e929b8cd6 100644 --- a/tests/lean/unique_instances.lean +++ b/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) := _