Mercurial > hg > GearsTemplate

changeset 514:f2a3acc766b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix RedBlackTree.agda
author ryokka
date Thu, 04 Jan 2018 17:46:59 +0900
parents 95865cab040a
children f86da73d611e
files src/parallel_execution/RedBlackTree.agda
diffstat 1 files changed, 38 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 15:10:24 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 17:46:59 2018 +0900
@@ -12,15 +12,15 @@
 record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
   field
     tree : treeImpl
-    treeMethods : TreeMethods {a} {t}
-  putTree : a -> (Tree -> t) -> t
+    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 -> Maybe a -> t) -> t
+  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 : Set where
+data Color {n : Level } : Set n where
   Red   : Color
   Black : Color
 
@@ -29,65 +29,68 @@
   GT : CompareResult
   EQ : CompareResult
 
-record Node (a k : Set) : Set where
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
   field
     key   : k
     value : a
-    right : Maybe (Node a)
-    left  : Maybe (Node a)
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
     color : Color
 open Node
 
-record RedBlackTree (a  k si : Set) : Set where
+record RedBlackTree {n m : Level } (a  k si : Set n) : Set (m Level.⊔ n) where
   field
     root : Maybe (Node a k )
-    stack : Stack si
+    nodeStack : Stack {n} {m} si
     compare : k -> k -> CompareResult
 
 open RedBlackTree
 
 open Stack
 
-insertCase3 : ?
-insertCase3 = ? -- tree datum parent grandparent next 
+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 : Set n} -> RedBlackTree ? ? -> a (Node a) (Node a) ? -> t
+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 = ?; stack = createSingleLinkedStack })
+...                                | Black = next (record { root = {!!}; nodeStack = createSingleLinkedStack })
 
-insertCase1 : {n m : Level } {t : Set m } {a : Set n} -> RedBlackTree ? ? -> a (Maybe (Node a) ) (Node a) ? -> t
-insertCase1 tree datum Nothing grandparent next = next (record { root = ?; stack = 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 : ?
-insertNode tree datum next = get2Stack (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 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)
 
-findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
-findNode1 tree datum n next with (compare datum n)
-...                                | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next)
-...                                | GT = findNode2 tree datum (right n) next
-...                                | LT = findNode2 tree datum (left n) 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
-    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 : ?
-    findNode3 nothing tree next = next tree
-    findNode3 (just n) tree next = 
-           popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))
+    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  {!!} )
 
-findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t
-findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next)
 
-putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
+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 datum n (\ tree1 -> insertNode tree1 datum next)
+...                                | Just n  = findNode tree {!!} n (\ tree1 -> insertNode tree1 datum next)
 
-getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
+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  = datum d
-    stack1 = record { root = (next d) }
+    data1  = {!!} 
+    stack1 = {!!}