Mercurial > hg > Gears > GearsAgda

changeset 515:54ff7a97aec1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix findNode in Agda
author ryokka
date Thu, 04 Jan 2018 19:45:32 +0900
parents f86da73d611e
children d595acd16550
files src/parallel_execution/RedBlackTree.agda src/parallel_execution/stack.agda
diffstat 2 files changed, 54 insertions(+), 51 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 18:10:15 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 19:45:32 2018 +0900
@@ -42,55 +42,58 @@
 record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
   field
     root : Maybe (Node a k)
-    nodeStack : Stack {n} {m} {{!!}} {t} si
+    nodeStack : Stack {n} {m} (Node a k) {t} si
     compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
 
 open Stack
 
-insertCase3 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase3 = {!!} -- tree datum parent grandparent next 
 
-insertCase2 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase2 tree datum parent grandparent next with (color parent)
-...                                | Red = insertCase3 tree datum parent grandparent next
-...                                | Black = next (record { root = {!!}; nodeStack = {!!}})
-
-insertCase1 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (Maybe (Node a k) ) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase1 tree datum Nothing grandparent next = next (record { root = {!!}; nodeStack = {!!} })
-insertCase1 tree datum (Just parent) grandparent next = insertCase2 tree datum parent grandparent next
-
-insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertNode tree datum next = get2Stack (nodeStack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; nodeStack = s }) datum d1 d2 next)
+insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+insertNode tree s datum next = get2Stack s (\ s d1 d2 -> {!!} tree s datum d1 d2 next)
 
-findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-findNode {n} {m} {a} {k} {si} {t} tree n0 n1 next = pushStack (nodeStack tree) n1 (\ s -> findNode1 (record tree {nodeStack = s }) n0 n1 next)
+findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
+findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
   where
-    findNode1 : RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> 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
+    findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
+    findNode2 s Nothing = next tree s n0
+    findNode2 s (Just n) = findNode tree s n0 n next
+    findNode1 : Stack (Node a k) si -> (Node a k)  -> t
+    findNode1 s n1 with (compare tree (key n0) (key n1))
+    ...                                | EQ = next tree s n0 
+    ...                                | GT = findNode2 s (right n1)
+    ...                                | LT = findNode2 s (left n1)
       where
-        findNode2 : RedBlackTree {n} {m} {t} a k si -> (Node a k) -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-        findNode2 tree datum Nothing next = insertNode tree {!!} next
-        findNode2 tree datum (Just n) next = findNode (record tree {root = Just n}) datum n next
-        findNode3 : RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-        findNode3 tree nothing next = next tree
-        findNode3 tree (Just n) next = 
-                  popStack (nodeStack tree) (\s d -> findNode3 tree d  {!!} )
+        -- findNode3 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
+        -- findNode3 s nothing = next tree s n0
+        -- findNode3 s (Just n) = 
+        --           popStack (nodeStack tree) (\s d -> findNode3 s d)
 
 
-putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-putRedBlackTree tree datum next with (root tree)
-...                                | Nothing = insertNode tree datum next
-...                                | Just n  = findNode tree {!!} n (\ tree1 -> insertNode tree1 datum next)
+leafNode : {n m : Level } {a k si : Set n} {t : Set m} -> k -> a -> Node a k
+leafNode k1 value = record {
+    key   = k1 ;
+    value = value ;
+    right = Nothing ;
+    left  = Nothing ;
+    color = Black 
+    }
 
-getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> (Code : RedBlackTree {n} {m} {t} a k si -> (Maybe a) -> t) -> t
-getRedBlackTree tree cs with (root tree)
-...                                | Nothing = cs tree  Nothing
-...                                | Just d  = cs stack1 (Just data1)
+putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
+putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = findNode tree (nodeStack tree) (leafNode {n} {m} {a} {k} {si} {t} k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
+
+getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
+getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
   where
-    data1  = {!!} 
-    stack1 = {!!}
+    checkNode : Maybe (Node a k) -> t
+    checkNode Nothing = cs tree Nothing
+    checkNode (Just n) = search n
+      where
+        search : Node a k -> t
+        search n with compare tree k1 (key n)
+        search n | LT = checkNode (left n)
+        search n | GT = checkNode (right n)
+        search n | EQ = cs tree (Just n)
--- a/src/parallel_execution/stack.agda	Thu Jan 04 18:10:15 2018 +0900
+++ b/src/parallel_execution/stack.agda	Thu Jan 04 19:45:32 2018 +0900
@@ -21,7 +21,7 @@
   Nothing : Maybe a
   Just    : a -> Maybe a
 
-record StackMethods {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
   field
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
@@ -30,19 +30,19 @@
     get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
 open StackMethods
 
-record Stack {n m : Level } {a : Set n } {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
   field
     stack : si
-    stackMethods : StackMethods {n} {m} {a} {t} si
-  pushStack :  a -> (Stack si -> t) -> t
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a -> (Stack a si -> t) -> t
   pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
-  popStack : (Stack si -> Maybe a  -> t) -> t
+  popStack : (Stack a si -> Maybe a  -> t) -> t
   popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  pop2Stack :  (Stack si -> Maybe a -> Maybe a -> t) -> t
+  pop2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
   pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
-  getStack :  (Stack si -> Maybe a  -> t) -> t
+  getStack :  (Stack a si -> Maybe a  -> t) -> t
   getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  get2Stack :  (Stack si -> Maybe a -> Maybe a -> t) -> t
+  get2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
   get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
 
 open Stack
@@ -123,7 +123,7 @@
 -----
 -- Basic stack implementations are specifications of a Stack
 --
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} {a} {t} (SingleLinkedStack a)
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
 singleLinkedStackSpec = record {
                                    push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
@@ -132,7 +132,7 @@
                                  ; get2 = get2SingleLinkedStack
                            }
 
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
 createSingleLinkedStack = record {
                              stack = emptySingleLinkedStack ;
                              stackMethods = singleLinkedStackSpec 
@@ -165,7 +165,7 @@
 
 -- after push 1 and 2, pop2 get 1 and 2
 
-testStack02 : {m : Level } -> ( Stack (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
+testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
 testStack02 cs = pushStack createSingleLinkedStack 1 (
    \s -> pushStack s 2 cs)
 
@@ -178,7 +178,7 @@
 testStack032  (Just d1) (Just d2) = testStack031 d1 d2
 testStack032  _ _ = False
 
-testStack03 : {m : Level } -> Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
+testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
 testStack03 s cs = pop2Stack s (
    \s d1 d2 -> cs d1 d2 )
 
@@ -199,7 +199,7 @@
 --    anyway some implementations may result s != s3
 --  
 
-stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} {D} {t}  ( SingleLinkedStack  D )
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
 
 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->