Views.idr

module Data.Vect.Views

import Data.Vect

||| View for traversing a vector backwards
public export
data SnocVect : Vect n a -> Type where
     Empty : SnocVect []
     Snoc : {x : a} -> {xs : Vect n a} ->
            (rec : SnocVect xs) -> SnocVect (xs ++ [x])

snocVectHelp : {xs : Vect n a} ->
               SnocVect xs -> (ys : Vect m a) -> SnocVect (xs ++ ys)
snocVectHelp {xs} x [] = rewrite vectNilRightNeutral xs in x
snocVectHelp {xs} x (y :: ys) 
    = rewrite vectAppendAssociative xs [y] ys in 
              snocVectHelp (Snoc x {x=y}) ys
                             
||| Covering function for the `SnocVect` view
||| Constructs the view in linear time
export
snocVect : (xs : Vect n a) -> SnocVect xs
snocVect xs = snocVectHelp Empty xs

||| View for splitting a vector in half, non-recursively
public export
data Split : Vect n a -> Type where
     SplitNil : Split []
     SplitOne : Split [x]
     SplitPair : {x, y : a} -> {xs : Vect n a} -> {ys : Vect m a} ->
                 Split (x :: xs ++ y :: ys)

splitHelp : (head : a) ->
            (xs : Vect n a) -> 
            (counter : Vect m a) -> Split (head :: xs)
splitHelp head [] counter = SplitOne
splitHelp head (x :: xs) [] = SplitPair {xs = []} {ys = xs}
splitHelp head (x :: xs) [y] = SplitPair {xs = []} {ys = xs}
splitHelp head (x :: xs) (_ :: _ :: ys) 
     = case splitHelp head xs ys of
            SplitOne => SplitPair {xs = []} {ys = []}
            SplitPair {xs} {ys} => SplitPair {xs = x :: xs} {ys}

||| Covering function for the `Split` view
||| Constructs the view in linear time
export
split : (xs : Vect n a) -> Split xs
split [] = SplitNil
split (x :: xs) = splitHelp x xs xs

||| View for splitting a vector in half, recursively
|||
||| This allows us to define recursive functions which repeatedly split vectors
||| in half, with base cases for the empty and singleton lists.
public export
data SplitRec : Vect n a -> Type where
     SplitRecNil : SplitRec []
     SplitRecOne : {x : a} -> SplitRec [x]
     SplitRecPair : {xs : Vect n a} -> 
                    {ys : Vect m a} -> -- Explicit, don't erase
                    (lrec : Lazy (SplitRec xs)) -> 
                    (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)

smallerPlusL : LTE (S (S m)) (S (plus m (S k)))
smallerPlusL {m} {k} = rewrite sym (plusSuccRightSucc m k) in
                              (LTESucc (LTESucc (lteAddRight _)))

smallerPlusR : LTE (S (S k)) (S (plus m (S k)))
smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
                               LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))

||| Covering function for the `SplitRec` view
||| Constructs the view in O(n lg n)
public export total
splitRec : (xs : Vect n a) -> SplitRec xs
splitRec {n} input with (sizeAccessible n)
  splitRec input | acc with (split input)
    splitRec [] | acc | SplitNil = SplitRecNil
    splitRec [x] | acc | SplitOne = SplitRecOne
    splitRec (x :: (xs ++ (y :: ys))) | Access acc | SplitPair
        = SplitRecPair
            (splitRec (x :: xs) | acc _ smallerPlusL)
            (splitRec (y :: ys) | acc _ smallerPlusR)