0 | module Data.CheckedEmpty.List
7 | import public Language.Implicits.IfUnsolved
14 | data Lst : (definitelyNotEmpty : Bool) -> Type -> Type where
16 | (::) : (0 _ : True `IfUnsolved` ine) => (0 _ : True `IfUnsolved` ne) =>
17 | a -> Lst ine a -> Lst ne a
19 | %name Lst
xs, ys, zs
23 | public export %inline
27 | public export %inline
34 | length : Lst ne a -> Nat
36 | length (_::xs) = S $
length xs
38 | public export %inline
39 | (.length) : Lst ne a -> Nat
40 | xs.length = length xs
43 | (++) : Lst nel a -> Lst ner a -> Lst (nel || ner) a
45 | (x::xs) ++ ys = x :: xs ++ ys
48 | Semigroup (Lst ne a) where
49 | xs <+> ys = rewrite sym $
orSameNeutral ne in xs ++ ys
52 | Monoid (Lst0 a) where
56 | index' : (xs : Lst ne a) -> Fin xs.length -> a
57 | index' (x::_ ) FZ = x
58 | index' (_::xs) (FS i) = index' xs i
60 | public export %inline
61 | index : Fin n -> (xs : Lst ne a) -> (0 _ : n = xs.length) => a
62 | index i xs @{Refl} = index' xs i
67 | iterateN : (n : Nat) -> (a -> a) -> a -> Lst (n /= 0) a
69 | iterateN (S n) f x = x :: iterateN n f x
72 | tabulateN : (n : Nat) -> (Fin n -> a) -> Lst (n /= 0) a
74 | tabulateN (S k) f = f FZ :: tabulateN k (f . FS)
77 | replicate : (n : Nat) -> a -> Lst (n /= 0) a
79 | replicate (S k) x = x :: replicate k x
83 | iterate : (a -> Maybe a) -> a -> Lst0 a
84 | iterate f x = x :: case f x of
86 | Just y => iterate f y
90 | unfoldr : (b -> Maybe (a, b)) -> b -> Lst0 a
91 | unfoldr f c = case f c of
93 | Just (a, n) => a :: unfoldr f n
100 | relaxF : Lst ne a -> Lst0 a
102 | relaxF (x::xs) = x::xs
104 | public export %inline
105 | relaxT : Lst1 a -> Lst ne a
106 | relaxT (x::xs) = x::xs
109 | relaxAnd : Lst ne a -> Lst (ne && nx) a
111 | relaxAnd (x::xs) = x::xs
113 | %transform "relaxF=id"
relaxF {ne} {a} = believe_me (\x => the (Lst ne a) x)
114 | %transform "relaxT=id"
relaxT {ne} {a} = believe_me (\x => the (Lst ne a) x)
115 | %transform "relaxAnd=id"
relaxAnd {ne} {a} = believe_me (\x => the (Lst ne a) x)
120 | strengthen : Lst ne a -> Maybe $
Lst1 a
121 | strengthen [] = Nothing
122 | strengthen (x::xs) = Just $
x::xs
127 | Functor (Lst ne) where
129 | map f (x::xs) = f x :: map f xs
131 | namespace NEHeteroOps
134 | bind : Lst nel a -> (a -> Lst ner b) -> Lst (nel && ner) b
136 | bind wh@(x::xs) f = do
137 | rewrite andCommutative nel ner
138 | let Just nxs = strengthen xs
139 | | Nothing => relaxAnd $
f x
140 | rewrite sym $
orSameNeutral ner
141 | relaxAnd $
f x ++ (assert_smaller wh nxs `bind` f)
143 | public export %inline
144 | bind' : Lst nel a -> Lst ner b -> Lst (nel && ner) b
145 | bind' xs ys = xs `bind` \_ => ys
147 | public export %inline
148 | join' : Lst nel (Lst ner a) -> Lst (nel && ner) a
149 | join' xs = xs `bind` id
151 | public export %inline
152 | ap : Lst nel (a -> b) -> Lst ner a -> Lst (nel && ner) b
153 | ap xs ys = xs `bind` (<$> ys)
155 | public export %inline
156 | Applicative (Lst ne) where
158 | xs <*> ys = rewrite sym $
andSameNeutral ne in xs `ap` ys
160 | public export %inline
161 | Alternative Lst0 where
163 | xs <|> ys = xs ++ ys
165 | public export %inline
166 | Monad (Lst ne) where
167 | xs >>= f = rewrite sym $
andSameNeutral ne in xs `bind` f
172 | foldrLazy : (op : a -> Lazy b -> b) -> (init : Lazy b) -> Lst ne a -> b
173 | foldrLazy _ init [] = init
174 | foldrLazy op init (x::xs) = x `op` foldrLazy op init xs
177 | Foldable (Lst ne) where
179 | foldr c n (x::xs) = c x (foldr c n xs)
182 | foldl f q (x::xs) = foldl f (f q x) xs
185 | null (_::_) = False
188 | toList (x::xs) = x :: toList xs
190 | foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
193 | foldl1 : (a -> a -> a) -> Lst1 a -> a
194 | foldl1 f (x::xs) = foldl f x xs
197 | foldr1 : (op : a -> Lazy a -> a) -> Lst1 a -> a
199 | foldr1 op xyys@(x::(y::ys)) = op x $
foldr1 op $
assert_smaller xyys $
y::ys
202 | Traversable (Lst ne) where
203 | traverse f [] = pure []
204 | traverse f (x::xs) = [| f x :: traverse f xs |]
209 | reverse : Lst ne a -> Lst ne a
211 | reverse (x::xs) = foldl (flip (::)) [x] xs
220 | head' : Lst ne a -> Maybe a
221 | head' = map head . strengthen
224 | tail : Lst1 a -> Lst0 a
225 | tail (_::xs) = relaxF xs
228 | tail' : Lst ne a -> Maybe $
Lst0 a
229 | tail' = map tail . strengthen
234 | last wh@(_::(y::ys)) = last $
assert_smaller wh $
y::ys
237 | last' : Lst ne a -> Maybe a
238 | last' = map last . strengthen
241 | init : Lst1 a -> Lst0 a
243 | init wh@(x::(y::ys)) = x :: init (assert_smaller wh $
y::ys)
246 | init' : Lst ne a -> Maybe $
Lst0 a
247 | init' = map init . strengthen
250 | unsnoc : Lst1 a -> (Lst0 a, a)
251 | unsnoc = go [] where
252 | go : (rev : Lst0 a) -> Lst1 a -> (Lst0 a, a)
253 | go rev xxs@(x::xs) = case strengthen xs of
254 | Nothing => (reverse rev, x)
255 | Just xs' => go (x::rev) $
assert_smaller xxs xs'
259 | tails : Lst ne a -> Lst1 $
Lst0 a
261 | tails xxs@(x::xs) = relaxF xxs :: tails (assert_smaller xxs xs)
265 | tails1 : Lst ne a -> Lst ne $
Lst1 a
267 | tails1 xxs@(x::xs) = (x::xs) :: case strengthen xs of
269 | Just xs' => relaxF $
tails1 $
assert_smaller xxs xs'
273 | inits : Lst ne a -> Lst1 $
Lst0 a
275 | inits (x::xs) = [] :: ((x::) <$> inits xs)
279 | inits1 : Lst ne a -> Lst ne $
Lst1 a
281 | inits1 (x::xs) = [x] :: ((x::) <$> inits1 xs)
286 | take : (n : Nat) -> Lst ne a -> Lst (ne && n /= 0) a
287 | take Z _ = rewrite andFalseFalse ne in []
289 | take (S k) (x::xs) = x :: take k xs
292 | drop : (n : Nat) -> Lst ne a -> Lst0 a
293 | drop Z xs = relaxF xs
295 | drop (S n) (_::xs) = drop n $
relaxF xs
298 | takeWhile : (a -> Bool) -> Lst ne a -> Lst0 a
299 | takeWhile p [] = []
300 | takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
303 | dropWhile : (a -> Bool) -> Lst ne a -> Lst0 a
304 | dropWhile p [] = []
305 | dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
310 | Zippable (Lst ne) where
311 | zipWith _ [] _ = []
312 | zipWith _ _ [] = []
313 | zipWith f xxs@((x::xs) @{_} @{ine}) (y::ys) =
314 | (f x y :: zipWith f (assert_smaller xxs $
relaxF xs) (relaxF ys)) @{%search} @{ine}
316 | zipWith3 _ [] _ _ = []
317 | zipWith3 _ _ [] _ = []
318 | zipWith3 _ _ _ [] = []
319 | zipWith3 f xxs@((x::xs) @{_} @{ine}) (y::ys) (z::zs) =
320 | (f x y z :: zipWith3 f (assert_smaller xxs $
relaxF xs) (relaxF ys) (relaxF zs)) @{%search} @{ine}
322 | unzipWith f [] = ([], [])
323 | unzipWith f (x::xs) = do
325 | let (ys, zs) = unzipWith f xs
328 | unzipWith3 f [] = ([], [], [])
329 | unzipWith3 f (x::xs) = do
330 | let (a, b, c) = f x
331 | let (as, bs, cs) = unzipWith3 f xs
332 | (a::as, b::bs, c::cs)
335 | zipWithStream : (a -> b -> c) -> Stream a -> Lst ne b -> Lst ne c
336 | zipWithStream _ _ [] = []
337 | zipWithStream f (x::xs) (y::ys) = f x y :: zipWithStream f xs ys
339 | public export %inline
340 | zipStream : Stream a -> Lst ne b -> Lst ne (a, b)
341 | zipStream = zipWithStream (,)
346 | filter : (a -> Bool) -> Lst ne a -> Lst0 a
348 | filter f (x::xs) = if f x then x :: filter f xs else filter f xs
351 | mapMaybe : (a -> Maybe b) -> Lst ne a -> Lst0 b
353 | mapMaybe f (x::xs) = case f x of
354 | Just y => y :: mapMaybe f xs
355 | Nothing => mapMaybe f xs
362 | fromFoldable : Foldable f => f a -> Lst0 a
363 | fromFoldable = foldr (::) []
368 | fromList : (xs : List a) -> Lst (not $
null xs) a
370 | fromList (x::xs) = x :: fromList xs
373 | Cast (List a) (Lst0 a) where
374 | cast xs = relaxF $
fromList xs
379 | fromList1 : List1 a -> Lst1 a
380 | fromList1 $
x:::xs = x :: fromList xs
383 | toList1 : Lst1 a -> List1 a
384 | toList1 $
x::xs = x ::: toList xs
387 | Cast (List1 a) (Lst True a) where
391 | Cast (Lst True a) (List1 a) where
397 | fromVect : Vect n a -> Lst (n /= Z) a
399 | fromVect (x::xs) = x :: fromVect xs
402 | Cast (Vect n a) (Lst (n /= Z) a) where
407 | public export %inline
408 | rangeFromTo : Range a => a -> a -> Lst0 a
409 | rangeFromTo l r = relaxF $
fromList $
rangeFromTo l r
411 | public export %inline
412 | rangeFromThenTo : Range a => a -> a -> a -> Lst0 a
413 | rangeFromThenTo x y z = relaxF $
fromList $
rangeFromThenTo x y z
418 | Show a => Show (Lst ne a) where
419 | show = show . toList
426 | {0 xs : Lst _ _} -> {0 uns0 : _} -> {0 uns1 : _} ->
427 | Uninhabited ([] = (::) @{uns0} @{uns1} x xs) where
428 | uninhabited Refl
impossible
431 | {0 xs : Lst _ _} -> {0 uns0 : _} -> {0 uns1 : _} ->
432 | Uninhabited ((::) @{uns0} @{uns1} x xs = []) where
433 | uninhabited Refl
impossible
437 | {0 xs : Lst _ _} ->
438 | {0 unsL0 : _} -> {0 unsL1 : _} ->
439 | {0 unsR0 : _} -> {0 unsR1 : _} ->
440 | Either (Uninhabited $
x === y) (Uninhabited $
xs === ys) =>
441 | Uninhabited ((::) @{unsL0} @{unsL1} x xs === (::) @{unsR0} @{unsR1} y ys) where
442 | uninhabited @{Left z} Refl = uninhabited @{z} Refl
443 | uninhabited @{Right z} Refl = uninhabited @{z} Refl
448 | Biinjective CheckedEmpty.List.(::) where
449 | biinjective Refl = (Refl, Refl)
454 | mapFusion : (g : b -> c) -> (f : a -> b) -> (xs : Lst ne a) -> map g (map f xs) = map (g . f) xs
455 | mapFusion g f [] = Refl
456 | mapFusion g f (x::xs) = rewrite mapFusion g f xs in Refl
459 | mapExt : (xs : Lst ne _) -> ((x : _) -> f x = g x) -> map f xs = map g xs
461 | mapExt (x::xs) fg = rewrite fg x in cong (g x ::) $
mapExt _ fg