0 | module SimpleCatenableDeque
2 | import CatenableDeque
7 | data SimpleCatDeque : (Type -> Type) -> Type -> Type where
8 | Shallow : d a -> SimpleCatDeque d a
9 | Deep : d a -> Lazy (SimpleCatDeque d (d a)) -> d a -> SimpleCatDeque d a
11 | tooSmall : {d : Type -> Type} -> Deque d => d a -> Bool
12 | tooSmall d = isEmpty d || isEmpty (tail d)
14 | dappendL : {d : Type -> Type} -> Deque d => d a -> d a -> d a
15 | dappendL d1 d2 = if isEmpty d1 then d2 else cons (head d1) d2
17 | dappendR : {d : Type -> Type} -> Deque d => d a -> d a -> d a
18 | dappendR d1 d2 = if isEmpty d2 then d1 else snoc d1 (head d2)
21 | {d : Type -> Type} -> Deque d => Deque (SimpleCatDeque d) where
22 | empty = Shallow empty
23 | isEmpty (Shallow d) = isEmpty d
26 | cons x (Shallow d) = Shallow (cons x d)
27 | cons x (Deep f m r) = Deep (cons x f) m r
29 | head (Shallow d) = head d
30 | head (Deep f m r) = head f
32 | tail (Shallow d) = Shallow (tail d)
33 | tail (Deep f m r) = let f' = tail f in
34 | if not (tooSmall f') then Deep f' m r
35 | else if isEmpty m then Shallow (dappendL f' r)
36 | else Deep (dappendL f' (head m)) (tail m) r
38 | snoc (Shallow d) x = Shallow (snoc d x)
39 | snoc (Deep f m r) x = Deep f m (snoc r x)
41 | last (Shallow d) = last d
42 | last (Deep f m r) = last r
44 | init (Shallow d) = Shallow (init d)
45 | init (Deep f m r) = let r' = init r in
46 | if not (tooSmall r') then Deep f m r'
47 | else if isEmpty m then Shallow (dappendR f r')
48 | else Deep f (init m) (dappendR (last m) r')
51 | {d : Type -> Type} -> Deque d => CatenableDeque (SimpleCatDeque d) where
52 | (Shallow d1) ++ (Shallow d2) =
53 | if tooSmall d1 then Shallow (dappendL d1 d2)
54 | else if tooSmall d2 then Shallow (dappendR d1 d2)
55 | else Deep d1 empty d2
56 | (Shallow d) ++ (Deep f m r) =
57 | if tooSmall d then Deep (dappendL d f) m r
58 | else Deep d (cons f m) r
59 | (Deep f m r) ++ (Shallow d) =
60 | if tooSmall d then Deep f m (dappendR r d)
61 | else Deep f (snoc m r) d
62 | (Deep f1 m1 r1) ++ (Deep f2 m2 r2) =
63 | let mf = assert_smaller (Deep f1 m1 r2) $
snoc m1 r1
64 | mr = assert_smaller (Deep f2 m2 r2) $
cons f2 m2
65 | in Deep f1 (mf ++ mr) r2