max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(kernel/inductive/inductive): kernel should reject inductive datatype declaration for I where I occurs in an index

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-10 17:43:18 -07:00
parent 932d14241b
commit 318c94bfce
4 changed files with 27 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -321,21 +321,6 @@ struct add_inductive_fn {
updt_type_checker();
}
/** \brief Return true iff \c t is a term of the form (I As t)
where I is the inductive datatype being defined, and As are the
global parameters of this declaration. */
bool is_valid_it_app(expr const & t) {
buffer<expr> args;
expr I = get_app_args(t, args);
if (!is_def_eq(I, m_it_const) || args.size() != m_it_num_args)
return false;
for (unsigned i = 0; i < m_decl.m_num_params; i++) {
if (m_param_consts[i] != args[i])
return false;
}
return true;
}
/** \brief Return true iff \c e is the inductive datatype being declared. */
bool is_it_occ(expr const & e) {
return is_constant(e) && const_name(e) == const_name(m_it_const);
@ -346,6 +331,26 @@ struct add_inductive_fn {
return (bool)find(t, [&](expr const & e, unsigned) { return is_it_occ(e); }); // NOLINT
}
/** \brief Return true iff \c t is a term of the form (I As t)
where I is the inductive datatype being defined, and As are the
global parameters of this declaration. Moreover I does not occur in t */
bool is_valid_it_app(expr const & t) {
buffer<expr> args;
expr I = get_app_args(t, args);
if (!is_def_eq(I, m_it_const) || args.size() != m_it_num_args)
return false;
unsigned i = 0;
for (; i < m_decl.m_num_params; i++) {
if (m_param_consts[i] != args[i])
return false;
}
for (; i < args.size(); i++) {
if (has_it_occ(args[i]))
return false;
}
return true;
}
/** \brief Return some(d_idx) iff \c t is a recursive argument, \c d_idx is the index of the recursive inductive datatype.
Return none otherwise. */
bool is_rec_argument(expr t) {

5
tests/lean/bad_index.lean Normal file
View file

@ -0,0 +1,5 @@
inductive foo1 : Type -> Type
| mk : foo1 (list (foo1 poly_unit)) -> foo1 (list (foo1 poly_unit))
inductive foo2 : Type -> Type
| mk : foo2 (foo2 poly_unit) -> foo2 (foo2 poly_unit)

2
tests/lean/bad_index.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
bad_index.lean:1:0: error: arg #1 of 'foo1.mk' contains a non valid occurrence of the datatypes being declared
bad_index.lean:4:0: error: arg #1 of 'foo2.mk' contains a non valid occurrence of the datatypes being declared

25
tests/lean/run/mutual_inductive.lean
View file

@ -174,28 +174,3 @@ check @bar.rec
check @rig.rec
end X9
namespace X10
mutual_inductive foo, bar, rig
with foo : Type -> Type
| mk : bar (foo poly_unit) -> foo (bar poly_unit)
with bar : Type -> Type
| mk : foo (bar poly_unit) -> bar (foo poly_unit)
with rig : Type -> Type
| mk : foo (bar (rig poly_unit)) -> rig (bar (foo poly_unit)) -> rig (bar (foo poly_unit))
check @foo
check @bar
check @rig
check @foo.rec
check @bar.rec
check @rig.rec
check @foo.has_sizeof_inst
check @bar.has_sizeof_inst
check @rig.has_sizeof_inst
check @foo.mk.sizeof_spec
check @bar.mk.sizeof_spec
check @rig.mk.sizeof_spec
end X10