
  0 | module Control.Eff.Reader
  1 | 
  2 | import Control.Eff.Internal
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | data ReaderL : (lbl : k) -> (env : Type) -> (a : Type) -> Type where
  8 |   [search lbl]
  9 |   Ask : ReaderL lbl env env
 10 | 
 11 | public export
 12 | Reader : (env,a : Type) -> Type
 13 | Reader = ReaderL ()
 14 | 
 15 | export
 16 | askAt : (0 lbl : k) -> Has (ReaderL lbl env) fs => Eff fs env
 17 | askAt lbl = send $ Ask {lbl}
 18 | 
 19 | export %inline
 20 | ask : Has (Reader env) fs => Eff fs env
 21 | ask = askAt ()
 22 | 
 23 | export %inline
 24 | asksAt : (0 lbl : k) -> Has (ReaderL lbl env) fs => (env -> a) -> Eff fs a
 25 | asksAt lbl f = f <$> askAt lbl
 26 | 
 27 | export %inline
 28 | asks : Has (Reader env) fs => (env -> a) -> Eff fs a
 29 | asks f = f <$> ask
 30 | 
 31 | --------------------------------------------------------------------------------
 32 | --          Running Reader
 33 | --------------------------------------------------------------------------------
 34 | 
 35 | export
 36 | handleReader :
 37 |      {0 m : Type -> Type}
 38 |   -> m env
 39 |   -> ReaderL lbl env a
 40 |   -> m a
 41 | handleReader x Ask = x
 42 | 
 43 | unReader : env -> ReaderL lbl env a -> a
 44 | unReader ve Ask = ve
 45 | 
 46 | export
 47 | runReaderAt :
 48 |      (0 lbl : k)
 49 |   -> {auto _ : Has (ReaderL lbl env) fs}
 50 |   -> env
 51 |   -> Eff fs t
 52 |   -> Eff (fs - ReaderL lbl env) t
 53 | runReaderAt _ ve = handleRelay pure $ \v,f => f (unReader ve v)
 54 | 
 55 | export %inline
 56 | runReader : Has (Reader env) fs => env -> Eff fs t -> Eff (fs - Reader env) t
 57 | runReader = runReaderAt ()
 58 |