
  0 | module Data.Alternative
  1 | 
  2 | %default total
  3 | 
  4 | -------------------------------
  5 | --- `Alternative` utilities ---
  6 | -------------------------------
  7 | 
  8 | public export %inline
  9 | atLeast : Alternative f => a -> f a -> f a
 10 | atLeast v = (<|> pure v)
 11 | 
 12 | public export %inline
 13 | optional : Alternative f => f a -> f (Maybe a)
 14 | optional = atLeast Nothing . map Just
 15 | 
 16 | -- `whenT b x` ~ `guard b $> x`
 17 | public export
 18 | whenT : Alternative f => Bool -> Lazy a -> f a
 19 | whenT True  x = pure x
 20 | whenT False _ = empty
 21 | 
 22 | public export
 23 | whenTs : Alternative f => Bool -> f a -> f a
 24 | whenTs True  x = x
 25 | whenTs False _ = empty
 26 | 
 27 | public export
 28 | whenJ : Alternative f => Maybe a -> (a -> b) -> f b
 29 | whenJ Nothing  _ = empty
 30 | whenJ (Just x) g = pure $ g x
 31 | 
 32 | public export
 33 | whenJs : Alternative f => Maybe a -> (a -> f b) -> f b
 34 | whenJs Nothing  _ = empty
 35 | whenJs (Just x) g = g x
 36 | 
 37 | public export
 38 | foldAlt : Alternative f => (a -> f b) -> List a -> f b
 39 | foldAlt _ []      = empty
 40 | foldAlt f (x::xs) = f x <|> foldAlt f xs
 41 | 
 42 | public export %inline
 43 | foldAlt' : Alternative f => List a -> (a -> f b) -> f b
 44 | foldAlt' = flip foldAlt
 45 |