3802a3d3d7af51ddff31943d5514382f01265770Lennart Poettering{- |

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekModule : $Header$

12b42c76672a66c2d4ea7212c14f8f1b5a62b78dTom GundersenDescription : Interface to the TPTP theorem prover via Darwin.

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekCopyright : (c) Heng Jiang, Uni Bremen 2004-2007

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-SzmekMaintainer : jiang@informatik.uni-bremen.de

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekStability : provisional

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-SzmekPortability : needs POSIX

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-SzmekInterface for the Darwin service, uses GUI.GenericATP.

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-SzmekSee <http://spass.mpi-sb.mpg.de/> for details on SPASS, and

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek<http://combination.cs.uiowa.edu/Darwin/> for Darwin.

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek-}

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmekmodule SoftFOL.ProveDarwin

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek ( darwinProver

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek , darwinCMDLautomaticBatch

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek , darwinConsChecker

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , ProverBinary (..)

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek ) where

b975b0d514321f169b3c4599a8ea92e13741b4e4Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek-- preliminary hacks for display of CASL models

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Logic.Prover

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport SoftFOL.Sign

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport SoftFOL.Translate

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport SoftFOL.ProverState

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Common.AS_Annotation as AS_Anno

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport qualified Common.Result as Result

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Common.ProofTree

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Common.ProverTools

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Common.SZSOntology

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Data.Char (isDigit)

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Data.List

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Data.Maybe

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Data.Time (timeToTimeOfDay)

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Data.Time.Clock (UTCTime (..), secondsToDiffTime, getCurrentTime)

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Control.Monad (when)

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport qualified Control.Concurrent as Concurrent

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport System.Exit

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport System.IO

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport System.Process

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport GUI.GenericATP

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Interfaces.GenericATPState

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekimport Proofs.BatchProcessing

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek-- * Prover implementation

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmekdata ProverBinary = Darwin | EDarwin

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekproverBinary :: ProverBinary -> String

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart PoetteringproverBinary b = case b of

299a55075d1bf478b9190191caefd5c1b934340dMark Eichin Darwin -> "darwin"

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek EDarwin -> "e-darwin"

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart Poettering

299a55075d1bf478b9190191caefd5c1b934340dMark Eichin{- | The Prover implementation. First runs the batch prover (with

299a55075d1bf478b9190191caefd5c1b934340dMark Eichin graphical feedback), then starts the GUI prover. -}

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart PoetteringdarwinProver

299a55075d1bf478b9190191caefd5c1b934340dMark Eichin :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart PoetteringdarwinProver b = mkAutomaticProver (proverBinary b) () (darwinGUI b)

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart Poettering $ darwinCMDLautomaticBatchAux b

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart Poettering

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart PoetteringdarwinConsChecker

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering :: ProverBinary -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart PoetteringdarwinConsChecker b = (mkConsChecker (proverBinary b) () $ consCheck b)

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering { ccNeedsTimer = False }

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek{- |

fbce11397f4d19821a9dfe66ee3ebe11cad90057Jan Engelhardt Record for prover specific functions. This is used by both GUI and command

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering line interface.

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering-}

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart PoetteringatpFun :: ProverBinary -- ^ the actual binary

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering -> String -- ^ theory name

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart PoetteringatpFun b thName = ATPFunctions

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering { initialProverState = spassProverState

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering , atpTransSenName = transSenName

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering , atpInsertSentence = insertSentenceGen

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering , goalOutput = showTPTPProblem thName

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , proverHelpText = "no help for darwin available"

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT"

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , fileExtensions = FileExtensions

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek { problemOutput = ".tptp"

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , proverOutput = ".spass"

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , theoryConfiguration = ".spcf" }

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart Poettering , runProver = runDarwin b

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek , createProverOptions = extraOpts }

c4e87748d5d3f574d335a87e3a6272276814b2fdPatrick Donnelly

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek-- ** GUI

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek{- |

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek Invokes the generic prover GUI. SPASS specific functions are omitted by

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek data type ATPFunctions.

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek-}

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekdarwinGUI

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek :: ProverBinary -- ^ the actual binary

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek -> String -- ^ theory name

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek -> Theory Sign Sentence ProofTree

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek -- ^ theory consisting of a signature and sentences

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek -> IO [ProofStatus ProofTree] -- ^ proof status for each goal

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekdarwinGUI b thName th freedefs =

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek genericATPgui (atpFun b thName) True (proverBinary b) thName th

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek freedefs emptyProofTree

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek-- ** command line function

