From dc7ab17d2a0919ba02df59e083523d71451490d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 31 Oct 2014 09:01:19 -0700 Subject: [PATCH] feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option --- src/frontends/lean/calc_proof_elaborator.cpp | 98 +++++++++++++------- src/frontends/lean/calc_proof_elaborator.h | 7 +- src/frontends/lean/elaborator.cpp | 3 +- src/frontends/lean/init_module.cpp | 3 + tests/lean/calc_assistant.lean | 26 ++++++ tests/lean/calc_assistant.lean.expected.out | 13 +++ 6 files changed, 113 insertions(+), 37 deletions(-) create mode 100644 tests/lean/calc_assistant.lean create mode 100644 tests/lean/calc_assistant.lean.expected.out diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index 1af677315..91d9918d9 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sexpr/option_declarations.h" #include "kernel/free_vars.h" #include "kernel/instantiate.h" #include "library/unifier.h" @@ -14,7 +15,28 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" #include "frontends/lean/calc.h" +#ifndef LEAN_DEFAULT_CALC_ASSISTANT +#define LEAN_DEFAULT_CALC_ASSISTANT true +#endif + namespace lean { +static name * g_elaborator_calc_assistant = nullptr; + +void initialize_calc_proof_elaborator() { + g_elaborator_calc_assistant = new name{"elaborator", "calc_assistant"}; + register_bool_option(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT, + "(elaborator) when needed lean automatically adds symmetry, " + "inserts missing arguments, and applies substitutions"); +} + +void finalize_calc_proof_elaborator() { + delete g_elaborator_calc_assistant; +} + +bool get_elaborator_calc_assistant(options const & o) { + return o.get_bool(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT); +} + static optional> mk_op(environment const & env, local_context & ctx, name_generator & ngen, type_checker_ptr & tc, name const & op, unsigned nunivs, unsigned nargs, std::initializer_list const & explicit_args, constraint_seq & cs, tag g) { @@ -95,8 +117,8 @@ static optional> apply_subst(environment const & env, local_con - adding ! - adding subst */ -constraint mk_calc_proof_cnstr(environment const & env, local_context const & _ctx, - expr const & m, expr const & _e, +constraint mk_calc_proof_cnstr(environment const & env, options const & opts, + local_context const & _ctx, expr const & m, expr const & _e, constraint_seq const & cs, unifier_config const & cfg, info_manager * im, bool relax) { justification j = mk_failed_to_synthesize_jst(env, m); @@ -112,19 +134,23 @@ constraint mk_calc_proof_cnstr(environment const & env, local_context const & _c e_type = s.instantiate(e_type); e_type = tc->whnf(e_type, new_cs); tag g = e.get_tag(); - // add '!' is needed - while (is_pi(e_type)) { - binder_info bi = binding_info(e_type); - if (!bi.is_implicit() && !bi.is_inst_implicit()) { - if (!has_free_var(binding_body(e_type), 0)) { - // if the rest of the type does not reference argument, - // then we also stop consuming arguments - break; + bool calc_assistant = get_elaborator_calc_assistant(opts); + + if (calc_assistant) { + // add '!' is needed + while (is_pi(e_type)) { + binder_info bi = binding_info(e_type); + if (!bi.is_implicit() && !bi.is_inst_implicit()) { + if (!has_free_var(binding_body(e_type), 0)) { + // if the rest of the type does not reference argument, + // then we also stop consuming arguments + break; + } } + expr imp_arg = ctx.mk_meta(ngen, some_expr(binding_domain(e_type)), g); + e = mk_app(e, imp_arg, g); + e_type = tc->whnf(instantiate(binding_body(e_type), imp_arg), new_cs); } - expr imp_arg = ctx.mk_meta(ngen, some_expr(binding_domain(e_type)), g); - e = mk_app(e, imp_arg, g); - e_type = tc->whnf(instantiate(binding_body(e_type), imp_arg), new_cs); } auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs) { @@ -155,33 +181,37 @@ constraint mk_calc_proof_cnstr(environment const & env, local_context const & _c return append(r, postponed); }; - std::unique_ptr saved_ex; - try { + if (!get_elaborator_calc_assistant(opts)) { return try_alternative(e, e_type, new_cs); - } catch (exception & ex) { - saved_ex.reset(ex.clone()); - } + } else { + std::unique_ptr saved_ex; + try { + return try_alternative(e, e_type, new_cs); + } catch (exception & ex) { + saved_ex.reset(ex.clone()); + } - constraint_seq symm_cs = new_cs; - auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g); - if (symm) { - try { return try_alternative(symm->first, symm->second, symm_cs); } catch (exception &) {} - } + constraint_seq symm_cs = new_cs; + auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g); + if (symm) { + try { return try_alternative(symm->first, symm->second, symm_cs); } catch (exception &) {} + } - constraint_seq subst_cs = new_cs; - if (auto subst = apply_subst(env, ctx, ngen, tc, e, e_type, meta_type, subst_cs, g)) { - try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {} - } - - if (symm) { - constraint_seq subst_cs = symm_cs; - if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) { + constraint_seq subst_cs = new_cs; + if (auto subst = apply_subst(env, ctx, ngen, tc, e, e_type, meta_type, subst_cs, g)) { try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {} } - } - saved_ex->rethrow(); - lean_unreachable(); + if (symm) { + constraint_seq subst_cs = symm_cs; + if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) { + try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {} + } + } + + saved_ex->rethrow(); + lean_unreachable(); + } }; bool owner = false; return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax); diff --git a/src/frontends/lean/calc_proof_elaborator.h b/src/frontends/lean/calc_proof_elaborator.h index 8509240a7..19c8d3b3f 100644 --- a/src/frontends/lean/calc_proof_elaborator.h +++ b/src/frontends/lean/calc_proof_elaborator.h @@ -16,8 +16,11 @@ namespace lean { - adding ! - adding subst */ -constraint mk_calc_proof_cnstr(environment const & env, local_context const & ctx, - expr const & m, expr const & e, +constraint mk_calc_proof_cnstr(environment const & env, options const & opts, + local_context const & ctx, expr const & m, expr const & e, constraint_seq const & cs, unifier_config const & cfg, info_manager * im, bool relax); + +void initialize_calc_proof_elaborator(); +void finalize_calc_proof_elaborator(); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c81c78462..4c480b156 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -310,7 +310,8 @@ expr elaborator::visit_calc_proof(expr const & e, optional const & t, cons pair ecs = visit(get_annotation_arg(e)); expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); register_meta(m); - constraint c = mk_calc_proof_cnstr(env(), m_context, m, ecs.first, ecs.second, m_unifier_config, + constraint c = mk_calc_proof_cnstr(env(), ios().get_options(), + m_context, m, ecs.first, ecs.second, m_unifier_config, im, m_relax_main_opaque); cs += c; return m; diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index ec9e6c345..f6a1e4413 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -25,6 +25,7 @@ Author: Leonardo de Moura #include "frontends/lean/token_table.h" #include "frontends/lean/info_tactic.h" #include "frontends/lean/placeholder_elaborator.h" +#include "frontends/lean/calc_proof_elaborator.h" #include "frontends/lean/scanner.h" #include "frontends/lean/pp.h" #include "frontends/lean/server.h" @@ -54,10 +55,12 @@ void initialize_frontend_lean_module() { initialize_info_tactic(); initialize_pp(); initialize_placeholder_elaborator(); + initialize_calc_proof_elaborator(); initialize_server(); } void finalize_frontend_lean_module() { finalize_server(); + finalize_calc_proof_elaborator(); finalize_placeholder_elaborator(); finalize_pp(); finalize_info_tactic(); diff --git a/tests/lean/calc_assistant.lean b/tests/lean/calc_assistant.lean new file mode 100644 index 000000000..d3cd41b4d --- /dev/null +++ b/tests/lean/calc_assistant.lean @@ -0,0 +1,26 @@ +import logic +open eq.ops + +set_option elaborator.calc_assistant false + +theorem tst1 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c := +calc a = b : H₁ -- error because calc assistant is off + ... = c : H₂ + +theorem tst2 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c := +calc a = b : !H₁⁻¹ + ... = c : H₂ -- error because calc assistant is off + +theorem tst3 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c := +calc a = b : !H₁⁻¹ + ... = c : H₂⁻¹ + +theorem tst4 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c := +calc a = b : eq.symm (H₁ a) + ... = c : eq.symm H₂ + +set_option elaborator.calc_assistant true + +theorem tst5 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c := +calc a = b : H₁ + ... = c : H₂ diff --git a/tests/lean/calc_assistant.lean.expected.out b/tests/lean/calc_assistant.lean.expected.out new file mode 100644 index 000000000..3c01c5299 --- /dev/null +++ b/tests/lean/calc_assistant.lean.expected.out @@ -0,0 +1,13 @@ +calc_assistant.lean:7:14: error: type mismatch at term + H₁ +has type + ∀ (x : num), + b = x +but is expected to have type + a = b +calc_assistant.lean:12:14: error: type mismatch at term + H₂ +has type + c = b +but is expected to have type + b = c