From 1e5ba9bd7557fa663a75b78b1eb4ae05aa400c34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Sep 2014 16:07:41 -0700 Subject: [PATCH] refactor(frontends/lean/elaborator): move coercion_elaborator to its own module --- src/frontends/lean/CMakeLists.txt | 3 +- src/frontends/lean/coercion_elaborator.cpp | 121 +++++++++++++++++++++ src/frontends/lean/coercion_elaborator.h | 37 +++++++ src/frontends/lean/elaborator.cpp | 111 ++----------------- 4 files changed, 169 insertions(+), 103 deletions(-) create mode 100644 src/frontends/lean/coercion_elaborator.cpp create mode 100644 src/frontends/lean/coercion_elaborator.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index b34ba6eaa..aaa9c3e65 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -6,6 +6,7 @@ decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp 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) +local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp +coercion_elaborator.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp new file mode 100644 index 000000000..8357ac2c3 --- /dev/null +++ b/src/frontends/lean/coercion_elaborator.cpp @@ -0,0 +1,121 @@ +/* +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 "kernel/type_checker.h" +#include "kernel/metavar.h" +#include "kernel/constraint.h" +#include "library/coercion.h" +#include "library/unifier.h" +#include "frontends/lean/choice_iterator.h" +#include "frontends/lean/coercion_elaborator.h" + +namespace lean { + +struct coercion_elaborator : public choice_iterator { + coercion_info_manager & m_info; + expr m_arg; + bool m_id; // true if identity was not tried yet + list m_choices; + list m_coercions; + + coercion_elaborator(coercion_info_manager & info, expr const & arg, + list const & choices, list const & coes): + m_info(info), m_arg(arg), m_id(true), m_choices(choices), m_coercions(coes) { + lean_assert(length(m_coercions) + 1 == length(m_choices)); + } + + optional next() { + if (!m_choices) + return optional(); + if (m_id) { + m_id = false; + m_info.erase_coercion_info(m_arg); + } else if (m_coercions) { + expr c = head(m_coercions); + m_coercions = tail(m_coercions); + m_info.save_coercion_info(m_arg, mk_app(c, m_arg)); + } + auto r = head(m_choices); + m_choices = tail(m_choices); + return optional(r); + } +}; + +constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, + expr const & m, expr const & a, expr const & a_type, + justification const & j, unsigned delay_factor, bool relax) { + auto choice_fn = [=, &tc, &infom](expr const & mvar, expr const & d_type, substitution const & s, + name_generator const & /* ngen */) { + expr new_a_type; + justification new_a_type_jst; + if (is_meta(a_type)) { + auto p = substitution(s).instantiate_metavars(a_type); + new_a_type = p.first; + new_a_type_jst = p.second; + } else { + new_a_type = a_type; + } + if (is_meta(new_a_type)) { + if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) { + // postpone... + return lazy_list(constraints(mk_coercion_cnstr(tc, infom, m, a, a_type, justification(), + delay_factor+1, relax))); + } else { + // giveup... + return lazy_list(constraints(mk_eq_cnstr(mvar, a, justification(), relax))); + } + } + constraint_seq cs; + new_a_type = tc.whnf(new_a_type, cs); + if (is_meta(d_type)) { + // case-split + buffer> alts; + get_user_coercions(tc.env(), new_a_type, alts); + buffer choices; + buffer coes; + // first alternative: no coercion + constraint_seq cs1 = cs + mk_eq_cnstr(mvar, a, justification(), relax); + choices.push_back(cs1.to_list()); + unsigned i = alts.size(); + while (i > 0) { + --i; + auto const & t = alts[i]; + expr coe = std::get<1>(t); + expr new_a = copy_tag(a, mk_app(coe, a)); + coes.push_back(coe); + constraint_seq csi = cs + mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax); + choices.push_back(csi.to_list()); + } + return choose(std::make_shared(infom, mvar, + to_list(choices.begin(), choices.end()), + to_list(coes.begin(), coes.end()))); + } else { + expr new_a = a; + expr new_d_type = tc.whnf(d_type, cs); + expr const & d_cls = get_app_fn(new_d_type); + if (is_constant(d_cls)) { + if (auto c = get_coercion(tc.env(), new_a_type, const_name(d_cls))) { + new_a = copy_tag(a, mk_app(*c, a)); + infom.save_coercion_info(a, new_a); + } else { + infom.erase_coercion_info(a); + } + } + cs += mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax); + return lazy_list(cs.to_list()); + } + }; + return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax); +} + +/** \brief Given a term a : a_type, and an expected type generate a metavariable with a delayed coercion. */ +pair mk_coercion_elaborator(type_checker & tc, coercion_info_manager & infom, local_context & ctx, + bool relax, expr const & a, expr const & a_type, expr const & expected_type, + justification const & j) { + expr m = ctx.mk_meta(some_expr(expected_type), a.get_tag()); + return mk_pair(m, mk_coercion_cnstr(tc, infom, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), relax)); +} +} diff --git a/src/frontends/lean/coercion_elaborator.h b/src/frontends/lean/coercion_elaborator.h new file mode 100644 index 000000000..84b1e6c91 --- /dev/null +++ b/src/frontends/lean/coercion_elaborator.h @@ -0,0 +1,37 @@ +/* +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 "kernel/expr.h" +#include "kernel/type_checker.h" +#include "frontends/lean/local_context.h" + +namespace lean { +/** \brief Abstract class for hiding details of the info_manager from the coercion_elaborator */ +class coercion_info_manager { +public: + virtual void erase_coercion_info(expr const & e) = 0; + virtual void save_coercion_info(expr const & e, expr const & c) = 0; +}; + +/** \brief Create a metavariable, and attach choice constraint for generating + coercions of the form f a, where \c f is registered coercion, + and \c a is the input argument that has type \c a_type, but is expected + to have type \c expected_type because of \c j. + + This function is used when the types \c a_type and/or \c expected_type + are not known at preprocessing time, and a choice function is used to + enumerate coercion functions \c f. + + \param relax True if opaque constants in the current module should be treated + as transparent + + \see coercion_info_manager +*/ +pair mk_coercion_elaborator( + type_checker & tc, coercion_info_manager & infom, local_context & ctx, bool relax, + expr const & a, expr const & a_type, expr const & expected_type, justification const & j); +} diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d32d9b256..c3497d518 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -43,6 +43,7 @@ Author: Leonardo de Moura #include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" #include "frontends/lean/placeholder_elaborator.h" +#include "frontends/lean/coercion_elaborator.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -65,7 +66,7 @@ elaborator_context::elaborator_context(environment const & env, io_state const & } /** \brief Helper class for implementing the \c elaborate functions. */ -class elaborator { +class elaborator : public coercion_info_manager { typedef name_map local_tactic_hints; typedef rb_map, expr_quick_cmp> cache; @@ -255,7 +256,7 @@ public: /** \brief Auxiliary function for saving information about which coercion was used by the elaborator. It marks that coercion c was used on e. */ - void save_coercion_info(expr const & e, expr const & c) { + virtual void save_coercion_info(expr const & e, expr const & c) { if (!m_no_info && infom() && pip()) { if (auto p = pip()->get_pos_info(e)) { expr t = m_tc[m_relax_main_opaque]->infer(c).first; @@ -265,7 +266,7 @@ public: } /** \brief Remove coercion information associated with \c e */ - void erase_coercion_info(expr const & e) { + virtual void erase_coercion_info(expr const & e) { if (!m_no_info && infom() && pip()) { if (auto p = pip()->get_pos_info(e)) m_pre_info_data.erase_coercion_info(p->first, p->second); @@ -403,108 +404,14 @@ public: return a; } - struct coercion_case_split : public choice_iterator { - elaborator & m_elab; - expr m_arg; - bool m_id; // true if identity was not tried yet - list m_choices; - list m_coercions; - - coercion_case_split(elaborator & elab, expr const & arg, list const & choices, list const & coes): - m_elab(elab), m_arg(arg), m_id(true), m_choices(choices), m_coercions(coes) { - lean_assert(length(m_coercions) + 1 == length(m_choices)); - } - - optional next() { - if (!m_choices) - return optional(); - if (m_id) { - m_id = false; - m_elab.erase_coercion_info(m_arg); - } else if (m_coercions) { - expr c = head(m_coercions); - m_coercions = tail(m_coercions); - m_elab.save_coercion_info(m_arg, ::lean::mk_app(c, m_arg)); - } - auto r = head(m_choices); - m_choices = tail(m_choices); - return optional(r); - } - }; - - constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type, - justification const & j, unsigned delay_factor) { - bool relax = m_relax_main_opaque; - auto choice_fn = [=](expr const & mvar, expr const & d_type, substitution const & s, - name_generator const & /* ngen */) { - type_checker & tc = *m_tc[relax]; - expr new_a_type; - justification new_a_type_jst; - if (is_meta(a_type)) { - auto p = substitution(s).instantiate_metavars(a_type); - new_a_type = p.first; - new_a_type_jst = p.second; - } else { - new_a_type = a_type; - } - if (is_meta(new_a_type)) { - if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) { - // postpone... - return lazy_list(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), - delay_factor+1))); - } else { - // giveup... - return lazy_list(constraints(mk_eq_cnstr(mvar, a, justification(), relax))); - } - } - constraint_seq cs; - new_a_type = tc.whnf(new_a_type, cs); - if (is_meta(d_type)) { - // case-split - buffer> alts; - get_user_coercions(env(), new_a_type, alts); - buffer choices; - buffer coes; - // first alternative: no coercion - constraint_seq cs1 = cs + mk_eq_cnstr(mvar, a, justification(), relax); - choices.push_back(cs1.to_list()); - unsigned i = alts.size(); - while (i > 0) { - --i; - auto const & t = alts[i]; - expr coe = std::get<1>(t); - expr new_a = mk_app(coe, a, a.get_tag()); - coes.push_back(coe); - constraint_seq csi = cs + mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax); - choices.push_back(csi.to_list()); - } - return choose(std::make_shared(*this, mvar, - to_list(choices.begin(), choices.end()), - to_list(coes.begin(), coes.end()))); - } else { - expr new_a = a; - expr new_d_type = tc.whnf(d_type, cs); - expr const & d_cls = get_app_fn(new_d_type); - if (is_constant(d_cls)) { - if (auto c = get_coercion(env(), new_a_type, const_name(d_cls))) { - new_a = mk_app(*c, a, a.get_tag()); - save_coercion_info(a, new_a); - } else { - erase_coercion_info(a); - } - } - cs += mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax); - return lazy_list(cs.to_list()); - } - }; - return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, m_relax_main_opaque); - } - /** \brief Given a term a : a_type, and an expected type generate a metavariable with a delayed coercion. */ pair mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type, justification const & j) { - expr m = m_full_context.mk_meta(some_expr(expected_type), a.get_tag()); - return to_ecs(m, mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic))); + bool relax = m_relax_main_opaque; + type_checker & tc = *m_tc[relax]; + pair ec = mk_coercion_elaborator(tc, *this, m_full_context, relax, + a, a_type, expected_type, j); + return to_ecs(ec.first, ec.second); } /** \brief Given a term a : a_type, ensure it has type \c expected_type. Apply coercions if needed