--- a/src/parallel_execution/stack.agda	Thu Jan 16 15:11:11 2020 +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