michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean/elaborator): move coercion_elaborator to its own module

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-10 16:07:41 -07:00
parent 6bc41f8dde
commit 1e5ba9bd75
4 changed files with 169 additions and 103 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/CMakeLists.txt
View file

@ -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})

121
src/frontends/lean/coercion_elaborator.cpp Normal file
View file

@ -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<constraints> m_choices;
list<expr> m_coercions;
coercion_elaborator(coercion_info_manager & info, expr const & arg,
list<constraints> const & choices, list<expr> 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<constraints> next() {
if (!m_choices)
return optional<constraints>();
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<constraints>(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>(constraints(mk_coercion_cnstr(tc, infom, m, a, a_type, justification(),
delay_factor+1, relax)));
} else {
// giveup...
return lazy_list<constraints>(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<std::tuple<name, expr, expr>> alts;
get_user_coercions(tc.env(), new_a_type, alts);
buffer<constraints> choices;
buffer<expr> 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<coercion_elaborator>(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<constraints>(cs.to_list());
}
};
return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax);
}
/** \brief Given a term <tt>a : a_type</tt>, and an expected type generate a metavariable with a delayed coercion. */
pair<expr, constraint> 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));
}
}

37
src/frontends/lean/coercion_elaborator.h Normal file
View file

@ -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 <tt>f a</tt>, 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<expr, constraint> 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);
}

111
src/frontends/lean/elaborator.cpp
View file

@ -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<expr> local_tactic_hints;
typedef rb_map<expr, pair<expr, constraint_seq>, 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<constraints> m_choices;
list<expr> m_coercions;
coercion_case_split(elaborator & elab, expr const & arg, list<constraints> const & choices, list<expr> 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<constraints> next() {
if (!m_choices)
return optional<constraints>();
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<constraints>(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>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(),
delay_factor+1)));
} else {
// giveup...
return lazy_list<constraints>(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<std::tuple<name, expr, expr>> alts;
get_user_coercions(env(), new_a_type, alts);
buffer<constraints> choices;
buffer<expr> 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<coercion_case_split>(*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<constraints>(cs.to_list());
}
};
return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, m_relax_main_opaque);
}
/** \brief Given a term <tt>a : a_type</tt>, and an expected type generate a metavariable with a delayed coercion. */
pair<expr, constraint_seq> 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<expr, constraint> 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 <tt>a : a_type</tt>, ensure it has type \c expected_type. Apply coercions if needed