diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 2e35fb8df..4545c34ae 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -121,7 +121,7 @@ struct add_inductive_fn { // or is never zero (under any parameter assignment). if (!is_zero(sort_level(t)) && !is_not_zero(sort_level(t))) throw kernel_exception(m_env, - "the resultant universe must be 0 or different" + "the resultant universe must be 0 or different " "from zero for all parameter/global level assignments"); if (first) { to_prop = is_zero(sort_level(t)); @@ -194,13 +194,13 @@ struct add_inductive_fn { return false; // nonrecursive argument } else if (is_pi(t)) { if (has_it_occ(binding_domain(t))) - throw kernel_exception(m_env, sstream() << "arg #" << arg_idx << " of '" << intro_name << "' " + throw kernel_exception(m_env, sstream() << "arg #" << (arg_idx + 1) << " of '" << intro_name << "' " "has a non positive occurrence of the datatypes being declared"); return check_positivity(instantiate(binding_body(t), mk_local_for(t)), intro_name, arg_idx); } else if (is_valid_it_app(t)) { return true; // recursive argument } else { - throw kernel_exception(m_env, sstream() << "arg #" << arg_idx << " of '" << intro_name << "' " + throw kernel_exception(m_env, sstream() << "arg #" << (arg_idx + 1) << " of '" << intro_name << "' " "contain a non valid occurrence of the datatypes being declared"); } } @@ -219,7 +219,7 @@ struct add_inductive_fn { while (is_pi(t)) { if (i < m_num_params) { if (!m_tc.is_def_eq(binding_domain(t), m_param_types[i])) - throw kernel_exception(m_env, sstream() << "arg #" << i << " of '" << n << "' " + throw kernel_exception(m_env, sstream() << "arg #" << (i + 1) << " of '" << n << "' " << "does not match inductive datatypes parameters'"); t = instantiate(binding_body(t), m_param_consts[i]); } else { @@ -228,11 +228,11 @@ struct add_inductive_fn { // 1- its level is <= inductive datatype level, OR // 2- m_env is impredicative and inductive datatype is at level 0 if (!(is_geq(m_it_levels[d_idx], sort_level(s)) || (is_zero(m_it_levels[d_idx]) && m_env.impredicative()))) - throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << i << ") " + throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") " << "of '" << n << "' is too big for the corresponding inductive datatype"); bool is_rec = check_positivity(binding_domain(t), n, i); if (found_rec && !is_rec) - throw kernel_exception(m_env, sstream() << "arg #" << i << " of '" << n << "' " + throw kernel_exception(m_env, sstream() << "arg #" << (i + 1) << " of '" << n << "' " << "is not recursive, but it occurs after recursive arguments"); if (is_rec) found_rec = true; @@ -241,8 +241,8 @@ struct add_inductive_fn { } else { t = binding_body(t); if (!closed(t)) - throw kernel_exception(m_env, sstream() << "invalid occurrence of recursive arg#" << i << - " of '" << n << "' the body of the functional type depends on it."); + throw kernel_exception(m_env, sstream() << "invalid occurrence of recursive arg#" << (i+1) << + " of '" << n << "', the body of the functional type depends on it."); } } i++; diff --git a/tests/lua/ind2.lua b/tests/lua/ind2.lua new file mode 100644 index 000000000..47b556f89 --- /dev/null +++ b/tests/lua/ind2.lua @@ -0,0 +1,103 @@ +local env = empty_environment() + +function bad_add_inductive(...) + arg = {...} + ok, msg = pcall(function() add_inductive(unpack(arg)) end) + assert(not ok) + print("\nExpected error: " .. msg:what()) +end + +local l = mk_param_univ("l") +local A = Const("A") +local U_l = mk_sort(l) +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local list_l = Const("list", {l}) -- list.{l} +local Nat = Const("nat") +local vec_l = Const("vec", {l}) -- vec.{l} +local zero = Const("zero") +local succ = Const("succ") +local forest_l = Const("forest", {l}) +local tree_l = Const("tree", {l}) +local n = Const("n") + +bad_add_inductive(env, + "nat", Type, + "zero", Bool, -- Incorrect result type + "succ", mk_arrow(Nat, Nat)) + +bad_add_inductive(env, {l}, 1, + {"tree", mk_arrow(U_l, U_l1), + "node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A))) + }, + {"forest", mk_arrow(U_l1, U_l1), -- Parameters of all inductive types must match + "emptyf", Pi({{A, U_l, true}}, forest_l(A)), + "consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))}) + +bad_add_inductive(env, {l}, 1, + {"tree", mk_arrow(U_l, U_l), -- Result may be in universe zero (e.g., l is instantiated with zero) + "node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A))) + }, + {"forest", mk_arrow(U_l, U_l1), + "emptyf", Pi({{A, U_l, true}}, forest_l(A)), + "consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))}) + +bad_add_inductive(env, + "nat", 1, Type, -- mismatch in the number of arguments claimed + "zero", Nat, + "succ", mk_arrow(Nat, Nat)) + +env = add_inductive(env, + "nat", Type, + "zero", Nat, + "succ", mk_arrow(Nat, Nat)) + +local Even = Const("Even") +local Odd = Const("Odd") +local b = Const("b") +bad_add_inductive(env, {}, + {"Even", mk_arrow(Nat, Type), + "zero_is_even", Even(zero), + "succ_odd", Pi(b, Nat, mk_arrow(Odd(b), Even(succ(b))))}, + {"Odd", mk_arrow(Nat, Bool), -- if one datatype lives in Bool/Prop, then all must live in Bool/Prop + "succ_even", Pi(b, Nat, mk_arrow(Even(b), Odd(succ(b))))}) + +bad_add_inductive(env, + "list", {l}, 1, mk_arrow(U_l, U_l1), + "nil", Pi({{A, U_l, true}}, mk_arrow(mk_arrow(list_l(A), Bool), list_l(A))), -- nonpositive occurrence of inductive datatype + "cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A)))) + +bad_add_inductive(env, + "list", {l}, 1, mk_arrow(U_l, U_l1), + "nil", Pi({{A, U_l, true}}, list_l(mk_arrow(A, A))), + "cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A)))) + +local list_1 = Const("list", {mk_level_one()}) + +bad_add_inductive(env, + "list", {l}, 1, mk_arrow(U_l, U_l1), + "nil", Pi({{A, U_l, true}}, list_l(A)), + "cons", Pi({{A, U_l, true}}, mk_arrow(A, list_1(Nat), list_l(A)))) -- all list occurrences must be of the form list_l(A) + +bad_add_inductive(env, + "list", {l}, 1, mk_arrow(U_l, U_l1), + "nil", Pi({{A, U_l, true}}, list_l(A)), + "cons", Pi({{A, Type, true}}, mk_arrow(A, list_1(A), list_1(A)))) + +bad_add_inductive(env, + "list", {l}, 1, mk_arrow(U_l, U_l1), + "nil", Pi({{A, U_l, true}}, mk_arrow(U_l, list_l(A))), + "cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A)))) + +bad_add_inductive(env, + "list", {l}, 1, mk_arrow(U_l, U_l1), + "nil", Pi({{A, U_l, true}}, list_l(A)), + "cons", Pi({{A, U_l, true}}, mk_arrow(list_l(A), A, list_l(A)))) + +env = add_decl(env, mk_var_decl("eq", Pi(A, Type, mk_arrow(A, A, Bool)))) +local eq = Const("eq") +local Nat2 = Const("nat2") +local a = Const("a") +bad_add_inductive(env, + "nat2", Type, + "zero2", Nat2, + "succ2", Pi(a, Nat2, mk_arrow(eq(Nat2, a, a), Nat2)))