|
1
|
1 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
|
|
|
2 field
|
|
|
3 top : Maybe (Element a)
|
|
|
4 open SingleLinkedStack
|
|
|
5
|
|
3
|
6 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
1
|
7 pushSingleLinkedStack stack datum next = next stack1
|
|
|
8 where
|
|
|
9 element = cons datum (top stack)
|
|
|
10 stack1 = record {top = Just element}
|
|
|
11
|
|
|
12 -- Basic stack implementations are specifications of a Stack
|
|
|
13
|
|
3
|
14 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
|
|
1
|
15 singleLinkedStackSpec = record {
|
|
|
16 push = pushSingleLinkedStack
|
|
|
17 ; pop = popSingleLinkedStack
|
|
|
18 ; pop2 = pop2SingleLinkedStack
|
|
|
19 ; get = getSingleLinkedStack
|
|
|
20 ; get2 = get2SingleLinkedStack
|
|
|
21 ; clear = clearSingleLinkedStack
|
|
|
22 }
|
|
|
23
|
|
3
|
24 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
|
|
1
|
25 createSingleLinkedStack = record {
|
|
|
26 stack = emptySingleLinkedStack ;
|
|
|
27 stackMethods = singleLinkedStackSpec
|
|
|
28 }
|
