From 05d1832425f2641d04ff338252274c56fb439490 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Jun 2014 22:32:53 -0700 Subject: [PATCH] refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs Signed-off-by: Leonardo de Moura --- src/frontends/lean/inductive_cmd.cpp | 4 +--- src/kernel/inductive/inductive.cpp | 4 ++-- src/kernel/type_checker.cpp | 4 ++-- src/kernel/type_checker.h | 15 ++++++++++++--- src/library/kernel_bindings.cpp | 14 ++++++++++++-- 5 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 677da32a79..538b01cd00 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -134,7 +134,7 @@ static void set_result_universes(buffer & decls, level_param_nam while (is_pi(t)) { if (i >= num_params) { try { - expr s = tc.ensure_sort(tc.infer(binding_domain(t))); + expr s = tc.ensure_type(binding_domain(t)); level lvl = sort_level(s); if (std::find(lvls.begin(), lvls.end(), lvl) == lvls.end()) lvls.push_back(lvl); @@ -339,5 +339,3 @@ void register_inductive_cmd(cmd_table & r) { add_cmd(r, cmd_info("inductive", "declare an inductive datatype", inductive_cmd)); } } - - diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 13ad57c4d7..8b687ba46d 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -375,7 +375,7 @@ struct add_inductive_fn { << "does not match inductive datatypes parameters'"); t = instantiate(binding_body(t), m_param_consts[i]); } else { - expr s = m_tc.ensure_sort(m_tc.infer(binding_domain(t))); + expr s = m_tc.ensure_type(binding_domain(t)); // the sort is ok IF // 1- its level is <= inductive datatype level, OR // 2- m_env is impredicative and inductive datatype is at level 0 @@ -454,7 +454,7 @@ struct add_inductive_fn { unsigned i = 0; while (is_pi(t)) { if (i >= m_num_params) { - expr s = m_tc.ensure_sort(m_tc.infer(binding_domain(t))); + expr s = m_tc.ensure_type(binding_domain(t)); if (!is_zero(sort_level(s))) return true; } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index f28baff1f0..d877b49464 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -422,8 +422,8 @@ expr type_checker::check(expr const & t, level_param_names const & ps) { return bool type_checker::is_def_eq(expr const & t, expr const & s) { return m_ptr->is_def_eq(t, s); } 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) { return m_ptr->ensure_pi(t, t); } -expr type_checker::ensure_sort(expr const & t) { return m_ptr->ensure_sort(t, t); } +expr type_checker::ensure_pi(expr const & t, expr const & s) { return m_ptr->ensure_pi(t, s); } +expr type_checker::ensure_sort(expr const & t, expr const & s) { return m_ptr->ensure_sort(t, s); } static void check_no_metavar(environment const & env, expr const & e) { if (has_metavar(e)) diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 74864057e1..a539c6ba5f 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -92,10 +92,19 @@ public: bool is_prop(expr const & t); /** \brief Return the weak head normal form of \c t. */ expr whnf(expr const & t); - /** \brief Return a Pi if \c t is convertible to a Pi type. Throw an exception otherwise. */ - expr ensure_pi(expr const & t); + /** \brief Return a Pi if \c t is convertible to a Pi type. Throw an exception otherwise. + The argument \c s is used when reporting errors */ + expr ensure_pi(expr const & t, expr const & s); + expr ensure_pi(expr const & t) { return ensure_pi(t, t); } + /** \brief Mare sure type of \c e is a Pi, and return it. Throw an exception otherwise. */ + expr ensure_fun(expr const & e) { return ensure_pi(infer(e), e); } + /** \brief Return a Sort if \c t is convertible to Sort. Throw an exception otherwise. + The argument \c s is used when reporting errors. */ + expr ensure_sort(expr const & t, expr const & s); /** \brief Return a Sort if \c t is convertible to Sort. Throw an exception otherwise. */ - expr ensure_sort(expr const & t); + expr ensure_sort(expr const & t) { return ensure_sort(t, t); } + /** \brief Mare sure type of \c e is a sort, and return it. Throw an exception otherwise. */ + expr ensure_type(expr const & e) { return ensure_sort(infer(e), e); } void swap(type_checker & tc) { std::swap(m_ptr, tc.m_ptr); } }; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index faeff45c23..195236291b 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1859,8 +1859,18 @@ int mk_type_checker(lua_State * L) { } } int type_checker_whnf(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->whnf(to_expr(L, 2))); } -int type_checker_ensure_pi(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->ensure_pi(to_expr(L, 2))); } -int type_checker_ensure_sort(lua_State * L) { return push_expr(L, to_type_checker_ref(L, 1)->ensure_sort(to_expr(L, 2))); } +int type_checker_ensure_pi(lua_State * L) { + if (lua_gettop(L) == 2) + return push_expr(L, to_type_checker_ref(L, 1)->ensure_pi(to_expr(L, 2))); + else + return push_expr(L, to_type_checker_ref(L, 1)->ensure_pi(to_expr(L, 2), to_expr(L, 3))); +} +int type_checker_ensure_sort(lua_State * L) { + if (lua_gettop(L) == 2) + return push_expr(L, to_type_checker_ref(L, 1)->ensure_sort(to_expr(L, 2))); + else + return push_expr(L, to_type_checker_ref(L, 1)->ensure_sort(to_expr(L, 2), to_expr(L, 3))); +} int type_checker_check(lua_State * L) { int nargs = lua_gettop(L); if (nargs <= 2)