Data.List.TailRec


   0 | ||| Contains:
   1 | |||
   2 | ||| 1. Tail recursive versions of the list processing functions from
   3 | |||    List.
   4 | |||
   5 | ||| 2. Extensional equality proofs that these variants are
   6 | |||    (extensionally) equivalent to their non-tail-recursive
   7 | |||    counterparts.
   8 | |||
   9 | ||| Note:
  10 | |||
  11 | ||| 1. Written in one sitting, feel free to refactor
  12 | |||
  13 | ||| 2. The proofs below also work on non-publicly exported
  14 | |||    definitions.  This could be due to a bug, and will need to be
  15 | |||    moved elsewhere if it's fixed.
  16 | module Data.List.TailRec
  17 | 
  18 | import Syntax.PreorderReasoning
  19 | import Syntax.WithProof
  20 | 
  21 | import Data.List
  22 | import Data.List1
  23 | 
  24 | %default total
  25 | 
  26 | lengthAcc : List a -> Nat -> Nat
  27 | lengthAcc [] acc = acc
  28 | lengthAcc (_::xs) acc = lengthAcc xs $ S acc
  29 | 
  30 | export
  31 | length : List a -> Nat
  32 | length xs = lengthAcc xs Z
  33 | 
  34 | lengthAccSucc : (xs : List a) -> (n : Nat) -> lengthAcc xs (S n) = S (lengthAcc xs n)
  35 | lengthAccSucc [] _ = Refl
  36 | lengthAccSucc (_::xs) n = rewrite lengthAccSucc xs (S n) in cong S Refl
  37 | 
  38 | export
  39 | length_ext : (xs : List a) -> List.length xs = List.TailRec.length xs
  40 | length_ext [] = Refl
  41 | length_ext (_::xs) = rewrite length_ext xs in sym $ lengthAccSucc xs Z
  42 | 
  43 | take_aux : Nat -> List a -> List a -> List a
  44 | take_aux Z     xs        acc = reverseOnto [] acc
  45 | take_aux (S n) []        acc = reverseOnto [] acc
  46 | take_aux (S n) (x :: xs) acc = take_aux n xs (x :: acc)
  47 | 
  48 | export
  49 | take : Nat -> List a -> List a
  50 | take n xs = take_aux n xs []
  51 | 
  52 | export
  53 | take_ext :
  54 |   (n : Nat) -> (xs : List a) ->
  55 |      List.take n xs = List.TailRec.take n xs
  56 | take_ext n xs = Calc $
  57 |   |~ List.take n xs
  58 |   ~~ reverse [] ++ (List.take n xs)  ...( Refl )
  59 |   ~~ reverseOnto (List.take n xs) [] ...( sym (revOnto (List.take n xs) []) )
  60 |   ~~ take_aux n xs []                     ...( sym (lemma n xs []) )
  61 |   where
  62 |     lemma : (n : Nat) -> (xs, acc : List a) ->
  63 |             take_aux n xs acc =  reverseOnto (List.take n xs) acc
  64 |     lemma Z     xs      acc = Refl
  65 |     lemma (S n) []      acc = Refl
  66 |     lemma (S n) (x::xs) acc = lemma n xs (x :: acc)
  67 | 
  68 | 
  69 | span_aux : (a -> Bool) -> List a -> List a -> (List a, List a)
  70 | span_aux p []      acc = (reverseOnto [] acc, [])
  71 | span_aux p (x::xs) acc =
  72 |   if p x then
  73 |     List.TailRec.span_aux p xs (x :: acc)
  74 |   else
  75 |     (reverseOnto [] acc, x::xs)
  76 | 
  77 | export
  78 | span : (a -> Bool) -> List a -> (List a, List a)
  79 | span p xs = span_aux p xs []
  80 | 
  81 | coe : (f : (i : a) -> Type) -> i = i' -> f i -> f i'
  82 | coe f Refl x = x
  83 | 
  84 | span_aux_ext : (p : a -> Bool) -> (xs, acc : List a) ->
  85 |   (reverseOnto (fst $ List.span p xs) acc, snd $ List.span p xs)
  86 |   =
  87 |   span_aux p xs acc
  88 | span_aux_ext p []      acc = Refl
  89 | -- This is disgusting. Please teach me a better way.
  90 | span_aux_ext p (x::xs) acc with (@@(p x), @@(List.span p xs))
  91 |  span_aux_ext p (x::xs) acc | ((True ** px_tru), ((pre, rest)**dl_pf)) =
  92 |    rewrite px_tru in
  93 |    rewrite dl_pf in
  94 |    let u = span_aux_ext p xs (x::acc) in
  95 |    coe (\u => (reverseOnto (x :: fst u) acc, snd u) =
  96 |                List.TailRec.span_aux p xs (x :: acc)) dl_pf u
  97 |  span_aux_ext p (x::xs) acc | ((False**px_fls), ((pre,rest)**dl_pf)) =
  98 |    rewrite px_fls in
  99 |    Refl
 100 | 
 101 | export
 102 | span_ext : (p : a -> Bool) -> (xs : List a) ->
 103 |   List.span p xs = List.TailRec.span p xs
 104 | span_ext p xs with (@@(List.span p xs))
 105 |   span_ext p xs |  ((pre, rest) ** pf) =
 106 |     rewrite pf in
 107 |     let u = span_aux_ext p xs [] in
 108 |     coe (\u => (fst u, snd u) = span_aux p xs []) pf u
 109 | 
 110 | export
 111 | break : (a -> Bool) -> List a -> (List a, List a)
 112 | break p xs = List.TailRec.span (not . p) xs
 113 | 
 114 | export
 115 | break_ext : (p : a -> Bool) -> (xs : List a) ->
 116 |   List.break p xs = List.TailRec.break p xs
 117 | break_ext p xs = span_ext (not . p) xs
 118 | 
 119 | splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a)
 120 | splitOnto acc p xs =
 121 |   case List.break p xs of
 122 |     (chunk, []       ) => reverseOnto (chunk ::: []) acc
 123 |     (chunk, (c::rest)) => splitOnto (chunk::acc) p $ assert_smaller xs rest
 124 | 
 125 | export
 126 | split : (a -> Bool) -> List a -> List1 (List a)
 127 | split p xs = splitOnto [] p xs
 128 | 
 129 | splitOnto_ext : (acc : List (List a)) -> (p : a -> Bool) -> (xs : List a) ->
 130 |               reverseOnto (List.split p xs) acc
 131 |               = List.TailRec.splitOnto acc p xs
 132 | splitOnto_ext  acc p xs with (@@(List.break p xs))
 133 |  splitOnto_ext acc p xs | ((chunk,  []    )**pf) =
 134 |    rewrite pf in
 135 |    Refl
 136 |  splitOnto_ext acc p xs | ((chunk, c::rest)**pf) =
 137 |    rewrite pf in
 138 |    rewrite splitOnto_ext (chunk::acc) p $ assert_smaller xs rest in
 139 |    Refl
 140 | 
 141 | export
 142 | split_ext : (p : a -> Bool) -> (xs : List a) ->
 143 |   List.split p xs = List.TailRec.split p xs
 144 | split_ext p xs = splitOnto_ext [] p xs
 145 | 
 146 | 
 147 | splitAtOnto : List a -> (n : Nat) -> (xs : List a) -> (List a, List a)
 148 | splitAtOnto acc Z     xs      = (reverseOnto [] acc, xs)
 149 | splitAtOnto acc (S n) []      = (reverseOnto [] acc, [])
 150 | splitAtOnto acc (S n) (x::xs) = splitAtOnto (x::acc) n xs
 151 | 
 152 | export
 153 | splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
 154 | splitAt n xs = splitAtOnto [] n xs
 155 | 
 156 | splitAtOnto_ext : (acc : List a) -> (n : Nat) -> (xs : List a) ->
 157 |   (reverseOnto (fst $ List.splitAt n xs) acc, snd $ List.splitAt n xs)
 158 |   = splitAtOnto acc n xs
 159 | splitAtOnto_ext  acc Z     xs      = Refl
 160 | splitAtOnto_ext  acc (S n) []      = Refl
 161 | splitAtOnto_ext  acc (S n) (x::xs) with (@@(List.splitAt n xs))
 162 |  splitAtOnto_ext acc (S n) (x::xs) | ((tk, dr)**pf) =
 163 |    rewrite pf in
 164 |    let u = splitAtOnto_ext (x::acc) n xs in
 165 |    coe (\u => (reverseOnto (x :: fst u) acc, snd u) =
 166 |                       splitAtOnto (x :: acc) n xs) pf u
 167 | 
 168 | export
 169 | splitAt_ext : (n : Nat) -> (xs : List a) ->
 170 |   List.splitAt n xs =
 171 |   List.TailRec.splitAt n xs
 172 | splitAt_ext  n xs with (@@(List.splitAt n xs))
 173 |  splitAt_ext n xs | ((tk, dr)**pf) =
 174 |    rewrite pf in
 175 |    rewrite sym $ splitAtOnto_ext [] n xs in
 176 |    rewrite pf in
 177 |    Refl
 178 | 
 179 | partitionOnto : List a -> List a -> (a -> Bool) -> List a -> (List a, List a)
 180 | partitionOnto lfts rgts p []      = (reverseOnto [] lfts, reverseOnto [] rgts)
 181 | partitionOnto lfts rgts p (x::xs) =
 182 |   if p x then
 183 |     partitionOnto (x :: lfts)     rgts  p xs
 184 |   else
 185 |     partitionOnto       lfts  (x::rgts) p xs
 186 | 
 187 | export
 188 | partition : (a -> Bool) -> List a -> (List a, List a)
 189 | partition p xs = partitionOnto [] [] p xs
 190 | 
 191 | partitionOnto_ext : (lfts, rgts : List a) -> (p : a -> Bool) -> (xs : List a) ->
 192 |   (reverseOnto (fst $ List.partition p xs) lfts
 193 |   ,reverseOnto (snd $ List.partition p xs) rgts)
 194 |   = List.TailRec.partitionOnto lfts rgts p xs
 195 | partitionOnto_ext  lfts rgts p [] = Refl
 196 | partitionOnto_ext  lfts rgts p (x::xs) with (@@(p x), @@(List.partition p xs))
 197 |  partitionOnto_ext lfts rgts p (x::xs) | ((True **px_tru), ((dl_l, dl_r)**dl_pf))
 198 |    = rewrite px_tru in
 199 |      rewrite dl_pf  in
 200 |      rewrite px_tru in
 201 |      let u = partitionOnto_ext (x :: lfts) rgts p xs in
 202 |      coe (\u => (reverseOnto (x :: fst u) lfts
 203 |                 ,reverseOnto (     snd u) rgts)
 204 |                 = partitionOnto (x :: lfts) rgts p xs) dl_pf u
 205 | 
 206 |  partitionOnto_ext lfts rgts p (x::xs) | ((False**px_fls), ((dl_l, dl_r)**dl_pf))
 207 |    = rewrite px_fls in
 208 |      rewrite dl_pf  in
 209 |      rewrite px_fls in
 210 |      let u = partitionOnto_ext lfts (x :: rgts) p xs in
 211 |      coe (\u => (reverseOnto (     fst u) lfts
 212 |                 ,reverseOnto (x :: snd u) rgts)
 213 |                 = partitionOnto lfts (x::rgts) p xs) dl_pf u
 214 | 
 215 | mergeReplicate_aux : a -> List a -> List a -> List a
 216 | mergeReplicate_aux sep []      acc = reverseOnto [] acc
 217 | mergeReplicate_aux sep (x::xs) acc = mergeReplicate_aux sep xs (x :: sep :: acc)
 218 | 
 219 | mergeReplicate_ext : (sep : a) -> (xs : List a) -> (acc : List a) ->
 220 |                    mergeReplicate_aux sep xs acc =
 221 |                    reverseOnto (mergeReplicate sep xs) acc
 222 | mergeReplicate_ext sep []      acc = Refl
 223 | mergeReplicate_ext sep (x::xs) acc = Calc $
 224 |   |~ mergeReplicate_aux sep xs (x :: sep :: acc)
 225 |   ~~ reverseOnto (sep :: x :: mergeReplicate sep xs) acc
 226 |                               ...( mergeReplicate_ext sep xs (x :: sep :: acc) )
 227 | 
 228 | export
 229 | intersperse : a -> List a -> List a
 230 | intersperse sep []      = []
 231 | intersperse sep (y::ys) = y :: mergeReplicate_aux sep ys []
 232 | 
 233 | export
 234 | intersperse_ext : (sep : a) -> (xs : List a) ->
 235 |               List.intersperse sep xs =
 236 |               List.TailRec.intersperse sep xs
 237 | intersperse_ext sep [] = Refl
 238 | intersperse_ext sep (y::ys) = cong (y::) (sym $ mergeReplicate_ext sep ys [])
 239 | 
 240 | mapMaybeOnto : List b -> (a -> Maybe b) -> List a -> List b
 241 | mapMaybeOnto acc f [] = reverseOnto [] acc
 242 | mapMaybeOnto acc f (x::xs) =
 243 |   case f x of
 244 |     Nothing => mapMaybeOnto acc f xs
 245 |     Just  y => mapMaybeOnto (y :: acc) f xs
 246 | 
 247 | export
 248 | mapMaybe : (a -> Maybe b) -> List a -> List b
 249 | mapMaybe f xs = mapMaybeOnto [] f xs
 250 | 
 251 | mapMaybeOnto_ext : (acc : List b) -> (f : a -> Maybe b) -> (xs : List a) ->
 252 |   reverseOnto (List.mapMaybe f xs) acc
 253 |   =
 254 |   mapMaybeOnto acc f xs
 255 | mapMaybeOnto_ext  acc f []                = Refl
 256 | mapMaybeOnto_ext  acc f (x::xs) with (f x)
 257 |  mapMaybeOnto_ext acc f (x::xs) | Nothing = mapMaybeOnto_ext acc f xs
 258 |  mapMaybeOnto_ext acc f (x::xs) | Just  y = mapMaybeOnto_ext (y :: acc) f xs
 259 | 
 260 | export
 261 | mapMaybe_ext : (f : a -> Maybe b) -> (xs : List a) ->
 262 |   List.mapMaybe f xs = List.TailRec.mapMaybe f xs
 263 | mapMaybe_ext f xs = mapMaybeOnto_ext [] f xs
 264 | 
 265 | export
 266 | sorted : Ord a => List a -> Bool
 267 | sorted [ ] = True
 268 | sorted [x] = True
 269 | sorted  (x :: xs@(y :: ys)) = case (x <= y) of
 270 |                                 False => False
 271 |                                 True  => List.TailRec.sorted xs
 272 | 
 273 | export
 274 | covering
 275 | sorted_ext : Ord a => (xs : List a) ->
 276 |   List.sorted xs = List.TailRec.sorted xs
 277 | sorted_ext []  = Refl
 278 | sorted_ext [x] = Refl
 279 | sorted_ext  (x :: y :: ys) with (x <= y)
 280 |  sorted_ext (x :: y :: ys) | False = Refl
 281 |  sorted_ext (x :: y :: ys) | True  = sorted_ext (y::ys)
 282 | 
 283 | mergeByOnto : List a -> (a -> a -> Ordering) -> List a -> List a -> List a
 284 | mergeByOnto acc order []           right         = reverseOnto right acc
 285 | mergeByOnto acc order left         []            = reverseOnto left  acc
 286 | mergeByOnto acc order left@(x::xs) right@(y::ys) =
 287 |   -- We need the variant annotations (bug #300)
 288 |   case order x y of
 289 |     LT => mergeByOnto (x :: acc) order (assert_smaller left xs)   right
 290 |     _  => mergeByOnto (y :: acc) order left                       (assert_smaller right ys)
 291 | 
 292 | covering
 293 | mergeByOnto_ext : (acc : List a)
 294 |                -> (order : a -> a -> Ordering)
 295 |                -> (left, right : List a)
 296 |                -> reverseOnto (mergeBy order left right) acc
 297 |                   = mergeByOnto acc order left right
 298 | mergeByOnto_ext acc order []           right         = Refl
 299 | mergeByOnto_ext  acc order left        []            with( left)
 300 |  mergeByOnto_ext acc order _           []            | []     = Refl
 301 |  mergeByOnto_ext acc order _           []            | (_::_) = Refl
 302 | mergeByOnto_ext acc order left@(x::xs) right@(y::ys) with (order x y)
 303 |  mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | LT =
 304 |                            mergeByOnto_ext (x :: acc) order xs (y::ys)
 305 |  -- We need to exhaust the two other cases explicitly to convince the
 306 |  -- typecheker. See #140
 307 |  mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | EQ =
 308 |                            mergeByOnto_ext (y :: acc) order (x::xs) ys
 309 |  mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | GT =
 310 |                            mergeByOnto_ext (y :: acc) order (x::xs) ys
 311 | 
 312 | export
 313 | mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
 314 | mergeBy order left right = mergeByOnto [] order left right
 315 | 
 316 | export
 317 | covering
 318 | mergeBy_ext : (order : a -> a -> Ordering) -> (left, right : List a) ->
 319 |   List.mergeBy order left right =
 320 |   List.TailRec.mergeBy order left right
 321 | mergeBy_ext order left right = mergeByOnto_ext [] order left right
 322 | 
 323 | export
 324 | merge : Ord a => List a -> List a -> List a
 325 | merge = List.TailRec.mergeBy compare
 326 | 
 327 | export
 328 | covering
 329 | merge_ext : Ord a => (left, right : List a) ->
 330 |   List.merge left right = List.TailRec.merge left right
 331 | merge_ext left right = mergeBy_ext compare left right
 332 | 
 333 | 
 334 | -- Not quite finished due to a bug.
 335 | 
 336 | sortBy_splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
 337 | sortBy_splitRec (_::_::xs) (y::ys) zs = sortBy_splitRec xs ys (zs . ((::) y))
 338 | sortBy_splitRec _          ys      zs = (zs [], ys)
 339 | 
 340 | sortBy_split : List a -> (List a, List a)
 341 | sortBy_split xs = sortBy_splitRec xs xs id
 342 | 
 343 | export
 344 | sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
 345 | sortBy cmp []  = []
 346 | sortBy cmp [x] = [x]
 347 | sortBy cmp zs = let (xs, ys) = sortBy_split zs in
 348 |     List.TailRec.mergeBy cmp
 349 |           (List.TailRec.sortBy cmp (assert_smaller zs xs))
 350 |           (List.TailRec.sortBy cmp (assert_smaller zs ys))
 351 | 
 352 | 
 353 |  {- Can't really finish this proof because Data.List doesn't export the definition of sortBy. -}
 354 |  {-
 355 | export
 356 | sortBy_ext : (cmp : a -> a -> Ordering) -> (xs : List a) ->
 357 |   List.sortBy cmp xs = List.TailRec.sortBy cmp xs
 358 | sortBy_ext  cmp []  = Refl
 359 | sortBy_ext  cmp [x] = Refl
 360 | sortBy_ext  cmp zs'@(z::zs) =
 361 |   Calc $
 362 |   |~ List.sortBy cmp (z::zs)
 363 |   ~~ (let (xs, ys) = sortBy_split zs' in
 364 |      List.mergeBy cmp
 365 |      (List.sortBy cmp xs)
 366 |      (List.sortBy cmp ys))
 367 |       ...( ?help0 )
 368 |   ~~
 369 |   let (xs, ys) = sortBy_split (z::zs) in
 370 |   List.TailRec.mergeBy cmp
 371 |     (List.TailRec.sortBy cmp xs)
 372 |     (List.TailRec.sortBy cmp ys)
 373 |     ...( ?help1 )
 374 | -}
 375 |