154
|
1 module stack where
|
|
2
|
155
|
3 record Stack {a : Set} (stackImpl : Set a) where
|
|
4 stack : stackImpl
|
|
5 push : stackImpl -> a -> (stackImpl -> T) -> T
|
|
6 pop : stackImpl -> (stackImpl -> maybe a -> T) -> T
|
|
7
|
|
8
|
|
9 createSingleLinkedStack : Stack (SingleLinkedStack {a})
|
|
10 createSingleLinkedStack = record {
|
|
11 stack = record { top = nothing;}
|
|
12 push = pushSingleLinkedStack;
|
|
13 pop = popSingleLinkedStack;
|
|
14 }
|
|
15
|
|
16
|
|
17 record Element {a : Set} : Set where
|
|
18 data : a
|
|
19 next : Maybe (Element a)
|
|
20
|
|
21 record SingleLinkedStack {a : Set} : Set where
|
|
22 top : Maybe (Element a)
|
|
23
|
|
24 pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> T) -> T
|
154
|
25 pushSingleLinkedStack stack data next = next stack1
|
|
26 where
|
|
27 element = record {next = top stack; data = data}
|
|
28 stack1 = record {top = just element}
|
|
29
|
|
30
|
155
|
31 popSingleLinkedStack : {a : Set} -> Maybe a -> Data -> (Code : Stack -> (Maybe a) -> T) -> T
|
154
|
32 popSingleLinkedStack stack data next with (top stack) =
|
|
33 ... | nothing = next stack nothing
|
|
34 ... | just a = next stack1 data1
|
|
35 where
|
|
36 data1 = data a
|
|
37 stack1 = record { top = (next a)}
|