From 4fd1ee761954f88d01b385aee83fc757e2a436c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Nov 2014 12:26:26 -0800
Subject: [PATCH] feat(library/definitional/util): add `is_recursive_datatype`
 auxiliary function

---
 src/library/definitional/CMakeLists.txt |  2 +-
 src/library/definitional/util.cpp       | 28 +++++++++++++++++++++++++
 src/library/definitional/util.h         | 20 ++++++++++++++++++
 3 files changed, 49 insertions(+), 1 deletion(-)
 create mode 100644 src/library/definitional/util.cpp
 create mode 100644 src/library/definitional/util.h

diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt
index 07dfa2ece..d0187d191 100644
--- a/src/library/definitional/CMakeLists.txt
+++ b/src/library/definitional/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp eq.cpp heq.cpp
-  no_confusion.cpp projection.cpp)
+  no_confusion.cpp util.cpp projection.cpp)
 
 target_link_libraries(definitional ${LEAN_LIBS})
diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp
new file mode 100644
index 000000000..9db90c0d8
--- /dev/null
+++ b/src/library/definitional/util.cpp
@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+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"
+
+namespace lean {
+bool is_recursive_datatype(environment const & env, name const & n) {
+    optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
+    if (!decls)
+        return false;
+    for (inductive::inductive_decl const & decl : std::get<2>(*decls)) {
+        for (inductive::intro_rule const & intro : inductive::inductive_decl_intros(decl)) {
+            expr type = inductive::intro_rule_type(intro);
+            while (is_pi(type)) {
+                if (find(binding_domain(type), [&](expr const & e, unsigned) {
+                            return is_constant(e) && const_name(e) == n; }))
+                    return true;
+                type = binding_body(type);
+            }
+        }
+    }
+    return false;
+}
+}
diff --git a/src/library/definitional/util.h b/src/library/definitional/util.h
new file mode 100644
index 000000000..998ec7f10
--- /dev/null
+++ b/src/library/definitional/util.h
@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
+    That is, it must be an inductive datatype AND contain a recursive constructor.
+
+    \remark Records are inductive datatypes, but they are not recursive.
+
+    \remerk For mutually indutive datatypes, \c n is considered recursive
+    if there is a constructor taking \c n.
+*/
+bool is_recursive_datatype(environment const & env, name const & n);
+}