From eb0abf557d5432c5c592043e16840effb9b6bd1a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 May 2014 09:53:51 -0700
Subject: [PATCH] feat(kernel/inductive): add inductive datatype kernel
 extension module interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt                  |  2 +
 src/kernel/inductive/CMakeLists.txt |  2 +
 src/kernel/inductive/inductive.cpp  | 31 +++++++++++++++
 src/kernel/inductive/inductive.h    | 58 +++++++++++++++++++++++++++++
 4 files changed, 93 insertions(+)
 create mode 100644 src/kernel/inductive/CMakeLists.txt
 create mode 100644 src/kernel/inductive/inductive.cpp
 create mode 100644 src/kernel/inductive/inductive.h

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8c3c3c506..edab51127 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -213,6 +213,8 @@ add_subdirectory(util/interval)
 set(LEAN_LIBS ${LEAN_LIBS} interval)
 add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
+add_subdirectory(kernel/inductive)
+set(LEAN_LIBS ${LEAN_LIBS} inductive)
 add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 # add_subdirectory(library/rewriter)
diff --git a/src/kernel/inductive/CMakeLists.txt b/src/kernel/inductive/CMakeLists.txt
new file mode 100644
index 000000000..b284e7a69
--- /dev/null
+++ b/src/kernel/inductive/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_library(inductive inductive.cpp)
+target_link_libraries(inductive ${LEAN_LIBS})
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
new file mode 100644
index 000000000..defcada8b
--- /dev/null
+++ b/src/kernel/inductive/inductive.cpp
@@ -0,0 +1,31 @@
+/*
+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/inductive/inductive.h"
+
+namespace lean {
+namespace inductive {
+environment add_inductive(environment const & env,  name const & ind_name, level_params const & level_params,
+                          telescope const & params, telescope const & indices, list<intro_rule> const & intro_rules,
+                          optional<unsigned> const & univ_offset) {
+    return add_inductive(env, level_params, params, list<inductive_decl>(std::make_tuple(ind_name, indices, intro_rules)), univ_offset);
+}
+
+environment add_inductive(environment const &          env,
+                          level_params const &         level_params,
+                          telescope const &            params,
+                          list<inductive_decl> const & decls,
+                          optional<unsigned> const &   univ_offset) {
+    // TODO(Leo)
+    std::cout << "add_inductive\n";
+    for (auto l : level_params) { std::cout << l << " "; } std::cout << "\n";
+    for (auto e : params) { std::cout << std::get<0>(e) << " "; } std::cout << "\n";
+    for (auto d : decls) { std::cout << std::get<0>(d) << " "; } std::cout << "\n";
+    if (univ_offset) std::cout << "offset: " << *univ_offset << "\n";
+    return env;
+}
+}
+}
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
new file mode 100644
index 000000000..45296a725
--- /dev/null
+++ b/src/kernel/inductive/inductive.h
@@ -0,0 +1,58 @@
+/*
+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 <memory>
+#include <utility>
+#include <tuple>
+#include "util/list.h"
+#include "kernel/environment.h"
+
+namespace lean {
+namespace inductive {
+/** \brief Return a normalizer extension for inductive dataypes. */
+std::unique_ptr<normalizer_extension> mk_extension();
+
+/** \brief Simple telescope */
+typedef list<std::tuple<name,             // binder name, used only for pretty printing
+                        expr,             // type
+                        expr_binder_info
+                        >> telescope;
+
+/** \brief Introduction rule */
+typedef std::tuple<name,              // introduction rule name
+                   telescope,         // arguments
+                   expr               // result type
+                   > intro_rule;
+
+typedef param_names level_params;
+
+/** \brief Inductive datatype */
+typedef std::tuple<name,                // datatype name
+                   telescope,           // indices
+                   list<intro_rule>     // introduction rules for this datatype
+                   > inductive_decl;
+
+/** \brief Declare a finite set of mutually dependent inductive datatypes. */
+environment add_inductive(environment const &          env,
+                          level_params const &         level_params,
+                          telescope const &            params,
+                          list<inductive_decl> const & decls,
+                          // By default the resultant inductive datatypes live in max(level_params),
+                          // we can add an offset/lift k, and the resultant type is succ^k(max(level_params)).
+                          // If none is provided, then for impredicative environments the result types are Bool/Prop (level 0)
+                          optional<unsigned> const &   univ_offset = optional<unsigned>(0));
+
+/** \brief Declare a single inductive datatype. */
+environment add_inductive(environment const &        env,
+                          name const &               ind_name,         // name of new inductive datatype
+                          level_params const &       level_params,     // level parameters
+                          telescope const &          params,           // parameters
+                          telescope const &          indices,          // indices
+                          list<intro_rule> const &   intro_rules,      // introduction rules
+                          optional<unsigned> const & univ_offset = optional<unsigned>(0));
+}
+}