Mercurial > hg > Members > atton > agda-proofs

changeset 28:67978ba63a6f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rewrite cs composition style
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 10:43:23 +0000
parents 892f8b3aa57e
children b8e606ab3a0b
files cbc/stack-product.agda
diffstat 1 files changed, 9 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- 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
+
 
 
 {-