feat(compiler/util): add is_recursive_rec_app

src/compiler/util.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/find_fn.h"
 #include "kernel/inductive/inductive.h"
 #include "library/util.h"
 
@@ -52,4 +53,38 @@ void get_rec_args(environment const & env, name const & n, buffer<buffer<bool>>
         }
     }
 }
+
+bool is_recursive_rec_app(environment const & env, expr const & e) {
+    buffer<expr> args;
+    name_generator ngen;
+    expr const & f = get_app_args(e, args);
+    if (!is_constant(f))
+        return false;
+    auto I_name = inductive::is_elim_rule(env, const_name(f));
+    if (!I_name || !is_recursive_datatype(env, *I_name) || is_inductive_predicate(env, *I_name))
+        return false;
+    unsigned nparams       = *inductive::get_num_params(env, *I_name);
+    unsigned nminors       = *inductive::get_num_minor_premises(env, *I_name);
+    unsigned ntypeformers  = *inductive::get_num_type_formers(env, *I_name);
+    buffer<buffer<bool>> is_rec_arg;
+    get_rec_args(env, *I_name, is_rec_arg);
+    for (unsigned i = nparams + ntypeformers, j = 0; i < nparams + ntypeformers + nminors; i++, j++) {
+        buffer<bool> const & minor_is_rec_arg = is_rec_arg[j];
+        expr minor = args[i];
+        buffer<expr> minor_ctx;
+        expr minor_body = fun_to_telescope(ngen, minor, minor_ctx, optional<binder_info>());
+        unsigned sz = std::min(minor_is_rec_arg.size(), minor_ctx.size());
+        if (find(minor_body, [&](expr const & e, unsigned) {
+                    if (!is_local(e))
+                        return false;
+                    for (unsigned k = 0; k < sz; k++) {
+                        if (minor_is_rec_arg[k] && mlocal_name(e) == mlocal_name(minor_ctx[k]))
+                            return true;
+                    }
+                    return false;
+                }))
+            return false;
+    }
+    return true;
+}
 }

src/compiler/util.h

@@ -13,4 +13,10 @@ namespace lean {
     \pre inductive::is_inductive_decl(env, n)
 */
 void get_rec_args(environment const & env, name const & n, buffer<buffer<bool>> & r);
+
+/** \brief Return true iff \c e is of the form <tt>(C.rec ...)</tt> and is recursive.
+    That is, \c C is a recursive inductive datatype, \c C is *not* an inductive predicate,
+    and at least one minor premise uses a recursive argument.
+*/
+bool is_recursive_rec_app(environment const & env, expr const & e);
 }