test(lua): add tests for exercising datatype validation code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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 <<
+                        throw kernel_exception(m_env, sstream() << "invalid occurrence of recursive arg#" << (i+1) <<
-                                               " of '" << n << "' the body of the functional type depends on it.");
+                                               " of '" << n << "', the body of the functional type depends on it.");
                 }
             }
             i++;

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