From f55a00a0220d21983c92bbda3f1b0680b2b4df78 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Aug 2019 09:29:05 -0700
Subject: [PATCH] feat(library/init/lean): add `LocalContext`

---
 library/init/data/persistentarray/basic.lean  |  6 ++
 .../init/data/persistenthashmap/basic.lean    |  3 +
 library/init/lean/localcontext.lean           | 97 +++++++++++++++++++
 3 files changed, 106 insertions(+)
 create mode 100644 library/init/lean/localcontext.lean

diff --git a/library/init/data/persistentarray/basic.lean b/library/init/data/persistentarray/basic.lean
index ba0b873b81..8815102933 100644
--- a/library/init/data/persistentarray/basic.lean
+++ b/library/init/data/persistentarray/basic.lean
@@ -36,6 +36,12 @@ namespace PersistentArray
 variables {α : Type u}
 open PersistentArrayNode
 
+def empty : PersistentArray α :=
+{}
+
+def isEmpty (a : PersistentArray α) : Bool :=
+a.size == 0
+
 instance : Inhabited (PersistentArray α) := ⟨{}⟩
 
 def mkEmptyArray : Array α := Array.mkEmpty branching.toNat
diff --git a/library/init/data/persistenthashmap/basic.lean b/library/init/data/persistenthashmap/basic.lean
index 8e58d6e768..479a8a27ab 100644
--- a/library/init/data/persistenthashmap/basic.lean
+++ b/library/init/data/persistenthashmap/basic.lean
@@ -44,6 +44,9 @@ variables {α : Type u} {β : Type v}
 
 def empty : PersistentHashMap α β := {}
 
+def isEmpty (m : PersistentHashMap α β) : Bool :=
+m.size == 0
+
 instance : Inhabited (PersistentHashMap α β) := ⟨{}⟩
 
 def mkEmptyEntries {α β} : Node α β :=
diff --git a/library/init/lean/localcontext.lean b/library/init/lean/localcontext.lean
new file mode 100644
index 0000000000..bc35d3ed94
--- /dev/null
+++ b/library/init/lean/localcontext.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.data.persistentarray.basic
+import init.data.persistenthashmap.basic
+import init.lean.expr
+
+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)
+
+namespace LocalDecl
+instance : Inhabited LocalDecl := ⟨ldecl (default _) (default _) (default _) (default _) (default _)⟩
+
+def isLet : LocalDecl → Bool
+| (cdecl _ _ _ _ _) := false
+| (ldecl _ _ _ _ _) := true
+
+def index : LocalDecl → Nat
+| (cdecl idx _ _ _ _) := idx
+| (ldecl idx _ _ _ _) := idx
+
+def name : LocalDecl → Name
+| (cdecl _ n _ _ _) := n
+| (ldecl _ n _ _ _) := n
+
+def userName : LocalDecl → Name
+| (cdecl _ _ n _ _) := n
+| (ldecl _ _ n _ _) := n
+
+def type : LocalDecl → Expr
+| (cdecl _ _ _ t _) := t
+| (ldecl _ _ _ t _) := t
+
+def binderInfo : LocalDecl → BinderInfo
+| (cdecl _ _ _ _ bi) := bi
+| (ldecl _ _ _ _ _)  := BinderInfo.default
+
+def valueOpt : LocalDecl → Option Expr
+| (cdecl _ _ _ _ _) := none
+| (ldecl _ _ _ _ v) := some v
+
+def value : LocalDecl → Expr
+| (cdecl _ _ _ _ _) := default _
+| (ldecl _ _ _ _ v) := v
+
+end LocalDecl
+
+structure LocalContext :=
+(nameToDecl : PHashMap Name LocalDecl   := PersistentHashMap.empty)
+(decls      : PArray (Option LocalDecl) := PersistentArray.empty)
+
+namespace LocalContext
+instance : Inhabited LocalContext := ⟨{}⟩
+
+def isEmpty (lctx : LocalContext) : Bool :=
+lctx.nameToDecl.isEmpty
+
+def mkLocalDecl (lctx : LocalContext) (name : Name) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : LocalDecl × LocalContext :=
+match lctx with
+| { nameToDecl := map, decls := decls } =>
+  let idx  := decls.size;
+  let decl := LocalDecl.cdecl idx name userName type bi;
+  (decl, { nameToDecl := map.insert name decl, decls := decls.push decl })
+
+def mkLetDecl (lctx : LocalContext) (name : Name) (userName : Name) (type : Expr) (value : Expr) : LocalDecl × LocalContext :=
+match lctx with
+| { nameToDecl := map, decls := decls } =>
+  let idx  := decls.size;
+  let decl := LocalDecl.ldecl idx name userName type value;
+  (decl, { nameToDecl := map.insert name decl, decls := decls.push decl })
+
+def find (lctx : LocalContext) (name : Name) : Option LocalDecl :=
+lctx.nameToDecl.find name
+
+/-
+private partial def popTailNoneAux : PArray (Option LocalDecl) → PArray (Option LocalDecl)
+| a :=
+  if a.size == 0 then a
+  else if
+
+def erase (lctx : LocalContext) (name : Name) : LocalContext :=
+match lctx with
+| { nameToDecl := map, decls := decls } =>
+  match map.find name with
+  | none      => lctx
+  | some decl => { nameToDecl := map.erase name, decls := decls.set decl.index none }
+-/
+
+end LocalContext
+
+end Lean