--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hoareRedBlackTree.agda	Fri Nov 01 19:12:52 2019 +0900
@@ -0,0 +1,118 @@
+module hoareRedBlackTree where
+
+
+open import Level hiding (zero)
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp
+open import Data.Maybe
+open import Data.Bool
+open import Data.Empty
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+open import stack
+
+
+
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    putImpl : treeImpl → a → (treeImpl → t) → t
+    getImpl  : treeImpl → (treeImpl → Maybe a → t) → t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+  putTree : a → (Tree treeImpl → t) → t
+  putTree d next = putImpl (treeMethods ) tree d (\t1 → next (record {tree = t1 ; treeMethods = treeMethods} ))
+  getTree : (Tree treeImpl → Maybe a → t) → t
+  getTree next = getImpl (treeMethods ) tree (\t1 d → next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+
+data Color {n : Level } : Set n where
+  Red   : Color
+  Black : Color
+
+
+record Node {n : Level } (a : Set n) (k : ℕ) : Set n where
+  inductive
+  field
+    key   : ℕ
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+record RedBlackTree {n m : Level } {t : Set m} (a : Set n) (k : ℕ) : Set (m Level.⊔ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    -- compare : k → k → Tri A B C
+    -- <-cmp 
+
+open RedBlackTree
+
+open SingleLinkedStack
+
+
+
+----
+-- find node potition to insert or to delete, the path will be in the stack
+--
+
+{-# TERMINATING #-}
+findNode : {n m  : Level } {a : Set n} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
+findNode {n} {m} {a} {k} {t} tree n0 next with root tree
+findNode {n} {m} {a} {k} {t} tree n0 next | nothing = next tree
+findNode {n} {m} {a} {k} {t} tree n0 next | just x with <-cmp (key x) (key n0)
+findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree
+findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next)
+findNode {n} {m} {a} {k} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next)
+
+
+findNode1 : {n m  : Level } {a : Set n} {k : ℕ} {t : Set m}  → RedBlackTree {n} {m} {t}   a k → (Node a k) → (RedBlackTree {n} {m} {t} a k → t) → t
+findNode1 {n} {m} {a} {k} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) n0 {!!}
+  where
+    findNode2 : (Maybe (Node a k)) → SingleLinkedStack (Node a k) → Node a k → (Maybe (Node a k) → SingleLinkedStack (Node a k) → t) → t
+    findNode2 nothing st n0 next = next nothing st
+    findNode2 (just x) st n0 next with (<-cmp (key n0) (key x))
+    findNode2 (just x) st n0 next | tri≈ ¬a b ¬c = {!!}
+    findNode2 (just x) st n0 next | tri< a ¬b ¬c = {!!}
+    findNode2 (just x) st n0 next | tri> ¬a ¬b c = {!!}
+
+    findNode3 : SingleLinkedStack (Node a k) → Node a k → t
+    findNode3 s1 n1 with (<-cmp (key n0) (key n1))
+    findNode3 s1 n1 | tri≈ ¬a b ¬c = next (record {root = root tree ; nodeStack = s1})
+    findNode3 s1 n1 | tri< a ¬b ¬c = pushSingleLinkedStack (nodeStack tree) n1 (λ s → findNode2 (left n1) s n0 {!!})
+    findNode3 s1 n1 | tri> ¬a ¬b c = {!!}
+
+-- pushSingleLinkedStack s n1 (\ s → findNode1 s n1)
+  -- module FindNode where
+  --   findNode2 : SingleLinkedStack (Node a k) → (Maybe (Node a k)) → t
+  --   findNode2 s nothing = next tree
+  --   findNode2 s (just n) = findNode tree s n0 n next
+  --   findNode1 : SingleLinkedStack (Node a k) → (Node a k)  → t
+  --   findNode1 s n1 with (<-cmp (key n0) (key n1))
+  --   findNode1 s n1 | tri< a ¬b ¬c = findNode2 s (right n1)
+  --   findNode1 s n1 | tri≈ ¬a b ¬c = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
+  --   findNode1 s n1 | tri> ¬a ¬b c = findNode2 s (left n1)
+    -- ...                                | EQ = popSingleLinkedStack s ( \s _ → next tree s (record n1 { key = key n1 ; value = value n0 } ) )
+    -- ...                                | GT = findNode2 s (right n1)
+    -- ...                                | LT = findNode2 s (left n1)
+
+
+createEmptyRedBlackTreeℕ : {n m  : Level} {t : Set m} (a : Set n) (b : ℕ)
+     → RedBlackTree {n} {m} {t} a b
+createEmptyRedBlackTreeℕ a b = record {
+        root = nothing
+     ;  nodeStack = emptySingleLinkedStack
+     -- ;  nodeComp = λ x x₁ → {!!}
+   }
+
+
+test = findNode (createEmptyRedBlackTreeℕ {!!} 1) 

--- a/redBlackTreeHoare.agda	Fri Nov 01 17:42:51 2019 +0900
+++ b/redBlackTreeHoare.agda	Fri Nov 01 19:12:52 2019 +0900
@@ -1,4 +1,4 @@
-module RedBlackTree where
+module RedBlackTreeHoare where
 
 
 open import Level hiding (zero)
@@ -51,6 +51,7 @@
     root : Maybe (Node a k)
     nodeStack : SingleLinkedStack  (Node a k)
     -- compare : k → k → Tri A B C
+    -- <-cmp 
 
 open RedBlackTree
 
@@ -192,6 +193,7 @@
     insertCase1 n0 s (just parent) nothing = replaceNode tree s (colorNode n0 Black) next
     insertCase1 n0 s (just parent) (just grandParent) = insertCase2 s n0 parent grandParent
 
+
 ----
 -- find node potition to insert or to delete, the path will be in the stack
 --
@@ -285,6 +287,6 @@
 
 -- test = (λ x → (createEmptyRedBlackTreeℕ x x) 
 
-ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0
+-- ts = createEmptyRedBlackTreeℕ {ℕ} {?} {!!} 0
 
 -- tes = putRedBlackTree {_} {_} {_} (createEmptyRedBlackTreeℕ {_} {_} {_} 3 3) 2 2 (λ t → t)