
  0 | module IO.Async.Resource
  1 | 
  2 | import Data.List.Quantifiers.Extra
  3 | import IO.Async.Fiber
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | interface Resource a where
  9 |   release : HasIO io => a -> io ()
 10 | 
 11 | export
 12 | useMany :
 13 |      {auto rs : All Resource ts}
 14 |   -> All (Async es) ts
 15 |   -> (HList ts -> Async es a)
 16 |   -> Async es a
 17 | useMany           []        f = f []
 18 | useMany @{_ :: _} (v :: vs) f =
 19 |   bracket v (\rv => useMany vs $ f . (rv::)) release
 20 | 
 21 | export %inline
 22 | use1 : Resource v => Async es v -> (v -> Async es a) -> Async es a
 23 | use1 x f = bracket x f release
 24 |