# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482488405 0
# Node ID 892f8b3aa57eb61ccb82506ad326f470015b069f
# Parent  d503a73186ceb4e3378989fc026f4725c91b8144
ReWrite stack.agda using product type definition

diff -r d503a73186ce -r 892f8b3aa57e cbc/product.agda
--- a/cbc/product.agda	Fri Dec 23 02:50:03 2016 +0000
+++ b/cbc/product.agda	Fri Dec 23 10:20:05 2016 +0000
@@ -6,7 +6,7 @@
 open import Function using (_∘_ ; id)
 open import Data.Unit
 
-data CodeSegment (I O : Set) : Set₁ where
+data CodeSegment (I O : Set) : Set where
   cs : (I -> O) -> CodeSegment I O
 
 
diff -r d503a73186ce -r 892f8b3aa57e cbc/stack-product.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/stack-product.agda	Fri Dec 23 10:20:05 2016 +0000
@@ -0,0 +1,151 @@
+module stack-product where
+
+open import product
+open import Data.Product
+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 -> Maybe a
+
+
+record Stack {a t : Set} (stackImpl : Set) : Set  where
+  field
+    stack : stackImpl
+    push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t
+    pop  : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t
+
+
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+
+
+
+pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t
+pushSingleLinkedStack = cs push
+  where
+    push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t
+    push (stack , datum , next) = goto next stack1
+      where
+        element = cons datum (top stack)
+        stack1  = record {top = Just element}
+
+popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t))  t
+popSingleLinkedStack = cs pop
+  where
+    pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> 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} -> Stack {a} {b} (SingleLinkedStack a)
+createSingleLinkedStack = record { stack = emptySingleLinkedStack
+                                 ; push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 }
+
+
+
+
+test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool
+test01 = cs test01'
+  where
+    test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool
+    test01' (record { top = Nothing } , _) = False
+    test01' (record { top = Just x } ,  _)  = True
+
+
+test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) Bool
+test02 = cs test02'
+  where
+    test02' : {a  : Set} -> SingleLinkedStack a -> Bool
+    test02' stack = goto popSingleLinkedStack (stack , test01)
+
+
+test03 : {a : Set} -> CodeSegment a Bool
+test03  = cs test03'
+  where
+    test03' : {a : Set} -> a -> Bool
+    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , test02)
+
+
+lemma : {A : Set} {a : A} -> goto test03 a ≡ False
+lemma = refl
+
+id : {A : Set} -> A -> A
+id a = a
+
+
+{-
+
+n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-push zero s            = s
+n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s)
+
+n-pop : {A : Set} {a : A} -> Nat -> 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 : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
+push-pop-equiv s = refl
+
+push-and-n-pop : {A : Set} {a : A} (n : Nat) (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 (suc (suc n)) (pushSingleLinkedStack s a id)
+  ≡⟨ refl ⟩
+  popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
+  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩
+  popSingleLinkedStack (n-pop n s) (\s _ -> s)
+  ≡⟨ refl ⟩
+  n-pop (suc n) s
+  ∎
+
+
+n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (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 (suc n) (n-push (suc n) s)
+  ≡⟨ refl ⟩
+  n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
+  ≡⟨ push-and-n-pop n (n-push n s)  ⟩
+  n-pop n (n-push n s)
+  ≡⟨ n-push-pop-equiv n s ⟩
+  s
+  ∎
+
+
+n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
+n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
+-}
+