3fde5f30bda2a70d97f3dc8fa918e42e1c07cc2cLennart Poettering

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek{- |

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering automatic command line interface to the Darwin prover.

847ae0ae7f29e7bfb245d692409fc2948eab7d1dLennart Poettering Darwin specific functions are omitted by data type ATPFunctions.

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek-}

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-SzmekdarwinCMDLautomaticBatch

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek :: Bool -- ^ True means include proved theorems

d868475ad62547f0a034dfaf038aff31b3d05372Zbigniew Jędrzejewski-Szmek -> Bool -- ^ True means save problem file

-> Concurrent.MVar (Result.Result [ProofStatus ProofTree])

-- ^ used to store the result of the batch run

-> String -- ^ theory name

-> TacticScript -- ^ default tactic script

-> Theory Sign Sentence ProofTree

-- ^ theory consisting of a signature and sentences

-> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

-> IO (Concurrent.ThreadId, Concurrent.MVar ())

-- ^ fst: identifier of the batch thread for killing it

-- snd: MVar to wait for the end of the thread

darwinCMDLautomaticBatch = darwinCMDLautomaticBatchAux Darwin

darwinCMDLautomaticBatchAux

:: ProverBinary -- ^ the actual binary

-> Bool -- ^ True means include proved theorems

-> Bool -- ^ True means save problem file

-> Concurrent.MVar (Result.Result [ProofStatus ProofTree])

-- ^ used to store the result of the batch run

-> String -- ^ theory name

-> TacticScript -- ^ default tactic script

-> Theory Sign Sentence ProofTree

-- ^ theory consisting of a signature and sentences

-> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

-> IO (Concurrent.ThreadId, Concurrent.MVar ())

-- ^ fst: identifier of the batch thread for killing it

-- snd: MVar to wait for the end of the thread

darwinCMDLautomaticBatchAux b inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun b thName) inclProvedThs saveProblem_batch

resultMVar (proverBinary b) thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

-- * Main prover functions

{- |

Runs the Darwin service. The tactic script only contains a string for the

time limit.

-}

consCheck

:: ProverBinary

-> String

-> TacticScript

-> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree

-> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

-> IO (CCStatus ProofTree)

consCheck b thName (TacticScript tl) tm freedefs = case tTarget tm of

Theory sig nSens -> let

saveTPTP = False

proverStateI = spassProverState sig (toNamedList nSens) freedefs

problem = showTPTPProblemM thName proverStateI []

extraOptions =

"-pc false -pmtptp true -fd true -to " ++ tl

saveFileName = reverse $ fst $ span (/= '/') $ reverse thName

runDarwinRealM :: IO (CCStatus ProofTree)

runDarwinRealM = do

let bin = proverBinary b

probl <- problem

noProg <- missingExecutableInPath bin

if noProg then

return CCStatus

{ ccResult = Nothing

, ccProofTree = ProofTree "Darwin not found"

, ccUsedTime = timeToTimeOfDay $ secondsToDiffTime 0 }

else do

when saveTPTP $ writeFile (saveFileName ++ ".tptp") probl

t <- getCurrentTime

let timeTmpFile = "/tmp/" ++ saveFileName ++ show (utctDay t)

++ "-" ++ show (utctDayTime t) ++ ".tptp"

writeFile timeTmpFile probl

let command = bin ++ " " ++ extraOptions ++ " " ++ timeTmpFile

(_, outh, errh, proch) <- runInteractiveCommand command

(szsState, output, tUsed) <- parseDarwinOut outh errh proch

let outState = proofStatM szsState output tUsed

return outState

proofStatM :: String -> [String] -> Int -> CCStatus ProofTree

proofStatM exitCode out tUsed = let

outState = CCStatus

{ ccResult = Just True

, ccProofTree = ProofTree $ unlines $ exitCode : out

, ccUsedTime = timeToTimeOfDay $ secondsToDiffTime

$ toInteger tUsed }

in if szsProved exitCode then outState else

outState

{ ccResult = if szsDisproved exitCode then Just False

else Nothing }

in runDarwinRealM

runDarwin

:: ProverBinary

-> SoftFOLProverState

-- ^ logical part containing the input Sign and axioms and possibly

-- goals that have been proved earlier as additional axioms

-> GenericConfig ProofTree -- ^ configuration to use

-> Bool -- ^ True means save TPTP file

-> String -- ^ name of the theory in the DevGraph

-> AS_Anno.Named SPTerm -- ^ goal to prove

-> IO (ATPRetval, GenericConfig ProofTree)

-- ^ (retval, configuration with proof status and complete output)

runDarwin b sps cfg saveTPTP thName nGoal = runDarwinReal where

bin = proverBinary b

simpleOptions = extraOpts cfg

extraOptions = maybe "-pc false"

(("-pc false -to " ++) . show) (timeLimit cfg)

saveFileName = thName ++ '_' : AS_Anno.senAttr nGoal

tmpFileName = reverse (fst $ span (/= '/') $ reverse thName) ++

'_' : AS_Anno.senAttr nGoal

runDarwinReal = do

noProg <- missingExecutableInPath bin

if noProg then

return

(ATPError ("Could not start " ++ bin ++ ". Check your $PATH"),

emptyConfig bin

(AS_Anno.senAttr nGoal) emptyProofTree)

else do

prob <- showTPTPProblem thName sps nGoal $

simpleOptions ++ ["Requested prover: " ++ bin]

when saveTPTP

(writeFile (saveFileName ++ ".tptp") prob)

t <- getCurrentTime

let timeTmpFile = "/tmp/" ++ tmpFileName ++ show (utctDay t) ++

"-" ++ show (utctDayTime t) ++ ".tptp"

writeFile timeTmpFile prob

let command = bin ++ " " ++ extraOptions ++ " " ++ timeTmpFile

(_, outh, errh, proch) <- runInteractiveCommand command

(exCode, output, tUsed) <- parseDarwinOut outh errh proch

let (err, retval) = proofStat exCode simpleOptions output tUsed

return (err,

cfg {proofStatus = retval,

resultOutput = output,

timeUsed = timeToTimeOfDay $

secondsToDiffTime $ toInteger tUsed})

proofStat exitCode options out tUsed = case () of

_ | szsProved exitCode -> (ATPSuccess, provedStatus options tUsed)

_ | szsDisproved exitCode -> (ATPSuccess, disProvedStatus options)

_ | szsTimeout exitCode ->

(ATPTLimitExceeded, defaultProofStatus options)

_ | szsStopped exitCode ->

(ATPBatchStopped, defaultProofStatus options)

_ -> (ATPError (unlines (exitCode : out)),

defaultProofStatus options)

defaultProofStatus opts =

(openProofStatus

(AS_Anno.senAttr nGoal) bin emptyProofTree)

{tacticScript = TacticScript $ show ATPTacticScript

{tsTimeLimit = configTimeLimit cfg,

tsExtraOpts = opts} }

disProvedStatus opts = (defaultProofStatus opts)

{goalStatus = Disproved}

provedStatus opts ut = ProofStatus

{ goalName = AS_Anno.senAttr nGoal

, goalStatus = Proved True

, usedAxioms = getAxioms

, usedProver = bin

, proofTree = emptyProofTree

, usedTime = timeToTimeOfDay $ secondsToDiffTime $ toInteger ut

, tacticScript = TacticScript $ show ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg, tsExtraOpts = opts }}

getAxioms = let

fl = formulaLists $ initialLogicalPart sps

fs = concatMap formulae $ filter isAxiomFormula fl

in map AS_Anno.senAttr fs

isAxiomFormula :: SPFormulaList -> Bool

isAxiomFormula fl =

case originType fl of

SPOriginAxioms -> True

_ -> False

getSZSStatusWord :: String -> Maybe String

getSZSStatusWord line = case words

$ fromMaybe (fromMaybe "" $ stripPrefix "% SZS status" line)

$ stripPrefix "SZS status" line of

[] -> Nothing

w : _ -> Just w

parseDarwinOut :: Handle -- ^ handel of stdout

-> Handle -- ^ handel of stderr

-> ProcessHandle -- ^ handel of process

-> IO (String, [String], Int)

-- ^ (exit code, complete output, used time)

parseDarwinOut outh _ procHndl =

-- darwin does not write to stderr here, so ignore output

-- err <- hGetLine errh

-- if null err then

readLineAndParse ("", [], -1) False

where

readLineAndParse (exCode, output, to) stateFound = do

procState <- isProcessRun

case procState of

ExitSuccess -> do

iseof <- hIsEOF outh

if iseof then

do -- ec <- isProcessRun proc

waitForProcess procHndl

return (exCode, reverse output, to)

else do

line <- hGetLine outh

if isPrefixOf "Couldn't find eprover" line

|| isInfixOf "darwin -h for further information" line

-- error by running darwin.

then do

waitForProcess procHndl

return ("Internal error.", line : output, to)

else case getSZSStatusWord line of

Just szsState | not stateFound ->

readLineAndParse (szsState, line : output, to)

True

_ -> if "CPU Time" `isPrefixOf` line -- get cup time

then let time = case takeWhile isDigit $ last (words line) of

ds@(_ : _) -> read ds

_ -> to

in readLineAndParse (exCode, line : output, time)

stateFound

else readLineAndParse (exCode, line : output, to)

stateFound

ExitFailure failure -> do

waitForProcess procHndl

return ("Process error " ++ show failure, output, to)

-- check if darwin running

isProcessRun = do

exitcode <- getProcessExitCode procHndl

case exitcode of

Nothing -> return ExitSuccess

Just (ExitFailure i) -> return (ExitFailure i)

Just ExitSuccess -> return ExitSuccess