# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482489803 0
# Node ID 67978ba63a6f12503d2ea3188f3cd044c256efa4
# Parent  892f8b3aa57eb61ccb82506ad326f470015b069f
Rewrite cs composition style

diff -r 892f8b3aa57e -r 67978ba63a6f cbc/stack-product.agda
--- a/cbc/stack-product.agda	Fri Dec 23 10:20:05 2016 +0000
+++ b/cbc/stack-product.agda	Fri Dec 23 10:43:23 2016 +0000
@@ -2,6 +2,7 @@
 
 open import product
 open import Data.Product
+open import Function using (id)
 open import Relation.Binary.PropositionalEquality
 
 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
@@ -83,25 +84,24 @@
     test01' (record { top = Just x } ,  _)  = True
 
 
-test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) Bool
+test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a)
 test02 = cs test02'
   where
-    test02' : {a  : Set} -> SingleLinkedStack a -> Bool
-    test02' stack = goto popSingleLinkedStack (stack , test01)
+    test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a)
+    test02' stack = goto popSingleLinkedStack (stack , (cs id))
 
 
-test03 : {a : Set} -> CodeSegment a Bool
+test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a)
 test03  = cs test03'
   where
-    test03' : {a : Set} -> a -> Bool
-    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , test02)
+    test03' : {a : Set} -> a -> SingleLinkedStack a
+    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id))
 
 
-lemma : {A : Set} {a : A} -> goto test03 a ≡ False
+lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False
 lemma = refl
 
-id : {A : Set} -> A -> A
-id a = a
+
 
 
 {-