feat(kernel/type_checker): add type_checker::is_def_eq method that takes a justification as argument

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-21 19:45:20 -07:00
parent fedbf8595b
commit f9a21166f0
3 changed files with 13 additions and 0 deletions

View file

@ -161,4 +161,11 @@ public:
template<typename Mk> simple_delayed_justification(Mk && mk):m_mk(mk) {}
virtual justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
};
class as_delayed_justification : public delayed_justification {
justification m_jst;
public:
as_delayed_justification(justification const & j):m_jst(j) {}
virtual justification get() { return m_jst; }
};
}

View file

@ -400,6 +400,10 @@ struct type_checker::imp {
return infer_type_core(e, false);
}
bool is_def_eq(expr const & t, expr const & s) { return m_conv->is_def_eq(t, s, m_conv_ctx); }
bool is_def_eq(expr const & t, expr const & s, justification const & j) {
as_delayed_justification djst(j);
return is_def_eq(t, s, djst);
}
expr whnf(expr const & t) { return m_conv->whnf(t, m_conv_ctx); }
};
@ -421,6 +425,7 @@ type_checker::~type_checker() {}
expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); }
expr type_checker::check(expr const & t, level_param_names const & ps) { return m_ptr->check(t, ps); }
bool type_checker::is_def_eq(expr const & t, expr const & s) { return m_ptr->is_def_eq(t, s); }
bool type_checker::is_def_eq(expr const & t, expr const & s, justification const & j) { return m_ptr->is_def_eq(t, s, j); }
bool type_checker::is_prop(expr const & t) { return m_ptr->is_prop(t); }
expr type_checker::whnf(expr const & t) { return m_ptr->whnf(t); }
expr type_checker::ensure_pi(expr const & t, expr const & s) { return m_ptr->ensure_pi(t, s); }

View file

@ -81,6 +81,7 @@ public:
expr check(expr const & t, level_param_names const & ps = level_param_names());
/** \brief Return true iff t is definitionally equal to s. */
bool is_def_eq(expr const & t, expr const & s);
bool is_def_eq(expr const & t, expr const & s, justification const & j);
/** \brief Return true iff t is a proposition. */
bool is_prop(expr const & t);
/** \brief Return the weak head normal form of \c t. */