7
|
1 -- Implementation
|
|
2 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
|
|
3 pushSingleLinkedStack stack datum next = next stack1
|
|
4 where
|
|
5 element = cons datum (top stack)
|
|
6 stack1 = record {top = Just element}
|
|
7
|
|
8
|
|
9 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
|
|
10 popSingleLinkedStack stack cs with (top stack)
|
|
11 ... | Nothing = cs stack Nothing
|
|
12 ... | Just d = cs stack1 (Just data1)
|
|
13 where
|
|
14 data1 = datum d
|
|
15 stack1 = record { top = (next d) }
|