From 634c0b5e9dad0441f6836d6b699e214362077869 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Sep 2015 20:34:14 -0700 Subject: [PATCH] feat(library/tactic,frontends/lean): propagate new options back to elaborator --- src/frontends/lean/elaborator.cpp | 15 +++++++++++---- src/frontends/lean/elaborator_context.cpp | 22 +++++++++++++++------- src/frontends/lean/elaborator_context.h | 5 ++++- src/frontends/lean/info_tactic.cpp | 4 ++-- src/library/simplifier/simp_tactic.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/check_expr_tactic.cpp | 2 +- src/library/tactic/elaborate.cpp | 2 +- src/library/tactic/elaborate.h | 2 +- src/library/tactic/exact_tactic.cpp | 2 +- src/library/tactic/let_tactic.cpp | 4 ++-- src/library/tactic/rewrite_tactic.cpp | 2 +- tests/lean/hott/disable_instances.hlean | 13 +++++++++++++ 13 files changed, 54 insertions(+), 23 deletions(-) create mode 100644 tests/lean/hott/disable_instances.hlean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 5b73bb311..37eff77eb 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1742,14 +1742,21 @@ optional elaborator::get_pre_tactic_for(expr const & mvar) { optional elaborator::pre_tactic_to_tactic(expr const & pre_tac) { try { - auto fn = [=](goal const & g, name_generator && ngen, expr const & e, optional const & expected_type, + auto fn = [=](goal const & g, options const & o, name_generator && ngen, expr const & e, optional const & expected_type, substitution const & subst, bool report_unassigned) { - elaborator aux_elaborator(m_ctx, std::move(ngen)); // Disable tactic hints when processing expressions nested in tactics. // We must do it otherwise, it is easy to make the system loop. bool use_tactic_hints = false; - return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, - use_tactic_hints, subst, report_unassigned); + if (o == m_ctx.m_options) { + elaborator aux_elaborator(m_ctx, std::move(ngen)); + return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, + use_tactic_hints, subst, report_unassigned); + } else { + elaborator_context aux_ctx(m_ctx, o); + elaborator aux_elaborator(aux_ctx, std::move(ngen)); + return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, + use_tactic_hints, subst, report_unassigned); + } }; return optional(expr_to_tactic(env(), fn, pre_tac, pip())); } catch (expr_to_tactic_exception & ex) { diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp index 1f9bcb0c4..62106973e 100644 --- a/src/frontends/lean/elaborator_context.cpp +++ b/src/frontends/lean/elaborator_context.cpp @@ -67,15 +67,23 @@ bool get_elaborator_lift_coercions(options const & opts) { elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, pos_info_provider const * pp, info_manager * info, bool check_unassigned): m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) { - m_use_local_instances = get_elaborator_local_instances(ios.get_options()); - m_ignore_instances = get_elaborator_ignore_instances(ios.get_options()); - m_flycheck_goals = get_elaborator_flycheck_goals(ios.get_options()); - m_fail_missing_field = get_elaborator_fail_missing_field(ios.get_options()); - m_lift_coercions = get_elaborator_lift_coercions(ios.get_options()); - init_options(ios.get_options()); + set_options(ios.get_options()); } -void elaborator_context::init_options(options const & opts) { +elaborator_context::elaborator_context(elaborator_context const & ctx, options const & o): + m_env(ctx.m_env), m_ios(ctx.m_ios), m_lls(ctx.m_lls), m_pos_provider(ctx.m_pos_provider), + m_info_manager(ctx.m_info_manager), m_check_unassigned(ctx.m_check_unassigned) { + set_options(o); +} + +void elaborator_context::set_options(options const & opts) { + m_options = opts; + m_use_local_instances = get_elaborator_local_instances(opts); + m_ignore_instances = get_elaborator_ignore_instances(opts); + m_flycheck_goals = get_elaborator_flycheck_goals(opts); + m_fail_missing_field = get_elaborator_fail_missing_field(opts); + m_lift_coercions = get_elaborator_lift_coercions(opts); + if (has_show_goal(opts, m_show_goal_line, m_show_goal_col)) { m_show_goal_at = true; } else { diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h index c37865e3d..08f9763ad 100644 --- a/src/frontends/lean/elaborator_context.h +++ b/src/frontends/lean/elaborator_context.h @@ -20,6 +20,7 @@ class elaborator_context { pos_info_provider const * m_pos_provider; info_manager * m_info_manager; // configuration + options m_options; bool m_check_unassigned; bool m_use_local_instances; bool m_ignore_instances; @@ -36,8 +37,9 @@ class elaborator_context { unsigned m_show_hole_line; unsigned m_show_hole_col; + void set_options(options const & opts); + /** \brief Support for showing information using hot-keys */ - void init_options(options const & opts); bool has_show_goal_at(unsigned & line, unsigned & col) const; void reset_show_goal_at(); @@ -46,6 +48,7 @@ class elaborator_context { public: elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true); + elaborator_context(elaborator_context const & ctx, options const & o); }; void initialize_elaborator_context(); void finalize_elaborator_context(); diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp index 4bbedf0b9..7b88c462e 100644 --- a/src/frontends/lean/info_tactic.cpp +++ b/src/frontends/lean/info_tactic.cpp @@ -32,11 +32,11 @@ struct scoped_info_tactic_proof_state { }; tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) { - return tactic1([=](environment const &, io_state const &, proof_state const & ps) -> proof_state { + return tactic1([=](environment const &, io_state const & ios, proof_state const & ps) -> proof_state { // create dummy variable just to communicate position to the elaborator expr dummy = mk_sort(mk_level_zero(), e.get_tag()); scoped_info_tactic_proof_state scope(ps); - fn(goal(), name_generator("dummy"), dummy, none_expr(), substitution(), false); + fn(goal(), ios.get_options(), name_generator("dummy"), dummy, none_expr(), substitution(), false); return ps; }); } diff --git a/src/library/simplifier/simp_tactic.cpp b/src/library/simplifier/simp_tactic.cpp index e774c5ea7..0ef6b3ca1 100644 --- a/src/library/simplifier/simp_tactic.cpp +++ b/src/library/simplifier/simp_tactic.cpp @@ -196,7 +196,7 @@ private: try { expr new_l; constraints cs; bool report_unassigned = true; - std::tie(new_l, m_subst, cs) = m_elab(m_g, m_ngen.mk_child(), l, none_expr(), m_subst, report_unassigned); + std::tie(new_l, m_subst, cs) = m_elab(m_g, m_ios.get_options(), m_ngen.mk_child(), l, none_expr(), m_subst, report_unassigned); if (cs) throw tactic_exception("invalid 'simp' tactic, fail to resolve generated constraints"); expr new_e = head_beta_reduce(m_elab_tc.infer(new_l).first); diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index ba13cc2c7..c9d6447c4 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -208,7 +208,7 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kin name_generator ngen = s.get_ngen(); expr new_e; substitution new_subst; constraints cs_; try { - auto ecs = elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false); + auto ecs = elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), s.get_subst(), false); std::tie(new_e, new_subst, cs_) = ecs; buffer cs; to_buffer(cs_, cs); diff --git a/src/library/tactic/check_expr_tactic.cpp b/src/library/tactic/check_expr_tactic.cpp index 374726bc1..a0adca6db 100644 --- a/src/library/tactic/check_expr_tactic.cpp +++ b/src/library/tactic/check_expr_tactic.cpp @@ -21,7 +21,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e, } goal const & g = head(gs); name_generator ngen = s.get_ngen(); - expr new_e = std::get<0>(elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false)); + expr new_e = std::get<0>(elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), s.get_subst(), false)); auto tc = mk_type_checker(env, ngen.mk_child()); expr new_t = tc->infer(new_e).first; auto out = regular(env, ios); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 5716c28e0..3b0d69b4a 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -45,7 +45,7 @@ optional elaborate_with_respect_to(environment const & env, io_state const optional elab_expected_type; if (enforce_type_during_elaboration) elab_expected_type = expected_type; - auto esc = elab(head(gs), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned); + auto esc = elab(head(gs), ios.get_options(), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned); expr new_e; substitution new_subst; constraints cs_; std::tie(new_e, new_subst, cs_) = esc; buffer cs; diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index 732c13582..d47b06f25 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -25,7 +25,7 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat 3- postponed constraints */ typedef std::tuple elaborate_result; -typedef std::function const &, substitution const &, bool)> elaborate_fn; /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 0b5c91f69..67e2a56c0 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -99,7 +99,7 @@ static tactic assumption_tactic_core(bool conservative) { goal g = head(gs); buffer hs; g.get_hyps(hs); - auto elab = [](goal const &, name_generator const &, expr const & H, + auto elab = [](goal const &, options const &, name_generator const &, expr const & H, optional const &, substitution const & s, bool) -> elaborate_result { return elaborate_result(H, s, constraints()); }; diff --git a/src/library/tactic/let_tactic.cpp b/src/library/tactic/let_tactic.cpp index b7e24a24e..53d142125 100644 --- a/src/library/tactic/let_tactic.cpp +++ b/src/library/tactic/let_tactic.cpp @@ -19,7 +19,7 @@ expr mk_let_tactic_expr(name const & id, expr const & e) { } tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { - return tactic01([=](environment const & env, io_state const &, proof_state const & s) { + return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { proof_state new_s = s; goals const & gs = new_s.get_goals(); if (!gs) { @@ -29,7 +29,7 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { goal const & g = head(gs); name_generator ngen = s.get_ngen(); bool report_unassigned = true; - elaborate_result esc = elab(g, ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned); + elaborate_result esc = elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned); expr new_e; substitution new_subst; constraints cs; std::tie(new_e, new_subst, cs) = esc; if (cs) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index c4d7f288d..4959955db 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -747,7 +747,7 @@ class rewrite_fn { optional> elaborate_core(expr const & e, bool fail_if_cnstrs) { expr new_expr; substitution new_subst; constraints cs; - std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false); + std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ios.get_options(), m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false); if (fail_if_cnstrs && cs) return optional>(); m_ps = proof_state(m_ps, new_subst); diff --git a/tests/lean/hott/disable_instances.hlean b/tests/lean/hott/disable_instances.hlean new file mode 100644 index 000000000..1f0b71cf1 --- /dev/null +++ b/tests/lean/hott/disable_instances.hlean @@ -0,0 +1,13 @@ +open is_equiv +constants (A B : Type) (f : A → B) + +definition H : is_equiv f := sorry + + +definition loop [instance] [h : is_equiv f] : is_equiv f := +h + +example (a : A) : let H' : is_equiv f := H in @(inv f) H' (f a) = a := +begin + with_options [elaborator.ignore_instances true] (apply left_inv f a) +end