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

feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-27 17:47:03 -08:00
parent 160dc71cb5
commit 55fde28954
2 changed files with 21 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/kernel/type_checker.cpp
View file

@ -398,18 +398,18 @@ public:
return infer_check(e, ctx, menv, uc, false); return infer_check(e, ctx, menv, uc, false);
} }
bool is_convertible(expr const & t1, expr const & t2, context const & ctx) { bool is_convertible(expr const & t1, expr const & t2, context const & ctx, optional<metavar_env> const & menv) {
set_ctx(ctx); set_ctx(ctx);
update_menv(none_menv()); update_menv(menv);
auto mk_justification = [](){ auto mk_justification = [](){
lean_unreachable(); return justification(); // LCOV_EXCL_LINE lean_unreachable(); return justification(); // LCOV_EXCL_LINE
}; };
return is_convertible(t1, t2, ctx, mk_justification); return is_convertible(t1, t2, ctx, mk_justification);
} }
bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) { bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional<metavar_env> const & menv) {
set_ctx(ctx); set_ctx(ctx);
update_menv(none_menv()); update_menv(menv);
if (t1 == t2) if (t1 == t2)
return true; return true;
expr new_t1 = normalize(t1, ctx, false); expr new_t1 = normalize(t1, ctx, false);
@ -445,9 +445,9 @@ public:
return is_bool(normalize(t, ctx, true)); return is_bool(normalize(t, ctx, true));
} }
expr ensure_pi(expr const & e, context const & ctx) { expr ensure_pi(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
set_ctx(ctx); set_ctx(ctx);
update_menv(none_menv()); update_menv(menv);
try { try {
return check_pi(e, expr(), ctx); return check_pi(e, expr(), ctx);
} catch (exception &) { } catch (exception &) {
@ -502,17 +502,26 @@ expr type_checker::check(expr const & e, context const & ctx, ro_metavar_env con
expr type_checker::check(expr const & e, context const & ctx) { expr type_checker::check(expr const & e, context const & ctx) {
return check(e, ctx, none_menv(), nullptr); return check(e, ctx, none_menv(), nullptr);
} }
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, optional<ro_metavar_env> const & menv) {
return m_ptr->is_convertible(t1, t2, ctx, ro_metavar_env::to_rw(menv));
}
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
return m_ptr->is_convertible(t1, t2, ctx); return m_ptr->is_convertible(t1, t2, ctx, none_menv());
}
bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional<ro_metavar_env> const & menv) {
return m_ptr->is_definitionally_equal(t1, t2, ctx, ro_metavar_env::to_rw(menv));
} }
bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) { bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) {
return m_ptr->is_definitionally_equal(t1, t2, ctx); return m_ptr->is_definitionally_equal(t1, t2, ctx, none_menv());
} }
void type_checker::check_type(expr const & e, context const & ctx) { void type_checker::check_type(expr const & e, context const & ctx) {
m_ptr->check_type(e, ctx); m_ptr->check_type(e, ctx);
} }
expr type_checker::ensure_pi(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
return m_ptr->ensure_pi(e, ctx, ro_metavar_env::to_rw(menv));
}
expr type_checker::ensure_pi(expr const & e, context const & ctx) { expr type_checker::ensure_pi(expr const & e, context const & ctx) {
return m_ptr->ensure_pi(e, ctx); return m_ptr->ensure_pi(e, ctx, none_menv());
} }
bool type_checker::is_proposition(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) { bool type_checker::is_proposition(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv)); return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv));

3
src/kernel/type_checker.h
View file

@ -85,12 +85,14 @@ public:
void check_type(expr const & e, context const & ctx = context()); void check_type(expr const & e, context const & ctx = context());
/** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx. */ /** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx. */
bool is_convertible(expr const & t1, expr const & t2, context const & ctx, optional<ro_metavar_env> const & menv);
bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context()); bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
/** \brief Return true iff \c t1 definitionally equal to \c t2 in the context \c ctx. /** \brief Return true iff \c t1 definitionally equal to \c t2 in the context \c ctx.
\remark is_definitionally_equal(t1, t2, ctx) implies is_convertible(t1, t2, ctx) \remark is_definitionally_equal(t1, t2, ctx) implies is_convertible(t1, t2, ctx)
*/ */
bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional<ro_metavar_env> const & menv);
bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx = context()); bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx = context());
/** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */ /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */
@ -104,6 +106,7 @@ public:
bool is_flex_proposition(expr const & e, context const & ctx = context()); bool is_flex_proposition(expr const & e, context const & ctx = context());
/** \brief Return a Pi if \c e is convertible to Pi. Throw an exception otherwise. */ /** \brief Return a Pi if \c e is convertible to Pi. Throw an exception otherwise. */
expr ensure_pi(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
expr ensure_pi(expr const & e, context const & ctx = context()); expr ensure_pi(expr const & e, context const & ctx = context());
/** \brief Reset internal caches */ /** \brief Reset internal caches */