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)

    m_res <- evalTree (any (not . snd)) promise_tree

    let res = fromMaybe [] m_res

    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]

Flags

Manual Flags

Name	Description	Default
werror		Disabled

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

Downloads

• stm-promise-0.0.1.tar.gz [browse] (Cabal source package)
• Package description (as included in the package)

Maintainer's Corner

Package maintainers

• DanRosen

For package maintainers and hackage trustees

• edit package information

Candidates

• No Candidates