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.