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

refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-19 22:32:53 -07:00
parent 0cc8117fb4
commit 05d1832425
5 changed files with 29 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/inductive_cmd.cpp
View file

@ -134,7 +134,7 @@ static void set_result_universes(buffer<inductive_decl> & 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));
}
}

4
src/kernel/inductive/inductive.cpp
View file

@ -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;
}

4
src/kernel/type_checker.cpp
View file

@ -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))

15
src/kernel/type_checker.h
View file

@ -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); }
};

14
src/library/kernel_bindings.cpp
View file

@ -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)