0 | module ImplicitCatenableDeque
2 | import CatenableDeque
7 | interface Sized (d : Type -> Type) where
12 | data ImplicitCatDeque : (Type -> Type) -> Type -> Type where
13 | Shallow : d a -> ImplicitCatDeque d a
14 | Deep : d a -> Lazy (ImplicitCatDeque d (CmpdElem d a)) -> d a
15 | -> Lazy (ImplicitCatDeque d (CmpdElem d a)) -> d a
16 | -> ImplicitCatDeque d a
18 | data CmpdElem : (Type -> Type) -> Type -> Type where
19 | Simple : d a -> CmpdElem d a
20 | Cmpd : d a -> Lazy (ImplicitCatDeque d (CmpdElem d a)) -> d a
23 | dappendL : {d : Type -> Type} -> Deque d => d a -> d a -> d a
25 | if isEmpty d1 then d2 else dappendL (assert_smaller d1 $
init d1) (cons (last d1) d2)
27 | dappendR : {d : Type -> Type} -> Deque d => d a -> d a -> d a
29 | if isEmpty d2 then d1 else dappendR (snoc d1 (head d2)) $
assert_smaller d2 (tail d2)
31 | replaceHead : {d : Type -> Type} -> Deque d => a -> ImplicitCatDeque d a -> ImplicitCatDeque d a
32 | replaceHead x (Shallow d) = Shallow (cons x (tail d))
33 | replaceHead x (Deep f a m b r) = Deep (cons x (tail f)) a m b r
35 | replaceLast : {d : Type -> Type} -> Deque d => ImplicitCatDeque d a -> a -> ImplicitCatDeque d a
36 | replaceLast (Shallow d) x = Shallow (snoc (init d) x)
37 | replaceLast (Deep f a m b r) x = Deep f a m b (snoc (init r) x)
39 | share : {d : Type -> Type} -> Deque d => d a -> d a -> (d a, d a, d a)
40 | share f r = let m = cons (last f) (cons (head r) empty) in (init f, m, tail r)
44 | {d : Type -> Type} -> (Deque d, Sized d) => Deque (ImplicitCatDeque d) where
45 | empty = Shallow empty
46 | isEmpty (Shallow d) = isEmpty d
49 | cons x (Shallow d) = Shallow (cons x d)
50 | cons x (Deep f a m b r) = Deep (cons x f) a m b r
52 | head (Shallow d) = head d
53 | head (Deep f a m b r) = head f
55 | tail (Shallow d) = Shallow (tail d)
56 | tail (Deep f a m b r) = assert_total $
57 | if size f > 3 then Deep (tail f) a m b r
58 | else if not (isEmpty a) then
60 | (Simple d) => let f' = dappendL (tail f) d
61 | in Deep f' (tail a) m b r
62 | (Cmpd f' c' r') => let f'' = dappendL (tail f) f'
63 | a'' = c' ++ replaceHead (Simple r') a
64 | in Deep f'' a'' m b r
65 | else if not (isEmpty b) then
67 | (Simple d) => let f' = dappendL (tail f) m
68 | in Deep f' empty d (tail b) r
69 | (Cmpd f' c' r') => let f'' = dappendL (tail f) m
70 | a'' = cons (Simple f') c'
71 | in Deep f'' a'' r' (tail b) r
72 | else Shallow (dappendL (tail f) m) ++ Shallow r
74 | snoc (Shallow d) x = Shallow (snoc d x)
75 | snoc (Deep f a m b r) x = Deep f a m b (snoc r x)
77 | last (Shallow d) = last d
78 | last (Deep f a m b r) = last r
80 | init (Shallow d) = Shallow (init d)
81 | init (Deep f a m b r) = assert_total $
82 | if size r > 3 then Deep f a m b (init r)
83 | else if not (isEmpty b) then
85 | (Simple d) => let r' = dappendR d (init r)
86 | in Deep f a m (init b) r'
87 | (Cmpd f' c' r') => let r'' = dappendR r' (init r)
88 | b'' = replaceLast b (Simple f') ++ c'
89 | in Deep f a m b'' r''
90 | else if not (isEmpty a) then
92 | (Simple d) => let r' = dappendR m (init r)
93 | in Deep f (init a) d empty r'
94 | (Cmpd f' c' r') => let r'' = dappendR m (init r)
95 | b'' = snoc c' (Simple r')
96 | in Deep f (init a) f' b'' r''
97 | else Shallow f ++ Shallow (dappendR m (init r))
100 | {d : Type -> Type} -> (Deque d, Sized d) => CatenableDeque (ImplicitCatDeque d) where
101 | (Shallow d1) ++ (Shallow d2) =
102 | if size d1 < 4 then Shallow (dappendL d1 d2)
103 | else if size d2 < 4 then Shallow (dappendR d1 d2)
104 | else let (f, m, r) = share d1 d2 in Deep f empty m empty r
105 | (Shallow d) ++ (Deep f a m b r) =
106 | if size d < 4 then Deep (dappendL d f) a m b r
107 | else Deep d (cons (Simple f) a) m b r
108 | (Deep f a m b r) ++ (Shallow d) =
109 | if size d < 4 then Deep f a m b (dappendR r d)
110 | else Deep f a m (snoc b (Simple r)) d
111 | (Deep f1 a1 m1 b1 r1) ++ (Deep f2 a2 m2 b2 r2) =
112 | let (r1', m, f2') = share r1 f2
113 | a1' = snoc a1 (Cmpd m1 b1 r1')
114 | b2' = cons (Cmpd f2' a2 m2) b2
115 | in Deep f1 a1' m b2' r2