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

refactor(kernel): move is_stuck predicate to converter

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-22 11:37:14 -07:00
parent 5687c24944
commit 76477aedd1
6 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/converter.cpp
View file

@ -26,7 +26,6 @@ pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const &
extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); } extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
/** \brief Do nothing converter */ /** \brief Do nothing converter */
struct dummy_converter : public converter { struct dummy_converter : public converter {
virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker &) { virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker &) {
@ -37,7 +36,7 @@ struct dummy_converter : public converter {
} }
virtual bool is_opaque(declaration const &) const { return false; } virtual bool is_opaque(declaration const &) const { return false; }
virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); } virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
virtual bool is_stuck(expr const &, type_checker &) { return false; } virtual optional<expr> is_stuck(expr const &, type_checker &) { return none_expr(); }
}; };
std::unique_ptr<converter> mk_dummy_converter() { std::unique_ptr<converter> mk_dummy_converter() {

2
src/kernel/converter.h
View file

@ -21,7 +21,7 @@ public:
virtual bool is_opaque(declaration const & d) const = 0; virtual bool is_opaque(declaration const & d) const = 0;
virtual optional<declaration> is_delta(expr const & e) const = 0; virtual optional<declaration> is_delta(expr const & e) const = 0;
virtual bool is_stuck(expr const & e, type_checker & c) = 0; virtual optional<expr> is_stuck(expr const & e, type_checker & c) = 0;
virtual pair<expr, constraint_seq> whnf(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; virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;

8
src/kernel/default_converter.cpp
View file

@ -50,8 +50,12 @@ bool default_converter::is_stuck(expr const & e) {
return static_cast<bool>(m_env.norm_ext().is_stuck(e, get_extension(*m_tc))); return static_cast<bool>(m_env.norm_ext().is_stuck(e, get_extension(*m_tc)));
} }
bool default_converter::is_stuck(expr const & e, type_checker & c) { optional<expr> default_converter::is_stuck(expr const & e, type_checker & c) {
return static_cast<bool>(m_env.norm_ext().is_stuck(e, get_extension(c))); if (is_meta(e)) {
return some_expr(e);
} else {
return m_env.norm_ext().is_stuck(e, get_extension(c));
}
} }
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */

2
src/kernel/default_converter.h
View file

@ -90,7 +90,7 @@ public:
virtual optional<declaration> is_delta(expr const & e) const; virtual optional<declaration> is_delta(expr const & e) const;
virtual bool is_opaque(declaration const & d) const; virtual bool is_opaque(declaration const & d) const;
virtual bool is_stuck(expr const & e, type_checker & c); virtual optional<expr> is_stuck(expr const & e, type_checker & c);
virtual pair<expr, constraint_seq> whnf(expr const & e_prime, 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); virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst);
}; };

6
src/kernel/type_checker.cpp
View file

@ -436,11 +436,7 @@ type_checker::type_checker(environment const & env):
type_checker::~type_checker() {} type_checker::~type_checker() {}
optional<expr> type_checker::is_stuck(expr const & e) { optional<expr> type_checker::is_stuck(expr const & e) {
if (is_meta(e)) { return m_conv->is_stuck(e, *this);
return some_expr(e);
} else {
return m_env.norm_ext().is_stuck(e, m_tc_ctx);
}
} }
void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) { void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {

2
src/kernel/type_checker.h
View file

@ -224,7 +224,7 @@ public:
optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); } optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
bool may_reduce_later(expr const & e) { return m_conv->is_stuck(e, *this); } bool may_reduce_later(expr const & e) { return !is_meta(e) && static_cast<bool>(m_conv->is_stuck(e, *this)); }
template<typename F> template<typename F>
typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) { typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {