0 | module Data.List.Views
 1 |
 2 | import Control.Relation
 3 | import Control.WellFounded
 4 | import Data.List
 5 | import Data.Nat
 6 |
 7 | %default total
 8 |
 9 | lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
10 |             length (xs ++ (y :: ys)) = S (length (xs ++ ys))
11 | lengthSuc [] _ _ = Refl
12 | lengthSuc (x :: xs) y ys = cong S (lengthSuc xs y ys)
13 |
14 | lengthLT : (xs : List a) -> (ys : List a) ->
15 |            LTE (length xs) (length (ys ++ xs))
16 | lengthLT xs [] = reflexive {x = length xs}
17 | lengthLT xs (x :: ys) = lteSuccRight (lengthLT _ _)
18 |
19 | smallerLeft : (ys : List a) -> (y : a) -> (zs : List a) ->
20 |               LTE (S (S (length ys))) (S (length (ys ++ (y :: zs))))
21 | smallerLeft [] y zs = LTESucc (LTESucc LTEZero)
22 | smallerLeft (z :: ys) y zs = LTESucc (smallerLeft ys _ _)
23 |
24 | smallerRight : (ys : List a) -> (zs : List a) ->
25 |                LTE (S (S (length zs))) (S (length (ys ++ (y :: zs))))
26 | smallerRight ys zs = rewrite lengthSuc ys y zs in
27 |                      (LTESucc (LTESucc (lengthLT _ _)))
28 |
29 | ||| View for splitting a list in half, non-recursively
30 | public export
31 | data Split : List a -> Type where
32 |      SplitNil : Split []
33 |      SplitOne : (x : a) -> Split [x]
34 |      SplitPair : (x : a) -> (xs : List a) ->
35 |                  (y : a) -> (ys : List a) ->
36 |                  Split (x :: xs ++ y :: ys)
37 |
38 | splitHelp : (head : a) ->
39 |             (xs : List a) ->
40 |             (counter : List a) -> Split (head :: xs)
41 | splitHelp head [] counter = SplitOne _
42 | splitHelp head (x :: xs) [] = SplitPair head [] x xs
43 | splitHelp head (x :: xs) [y] = SplitPair head [] x xs
44 | splitHelp head (x :: xs) (_ :: _ :: ys)
45 |     = case splitHelp head xs ys of
46 |            SplitOne x => SplitPair x [] _ []
47 |            SplitPair x' xs y' ys => SplitPair x' (x :: xs) y' ys
48 |
49 | ||| Covering function for the `Split` view
50 | ||| Constructs the view in linear time
51 | export
52 | split : (xs : List a) -> Split xs
53 | split [] = SplitNil
54 | split (x :: xs) = splitHelp x xs xs
55 |
56 | public export
57 | data SplitRec : List a -> Type where
58 |      SplitRecNil : SplitRec []
59 |      SplitRecOne : (x : a) -> SplitRec [x]
60 |      SplitRecPair : (lefts, rights : List a) -> -- Explicit, don't erase
61 |                     (lrec : Lazy (SplitRec lefts)) ->
62 |                     (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
63 |
64 | ||| Covering function for the `SplitRec` view
65 | ||| Constructs the view in O(n lg n)
66 | public export
67 | splitRec : (xs : List a) -> SplitRec xs
68 | splitRec xs with (sizeAccessible xs)
69 |   splitRec xs | acc with (split xs)
70 |     splitRec []  | acc | SplitNil = SplitRecNil
71 |     splitRec [x] | acc | SplitOne x = SplitRecOne x
72 |     splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair y ys z zs
73 |       = SplitRecPair _ _
74 |           (splitRec (y :: ys) | acc _ (smallerLeft ys z zs))
75 |           (splitRec (z :: zs) | acc _ (smallerRight ys zs))
76 |
77 | ||| View for traversing a list backwards
78 | public export
79 | data SnocList : List a -> Type where
80 |      Empty : SnocList []
81 |      Snoc : (x : a) -> (xs : List a) ->
82 |             (rec : SnocList xs) -> SnocList (xs ++ [x])
83 |
84 | snocListHelp : {input : _} ->
85 |                SnocList input -> (rest : List a) -> SnocList (input ++ rest)
86 | snocListHelp snoc [] = rewrite appendNilRightNeutral input in snoc
87 | snocListHelp snoc (x :: xs)
88 |    = rewrite appendAssociative input [x] xs in
89 |              snocListHelp (Snoc x input snoc) xs
90 |
91 | ||| Covering function for the `SnocList` view
92 | ||| Constructs the view in linear time
93 | export
94 | snocList : (xs : List a) -> SnocList xs
95 | snocList xs = snocListHelp Empty xs
96 |