|
1
|
1 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
|
|
|
2 singleLinkedStackSpec = record {
|
|
|
3 push = pushSingleLinkedStack
|
|
|
4 ; pop = popSingleLinkedStack
|
|
|
5 ; pop2 = pop2SingleLinkedStack
|
|
|
6 ; get = getSingleLinkedStack
|
|
|
7 ; get2 = get2SingleLinkedStack
|
|
|
8 ; clear = clearSingleLinkedStack
|
|
|
9 }
|
|
|
10
|
|
|
11 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
|
|
|
12 createSingleLinkedStack = record {
|
|
|
13 stack = emptySingleLinkedStack ;
|
|
|
14 stackMethods = singleLinkedStackSpec
|
|
|
15 }
|
|
|
16
|
|
|
17 -- Implementation
|
|
|
18
|
|
|
19 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
|
|
|
20 pushSingleLinkedStack stack datum next = next stack1
|
|
|
21 where
|
|
|
22 element = cons datum (top stack)
|
|
|
23 stack1 = record {top = Just element}
|
|
|
24
|
|
|
25
|
|
|
26 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
|
|
|
27 popSingleLinkedStack stack cs with (top stack)
|
|
|
28 ... | Nothing = cs stack Nothing
|
|
|
29 ... | Just d = cs stack1 (Just data1)
|
|
|
30 where
|
|
|
31 data1 = datum d
|
|
|
32 stack1 = record { top = (next d) }
|
|
|
33
|
|
|
34 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
|
|
|
35 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
|
|
|
36 ... | Nothing = cs stack Nothing Nothing
|
|
|
37 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
|
|
|
38 where
|
|
|
39 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
|
|
|
40 pop2SingleLinkedStack' stack cs with (next d)
|
|
|
41 ... | Nothing = cs stack Nothing Nothing
|
|
|
42 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
|
|
|
43
|
|
|
44
|
|
|
45 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
|
|
|
46 getSingleLinkedStack stack cs with (top stack)
|
|
|
47 ... | Nothing = cs stack Nothing
|
|
|
48 ... | Just d = cs stack (Just data1)
|
|
|
49 where
|
|
|
50 data1 = datum d
|
|
|
51
|
|
|
52 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
|
|
|
53 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
|
|
|
54 ... | Nothing = cs stack Nothing Nothing
|
|
|
55 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
|
|
|
56 where
|
|
|
57 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
|
|
|
58 get2SingleLinkedStack' stack cs with (next d)
|
|
|
59 ... | Nothing = cs stack Nothing Nothing
|
|
|
60 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
|
|
|
61
|
|
|
62 clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
|
|
|
63 clearSingleLinkedStack stack next = next (record {top = Nothing})
|
