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 = {!!}