
  0 | module Data.Container.Maybe
  1 | 
  2 | import Data.Container.Morphism
  3 | 
  4 | public export
  5 | maybeMap : (a -> b) -> Maybe a -> Maybe b
  6 | maybeMap f (Just x) = Just (f x)
  7 | maybeMap f Nothing = Nothing
  8 | 
  9 | public export
 10 | maybeJoin : Maybe (Maybe x) -> Maybe x
 11 | maybeJoin (Just (Just v)) = Just v
 12 | maybeJoin _ = Nothing
 13 | 
 14 | public export
 15 | data All : (x -> Type) -> Maybe x -> Type where
 16 |   Nah : All pred Nothing
 17 |   Aye : {v : x} -> pred v -> All pred (Just v)
 18 | 
 19 | public export
 20 | obtain : All p (Just a) -> p a
 21 | obtain (Aye x) = x
 22 | 
 23 | public export
 24 | MaybeAllIdris : Container -> Container
 25 | MaybeAllIdris c = (!>) (Maybe c.req) (All c.res)
 26 | 
 27 | public export
 28 | maybeAllPure : (x : Container) -> x =%> MaybeAllIdris x
 29 | maybeAllPure _ = Just <| \x, y => obtain y
 30 | 
 31 | public export
 32 | maybeAllJoinBwd : (x : Maybe (Maybe a)) -> All f (Maybe.maybeJoin x) -> All (All f) x
 33 | maybeAllJoinBwd (Just (Just v)) (Aye y) = Aye (Aye y)
 34 | maybeAllJoinBwd (Just Nothing) b = Aye Nah
 35 | maybeAllJoinBwd Nothing b = Nah
 36 | 
 37 | public export
 38 | maybeAllJoin : (x : Container) -> MaybeAllIdris (MaybeAllIdris x) =%> MaybeAllIdris x
 39 | maybeAllJoin _ =  maybeJoin <| maybeAllJoinBwd
 40 | 
 41 | public export
 42 | bwdMaybeAllF: {0 x, y : Container} -> {mor : x =%> y} -> (v : Maybe x.req) ->
 43 |               All y.res (maybeMap mor.fwd v) -> All x.res v
 44 | bwdMaybeAllF Nothing Nah = Nah
 45 | bwdMaybeAllF (Just v) (Aye z) = Aye (mor.bwd v z)
 46 | 
 47 | public export
 48 | MaybeAllIdrisFunctor : a =%> b -> MaybeAllIdris a =%> MaybeAllIdris b
 49 | MaybeAllIdrisFunctor x = maybeMap x.fwd <| bwdMaybeAllF
 50 |