0 | module Data.List.Views.Extra
  1 |
  2 | import Data.List
  3 | import Data.List.Reverse
  4 | import Data.List.Views
  5 | import Data.Nat
  6 | import Data.List.Equalities
  7 |
  8 | %default total
  9 |
 10 | ||| Proof that two numbers differ by at most one
 11 | public export
 12 | data Balanced : Nat -> Nat -> Type where
 13 |   BalancedZ   : Balanced Z Z
 14 |   BalancedL   : Balanced (S Z) Z
 15 |   BalancedRec : Balanced n m -> Balanced (S n) (S m)
 16 |
 17 | %name Balanced bal, b
 18 |
 19 | Uninhabited (Balanced Z (S k)) where
 20 |   uninhabited BalancedZ impossible
 21 |   uninhabited BalancedL impossible
 22 |   uninhabited (BalancedRec rec) impossible
 23 |
 24 | export
 25 | balancedPred : Balanced (S x) (S y) -> Balanced x y
 26 | balancedPred (BalancedRec pred) = pred
 27 |
 28 | export
 29 | mkBalancedEq : {n, m : Nat} -> n = m -> Balanced n m
 30 | mkBalancedEq {n = 0} Refl = BalancedZ
 31 | mkBalancedEq {n = (S k)} Refl = BalancedRec $ mkBalancedEq {n = k} Refl
 32 |
 33 | export
 34 | mkBalancedL : {n, m : Nat} -> n = S m -> Balanced n m
 35 | mkBalancedL {m = 0} Refl = BalancedL
 36 | mkBalancedL {m = S k} Refl = BalancedRec (mkBalancedL Refl)
 37 |
 38 | ||| View of a list split into two halves
 39 | |||
 40 | ||| The lengths of the lists are guaranteed to differ by at most one
 41 | public export
 42 | data SplitBalanced : List a -> Type where
 43 |   MkSplitBal
 44 |     : {xs, ys : List a}
 45 |     -> Balanced (length xs) (length ys)
 46 |     -> SplitBalanced (xs ++ ys)
 47 |
 48 | private
 49 | splitBalancedHelper
 50 |   : (revLs : List a)
 51 |   -> (rs : List a)
 52 |   -> (doubleSkip : List a)
 53 |   -> (length rs = length revLs + length doubleSkip)
 54 |   -> SplitBalanced (reverse revLs ++ rs)
 55 | splitBalancedHelper revLs rs [] prf = MkSplitBal balancedLeftsAndRights
 56 |   where
 57 |     lengthsEqual : length rs = length revLs
 58 |     lengthsEqual =
 59 |       rewrite sym (plusZeroRightNeutral (length revLs)) in prf
 60 |     balancedLeftsAndRights : Balanced (length (reverse revLs)) (length rs)
 61 |     balancedLeftsAndRights =
 62 |       rewrite reverseLength revLs in
 63 |         rewrite lengthsEqual in
 64 |           mkBalancedEq Refl
 65 | splitBalancedHelper revLs [] (x :: xs) prf =
 66 |   absurd $
 67 |     the (0 = S (plus (length revLs) (length xs))) $
 68 |       rewrite plusSuccRightSucc (length revLs) (length xs) in
 69 |         prf
 70 | splitBalancedHelper revLs (x :: rs) [lastItem] prf =
 71 |   rewrite appendAssociative (reverse revLs) [x] rs in
 72 |     rewrite sym (reverseCons x revLs) in
 73 |       MkSplitBal $
 74 |         the (Balanced (length (reverseOnto [x] revLs)) (length rs)) $
 75 |           rewrite reverseCons x revLs in
 76 |             rewrite lengthSnoc x (reverse revLs) in
 77 |               rewrite reverseLength revLs in
 78 |                 rewrite lengthsEqual in
 79 |                   mkBalancedL Refl
 80 |   where
 81 |     lengthsEqual : length rs = length revLs
 82 |     lengthsEqual =
 83 |       cong pred $
 84 |         the (S (length rs) = S (length revLs)) $
 85 |           rewrite plusCommutative 1 (length revLs) in prf
 86 | splitBalancedHelper revLs (x :: oneFurther) (_ :: (_ :: twoFurther)) prf =
 87 |   rewrite appendAssociative (reverse revLs) [x] oneFurther in
 88 |     rewrite sym (reverseCons x revLs) in
 89 |       splitBalancedHelper (x :: revLs) oneFurther twoFurther $
 90 |         cong pred $
 91 |           the (S (length oneFurther) = S (S (plus (length revLs) (length twoFurther)))) $
 92 |           rewrite plusSuccRightSucc (length revLs) (length twoFurther) in
 93 |             rewrite plusSuccRightSucc (length revLs) (S (length twoFurther)) in
 94 |               prf
 95 |
 96 | ||| Covering function for the `SplitBalanced`
 97 | |||
 98 | ||| Constructs the view in linear time
 99 | export
