
  0 | module TyTTP.Core.Context
  1 | 
  2 | import public Control.Monad.Trans
  3 | import TyTTP.Core.Request
  4 | import TyTTP.Core.Response
  5 | 
  6 | public export
  7 | record Context me u v h1 s h2 a b where
  8 |   constructor MkContext
  9 |   request : Request me u v h1 a
 10 |   response : Response s h2 b
 11 | 
 12 | export
 13 | Functor (Context me u v h1 s h2 a) where
 14 |   map f step = { response $= map f } step
 15 | 
 16 | export
 17 | Bifunctor (Context me u v h1 s h2) where
 18 |   bimap f g step = { request $= map f, response $= map g } step
 19 | 
 20 | export
 21 | infixr 0 :>
 22 | 
 23 | export
 24 | infixr 0 :>>
 25 | 
 26 | export
 27 | (:>) : MonadTrans t
 28 |   => Monad m
 29 |   => (f : (a -> (t m) b) -> c)
 30 |   -> (handler : a -> m b)
 31 |   -> c
 32 | (:>) f handler = f $ \a => lift $ handler a
 33 | 
 34 | export
 35 | (:>>) : MonadTrans t1
 36 |   => MonadTrans t2
 37 |   => Monad m
 38 |   => Monad (t1 m)
 39 |   => (f : (a -> (t2 (t1 m)) b) -> c)
 40 |   -> (handler : a -> m b)
 41 |   -> c
 42 | (:>>) f handler = f $ \a => lift $ lift $ handler a
 43 |