Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-product.agda @ 27:892f8b3aa57e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ReWrite stack.agda using product type definition
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 10:20:05 +0000
parents
children 67978ba63a6f
comparison
equal deleted inserted replaced
26:d503a73186ce 27:892f8b3aa57e
1 module stack-product where
2
3 open import product
4 open import Data.Product
5 open import Relation.Binary.PropositionalEquality
6
7 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
8 goto = executeCS
9
10 data Bool : Set where
11 True : Bool
12 False : Bool
13
14 data Maybe (a : Set) : Set where
15 Nothing : Maybe a
16 Just : a -> Maybe a
17
18
19 record Stack {a t : Set} (stackImpl : Set) : Set where
20 field
21 stack : stackImpl
22 push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t
23 pop : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t
24
25
26 data Element (a : Set) : Set where
27 cons : a -> Maybe (Element a) -> Element a
28
29 datum : {a : Set} -> Element a -> a
30 datum (cons a _) = a
31
32 next : {a : Set} -> Element a -> Maybe (Element a)
33 next (cons _ n) = n
34
35 record SingleLinkedStack (a : Set) : Set where
36 field
37 top : Maybe (Element a)
38 open SingleLinkedStack
39
40 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
41 emptySingleLinkedStack = record {top = Nothing}
42
43
44
45
46 pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t
47 pushSingleLinkedStack = cs push
48 where
49 push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t
50 push (stack , datum , next) = goto next stack1
51 where
52 element = cons datum (top stack)
53 stack1 = record {top = Just element}
54
55 popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) t
56 popSingleLinkedStack = cs pop
57 where
58 pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t
59 pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing)
60 pop (record { top = Just x } , nextCS) = goto nextCS (stack1 , (Just datum1))
61 where
62 datum1 = datum x
63 stack1 = record { top = (next x) }
64
65
66
67
68
69 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
70 createSingleLinkedStack = record { stack = emptySingleLinkedStack
71 ; push = pushSingleLinkedStack
72 ; pop = popSingleLinkedStack
73 }
74
75
76
77
78 test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool
79 test01 = cs test01'
80 where
81 test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool
82 test01' (record { top = Nothing } , _) = False
83 test01' (record { top = Just x } , _) = True
84
85
86 test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) Bool
87 test02 = cs test02'
88 where
89 test02' : {a : Set} -> SingleLinkedStack a -> Bool
90 test02' stack = goto popSingleLinkedStack (stack , test01)
91
92
93 test03 : {a : Set} -> CodeSegment a Bool
94 test03 = cs test03'
95 where
96 test03' : {a : Set} -> a -> Bool
97 test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , test02)
98
99
100 lemma : {A : Set} {a : A} -> goto test03 a ≡ False
101 lemma = refl
102
103 id : {A : Set} -> A -> A
104 id a = a
105
106
107 {-
108
109 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
110 n-push zero s = s
111 n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s)
112
113 n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
114 n-pop zero s = s
115 n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s)
116
117 open ≡-Reasoning
118
119 push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
120 push-pop-equiv s = refl
121
122 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
123 push-and-n-pop zero s = refl
124 push-and-n-pop {A} {a} (suc n) s = begin
125 n-pop (suc (suc n)) (pushSingleLinkedStack s a id)
126 ≡⟨ refl ⟩
127 popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
128 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩
129 popSingleLinkedStack (n-pop n s) (\s _ -> s)
130 ≡⟨ refl ⟩
131 n-pop (suc n) s
132 ∎
133
134
135 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
136 n-push-pop-equiv zero s = refl
137 n-push-pop-equiv {A} {a} (suc n) s = begin
138 n-pop (suc n) (n-push (suc n) s)
139 ≡⟨ refl ⟩
140 n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
141 ≡⟨ push-and-n-pop n (n-push n s) ⟩
142 n-pop n (n-push n s)
143 ≡⟨ n-push-pop-equiv n s ⟩
144 s
145 ∎
146
147
148 n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack
149 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
150 -}
151