
   0 | module Data.CheckedEmpty.List.Lazy
   1 | 
   2 | import Control.Function
   3 | 
   4 | import Data.Bool
   5 | import Data.List.Lazy
   6 | import Data.Fin
   7 | import Data.Zippable
   8 | 
   9 | import public Language.Implicits.IfUnsolved
  10 | 
  11 | %default total
  12 | 
  13 | --- Types definitions ---
  14 | 
  15 | public export
  16 | data LazyLst : (definitelyNotEmpty : Bool) -> Type -> Type where
  17 |   Nil  : LazyLst False a
  18 |   (::) : (0 _ : True `IfUnsolved` ine) => (0 _ : True `IfUnsolved` ne) =>
  19 |          a -> Lazy (LazyLst ine a) -> LazyLst ne a
  20 | 
  21 | %name LazyLst xs, ys, zs
  22 | 
  23 | ||| An alias for a list that definitely may be empty.
  24 | ||| Don't use this if you can be polymorphic on the boolean type argument.
  25 | public export %inline
  26 | LazyLst0 : Type -> Type
  27 | LazyLst0 = LazyLst False
  28 | 
  29 | public export %inline
  30 | LazyLst1 : Type -> Type
  31 | LazyLst1 = LazyLst True
  32 | 
  33 | --- Basic functions ---
  34 | 
  35 | public export
  36 | length : LazyLst ne a -> Nat
  37 | length []      = Z
  38 | length (_::xs) = S $ length xs
  39 | 
  40 | public export %inline
  41 | (.length) : LazyLst ne a -> Nat
  42 | xs.length = length xs
  43 | 
  44 | public export
  45 | (++) : LazyLst nel a -> Lazy (LazyLst ner a) -> LazyLst (nel || ner) a
  46 | []      ++ ys = ys
  47 | (x::xs) ++ ys = x :: xs ++ ys
  48 | 
  49 | public export
  50 | Semigroup (LazyLst ne a) where
  51 |   xs <+> ys = rewrite sym $ orSameNeutral ne in xs ++ ys
  52 | 
  53 | public export
  54 | Monoid (LazyLst0 a) where
  55 |   neutral = []
  56 | 
  57 | public export
  58 | index' : (xs : LazyLst ne a) -> Fin xs.length -> a
  59 | index' (x::_ ) FZ     = x
  60 | index' (_::xs) (FS i) = index' xs i
  61 | 
  62 | public export %inline
  63 | index : Fin n -> (xs : LazyLst ne a) -> (0 _ : n = xs.length) => a
  64 | index i xs @{Refl} = index' xs i
  65 | 
  66 | --- Creation ---
  67 | 
  68 | public export
  69 | iterateN : (n : Nat) -> (a -> a) -> a -> LazyLst (n /= 0) a
  70 | iterateN Z     _ x = []
  71 | iterateN (S n) f x = x :: iterateN n f (f x)
  72 | 
  73 | public export
  74 | tabulateN : (n : Nat) -> (Fin n -> a) -> LazyLst (n /= 0) a
  75 | tabulateN 0     _ = []
  76 | tabulateN (S k) f = f FZ :: tabulateN k (f . FS)
  77 | 
  78 | public export
  79 | replicate : (n : Nat) -> a -> LazyLst (n /= 0) a
  80 | replicate Z     _ = []
  81 | replicate (S k) x = x :: replicate k x
  82 | 
  83 | covering
  84 | public export
  85 | iterate : (a -> Maybe a) -> a -> LazyLst0 a
  86 | iterate f x = x :: case f x of
  87 |   Nothing => []
  88 |   Just y  => iterate f y
  89 | 
  90 | covering
  91 | public export
  92 | unfoldr : (b -> Maybe (a, b)) -> b -> LazyLst0 a
  93 | unfoldr f c = case f c of
  94 |   Nothing     => []
  95 |   Just (a, n) => a :: unfoldr f n
  96 | 
  97 | --- Internal conversions ---
  98 | 
  99 | -- Relaxation --
 100 | 
 101 | public export
 102 | relaxF : LazyLst ne a -> LazyLst0 a
 103 | relaxF []      = []
 104 | relaxF (x::xs) = x::xs
 105 | 
 106 | public export %inline
 107 | relaxT : LazyLst1 a -> LazyLst ne a
 108 | relaxT (x::xs) = x::xs
 109 | 
 110 | public export
 111 | relaxAnd : LazyLst ne a -> LazyLst (ne && nx) a
 112 | relaxAnd []      = []
 113 | relaxAnd (x::xs) = x::xs
 114 | 
 115 | %transform "relaxF=id"   relaxF   {ne} {a} = believe_me (\x => the (LazyLst ne a) x)
 116 | %transform "relaxT=id"   relaxT   {ne} {a} = believe_me (\x => the (LazyLst ne a) x)
 117 | %transform "relaxAnd=id" relaxAnd {ne} {a} = believe_me (\x => the (LazyLst ne a) x)
 118 | 
 119 | -- Strengthening --
 120 | 
 121 | public export
 122 | strengthen : LazyLst ne a -> Maybe $ LazyLst1 a
 123 | strengthen []      = Nothing
 124 | strengthen (x::xs) = Just $ x::xs
 125 | 
 126 | --- Functor ---
 127 | 
 128 | public export
 129 | Functor (LazyLst ne) where
 130 |   map f []      = []
 131 |   map f (x::xs) = f x :: map f xs
 132 | 
 133 | namespace NEHeteroOps
 134 | 
 135 |   public export
 136 |   bind : LazyLst nel a -> (a -> LazyLst ner b) -> LazyLst (nel && ner) b
 137 |   bind [] _ = []
 138 |   bind wh@(x::xs) f = do
 139 |     rewrite andCommutative nel ner
 140 |     let Just nxs = strengthen xs
 141 |       | Nothing => relaxAnd $ f x
 142 |     rewrite sym $ orSameNeutral ner
 143 |     relaxAnd $ f x ++ (assert_smaller wh nxs `bind` f)
 144 | 
 145 |   public export %inline
 146 |   bind' : LazyLst nel a -> LazyLst ner b -> LazyLst (nel && ner) b
 147 |   bind' xs ys = xs `bind` \_ => ys
 148 | 
 149 |   public export %inline
 150 |   join' : LazyLst nel (LazyLst ner a) -> LazyLst (nel && ner) a
 151 |   join' xs = xs `bind` id
 152 | 
 153 |   public export %inline
 154 |   ap : LazyLst nel (a -> b) -> LazyLst ner a -> LazyLst (nel && ner) b
 155 |   ap xs ys = xs `bind` (<$> ys)
 156 | 
 157 | public export %inline
 158 | Applicative (LazyLst ne) where
 159 |   pure x = [x]
 160 |   xs <*> ys = rewrite sym $ andSameNeutral ne in xs `ap` ys
 161 | 
 162 | public export %inline
 163 | Alternative LazyLst0 where
 164 |   empty = []
 165 |   (<|>) = (++)
 166 | 
 167 | public export %inline
 168 | Monad (LazyLst ne) where
 169 |   xs >>= f = rewrite sym $ andSameNeutral ne in xs `bind` f
 170 | 
 171 | --- Folds ---
 172 | 
 173 | public export
 174 | foldrLazy : (op : a -> Lazy b -> b) -> (init : Lazy b) -> LazyLst ne a -> b
 175 | foldrLazy _  init []      = init
 176 | foldrLazy op init (x::xs) = x `op` foldrLazy op init xs
 177 | 
 178 | public export
 179 | Foldable (LazyLst ne) where
 180 |   foldr c n []      = n
 181 |   foldr c n (x::xs) = c x (foldr c n xs)
 182 | 
 183 |   foldl f q []      = q
 184 |   foldl f q (x::xs) = foldl f (f q x) xs
 185 | 
 186 |   null []     = True
 187 |   null (_::_) = False
 188 | 
 189 |   foldlM op init []      = pure init
 190 |   foldlM op init (x::xs) = op init x >>= \next => foldlM op next xs
 191 | 
 192 |   toList []      = []
 193 |   toList (x::xs) = x :: toList xs
 194 | 
 195 |   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
 196 | 
 197 | public export
 198 | foldl1 : (a -> a -> a) -> LazyLst1 a -> a
 199 | foldl1 f (x::xs) = foldl f x xs
 200 | 
 201 | public export
 202 | foldr1 : (a -> Lazy a -> a) -> LazyLst1 a -> a
 203 | foldr1 op [x] = x
 204 | foldr1 op (x::xs@(y::ys)) = op x $ foldr1 op $ assert_smaller xs (y::ys)
 205 | 
 206 | public export
 207 | traverse_ : Monad m => (a -> m b) -> LazyLst ne a -> m Unit
 208 | traverse_ f = foldrLazy ((>>) . ignore . f) (pure ())
 209 | 
 210 | public export %inline
 211 | for_ : Monad m => LazyLst ne a -> (a -> m b) -> m Unit
 212 | for_ = flip Lazy.traverse_
 213 | 
 214 | public export %inline
 215 | sequence_ : Monad m => LazyLst ne (m a) -> m Unit
 216 | sequence_ = Lazy.traverse_ id
 217 | 
 218 | --- Picking ---
 219 | 
 220 | public export
 221 | head : LazyLst1 a -> a
 222 | head (x::_) = x
 223 | 
 224 | public export
 225 | head' : LazyLst ne a -> Maybe a
 226 | head' = map head . strengthen
 227 | 
 228 | public export
 229 | tail : LazyLst1 a -> LazyLst0 a
 230 | tail (_::xs) = relaxF xs
 231 | 
 232 | public export
 233 | tail' : LazyLst ne a -> Maybe $ LazyLst0 a
 234 | tail' = map tail . strengthen
 235 | 
 236 | public export
 237 | last : LazyLst1 a -> a
 238 | last [x]     = x
 239 | last wh@(_::(y::ys)) = last $ assert_smaller wh $ y::ys
 240 | 
 241 | public export
 242 | last' : LazyLst ne a -> Maybe a
 243 | last' = map last . strengthen
 244 | 
 245 | public export
 246 | init : LazyLst1 a -> LazyLst0 a
 247 | init [x] = []
 248 | init wh@(x::(y::ys)) = x :: init (assert_smaller wh $ y::ys)
 249 | 
 250 | public export
 251 | init' : LazyLst ne a -> Maybe $ LazyLst0 a
 252 | init' = map init . strengthen
 253 | 
 254 | -- Returns the longest first
 255 | public export
 256 | tails : LazyLst ne a -> LazyLst1 $ LazyLst0 a
 257 | tails []          = [ [] ]
 258 | tails xxs@(x::xs) = relaxF xxs :: tails (assert_smaller xxs xs)
 259 | 
 260 | -- Returns the longest first
 261 | public export
 262 | tails1 : LazyLst ne a -> LazyLst ne $ LazyLst1 a
 263 | tails1 [] = []
 264 | tails1 xxs@(x::xs) = (x::xs) :: case strengthen xs of
 265 |   Nothing  => []
 266 |   Just xs' => relaxF $ tails1 $ assert_smaller xxs xs'
 267 | 
 268 | -- Returns the shortest first
 269 | public export
 270 | inits : LazyLst ne a -> LazyLst1 $ LazyLst0 a
 271 | inits []      = [ [] ]
 272 | inits (x::xs) = [] :: ((x::) <$> inits xs)
 273 | 
 274 | -- Returns the shortest first
 275 | public export
 276 | inits1 : LazyLst ne a -> LazyLst ne $ LazyLst1 a
 277 | inits1 []      = []
 278 | inits1 (x::xs) = [x] :: ((x::) <$> inits1 xs)
 279 | 
 280 | --- Sublisting ---
 281 | 
 282 | public export
 283 | take : (n : Nat) -> LazyLst ne a -> LazyLst (ne && n /= 0) a
 284 | take Z     _       = rewrite andFalseFalse ne in []
 285 | take _     []      = []
 286 | take (S k) (x::xs) = x :: take k xs
 287 | 
 288 | public export
 289 | drop : (n : Nat) -> LazyLst ne a -> LazyLst0 a
 290 | drop Z     xs      = relaxF xs
 291 | drop (S _) []      = []
 292 | drop (S n) (_::xs) = drop n $ relaxF xs
 293 | 
 294 | public export
 295 | takeWhile : (a -> Bool) -> LazyLst ne a -> LazyLst0 a
 296 | takeWhile p []      = []
 297 | takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
 298 | 
 299 | public export
 300 | dropWhile : (a -> Bool) -> LazyLst ne a -> LazyLst0 a
 301 | dropWhile p []      = []
 302 | dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
 303 | 
 304 | --- Zippings ---
 305 | 
 306 | public export
 307 | Zippable (LazyLst ne) where
 308 |   zipWith _ [] _ = []
 309 |   zipWith _ _ [] = []
 310 |   zipWith f xxs@((x::xs) @{_} @{ine}) (y::ys) =
 311 |     (f x y :: zipWith f (assert_smaller xxs $ relaxF xs) (relaxF ys)) @{%search} @{ine}
 312 | 
 313 |   zipWith3 _ [] _ _ = []
 314 |   zipWith3 _ _ [] _ = []
 315 |   zipWith3 _ _ _ [] = []
 316 |   zipWith3 f xxs@((x::xs) @{_} @{ine}) (y::ys) (z::zs) =
 317 |     (f x y z :: zipWith3 f (assert_smaller xxs $ relaxF xs) (relaxF ys) (relaxF zs)) @{%search} @{ine}
 318 | 
 319 |   unzipWith  f xs = (xs <&> fst . f, xs <&> snd . f)
 320 |   unzipWith3 f xs = (xs <&> fst . f, xs <&> fst . snd . f, xs <&> snd . snd . f)
 321 | 
 322 | public export
 323 | zipWithStream : (a -> b -> c) -> Stream a -> LazyLst ne b -> LazyLst ne c
 324 | zipWithStream _ _       []      = []
 325 | zipWithStream f (x::xs) (y::ys) = f x y :: zipWithStream f xs ys
 326 | 
 327 | public export %inline
 328 | zipStream : Stream a -> LazyLst ne b -> LazyLst ne (a, b)
 329 | zipStream = zipWithStream (,)
 330 | 
 331 | --- Filtering ---
 332 | 
 333 | public export
 334 | filter : (a -> Bool) -> LazyLst ne a -> LazyLst0 a
 335 | filter _ []      = []
 336 | filter f (x::xs) = if f x then x :: filter f xs else filter f xs
 337 | 
 338 | public export
 339 | mapMaybe : (a -> Maybe b) -> LazyLst ne a -> LazyLst0 b
 340 | mapMaybe _ [] = []
 341 | mapMaybe f (x::xs) = case f x of
 342 |                        Just y  => y :: mapMaybe f xs
 343 |                        Nothing => mapMaybe f xs
 344 | 
 345 | --- External conversions ---
 346 | 
 347 | -- Foldable --
 348 | 
 349 | public export
 350 | fromFoldable : Foldable f => f a -> LazyLst0 a
 351 | fromFoldable = foldr (\x, xs => x :: xs) []
 352 | 
 353 | -- List --
 354 | 
 355 | public export
 356 | fromList : (xs : List a) -> LazyLst (not $ null xs) a
 357 | fromList []      = []
 358 | fromList (x::xs) = x :: fromList xs
 359 | 
 360 | public export
 361 | Cast (List a) (LazyLst0 a) where
 362 |   cast xs = relaxF $ fromList xs
 363 | 
 364 | -- LazyList --
 365 | 
 366 | public export
 367 | fromLazyList : (xs : LazyList a) -> LazyLst (not $ null xs) a
 368 | fromLazyList []      = []
 369 | fromLazyList (x::xs) = x :: fromLazyList xs
 370 | 
 371 | public export
 372 | Cast (LazyList a) (LazyLst0 a) where
 373 |   cast xs = relaxF $ fromLazyList xs
 374 | 
 375 | public export
 376 | toLazyList : LazyLst ne a -> LazyList a
 377 | toLazyList []      = []
 378 | toLazyList (x::xs) = x :: toLazyList xs
 379 | 
 380 | public export
 381 | Cast (LazyLst ne a) (LazyList a) where
 382 |   cast = toLazyList
 383 | 
 384 | -- Stream --
 385 | 
 386 | covering
 387 | public export
 388 | fromStream : Stream a -> LazyLst1 a
 389 | fromStream $ x::xs = x :: fromStream xs
 390 | 
 391 | --- Range syntax ---
 392 | 
 393 | -- not really lazy in its nature
 394 | public export %inline
 395 | rangeFromTo : Range a => a -> a -> LazyLst0 a
 396 | rangeFromTo l r = relaxF $ fromList $ rangeFromTo l r
 397 | 
 398 | -- not really lazy in its nature
 399 | public export %inline
 400 | rangeFromThenTo : Range a => a -> a -> a -> LazyLst0 a
 401 | rangeFromThenTo x y z = relaxF $ fromList $ rangeFromThenTo x y z
 402 | 
 403 | covering
 404 | public export %inline
 405 | rangeFrom : Range a => (0 _ : IfUnsolved ne True) => a -> LazyLst ne a
 406 | rangeFrom = relaxT . fromStream . rangeFrom
 407 | 
 408 | covering
 409 | public export %inline
 410 | rangeFromThen : Range a => (0 _ : IfUnsolved ne True) => a -> a -> LazyLst ne a
 411 | rangeFromThen = relaxT .: fromStream .: rangeFromThen
 412 | 
 413 | --- Showing ---
 414 | 
 415 | export
 416 | Show a => Show (LazyLst ne a) where
 417 |   show = show . toList
 418 | 
 419 | export
 420 | [DoNotEval] Show a => Show (LazyLst ne a) where
 421 |   show []     = "[]"
 422 |   show (x::_) = "\{show x} :: <lazy>"
 423 | 
 424 | --- Properties ---
 425 | 
 426 | -- type itself, inhabitance --
 427 | 
 428 | export
 429 | {0 xs : LazyLst _ _} -> {0 uns0 : _} -> {0 uns1 : _} ->
 430 | Uninhabited ([] = (::) @{uns0} @{uns1} x xs) where
 431 |   uninhabited Refl impossible
 432 | 
 433 | export
 434 | {0 xs : LazyLst _ _} -> {0 uns0 : _} -> {0 uns1 : _} ->
 435 | Uninhabited ((::) @{uns0} @{uns1} x xs = []) where
 436 |   uninhabited Refl impossible
 437 | 
 438 | -- If either head or tail is not propositionally equal, conses are not propositionally equal
 439 | export
 440 | {0 xs : LazyLst _ _} ->
 441 | {0 unsL0 : _} -> {0 unsL1 : _} ->
 442 | {0 unsR0 : _} -> {0 unsR1 : _} ->
 443 | Either (Uninhabited $ x === y) (Uninhabited $ xs === ys) =>
 444 | Uninhabited ((::) @{unsL0} @{unsL1} x xs === (::) @{unsR0} @{unsR1} y ys) where
 445 |   uninhabited @{Left  z} Refl = uninhabited @{z} Refl
 446 |   uninhabited @{Right z} Refl = uninhabited @{z} Refl
 447 | 
 448 | -- type itself, constructors --
 449 | 
 450 | export
 451 | Biinjective (with CheckedEmpty.List.Lazy.(::) \x, y => x :: y) where
 452 |   biinjective Refl = (Refl, Refl)
 453 | 
 454 | export
 455 | mapFusion : (g : b -> c) -> (f : a -> b) -> (xs : LazyLst ne a) -> map g (map f xs) = map (g . f) xs
 456 | mapFusion g f []      = Refl
 457 | mapFusion g f (x::xs) = rewrite mapFusion g f xs in Refl
 458 | 
 459 | export
 460 | mapExt : (xs : LazyLst ne _) -> ((x : _) -> f x = g x) -> map f xs = map g xs
 461 | mapExt []      _  = Refl
 462 | mapExt (x::xs) fg = rewrite fg x in cong (g x ::) $ mapExt _ fg
 463 |