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

fix(library/definitional/projection): remove redundant 'error in'

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-29 13:42:50 -07:00
parent 854e7ba1be
commit 88d55bfef0
2 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/definitional/projection.cpp
View file

@ -14,23 +14,23 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
[[ noreturn ]] static void throw_ill_formed(name const & n) { [[ 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() << "projection generation, '" << n << "' is an ill-formed inductive datatype");
} }
static pair<unsigned, inductive::intro_rule> get_nparam_intro_rule(environment const & env, name const & n) { static pair<unsigned, inductive::intro_rule> get_nparam_intro_rule(environment const & env, name const & n) {
optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n); optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
if (!decls) if (!decls)
throw exception(sstream() << "error in projection generation, '" << n << "' is not an inductive datatype"); throw exception(sstream() << "projection generation, '" << n << "' is not an inductive datatype");
optional<unsigned> num_indices = inductive::get_num_indices(env, n); optional<unsigned> num_indices = inductive::get_num_indices(env, n);
if (num_indices && *num_indices > 0) if (num_indices && *num_indices > 0)
throw exception(sstream() << "error in projection generation, '" throw exception(sstream() << "projection generation, '"
<< n << "' is an indexed inductive datatype family"); << n << "' is an indexed inductive datatype family");
unsigned num_params = std::get<1>(*decls); unsigned num_params = std::get<1>(*decls);
for (auto const & decl : std::get<2>(*decls)) { for (auto const & decl : std::get<2>(*decls)) {
if (inductive::inductive_decl_name(decl) == n) { if (inductive::inductive_decl_name(decl) == n) {
auto intros = inductive::inductive_decl_intros(decl); auto intros = inductive::inductive_decl_intros(decl);
if (length(intros) != 1) if (length(intros) != 1)
throw exception(sstream() << "error in projection generation, '" throw exception(sstream() << "projection generation, '"
<< n << "' does not have a single constructor"); << n << "' does not have a single constructor");
return mk_pair(num_params, head(intros)); return mk_pair(num_params, head(intros));
} }
@ -60,7 +60,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
name rec_name = inductive::get_elim_name(n); name rec_name = inductive::get_elim_name(n);
declaration ind_decl = env.get(n); declaration ind_decl = env.get(n);
if (env.impredicative() && is_prop(ind_decl.get_type())) if (env.impredicative() && is_prop(ind_decl.get_type()))
throw exception(sstream() << "error in projection generation, '" << n << "' is a proposition"); throw exception(sstream() << "projection generation, '" << n << "' is a proposition");
declaration rec_decl = env.get(rec_name); declaration rec_decl = env.get(rec_name);
level_param_names lvl_params = ind_decl.get_univ_params(); level_param_names lvl_params = ind_decl.get_univ_params();
levels lvls = param_names_to_levels(lvl_params); levels lvls = param_names_to_levels(lvl_params);
@ -86,7 +86,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
environment new_env = env; environment new_env = env;
for (name const & proj_name : proj_names) { for (name const & proj_name : proj_names) {
if (!is_pi(intro_type)) if (!is_pi(intro_type))
throw exception(sstream() << "error generating projection '" << proj_name << "', '" throw exception(sstream() << "generating projection '" << proj_name << "', '"
<< n << "' does not have sufficient data"); << n << "' does not have sufficient data");
expr result_type = binding_domain(intro_type); expr result_type = binding_domain(intro_type);
buffer<expr> proj_args; buffer<expr> proj_args;

14
tests/lean/proj.lean.expected.out
View file

@ -1,8 +1,8 @@
proj.lean:7:0: error: error in projection generation, 'or' does not have a single constructor proj.lean:7:0: error: projection generation, 'or' does not have a single constructor
proj.lean:8:0: error: error in projection generation, 'and' is a proposition proj.lean:8:0: error: projection generation, 'and' is a proposition
proj.lean:9:0: error: error in projection generation, 'eq.refl' is not an inductive datatype proj.lean:9:0: error: 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:10:0: error: 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:11:0: error: 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:16:0: 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: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 proj.lean:25:0: error: projection generation, 'funny' is an indexed inductive datatype family