From d647954f9380df6d1136615a6b7ccf1ea0505abe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Sep 2014 10:21:10 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): constraints associated with 'proof-qed' blocks are solved independently, closes #82 --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 38 +++++------- src/frontends/lean/local_context.cpp | 1 + src/frontends/lean/local_context.h | 1 + src/frontends/lean/placeholder_elaborator.cpp | 19 ------ src/frontends/lean/proof_qed_elaborator.cpp | 62 +++++++++++++++++++ src/frontends/lean/proof_qed_elaborator.h | 17 +++++ src/frontends/lean/util.cpp | 31 ++++++++++ src/frontends/lean/util.h | 14 +++++ src/library/unifier.cpp | 6 +- src/library/unifier.h | 15 +++-- 11 files changed, 156 insertions(+), 50 deletions(-) create mode 100644 src/frontends/lean/proof_qed_elaborator.cpp create mode 100644 src/frontends/lean/proof_qed_elaborator.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index aaa9c3e65..8747c56c3 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,6 +7,6 @@ dependencies.cpp parser_bindings.cpp begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp -coercion_elaborator.cpp) +coercion_elaborator.cpp proof_qed_elaborator.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0cb5961cd..e0a6fa48c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -45,6 +45,7 @@ Author: Leonardo de Moura #include "frontends/lean/choice_iterator.h" #include "frontends/lean/placeholder_elaborator.h" #include "frontends/lean/coercion_elaborator.h" +#include "frontends/lean/proof_qed_elaborator.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -153,11 +154,11 @@ class elaborator : public coercion_info_manager { }; public: - elaborator(elaborator_context & env, list const & ctx, name_generator const & ngen): + elaborator(elaborator_context & env, name_generator const & ngen): m_env(env), m_ngen(ngen), - m_context(m_ngen.next(), ctx), - m_full_context(m_ngen.next(), ctx), + m_context(m_ngen.next()), + m_full_context(m_ngen.next()), m_unifier_config(env.m_ios.get_options(), true /* use exceptions */, true /* discard */) { m_relax_main_opaque = false; m_no_info = false; @@ -326,10 +327,13 @@ public: return m; } - expr visit_proof_qed(expr const & e, optional const & /* t */, constraint_seq & cs) { + expr visit_proof_qed(expr const & e, optional const & t, constraint_seq & cs) { lean_assert(is_proof_qed_annotation(e)); - // TODO(Leo) - return visit(get_annotation_arg(e), cs); + pair ecs = visit(get_annotation_arg(e)); + pair mc = mk_proof_qed_elaborator(env(), m_full_context, ecs.first, t, ecs.second, + m_unifier_config, m_relax_main_opaque); + cs += mc.second; + return mc.first; } /** \brief Make sure \c f is really a function, if it is not, try to apply coercions. @@ -642,18 +646,7 @@ public: constraint_seq v_cs; expr v = visit(get_typed_expr_expr(e), v_cs); expr v_type = infer_type(v, v_cs); - justification j = mk_justification(e, [=](formatter const & fmt, substitution const & subst) { - substitution s(subst); - format expected_fmt, given_fmt; - std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, s.instantiate(t), s.instantiate(v_type)); - format r("type mismatch at term"); - r += pp_indent_expr(fmt, s.instantiate(v)); - r += compose(line(), format("has type")); - r += given_fmt; - r += compose(line(), format("but is expected to have type")); - r += expected_fmt; - return r; - }); + justification j = mk_type_mismatch_jst(v, v_type, t, e); auto new_vcs = ensure_has_type(v, v_type, t, j, m_relax_main_opaque); v = new_vcs.first; cs += t_cs + new_vcs.second + v_cs; @@ -914,7 +907,10 @@ public: return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end())); } - std::tuple operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) { + std::tuple operator()(list const & ctx, expr const & e, bool _ensure_type, + bool relax_main_opaque) { + m_context.set_ctx(ctx); + m_full_context.set_ctx(ctx); flet set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(env())); constraint_seq cs; expr r = visit(e, cs); @@ -961,11 +957,11 @@ static name g_tmp_prefix = name::mk_internal_unique_name(); std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, bool relax_main_opaque, bool ensure_type) { - return elaborator(env, ctx, name_generator(g_tmp_prefix))(e, ensure_type, relax_main_opaque); + return elaborator(env, name_generator(g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque); } std::tuple elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v, bool is_opaque) { - return elaborator(env, list(), name_generator(g_tmp_prefix))(t, v, n, is_opaque); + return elaborator(env, name_generator(g_tmp_prefix))(t, v, n, is_opaque); } } diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp index f427e8ff7..ad558e817 100644 --- a/src/frontends/lean/local_context.cpp +++ b/src/frontends/lean/local_context.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "frontends/lean/local_context.h" namespace lean { +local_context::local_context(name const & prefix):m_ngen(prefix) {} local_context::local_context(name const & prefix, list const & ctx): m_ngen(prefix) { set_ctx(ctx); diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h index 93d7cf643..903a44ca7 100644 --- a/src/frontends/lean/local_context.h +++ b/src/frontends/lean/local_context.h @@ -22,6 +22,7 @@ class local_context { buffer m_ctx_buffer; // m_ctx as a buffer buffer m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg public: + local_context(name const & prefix); local_context(name const & prefix, list const & ctx); void set_ctx(list const & ctx); diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 8e8bafd7e..a0d5f3e78 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -250,25 +250,6 @@ pair mk_placeholder_elaborator(std::shared_ptr update_meta(expr const & meta, substitution s) { - buffer args; - expr mvar = get_app_args(meta, args); - justification j; - auto p = s.instantiate_metavars(mlocal_type(mvar)); - mvar = update_mlocal(mvar, p.first); - j = p.second; - for (expr & arg : args) { - auto p = s.instantiate_metavars(mlocal_type(arg)); - arg = update_mlocal(arg, p.first); - j = mk_composite1(j, p.second); - } - return mk_pair(mk_app(mvar, args), j); -} - constraint mk_placeholder_root_cnstr(std::shared_ptr const & C, expr const & m, bool is_strict, unifier_config const & cfg, unsigned delay_factor) { environment const & env = C->env(); diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp new file mode 100644 index 000000000..c93d8a40e --- /dev/null +++ b/src/frontends/lean/proof_qed_elaborator.cpp @@ -0,0 +1,62 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/unifier.h" +#include "library/opaque_hints.h" +#include "library/metavar_closure.h" +#include "frontends/lean/util.h" +#include "frontends/lean/local_context.h" + +namespace lean { +constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e, + constraint_seq const & cs, unifier_config const & cfg, bool relax) { + justification j = mk_failed_to_synthesize_jst(env, m); + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, + name_generator const & _ngen) { + name_generator ngen(_ngen); + type_checker_ptr tc(mk_type_checker_with_hints(env, ngen.mk_child(), relax)); + pair tcs = tc->infer(e); + expr e_type = tcs.first; + justification new_j = mk_type_mismatch_jst(e, e_type, meta_type); + pair dcs = tc->is_def_eq(e_type, meta_type, new_j); + if (!dcs.first) + throw unifier_exception(new_j, s); + constraint_seq new_cs = cs + tcs.second + dcs.second; + buffer cs_buffer; + new_cs.linearize(cs_buffer); + cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax)); + unifier_config new_cfg(cfg); + new_cfg.m_discard = false; + unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, new_cfg); + auto p = seq.pull(); + lean_assert(p); + substitution new_s = p->first.first; + constraints postponed = map(p->first.second, + [&](constraint const & c) { + // we erase internal justifications + return update_justification(c, j); + }); + metavar_closure cls(meta); + cls.add(meta_type); + constraints r = cls.mk_constraints(new_s, j, relax); + return append(r, postponed); + }; + bool owner = false; + return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax); +} + +/** \brief Create a metavariable m, and attach "choice" constraint that postpone the + solving the constraints (cs union m =?= e). +*/ +pair mk_proof_qed_elaborator( + environment const & env, local_context & ctx, + expr const & e, optional const & type, constraint_seq const & cs, + unifier_config const & cfg, bool relax) { + expr m = ctx.mk_meta(type, e.get_tag()); + constraint c = mk_proof_qed_cnstr(env, m, e, cs, cfg, relax); + return mk_pair(m, c); +} +} diff --git a/src/frontends/lean/proof_qed_elaborator.h b/src/frontends/lean/proof_qed_elaborator.h new file mode 100644 index 000000000..e426d9c8a --- /dev/null +++ b/src/frontends/lean/proof_qed_elaborator.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/unifier.h" + +namespace lean { +/** \brief Create a metavariable m, and attach "choice" constraint that postpone the + solving the constraints (cs union m =?= e). +*/ +pair mk_proof_qed_elaborator(environment const & env, local_context & ctx, + expr const & e, optional const & type, constraint_seq const & cs, + unifier_config const & cfg, bool relax); +} diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 0e7459831..b829aff00 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/replace_fn.h" +#include "kernel/error_msgs.h" #include "kernel/for_each_fn.h" #include "library/scoped_ext.h" #include "library/locals.h" @@ -226,4 +227,34 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const & return format("failed to synthesize placeholder") + line() + ps.pp(fmt); }); } + +justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src) { + return mk_justification(src, [=](formatter const & fmt, substitution const & subst) { + substitution s(subst); + format expected_fmt, given_fmt; + std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, s.instantiate(t), s.instantiate(v_type)); + format r("type mismatch at term"); + r += pp_indent_expr(fmt, s.instantiate(v)); + r += compose(line(), format("has type")); + r += given_fmt; + r += compose(line(), format("but is expected to have type")); + r += expected_fmt; + return r; + }); +} + +pair update_meta(expr const & meta, substitution s) { + buffer args; + expr mvar = get_app_args(meta, args); + justification j; + auto p = s.instantiate_metavars(mlocal_type(mvar)); + mvar = update_mlocal(mvar, p.first); + j = p.second; + for (expr & arg : args) { + auto p = s.instantiate_metavars(mlocal_type(arg)); + arg = update_mlocal(arg, p.first); + j = mk_composite1(j, p.second); + } + return mk_pair(mk_app(mvar, args), j); +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 1b754ccd3..2c58c8b6f 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -49,4 +49,18 @@ expr instantiate_meta(expr const & meta, substitution & subst); /** \brief Return a 'failed to synthesize placholder' justification for the given metavariable application \c m of the form (?m l_1 ... l_k) */ justification mk_failed_to_synthesize_jst(environment const & env, expr const & m); + +/** \brief Return a justification for \c v_type being definitionally equal to \c t, + v : v_type, the expressiong \c src is used to extract position information. +*/ +justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src); +inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t) { + return mk_type_mismatch_jst(v, v_type, t, v); +} + +/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of + ?m and local constants l_i + Return the updated expression and a justification for all substitutions. +*/ +pair update_meta(expr const & meta, substitution s); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 675a910ce..089cb0ba6 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -245,9 +245,9 @@ unify_status unify_simple(substitution & s, constraint const & c) { } static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false); -static unsigned g_group_size = 1u << 29; -constexpr unsigned g_num_groups = 7; -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}; +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}; static unsigned get_group_first_index(cnstr_group g) { return g_cnstr_group_first_index[static_cast(g)]; } diff --git a/src/library/unifier.h b/src/library/unifier.h index a70163e96..ccdddbfe2 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -53,7 +53,8 @@ unify_result_seq unify(environment const & env, expr const & lhs, expr const & r substitution const & s = substitution(), unifier_config const & c = unifier_config()); /** - The unifier divides the constraints in 8 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed + The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, + Epilogue, FlexFlex, MaxDelayed 1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t. The are not even inserted in the constraint priority queue. @@ -71,13 +72,15 @@ unify_result_seq unify(environment const & env, expr const & lhs, expr const & r 6) ClassInstance: for delayed choice constraints (we use this group for class-instance). - 7) 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. + 7) Epilogue: constraints that must be solved before FlexFlex are discarded/postponed. - 8) MaxDelayed: maximally delayed constraint group + 8) 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 */ -enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed }; +enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, Epilogue, FlexFlex, MaxDelayed }; inline unsigned to_delay_factor(cnstr_group g) { return static_cast(g); } class unifier_exception : public exception {