|
574
|
1 open import Level renaming (suc to succ ; zero to Zero )
|
|
|
2 module Queue where
|
|
|
3
|
|
|
4 open import Relation.Binary.PropositionalEquality
|
|
|
5 open import Relation.Binary.Core
|
|
|
6 open import Data.Nat
|
|
|
7
|
|
|
8 data Maybe {n : Level } (a : Set n) : Set n where
|
|
|
9 Nothing : Maybe a
|
|
|
10 Just : a -> Maybe a
|
|
|
11
|
|
|
12 data Bool {n : Level }: Set n where
|
|
|
13 True : Bool
|
|
|
14 False : Bool
|
|
|
15
|
|
|
16
|
|
|
17 record QueueMethods {n m : Level} (a : Set n) {t : Set m} (queueImpl : Set n) : Set (m Level.⊔ n) where
|
|
|
18 field
|
|
|
19 put : queueImpl -> a -> (queueImpl -> t) -> t
|
|
|
20 take : queueImpl -> (queueImpl -> Maybe a -> t) -> t
|
|
|
21 clear : queueImpl -> (queueImpl -> t) -> t
|
|
|
22 open QueueMethods
|
|
|
23
|
|
|
24 record Queue {n m : Level} (a : Set n) {t : Set m} (qu : Set n) : Set (m Level.⊔ n) where
|
|
|
25 field
|
|
|
26 queue : qu
|
|
|
27 queueMethods : QueueMethods {n} {m} a {t} qu
|
|
|
28 putQueue : a -> (Queue a qu -> t) -> t
|
|
|
29 putQueue a next = put (queueMethods) (queue) a (\q1 -> next record {queue = q1 ; queueMethods = queueMethods})
|
|
|
30 takeQueue : (Queue a qu -> Maybe a -> t) -> t
|
|
|
31 takeQueue next = take (queueMethods) (queue) (\q1 d1 -> next record {queue = q1 ; queueMethods = queueMethods} d1)
|
|
|
32 clearQueue : (Queue a qu -> t) -> t
|
|
|
33 clearQueue next = clear (queueMethods) (queue) (\q1 -> next record {queue = q1 ; queueMethods = queueMethods})
|
|
|
34 open Queue
|
|
|
35
|
|
|
36
|
|
|
37
|
|
|
38 record Element {n : Level} (a : Set n) : Set n where
|
|
|
39 inductive
|
|
|
40 constructor cons
|
|
|
41 field
|
|
|
42 datum : a -- `data` is reserved by Agda.
|
|
|
43 next : Maybe (Element a)
|
|
|
44 open Element
|
|
|
45
|
|
|
46
|
|
|
47 record SingleLinkedQueue {n : Level} (a : Set n) : Set n where
|
|
|
48 field
|
|
|
49 top : Maybe (Element a)
|
|
|
50 last : Maybe (Element a)
|
|
|
51 open SingleLinkedQueue
|
|
|
52
|
|
|
53
|
|
|
54 {-# TERMINATING #-}
|
|
|
55 reverseElement : {n : Level} {a : Set n} -> Element a -> Maybe (Element a) -> Element a
|
|
|
56 reverseElement el Nothing with next el
|
|
|
57 ... | Just el1 = reverseElement el1 (Just rev)
|
|
|
58 where
|
|
|
59 rev = cons (datum el) Nothing
|
|
|
60 ... | Nothing = el
|
|
|
61 reverseElement el (Just el0) with next el
|
|
|
62 ... | Just el1 = reverseElement el1 (Just (cons (datum el) (Just el0)))
|
|
|
63 ... | Nothing = (cons (datum el) (Just el0))
|
|
|
64
|
|
|
65
|
|
|
66 {-# TERMINATING #-}
|
|
|
67 putSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> SingleLinkedQueue a -> a -> (Code : SingleLinkedQueue a -> t) -> t
|
|
|
68 putSingleLinkedQueue queue a cs with top queue
|
|
|
69 ... | Just te = cs queue1
|
|
|
70 where
|
|
|
71 re = reverseElement te Nothing
|
|
|
72 ce = cons a (Just re)
|
|
|
73 commit = reverseElement ce Nothing
|
|
|
74 queue1 = record queue {top = Just commit}
|
|
|
75 ... | Nothing = cs queue1
|
|
|
76 where
|
|
|
77 cel = record {datum = a ; next = Nothing}
|
|
|
78 queue1 = record {top = Just cel ; last = Just cel}
|
|
|
79
|
|
|
80 {-# TERMINATING #-}
|
|
|
81 takeSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> SingleLinkedQueue a -> (Code : SingleLinkedQueue a -> (Maybe a) -> t) -> t
|
|
|
82 takeSingleLinkedQueue queue cs with (top queue)
|
|
|
83 ... | Just te = cs record {top = (next te) ; last = Just (lastElement te)} (Just (datum te))
|
|
|
84 where
|
|
|
85 lastElement : {n : Level} {a : Set n} -> Element a -> Element a
|
|
|
86 lastElement el with next el
|
|
|
87 ... | Just el1 = lastElement el1
|
|
|
88 ... | Nothing = el
|
|
|
89 ... | Nothing = cs queue Nothing
|
|
|
90
|
|
|
91 clearSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> SingleLinkedQueue a -> (SingleLinkedQueue a -> t) -> t
|
|
|
92 clearSingleLinkedQueue queue cs = cs (record {top = Nothing ; last = Nothing})
|
|
|
93
|
|
|
94
|
|
|
95 emptySingleLinkedQueue : {n : Level} {a : Set n} -> SingleLinkedQueue a
|
|
|
96 emptySingleLinkedQueue = record {top = Nothing ; last = Nothing}
|
|
|
97
|
|
|
98 singleLinkedQueueSpec : {n m : Level } {t : Set m } {a : Set n} -> QueueMethods {n} {m} a {t} (SingleLinkedQueue a)
|
|
|
99 singleLinkedQueueSpec = record {
|
|
|
100 put = putSingleLinkedQueue
|
|
|
101 ; take = takeSingleLinkedQueue
|
|
|
102 ; clear = clearSingleLinkedQueue
|
|
|
103 }
|
|
|
104
|
|
|
105
|
|
|
106 createSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> Queue {n} {m} a {t} (SingleLinkedQueue a)
|
|
|
107 createSingleLinkedQueue = record {
|
|
|
108 queue = emptySingleLinkedQueue ;
|
|
|
109 queueMethods = singleLinkedQueueSpec
|
|
|
110 }
|
|
|
111
|
|
|
112
|
|
|
113 check1 = putSingleLinkedQueue emptySingleLinkedQueue 1 (\q1 -> putSingleLinkedQueue q1 2 (\q2 -> putSingleLinkedQueue q2 3 (\q3 -> putSingleLinkedQueue q3 4 (\q4 -> putSingleLinkedQueue q4 5 (\q5 -> q5)))))
|
|
|
114
|
|
|
115
|
|
|
116 check2 = putSingleLinkedQueue emptySingleLinkedQueue 1 (\q1 -> putSingleLinkedQueue q1 2 (\q2 -> putSingleLinkedQueue q2 3 (\q3 -> putSingleLinkedQueue q3 4 (\q4 -> takeSingleLinkedQueue q4 (\q d -> q)))))
|
|
|
117
|
|
|
118
|
|
|
119 test01 : {n : Level } {a : Set n} -> SingleLinkedQueue a -> Maybe a -> Bool {n}
|
|
|
120 test01 queue _ with (top queue)
|
|
|
121 ... | (Just _) = True
|
|
|
122 ... | Nothing = False
|
