0 | module Stellar.API.Maybe
  1 |
  2 | import Stellar.API.Definition
  3 | import Stellar.API.Morphism
  4 | import Stellar.API.Interface
  5 | import public Data.Maybe.Any
  6 | import public Data.Maybe.All
  7 | import Data.Product
  8 | import Data.Coproduct
  9 |
 10 | %hide Prelude.Ops.infixl.(>>)
 11 | %hide Prelude.Ops.infixl.(|>)
 12 |
 13 | %default total
 14 |
 15 | maybeJoin : Maybe (Maybe a) -> Maybe a
 16 | maybeJoin (Just x) = x
 17 | maybeJoin Nothing = Nothing
 18 |
 19 | %hide Prelude.(>=>)
 20 | ----------------------------------------------------------------------------------
 21 | -- Ignore errors
 22 | ----------------------------------------------------------------------------------
 23 | namespace Any
 24 |
 25 |   public export
 26 |   Maybe : API -> API
 27 |   Maybe a = (x : Maybe a.message) !> Any a.response x
 28 |
 29 |   export
 30 |   map_Maybe : a =&> b -> Any.Maybe a =&> Any.Maybe b
 31 |   map_Maybe m =
 32 |     !! \case Nothing => Nothing ## absurd
 33 |              (Just x) => let x1 ## x2 = m.continuation x
 34 |                           in Just x1 ## Here . x2 . extract
 35 |
 36 |   AnyJoin : {0 a : API} -> (x : Maybe (Maybe (a .message))) -> Any (a .response) (maybeJoin x) -> Any (Any (a .response)) x
 37 |   AnyJoin Nothing y = absurd y
 38 |   AnyJoin (Just x) y = Here y
 39 |
 40 |   export
 41 |   maybeAnyJoin : Any.Maybe (Any.Maybe a) =&> Any.Maybe a
 42 |   maybeAnyJoin = !! \x => maybeJoin x ## AnyJoin x
 43 |
 44 |   export
 45 |   nothing : a =&> Any.Maybe b
 46 |   nothing = !! \x => Nothing ## absurd
 47 |
 48 |   public export
 49 |   distribMaybe : Monad m => Lift m (Any.Maybe a) =&> Any.Maybe (Lift m a)
 50 |   distribMaybe =
 51 |     !! \case Nothing => Nothing ## absurd
 52 |              (Just x) => Just x ## \v => extract v >>= (pure . Any.Here)
 53 |
 54 |   export
 55 |   implementation APIFunctor (=&>) Any.Maybe where
 56 |     map = map_Maybe
 57 |
 58 |   export
 59 |   implementation APIPointed (=&>) Any.Maybe where
 60 |     pure = !! \x => Just x ## extract
 61 |
 62 |   export
 63 |   implementation APIMonad (=&>) Any.Maybe where
 64 |     join = maybeAnyJoin
 65 |
 66 |   export
 67 |   implementation APIBifunctor (=&>) (*) where
 68 |     bimap f g = !! \x => let f1 ## k = f.continuation x.π1
 69 |                            ; g1 ## l = g.continuation x.π2
 70 |                          in (f1 && g1) ## Prelude.bimap k l
 71 |
 72 |   export
 73 |   implementation Cartesian (=&>) (*) where
 74 |     (&&&) p1 p2 = !! \x => let x1 ## y1 = p1.continuation x
 75 |                                x2 ## y2 = p2.continuation x
 76 |                             in (x1 && x2) ## choice y1 y2
 77 |     fst = !! \x => x.π1 ## (<+)
 78 |     snd = !! \x => x.π2 ## (+>)
 79 |
 80 |   export
 81 |   implementation APIAlternative (=&>) (*) Any.Maybe where
 82 |     err = nothing
 83 |     firstSuccess = !! \case (Just x && _) => Just x ## (<+)
 84 |                             (Nothing && y) => y ## (+>)
 85 |
 86 | --   export
 87 | --   kleisli : a =&> Any.Maybe b -> b =&> Any.Maybe c -> a =&> Any.Maybe c
 88 | --   kleisli m1 m2 = m1 >=> m2
 89 |
 90 | public export
 91 | strength : ((Any.Maybe x) // y) =&> (Any.Maybe (x // y))
 92 | strength =
 93 |   !! \case (Nothing && p2) => Nothing ## absurd
 94 |            ((Just p1) && p2) => Just (p1 && p2) ## \(Here v) => Here v.π1 && v.π2
 95 |
 96 | ----------------------------------------------------------------------------------
 97 | -- Handle errors
 98 | ----------------------------------------------------------------------------------
 99 |
100 | namespace All
101 |
102 |   public export
103 |   Maybe : API -> API
104 |   Maybe a = (x : Maybe a.message) !> All a.response x
105 |
106 |   public export
107 |   distribMaybe : Monad m => Lift m (All.Maybe a) =&> All.Maybe (Lift m a)
108 |   distribMaybe =
109 |     !! \case Nothing => Nothing ## \[] => pure []
110 |              (Just x) => Just x ## map Value . (.value)
111 |
112 |   public export
113 |   map_Maybe : a =&> b -> All.Maybe a =&> All.Maybe b
114 |   map_Maybe m =
115 |     !! \case Nothing => Nothing ## \[] => []
116 |              (Just x) => let x1 ## x2 = m.continuation x in Just x1 ## app x2
117 |
118 |   public export
119 |   AllToAnyTypes : forall a. (x : Maybe a.message) -> Any a.response x -> All a.response x
120 |   AllToAnyTypes Nothing (Here x) impossible
121 |   AllToAnyTypes (Just x) (Here y) = Value y
122 |
123 |   public export
124 |   AnyToAll : forall a. All.Maybe a =&> Any.Maybe a
125 |   AnyToAll = !! \x => x ## \(Here y) => Value y
126 |
127 |   AllJoin : {0 a : API} -> (x : Maybe (Maybe a.message)) -> All a.response (maybeJoin x) -> All (All a.response) x
128 |   AllJoin Nothing y = []
129 |   AllJoin (Just x) y = Value y
130 |
131 |   export
132 |   maybeAllJoin : All.Maybe (All.Maybe a) =&> All.Maybe a
133 |   maybeAllJoin = !! \x => maybeJoin x ## AllJoin x
134 |
135 |   export
136 |   maybeEnd : All.Maybe End =&> End
137 |   maybeEnd = !! \x => () ## const (fromMaybe id x)
138 |
139 |   export
140 |   implementation APIFunctor (=&>) All.Maybe where
141 |     map = map_Maybe
142 |
143 |   export
144 |   implementation APIPointed (=&>) All.Maybe where
145 |     pure = !! \x => Just x ## (.value)
146 |
147 |   export
148 |   implementation APIMonad (=&>) All.Maybe where
149 |     join = maybeAllJoin
150 |
151 |   export
152 |   kleisli : a =&> All.Maybe b -> b =&> All.Maybe c -> a =&> All.Maybe c
153 |   kleisli m1 m2 = (m1 >=> m2) {f = All.Maybe}
154 |
155 | ||| Given a default output, we can convert from `Any.Maybe` to `All.Maybe`
156 | export
157 | AnyToAll : (defOutput : (x : a.message) -> a.response x) -> a =&> Any.Maybe b -> a =&> All.Maybe b
158 | AnyToAll defout m = !! \x =>
159 |     case m.continuation x of
160 |          (Just x ## y) =>  Just x ## (\z => y (Here z.value))
161 |          (Nothing ## y) => Nothing ## (const (defout x))
162 |