From 30571ce4185ed189333930aff53f597bed1fd242 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Oct 2014 13:37:30 -0700 Subject: [PATCH] fix(library/definitional/projection): error messages for projection generation --- src/library/definitional/projection.cpp | 27 ++++++++++++++++--------- tests/lean/proj.lean | 25 +++++++++++++++++++++++ tests/lean/proj.lean.expected.out | 8 ++++++++ 3 files changed, 51 insertions(+), 9 deletions(-) create mode 100644 tests/lean/proj.lean create mode 100644 tests/lean/proj.lean.expected.out diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index c4dfccb4f..df5de6d64 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -14,30 +14,37 @@ Author: Leonardo de Moura namespace lean { [[ noreturn ]] static void throw_ill_formed(name const & n) { - throw exception(sstream() << "error in 'projection' generation, '" << n << "' is an ill-formed inductive datatype"); + throw exception(sstream() << "error in projection generation, '" << n << "' is an ill-formed inductive datatype"); } static pair get_nparam_intro_rule(environment const & env, name const & n) { optional decls = inductive::is_inductive_decl(env, n); if (!decls) - throw exception(sstream() << "error in 'projection' generation, '" << n << "' is not an inductive datatype"); + throw exception(sstream() << "error in projection generation, '" << n << "' is not an inductive datatype"); + optional num_indices = inductive::get_num_indices(env, n); + if (num_indices && *num_indices > 0) + throw exception(sstream() << "error in projection generation, '" + << n << "' is an indexed inductive datatype family"); unsigned num_params = std::get<1>(*decls); for (auto const & decl : std::get<2>(*decls)) { if (inductive::inductive_decl_name(decl) == n) { auto intros = inductive::inductive_decl_intros(decl); if (length(intros) != 1) - throw exception(sstream() << "error in 'projection' generation, '" - << n << "' must have a single constructor"); + throw exception(sstream() << "error in projection generation, '" + << n << "' does not have a single constructor"); return mk_pair(num_params, head(intros)); } } - optional num_indices = inductive::get_num_indices(env, n); - if (num_indices && *num_indices > 0) - throw exception(sstream() << "error in 'projection' generation, '" - << n << "' is an indexed inductive datatype family"); throw_ill_formed(n); } +static bool is_prop(expr type) { + while (is_pi(type)) { + type = binding_body(type); + } + return is_sort(type) && is_zero(sort_level(type)); +} + environment mk_projections(environment const & env, name const & n, buffer const & proj_names) { // Given an inductive datatype C A (where A represent parameters) // intro : Pi A (x_1 : B_1[A]) (x_2 : B_2[A, x_1]) ..., C A @@ -52,6 +59,8 @@ environment mk_projections(environment const & env, name const & n, buffer expr intro_type = inductive::intro_rule_type(intro); name rec_name = inductive::get_elim_name(n); declaration ind_decl = env.get(n); + if (env.impredicative() && is_prop(ind_decl.get_type())) + throw exception(sstream() << "error in projection generation, '" << n << "' is a proposition"); declaration rec_decl = env.get(rec_name); level_param_names lvl_params = ind_decl.get_univ_params(); levels lvls = param_names_to_levels(lvl_params); @@ -77,7 +86,7 @@ environment mk_projections(environment const & env, name const & n, buffer environment new_env = env; for (name const & proj_name : proj_names) { if (!is_pi(intro_type)) - throw exception(sstream() << "error in projection '" << proj_name << "' generation, '" + throw exception(sstream() << "error generating projection '" << proj_name << "', '" << n << "' does not have sufficient data"); expr result_type = binding_domain(intro_type); buffer proj_args; diff --git a/tests/lean/proj.lean b/tests/lean/proj.lean new file mode 100644 index 000000000..1fcd06a86 --- /dev/null +++ b/tests/lean/proj.lean @@ -0,0 +1,25 @@ +import logic data.nat.basic + +inductive vector (T : Type) : nat → Type := + nil {} : vector T nat.zero, + cons : T → ∀{n}, vector T n → vector T (nat.succ n) + +#projections or +#projections and +#projections eq.refl +#projections eq +#projections vector + +inductive point := +mk : nat → nat → point + +#projections point :: x y z + +#projections point :: x y + +#projections point :: x y + +inductive funny : nat → Type := +mk : Π (a : nat), funny a + +#projections funny diff --git a/tests/lean/proj.lean.expected.out b/tests/lean/proj.lean.expected.out new file mode 100644 index 000000000..a0c06dfa7 --- /dev/null +++ b/tests/lean/proj.lean.expected.out @@ -0,0 +1,8 @@ +proj.lean:7:0: error: error in projection generation, 'or' does not have a single constructor +proj.lean:8:0: error: error in projection generation, 'and' is a proposition +proj.lean:9:0: error: error in projection generation, 'eq.refl' is not an inductive datatype +proj.lean:10:0: error: error in projection generation, 'eq' is an indexed inductive datatype family +proj.lean:11:0: error: error in projection generation, 'vector' is an indexed inductive datatype family +proj.lean:16:0: error: error generating projection 'point.z', 'point' does not have sufficient data +proj.lean:20:0: error: invalid object declaration, environment already has an object named 'point.x' +proj.lean:25:0: error: error in projection generation, 'funny' is an indexed inductive datatype family