
  0 | module Control.Monad.Resource
  1 | 
  2 | import Control.Monad.MCancel
  3 | import Control.Monad.MErr
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | interface Resource (0 f : List Type -> Type -> Type) (0 a : Type) | a where
  9 |   cleanup : a -> f [] ()
 10 | 
 11 | ||| Allocate a resource, use it in a program, and make sure to release it
 12 | ||| afterwards.
 13 | export %inline
 14 | use1 : MCancel f => Resource f a => f es a -> (a -> f es b) -> f es b
 15 | use1 alloc act = bracket alloc act cleanup
 16 | 
 17 | ||| Like `use1` but for a heterogeneous list of resources.
 18 | export
 19 | use :
 20 |      {auto all : All (Resource f) ts}
 21 |   -> {auto can : MCancel f}
 22 |   -> (allocs   : All (f es) ts)
 23 |   -> (act      : HList ts -> f es b)
 24 |   -> f es b
 25 | use @{[]}   []     act = act []
 26 | use @{_::_} (h::t) act = use1 h (\r => use t (act . (r::)))
 27 |