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

refactor(kernel): expose may_reduce_later method

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 20:36:26 -08:00
parent b57f93bad5
commit fcd67649ed
6 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/converter.cpp
View file

@ -38,6 +38,7 @@ struct dummy_converter : public converter {
virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
virtual bool is_opaque(declaration const &) const { return false; }
virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
virtual bool may_reduce_later(expr const &, type_checker &) { return false; }
};
std::unique_ptr<converter> mk_dummy_converter() {

7
src/kernel/converter.h
View file

@ -18,11 +18,14 @@ protected:
extension_context & get_extension(type_checker & tc);
public:
virtual ~converter() {}
virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
virtual optional<module_idx> get_module_idx() const = 0;
virtual bool is_opaque(declaration const & d) const = 0;
virtual optional<declaration> is_delta(expr const & e) const = 0;
virtual bool may_reduce_later(expr const & e, type_checker & c) = 0;
virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
};

4
src/kernel/default_converter.cpp
View file

@ -51,6 +51,10 @@ bool default_converter::may_reduce_later(expr const & e) {
return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(*m_tc)));
}
bool default_converter::may_reduce_later(expr const & e, type_checker & c) {
return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(c)));
}
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
expr default_converter::whnf_core(expr const & e) {
check_system("whnf");

1
src/kernel/default_converter.h
View file

@ -77,6 +77,7 @@ public:
virtual bool is_opaque(declaration const & d) const;
virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
virtual bool may_reduce_later(expr const & e, type_checker & c);
virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);
virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst);
};

2
src/kernel/type_checker.h
View file

@ -215,6 +215,8 @@ public:
optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
bool may_reduce_later(expr const & e) { return m_conv->may_reduce_later(e, *this); }
template<typename F>
typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
flet<level_param_names const *> updt(m_params, &ps);

4
src/library/unifier.cpp
View file

@ -940,7 +940,9 @@ struct unifier_fn {
unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
add_meta_occ(lhs, cidx);
add_meta_occ(rhs, cidx);
} else if (m_plugin->delay_constraint(*m_tc[relax], c)) {
} else if (m_tc[relax]->may_reduce_later(lhs) ||
m_tc[relax]->may_reduce_later(rhs) ||
m_plugin->delay_constraint(*m_tc[relax], c)) {
unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
add_meta_occs(lhs, cidx);
add_meta_occs(rhs, cidx);