Mercurial > hg > GearsTemplate
view src/parallel_execution/RedBlackTree.agda @ 514:f2a3acc766b5
fix RedBlackTree.agda
author | ryokka |
---|---|
date | Thu, 04 Jan 2018 17:46:59 +0900 |
parents | 95865cab040a |
children | f86da73d611e |
line wrap: on
line source
module RedBlackTree where open import stack open import Level 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 data CompareResult {n : Level } : Set n where LT : CompareResult GT : CompareResult EQ : CompareResult 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 open Node record RedBlackTree {n m : Level } (a k si : Set n) : Set (m Level.⊔ n) where field root : Maybe (Node a k ) nodeStack : Stack {n} {m} si compare : k -> k -> CompareResult open RedBlackTree open Stack insertCase3 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {!!} {!!} {!!} -> t) -> t insertCase3 = {!!} -- tree datum parent grandparent next insertCase2 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {!!} {!!} {!!} -> t) -> t insertCase2 tree datum parent grandparent next with (color parent) ... | Red = insertCase3 tree datum parent grandparent next ... | Black = next (record { root = {!!}; nodeStack = createSingleLinkedStack }) insertCase1 : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (Maybe (Node a k) ) -> (Maybe (Node a k)) -> (RedBlackTree {!!} {!!} {!!} -> t) -> t insertCase1 tree datum Nothing grandparent next = next (record { root = {!!}; nodeStack = createSingleLinkedStack }) insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next insertNode : {n m : Level } {t : Set m } {a k : Set n} -> RedBlackTree {!!} {!!} {!!} -> a -> (RedBlackTree {!!} {!!} {!!} -> t) -> t insertNode tree datum next = get2Stack (nodeStack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; nodeStack = s }) datum d1 d2 next) findNode : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree a k {!!} -> (Node a k) -> (Node a k) -> (RedBlackTree a k {!!} -> t) -> t findNode {n} {m} {a} {k} {t} tree n1 next = pushStack (nodeStack tree) n1 (\ s -> findNode1 (record tree {nodeStack = s }) n1 next) where findNode1 : RedBlackTree a k {!!} -> (Node a k) -> (Node a k) -> (RedBlackTree a k {!!} -> t) -> t findNode1 tree n0 n1 next with (compare tree (key n0) (key n1)) ... | EQ = popStack (nodeStack tree) (\s d -> {!!} d (record tree { root = Just (record n {node = datum}); stack = s }) next) ... | GT = {!!} tree datum (right n) next ... | LT = findNode2 tree {!!} (left n1) next where findNode2 : RedBlackTree a k {!!} -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree a k {!!} -> t) -> t findNode2 tree datum Nothing next = insertNode tree datum next findNode2 tree datum (Just n) next = findNode (record tree {root = Just n}) datum n next findNode3 : RedBlackTree a k {!!} -> (Maybe (Node a k)) -> (RedBlackTree a k {!!} -> t) -> t findNode3 tree nothing next = next tree findNode3 tree (Just n) next = popStack (nodeStack tree) (\s d -> findNode3 tree d {!!} ) putRedBlackTree : {a t : Set} -> RedBlackTree {!!} {!!} {!!} -> a -> (RedBlackTree {!!} {!!} {!!} -> t) -> t putRedBlackTree tree datum next with (root tree) ... | Nothing = insertNode tree datum next ... | Just n = findNode tree {!!} n (\ tree1 -> insertNode tree1 datum next) getRedBlackTree : {a t : Set} -> RedBlackTree {!!} {!!} {!!} -> (Code : RedBlackTree {!!} {!!} {!!} -> (Maybe a) -> t) -> t getRedBlackTree tree cs with (root tree) ... | Nothing = cs tree Nothing ... | Just d = cs stack1 (Just data1) where data1 = {!!} stack1 = {!!}