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

refactor(frontends/lean/coercion_elaborator): simplify

Browse source 
coercion_elaborator interface
This commit is contained in:
Leonardo de Moura 2014-09-25 08:48:31 -07:00
parent a61b95a87e
commit fce1113b80
3 changed files with 13 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/coercion_elaborator.cpp
View file

@ -54,6 +54,8 @@ optional<constraints> coercion_elaborator::next() {
return optional<constraints>(r); return optional<constraints>(r);
} }
/** \brief Given a term <tt>a : a_type</tt>, and a metavariable \c m, creates a constraint
that considers coercions from a_type to the type assigned to \c m. */
constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom, constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
expr const & m, expr const & a, expr const & a_type, expr const & m, expr const & a, expr const & a_type,
justification const & j, unsigned delay_factor, bool relax) { justification const & j, unsigned delay_factor, bool relax) {
@ -126,12 +128,4 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
}; };
return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax); 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));
}
} }

22
src/frontends/lean/coercion_elaborator.h
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/type_checker.h" #include "kernel/type_checker.h"
#include "frontends/lean/local_context.h"
namespace lean { namespace lean {
/** \brief Abstract class for hiding details of the info_manager from the coercion_elaborator */ /** \brief Abstract class for hiding details of the info_manager from the coercion_elaborator */
@ -30,27 +29,22 @@ public:
optional<constraints> next(); optional<constraints> next();
}; };
/** \brief Create a metavariable, and attach choice constraint for generating /** \brief Given a term <tt>a : a_type</tt>, and a metavariable \c m, creates a constraint
coercions of the form <tt>f a</tt>, where \c f is registered coercion, that considers coercions from a_type to the type assigned to \c m.
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 This function is used when the types \c a_type and/or the type of \c m
are not known at preprocessing time, and a choice function is used to are not known at preprocessing time, and a choice function is used to
enumerate coercion functions \c f. enumerate coercion functions \c f. By "not known", we mean the type is a
metavariable application.
\param relax True if opaque constants in the current module should be treated \param relax True if opaque constants in the current module should be treated
as transparent as transparent
\see coercion_info_manager \see coercion_info_manager
*/ */
pair<expr, constraint> mk_coercion_elaborator( constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
type_checker & tc, coercion_info_manager & infom, local_context & ctx, bool relax, expr const & m, expr const & a, expr const & a_type,
expr const & a, expr const & a_type, expr const & expected_type, justification const & j); justification const & j, unsigned delay_factor, bool relax);
pair<expr, constraint> coercions_to_choice(coercion_info_manager & infom, local_context & ctx,
list<expr> const & coes, expr const & a,
justification const & j, bool relax);
list<expr> get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs); list<expr> get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs);
} }

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

@ -479,9 +479,9 @@ public:
justification const & j) { justification const & j) {
bool relax = m_relax_main_opaque; bool relax = m_relax_main_opaque;
type_checker & tc = *m_tc[relax]; type_checker & tc = *m_tc[relax];
pair<expr, constraint> ec = mk_coercion_elaborator(tc, *this, m_full_context, relax, expr m = m_full_context.mk_meta(some_expr(expected_type), a.get_tag());
a, a_type, expected_type, j); constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), relax);
return to_ecs(ec.first, ec.second); return to_ecs(m, c);
} }
/** \brief Given a term <tt>a : a_type</tt>, ensure it has type \c expected_type. Apply coercions if needed /** \brief Given a term <tt>a : a_type</tt>, ensure it has type \c expected_type. Apply coercions if needed