From bad3f8e77e61738c7fded53ced4046115b9f889c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Aug 2019 10:47:50 -0700
Subject: [PATCH] chore(kernel/local_ctx): use new representation defined at
 `localcontext.lean`

---
 src/kernel/local_ctx.cpp |  9 +++------
 src/kernel/local_ctx.h   | 23 +++++++++++++++--------
 2 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp
index d0c8644ac3..24dd94fad1 100644
--- a/src/kernel/local_ctx.cpp
+++ b/src/kernel/local_ctx.cpp
@@ -24,15 +24,12 @@ bool is_local_decl_ref(expr const & e) { // TODO(Leo): delete
 local_decl::local_decl():object_ref(*g_dummy_decl) {}
 
 local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v):
-    object_ref(mk_cnstr(0, n, un, t, v, sizeof(unsigned) + sizeof(unsigned char))) {
-    cnstr_set_scalar<unsigned>(raw(), sizeof(object*)*4, idx);
-    cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*4+sizeof(unsigned), 0);
+    object_ref(mk_cnstr(1, nat(idx), n, un, t, v)) {
 }
 
 local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, binder_info bi):
-    object_ref(mk_cnstr(0, n, un, t, object_ref(box(0)), sizeof(unsigned) + sizeof(unsigned char))) {
-    cnstr_set_scalar<unsigned>(raw(), sizeof(object*)*4, idx);
-    cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*4+sizeof(unsigned), static_cast<unsigned char>(bi));
+    object_ref(mk_cnstr(0, nat(idx), n, un, t, sizeof(unsigned char))) {
+    cnstr_set_scalar<unsigned char>(raw(), sizeof(object*)*4, static_cast<unsigned char>(bi));
 }
 
 local_decl::local_decl(local_decl const & d, expr const & t, expr const & v):
diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h
index a7b4554841..1a1daed55f 100644
--- a/src/kernel/local_ctx.h
+++ b/src/kernel/local_ctx.h
@@ -11,6 +11,11 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
+/*
+inductive LocalDecl
+| cdecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (bi : BinderInfo)
+| ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
+*/
 class local_decl : public object_ref {
     friend class local_ctx;
     friend class local_context;
@@ -26,16 +31,18 @@ public:
     local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; }
     local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; }
     friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); }
-    name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 0)); }
-    name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
-    expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
+    unsigned get_idx() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
+    name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
+    name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 2)); }
+    expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 3)); }
     optional<expr> get_value() const {
-        /* Remark: if we decide to expose `local_decl` in Lean, we will need to use Lean `option` type. */
-        if (is_scalar(cnstr_get(raw(), 3))) return none_expr();
-        else return some_expr(static_cast<expr const &>(cnstr_get_ref(raw(), 3)));
+        if (cnstr_tag(raw()) == 0) return none_expr();
+        return some_expr(static_cast<expr const &>(cnstr_get_ref(raw(), 4)));
+    }
+    binder_info get_info() const {
+        if (cnstr_tag(raw()) == 0) return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*4));
+        else return binder_info();
     }
-    unsigned get_idx() const { return cnstr_get_scalar<unsigned>(raw(), sizeof(object*)*4); }
-    binder_info get_info() const { return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(raw(), sizeof(object*)*4+sizeof(unsigned))); }
     expr mk_ref() const;
 };