--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/stack-product.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,158 @@
+module stack-product where
+
+open import product
+open import Data.Product
+open import Data.Nat
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality
+
+-- definition based from Gears(209:5708390a9d88) src/parallel_execution
+goto = executeCS
+
+data Bool : Set where
+  True  : Bool
+  False : Bool
+
+data Maybe (a : Set) : Set  where
+  Nothing : Maybe a
+  Just    : a @$\rightarrow$@ Maybe a
+
+
+record Stack {a t : Set} (stackImpl : Set) : Set  where
+  field
+    stack : stackImpl
+    push : CodeSegment (stackImpl @$\times$@ a @$\times$@ (CodeSegment stackImpl t)) t
+    pop  : CodeSegment (stackImpl @$\times$@ (CodeSegment (stackImpl @$\times$@ Maybe a) t)) t
+
+
+data Element (a : Set) : Set where
+  cons : a @$\rightarrow$@ Maybe (Element a) @$\rightarrow$@ Element a
+
+datum : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ a
+datum (cons a _) = a
+
+next : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+emptySingleLinkedStack : {a : Set} @$\rightarrow$@ SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+
+
+
+pushSingleLinkedStack : {a t : Set} @$\rightarrow$@ CodeSegment ((SingleLinkedStack a) @$\times$@ a @$\times$@ (CodeSegment (SingleLinkedStack a) t)) t
+pushSingleLinkedStack = cs push
+  where
+    push : {a t : Set} @$\rightarrow$@ ((SingleLinkedStack a) @$\times$@ a @$\times$@ (CodeSegment (SingleLinkedStack a) t)) @$\rightarrow$@ t
+    push (stack , datum , next) = goto next stack1
+      where
+        element = cons datum (top stack)
+        stack1  = record {top = Just element}
+
+popSingleLinkedStack : {a t : Set} @$\rightarrow$@ CodeSegment (SingleLinkedStack a @$\times$@ (CodeSegment (SingleLinkedStack a @$\times$@ Maybe a) t))  t
+popSingleLinkedStack = cs pop
+  where
+    pop : {a t : Set} @$\rightarrow$@ (SingleLinkedStack a @$\times$@ (CodeSegment (SingleLinkedStack a @$\times$@ Maybe a) t)) @$\rightarrow$@ t
+    pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) 
+    pop (record { top = Just x } , nextCS)  = goto nextCS (stack1 , (Just datum1))
+      where
+        datum1 = datum x
+        stack1 = record { top = (next x) }
+
+
+
+
+
+createSingleLinkedStack : {a b : Set} @$\rightarrow$@ Stack {a} {b} (SingleLinkedStack a)
+createSingleLinkedStack = record { stack = emptySingleLinkedStack
+                                 ; push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 }
+
+
+
+
+test01 : {a : Set} @$\rightarrow$@ CodeSegment (SingleLinkedStack a @$\times$@ Maybe a) Bool
+test01 = cs test01'
+  where
+    test01' : {a : Set} @$\rightarrow$@ (SingleLinkedStack a @$\times$@ Maybe a) @$\rightarrow$@ Bool
+    test01' (record { top = Nothing } , _) = False
+    test01' (record { top = Just x } ,  _)  = True
+
+
+test02 : {a : Set} @$\rightarrow$@ CodeSegment (SingleLinkedStack a) (SingleLinkedStack a @$\times$@ Maybe a)
+test02 = cs test02'
+  where
+    test02' : {a : Set} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\times$@ Maybe a)
+    test02' stack = goto popSingleLinkedStack (stack , (cs id))
+
+
+test03 : {a : Set} @$\rightarrow$@ CodeSegment a (SingleLinkedStack a)
+test03  = cs test03'
+  where
+    test03' : {a : Set} @$\rightarrow$@ a @$\rightarrow$@ SingleLinkedStack a
+    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id))
+
+
+lemma : {A : Set} {a : A} @$\rightarrow$@ goto (test03 ◎ test02 ◎ test01) a @$\equiv$@ False
+lemma = refl
+
+
+n-push : {A : Set} {a : A} @$\rightarrow$@ CodeSegment (@$\mathbb{N}$@  @$\times$@ SingleLinkedStack A) (@$\mathbb{N}$@ @$\times$@ SingleLinkedStack A)
+n-push {A} {a} = cs (push {A} {a})
+  where
+    push : {A : Set} {a : A} @$\rightarrow$@ (@$\mathbb{N}$@ @$\times$@ SingleLinkedStack A) @$\rightarrow$@ (@$\mathbb{N}$@ @$\times$@ SingleLinkedStack A)
+    push {A} {a} (zero  , s) = (zero , s)
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
+
+
+{-
+
+n-push : {A : Set} {a : A} @$\rightarrow$@ Nat @$\rightarrow$@ SingleLinkedStack A @$\rightarrow$@ SingleLinkedStack A
+n-push zero s            = s
+n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s @$\rightarrow$@ s)
+
+n-pop : {A : Set} {a : A} @$\rightarrow$@ Nat @$\rightarrow$@ SingleLinkedStack A @$\rightarrow$@ SingleLinkedStack A
+n-pop zero    s         = s
+n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ @$\rightarrow$@ s)
+
+open @$\equiv$@-Reasoning
+
+push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) @$\rightarrow$@ popSingleLinkedStack (pushSingleLinkedStack s a (\s @$\rightarrow$@ s)) (\s _ @$\rightarrow$@ s) @$\equiv$@ s
+push-pop-equiv s = refl
+
+push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) @$\rightarrow$@ n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) @$\equiv$@ 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 (suc (suc n)) (pushSingleLinkedStack s a id)
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ @$\rightarrow$@ s)
+  @$\equiv$@@$\langle$@ cong (\s @$\rightarrow$@ popSingleLinkedStack s (\s _ @$\rightarrow$@ s)) (push-and-n-pop n s) @$\rangle$@
+  popSingleLinkedStack (n-pop n s) (\s _ @$\rightarrow$@ s)
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  n-pop (suc n) s
+  @$\blacksquare$@
+
+
+n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) @$\rightarrow$@ (n-pop {A} {a} n (n-push {A} {a} n s)) @$\equiv$@ s
+n-push-pop-equiv zero s            = refl
+n-push-pop-equiv {A} {a} (suc n) s = begin
+  n-pop (suc n) (n-push (suc n) s)
+  @$\equiv$@@$\langle$@ refl @$\rangle$@
+  n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s @$\rightarrow$@ s))
+  @$\equiv$@@$\langle$@ push-and-n-pop n (n-push n s)  @$\rangle$@
+  n-pop n (n-push n s)
+  @$\equiv$@@$\langle$@ n-push-pop-equiv n s @$\rangle$@
+  s
+  @$\blacksquare$@
+
+
+n-push-pop-equiv-empty : {A : Set} {a : A} @$\rightarrow$@ (n : Nat) @$\rightarrow$@ n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  @$\equiv$@ emptySingleLinkedStack
+n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
+-}
+