--- a/src/parallel_execution/RedBlackTree.agda	Wed Jan 19 17:51:07 2022 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-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 {n}
-open Node
-
-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} (Node a k) {t} si
-    compare : k -> k -> CompareResult {n}
-
-open RedBlackTree
-
-open Stack
-
---
--- put new node at parent node, and rebuild tree to the top
---
-{-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
-replaceNode : {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 -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
-      \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
-  where
-        replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
-        replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )   
-        replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
-        replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
-        replaceNode1 s (Just grandParent) result with result
-        ... | LT =  replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
-        ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
-        ... | EQ =  next tree 
-
-rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-insertCase5 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-{-# TERMINATING #-}
-insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
-   where
-    insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
-          -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
-    insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
-    insertCase3 s n0 parent grandParent with left grandParent | right grandParent
-    ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
-    ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
-    ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
-    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
-    ...                   | _ with color uncle
-    ...                           | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 
-           record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } )  ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
-    ...                           | Black = insertCase4 tree s n0 parent grandParent next
-    insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
-    insertCase2 s n0 parent grandParent with color parent
-    ... | Black = replaceNode tree s grandParent n0 next
-    ... | Red = insertCase3 s n0 parent grandParent
-    insertCase1 s n0 Nothing Nothing = next tree
-    insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
-    insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
-    insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
-      where
-
-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 : 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)
-
-
-leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
-leafNode k1 value = record {
-    key   = k1 ;
-    value = value ;
-    right = Nothing ;
-    left  = Nothing ;
-    color = Black 
-  }
-
-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 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
-    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	Wed Jan 19 17:51:07 2022 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-open import Level renaming (suc to succ ; zero to Zero )
-module stack  where
-
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.Core
-open import Data.Nat
-
-ex : 1 + 2 ≡ 3
-ex = refl
-
-data Bool {n : Level } : Set n where
-  True  : Bool
-  False : Bool
-
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
-
-data Maybe {n : Level } (a : Set n) : Set n where
-  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
-  field
-    push : stackImpl -> a -> (stackImpl -> t) -> t
-    pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-    pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
-    get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-    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
-  field
-    stack : si
-    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 a si -> Maybe a  -> t) -> t
-  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  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 a si -> Maybe a  -> t) -> t
-  getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  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
-
-data Element {n : Level } (a : Set n) : Set n where
-  cons : a -> Maybe (Element a) -> Element a
-
-datum : {n : Level } {a : Set n} -> Element a -> a
-datum (cons a _) = a
-
-next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
-next (cons _ n) = n
-
-
-{-
--- cannot define recrusive record definition. so use linked list with maybe.
-record Element {l : Level} (a : Set n l) : Set n (suc l) where
-  field
-    datum : a  -- `data` is reserved by Agda.
-    next : Maybe (Element a)
--}
-
-
-
-record SingleLinkedStack {n : Level } (a : Set n) : Set n where
-  field
-    top : Maybe (Element a)
-open SingleLinkedStack
-
-pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
-pushSingleLinkedStack stack datum next = next stack1
-  where
-    element = cons datum (top stack)
-    stack1  = record {top = Just element}
-
-
-popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-popSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack1 (Just data1)
-  where
-    data1  = datum d
-    stack1 = record { top = (next d) }
-
-pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
-...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
-  where
-    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 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
-getSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack (Just data1)
-  where
-    data1  = datum d
-
-get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
-...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
-  where
-    get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-    get2SingleLinkedStack' stack cs with (next d)
-    ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
-
-
-
-emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
-emptySingleLinkedStack = record {top = Nothing}
-
------
--- 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)
-...                  | (Just _) = True
-...                  | Nothing  = False
-
-
-test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
-test02 stack = popSingleLinkedStack stack test01
-
-test03 : {n : Level } {a : Set n} -> a ->  Bool
-test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
-
--- after a push and a pop, the stack is empty
-lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
-lemma = refl
-
-testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
-testStack01 v = pushStack createSingleLinkedStack v (
-   \s -> popStack s (\s1 d1 -> True))
-
--- after push 1 and 2, pop2 get 1 and 2
-
-testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
-testStack02 cs = pushStack createSingleLinkedStack 1 (
-   \s -> pushStack s 2 cs)
-
-
-testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
-testStack031 2 1 = True
-testStack031 _ _ = False
-
-testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
-testStack032  (Just d1) (Just d2) = testStack031 d1 d2
-testStack032  _ _ = False
-
-testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
-testStack03 s cs = pop2Stack s (
-   \s d1 d2 -> cs d1 d2 )
-
-testStack04 : Bool
-testStack04 = testStack02 (\s -> testStack03 s testStack032)
-
-testStack05 : testStack04 ≡ True
-testStack05 = refl
-
-------
---
--- 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 use stack s ≡ stack s3 is ok.
---    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 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
-id a = a
-
--- push a, n times
-
-n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
-n-push zero s            = s
-n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) 
-
-n-pop :  {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
-n-pop zero    s         = s
-n-pop  {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
-
-open ≡-Reasoning
-
-push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
-push-pop-equiv s = refl
-
-push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {_} {A} {a} n s
-push-and-n-pop zero s            = refl
-push-and-n-pop {_} {A} {a} (suc n) s = begin
-   n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
-  ≡⟨ refl ⟩
-   popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
-  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ 
-   popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
-  ≡⟨ refl ⟩
-    n-pop {_} {A} {a} (suc n) s
-  ∎
-  
-
-n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s
-n-push-pop-equiv zero s            = refl
-n-push-pop-equiv {_} {A} {a} (suc n) s = begin
-    n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
-  ≡⟨ refl ⟩
-    n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
-  ≡⟨ push-and-n-pop n (n-push n s)  ⟩
-    n-pop {_} {A} {a} n (n-push n s)
-  ≡⟨ n-push-pop-equiv n s ⟩
-    s
-  ∎
-
-
-n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
-n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack