|
2
|
1 record Element {l : Level} (a : Set l) : Set l where
|
|
|
2 inductive
|
|
|
3 constructor cons
|
|
|
4 field
|
|
|
5 datum : a -- `data` is reserved by Agda.
|
|
|
6 next : Maybe (Element a)
|
|
|
7 open Element
|
|
|
8
|
|
|
9 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
|
|
|
10 field
|
|
|
11 top : Maybe (Element a)
|
|
|
12 open SingleLinkedStack
|
|
|
13
|
|
|
14 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
|
|
|
15 pushSingleLinkedStack stack datum next = next stack1
|
|
|
16 where
|
|
|
17 element = cons datum (top stack)
|
|
|
18 stack1 = record {top = Just element}
|
|
|
19
|
|
|
20 -- push 以下は省略
|
|
|
21
|
|
|
22 -- Basic stack implementations are specifications of a Stack
|
|
|
23
|
|
|
24 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
|
|
|
25 singleLinkedStackSpec = record {
|
|
|
26 push = pushSingleLinkedStack
|
|
|
27 ; pop = popSingleLinkedStack
|
|
|
28 ; pop2 = pop2SingleLinkedStack
|
|
|
29 ; get = getSingleLinkedStack
|
|
|
30 ; get2 = get2SingleLinkedStack
|
|
|
31 ; clear = clearSingleLinkedStack
|
|
|
32 }
|
|
|
33
|
|
|
34 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
|
|
|
35 createSingleLinkedStack = record {
|
|
|
36 stack = emptySingleLinkedStack ;
|
|
|
37 stackMethods = singleLinkedStackSpec
|
|
|
38 }
|
