Members/Moririn: redBlackTreeTest.agda annotate

annotate redBlackTreeTest.agda @ 628:ec2506b532ba

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 08 Nov 2021 23:44:24 +0900
parents	7bacba816277
children

rev	line source
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	1 module redBlackTreeTest where
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	2
554 988c12d7f887 use another nat comparator Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 553 diff changeset	3 open import Level hiding (zero) renaming ( suc to succ )
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	4
553 7d9af1d4b5af add compareTri ryokka parents: 552 diff changeset	5 open import Data.Empty
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	6 open import Data.List
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	7 open import Data.Maybe
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	8 open import Data.Bool
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	9 open import Data.Nat
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	10 open import Data.Nat.Properties as NatProp
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	11
553 7d9af1d4b5af add compareTri ryokka parents: 552 diff changeset	12 open import Relation.Nullary
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	13 open import Relation.Binary
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	14
40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	15 open import Algebra
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	16
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	17 open import RedBlackTree
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	18 open import stack
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	19
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	20 open Tree
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	21 open Node
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	22 open RedBlackTree.RedBlackTree
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	23 open Stack
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	24
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	25 -- tests
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	26
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	27 putTree1 : {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
543 1595dd84fc3e fix use SingleLinkedStack ryokka parents: 542 diff changeset	28 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	29 ... \| nothing = next (record tree {root = just (leafNode k1 value) })
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	30 ... \| just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next))
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	31
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	32 open import Relation.Binary.PropositionalEquality
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	33 open import Relation.Binary.Core
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	34 open import Function
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	35
fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	36
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	37 -- check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	38 -- check1 nothing _ = false
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	39 -- check1 (just n) x with Data.Nat.compare (value n) x
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	40 -- ... \| equal _ = true
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	41 -- ... \| _ = false
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	42
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	43 check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	44 check2 nothing _ = false
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	45 check2 (just n) x with compare2 (value n) x
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	46 ... \| EQ = true
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	47 ... \| _ = false
549 bc3208d510cd add some Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 548 diff changeset	48
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	49 test1 : {m : Level} {A B C : Set} → putTree1 {Level.zero} {succ Level.zero} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ {!!} {!!} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true ))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	50 test1 = {!!}
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	51
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	52 -- test2 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	53 -- λ t → putTree1 t 2 2 (
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	54 -- λ t → getRedBlackTree t 1 (
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	55 -- λ t x → check2 {m} x 1 ≡ true )))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	56 -- test2 = refl
537 fffeaf0b0024 add stackTest redBlackTreeTest ryokka parents: diff changeset	57
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	58 -- open ≡-Reasoning
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	59 -- test3 : {m : Level} → putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	60 -- $ λ t → putTree1 t 2 2
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	61 -- $ λ t → putTree1 t 3 3
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	62 -- $ λ t → putTree1 t 4 4
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	63 -- $ λ t → getRedBlackTree t 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	64 -- $ λ t x → check2 {m} x 1 ≡ true
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	65 -- test3 {m} = begin
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	66 -- check2 {m} (just (record {key = 1 ; value = 1 ; color = Black ; left = nothing ; right = just (leafNode 2 2)})) 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	67 -- ≡⟨ refl ⟩
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	68 -- true
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	69 -- ∎
542 ee65e69c9b62 puttree1 act ryokka parents: 541 diff changeset	70
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	71 -- test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	72 -- $ λ t → putTree1 t 2 2
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	73 -- $ λ t → putTree1 t 3 3
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	74 -- $ λ t → putTree1 t 4 4
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	75 -- $ λ t → getRedBlackTree t 4
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	76 -- $ λ t x → x
538 5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work ryokka parents: 537 diff changeset	77
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	78 -- -- test5 : Maybe (Node ℕ ℕ)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	79 -- test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	80 -- $ λ t → putTree1 t 6 6
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	81 -- $ λ t0 → clearSingleLinkedStack (nodeStack t0)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	82 -- $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	83 -- $ λ t1 s n1 → replaceNode t1 s n1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	84 -- $ λ t → getRedBlackTree t 3
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	85 -- -- $ λ t x → SingleLinkedStack.top (stack s)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	86 -- -- $ λ t x → n1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	87 -- $ λ t x → root t
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	88 -- where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	89 -- findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	90 -- findNode1 t s n1 nothing next = next t s n1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	91 -- findNode1 t s n1 ( just n2 ) next = findNode t s n1 n2 next
538 5c001e8ba0d5 add redBlackTreeTest.agda test5,test51. but not work ryokka parents: 537 diff changeset	92
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	93 -- -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t →
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	94 -- -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ just (record { key = 1; value = 1; left = just (record { key = 2 ; value = 2 } ); right = nothing} )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	95 -- -- test51 = refl
539 39d465c20e5a print contant tree. C-c C-n test. ryokka parents: 538 diff changeset	96
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	97 -- test6 : Maybe (Node ℕ ℕ)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	98 -- test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)})
539 39d465c20e5a print contant tree. C-c C-n test. ryokka parents: 538 diff changeset	99
39d465c20e5a print contant tree. C-c C-n test. ryokka parents: 538 diff changeset	100
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	101 -- test7 : Maybe (Node ℕ ℕ)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	102 -- test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	103 -- where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	104 -- tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	105 -- k1 = 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	106 -- n2 = leafNode 0 0
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	107 -- value1 = 1
539 39d465c20e5a print contant tree. C-c C-n test. ryokka parents: 538 diff changeset	108
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	109 -- test8 : Maybe (Node ℕ ℕ)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	110 -- test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	111 -- $ λ t → putTree1 t 2 2 (λ t → root t)
544 4f692df9b3db add reference ryokka parents: 543 diff changeset	112
4f692df9b3db add reference ryokka parents: 543 diff changeset	113
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	114 -- test9 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 {m} x 1 ≡ true ))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	115 -- test9 = refl
544 4f692df9b3db add reference ryokka parents: 543 diff changeset	116
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	117 -- test10 : {m : Level} → putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	118 -- λ t → putRedBlackTree t 2 2 (
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	119 -- λ t → getRedBlackTree t 1 (
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	120 -- λ t x → check2 {m} x 1 ≡ true )))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	121 -- test10 = refl
545 b180dc78abcf add someTest ryokka parents: 544 diff changeset	122
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	123 -- test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	124 -- $ λ t → putRedBlackTree t 2 2
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	125 -- $ λ t → putRedBlackTree t 3 3
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	126 -- $ λ t → getRedBlackTree t 2
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	127 -- $ λ t x → root t
545 b180dc78abcf add someTest ryokka parents: 544 diff changeset	128
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	129
40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	130 compTri : ( x y : ℕ ) -> Tri (x < y) ( x ≡ y ) ( x > y )
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	131 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder)
565 ba7c5f1c2937 this slightly better Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 564 diff changeset	132 where open import Relation.Binary
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	133
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	134 checkT : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	135 checkT nothing _ = false
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	136 checkT (just n) x with compTri (value n) x
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	137 ... \| tri≈ _ _ _ = true
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	138 ... \| _ = false
564 40ab3d39e49d using strict total order Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 563 diff changeset	139
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	140 checkEQ : {m : Level } ( x : ℕ ) -> ( n : Node ℕ ℕ ) -> (value n ) ≡ x -> checkT {m} (just n) x ≡ true
565 ba7c5f1c2937 this slightly better Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 564 diff changeset	141 checkEQ x n refl with compTri (value n) x
566 d9ef8333ff79 use ⊥-elim (neq refl) Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 565 diff changeset	142 ... \| tri≈ _ refl _ = refl
d9ef8333ff79 use ⊥-elim (neq refl) Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 565 diff changeset	143 ... \| tri> _ neq gt = ⊥-elim (neq refl)
d9ef8333ff79 use ⊥-elim (neq refl) Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 565 diff changeset	144 ... \| tri< lt neq _ = ⊥-elim (neq refl)
565 ba7c5f1c2937 this slightly better Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 564 diff changeset	145
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	146 -- checkEQ' : {m : Level } ( x y : ℕ ) -> ( eq : x ≡ y ) -> ( x ≟ y ) ≡ yes eq
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	147 -- checkEQ' x y refl with x ≟ y
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	148 -- ... \| yes refl = refl
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	149 -- ... \| no neq = ⊥-elim ( neq refl )
546 b654ce34c894 add putTest1Lemma1, putTest1 ryokka parents: 545 diff changeset	150
571 1eccf1f18a59 add more detail Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 570 diff changeset	151 --- search -> checkEQ
1eccf1f18a59 add more detail Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 570 diff changeset	152 --- findNode -> search
1eccf1f18a59 add more detail Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 570 diff changeset	153
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	154 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} {A B C : Set Level.zero } → RedBlackTree {Level.zero} {m} {t} {A} {B} {C} a ℕ
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	155 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; nodeComp = λ x x₁ → {!!} } -- record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compTri }
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	156
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	157
573 8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	158 open stack.SingleLinkedStack
8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	159 open stack.Element
8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	160
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	161
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	162 insertP : { a : Set } { t : Set } {P : Set } → ( f : ( a → t ) → t ) ( g : a → t ) ( g' : P → a → t )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	163 → ( p : P )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	164 → ( g ≡ g' p )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	165 → f ( λ x → g' p x ) ≡ f ( λ x → g x )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	166 insertP f g g' p refl = refl
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	167
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	168
573 8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	169 {-# TERMINATING #-}
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	170 inStack : {l : Level} (n : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → Bool
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	171 inStack {l} n s with ( top s )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	172 ... \| nothing = true
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	173 ... \| just n1 with compTri (key n) (key (datum n1))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	174 ... \| tri> _ neq _ = inStack {l} n ( record { top = next n1 } )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	175 ... \| tri< _ neq _ = inStack {l} n ( record { top = next n1 } )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	176 ... \| tri≈ _ refl _ = false
573 8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	177
8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	178 record StackTreeInvariant ( n : Node ℕ ℕ )
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	179 <<<<<<< working copy
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	180 ( s : SingleLinkedStack (Node ℕ ℕ) ) : Set where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	181 \|\|\|\|\|\|\| base
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	182 ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	183 =======
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	184 ( s : SingleLinkedStack (Node ℕ ℕ) ) ( t : RedBlackTree ℕ ℕ ) : Set where
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	185 >>>>>>> destination
573 8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	186 field
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	187 <<<<<<< working copy
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	188 -- sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	189 notInStack : inStack n s ≡ True → ⊥
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	190 \|\|\|\|\|\|\| base
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	191 sti : replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT x1 (value n) ≡ True)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	192 notInStack : inStack n s ≡ True → ⊥
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	193 =======
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	194 sti : {m : Level} → replaceNode t s n $ λ t1 → getRedBlackTree t1 (key n) (λ t2 x1 → checkT {m} x1 (value n) ≡ true)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	195 notInStack : {m : Level} → inStack {m} n s ≡ true → ⊥
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	196 >>>>>>> destination
573 8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	197
8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	198 open StackTreeInvariant
8777baeb90f8 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 572 diff changeset	199
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	200 <<<<<<< working copy
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	201 putTest1 : (n : Maybe (Node ℕ ℕ))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	202 → (k : ℕ) (x : ℕ)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	203 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	204 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	205 putTest1 n k x with n
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	206 ... \| Just n1 = lemma0
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	207 where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	208 tree0 : (n1 : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	209 tree0 n1 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	210 lemma2 : (n1 : Node ℕ ℕ) (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	211 → findNode (tree0 n1 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	212 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	213 lemma2 n1 s STI with compTri k (key n1)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	214 ... \| tri> le eq gt with (right n1)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	215 ... \| Just rightNode = {!!} -- ( lemma2 rightNode ( record { top = Just ( cons n1 (top s) ) } ) (record {notInStack = {!!} } ) )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	216 ... \| Nothing with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	217 ... \| tri≈ _ refl _ = {!!}
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	218 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	219 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	220 lemma2 n1 s STI \| tri< le eq gt = {!!}
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	221 lemma2 n1 s STI \| tri≈ le refl gt = lemma5 s ( tree0 n1 s ) n1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	222 where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	223 lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	224 ( \ s1 _ -> (replaceNode (tree0 n1 s1) s1 (record n1 { key = k ; value = x } ) (λ t →
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	225 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	226 lemma5 s t n with (top s)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	227 ... \| Just n2 with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	228 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	229 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	230 ... \| tri≈ _ refl _ = ⊥-elim ( (notInStack STI) {!!} )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	231 lemma5 s t n \| Nothing with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	232 ... \| tri≈ _ refl _ = checkEQ x _ refl
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	233 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	234 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	235 lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 n1 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	236 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	237 lemma0 = lemma2 n1 (record {top = Nothing}) ( record { notInStack = {!!} } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	238 ... \| Nothing = lemma1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	239 where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	240 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	241 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	242 ( λ t x1 → checkT x1 x ≡ True)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	243 lemma1 with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	244 ... \| tri≈ _ refl _ = checkEQ x _ refl
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	245 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	246 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	247 \|\|\|\|\|\|\| base
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	248 putTest1 : (n : Maybe (Node ℕ ℕ))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	249 → (k : ℕ) (x : ℕ)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	250 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	251 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	252 putTest1 n k x with n
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	253 ... \| Just n1 = lemma0
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	254 where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	255 tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	256 tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	257 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	258 → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	259 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True)))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	260 lemma2 s STI with compTri k (key n1)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	261 ... \| tri≈ le refl gt = lemma5 s ( tree0 s ) n1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	262 where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	263 lemma5 : (s : SingleLinkedStack (Node ℕ ℕ) ) → ( t : RedBlackTree ℕ ℕ ) → ( n : Node ℕ ℕ ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	264 ( \ s1 _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t →
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	265 GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	266 lemma5 s t n with (top s)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	267 ... \| Just n2 with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	268 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	269 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	270 ... \| tri≈ _ refl _ = ⊥-elim ( (notInStack STI) {!!} )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	271 lemma5 s t n \| Nothing with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	272 ... \| tri≈ _ refl _ = checkEQ x _ refl
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	273 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	274 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	275 ... \| tri> le eq gt = sti ( record { sti = {!!} ; notInStack = {!!} } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	276 ... \| tri< le eq gt = {!!}
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	277 lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ tree1 s n1 → replaceNode tree1 s n1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	278 (λ t → getRedBlackTree t k (λ t x1 → checkT x1 x ≡ True))))
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	279 lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!} ; notInStack = {!!} } )
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	280 ... \| Nothing = lemma1
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	281 where
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	282 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record {
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	283 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y } ) k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	284 ( λ t x1 → checkT x1 x ≡ True)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	285 lemma1 with compTri k k
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	286 ... \| tri≈ _ refl _ = checkEQ x _ refl
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	287 ... \| tri< _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	288 ... \| tri> _ neq _ = ⊥-elim (neq refl)
7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	289 =======
575 73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	290
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	291 -- testn : {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	292 -- testn = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	293 -- $ λ t → putTree1 t 1 1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	294 -- $ λ t → putTree1 t 3 3 (λ ta → record {root = root ta ; nodeStack = nodeStack ta })
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	295
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	296
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	297 -- List と Node で書こうとしたがなんだかんだListに直したほうが楽そうだった
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	298
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	299 nullNode = (record {key = 0 ; value = 0 ; right = nothing ; left = nothing ; color = Red})
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	300
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	301 -- treeTotal : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → (List ℕ → t) → t
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	302 -- treeTotal {m} {t} s tr next with (left tr) \| (right tr)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	303 -- treeTotal {m} {t} s tr next \| nothing \| nothing = next ((key tr) ∷ [])
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	304 -- treeTotal {m} {t} s tr next \| nothing \| just x = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	305 -- treeTotal {m} {t} s tr next \| just x \| nothing = treeTotal {m} {t} s x (λ li → next ((key tr) ∷ li))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	306 -- treeTotal {m} {t} s tr next \| just x \| just x₁ = treeTotal {m} {t} s x (λ li1 → treeTotal {m} {t} s x₁ (λ li2 → next (s ++ li1 ++ li2)))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	307 treeTotal : { n m : Level } {a : Set n} {t : Set m} → ( s : List a ) → ( tr : (Node a a) ) → List a
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	308 treeTotal {n} {m} {a} {t} s tr with (left tr) \| (right tr)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	309 treeTotal {n} {m} {a} {t} s tr \| nothing \| nothing = (key tr) ∷ []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	310 treeTotal {n} {m} {a} {t} s tr \| nothing \| just x = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	311 treeTotal {n} {m} {a} {t} s tr \| just x \| nothing = (key tr) ∷ (treeTotal {n} {m} {a} {t} s x)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	312 treeTotal {n} {m} {a} {t} s tr \| just x \| just x₁ = s ++ ((key tr) ∷ (treeTotal {n} {m} {a} {t} s x) ++ (treeTotal {n} {m} {a} {t} s x₁))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	313
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	314
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	315 -- treeTotalA : { m : Level } {t : Set m} → ( s : List ℕ ) → ( tr : (Node ℕ ℕ) ) → List ℕ
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	316
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	317 -- (treeTotal {_} {ℕ} ([]) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} testn 5 5 {!!}))))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	318
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	319 -- exput : (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ ℕ))) (λ total → {!!})) ≡ {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	320 -- exput = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	321
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	322
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	323 -- aaa = (treeTotal {_} {_} {ℕ} {_} (5 ∷ []) ((record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black })))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	324
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	325
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	326 -- fuga = putTree1 {_} {_} {ℕ} {ℕ} (record {root = just (record { key = 4 ; value = 4 ; right = just (leafNode 6 6) ; left = just (leafNode 3 3) ; color = Black }) ; nodeStack = ( record {top = nothing}) ; compare = (λ x x₁ → EQ) }) 5 5 (λ aaa → aaa )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	327
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	328 -- nontree ++ 2 :: []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	329
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	330 -- piyo = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 2 2 ( λ t1 → findNode t1 (record {top = nothing}) (leafNode 2 2) (Data.Maybe.fromMaybe nullNode (root t1)) (λ tree stack node → {!!}))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	331
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	332
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	333 -- exn2l : {!!} ≡ (treeTotal {_} {ℕ} ([]) (putTree1 {_} {_} {ℕ} {ℕ} {!!} 5 5 (λ t → {!!}))) -- (treeTotal {_} {ℕ} (5 ∷ []) (Data.Maybe.fromMaybe nullNode (root testn)))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	334 -- exn2l = refl
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	335
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	336
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	337
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	338
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	339
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	340 -- record FS {n m : Level } {a : Set n} {t : Set m} (oldTotal : List a) ( s : List a ) ( tr : (Node a a) ) : Set where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	341 -- field
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	342 -- total : treeTotal {n} {m} {a} {t} s tr ≡ oldTotal
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	343 -- -- usage = FS.total -- relation
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	344
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	345 -- data P { n m : Level } { t : Set m } : Set where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	346 -- P₀ : (old : List ℕ) ( s : List ℕ ) → (tr : (Node ℕ ℕ) ) → FS {m} {t} old s tr → P
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	347
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	348
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	349
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	350 -- ttt = putTree1 {_} {_} {ℕ} {ℕ}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	351
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	352 -- record TreeInterface {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set n where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	353 -- field
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	354 -- tree : treeImpl
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	355 -- list : List ℕ
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	356 -- node : Node ℕ ℕ
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	357 -- putTreeHoare : (FS {_} {ℕ} list list node) → putTree1 {!!} {!!} {!!} {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	358
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	359 stack2list : {n m : Level} {t : Set m} {a : Set n} → (s : SingleLinkedStack a) → List a
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	360 stack2list stack with top stack
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	361 stack2list stack \| just x = (datum x) ∷ (elm2list {_} {_} {ℕ} x)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	362 where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	363 elm2list : {n m : Level} {t : Set m} {a : Set n} → (elm : (Element a)) → List a
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	364 elm2list el with next el
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	365 elm2list el \| just x = (datum el) ∷ (elm2list {_} {_} {ℕ} x)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	366 elm2list el \| nothing = (datum el) ∷ []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	367 stack2list stack \| nothing = []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	368
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	369
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	370 -- list2element : {n m : Level} {t : Set m} {a : Set n} → (l : List a) → Maybe (Element a)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	371 -- list2element [] = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	372 -- list2element (x ∷ l) = just (cons x (list2element {_} {_} {ℕ} l))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	373
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	374 -- ltest = list2element (1 ∷ 2 ∷ 3 ∷ [])
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	375
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	376 list2stack : {n m : Level} {t : Set m} {a : Set n} {st : SingleLinkedStack a} → (l : List a) → SingleLinkedStack a
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	377 list2stack {n} {m} {t} {a} {s} (x ∷ l) = pushSingleLinkedStack s x (λ s1 → list2stack {n} {m} {t} {a} {s1} l )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	378 list2stack {n} {m} {t} {a} {s} [] = s
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	379
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	380
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	381
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	382 -- stest = list2stack (1 ∷ 2 ∷ 3 ∷ [])
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	383
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	384 open Node
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	385
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	386 exfind : { m : Level } { t : Set m} → (dt : ℕ) → (node : (Node ℕ ℕ)) → (st : List ℕ) → findNode {_} {_} {ℕ} {ℕ} (redBlackInSomeState ℕ (just node)) (emptySingleLinkedStack) (leafNode dt dt) (node) (λ t1 st1 n1 → (( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ≡ ( treeTotal {_} {m} {ℕ} {t} (dt ∷ st) (node) ) ))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	387 exfind dt node st with left node \| right node
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	388 exfind dt node st \| just x \| just x₁ = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	389 exfind dt node st \| just x \| nothing = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	390 exfind dt node st \| nothing \| just x = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	391 exfind dt node st \| nothing \| nothing with (compTri dt (key node))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	392 exfind dt node st \| nothing \| nothing \| tri< a ¬b ¬c = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	393 exfind dt node st \| nothing \| nothing \| tri≈ ¬a b ¬c = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	394 exfind dt node st \| nothing \| nothing \| tri> ¬a ¬b c = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	395
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	396 -- exput : (ni : ℕ) → (tn : Node ℕ ℕ) → (ts : List ℕ) → (treeTotal {_} {ℕ} (ni ∷ ts) tn)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	397 -- ≡ (treeTotal {_} {ℕ} (ts) (Data.Maybe.fromMaybe nullNode (root (putTree1 {_} {_} {ℕ} {ℕ} (record { root = just tn } ) ni ni (λ tt → tt)))))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	398 -- exput datum node [] with (right node) \| (left node)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	399 -- exput datum node [] \| nothing \| nothing = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	400 -- exput datum node [] \| just x \| just x₁ = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	401 -- exput datum node [] \| just x \| nothing = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	402 -- exput datum node [] \| nothing \| just x = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	403 -- exput datum node (x ∷ stack₁) = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	404
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	405
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	406 -- proofTree : {n m : Level} {t : Set m} {a : Set n} (old stackl : List ℕ) → (node : Node ℕ ℕ) → (FS {_} {ℕ} old stackl node) → (tree : RedBlackTree ℕ ℕ) → (key : ℕ) → findNode {{!!}} {{!!}} {{!!}} {{!!}} tree (list2stack {!!} (record {top = nothing})) (leafNode key key) node (λ tree1 stack1 datum → {!!})
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	407 -- -- -- -- putTree1 tree key key (λ t → (FS {_} {ℕ} old stackl (Data.Maybe.fromMaybe nullNode (root tree))) )
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	408 -- proofTree old stack node fs t k = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	409
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	410 -- FS は証明そのものになると思ってたけど実は違いそう
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	411 -- oldTotal と現在の node, stack の組み合わせを比較する
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	412 -- oldTotal はどうやって作る? ><
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	413 -- treeTotal は list と node を受け取ってそれの total を出すのでそれで作る(list に put するデータなどを入れることで適当に作れる)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	414
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	415 -- p : {n m : Level} {t : Set m} {a : Set n} → ( s : SingleLinkedStack ℕ ) ( tr : (Node ℕ ℕ) ) ( tree : RedBlackTree ℕ ℕ ) (k : ℕ) → (FS (treeTotal (k ∷ (stack2list s)) tr) (stack2list s) tr) → putTree1 tree k k (λ atree → FS (treeTotal (stack2list s) (Data.Maybe.fromMaybe (tr) (root atree))) {!!} {!!})
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	416 -- p stack node tree key = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	417
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	418 -- tt = (FS {_} {ℕ} [] [] (Data.Maybe.fromMaybe nullNode (root (createEmptyRedBlackTreeℕ {_} ℕ {ℕ}))))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	419
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	420 -- ttt : (a : P) → P
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	421 -- ttt a = P₀ {!!} {!!} (record { key = {!!} ; value = {!!} ; right = {!!} ; left = {!!} ; color = {!!} }) (record { total = {!!} })
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	422
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	423
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	424 -- FS では stack tree をあわせた整合性を示したい
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	425 -- そのためには...?
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	426 -- stack は前の node (というか一段上)が入ってる
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	427 -- tree は現在の node がある
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	428
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	429
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	430 -- tr(Node ℕ ℕ) s (List (Node))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	431 -- 3 []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	432 -- / \
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	433 -- 2 5
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	434 -- / / \
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	435 -- 1 4 6
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	436
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	437 -- search 6 (6 > 3)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	438 -- tr(Node ℕ ℕ) s (List (Node))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	439 -- 5 just (node (1 2 nothing) 3 (4 5 6)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	440 -- / \ []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	441 -- 4 6
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	442
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	443 -- search 6 (6 > 5)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	444 -- tr(Node ℕ ℕ) s (List (Node))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	445 -- 6 just (node (4 5 6))
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	446 -- just (node (1 2 nothing) 3 (4 5 6)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	447 -- []
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	448
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	449 -- just 6 → true みたいな感じ
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	450
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	451 -- stack に node ごと入れるのは間違い…？
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	452 -- 一応非破壊な感じがする(新しく作り直してる)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	453 -- どう釣り合いをとるか
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	454
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	455 -- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	456 -- stack+tree {n} stack mid org = st stack mid org where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	457 -- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	458 -- st [] _ _ = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	459 -- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) \| Data.Nat.compare (value x) (value org)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	460 -- st (x ∷ []) n n1 \| equal .(key x) \| equal .(value x) = just org
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	461 -- st (x ∷ []) n n1 \| _ \| _ = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	462 -- st (x ∷ a) n n1 with st a n n1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	463 -- st (x ∷ a) n n1 \| just x₁ = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	464 -- st (x ∷ a) n n1 \| nothing = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	465
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	466
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	467 -- stack+tree : {n m : Level} {t : Set m} → List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → (Maybe (Node ℕ ℕ) → t) → t
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	468 -- stack+tree {n} stack mid org cg = st stack mid org
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	469 -- where
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	470 -- st : List (Node ℕ ℕ) → Node ℕ ℕ → Node ℕ ℕ → Maybe (Node ℕ ℕ)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	471 -- st [] _ _ = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	472 -- st (x ∷ []) n n1 with Data.Nat.compare (key x) (key org) \| Data.Nat.compare (value x) (value org)
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	473 -- st (x ∷ []) n n1 \| equal .(key x) \| equal .(value x) = just org
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	474 -- st (x ∷ []) n n1 \| _ \| _ = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	475 -- st (x ∷ a) n n1 with st a n n1
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	476 -- st (x ∷ a) n n1 \| just x₁ = {!!}
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	477 -- st (x ∷ a) n n1 \| nothing = nothing
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	478
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	479 -- findNodePush : {n : Level} → (stack : List (Node ℕ ℕ)) → (mid : Node ℕ ℕ) → (org : Node ℕ ℕ) → stack+tree stack mid org ≡ just ?
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	480 -- → ? {return (? ∷ stack),mid'} → stack+tree (? ∷ stack) (mid') org ≡ just ?
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	481 -- findNodePush
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	482
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	483 -- stack+tree が just だって言えたらよい
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	484 -- {}2 は orig のどっちかのNode
73fc32092b64 push local rbtree ryokka parents: 574 diff changeset	485
578 7bacba816277 use list base simple stack Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 575 diff changeset	486 >>>>>>> destination

Mercurial > hg > Members > Moririn

annotate redBlackTreeTest.agda @ 628:ec2506b532ba