0 | ||| Views for Vect
 1 | module Data.Vect.Views
 2 |
 3 | import Control.WellFounded
 4 | import Data.Vect
 5 | import Data.Nat
 6 |
 7 | %default total
 8 |
 9 | ||| View for splitting a vector in half, non-recursively
10 | public export
11 | data Split : Vect n a -> Type where
12 |     SplitNil : Split []
13 |     SplitOne : Split [x]
14 |     ||| two non-empty parts
15 |     SplitPair : {n : Nat} -> {m : Nat} ->
16 |                 (x : a) -> (xs : Vect n a) -> (y : a) -> (ys : Vect m a) ->
17 |                 Split (x :: xs ++ y :: ys)
18 |
19 | splitHelp : {n : Nat} -> (head : a) -> (zs : Vect n a) ->
20 |             Nat -> Split (head :: zs)
21 | splitHelp head [] _ = SplitOne
22 | splitHelp head (z :: zs) 0 = SplitPair head [] z zs
23 | splitHelp head (z :: zs) 1 = SplitPair head [] z zs
24 | splitHelp head (z :: zs) (S (S k))
25 |   = case splitHelp z zs k of
26 |          SplitOne => SplitPair head [] z zs
27 |          SplitPair x xs y ys => SplitPair head (x :: xs) y ys
28 |
29 | ||| Covering function for the `Split` view
30 | ||| Constructs the view in linear time
31 | export
32 | split : {n : Nat} -> (xs : Vect n a) -> Split xs
33 | split [] = SplitNil
34 | split {n = S k} (x :: xs) = splitHelp x xs k
35 |
36 | ||| View for splitting a vector in half, recursively
37 | |||
38 | ||| This allows us to define recursive functions which repeatedly split vectors
39 | ||| in half, with base cases for the empty and singleton lists.
40 | public export
41 | data SplitRec : Vect k a -> Type where
42 |   SplitRecNil : SplitRec []
43 |   SplitRecOne : SplitRec [x]
44 |   SplitRecPair : {n : Nat} -> {m : Nat} -> {xs : Vect (S n) a} -> {ys : Vect (S m) a} ->
45 |     (lrec : Lazy (SplitRec xs)) -> (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
46 |
47 | smallerPlusL : (m : Nat) -> (k : Nat) -> LTE (S (S m)) (S (m + S k))
48 | smallerPlusL m k = rewrite sym (plusSuccRightSucc m k) in LTESucc $ LTESucc $ lteAddRight _
49 |
50 | smallerPlusR : (m : Nat) -> (k : Nat) -> LTE (S (S k)) (S (m + S k))
51 | smallerPlusR m k = rewrite sym (plusSuccRightSucc m k) in
52 |                     LTESucc $ LTESucc $ rewrite plusCommutative m k in lteAddRight _
53 |
54 | ||| Covering function for the `SplitRec` view
55 | ||| Constructs the view in O(n lg n)
56 | public export total
57 | splitRec : {k : Nat} -> (xs : Vect k a) -> SplitRec xs
58 | splitRec input with (sizeAccessible k)
59 |   splitRec input | acc with (split input)
60 |     splitRec {k = 0} []  | acc | SplitNil = SplitRecNil
61 |     splitRec {k = 1} [x] | acc | SplitOne = SplitRecOne
62 |     splitRec {k = S nl + S nr} (x :: xs ++ y :: ys) | Access rec | SplitPair x xs y ys =
63 |       SplitRecPair
64 |         (splitRec {k = S nl} (x :: xs) | rec _ $ smallerPlusL nl nr)
65 |         (splitRec {k = S nr} (y :: ys) | rec _ $ smallerPlusR nl nr)
66 |