From 1a6629ce3b0fa672ce77d04f1ffb7480c8dc6c19 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 17 Jan 2017 23:10:02 +0100 Subject: [PATCH] feat(frontends/lean/parser): keep list of tasks that have to succeed --- src/frontends/lean/definition_cmds.cpp | 8 +++- src/frontends/lean/parser.cpp | 39 ++++++++++++++++++-- src/frontends/lean/parser.h | 17 +++++++-- src/kernel/declaration.cpp | 2 +- src/library/module_mgr.cpp | 13 ++++++- src/library/module_mgr.h | 4 +- tests/lean/fail/example.lean | 2 + tests/lean/run/apply4.lean | 4 +- tests/lean/run/auto_quote1.lean | 4 +- tests/lean/run/elab_crash1.lean | 4 +- tests/lean/run/simplify_with_hypotheses.lean | 4 +- 11 files changed, 79 insertions(+), 22 deletions(-) create mode 100644 tests/lean/fail/example.lean diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index a0e4f662fc..7613a0ebff 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -363,6 +363,8 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe mk_theorem(c_real_name, to_list(lp_names), type, *val) : mk_definition(new_env, c_real_name, to_list(lp_names), type, *val, use_conv_opt, is_trusted)); auto cdef = check(p, new_env, c_name, def, pos); + if (cdef.get_declaration().is_theorem()) + p.require_success(cdef.get_declaration().get_value_task()); new_env = module::add(new_env, cdef); check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, modifiers.m_is_noncomputable); @@ -733,6 +735,7 @@ public: ERROR); error_msg.set_exception(ex); error_msg.report(); + throw std::exception(); // this bypasses the default exception reporting } return {}; } @@ -787,15 +790,16 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif auto elab_task = get_global_task_queue()->submit( decl_env, p.get_options(), header_pos, new_params, new_fn, val, thm_finfo, is_rfl, type, elab.mctx(), elab.lctx(), p.get_parser_pos_provider(header_pos)); + p.require_success(elab_task); env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, elab_task, modifiers, attrs, doc_string, header_pos); } else if (kind == Example) { - get_global_task_queue()->submit( + p.require_success(get_global_task_queue()->submit( p.env(), p.get_options(), modifiers, to_list(lp_names), new_params, fn, val, elab.mctx(), elab.lctx(), - p.get_parser_pos_provider(header_pos)); + p.get_parser_pos_provider(header_pos))); return p.env(); } else { std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 13970b12e2..b131bc114d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2224,7 +2224,34 @@ void parser::get_imports(std::vector & imports) { parse_imports(fingerprint, imports); } -bool parser::parse_commands() { +struct combine_parse_success_task : public task { + list m_required_successes; + + combine_parse_success_task(list const & required_successes) : + task(), m_required_successes(required_successes) {} + + void description(std::ostream & out) const override { + out << "Checking parse success (" << get_module_id() << ")"; + } + + std::vector get_dependencies() override { + std::vector deps; + for (auto & d : m_required_successes) + deps.push_back(d); + return deps; + } + + bool is_tiny() const override { return true; } + + bool do_priority_inversion() const override { return false; } + + bool execute() override { + for (auto & d : m_required_successes) get_global_task_queue()->wait(d); + return true; + } +}; + +task_result parser::parse_commands() { protected_call([&]() { // We disable hash-consing while parsing to make sure the pos-info are correct. scoped_expr_caching disable(false); @@ -2295,7 +2322,12 @@ bool parser::parse_commands() { m_env = pop_scope_core(m_env, m_ios); } }, [](){}); - return !m_found_errors; + + if (m_found_errors) { + return mk_pure_task_result(false, "parse success"); + } else { + return get_global_task_queue()->submit(m_required_successes); + } } bool parser::curr_is_command_like() const { @@ -2318,7 +2350,8 @@ void parser::save_snapshot(scope_message_context & smc, pos_info p) { m_snapshot_vector->push_back(std::make_shared( m_env, smc.get_sub_buckets(), m_local_level_decls, m_local_decls, m_level_variables, m_variables, m_include_vars, - m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_next_inst_idx, p)); + m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_next_inst_idx, p, + m_required_successes)); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d99b2a60f5..cbfa40ddc0 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -67,12 +67,14 @@ struct snapshot { parser_scope_stack m_parser_scope_stack; unsigned m_next_inst_idx; pos_info m_pos; + list m_required_successes; snapshot(environment const & env, name_set const & sub_buckets, local_level_decls const & lds, local_expr_decls const & eds, name_set const & lvars, name_set const & vars, name_set const & includes, options const & opts, bool imports_parsed, parser_scope_stack const & pss, - unsigned next_inst_idx, pos_info const & pos): + unsigned next_inst_idx, pos_info const & pos, list const & required_successes): m_env(env), m_sub_buckets(sub_buckets), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes), - m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos) {} + m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos), + m_required_successes(required_successes) {} }; typedef std::vector> snapshot_vector; @@ -171,6 +173,9 @@ class parser : public abstract_parser { // Docgen optional m_doc_string; + // Tasks that need to be successful (no exception) for parsing to succeed + list m_required_successes; + void throw_parser_exception(char const * msg, pos_info p); void throw_nested_exception(throwable const & ex, pos_info p); @@ -196,7 +201,7 @@ class parser : public abstract_parser { void process_imports(); void parse_command(); - bool parse_commands(); + task_result parse_commands(); void process_postponed(buffer const & args, bool is_left, buffer const & kinds, buffer> const & nargs, buffer const & ps, buffer> const & scoped_info, list const & postponed, pos_info const & p, buffer & new_args); @@ -516,11 +521,15 @@ public: bool used_sorry() const { return m_used_sorry; } void declare_sorry_if_used(); + void require_success(generic_task_result const & t) { + m_required_successes = cons(t, m_required_successes); + } + /** return true iff profiling is enabled */ bool profiling() const { return m_profile; } /** parse all commands in the input stream */ - bool operator()() { return parse_commands(); } + task_result operator()() { return parse_commands(); } void get_imports(std::vector &); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index d640b6a90e..a2880c55d5 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -60,7 +60,7 @@ unsigned declaration::get_num_univ_params() const { return length(get_univ_param expr const & declaration::get_type() const { return m_ptr->m_type; } task_result const & declaration::get_value_task() const { - lean_assert(is_definition()); + lean_assert(is_theorem()); return m_ptr->m_proof; } expr const & declaration::get_value() const { diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index 8dfd1e29ee..8daa4fd893 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -18,6 +18,14 @@ Author: Gabriel Ebner namespace lean { +bool module_info::parse_result::is_ok() const { + try { + return m_parsed_ok.get() && m_proofs_are_correct.get(); + } catch (...) { + return false; + } +} + void module_mgr::mark_out_of_date(module_id const & id, buffer & to_rebuild) { for (auto & mod : m_modules) { if (!mod.second || mod.second->m_out_of_date) continue; @@ -123,7 +131,7 @@ public: use_exceptions, (m_snapshots.empty() || !m_use_snapshots) ? std::shared_ptr() : m_snapshots.back(), m_use_snapshots ? &m_snapshots : nullptr); - bool parsed_ok = p(); + auto parsed_ok = p(); module_info::parse_result mod; @@ -161,6 +169,7 @@ public: if (auto res = m_mod->m_result.peek()) { for (auto & mdf : res->m_loaded_module->m_modifications) mdf->get_task_dependencies(deps); + deps.push_back(res->m_parsed_ok); deps.push_back(res->m_proofs_are_correct); } @@ -257,7 +266,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set parse_olean_modifications(parsed_olean.second, id), {} }, m_initial_env, [=] { return mk_loader(id, deps); }); - res.m_parsed_ok = true; + res.m_parsed_ok = mk_pure_task_result(true, "olean parse success"); res.m_proofs_are_correct = mk_pure_task_result(true, ""); mod->m_result = mk_pure_task_result(res, "Loading " + olean_fn); diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h index 2739a82e3b..9d7392befc 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -47,9 +47,9 @@ struct module_info { struct parse_result { options m_opts; - bool m_parsed_ok = false; + task_result m_parsed_ok; task_result m_proofs_are_correct; - bool is_ok() const { return m_parsed_ok && m_proofs_are_correct.get(); } + bool is_ok() const; std::shared_ptr m_loaded_module; diff --git a/tests/lean/fail/example.lean b/tests/lean/fail/example.lean new file mode 100644 index 0000000000..8ea5fa9d15 --- /dev/null +++ b/tests/lean/fail/example.lean @@ -0,0 +1,2 @@ +open tactic expr +example : false := by do exact $ const `does_not_exist [] diff --git a/tests/lean/run/apply4.lean b/tests/lean/run/apply4.lean index a5d27f44e8..615c844cf9 100644 --- a/tests/lean/run/apply4.lean +++ b/tests/lean/run/apply4.lean @@ -20,7 +20,7 @@ set_option pp.all false example (a b : nat) : a = 0 → a = b := by do intro `H, - apply_core semireducible tt ff (expr.const `foo [level.of_nat 1]), + apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]), trace_state, a ← get_local `a, trace_state, @@ -45,6 +45,6 @@ by do example (a b : nat) : a = 0 → a = b := by do `[intro], - apply_core semireducible tt ff (expr.const `foo [level.of_nat 1]), + apply_core semireducible ff tt ff (expr.const `foo [level.of_nat 1]), `[exact inhabited.mk a], reflexivity diff --git a/tests/lean/run/auto_quote1.lean b/tests/lean/run/auto_quote1.lean index 6dcbdbddc4..a3b712bc2d 100644 --- a/tests/lean/run/auto_quote1.lean +++ b/tests/lean/run/auto_quote1.lean @@ -56,7 +56,7 @@ begin induction m with m' ih, { -- Remark: Used change here to make sure nat.zero is replaced with polymorphic zero. -- dsimp tactic should fix that in the future. - change n + 0 = 0 + n, rw zadd n }, + change n + 0 = 0 + n, simp [zadd] }, { change succ (n + m') = succ m' + n, rw [succ_add, ih] } end @@ -72,7 +72,7 @@ begin induction m with m' ih, show n + 0 = 0 + n, begin - change n + 0 = 0 + n, rw zadd n + change n + 0 = 0 + n, simp [zadd] end, show n + succ m' = succ m' + n, { change succ (n + m') = succ m' + n, diff --git a/tests/lean/run/elab_crash1.lean b/tests/lean/run/elab_crash1.lean index ffcd4d9816..bc4d8773b1 100644 --- a/tests/lean/run/elab_crash1.lean +++ b/tests/lean/run/elab_crash1.lean @@ -4,10 +4,10 @@ meta definition to_expr_target (a : pexpr) : tactic expr := do tgt ← target, to_expr `((%%a : %%tgt)) -example (A : Type) (a : A) : A := +noncomputable example (A : Type) (a : A) : A := by do to_expr_target `(sorry) >>= exact -example (A : Type) (a : A) : A := +noncomputable example (A : Type) (a : A) : A := by do refine `(sorry) example (a : nat) : nat := diff --git a/tests/lean/run/simplify_with_hypotheses.lean b/tests/lean/run/simplify_with_hypotheses.lean index 6ae43c9ccd..12aa24671f 100644 --- a/tests/lean/run/simplify_with_hypotheses.lean +++ b/tests/lean/run/simplify_with_hypotheses.lean @@ -1,9 +1,9 @@ open tactic -example (A : Type) (a₁ a₂ : A) (f : A → A) (H₀ : a₁ = a₂) : f a₁ = f a₂ := by simp_using_hs >> try reflexivity +example (A : Type) (a₁ a₂ : A) (f : A → A) (H₀ : a₁ = a₂) : f a₁ = f a₂ := by do simp_using_hs >> try reflexivity example (A : Type) (a₁ a₁' a₂ a₂' : A) (f : A → A) (H₀ : a₁' = a₂') (H₁ : f a₁ = a₁') (H₂ : f a₂ = a₂') -: f a₁ = f a₂ := by simp_using_hs >> try reflexivity +: f a₁ = f a₂ := by do simp_using_hs >> try reflexivity constants (A : Type.{1}) (x y z w : A) (f : A → A) (H₁ : f (f x) = f y) (H₂ : f (f y) = f z) (H₃ : f (f z) = w)