|
0
|
1 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
|
|
|
2 pushSingleLinkedStack stack datum next = next stack1
|
|
|
3 where
|
|
|
4 element = cons datum (top stack)
|
|
|
5 stack1 = record {top = Just element}
|
|
|
6
|
|
|
7 -- Basic stack implementations are specifications of a Stack
|
|
|
8
|
|
|
9 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
|
|
|
10 singleLinkedStackSpec = record {
|
|
|
11 push = pushSingleLinkedStack
|
|
|
12 ; pop = popSingleLinkedStack
|
|
|
13 }
|
|
|
14
|
|
|
15 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
|
|
|
16 createSingleLinkedStack = record {
|
|
|
17 stack = emptySingleLinkedStack ;
|
|
|
18 tackMethods = singleLinkedStackSpec
|
|
|
19 }
|
