From 55fde289546c71ab3225e1116303b6a4edab0be6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jan 2014 17:47:03 -0800 Subject: [PATCH] feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 27 ++++++++++++++++++--------- src/kernel/type_checker.h | 3 +++ 2 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 6ae10f17f..666fb2b9f 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -398,18 +398,18 @@ public: 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 const & menv) { set_ctx(ctx); - update_menv(none_menv()); + update_menv(menv); auto mk_justification = [](){ lean_unreachable(); return justification(); // LCOV_EXCL_LINE }; 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 const & menv) { set_ctx(ctx); - update_menv(none_menv()); + update_menv(menv); if (t1 == t2) return true; expr new_t1 = normalize(t1, ctx, false); @@ -445,9 +445,9 @@ public: 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 const & menv) { set_ctx(ctx); - update_menv(none_menv()); + update_menv(menv); try { return check_pi(e, expr(), ctx); } 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) { return check(e, ctx, none_menv(), nullptr); } +bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, optional 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) { - 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 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) { - 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) { m_ptr->check_type(e, ctx); } +expr type_checker::ensure_pi(expr const & e, context const & ctx, optional 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) { - 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 const & menv) { return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv)); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 8280580be..f89b03272 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -85,12 +85,14 @@ public: 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. */ + bool is_convertible(expr const & t1, expr const & t2, context const & ctx, optional const & menv); 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. \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 const & menv); 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) */ @@ -104,6 +106,7 @@ public: 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. */ + expr ensure_pi(expr const & e, context const & ctx, optional const & menv); expr ensure_pi(expr const & e, context const & ctx = context()); /** \brief Reset internal caches */