# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1523413797 -32400
# Node ID 40ab3d39e49d54695585e7ca162b60dc3b445419
# Parent  8634f448e69963f2e40a9683813764c223d2822a
using strict total order

diff -r 8634f448e699 -r 40ab3d39e49d RedBlackTree.agda
--- a/RedBlackTree.agda	Fri Mar 30 11:09:06 2018 +0900
+++ b/RedBlackTree.agda	Wed Apr 11 11:29:57 2018 +0900
@@ -2,6 +2,9 @@
 
 open import stack
 open import Level hiding (zero)
+open import Relation.Binary
+open import Data.Nat.Properties   as NatProp
+
 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
@@ -215,17 +218,28 @@
 ... | equal _ = EQ
 ... | greater _ _ = GT
 
+compareT :  ℕ → ℕ → CompareResult {Level.zero}
+compareT x y with IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) x y
+... | tri≈ _ _ _ = EQ
+... | tri< _ _ _ = LT
+... | tri> _ _ _ = GT
+
 compare2 : (x y : ℕ ) -> CompareResult {Level.zero}
 compare2 zero zero = EQ
 compare2 (suc _) zero = GT
 compare2  zero (suc _) = LT
 compare2  (suc x) (suc y) = compare2 x y
 
+putUnblanceTree : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t
+putUnblanceTree {n} {m} {a} {k} {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (λ  s → findNode tree s (leafNode k1 value) n2 (λ  tree1 s n1 → replaceNode tree1 s n1 next))
+
 
 createEmptyRedBlackTreeℕ : { m : Level } (a : Set Level.zero) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ 
 createEmptyRedBlackTreeℕ  {m} a {t} = record {
         root = Nothing
      ;  nodeStack = emptySingleLinkedStack
-     ;  compare = compare2
+     ;  compare = compareT
    }
  
diff -r 8634f448e699 -r 40ab3d39e49d redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Fri Mar 30 11:09:06 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Apr 11 11:29:57 2018 +0900
@@ -9,6 +9,11 @@
 open import Data.Nat
 open import Relation.Nullary
 
+
+open import Algebra
+open import Relation.Binary
+open import Data.Nat.Properties   as NatProp
+
 open Tree
 open Node
 open RedBlackTree.RedBlackTree
@@ -120,7 +125,7 @@
 
 
 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ 
-redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
+redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT }
 
 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero}
 -- compare2 zero zero = EQ
@@ -242,34 +247,41 @@
       lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
       lemma2 = refl
 
+open IsStrictTotalOrder
+
+compTri :  ( x y : ℕ ) ->  Tri  (x < y) ( x ≡ y )  ( x > y )
+compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 
+
+checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
+checkT Nothing _ = False
+checkT (Just n) x with compTri (value n)  x
+...  | tri≈ _ _ _ = True
+...  | _ = False
+
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ) 
          → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-         (λ  t → getRedBlackTree t k (λ  t x1 → check2 x1 x  ≡ True)) 
+         (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
 putTest1 n k x with n
 ...  | Just n1 = lemma2 ( record { top = Nothing } )
    where
-     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
-         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
-     lemma2 s with compare2 k (key n1)
-     ... |  EQ = lemma3 {!!}
+     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) →
+       putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compareT }) k x (λ t →
+       GetRedBlackTree.checkNode t k (λ t₁ x1 → checkT x1 x ≡ True) (root t))
+     lemma2 s with compTri k (key n1)
+     ... |  tri≈ le eq gt = lemma3
         where 
-           lemma3 : compare2 k (key n1) ≡  EQ → getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+           lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
-               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( λ  t x1 → check2 x1 x  ≡ True)
-           lemma3 eq with compare2 x x | putTest1Lemma2 x 
-           ... | EQ | refl with compare2 k (key n1)  | eq
-           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
-           ...                    | EQ | refl = refl
-     ... |  GT = {!!}
-     ... |  LT = {!!}
+               } ) ; nodeStack = s ; compare = λ x₁ y → compareT x₁ y  } ) k ( λ  t x1 → checkT x1 x  ≡ True)
+           lemma3 = {!!}
+     ... |  tri> le eq gt = {!!}
+     ... |  tri< le eq gt = {!!}
 ...  | Nothing =  lemma1  
    where 
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red 
-        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
-        ( λ  t x1 → check2 x1 x  ≡ True) 
-     lemma1 with compare2 k k | putTest1Lemma2 k
-     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
-     ...              | EQ | refl = refl
+        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
+        ( λ  t x1 → checkT x1 x  ≡ True) 
+     lemma1 = {!!}