Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/stack-product.agda @ 2:c7acb9211784

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