From 96f391dda2d4c6ef0bc9a995ddfdd5895250b3a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Feb 2016 16:01:12 -0800 Subject: [PATCH] feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command --- src/frontends/lean/structure_cmd.cpp | 34 +++++++++++++------- src/library/definitional/projection.cpp | 15 ++++++--- tests/lean/bad_structures.lean | 2 +- tests/lean/bad_structures.lean.expected.out | 1 - tests/lean/bad_structures2.lean | 3 ++ tests/lean/bad_structures2.lean.expected.out | 3 +- tests/lean/proj.lean.expected.out | 1 - tests/lean/run/pred_using_structure_cmd.lean | 13 ++++++++ 8 files changed, 52 insertions(+), 20 deletions(-) create mode 100644 tests/lean/run/pred_using_structure_cmd.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 37c0f803e..3f8042af5 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/module.h" #include "library/aliases.h" +#include "library/annotation.h" #include "library/coercion.h" #include "library/explicit.h" #include "library/protected.h" @@ -106,7 +107,9 @@ struct structure_cmd_fn { buffer m_fields; std::vector m_renames; std::vector m_field_maps; + bool m_explicit_universe_params; bool m_infer_result_universe; + bool m_inductive_predicate; levels m_ctx_levels; // context levels for creating aliases buffer m_ctx_locals; // context local constants for creating aliases @@ -115,7 +118,9 @@ struct structure_cmd_fn { structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_namespace(get_namespace(m_env)) { m_tc = mk_type_checker(m_env); - m_infer_result_universe = false; + m_explicit_universe_params = false; + m_infer_result_universe = false; + m_inductive_predicate = false; m_gen_eta = get_structure_eta_thm(p.get_options()); m_gen_proj_mk = get_structure_proj_mk_thm(p.get_options()); } @@ -127,10 +132,12 @@ struct structure_cmd_fn { m_name = m_namespace + m_name; buffer ls_buffer; if (parse_univ_params(m_p, ls_buffer)) { - m_infer_result_universe = false; + m_explicit_universe_params = true; + m_infer_result_universe = false; m_level_names.append(ls_buffer); } else { - m_infer_result_universe = true; + m_explicit_universe_params = false; + m_infer_result_universe = true; } m_modifiers.parse(m_p); } @@ -239,8 +246,15 @@ struct structure_cmd_fn { if (m_p.curr_is_token(get_colon_tk())) { m_p.next(); m_type = m_p.parse_expr(); + while (is_annotation(m_type)) + m_type = get_annotation_arg(m_type); + m_inductive_predicate = m_env.impredicative() && is_zero(sort_level(m_type)); if (!is_sort(m_type)) throw parser_error("invalid 'structure', 'Type' expected", pos); + + if (m_inductive_predicate) + m_infer_result_universe = false; + if (m_infer_result_universe) { if (!is_placeholder(sort_level(m_type))) throw parser_error("invalid 'structure', resultant universe level is computed " @@ -248,10 +262,6 @@ struct structure_cmd_fn { } else { if (has_placeholder(m_type)) throw_explicit_universe(pos); - level l = sort_level(m_type); - if (m_env.impredicative() && !is_not_zero(l)) - throw parser_error("invalid 'structure', the resultant universe level should not be zero " - "for any universe parameter assignment", pos); } } else { if (!m_infer_result_universe) @@ -462,7 +472,7 @@ struct structure_cmd_fn { /** \brief Add params, fields and references to parent structures into parser local scope */ void add_locals() { - if (!m_infer_result_universe) { + if (m_explicit_universe_params) { for (name const & l : m_level_names) m_p.add_local_level(l, mk_param_univ(l)); } @@ -948,9 +958,11 @@ struct structure_cmd_fn { declare_projections(); declare_auxiliary(); declare_coercions(); - declare_eta(); - declare_proj_over_mk(); - declare_no_confustion(); + if (!m_inductive_predicate) { + declare_eta(); + declare_proj_over_mk(); + declare_no_confustion(); + } return m_env; } }; diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 6f56e381d..64572d497 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -192,9 +192,10 @@ 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() << "projection generation, '" << n << "' is a proposition"); declaration rec_decl = env.get(rec_name); + bool is_predicate = env.impredicative() && is_prop(ind_decl.get_type()); + bool elim_to_prop = rec_decl.get_num_univ_params() == ind_decl.get_num_univ_params(); + bool dep_elim = inductive::has_dep_elim(env, n); level_param_names lvl_params = ind_decl.get_univ_params(); levels lvls = param_names_to_levels(lvl_params); buffer params; // datatype parameters @@ -222,16 +223,20 @@ environment mk_projections(environment const & env, name const & n, buffer if (!is_pi(intro_type)) throw exception(sstream() << "generating projection '" << proj_name << "', '" << n << "' does not have sufficient data"); + type_checker tc(new_env); expr result_type = binding_domain(intro_type); + if (is_predicate && !tc.is_prop(result_type).first) { + throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', " + << "type is an inductive predicate, but field is not a proposition"); + } buffer proj_args; proj_args.append(params); proj_args.push_back(c); - expr type_former = Fun(c, result_type); + expr type_former = dep_elim ? Fun(c, result_type) : result_type; expr minor_premise = Fun(intro_type_args, mk_var(intro_type_args.size() - i - 1)); expr major_premise = c; - type_checker tc(new_env); level l = sort_level(tc.ensure_sort(tc.infer(result_type).first).first); - levels rec_lvls = append(to_list(l), lvls); + levels rec_lvls = elim_to_prop ? lvls : append(to_list(l), lvls); expr rec = mk_constant(rec_name, rec_lvls); buffer rec_args; rec_args.append(params); diff --git a/tests/lean/bad_structures.lean b/tests/lean/bad_structures.lean index e0a948933..fe86c887c 100644 --- a/tests/lean/bad_structures.lean +++ b/tests/lean/bad_structures.lean @@ -7,6 +7,6 @@ structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type := structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{l} := (pr1 : A) (pr2 : B) -structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} := +structure prod2.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} := (pr1 : A) (pr2 : B) end foo diff --git a/tests/lean/bad_structures.lean.expected.out b/tests/lean/bad_structures.lean.expected.out index febcd137a..9f0c43ff9 100644 --- a/tests/lean/bad_structures.lean.expected.out +++ b/tests/lean/bad_structures.lean.expected.out @@ -1,3 +1,2 @@ bad_structures.lean:1:71: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used -bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment diff --git a/tests/lean/bad_structures2.lean b/tests/lean/bad_structures2.lean index b9c0a20c9..5d53736c3 100644 --- a/tests/lean/bad_structures2.lean +++ b/tests/lean/bad_structures2.lean @@ -29,3 +29,6 @@ structure bla2 extends Type structure bla2 : Prop := (x : Prop) + +structure bla3 : Prop := +(x : nat) diff --git a/tests/lean/bad_structures2.lean.expected.out b/tests/lean/bad_structures2.lean.expected.out index 714cda658..a5ecf0e63 100644 --- a/tests/lean/bad_structures2.lean.expected.out +++ b/tests/lean/bad_structures2.lean.expected.out @@ -8,4 +8,5 @@ bad_structures2.lean:18:2: error: invalid field, identifier expected bad_structures2.lean:23:36: error: invalid 'structure' renaming, parent structure 'foo' does not contain field 'y' bad_structures2.lean:25:23: error: invalid 'structure' extends, 'nat' is not a structure bad_structures2.lean:27:23: error: invalid 'structure', expression must be a 'parent' structure -bad_structures2.lean:30:15: error: invalid 'structure', 'Type' expected +bad_structures2.lean:30:0: error: failed to generate projection 'bla2.x' for 'bla2', type is an inductive predicate, but field is not a proposition +bad_structures2.lean:33:0: error: failed to generate projection 'bla3.x' for 'bla3', type is an inductive predicate, but field is not a proposition diff --git a/tests/lean/proj.lean.expected.out b/tests/lean/proj.lean.expected.out index c0f4521e6..cdac41a99 100644 --- a/tests/lean/proj.lean.expected.out +++ b/tests/lean/proj.lean.expected.out @@ -1,5 +1,4 @@ proj.lean:7:0: error: projection generation, 'or' does not have a single constructor -proj.lean:8:0: error: projection generation, 'and' is a proposition proj.lean:9:0: error: projection generation, 'eq.refl' is not an inductive datatype proj.lean:10:0: error: projection generation, 'eq' is an indexed inductive datatype family proj.lean:11:0: error: projection generation, 'vector' is an indexed inductive datatype family diff --git a/tests/lean/run/pred_using_structure_cmd.lean b/tests/lean/run/pred_using_structure_cmd.lean new file mode 100644 index 000000000..870fb0d37 --- /dev/null +++ b/tests/lean/run/pred_using_structure_cmd.lean @@ -0,0 +1,13 @@ +variable {A : Type} + +structure has_refl (R : A → A → Prop) : Prop := +(refl : ∀ a, R a a) + +structure is_equiv (R : A → A → Prop) extends has_refl R : Prop := +(symm : ∀ a b, R a b → R b a) +(trans : ∀ a b c, R a b → R b c → R a c) + +check @is_equiv.refl +check @is_equiv.symm +check @is_equiv.trans +check @is_equiv.to_has_refl