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

refactor(kernel/type_checker): remove trace capability, we get it for free with tags

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-12 16:38:53 -07:00
parent 2593f65ce1
commit 3bc83fae56
3 changed files with 15 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/kernel/instantiate.cpp
View file

@ -11,8 +11,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
namespace lean { namespace lean {
template<typename P = default_replace_postprocessor> expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst) {
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, P const & p = P()) {
if (s >= get_free_var_range(a) || n == 0) if (s >= get_free_var_range(a) || n == 0)
return a; return a;
return replace(a, [=](expr const & m, unsigned offset) -> optional<expr> { return replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
@ -33,7 +32,7 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, P c
} }
} }
return none_expr(); return none_expr();
}, p); });
} }
expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, 0, n, s); } expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, 0, n, s); }
@ -41,14 +40,6 @@ expr instantiate(expr const & e, std::initializer_list<expr> const & l) { retur
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); } expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); } expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); }
expr instantiate(expr const & e, unsigned n, expr const * s, std::function<void(expr const & old_e, expr const & new_e)> const & new_eh) {
return instantiate(e, 0, n, s, new_eh);
}
expr instantiate(expr const & e, expr const & s, std::function<void(expr const & old_e, expr const & new_e)> const & new_eh) {
return instantiate(e, 1, &s, new_eh);
}
bool is_head_beta(expr const & t) { bool is_head_beta(expr const & t) {
expr const * it = &t; expr const * it = &t;
while (is_app(*it)) { while (is_app(*it)) {

11
src/kernel/instantiate.h
View file

@ -18,17 +18,6 @@ expr instantiate(expr const & e, unsigned i, expr const & s);
/** \brief Replace free variable \c 0 with \c s in \c e. */ /** \brief Replace free variable \c 0 with \c s in \c e. */
expr instantiate(expr const & e, expr const & s); expr instantiate(expr const & e, expr const & s);
/**
\brief Replace the free variables in \c e.
Whenever a new sub-expression is created in the process, the procedure \c new_eh is invoked.
*/
expr instantiate(expr const & e, unsigned n, expr const * s, std::function<void(expr const & old_e, expr const & new_e)> const & new_eh);
/**
\brief Replace free variable \c 0 with \c s in \c e.
Whenever a new sub-expression is created in the process, the procedure \c new_eh is invoked.
*/
expr instantiate(expr const & e, expr const & s, std::function<void(expr const & old_e, expr const & new_e)> const & new_eh);
expr apply_beta(expr f, unsigned num_args, expr const * args); expr apply_beta(expr f, unsigned num_args, expr const * args);
bool is_head_beta(expr const & t); bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t); expr head_beta_reduce(expr const & t);

52
src/kernel/type_checker.cpp
View file

@ -63,10 +63,6 @@ struct type_checker::imp {
expr_struct_map<expr> m_infer_type_cache; expr_struct_map<expr> m_infer_type_cache;
converter_context m_conv_ctx; converter_context m_conv_ctx;
type_checker_context m_tc_ctx; type_checker_context m_tc_ctx;
// The following mapping is used to store the relationship
// between temporary expressions created during type checking and the original ones.
// We need that to be able to produce error messages containing position information.
expr_map<expr> m_trace;
bool m_memoize; bool m_memoize;
// temp flag // temp flag
param_names m_params; param_names m_params;
@ -83,35 +79,13 @@ struct type_checker::imp {
return none_expr(); return none_expr();
} }
/** \brief Add entry <tt>new_e -> old_e</tt> in the traceability mapping */
void add_trace(expr const & old_e, expr const & new_e) {
if (!is_eqp(old_e, new_e))
m_trace.insert(mk_pair(new_e, old_e));
}
/** \brief Return the input (sub) expression that corresponds to the (temporary) expression \c e. */
expr trace_back(expr e) const {
while (true) {
auto it = m_trace.find(e);
if (it != m_trace.end())
e = it->second;
else
return e;
}
}
/** \brief Replace free variable \c 0 with \c s in \c e, and trace new sub-expressions created in the process. */
expr instantiate_with_trace(expr const & e, expr const & s) {
return lean::instantiate(e, s, [&](expr const & old_e, expr const & new_e) { add_trace(old_e, new_e); });
}
/** /**
\brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant. \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
It also returns the fresh local constant. It also returns the fresh local constant.
*/ */
std::pair<expr, expr> open_binder_body(expr const & e) { std::pair<expr, expr> open_binder_body(expr const & e) {
expr local = mk_local(m_gen.next() + binder_name(e), binder_domain(e)); expr local = mk_local(m_gen.next() + binder_name(e), binder_domain(e));
return mk_pair(instantiate_with_trace(binder_body(e), local), local); return mk_pair(instantiate(binder_body(e), local), local);
} }
/** \brief Add given constraint to the constraint handler m_chandler. */ /** \brief Add given constraint to the constraint handler m_chandler. */
@ -190,14 +164,14 @@ struct type_checker::imp {
return e; return e;
} else if (is_meta(e)) { } else if (is_meta(e)) {
expr r = mk_sort(mk_meta_univ(m_gen.next())); expr r = mk_sort(mk_meta_univ(m_gen.next()));
justification j = mk_justification(trace_back(s), justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_type_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s)); return pp_type_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
}); });
add_cnstr(mk_eq_cnstr(e, r, j)); add_cnstr(mk_eq_cnstr(e, r, j));
return r; return r;
} else { } else {
throw_kernel_exception(m_env, trace_back(s), throw_kernel_exception(m_env, s,
[=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, m_env, o, s); }); [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, m_env, o, s); });
} }
} }
@ -222,7 +196,7 @@ struct type_checker::imp {
} else if (is_meta(e)) { } else if (is_meta(e)) {
buffer<expr> telescope; buffer<expr> telescope;
if (!meta_to_telescope(e, telescope)) if (!meta_to_telescope(e, telescope))
throw_kernel_exception(m_env, trace_back(s), throw_kernel_exception(m_env, s,
[=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); }); [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); });
expr ta = mk_sort(mk_meta_univ(m_gen.next())); expr ta = mk_sort(mk_meta_univ(m_gen.next()));
expr A = mk_metavar(m_gen.next(), mk_tele_pi(telescope, ta)); expr A = mk_metavar(m_gen.next(), mk_tele_pi(telescope, ta));
@ -236,14 +210,14 @@ struct type_checker::imp {
args.push_back(Var(0)); args.push_back(Var(0));
expr B_args = mk_app(B, args.size(), args.data()); expr B_args = mk_app(B, args.size(), args.data());
expr r = mk_pi(g_x_name, A, B); expr r = mk_pi(g_x_name, A, B);
justification j = mk_justification(trace_back(s), justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s)); return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
}); });
add_cnstr(mk_eq_cnstr(e, r, j)); add_cnstr(mk_eq_cnstr(e, r, j));
return r; return r;
} else { } else {
throw_kernel_exception(m_env, trace_back(s), throw_kernel_exception(m_env, s,
[=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); }); [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); });
} }
} }
@ -251,7 +225,7 @@ struct type_checker::imp {
/** \brief Create a justification for the level constraint <tt>lhs <= rhs</tt> associated with constanc \c c. */ /** \brief Create a justification for the level constraint <tt>lhs <= rhs</tt> associated with constanc \c c. */
justification mk_lvl_cnstr_jst(expr const & c, level const & lhs, level const & rhs) { justification mk_lvl_cnstr_jst(expr const & c, level const & lhs, level const & rhs) {
lean_assert(is_constant(c)); lean_assert(is_constant(c));
return mk_justification(trace_back(c), return mk_justification(c,
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_def_lvl_cnstrs_satisfied(fmt, m_env, o, return pp_def_lvl_cnstrs_satisfied(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(c), subst.instantiate_metavars_wo_jst(c),
@ -266,7 +240,7 @@ struct type_checker::imp {
*/ */
justification mk_app_mismatch_jst(expr const & e, expr const & fn_type, expr const & arg_type) { justification mk_app_mismatch_jst(expr const & e, expr const & fn_type, expr const & arg_type) {
lean_assert(is_app(e)); lean_assert(is_app(e));
return mk_justification(trace_back(e), return mk_justification(e,
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_app_type_mismatch(fmt, m_env, o, return pp_app_type_mismatch(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(e), subst.instantiate_metavars_wo_jst(e),
@ -281,7 +255,7 @@ struct type_checker::imp {
*/ */
justification mk_let_mismatch_jst(expr const & e, expr const & val_type) { justification mk_let_mismatch_jst(expr const & e, expr const & val_type) {
lean_assert(is_let(e)); lean_assert(is_let(e));
return mk_justification(trace_back(e), return mk_justification(e,
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_def_type_mismatch(fmt, m_env, o, let_name(e), return pp_def_type_mismatch(fmt, m_env, o, let_name(e),
subst.instantiate_metavars_wo_jst(let_type(e)), subst.instantiate_metavars_wo_jst(let_type(e)),
@ -292,7 +266,7 @@ struct type_checker::imp {
static constexpr char const * g_macro_error_msg = "failed to type check macro expansion"; static constexpr char const * g_macro_error_msg = "failed to type check macro expansion";
justification mk_macro_jst(expr const & e) { justification mk_macro_jst(expr const & e) {
return mk_justification(trace_back(e), return mk_justification(e,
[=](formatter const &, options const &, substitution const &) { [=](formatter const &, options const &, substitution const &) {
return format(g_macro_error_msg); return format(g_macro_error_msg);
}); });
@ -387,7 +361,7 @@ struct type_checker::imp {
expr a_type = infer_type_core(app_arg(e), infer_only); expr a_type = infer_type_core(app_arg(e), infer_only);
delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); }); delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); });
if (!is_def_eq(a_type, binder_domain(f_type), jst)) { if (!is_def_eq(a_type, binder_domain(f_type), jst)) {
throw_kernel_exception(m_env, trace_back(e), throw_kernel_exception(m_env, e,
[=](formatter const & fmt, options const & o) { [=](formatter const & fmt, options const & o) {
return pp_app_type_mismatch(fmt, m_env, o, e, binder_domain(f_type), a_type); return pp_app_type_mismatch(fmt, m_env, o, e, binder_domain(f_type), a_type);
}); });
@ -402,13 +376,13 @@ struct type_checker::imp {
expr val_type = infer_type_core(let_value(e), infer_only); expr val_type = infer_type_core(let_value(e), infer_only);
delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); }); delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); });
if (!is_def_eq(val_type, let_type(e), jst)) { if (!is_def_eq(val_type, let_type(e), jst)) {
throw_kernel_exception(m_env, trace_back(e), throw_kernel_exception(m_env, e,
[=](formatter const & fmt, options const & o) { [=](formatter const & fmt, options const & o) {
return pp_def_type_mismatch(fmt, m_env, o, let_name(e), let_type(e), val_type); return pp_def_type_mismatch(fmt, m_env, o, let_name(e), let_type(e), val_type);
}); });
} }
} }
r = infer_type_core(instantiate_with_trace(let_body(e), let_value(e)), infer_only); r = infer_type_core(instantiate(let_body(e), let_value(e)), infer_only);
break; break;
} }