-
Notifications
You must be signed in to change notification settings - Fork 4
/
SMTPool.hs
64 lines (56 loc) · 2.17 KB
/
SMTPool.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
{-# LANGUAGE ExistentialQuantification,FlexibleContexts #-}
module SMTPool where
import Language.SMTLib2.Internals.Backend
import Language.SMTLib2.Internals.Monad
import Data.Pool
import Control.Exception
import Control.Monad.State.Strict
import qualified Data.Set as Set
data SMTInstance info b = SMTInstance { instanceState :: SMTState b
, instanceInfo :: info b
}
data SMTPool info = forall b. (Backend b,SMTMonad b ~ IO)
=> SMTPool (Pool (SMTInstance info b))
newtype PoolVars a b = PoolVars (a (Expr b))
createSMTPool :: (Backend b,SMTMonad b ~ IO)
=> IO b
-> SMT b (info b)
-> IO (SMTPool info)
createSMTPool createBackend (SMT info)
= fmap SMTPool $
createPool (do
b <- createBackend
let st0 = SMTState b Set.empty
(info',st1) <- (runStateT info st0) `onException`
(exit b)
return $ SMTInstance st1 info')
(\(SMTInstance { instanceState = st }) -> exit (backend st) >> return ())
1 5 10
withSMTPool :: SMTPool info
-> (forall b. Backend b => info b -> SMT b c)
-> IO c
withSMTPool pool act = do
Right res <- withSMTPool' pool
(\info -> do
res <- act info
return (Right (res,info)))
return res
withSMTPool' :: SMTPool info
-> (forall b. Backend b => info b -> SMT b (Either c (r,info b)))
-> IO (Either c r)
withSMTPool' (SMTPool pool) act = do
(inst@SMTInstance { instanceState = st0
, instanceInfo = info },local) <- takeResource pool
(do
let SMT act' = act info
(res,st1) <- (runStateT act' st0) `onException`
(exit $ backend st0)
case res of
Left x -> do
destroyResource pool local inst
return (Left x)
Right (res,info') -> do
putResource local (SMTInstance { instanceState = st1
, instanceInfo = info' })
return (Right res))
`onException` (destroyResource pool local inst)