comparison cbc/stack-product.agda @ 28:67978ba63a6f

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
comparison
equal deleted inserted replaced
27:892f8b3aa57e 28:67978ba63a6f
1 module stack-product where 1 module stack-product where
2 2
3 open import product 3 open import product
4 open import Data.Product 4 open import Data.Product
5 open import Function using (id)
5 open import Relation.Binary.PropositionalEquality 6 open import Relation.Binary.PropositionalEquality
6 7
7 -- definition based from Gears(209:5708390a9d88) src/parallel_execution 8 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
8 goto = executeCS 9 goto = executeCS
9 10
81 test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool 82 test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool
82 test01' (record { top = Nothing } , _) = False 83 test01' (record { top = Nothing } , _) = False
83 test01' (record { top = Just x } , _) = True 84 test01' (record { top = Just x } , _) = True
84 85
85 86
86 test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) Bool 87 test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a)
87 test02 = cs test02' 88 test02 = cs test02'
88 where 89 where
89 test02' : {a : Set} -> SingleLinkedStack a -> Bool 90 test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a)
90 test02' stack = goto popSingleLinkedStack (stack , test01) 91 test02' stack = goto popSingleLinkedStack (stack , (cs id))
91 92
92 93
93 test03 : {a : Set} -> CodeSegment a Bool 94 test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a)
94 test03 = cs test03' 95 test03 = cs test03'
95 where 96 where
96 test03' : {a : Set} -> a -> Bool 97 test03' : {a : Set} -> a -> SingleLinkedStack a
97 test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , test02) 98 test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id))
98 99
99 100
100 lemma : {A : Set} {a : A} -> goto test03 a ≡ False 101 lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False
101 lemma = refl 102 lemma = refl
102 103
103 id : {A : Set} -> A -> A 104
104 id a = a
105 105
106 106
107 {- 107 {-
108 108
109 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A 109 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A