annotate src/parallel_execution/stack.agda @ 155:19cc626943e4

stack.agda
author atton
date Tue, 15 Nov 2016 19:33:13 +0900 (2016-11-15)
parents efef5d4df54f
children 0aa2265660a0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
1 module stack where
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
2
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
3 record Stack {a : Set} (stackImpl : Set a) where
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
4 stack : stackImpl
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
5 push : stackImpl -> a -> (stackImpl -> T) -> T
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
6 pop : stackImpl -> (stackImpl -> maybe a -> T) -> T
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
7
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
8
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
9 createSingleLinkedStack : Stack (SingleLinkedStack {a})
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
10 createSingleLinkedStack = record {
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
11 stack = record { top = nothing;}
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
12 push = pushSingleLinkedStack;
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
13 pop = popSingleLinkedStack;
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
14 }
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
15
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
16
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
17 record Element {a : Set} : Set where
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
18 data : a
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
19 next : Maybe (Element a)
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
20
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
21 record SingleLinkedStack {a : Set} : Set where
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
22 top : Maybe (Element a)
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
23
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
24 pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> T) -> T
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
25 pushSingleLinkedStack stack data next = next stack1
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
26 where
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
27 element = record {next = top stack; data = data}
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
28 stack1 = record {top = just element}
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
29
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
30
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
31 popSingleLinkedStack : {a : Set} -> Maybe a -> Data -> (Code : Stack -> (Maybe a) -> T) -> T
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
32 popSingleLinkedStack stack data next with (top stack) =
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
33 ... | nothing = next stack nothing
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
34 ... | just a = next stack1 data1
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
35 where
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
36 data1 = data a
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
37 stack1 = record { top = (next a)}