feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes

The new test contains examples that required explicit levels.
This commit is contained in:
Leonardo de Moura 2014-11-12 09:11:19 -08:00
parent ef5a3e83ad
commit 5312afa7ec
3 changed files with 68 additions and 9 deletions

View file

@ -447,21 +447,47 @@ struct inductive_cmd_fn {
} }
} }
/* \brief Add \c lvl to \c r_lvls (if it is not already there.
\pre lvl does not contain m_u.
*/
void accumulate_level(level const & lvl, buffer<level> & r_lvls) {
if (occurs(m_u, lvl)) {
throw exception("failed to infer inductive datatype resultant universe, "
"provide the universe levels explicitly");
} else if (std::find(r_lvls.begin(), r_lvls.end(), lvl) == r_lvls.end()) {
r_lvls.push_back(lvl);
}
}
/** \bried Accumulate the universe levels occurring in an introduction rule argument universe.
In general, the argument of an introduction rule has type
Pi (a_1 : A_1) (a_2 : A_1[a_1]) ..., B[a_1, a_2, ...]
The universe associated with it will be
imax(l_1, imax(l_2, ..., r))
where l_1 is the unvierse of A_1, l_2 of A_2, and r of B[a_1, ..., a_n].
The result placeholder m_u must only appear as r.
*/
void accumulate_levels(level const & lvl, buffer<level> & r_lvls) {
if (lvl == m_u) {
// ignore this is the auxiliary lvl
} else if (is_imax(lvl)) {
level lhs = imax_lhs(lvl);
level rhs = imax_rhs(lvl);
accumulate_level(lhs, r_lvls);
accumulate_levels(rhs, r_lvls);
} else {
accumulate_level(lvl, r_lvls);
}
}
/** \brief Traverse the introduction rule type and collect the universes where arguments reside in \c r_lvls. /** \brief Traverse the introduction rule type and collect the universes where arguments reside in \c r_lvls.
This information is used to compute the resultant universe level for the inductive datatype declaration. This information is used to compute the resultant universe level for the inductive datatype declaration.
*/ */
void accumulate_levels(expr intro_type, buffer<level> & r_lvls) { void accumulate_levels(expr intro_type, buffer<level> & r_lvls) {
while (is_pi(intro_type)) { while (is_pi(intro_type)) {
expr s = m_tc->ensure_type(binding_domain(intro_type)).first; expr s = m_tc->ensure_type(binding_domain(intro_type)).first;
level l = sort_level(s); accumulate_levels(sort_level(s), r_lvls);
if (l == m_u) {
// ignore, this is the auxiliary level
} else if (occurs(m_u, l)) {
throw exception("failed to infer inductive datatype resultant universe, "
"provide the universe levels explicitly");
} else if (std::find(r_lvls.begin(), r_lvls.end(), l) == r_lvls.end()) {
r_lvls.push_back(l);
}
intro_type = instantiate(binding_body(intro_type), mk_local_for(intro_type)); intro_type = instantiate(binding_body(intro_type), mk_local_for(intro_type));
} }
} }

31
tests/lean/ftree.lean Normal file
View file

@ -0,0 +1,31 @@
import data.list
namespace explicit
inductive ftree.{l₁ l₂} (A : Type.{l₁}) (B : Type.{l₂}) : Type.{max 1 l₁ l₂} :=
leafa : A → ftree A B,
leafb : B → ftree A B,
node : (A → ftree A B) → (B → ftree A B) → ftree A B
end explicit
namespace implicit
inductive ftree (A : Type) (B : Type) : Type :=
leafa : ftree A B,
node : (A → B → ftree A B) → (B → ftree A B) → ftree A B
set_option pp.universes true
check ftree
end implicit
namespace implicit2
inductive ftree (A : Type) (B : Type) : Type :=
leafa : A → ftree A B,
leafb : B → ftree A B,
node : (list A → ftree A B) → (B → ftree A B) → ftree A B
check ftree
end implicit2

View file

@ -0,0 +1,2 @@
ftree.{l_1 l_2} : Type.{l_1} → Type.{l_2} → Type.{max 1 l_1 l_2}
ftree.{l_1 l_2} : Type.{l_1} → Type.{l_2} → Type.{max 1 l_1 l_2}