From d6d72ba80e2914a5498c47561fbf66ecf2bbf915 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 May 2014 10:40:53 -0700
Subject: [PATCH] refactor(kernel): add binder structure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/expr.cpp                |  8 +++-----
 src/kernel/expr.h                  | 25 +++++++++++++++++++------
 src/kernel/inductive/inductive.cpp |  2 +-
 src/kernel/inductive/inductive.h   |  6 ------
 src/library/kernel_bindings.cpp    | 13 +++++++++++++
 5 files changed, 36 insertions(+), 18 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 49cad39ac..8b2d176c9 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -149,15 +149,13 @@ expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const
                    t.has_param_univ() || b.has_param_univ(),
                    std::max(get_depth(t), get_depth(b)) + 1,
                    std::max(get_free_var_range(t), dec(get_free_var_range(b)))),
-    m_name(n),
-    m_domain(t),
-    m_body(b),
-    m_info(i) {
+    m_binder(n, t, i),
+    m_body(b) {
     lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi);
 }
 void expr_binder::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_body, todelete);
-    dec_ref(m_domain, todelete);
+    dec_ref(m_binder.m_type, todelete);
     delete(this);
 }
 
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 92dedb1e3..1ae6c6cd2 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -238,20 +238,33 @@ public:
 bool operator==(expr_binder_info const & i1, expr_binder_info const & i2);
 inline bool operator!=(expr_binder_info const & i1, expr_binder_info const & i2) { return !(i1 == i2); }
 
+class binder {
+    friend class expr_binder;
+    name             m_name;
+    expr             m_type;
+    expr_binder_info m_info;
+public:
+    binder(name const & n, expr const & t, expr_binder_info const & bi):
+        m_name(n), m_type(t), m_info(bi) {}
+    name const & get_name() const { return m_name; }
+    expr const & get_type() const { return m_type; }
+    expr_binder_info const & get_info() const { return m_info; }
+};
+
+typedef list<binder> telescope;
+
 /** \brief Super class for lambda and pi */
 class expr_binder : public expr_composite {
-    name             m_name;
-    expr             m_domain;
+    binder           m_binder;
     expr             m_body;
-    expr_binder_info m_info;
     friend class expr_cell;
     void dealloc(buffer<expr_cell*> & todelete);
 public:
     expr_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info());
-    name const & get_name() const   { return m_name; }
-    expr const & get_domain() const { return m_domain; }
+    name const & get_name() const   { return m_binder.get_name(); }
+    expr const & get_domain() const { return m_binder.get_type(); }
     expr const & get_body() const   { return m_body; }
-    expr_binder_info const & get_info() const { return m_info; }
+    expr_binder_info const & get_info() const { return m_binder.get_info(); }
 };
 
 /** \brief Let expressions */
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index defcada8b..c2241af32 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -22,7 +22,7 @@ environment add_inductive(environment const &          env,
     // 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 e : params) { std::cout << e.get_name() << " "; } 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
index 45296a725..46550b13c 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -16,12 +16,6 @@ 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
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index a468d3da4..5c24a6d68 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/metavar.h"
 #include "kernel/error_msgs.h"
 #include "kernel/type_checker.h"
+#include "kernel/inductive/inductive.h"
 #include "library/occurs.h"
 #include "library/io_state_stream.h"
 #include "library/expr_lt.h"
@@ -1632,6 +1633,18 @@ static void open_type_checker(lua_State * L) {
     SET_GLOBAL_FUN(add_declaration, "add_decl");
 }
 
+telescope to_telescope(lua_State * L, int idx) {
+    luaL_checktype(L, idx, LUA_TTABLE);
+    lua_pushvalue(L, idx);  // push table on the top
+    int sz = objlen(L, -1); // get table size
+    telescope r;
+    for (int i = sz; i >= 1; i--) {
+        // TODO(Leo)
+    }
+    lua_pop(L, 1); // pop table from the top
+    return r;
+}
+
 void open_kernel_module(lua_State * L) {
     open_level(L);
     open_list_level(L);