stm-promise: Simple STM Promises for IO computations and external processes
Simple STM Promises for IO computations and external processes. Experimental release.
Example with running the theorem prover eprover in parallel. Given this file structure:
├── mul-commutative │ ├── induction_x_0.tptp │ ├── induction_x_1.tptp │ ├── induction_x_y_0.tptp │ ├── induction_x_y_1.tptp │ ├── induction_x_y_2.tptp │ ├── induction_x_y_3.tptp │ ├── induction_y_0.tptp │ ├── induction_y_1.tptp │ └── no_induction_0.tptp └── plus-commutative ├── induction_x_0.tptp ├── induction_x_1.tptp ├── induction_x_y_0.tptp ├── induction_x_y_1.tptp ├── induction_x_y_2.tptp ├── induction_x_y_3.tptp ├── induction_y_0.tptp ├── induction_y_1.tptp └── no_induction_0.tptp
We can capture these different obligations and goals with a Control.Concurrent.STM.Promise.Tree.Tree
.
file_tree :: Tree FilePath file_tree = fmap (++ ".tptp") $ tryAll [ fmap ("mul-commutative/" ++) $ requireAny [ fmap ("induction_x_" ++) $ requireAll $ map Leaf ["0","1"] , fmap ("induction_y_" ++) $ requireAll $ map Leaf ["0","1"] , fmap ("induction_x_y_" ++) $ requireAll $ map Leaf ["0","1","2","3"] , Leaf "no_induction_0" ] , fmap ("plus-commutative/" ++) $ requireAny [ fmap ("induction_x_" ++) $ requireAll $ map Leaf ["0","1"] , fmap ("induction_y_" ++) $ requireAll $ map Leaf ["0","1"] , fmap ("induction_x_y_" ++) $ requireAll $ map Leaf ["0","1","2","3"] , Leaf "no_induction_0" ] ]
A successful invocation either contains Theorem
or Unsatisfiable
.
success :: ProcessResult -> Bool success r = excode r == ExitSuccess && any (`isInfixOf` stdout r) ok where ok = ["Theorem","Unsatisfiable"]
Making a promise for an eprover process:
eproverPromise :: FilePath -> IO (Promise [(FilePath,Bool)]) eproverPromise file = do let args = ["-xAuto","-tAuto",'-':"-tptp3-format","-s"] promise <- processPromise "eprover" (file : args) "" let chres :: ProcessResult -> [(FilePath,Bool)] chres r = [ (file,success r) ] return $ fmap chres promise
Evaluate this in parallel, with a 1 second timeout for each invocation:
main :: IO () main = do promise_tree <- mapM eproverPromise file_tree let timeout = 1000 * 1000 -- microseconds processes = 2 workers (Just timeout) processes (interleave promise_tree) (_,res) <- evalTree (any (not . snd)) promise_tree putStrLn "Results: " mapM_ print res
The result of this run is:
Results: ("plus-commutative/induction_x_y_0.tptp",True) ("plus-commutative/induction_x_y_1.tptp",True) ("plus-commutative/induction_x_y_2.tptp",True) ("plus-commutative/induction_x_y_3.tptp",True)
This means that four out of four obligations for commutativity of plus succeeded when doing induction on both x and y.
Modules
[Index]
Downloads
- stm-promise-0.0.3.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 0.0.1, 0.0.1.1, 0.0.2, 0.0.3.0, 0.0.3.1 |
---|---|
Dependencies | base (>=4 && <5), mtl (>=2.1.2 && <3), process (>=1.0.1.1 && <2), stm (>=2.3 && <3), unix (>=2.5) [details] |
License | LGPL-3.0-only |
Author | Dan Rosén |
Maintainer | Dan Rosén <danr@chalmers.se> |
Category | Concurrency |
Home page | http://www.github.com/danr/stm-promise |
Bug tracker | http://www.github.com/danr/stm-promise/issues |
Source repo | head: git clone git://github.com/danr/stm-promise.git |
Uploaded | by DanRosen at 2014-10-13T15:53:58Z |
Distributions | |
Reverse Dependencies | 1 direct, 0 indirect [details] |
Downloads | 4055 total (10 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs uploaded by user Build status unknown [no reports yet] |