|
1
|
1 open import Level renaming (suc to succ ; zero to Zero )
|
|
|
2 module stack where
|
|
|
3
|
|
|
4 open import Relation.Binary.PropositionalEquality
|
|
|
5 open import Relation.Binary.Core
|
|
|
6 open import Data.Nat
|
|
|
7
|
|
|
8 ex : 1 + 2 @$\equiv$@ 3
|
|
|
9 ex = refl
|
|
|
10
|
|
|
11 data Bool {n : Level } : Set n where
|
|
|
12 True : Bool
|
|
|
13 False : Bool
|
|
|
14
|
|
|
15 record _@$\wedge$@_ {n : Level } (a : Set n) (b : Set n): Set n where
|
|
|
16 field
|
|
|
17 pi1 : a
|
|
|
18 pi2 : b
|
|
|
19
|
|
|
20 data Maybe {n : Level } (a : Set n) : Set n where
|
|
|
21 Nothing : Maybe a
|
|
|
22 Just : a @$\rightarrow$@ Maybe a
|
|
|
23
|
|
|
24 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
|
|
|
25 field
|
|
|
26 push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
27 pop : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
28 pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
29 get : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
30 get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
31 clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
32 open StackMethods
|
|
|
33
|
|
|
34 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where
|
|
|
35 field
|
|
|
36 stack : si
|
|
|
37 stackMethods : StackMethods {n} {m} a {t} si
|
|
|
38 pushStack : a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
39 pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
|
|
|
40 popStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
41 popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
|
|
|
42 pop2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
43 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
|
|
|
44 getStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
45 getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
|
|
|
46 get2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
47 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
|
|
|
48 clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
49 clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
|
|
|
50
|
|
|
51 open Stack
|
|
|
52
|
|
|
53 {--
|
|
|
54 data Element {n : Level } (a : Set n) : Set n where
|
|
|
55 cons : a @$\rightarrow$@ Maybe (Element a) @$\rightarrow$@ Element a
|
|
|
56
|
|
|
57
|
|
|
58 datum : {n : Level } {a : Set n} @$\rightarrow$@ Element a @$\rightarrow$@ a
|
|
|
59 datum (cons a _) = a
|
|
|
60
|
|
|
61 next : {n : Level } {a : Set n} @$\rightarrow$@ Element a @$\rightarrow$@ Maybe (Element a)
|
|
|
62 next (cons _ n) = n
|
|
|
63 --}
|
|
|
64
|
|
|
65
|
|
|
66 -- cannot define recrusive record definition. so use linked list with maybe.
|
|
|
67 record Element {l : Level} (a : Set l) : Set l where
|
|
|
68 inductive
|
|
|
69 constructor cons
|
|
|
70 field
|
|
|
71 datum : a -- `data` is reserved by Agda.
|
|
|
72 next : Maybe (Element a)
|
|
|
73
|
|
|
74 open Element
|
|
|
75
|
|
|
76
|
|
|
77 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
|
|
|
78 field
|
|
|
79 top : Maybe (Element a)
|
|
|
80 open SingleLinkedStack
|
|
|
81
|
|
|
82 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
83 pushSingleLinkedStack stack datum next = next stack1
|
|
|
84 where
|
|
|
85 element = cons datum (top stack)
|
|
|
86 stack1 = record {top = Just element}
|
|
|
87
|
|
|
88
|
|
|
89 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
90 popSingleLinkedStack stack cs with (top stack)
|
|
|
91 ... | Nothing = cs stack Nothing
|
|
|
92 ... | Just d = cs stack1 (Just data1)
|
|
|
93 where
|
|
|
94 data1 = datum d
|
|
|
95 stack1 = record { top = (next d) }
|
|
|
96
|
|
|
97 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
98 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
|
|
|
99 ... | Nothing = cs stack Nothing Nothing
|
|
|
100 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
|
|
|
101 where
|
|
|
102 pop2SingleLinkedStack' : {n m : Level } {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
103 pop2SingleLinkedStack' stack cs with (next d)
|
|
|
104 ... | Nothing = cs stack Nothing Nothing
|
|
|
105 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
|
|
|
106
|
|
|
107
|
|
|
108 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
109 getSingleLinkedStack stack cs with (top stack)
|
|
|
110 ... | Nothing = cs stack Nothing
|
|
|
111 ... | Just d = cs stack (Just data1)
|
|
|
112 where
|
|
|
113 data1 = datum d
|
|
|
114
|
|
|
115 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
116 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
|
|
|
117 ... | Nothing = cs stack Nothing Nothing
|
|
|
118 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
|
|
|
119 where
|
|
|
120 get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
121 get2SingleLinkedStack' stack cs with (next d)
|
|
|
122 ... | Nothing = cs stack Nothing Nothing
|
|
|
123 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
|
|
|
124
|
|
|
125 clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
126 clearSingleLinkedStack stack next = next (record {top = Nothing})
|
|
|
127
|
|
|
128
|
|
|
129 emptySingleLinkedStack : {n : Level } {a : Set n} @$\rightarrow$@ SingleLinkedStack a
|
|
|
130 emptySingleLinkedStack = record {top = Nothing}
|
|
|
131
|
|
|
132 -----
|
|
|
133 -- Basic stack implementations are specifications of a Stack
|
|
|
134 --
|
|
|
135 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
|
|
|
136 singleLinkedStackSpec = record {
|
|
|
137 push = pushSingleLinkedStack
|
|
|
138 ; pop = popSingleLinkedStack
|
|
|
139 ; pop2 = pop2SingleLinkedStack
|
|
|
140 ; get = getSingleLinkedStack
|
|
|
141 ; get2 = get2SingleLinkedStack
|
|
|
142 ; clear = clearSingleLinkedStack
|
|
|
143 }
|
|
|
144
|
|
|
145 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
|
|
|
146 createSingleLinkedStack = record {
|
|
|
147 stack = emptySingleLinkedStack ;
|
|
|
148 stackMethods = singleLinkedStackSpec
|
|
|
149 }
|
