0 | module Control.App
  1 |
  2 | import Data.IORef
  3 |
  4 | %default covering
  5 |
  6 | ||| `Error` is a type synonym for `Type`, specify for exception handling.
  7 | public export
  8 | Error : Type
  9 | Error = Type
 10 |
 11 | public export
 12 | data HasErr : Error -> List Error -> Type where
 13 |      Here : HasErr e (e :: es)
 14 |      There : HasErr e es -> HasErr e (e' :: es)
 15 |
 16 | ||| States whether the program's execution path is linear or might throw exceptions so that we can know
 17 | ||| whether it is safe to reference linear resources.
 18 | public export
 19 | data Path = MayThrow | NoThrow
 20 |
 21 | public export
 22 | data Usage = One | Any
 23 |
 24 | public export
 25 | 0 Has : List (a -> Type) -> a -> Type
 26 | Has [] es = ()
 27 | Has [e] es = e es
 28 | Has (e :: es') es = (e es, Has es' es)
 29 |
 30 | data OneOf : List Type -> Path -> Type where
 31 |      First : e -> OneOf (e :: es) MayThrow
 32 |      Later : OneOf es MayThrow -> OneOf (e :: es) MayThrow
 33 |
 34 | public export
 35 | data SafeBind : Path -> (l' : Path) -> Type where
 36 |      [search l']
 37 |      SafeSame : SafeBind l l
 38 |      SafeToThrow : SafeBind NoThrow MayThrow
 39 |
 40 | updateP : SafeBind p p' => OneOf es p -> OneOf es p'
 41 | updateP @{SafeSame} x = x
 42 | updateP @{SafeToThrow} x impossible
 43 |
 44 | Uninhabited (OneOf [] p) where
 45 |   uninhabited (First x) impossible
 46 |   uninhabited (Later x) impossible
 47 |
 48 | Uninhabited (OneOf es NoThrow) where
 49 |   uninhabited (First x) impossible
 50 |   uninhabited (Later x) impossible
 51 |
 52 | 0 execTy : Path -> List Error -> Type -> Type
 53 | execTy p es ty = Either (OneOf es p) ty
 54 |
 55 | data AppRes : Type -> Type where
 56 |      MkAppRes : (result : a) -> (1 x : %World) -> AppRes a
 57 |
 58 | data App1Res : Usage -> Type -> Type where
 59 |      MkApp1Res1 : (1 result : a) -> (1 x : %World) -> App1Res One a
 60 |      MkApp1ResW : (result : a) -> (1 x : %World) -> App1Res Any a
 61 |
 62 | PrimApp : Type -> Type
 63 | PrimApp a = (1 x : %World) -> AppRes a
 64 |
 65 | prim_app_pure : a -> PrimApp a
 66 | prim_app_pure = MkAppRes
 67 |
 68 | prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b
 69 | prim_app_bind fn k w
 70 |     = let MkAppRes x' w' = fn w in k x' w'
 71 |
 72 | toPrimApp : (1 act : IO a) -> PrimApp a
 73 | toPrimApp x
 74 |     = \w => case toPrim x w of
 75 |                  MkIORes r w => MkAppRes r w
 76 |
 77 | PrimApp1 : Usage -> Type -> Type
 78 | PrimApp1 u a = (1 x : %World) -> App1Res u a
 79 |
 80 | toPrimApp1 : {u : _} -> (1 act : IO a) -> PrimApp1 u a
 81 | toPrimApp1 x
 82 |     = \w => case toPrim x w of
 83 |                  MkIORes r w =>
 84 |                      case u of
 85 |                           One => MkApp1Res1 r w
 86 |                           Any => MkApp1ResW r w
 87 |
 88 | prim_app1_bind : (1 act : PrimApp1 Any a) ->
 89 |                  (1 k : a -> PrimApp1 u b) -> PrimApp1 u b
 90 | prim_app1_bind fn k w
 91 |     = let MkApp1ResW x' w' = fn w in k x' w'
 92 |
 93 | ||| A type supports throwing and catching exceptions. See `interface Exception err e` for details.
 94 | ||| @ l  An implicit Path states whether the program's execution path is linear or might throw
 95 | |||      exceptions. The default value is `MayThrow` which represents that the program might throw.
 96 | ||| @ es A list of exception types that can be thrown. Constrained interfaces can be defined by
 97 | |||      parameterising with a list of errors `es`.
 98 | export
 99 | data App : {default MayThrow l : Path} ->
100 |            (es : List Error) -> Type -> Type where
101 |      MkApp : (1 prog : (1 w : %World) -> AppRes (execTy l e t)) -> App {l} e t
102 |
103 | export
104 | data App1 : {default One u : Usage} ->
105 |             (es : List Error) -> Type -> Type where
106 |      MkApp1 : (1 prog : (1 w : %World) -> App1Res u t) -> App1 {u} e t
107 |
108 | bindApp : SafeBind l l' =>
109 |           App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
110 | bindApp (MkApp prog) next
111 |     = MkApp $ \world =>
112 |           let MkAppRes x' world' = prog world in
113 |               case x' of
114 |                    Right res =>
115 |                          let MkApp r = next res in
116 |                              r world'
117 |                    Left err => MkAppRes (Left (updateP err)) world'
118 |
119 | public export
120 | Cont1Type : Usage -> Type -> Usage -> List Error -> Type -> Type
121 | Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
122 | Cont1Type Any a u e b = (x : a) -> App1 {u} e b
123 |
124 | export
125 | bindApp1 : {u : _} -> (1 act : App1 {u} e a) ->
126 |            (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
127 | bindApp1 {u=One} (MkApp1 fn)
128 |     = \k => MkApp1 (\w => let MkApp1Res1 x' w' = fn w
129 |                               MkApp1 res = k x' in
130 |                               res w')
131 | bindApp1 {u=Any} (MkApp1 fn)
132 |     = \k => MkApp1 (\w => let MkApp1ResW x' w' = fn w
133 |                               MkApp1 res = k x' in
134 |                               res w')
135 |
136 | ||| When type is present in app "errors" list, app is allowed to perform I/O.
137 | public export
138 | data AppHasIO : Type where
139 |
140 | public export
141 | Uninhabited AppHasIO where
142 |   uninhabited _ impossible
143 |
144 | absurdWith1 : (1 w : b) -> OneOf e NoThrow -> any
145 | absurdWith1 w (First p) impossible
146 |
147 | absurdWithAppHasIO : (1 w : b) -> OneOf [AppHasIO] t -> any
148 | absurdWithAppHasIO w (First p) impossible
149 |
150 | absurdWith2 : (1 x : a) -> (1 w : b) -> OneOf e NoThrow -> any
151 | absurdWith2 x w (First p) impossible
152 |
153 | export
154 | bindL : App {l=NoThrow} e a -> (1 k : a -> App {l} e b) -> App {l} e b
155 | bindL (MkApp prog) next
156 |     = MkApp $ \world =>
157 |           let MkAppRes x' world' = prog world in
158 |               case x' of
159 |                    Right res =>
160 |                          let MkApp r = next res in
161 |                              r world'
162 |                    Left err => absurdWith2 next world' err
163 |
164 | export
165 | seqL : App {l=NoThrow} e () -> (1 k : App {l} e b) -> App {l} e b
166 | seqL ma mb = bindL ma (\ () => mb)
167 |
168 | export
169 | app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
170 | app (MkApp prog)
171 |     = MkApp1 $ \world =>
172 |           let MkAppRes x' world' = prog world in
173 |               case x' of
174 |                    Left err => absurdWith1 world' err
175 |                    Right res => MkApp1ResW res world'
176 |
177 | export
178 | app1 : (1 p : App1 {u=Any} e a) -> App {l} e a
179 | app1 (MkApp1 prog)
180 |     = MkApp $ \world =>
181 |           let MkApp1ResW x' world' = prog world in
182 |               MkAppRes (Right x') world'
183 |
184 | pureApp : a -> App {l} e a
185 | pureApp x = MkApp $ MkAppRes (Right x)
186 |
187 | export
188 | Functor (App {l} es) where
189 |   map f ap = bindApp ap $ \ap' => pureApp (f ap')
190 |
191 | export
192 | Applicative (App {l} es) where
193 |   pure = pureApp
194 |   (<*>) f a = bindApp f $ \f' =>
195 |               bindApp a $ \a' => pure (f' a')
196 |
197 | export
198 | Monad (App es) where
199 |   (>>=) = bindApp -- won't get used, but handy to have the instance
200 |
201 | export
202 | (>>=) : SafeBind l l' =>
203 |         App {l} e a -> (k : a -> App {l=l'} e b) -> App {l=l'} e b
204 | (>>=) = bindApp
205 |
206 | namespace App1
207 |   export
208 |   (>>=) : {u : _} -> (1 act : App1 {u} e a) ->
209 |           (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
210 |   (>>=) = bindApp1
211 |
212 |   delay : {u_act : _} -> (1 _ : App1 {u=u_k} e b) -> Cont1Type u_act () u_k e b
213 |   delay mb = case u_act of
214 |                   One => \ () => mb
215 |                   Any => \ _ => mb
216 |
217 |   export %inline
218 |   (>>) : {u_act : _} -> (1 _ : App1 {u=u_act} e ()) ->
219 |          (1 _ : App1 {u=u_k} e b) -> App1 {u=u_k} e b
220 |   ma >> mb = ma >>= delay mb
221 |
222 |   export
223 |   pure : (x : a) -> App1 {u=Any} e a
224 |   pure x =  MkApp1 $ MkApp1ResW x
225 |
226 |   export
227 |   pure1 : (1 x : a) -> App1 e a
228 |   pure1 x =  MkApp1 $ MkApp1Res1 x
229 |
230 | export
231 | data State : (tag : a) -> Type -> List Error -> Type where
232 |      [search tag]
233 |      MkState : IORef t -> State tag t e
234 |
235 | %hint export
236 | mapState : State tag t e -> State tag t (eff :: e)
237 | mapState (MkState s) = MkState s
238 |
239 | export
240 | get : (0 tag : _) -> State tag t e => App {l} e t
241 | get tag @{MkState r}
242 |     = MkApp $
243 |           prim_app_bind (toPrimApp $ readIORef r) $ \val =>
244 |           MkAppRes (Right val)
245 |
246 | export
247 | put : (0 tag : _) -> State tag t e => (val : t) -> App {l} e ()
248 | put tag @{MkState r} val
249 |     = MkApp $
250 |           prim_app_bind (toPrimApp $ writeIORef r val) $ \val =>
251 |           MkAppRes (Right ())
252 |
253 | export
254 | modify : (0 tag : _) -> State tag t e => (p : t -> t) -> App {l} e ()
255 | modify tag f
256 |     = let (>>=) = bindL in
257 |           do x <- get tag
258 |              put tag (f x)
259 |
260 | export
261 | new : t -> (p : State tag t e => App {l} e a) -> App {l} e a
262 | new val prog
263 |     = MkApp $
264 |          prim_app_bind (toPrimApp $ newIORef val) $ \ref =>
265 |             let st = MkState ref
266 |                 MkApp res = prog @{st} in
267 |                 res
268 |
269 | ||| An alias for `HasErr`.
270 | public export
271 | Exception : Error -> List Error -> Type
272 | Exception = HasErr
273 |
274 | findException : HasErr e es -> e -> OneOf es MayThrow
275 | findException Here err = First err
276 | findException (There p) err = Later $ findException p err
277 |
278 | findError : HasErr e es -> OneOf es MayThrow -> Maybe e
279 | findError Here (First err) = Just err
280 | findError (There p) (Later q) = findError p q
281 | findError _ _ = Nothing
282 |
283 | export
284 | throw : HasErr err es => err -> App es a
285 | throw err = MkApp $ MkAppRes (Left (findException %search err))
286 |
287 | export
288 | catch : HasErr err es => App es a -> (err -> App es a) -> App es a
289 | catch (MkApp prog) handler
290 |       = MkApp $
291 |            prim_app_bind prog $ \res =>
292 |               case res of
293 |                    Left err =>
294 |                         case findError %search err of
295 |                              Nothing => MkAppRes (Left err)
296 |                              Just err' =>
297 |                                   let MkApp e' = handler err' in
298 |                                       e'
299 |                    Right ok => MkAppRes (Right ok)
300 |
301 | export
302 | handle : App (err :: e) a ->
303 |          (onok : a -> App e b) ->
304 |          (onerr : err -> App e b) -> App e b
305 | handle (MkApp prog) onok onerr
306 |     = MkApp $
307 |            prim_app_bind prog $ \res =>
308 |              case res of
309 |                   Left (First err) =>
310 |                         let MkApp err' = onerr err in
311 |                             err'
312 |                   Left (Later p) =>
313 |                         -- different exception, so rethrow
314 |                         MkAppRes (Left p)
315 |                   Right ok =>
316 |                         let MkApp ok' = onok ok in
317 |                             ok'
318 |
319 | export
320 | lift : App e a -> App (err :: e) a
321 | lift (MkApp prog)
322 |     = MkApp $
323 |            prim_app_bind prog $ \res =>
324 |             case res of
325 |                  Left err => MkAppRes (Left (Later err))
326 |                  Right ok => MkAppRes (Right ok)
327 |
328 | public export
329 | Init : List Error
330 | Init = [AppHasIO]
331 |
332 | ||| The only way provided by `Control.App` to run an App.
333 | ||| @ Init A concrete list of errors.
334 | export
335 | run : App {l} Init a -> IO a
336 | run (MkApp prog)
337 |     = primIO $ \w =>
338 |            case (prim_app_bind prog $ \r =>
339 |                    case r of
340 |                         Right res => MkAppRes res
341 |                         Left (First err) => absurd err) w of
342 |                 MkAppRes r w => MkIORes r w
343 |
344 | export
345 | noThrow : App Init a -> App Init {l=NoThrow} a
346 | noThrow (MkApp prog)
347 |     = MkApp $ \w =>
348 |               case prog w of
349 |                    MkAppRes (Left err) w => absurdWithAppHasIO w err
350 |                    MkAppRes (Right res) w => MkAppRes (Right res) w
351 |
352 | public export
353 | interface PrimIO e where
354 |   primIO : IO a -> App {l} e a
355 |   primIO1 : (1 act : IO a) -> App1 e a
356 |   -- fork starts a new environment, so that any existing state can't get
357 |   -- passed to it (since it'll be tagged with the wrong environment)
358 |   fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()
359 |
360 | export
361 | HasErr AppHasIO e => PrimIO e where
362 |   primIO op =
363 |         MkApp $ \w =>
364 |             let MkAppRes r w = toPrimApp op w in
365 |                 MkAppRes (Right r) w
366 |
367 |   primIO1 op = MkApp1 $ toPrimApp1 op
368 |
369 |   fork thread
370 |       = MkApp $
371 |             prim_app_bind
372 |                 (toPrimApp $ Prelude.fork $
373 |                       do run thread
374 |                          pure ())
375 |                     $ \_ =>
376 |                MkAppRes (Right ())
377 |
378 | export
379 | new1 :  t -> (1 p : State tag t e => App1 {u} e a) -> App1 {u} e a
380 | new1 val prog
381 |     = MkApp1 $ prim_app1_bind (toPrimApp1 $ newIORef val) $ \ref =>
382 |         let st = MkState ref
383 |             MkApp1 res = prog @{st} in
384 |             res
385 |
386 | public export
387 | data FileEx = GenericFileEx Int -- errno
388 |             | FileReadError
389 |             | FileWriteError
390 |             | FileNotFound
391 |             | PermissionDenied
392 |             | FileExists
393 |
394 | export
395 | Show FileEx where
396 |   show (GenericFileEx errno) = "File error: " ++ show errno
397 |   show FileReadError = "File Read Error"
398 |   show FileWriteError = "File Write Error"
399 |   show FileNotFound = "File Not Found"
400 |   show PermissionDenied = "Permission Denied"
401 |   show FileExists = "File Exists"
402 |
403 | public export
404 | data IOError
405 |      = GenericErr String
406 |      | FileErr FileEx
407 |
408 | export
409 | Show IOError where
410 |   show (GenericErr str) = "IO error: " ++ str
411 |   show (FileErr f) = "File error: " ++ show f
412 |