stm-promise

Simple STM Promises for IO computations and external processes http://www.github.com/danr/stm-promise

Latest on Hackage:0.0.3.1

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

LGPL-3 licensed by Dan Rosén
Maintained by Dan Rosén

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.

Depends on:
Used by 1 package:
comments powered byDisqus