Mercurial > hg > GearsTemplate

changeset 517:d595acd16550

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
author Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
date Thu, 04 Jan 2018 19:51:14 +0900
parents 62a77785cb2b (current diff) 54ff7a97aec1 (diff)
children b6be5a5c8b9f c9f90f573efe
files
diffstat 2 files changed, 110 insertions(+), 81 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 19:50:46 2018 +0900
+++ b/src/parallel_execution/RedBlackTree.agda	Thu Jan 04 19:51:14 2018 +0900
@@ -1,78 +1,99 @@
 module RedBlackTree where
 
 open import stack
+open import Level
 
-record Tree {a t : Set} (treeImpl : Set) : Set  where
+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
-    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
-    getImpl  : treeImpl -> (treeImpl -> Maybe a -> 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 treeImpl -> Maybe a -> t) -> t
+  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
 
 open Tree
 
-
-putTree : {a t : Set} -> Tree -> a -> (Tree -> t) -> t
-putTree {a} {t} t0 d next = (putImpl t0) (tree t0) d (\t1 -> next (record t0 {tree = t1} ))
-
-getTree : {a t : Set} -> Tree -> (Tree -> t) -> t
-getTree {a} {t} t0  next = (getImpl t0) (tree t0) (\t1 -> next t0)
-
-
-data Color : Set where
+data Color {n : Level } : Set n where
   Red   : Color
   Black : Color
 
-record Node (a : Set) : Set where
+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
-    node  : Element a
-    right : Maybe (Node a)
-    left  : Maybe (Node a)
-    color : Color
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
 
-record RedBlackTree (a : Set) : Set where
+record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
   field
-    root : Maybe (Node a)
-    stack : Stack
+    root : Maybe (Node a k)
+    nodeStack : Stack {n} {m} (Node a k) {t} si
+    compare : k -> k -> CompareResult {n}
 
 open RedBlackTree
 
-insertNode : ?
-insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)
+open Stack
+
 
-putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> 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)
-
-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)
+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)
 
-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 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
-    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 nothing tree next = next tree
-    findNode3 (just n) tree next = 
-           popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } }))
+    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
+        -- 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)
 
 
-insertCase1 tree datum nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack })
-insertCase1 tree datum (just parent) grandparent next = insertCase2 tree datum parent grandparent next
-
-insertCase2 tree datum parent grandparent next with (color parent)
-...                                | Red = insertCase3 tree datum parent grandparent next
-...                                | Black = next (record { root = ?; stack = createSingleLinkedStack })
+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 
+    }
 
-insertCase3 tree datum parent grandparent next 
+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 : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
-getRedBlackTree tree cs with (root tree)
-...                                | Nothing = cs tree  Nothing
-...                                | Just d  = cs stack1 (Just data1)
+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  = datum d
-    stack1 = record { root = (next d) }
+    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 19:50:46 2018 +0900
+++ b/src/parallel_execution/stack.agda	Thu Jan 04 19:51:14 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
@@ -95,7 +95,7 @@
     pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
     pop2SingleLinkedStack' stack cs with (next d)
     ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1))
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
     
 
 getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
@@ -120,18 +120,28 @@
 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
 
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-                             stack = emptySingleLinkedStack ;
-                             stackMethods = record {
+-----
+-- 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 = record {
                                    push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
                                  ; pop2 = pop2SingleLinkedStack
                                  ; get  = getSingleLinkedStack
                                  ; get2 = get2SingleLinkedStack
-                                 }
                            }
 
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = singleLinkedStackSpec 
+                           }
+
+----
+--
+-- proof of properties ( concrete cases )
+--
 
 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
 test01 stack _ with (top stack)
@@ -155,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)
 
@@ -168,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 )
 
@@ -180,23 +190,21 @@
 
 ------
 --
+-- proof of properties with indefinite state of stack
+--
 -- this should be proved by properties of the stack inteface, not only by the implementation,
 --    and the implementation have to provides the properties.
 --
---    we cannot write "s ≡ s3", since level of the Set does not fit , but we cant use stack s ≡ stack s3
+--    we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok.
+--    anyway some implementations may result s != s3
 --  
--- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) ->
---     pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))))
--- push->push->pop2 {l} {D} x y s = {!!}
---    where
---       t0 :  (s3 : Stack {_} {succ l} {D} {Set l} (SingleLinkedStack D)) (x1 y1 : Maybe D) -> (stack s ≡ stack s3 )  ->  (Just x ≡ x1 ) -> (Just y ≡ y1 )
---           -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) )) 
---       t0 s3 x1 y1 refl refl refl = record { pi1 = refl ; pi2 = record { pi1 = refl ; pi2 = refl } }
---       t1 :  (s2 : Stack (SingleLinkedStack D))  ->   pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
---       t1 s2 = {!!} 
---       t2 :  (s1 : Stack (SingleLinkedStack D)) (x1 y1 : Maybe D) ->   
---            pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ) ))
---       t2 s1 = {!!}
+
+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 ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
 
 
 id : {n : Level} {A : Set n} -> A -> A