0 | module FS.Resource
 1 |
 2 | import public Control.Monad.MCancel
 3 | import public Control.Monad.Resource
 4 | import public FS.Pull
 5 |
 6 | %default total
 7 |
 8 | ||| Like `bracket`, but acquires the resource in the current scope.
 9 | export
10 | bracketWeak : (f es x) -> (x -> f [] ()) -> (x -> Pull f o es r) -> Pull f o es r
11 | bracketWeak acq cleanup g = acquire acq cleanup >>= g
12 |
13 | ||| Acquires a resource used for running a stream
14 | ||| making sure it is properly cleaned up once the stream terminates.
15 | export %inline
16 | bracket : (f es x) -> (x -> f [] ()) -> (x -> Pull f o es r) -> Pull f o es r
17 | bracket acq cl = newScope . bracketWeak acq cl
18 |
19 | ||| Makes sure the given cleanup action is run once the stream
20 | ||| terminates.
21 | |||
22 | ||| Like `finally` but does not create a new inner scope.
23 | export
24 | finallyWeak : Applicative (f es) => f [] () -> Pull f o es r -> Pull f o es r
25 | finallyWeak cleanup = bracketWeak (pure ()) (const cleanup) . const
26 |
27 | ||| Makes sure the given cleanup action is run once the stream
28 | ||| terminates.
29 | export
30 | finally : Applicative (f es) => f [] () -> Pull f o es r -> Pull f o es r
31 | finally cleanup = bracket (pure ()) (const cleanup) . const
32 |
33 | ||| Like `resource`, but acquires the resource in the current scope.
34 | export %inline
35 | resourceWeak :
36 |      {auto res : Resource f x}
37 |   -> (acquire : f es x)
38 |   -> (x -> Pull f o es r)
39 |   -> Pull f o es r
40 | resourceWeak acq = bracketWeak acq cleanup
41 |
42 | ||| Acquires a resource in a new scope, closing it once the scope is
43 | ||| cleaned up.
44 | export %inline
45 | resource :
46 |      {auto res : Resource f x}
47 |   -> (acquire : f es x)
48 |   -> (x -> Pull f o es r)
49 |   -> Pull f o es r
50 | resource acq = bracket acq cleanup
51 |
52 | export
53 | resourcesWeak :
54 |      {auto all : All (Resource f) rs}
55 |   -> (acquire : All (f es) rs)
56 |   -> (HList rs -> Pull f o es r)
57 |   -> Pull f o es r
58 | resourcesWeak @{_ :: _} (a::as) g =
59 |   resourceWeak a $ \r => resourcesWeak as (\res => g (r::res))
60 | resourcesWeak @{[]} [] g = g []
61 |
62 | export
63 | resources :
64 |      {auto all : All (Resource f) rs}
65 |   -> (acquire : All (f es) rs)
66 |   -> (HList rs -> Pull f o es r)
67 |   -> Pull f o es r
68 | resources acqs = newScope . resourcesWeak acqs
69 |