
  0 | module Control.Eff.Internal
  1 | 
  2 | import public Control.MonadRec
  3 | import public Control.Monad.Free
  4 | import public Data.Union
  5 | import public Data.Subset
  6 | 
  7 | %default total
  8 | 
  9 | ||| An effectful computation yielding a value
 10 | ||| of type `t` and supporting the effects listed
 11 | ||| in `fs`.
 12 | public export
 13 | Eff : (fs : List (Type -> Type)) -> (t : Type) -> Type
 14 | Eff fs = Free (Union fs)
 15 | 
 16 | ||| Lift a an effectful comutation into the `Eff` monad.
 17 | export
 18 | send : Has f fs => f t -> Eff fs t
 19 | send = lift . inj
 20 | 
 21 | ||| Handle all effectful computations in `m`,
 22 | ||| returning the underlying free monad.
 23 | export
 24 | toFree : Eff fs t -> Handler fs m -> Free m t
 25 | toFree eff h = mapK (handleAll h) eff
 26 | 
 27 | ||| Run an effectful computation without overflowing
 28 | ||| the stack by handling all computations in monad `m`.
 29 | export
 30 | runEff : MonadRec m => Eff fs t -> Handler fs m -> m t
 31 | runEff eff h = foldMap (handleAll h) eff
 32 | 
 33 | ||| Extract the (pure) result of an effectful computation
 34 | ||| where all effects have been handled.
 35 | export
 36 | extract : Eff [] a -> a
 37 | extract fr = case toView fr of
 38 |   Pure val => val
 39 |   Bind u _ => absurd u
 40 | 
 41 | export
 42 | handleRelay :
 43 |      {auto prf : Has f fs}
 44 |   -> (a -> Eff (fs - f) b)
 45 |   -> (forall v . f v -> (v -> Eff (fs - f) b) -> Eff (fs - f) b)
 46 |   -> Eff fs a
 47 |   -> Eff (fs - f) b
 48 | handleRelay fval fcont fr = case toView fr of
 49 |   Pure val => fval val
 50 |   Bind x g => case decomp {prf} x of
 51 |     Left y  => assert_total $ lift y >>= handleRelay fval fcont . g
 52 |     Right y => assert_total $ fcont y (handleRelay fval fcont . g)
 53 | 
 54 | export
 55 | handle :
 56 |      {auto prf : Has f fs}
 57 |   -> (forall v . f v -> (resume: v -> Eff (fs - f) b) -> Eff (fs - f) b)
 58 |   -> Eff fs b
 59 |   -> Eff (fs - f) b
 60 | handle fcont fr = handleRelay pure fcont fr
 61 | 
 62 | export
 63 | handleRelayS :
 64 |      {auto prf : Has f fs}
 65 |   -> s
 66 |   -> (s -> a -> Eff (fs - f) b)
 67 |   -> (forall v . s -> f v -> (s -> v -> Eff (fs - f) b) -> Eff (fs - f) b)
 68 |   -> Eff fs a
 69 |   -> Eff (fs - f) b
 70 | handleRelayS vs fval fcont fr = case toView fr of
 71 |   Pure val => fval vs val
 72 |   Bind x g => case decomp {prf} x of
 73 |     Left y  => assert_total $ lift y >>= handleRelayS vs fval fcont . g
 74 |     Right y => assert_total $ fcont vs y (\vs2 => handleRelayS vs2 fval fcont . g)
 75 | 
 76 | 
 77 | ||| Turn effect monad into a more relaxed one. Can be used to reorder effects as well. See src/Test/Ordering.idr for usage.
 78 | export
 79 | lift : Subset fs fs' => Eff fs a -> Eff fs' a
 80 | lift @{s} fr = case toView fr of
 81 |   Pure val => pure val
 82 |   Bind x g => do
 83 |     let mx := weaken @{s} x
 84 |     freex <- lift mx
 85 |     lift (assert_smaller fr (g freex))
 86 |