Mercurial > hg > Members > atton > agda-proofs
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 |