@@ -1,6 +1,7 @@
11module Data.List.Views
22
33import Data.List
4+import Data.Nat.Views
45
56lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
67 length (xs ++ (y :: ys)) = S (length (xs ++ ys))
@@ -42,6 +43,7 @@ splitHelp head (x :: xs) (_ :: _ :: ys)
4243 SplitPair {xs} {ys} => SplitPair {xs = (x :: xs)} {ys = ys}
4344
4445||| Covering function for the `Split` view
46+||| Constructs the view in linear time
4547export
4648split : (xs : List a) -> Split xs
4749split [] = SplitNil
@@ -70,6 +72,7 @@ splitRecFix xs srec with (split xs)
7072 SplitRecPair left right
7173
7274||| Covering function for the `SplitRec` view
75+||| Constructs the view in O(n lg n)
7376export total
7477splitRec : (xs : List a) -> SplitRec xs
7578splitRec xs = accInd splitRecFix xs (smallerAcc xs)
@@ -87,6 +90,7 @@ snocListHelp {xs} x (y :: ys)
8790 = rewrite appendAssociative xs [y] ys in snocListHelp (Snoc x {x=y}) ys
8891
8992||| Covering function for the `SnocList` view
93+||| Constructs the view in linear time
9094export
9195snocList : (xs : List a) -> SnocList xs
9296snocList xs = snocListHelp Empty xs
@@ -107,6 +111,7 @@ filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filte
107111filteredROK p x xs = LTESucc (filterSmaller xs)
108112
109113||| Covering function for the `Filtered` view
114+||| Constructs the view in O(n lg n)
110115export
111116filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
112117filtered p inp with (smallerAcc inp)
@@ -115,3 +120,100 @@ filtered p inp with (smallerAcc inp)
115120 = FRec (Delay (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs)))
116121 (Delay (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs)))
117122
123+lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
124+lenImpossible {n = Z} _ Refl impossible
125+lenImpossible {n = (S _)} Refl _ impossible
126+
127+total
128+lsplit : (xs : List a) ->
129+ (n : Nat) -> (n = length xs) ->
130+ (left, right : Nat) -> (n = left + right) ->
131+ (ls : List a ** rs : List a **
132+ (length ls = left, length rs = right, xs = ls ++ rs))
133+lsplit xs n prf Z right prf1 = ([] ** xs ** (Refl, rewrite sym prf in prf1, Refl))
134+lsplit [] n prf (S k) right prf1 = void $ lenImpossible prf prf1
135+lsplit (x :: xs) (S k) prf (S l) right prf1
136+ = let (lsrec' ** rsrec' ** (lprf, rprf, recprf))
137+ = lsplit xs k (succInjective _ _ prf) l right (succInjective _ _ prf1) in
138+ (x :: lsrec' ** rsrec' ** (eqSucc _ _ lprf, rprf, rewrite recprf in Refl))
139+lsplit (_ :: _) Z Refl (S _) _ _ impossible
140+
141+data Balanced : Nat -> Nat -> Type where
142+ BalancedZ : Balanced Z Z
143+ BalancedL : Balanced (S Z) Z
144+ BalancedRec : Balanced n m -> Balanced (S n) (S m)
145+
146+-- Question: worth exporting?
147+data SplitBalanced : List a -> Type where
148+ MkSplitBal : {xs, ys : List a} ->
149+ Balanced (length xs) (length ys) -> SplitBalanced (xs ++ ys)
150+
151+mkBalancedL : n = S x -> m = x -> Balanced n m
152+mkBalancedL {m = Z} Refl Refl = BalancedL
153+mkBalancedL {m = (S k)} Refl Refl = BalancedRec (mkBalancedL Refl Refl)
154+
155+mkBalanced : n = x -> m = x -> Balanced n m
156+mkBalanced {n = Z} Refl Refl = BalancedZ
157+mkBalanced {n = (S _)} {m = Z} Refl Refl impossible
158+mkBalanced {n = (S k)} {m = (S k)} Refl Refl = BalancedRec (mkBalanced Refl Refl)
159+
160+splitBalancedLen : (xs : List a) -> (n : Nat) -> (n = length xs) -> SplitBalanced xs
161+splitBalancedLen xs n prf with (half n)
162+ splitBalancedLen xs (S (x + x)) prf | HalfOdd
163+ = let (xs' ** ys' ** (lprf, rprf, apprf)) =
164+ lsplit xs (S (x + x)) prf (S x) x Refl in
165+ rewrite apprf in (MkSplitBal (mkBalancedL lprf rprf))
166+ splitBalancedLen xs (x + x) prf | HalfEven
167+ = let (xs' ** ys' ** (lprf, rprf, apprf)) =
168+ lsplit xs (x + x) prf x x Refl in
169+ rewrite apprf in (MkSplitBal (mkBalanced lprf rprf))
170+
171+splitBalanced : (xs : List a) -> SplitBalanced xs
172+splitBalanced xs = splitBalancedLen xs (length xs) Refl
173+
174+||| The `VList` view allows us to recurse on the middle of a list,
175+||| inspecting the front and back elements simultaneously.
176+public export
177+data VList : List a -> Type where
178+ VNil : VList []
179+ VOne : VList [x]
180+ VCons : {x : a} -> {y : a} -> {xs : List a} ->
181+ VList xs -> VList (x :: xs ++ [y])
182+
183+total
184+balRec : (zs, xs : List a) ->
185+ Balanced (S (length zs)) (S (length xs)) ->
186+ Balanced (length zs) (length xs)
187+balRec zs xs (BalancedRec x) = x
188+
189+lengthSnoc : (x : _) -> (xs : List a) -> length (xs ++ [x]) = S (length xs)
190+lengthSnoc x [] = Refl
191+lengthSnoc x (_ :: xs) = cong (lengthSnoc x xs)
192+
193+Uninhabited (Balanced Z (S k)) where
194+ uninhabited BalancedZ impossible
195+ uninhabited BalancedL impossible
196+ uninhabited (BalancedRec _) impossible
197+
198+toVList : (xs : List a) -> SnocList ys ->
199+ Balanced (length xs) (length ys) -> VList (xs ++ ys)
200+toVList [] Empty y = VNil
201+toVList [x] Empty BalancedL = VOne
202+toVList (z :: zs) (Snoc {xs} {x} srec) prf
203+ = rewrite appendAssociative zs xs [x] in
204+ VCons (toVList zs srec (balRec zs xs
205+ (rewrite sym $ lengthSnoc x xs in prf)))
206+toVList [] (Snoc {xs} {x} _) prf
207+ = let prf' : Balanced Z (S (length xs)) = rewrite sym $ lengthSnoc x xs in prf in
208+ absurd prf'
209+
210+||| Covering function for `VList`
211+||| Constructs the view in linear time.
212+export
213+vlist : (xs : List a) -> VList xs
214+vlist xs with (splitBalanced xs)
215+ vlist (ys ++ zs) | (MkSplitBal prf)
216+ = toVList ys (snocList zs) prf
217+
218+
219+