From 04eaf184a92606a56e54d0d6c8d59437557263fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Feb 2016 18:41:55 -0800 Subject: [PATCH] feat(frontends/lean,library/unifier): checkpoints at have-expressions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit @avigad, @fpvandoorn, @rlewis1988, @dselsam This commit modifies how have-expressions are elaborated. Now, to process have H : , from , we first process the constraints in and simultaneously. After all these constraints are solved, the elaborator performs a Prolog-like cut, and process the constraints in . So, all overloads, type classes and coercions in and are solved before we start processing . Moreover, while processing , we cannot backtrack to and anymore. I fixed all affected proofs in the standard and HoTT libraries in previous commits pushed today and yesterday. I think most affected proofs were not using a good style and/or were easy to fix. Here is a common pattern that does not work anymore. structure has_scalar [class] (F V : Type) := (smul : F → V → V) infixl ` • `:73 := has_scalar.smul proposition smul_zero (a : R) : a • (0 : M) = 0 := have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero], !add.left_cancel this The `have` doesn't work because Lean can't figure out the type of 0 before it starts processing `!add.left_cancel this`. This is easy to fix, we just have to annotate one of the `0`s in the `have`: proposition smul_zero (a : R) : a • (0 : M) = 0 := have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero], !add.left_cancel this BTW, all tactics are still being executed after all constraints are solved. We may change that in the future. I didn't want to execute the tactics at before because of universe meta-variables. In Lean, unassigned universe meta-variables become parameters. Moreover, we perform this conversion *before* we start processing tactics. Reason: universe meta-variables create many problems for tactics such as `rewrite`, `blast` and `simp`. Finally, we can recover the previous behavior using the option set_option parser.checkpoint_have false --- src/frontends/lean/builtin_exprs.cpp | 18 ++++++ src/frontends/lean/elaborator.cpp | 36 +++++++++++- src/frontends/lean/elaborator.h | 2 + src/library/annotation.cpp | 13 +++-- src/library/annotation.h | 2 + src/library/unifier.cpp | 85 +++++++++++++++++++++++----- src/library/unifier.h | 9 ++- 7 files changed, 141 insertions(+), 24 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 074290468..7ce415aa5 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.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 "util/sstream.h" #include "kernel/abstract.h" #include "library/annotation.h" @@ -36,7 +37,17 @@ Author: Leonardo de Moura #include "frontends/lean/obtain_expr.h" #include "frontends/lean/nested_declaration.h" +#ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE +#define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true +#endif + namespace lean { +static name * g_parser_checkpoint_have = nullptr; + +bool get_parser_checkpoint_have(options const & opts) { + return opts.get_bool(*g_parser_checkpoint_have, LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE); +} + namespace notation { static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) { if (p.curr_is_token(get_llevel_curly_tk())) { @@ -475,6 +486,8 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con } // remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables. body = abstract(body, l); + if (get_parser_checkpoint_have(p.get_options())) + body = mk_checkpoint_annotation(body); expr r = p.save_pos(mk_have_annotation(p.save_pos(mk_lambda(id, prop, body, bi), pos)), pos); return p.mk_app(r, proof, pos); } @@ -814,6 +827,10 @@ void initialize_builtin_exprs() { *g_nud_table = notation::init_nud_table(); g_led_table = new parse_table(); *g_led_table = notation::init_led_table(); + + g_parser_checkpoint_have = new name{"parser", "checkpoint_have"}; + register_bool_option(*g_parser_checkpoint_have, LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE, + "(parser) introduces a checkpoint on have-expressions, checkpoints are like Prolog-cuts"); } void finalize_builtin_exprs() { @@ -821,5 +838,6 @@ void finalize_builtin_exprs() { delete g_nud_table; delete notation::H_obtain_from; delete notation::g_not; + delete g_parser_checkpoint_have; } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d596a399c..a49c89ccd 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -40,6 +40,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/choice_iterator.h" #include "library/projection.h" +#include "library/trace.h" #include "library/pp_options.h" #include "library/class_instance_resolution.h" #include "library/tactic/expr_to_tactic.h" @@ -1239,8 +1240,9 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) { expr new_eqns = new_s.instantiate_all(eqns); bool reject_type_is_meta = false; new_eqns = solve_unassigned_mvars(new_s, new_eqns, reject_type_is_meta); - if (display_unassigned_mvars(new_eqns, new_s)) + if (display_unassigned_mvars(new_eqns, new_s)) { return lazy_list(); + } type_checker_ptr tc = mk_type_checker(_env, std::move(ngen)); new_eqns = assign_equation_lhs_metas(*tc, new_eqns); expr val = compile_equations(*tc, _ios, new_eqns, meta, meta_type); @@ -1331,7 +1333,8 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { expr m = m_full_context.mk_meta(m_ngen, some_expr(type), eqns.get_tag()); register_meta(m); constraint c = mk_equations_cnstr(m, new_eqns); - cs += c; + /* We use stack policy for processing MaxDelayed constraints */ + cs = c + cs; return m; } @@ -1695,6 +1698,33 @@ expr elaborator::visit_prenum(expr const & e, constraint_seq & cs) { } } +expr elaborator::visit_checkpoint_expr(expr const & e, constraint_seq & cs) { + expr arg = get_annotation_arg(e); + expr m; + if (is_by(arg)) + m = m_context.mk_meta(m_ngen, none_expr(), e.get_tag()); + else + m = m_full_context.mk_meta(m_ngen, none_expr(), e.get_tag()); + register_meta(m); + local_context ctx = m_context; + local_context full_ctx = m_full_context; + bool in_equation_lhs = m_in_equation_lhs; + auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */, + name_generator && /* ngen */) { + flet set1(m_context, ctx); + flet set2(m_full_context, full_ctx); + flet set3(m_in_equation_lhs, in_equation_lhs); + pair rcs = visit(arg); + expr r = rcs.first; + constraint_seq cs = rcs.second; + cs = mk_eq_cnstr(meta, r, justification()) + cs; + return lazy_list(cs.to_list()); + }; + justification j; + cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Checkpoint), true, j); + return m; +} + expr elaborator::visit_core(expr const & e, constraint_seq & cs) { if (is_prenum(e)) { return visit_prenum(e, cs); @@ -1738,6 +1768,8 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) { return visit_structure_instance(e, cs); } else if (is_obtain_expr(e)) { return visit_obtain_expr(e, cs); + } else if (is_checkpoint_annotation(e)) { + return visit_checkpoint_expr(e, cs); } else { switch (e.kind()) { case expr_kind::Local: return e; diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 667de2ff7..c0e69f939 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -190,6 +190,8 @@ class elaborator : public coercion_info_manager { expr visit_prenum(expr const & e, constraint_seq & cs); + expr visit_checkpoint_expr(expr const & e, constraint_seq & cs); + void check_used_local_tactic_hints(); void show_goal(proof_state const & ps, expr const & start, expr const & end, expr const & curr); diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index 242848eca..fb6c0086f 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -133,23 +133,28 @@ expr copy_annotations(expr const & from, expr const & to) { return r; } -static name * g_have = nullptr; -static name * g_show = nullptr; +static name * g_have = nullptr; +static name * g_show = nullptr; +static name * g_checkpoint = nullptr; expr mk_have_annotation(expr const & e) { return mk_annotation(*g_have, e); } expr mk_show_annotation(expr const & e) { return mk_annotation(*g_show, e); } +expr mk_checkpoint_annotation(expr const & e) { return mk_annotation(*g_checkpoint, e); } bool is_have_annotation(expr const & e) { return is_annotation(e, *g_have); } bool is_show_annotation(expr const & e) { return is_annotation(e, *g_show); } +bool is_checkpoint_annotation(expr const & e) { return is_annotation(e, *g_checkpoint); } void initialize_annotation() { g_annotation = new name("annotation"); g_annotation_opcode = new std::string("Annot"); g_annotation_macros = new annotation_macros(); - g_have = new name("have"); - g_show = new name("show"); + g_have = new name("have"); + g_show = new name("show"); + g_checkpoint = new name("checkpoint"); register_annotation(*g_have); register_annotation(*g_show); + register_annotation(*g_checkpoint); register_macro_deserializer(get_annotation_opcode(), [](deserializer & d, unsigned num, expr const * args) { diff --git a/src/library/annotation.h b/src/library/annotation.h index 2d874f275..010e00f74 100644 --- a/src/library/annotation.h +++ b/src/library/annotation.h @@ -57,10 +57,12 @@ expr copy_annotations(expr const & from, expr const & to); expr mk_have_annotation(expr const & e); /** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */ expr mk_show_annotation(expr const & e); +expr mk_checkpoint_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_have_annotation. */ bool is_have_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_show_annotation. */ bool is_show_annotation(expr const & e); +bool is_checkpoint_annotation(expr const & e); /** \brief Return the serialization 'opcode' for annotation macros. */ std::string const & get_annotation_opcode(); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 3959061af..c96ff69d8 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -289,15 +289,30 @@ unify_status unify_simple(substitution & s, constraint const & c) { static constraint * g_dont_care_cnstr = nullptr; static unsigned g_group_size = 1u << 28; -constexpr unsigned g_num_groups = 8; -static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size, 7*g_group_size}; +constexpr unsigned g_num_groups = 9; +static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size, 7*g_group_size, 8*g_group_size}; static unsigned get_group_first_index(cnstr_group g) { return g_cnstr_group_first_index[static_cast(g)]; } -static cnstr_group to_cnstr_group(unsigned d) { - if (d >= g_num_groups) - d = g_num_groups-1; - return static_cast(d); + +static unsigned get_group_last_index(cnstr_group g) { + unsigned idx = static_cast(g); + lean_assert(idx < g_num_groups); + if (idx == g_num_groups - 1) { + lean_assert(g == cnstr_group::MaxDelayed); + return std::numeric_limits::max() - g_group_size; + } else { + lean_assert(idx < g_num_groups - 1); + return g_cnstr_group_first_index[idx+1] - 1; + } +} + +static cnstr_group to_cnstr_group(unsigned cidx) { + for (unsigned i = 1; i < g_num_groups; i++) { + if (cidx < g_cnstr_group_first_index[i]) + return static_cast(i); + } + return cnstr_group::MaxDelayed; } /** \brief Convert choice constraint delay factor to cnstr_group */ @@ -329,7 +344,7 @@ struct unifier_fn { name_generator m_ngen; substitution m_subst; constraints m_postponed; // constraints that will not be solved - owned_map m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m + owned_map m_owned_map; // mapping from metavariable name m to constraint idx expr_map m_type_map; // auxiliary map for storing the type of the expr in choice constraints unifier_plugin m_plugin; type_checker_ptr m_tc; @@ -542,14 +557,46 @@ struct unifier_fn { return added; } - /** \brief Add constraint to the constraint queue */ + /** \brief Add constraint to the constraint queue. + + \remark We use FIFO policy for all but MaxDelayed group. + */ unsigned add_cnstr(constraint const & c, cnstr_group g) { - unsigned cidx = m_next_cidx + get_group_first_index(g); + unsigned cidx; + if (g == cnstr_group::MaxDelayed) { + // MaxDelayed is a stack + cidx = get_group_last_index(g) - m_next_cidx; + /* Make sure there is at least one free space between any two MAX_DELAYED constraints. + We want to put constraints containing the variable owned by a MAX_DELAYED constraint c + after it and before the next MAX_DELAYED constraint c. */ + m_next_cidx += 2; + } else { + cidx = m_next_cidx + get_group_first_index(g); + m_next_cidx++; + } m_cnstrs.insert(cnstr(c, cidx)); - m_next_cidx++; return cidx; } + /** \brief Add constraint \c to the constraint queue, but + make sure it occurs AFTER the the constraint with index \c cidx. + + \remark We used this method to make sure \c c is going to be + processed after the constraint \c cidx. */ + unsigned add_cnstr_after(constraint const & c, unsigned cidx) { + cnstr_group g = to_cnstr_group(cidx); + unsigned new_cidx; + if (g == cnstr_group::MaxDelayed) { + // See add_cnstr + new_cidx = cidx + 1; + } else { + new_cidx = m_next_cidx + get_group_first_index(g); + m_next_cidx++; + } + m_cnstrs.insert(cnstr(c, new_cidx)); + return new_cidx; + } + /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j */ bool is_def_eq(expr const & t1, expr const & t2, justification const & j) { @@ -993,7 +1040,7 @@ struct unifier_fn { if (auto d = is_owned(c)) { // Metavariable in the constraint is owned by choice constraint. // So, we postpone this constraint. - add_cnstr(c, to_cnstr_group(*d+1)); + add_cnstr_after(c, *d); return true; } @@ -1126,12 +1173,12 @@ struct unifier_fn { bool preprocess_choice_constraint(constraint c) { if (!cnstr_on_demand(c)) { + unsigned cidx = add_cnstr(c, get_choice_cnstr_group(c)); if (cnstr_is_owner(c)) { expr m = get_app_fn(cnstr_expr(c)); lean_assert(is_metavar(m)); - m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(c)); + m_owned_map.insert(mlocal_name(m), cidx); } - add_cnstr(c, get_choice_cnstr_group(c)); return true; } else { expr m = cnstr_expr(c); @@ -2621,6 +2668,10 @@ struct unifier_fn { return Continue; } + void cut_search() { + m_case_splits.clear(); + } + /** \brief Process the next constraint in the constraint queue m_cnstrs */ bool process_next() { lean_assert(!m_cnstrs.empty()); @@ -2634,7 +2685,11 @@ struct unifier_fn { postpone(c); return true; } - lean_trace("unifier", tout() << "process_next: " << c << "\n";); + if (cidx >= get_group_first_index(cnstr_group::Checkpoint) && + cidx < get_group_first_index(cnstr_group::FlexFlex)) { + cut_search(); + } + lean_trace("unifier", tout() << "process_next: " << cidx << " " << static_cast(to_cnstr_group(cidx)) << " " << c << "\n";); m_cnstrs.erase_min(); if (is_choice_cnstr(c)) { return process_choice_constraint(c); @@ -2684,7 +2739,7 @@ struct unifier_fn { // Metavariable in the constraint is owned by choice constraint. // choice constraint was postponed... since c was not modifed // So, we should postpone this one too. - add_cnstr(c, to_cnstr_group(*d+1)); + add_cnstr_after(c, *d); return true; } else if (is_flex_rigid(c)) { return process_flex_rigid(c); diff --git a/src/library/unifier.h b/src/library/unifier.h index 0c95f7103..516fc0dcf 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -100,13 +100,16 @@ unify_result_seq unify(environment const & env, expr const & lhs, expr const & r 7) Epilogue: constraints that must be solved before FlexFlex are discarded/postponed. - 8) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other + 8) Checkpoint: unifier performs a prolog-like cut for any constraint in this group. + + 9) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then we simply discard it (or save it and return to the caller as residue). - 9) MaxDelayed: maximally delayed constraint group + 10) MaxDelayed: maximally delayed constraint group */ -enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, Epilogue, FlexFlex, MaxDelayed }; +enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, + Epilogue, Checkpoint, FlexFlex, MaxDelayed }; inline unsigned to_delay_factor(cnstr_group g) { return static_cast(g); } class unifier_exception : public exception {