feat(frontends/lean): add 'print [recursor]' command for debugging purposes

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

src/library/user_recursors.cpp

@@ -58,7 +58,7 @@ static void throw_invalid_major(buffer<expr> 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<unsigned> 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));
     }

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

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