The stm-promise package

[Tags: lgpl, library]

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.


Properties

Versions0.0.1, 0.0.1.1, 0.0.2
Dependenciesbase (==4.*), mtl (>=2.1.2 && <3), process (>=1.0.1.1 && <2), stm (>=2.3 && <3)
LicenseLGPL-3
AuthorDan Rosén
MaintainerDan Rosén <danr@chalmers.se>
CategoryConcurrency
Home pagehttp://www.github.com/danr/stm-promise
Bug trackerhttp://www.github.com/danr/stm-promise/issues
Source repositoryhead: git clone git://github.com/danr/stm-promise.git
Upload dateWed Mar 6 09:39:47 UTC 2013
Uploaded byDanRosen
Downloads202 total (21 in last 30 days)

Modules

Flags

NameDescriptionDefault
werrorDisabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees