From fab7934265b4f07184baa4fd9d041bb16e5e2bcc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Jul 2014 02:53:02 +0100 Subject: [PATCH] refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 239 +++++++++++++++++------------- src/library/placeholder.cpp | 22 ++- src/library/placeholder.h | 8 +- tests/lean/run/class7.lean | 25 ++++ tests/lean/run/class8.lean | 33 +++++ tests/lean/run/group2.lean | 2 + tests/lean/run/tactic25.lean | 2 - 7 files changed, 213 insertions(+), 118 deletions(-) create mode 100644 tests/lean/run/class7.lean create mode 100644 tests/lean/run/class8.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 267c60d17..ba4719de2 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -268,21 +268,26 @@ class elaborator { This is a helper class for implementing this choice function. */ struct placeholder_elaborator : public choice_elaborator { - elaborator & m_elab; - expr m_mvar; - expr m_mvar_type; // elaborated type of the metavariable - list m_local_instances; // local instances that should also be included in the class-instance resolution. - list m_instances; // global declaration names that are class instances. This information is retrieved using #get_class_instances. - context m_ctx; // local context for m_mvar - substitution m_subst; - justification m_jst; + elaborator & m_elab; + expr m_meta; + expr m_meta_type; // elaborated type of the metavariable + list m_local_instances; // local instances that should also be included in the class-instance resolution. + list m_instances; // global declaration names that are class instances. + // This information is retrieved using #get_class_instances. + list m_tactics; + proof_state_seq m_tactic_result; // result produce by last executed tactic. + buffer m_mvars_in_meta_type; // metavariables that occur in m_meta_type, the tactics may instantiate some of them + context m_ctx; // local context for m_meta + substitution m_subst; + justification m_jst; - placeholder_elaborator(elaborator & elab, expr const & mvar, expr const & mvar_type, - list const & local_insts, list const & instances, bool has_tactic_hints, - context const & ctx, substitution const & s, justification const & j): - choice_elaborator(has_tactic_hints), - m_elab(elab), m_mvar(mvar), m_mvar_type(mvar_type), m_local_instances(local_insts), m_instances(instances), - m_ctx(ctx), m_subst(s), m_jst(j) { + placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type, + list const & local_insts, list const & instances, list const & tacs, + context const & ctx, substitution const & s, justification const & j, bool ignore_failure): + choice_elaborator(ignore_failure), + m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances), + m_tactics(tacs), m_ctx(ctx), m_subst(s), m_jst(j) { + collect_metavars(meta_type, m_mvars_in_meta_type); } optional try_instance(name const & inst) { @@ -291,29 +296,47 @@ class elaborator { return optional(); expr type = decl->get_type(); // create the term pre (inst _ ... _) - expr pre = copy_tag(m_mvar, mk_explicit(copy_tag(m_mvar, mk_constant(inst)))); + expr pre = copy_tag(m_meta, mk_explicit(copy_tag(m_meta, mk_constant(inst)))); while (is_pi(type)) { type = binding_body(type); - pre = copy_tag(m_mvar, ::lean::mk_app(pre, copy_tag(m_mvar, mk_expr_placeholder()))); + pre = copy_tag(m_meta, ::lean::mk_app(pre, copy_tag(m_meta, mk_strict_expr_placeholder()))); } try { scope s(m_elab, m_ctx, m_subst); expr r = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc. justification j = m_elab.m_accumulated; m_elab.consume_tc_cnstrs(); + for (auto & c : m_elab.m_constraints) + c = update_justification(c, mk_composite1(m_jst, c.get_justification())); list cs = to_list(m_elab.m_constraints.begin(), m_elab.m_constraints.end()); - cs = cons(mk_eq_cnstr(m_mvar, r, mk_composite1(m_jst, j)), cs); + cs = cons(mk_eq_cnstr(m_meta, r, mk_composite1(m_jst, j)), cs); return optional(cs); } catch (exception &) { return optional(); } } + optional get_next_tactic_result() { + while (auto next = m_tactic_result.pull()) { + m_tactic_result = next->second; + if (!empty(next->first.get_goals())) + continue; // has unsolved goals + substitution subst = next->first.get_subst(); + buffer cs; + expr const & mvar = get_app_fn(m_meta); + cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst)); + for (auto const & mvar : m_mvars_in_meta_type) + cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst)); + return optional(to_list(cs.begin(), cs.end())); + } + return optional(); + } + virtual optional next() { while (!empty(m_local_instances)) { expr inst = head(m_local_instances); m_local_instances = tail(m_local_instances); - constraints cs(mk_eq_cnstr(m_mvar, inst, m_jst)); + constraints cs(mk_eq_cnstr(m_meta, inst, m_jst)); return optional(cs); } while (!empty(m_instances)) { @@ -322,6 +345,18 @@ class elaborator { if (auto cs = try_instance(inst)) return cs; } + if (auto cs = get_next_tactic_result()) + return cs; + while (!empty(m_tactics)) { + tactic const & tac = head(m_tactics).get_tactic(); + m_tactics = tail(m_tactics); + proof_state ps(goals(goal(m_meta, m_meta_type)), m_subst, m_elab.m_ngen.mk_child()); + try { + m_tactic_result = tac(m_elab.m_env, m_elab.m_ios, ps); + if (auto cs = get_next_tactic_result()) + return cs; + } catch (...) {} + } return optional(); } }; @@ -513,14 +548,18 @@ public: bool is_class(expr const & type) { expr f = get_app_fn(type); - return is_constant(f) && ::lean::is_class(m_env, const_name(f)); + if (!is_constant(f)) + return false; + name const & cls_name = const_name(f); + return ::lean::is_class(m_env, cls_name) || !empty(get_tactic_hints(m_env, cls_name)); } - bool may_be_class(expr const & type) { - if (is_meta(type)) - return true; - else - return is_class(type); + static expr instantiate_meta(expr const & meta, substitution const & subst) { + buffer locals; + expr mvar = get_app_args(meta, locals); + mvar = update_mlocal(mvar, subst.instantiate(mlocal_type(mvar))); + for (auto & local : locals) local = subst.instantiate(local); + return ::lean::mk_app(mvar, locals); } /** \brief Return a 'failed to synthesize placholder' justification for the given @@ -528,53 +567,62 @@ public: justification mk_failed_to_synthesize_jst(expr const & m) { environment env = m_env; return mk_justification(m, [=](formatter const & fmt, substitution const & subst) { - buffer locals; - expr mvar = get_app_args(m, locals); - mvar = update_mlocal(mvar, subst.instantiate(mlocal_type(mvar))); - for (auto & local : locals) local = subst.instantiate(local); - expr new_m = ::lean::mk_app(mvar, locals); + expr new_m = instantiate_meta(m, subst); expr new_type = type_checker(env).infer(new_m); proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare")); return format({format("failed to synthesize placeholder"), line(), ps.pp(fmt)}); }); } - /** \brief Create a metavariable, but also add a class-constraint if type is a class - or a metavariable. - */ - expr mk_placeholder_meta(optional const & type, tag g) { - expr m = mk_meta(type, g); - if (!type || may_be_class(*type)) { - context ctx = m_ctx; - justification j = mk_failed_to_synthesize_jst(m); - auto choice_fn = [=](expr const & mvar, expr const & mvar_type, substitution const & s, name_generator const & /* ngen */) { - if (!is_class(mvar_type)) - return lazy_list(constraints()); - list local_insts; - if (m_use_local_instances) { - buffer buffer; - for (auto const & l : ctx) { - if (!is_local(l)) - continue; - expr inst_type = mlocal_type(l); - if (!is_constant(get_app_fn(inst_type)) || - const_name(get_app_fn(inst_type)) != const_name(get_app_fn(mvar_type))) - continue; - buffer.push_back(l); - } - local_insts = to_list(buffer.begin(), buffer.end()); - } - auto insts = get_class_instances(mvar_type); - if (empty(insts) && empty(local_insts)) { - return lazy_list(constraints()); - } else { - bool has_tactic_hints = !empty(get_tactic_hints(m_env, const_name(get_app_fn(mvar_type)))); - return choose(std::make_shared(*this, mvar, mvar_type, local_insts, insts, has_tactic_hints, - ctx, s, j)); - } - }; - add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j)); + /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ + static list get_local_instances(context ctx, name const & cls_name) { + buffer buffer; + for (auto const & l : ctx) { + if (!is_local(l)) + continue; + expr inst_type = mlocal_type(l); + if (!is_constant(get_app_fn(inst_type)) || const_name(get_app_fn(inst_type)) != cls_name) + continue; + buffer.push_back(l); } + return to_list(buffer.begin(), buffer.end()); + } + + /** \brief Create a metavariable, and attach choice constraint for generating + solutions using class-instances and tactic-hints. + */ + expr mk_placeholder_meta(optional const & type, tag g, bool is_strict = false) { + expr m = mk_meta(type, g); + context ctx = m_ctx; + justification j = mk_failed_to_synthesize_jst(m); + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & /* ngen */) { + expr const & mvar = get_app_fn(meta); + if (is_class(meta_type)) { + name const & cls_name = const_name(get_app_fn(meta_type)); + list local_insts; + if (m_use_local_instances) + local_insts = get_local_instances(ctx, cls_name); + list insts = get_class_instances(meta_type); + list tacs; + if (!s.is_assigned(mvar)) + tacs = get_tactic_hints(m_env, cls_name); + if (empty(local_insts) && empty(insts) && empty(tacs)) + return lazy_list(); // nothing to be done + bool ignore_failure = false; // we are always strict with placeholders associated with classes + return choose(std::make_shared(*this, meta, meta_type, local_insts, insts, tacs, ctx, s, j, + ignore_failure)); + } else if (s.is_assigned(mvar)) { + // if the metavariable is assigned and it is not a class, then we just ignore it, and return + // the an empty set of constraints. + return lazy_list(constraints()); + } else { + list tacs = get_tactic_hints(m_env); + bool ignore_failure = !is_strict; + return choose(std::make_shared(*this, meta, meta_type, list(), list(), tacs, ctx, s, j, + ignore_failure)); + } + }; + add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j)); return m; } @@ -597,7 +645,7 @@ public: expr visit_expecting_type_of(expr const & e, expr const & t) { if (is_placeholder(e) && !placeholder_type(e)) - return mk_placeholder_meta(some_expr(t), e.get_tag()); + return mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e)); else if (is_choice(e)) return visit_choice(e, some_expr(t)); else if (is_by(e)) @@ -754,7 +802,7 @@ public: } expr visit_placeholder(expr const & e) { - return mk_placeholder_meta(placeholder_type(e), e.get_tag()); + return mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e)); } level replace_univ_placeholder(level const & l) { @@ -914,7 +962,7 @@ public: return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), true, m_ios.get_options()); } - void collect_metavars(expr const & e, buffer & mvars) { + static void collect_metavars(expr const & e, buffer & mvars) { for_each(e, [&](expr const & e, unsigned) { if (is_metavar(e)) { mvars.push_back(e); @@ -983,24 +1031,22 @@ public: /** \brief Try to instantiate meta-variable \c mvar (modulo its state ps) using the given tactic. If it succeeds, then update subst with the solution. - If \c report_failure is true, then display error messages. to the user. Return true iff the metavariable \c mvar has been assigned. */ - bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac, bool report_failure) { + bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac) { lean_assert(length(ps.get_goals()) == 1); - lean_assert(get_app_fn(head(ps.get_goals()).get_meta()) == mvar); // make sure ps is a really a proof state for mvar. + // make sure ps is a really a proof state for mvar. + lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar)); try { proof_state_seq seq = tac(m_env, m_ios, ps); auto r = seq.pull(); if (!r) { // tactic failed to produce any result - if (report_failure) - display_unsolved_proof_state(mvar, ps, "tactic failed"); + display_unsolved_proof_state(mvar, ps, "tactic failed"); return false; } else if (!empty(r->first.get_goals())) { // tactic contains unsolved subgoals - if (report_failure) - display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); return false; } else { subst = r->first.get_subst(); @@ -1009,48 +1055,27 @@ public: return true; } } catch (tactic_exception & ex) { - if (report_failure) { - auto out = regular(m_env, m_ios); - display_error_pos(out, m_pos_provider, ex.get_expr()); - out << " tactic failed: " << ex.what() << "\n"; - } + auto out = regular(m_env, m_ios); + display_error_pos(out, m_pos_provider, ex.get_expr()); + out << " tactic failed: " << ex.what() << "\n"; return false; } } - bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, list const & tacs) { - return std::any_of(tacs.begin(), tacs.end(), - [&](tactic_hint_entry const & e) { - return try_using(subst, mvar, ps, e.get_tactic(), false); - }); - } - void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited) { if (visited.contains(mlocal_name(mvar))) return; visited.insert(mlocal_name(mvar)); - auto meta = mvar_to_meta(mvar); - if (!meta) - return; - buffer locals; - get_app_args(*meta, locals); - for (expr & l : locals) - l = subst.instantiate(l); - mvar = update_mlocal(mvar, subst.instantiate(mlocal_type(mvar))); - meta = ::lean::mk_app(mvar, locals); - expr type = m_tc->infer(*meta); - // first solve unassigned metavariables in type - type = solve_unassigned_mvars(subst, type, visited); - proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child()); if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) { - try_using(subst, mvar, ps, *local_hint, true); - } else { - if (is_constant(get_app_fn(type))) { - name cls = const_name(get_app_fn(type)); - if (try_using(subst, mvar, ps, get_tactic_hints(m_env, cls))) - return; - } - try_using(subst, mvar, ps, get_tactic_hints(m_env)); + auto meta = mvar_to_meta(mvar); + if (!meta) + return; + meta = instantiate_meta(*meta, subst); + expr type = m_tc->infer(*meta); + // first solve unassigned metavariables in type + type = solve_unassigned_mvars(subst, type, visited); + proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child()); + try_using(subst, mvar, ps, *local_hint); } } diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index b6c8b5186..fb97dac45 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -10,7 +10,8 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" namespace lean { -static name g_placeholder_name = name(name::mk_internal_unique_name(), "_"); +static name g_placeholder_name = name(name::mk_internal_unique_name(), "_"); +static name g_strict_placeholder_name = name(name::mk_internal_unique_name(), "_"); MK_THREAD_LOCAL_GET(unsigned, get_placeholder_id, 0) static unsigned next_placeholder_id() { unsigned & c = get_placeholder_id(); @@ -19,19 +20,26 @@ static unsigned next_placeholder_id() { return r; } level mk_level_placeholder() { return mk_global_univ(name(g_placeholder_name, next_placeholder_id())); } -expr mk_expr_placeholder(optional const & type) { - name n(g_placeholder_name, next_placeholder_id()); +expr mk_expr_placeholder(optional const & type, bool strict) { + name const & prefix = strict ? g_strict_placeholder_name : g_placeholder_name; + name n(prefix, next_placeholder_id()); if (type) return mk_local(n, *type); else return mk_constant(n); } -static bool is_placeholder(name const & n) { return !n.is_atomic() && n.get_prefix() == g_placeholder_name; } +static bool is_placeholder(name const & n) { + return !n.is_atomic() && (n.get_prefix() == g_placeholder_name || n.get_prefix() == g_strict_placeholder_name); +} +static bool is_strict_placeholder(name const & n) { + return !n.is_atomic() && n.get_prefix() == g_strict_placeholder_name; +} bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); } bool is_placeholder(expr const & e) { - return - (is_constant(e) && is_placeholder(const_name(e))) || - (is_local(e) && is_placeholder(mlocal_name(e))); + return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(mlocal_name(e))); +} +bool is_strict_placeholder(expr const & e) { + return (is_constant(e) && is_strict_placeholder(const_name(e))) || (is_local(e) && is_strict_placeholder(mlocal_name(e))); } optional placeholder_type(expr const & e) { diff --git a/src/library/placeholder.h b/src/library/placeholder.h index 8d55011cd..9f122a0e2 100644 --- a/src/library/placeholder.h +++ b/src/library/placeholder.h @@ -15,14 +15,18 @@ namespace lean { level mk_level_placeholder(); /** \brief Return a new expression placeholder expression. */ -expr mk_expr_placeholder(optional const & type = none_expr()); +expr mk_expr_placeholder(optional const & type = none_expr(), bool strict = false); +inline expr mk_strict_expr_placeholder(optional const & type = none_expr()) { return mk_expr_placeholder(type, true); } /** \brief Return true if the given level is a placeholder. */ bool is_placeholder(level const & e); -/** \brief Return true iff the given expression is a placeholder. */ +/** \brief Return true iff the given expression is a placeholder (strict or not). */ bool is_placeholder(expr const & e); +/** \brief Return true iff the given expression is a strict placeholder (strict or not). */ +bool is_strict_placeholder(expr const & e); + /** \brief Return the type of the placeholder (if available) */ optional placeholder_type(expr const & e); diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean new file mode 100644 index 000000000..5bfc129cf --- /dev/null +++ b/tests/lean/run/class7.lean @@ -0,0 +1,25 @@ +import standard +using num tactic + +inductive inh (A : Type) : Type := +| inh_intro : A -> inh A + +instance inh_intro + +theorem inh_bool [instance] : inh Bool +:= inh_intro true + +theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) +:= inh_rec (λ b, inh_intro (λ a : A, b)) H + +definition assump := eassumption; now + +set_option elaborator.local_instances false +tactic_hint [inh] assump +tactic_hint assump + +theorem tst {A B : Type} (H : inh B) : inh (A → B → B) + +theorem T1 {A : Type} (a : A) : inh A + +theorem T2 : inh Bool diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean new file mode 100644 index 000000000..3e9044130 --- /dev/null +++ b/tests/lean/run/class8.lean @@ -0,0 +1,33 @@ +import standard +using num tactic pair + +inductive inh (A : Type) : Bool := +| inh_intro : A -> inh A + +instance inh_intro + +theorem inh_elim {A : Type} {B : Bool} (H1 : inh A) (H2 : A → B) : B +:= inh_rec H2 H1 + +theorem inh_exists [instance] {A : Type} {P : A → Bool} (H : ∃x, P x) : inh A +:= obtain w Hw, from H, inh_intro w + +theorem inh_bool [instance] : inh Bool +:= inh_intro true + +theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) +:= inh_rec (λb, inh_intro (λa : A, b)) H + +theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (pair A B) +:= inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (mk_pair a b))) + +definition assump := eassumption +tactic_hint assump + +theorem tst {A B : Type} (H : inh B) : inh (A → B → B) + +theorem T1 {A B C D : Type} {P : C → Bool} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Bool) + +(* +print(get_env():find("T1"):value()) +*) \ No newline at end of file diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index cb72a1ec1..5d1b2b6f2 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -61,5 +61,7 @@ definition real_group_struct [inline] [instance] : group_struct pos_real variables x y : pos_real check x * y +set_option pp.implicit true +print "---------------" theorem T (a b : pos_real): (rmul a b) = a*b := refl (rmul a b) diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index 20382cce2..6cbc7081c 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -16,6 +16,4 @@ definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | assumption]) tactic_hint [or] my_tac3 - theorem T3 {a b c : Bool} (Hb : b) : a ∨ b ∨ c -