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

fix(frontends/lean/structure_cmd): universe level validation

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-04 22:19:23 -08:00
parent 588ad210a2
commit 5b87d060cf
3 changed files with 32 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/structure_cmd.cpp
View file

@ -201,6 +201,10 @@ struct structure_cmd_fn {
}
}
void throw_explicit_universe(pos_info const & pos) {
throw parser_error("invalid 'structure', the resultant universe must be provided when explicit universe levels are being used", pos);
}
/** \brief Parse resultant universe */
void parse_result_type() {
auto pos = m_p.pos();
@ -209,7 +213,14 @@ struct structure_cmd_fn {
m_type = m_p.parse_expr();
if (!is_sort(m_type))
throw parser_error("invalid 'structure', 'Type' expected", pos);
if (has_placeholder(m_type))
throw_explicit_universe(pos);
level l = sort_level(m_type);
if (m_env.impredicative() && !is_not_zero(l))
throw parser_error("invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment", pos);
} else {
if (!m_infer_result_universe)
throw_explicit_universe(pos);
m_type = m_p.save_pos(mk_sort(mk_level_placeholder()), pos);
}
}

11
tests/lean/bad_structures.lean Normal file
View file

@ -0,0 +1,11 @@
structure prod.{l} (A : Type.{l}) (B : Type.{l}) :=
(pr1 : A) (pr2 : B)
structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type :=
(pr1 : A) (pr2 : B)
structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{l} :=
(pr1 : A) (pr2 : B)
structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} :=
(pr1 : A) (pr2 : B)

10
tests/lean/bad_structures.lean.expected.out Normal file
View file

@ -0,0 +1,10 @@
bad_structures.lean:1:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment
generated type
proj_type: Pi {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), A
proj_val: fun {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), (prod.rec.{l l} A B (fun (c : prod.{l} A B), A) (fun (pr1 : A) (pr2 : B), pr1) c)
proj_type: Pi {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), B
proj_val: fun {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), (prod.rec.{l l} A B (fun (c : prod.{l} A B), B) (fun (pr1 : A) (pr2 : B), pr2) c)
generated projs
generated auxiliary