Mercurial > hg > Papers > 2018 > ryokka-sigos
view Paper/src/AgdaTreeImpl.agda @ 1:bf2887cd22c1
fix Paper
author | ryokka |
---|---|
date | Fri, 13 Apr 2018 19:47:50 +0900 |
parents | |
children | 576637483425 |
line wrap: on
line source
record Node {n : Level } (a k : Set n) : Set n where inductive field key : k value : a right : Maybe (Node a k) left : Maybe (Node a k) color : Color {n} open Node leafNode : {n : Level } {a k : Set n} -> k -> a -> Node a k leafNode k1 value = record { key = k1 ; value = value ; right = Nothing ; left = Nothing ; color = Red } open leafNode record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where field root : Maybe (Node a k) nodeStack : SingleLinkedStack (Node a k) compare : k -> k -> CompareResult {n} open RedBlackTree putRedBlackTree : {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 putRedBlackTree {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 -> insertNode tree1 s n1 next)) -- 以下省略