From f403ea984b50942229e901877759e6049afe9392 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 May 2015 15:08:10 -0700 Subject: [PATCH] feat(frontends/lean): add 'print [recursor]' command for debugging purposes --- src/frontends/lean/builtin_cmds.cpp | 19 +++++++++++++++ src/library/user_recursors.cpp | 4 ++-- tests/lean/urec.lean | 7 ++++++ tests/lean/urec.lean.expected.out | 36 +++++++++++++++++++++++++++++ 4 files changed, 64 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2be998019..1a8add25a 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "library/class.h" #include "library/flycheck.h" #include "library/util.h" +#include "library/user_recursors.h" #include "library/pp_options.h" #include "library/definitional/projection.h" #include "frontends/lean/util.h" @@ -227,6 +228,21 @@ static void print_inductive(parser & p, name const & n, pos_info const & pos) { } } +static void print_recursor_info(parser & p) { + name c = p.check_constant_next("invalid 'print [recursor]', constant expected"); + recursor_info info = get_recursor_info(p.env(), c); + p.regular_stream() << "recursor information\n" + << " num. parameters: " << info.get_num_params() << "\n" + << " num. indices: " << info.get_num_indices() << "\n"; + if (auto r = info.get_motive_univ_pos()) + p.regular_stream() << " motive univ. pos. : " << *r << "\n"; + else + p.regular_stream() << " recursor eliminate only to Prop\n"; + p.regular_stream() << " motive pos.: " << info.get_motive_pos() << "\n" + << " major premise pos.: " << info.get_major_pos() << "\n" + << " dep. elimination: " << info.has_dep_elim() << "\n"; +} + bool print_constant(parser & p, char const * kind, declaration const & d) { io_state_stream out = p.regular_stream(); out << kind << " " << d.get_name(); @@ -388,6 +404,9 @@ environment print_cmd(parser & p) { auto pos = p.pos(); name c = p.check_constant_next("invalid 'print inductive', constant expected"); print_inductive(p, c, pos); + } else if (p.curr_is_token(get_recursor_tk())) { + p.next(); + print_recursor_info(p); } else if (print_polymorphic(p)) { } else { throw parser_error("invalid print command", p.pos()); diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index cb5d82220..559acb028 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -58,7 +58,7 @@ static void throw_invalid_major(buffer const & tele, expr const & I, unsig recursor_info mk_recursor_info(environment const & env, name const & r) { if (auto I = inductive::is_elim_rule(env, r)) { - if (*inductive::get_num_type_formers(env, r) > 1) + if (*inductive::get_num_type_formers(env, *I) > 1) throw exception(sstream() << "unsupported recursor '" << r << "', it has multiple motives"); optional motive_univ_pos; if (env.get(name(*I, "rec")).get_num_univ_params() != env.get(name(*I)).get_num_univ_params()) @@ -66,7 +66,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r) { return recursor_info(r, *I, *inductive::get_num_params(env, *I), *inductive::get_num_indices(env, *I), - *inductive::get_elim_major_idx(env, *I), + *inductive::get_elim_major_idx(env, r), motive_univ_pos, inductive::has_dep_elim(env, *I)); } diff --git a/tests/lean/urec.lean b/tests/lean/urec.lean index 08008a1c6..a378b947d 100644 --- a/tests/lean/urec.lean +++ b/tests/lean/urec.lean @@ -31,3 +31,10 @@ set_option pp.implicit true set_option pp.universes true check @myrec + +print [recursor] myrec +print [recursor] nat.induction_on +check @vector.induction_on +print [recursor] vector.induction_on +check @Exists.rec +print [recursor] Exists.rec diff --git a/tests/lean/urec.lean.expected.out b/tests/lean/urec.lean.expected.out index c17a9bdf0..8ab087d2d 100644 --- a/tests/lean/urec.lean.expected.out +++ b/tests/lean/urec.lean.expected.out @@ -5,3 +5,39 @@ urec.lean:23:0: error: invalid user defined recursor, resultant type of minor pr myrec.{l_1 l_2} : Π (A : Type.{l_1}) (M : list.{l_1} A → Type.{l_2}) (l : list.{l_1} A), M (@nil.{l_1} A) → (Π (a : A), M [a]) → (Π (a₁ a₂ : A), M [a₁, a₂]) → M l +recursor information + num. parameters: 1 + num. indices: 0 + motive univ. pos. : 1 + motive pos.: 1 + major premise pos.: 2 + dep. elimination: 1 +recursor information + num. parameters: 0 + num. indices: 0 + recursor eliminate only to Prop + motive pos.: 0 + major premise pos.: 1 + dep. elimination: 1 +vector.induction_on.{l_1} : + ∀ {A : Type.{l_1}} {C : Π (a : nat), vector.{l_1} A a → Prop} {a : nat} (n : vector.{l_1} A a), + C nat.zero (@vector.nil.{l_1} A) → + (∀ {n : nat} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) → + C a n +recursor information + num. parameters: 1 + num. indices: 1 + recursor eliminate only to Prop + motive pos.: 1 + major premise pos.: 3 + dep. elimination: 1 +Exists.rec.{l_1} : + ∀ {A : Type.{l_1}} {P : A → Prop} {C : Prop}, + (∀ (a : A), P a → C) → @Exists.{l_1} A P → C +recursor information + num. parameters: 2 + num. indices: 0 + recursor eliminate only to Prop + motive pos.: 2 + major premise pos.: 4 + dep. elimination: 0