100 | splitBalanced : (input : List a) -> SplitBalanced input
101 | splitBalanced input = splitBalancedHelper [] input input Refl
102 |
103 | ||| The `VList` view allows us to recurse on the middle of a list,
104 | ||| inspecting the front and back elements simultaneously.
105 | public export
106 | data VList : List a -> Type where
107 |   VNil : VList []
108 |   VOne : VList [x]
109 |   VCons : {x, y : a} -> {xs : List a} -> (rec : Lazy (VList xs)) -> VList (x :: xs ++ [y])
110 |
111 | private
112 | toVList
113 |   : (xs : List a)
114 |   -> SnocList ys
115 |   -> Balanced (length xs) (length ys)
116 |   -> VList (xs ++ ys)
117 | toVList [] Empty BalancedZ = VNil
118 | toVList [x] Empty BalancedL = VOne
119 | toVList [] (Snoc x zs rec) prf =
120 |   absurd $
121 |     the (Balanced 0 (S (length zs))) $
122 |       rewrite sym (lengthSnoc x zs) in prf
123 | toVList (x :: xs) (Snoc y ys srec) prf =
124 |   rewrite appendAssociative xs ys [y] in
125 |     VCons $
126 |       toVList xs srec $
127 |         balancedPred $
128 |           rewrite sym (lengthSnoc y ys) in prf
129 |
130 | ||| Covering function for `VList`
131 | ||| Constructs the view in linear time.
132 | export
133 | vList : (xs : List a) -> VList xs
134 | vList xs with (splitBalanced xs)
135 |   vList (ys ++ zs) | (MkSplitBal prf) = toVList ys (snocList zs) prf
136 |
137 | ||| Lazy filtering of a list based on a predicate.
138 | public export
139 | data LazyFilterRec : List a -> Type where
140 |   Exhausted : (skip : List a) -> LazyFilterRec skip
141 |   Found     : (skip : List a) -- initial non-matching elements
142 |             -> (head : a)      -- first match
143 |             -> Lazy (LazyFilterRec rest)
144 |             -> LazyFilterRec (skip ++ (head :: rest))
145 |
146 | ||| Covering function for the LazyFilterRec view.
147 | ||| Constructs the view lazily in linear time.
148 | export
149 | lazyFilterRec : (pred : (a -> Bool)) -> (xs : List a) -> LazyFilterRec xs
150 | lazyFilterRec pred [] = Exhausted []
151 | lazyFilterRec pred (x :: xs) with (pred x)
152 |   lazyFilterRec pred (x :: xs) | True = Found [] x (lazyFilterRec pred xs)
153 |   lazyFilterRec pred (x :: []) | False = Exhausted [x]
154 |   lazyFilterRec pred (x :: rest@(_ :: xs)) | False = filterHelper [x] rest
155 |     where
156 |       filterHelper
157 |         : (reverseOfSkipped : List a)
158 |         -> {auto prf1 : NonEmpty reverseOfSkipped}
159 |         -> (rest : List a)
160 |         -> {auto prf2 : NonEmpty rest}
161 |         -> LazyFilterRec (reverse reverseOfSkipped ++ rest)
162 |       filterHelper revSkipped (y :: xs) with (pred y)
163 |         filterHelper revSkipped (y :: xs) | True =
164 |           Found (reverse revSkipped) y (lazyFilterRec pred xs)
165 |         filterHelper revSkipped (y :: []) | False =
166 |           rewrite sym (reverseOntoSpec [y] revSkipped) in
167 |           Exhausted $ reverse (y :: revSkipped)
168 |         filterHelper revSkipped (y :: (z :: zs)) | False =
169 |           rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in
170 |             rewrite sym (reverseOntoSpec [y] revSkipped) in
171 |               filterHelper (y :: revSkipped) (z :: zs)
172 |