[Haskell-cafe] Screen scraping with an interactive process: Buffering problems?

[Denis Bueno]

Hi all,

I'm writing some code to interact with an ACL2 [0] process.  I'd like
to be able to write a function

    test :: String -> IO Bool

that will attempt to prove something by forking an ACL2 process and
screen scraping its output, to see whether the conjecture was proved.

The code below [1] is close: it launches the process, sends the
conjecture to ACL2, and reads ACL2's output line-by-line until it
finds "Proof succeeded" or "attempt has failed".  This works well
enough for the simple case, but there is a problem.

In readACL2Answer, the code shouldn't have to check for success *and*
failure, since the conditions are complementary.  But if I change that
code to check only for success, then it is possible (and indeed it
happens every time) that if I send ACL2 a conjecture it can't prove,
readACL2Answer blocks indefinitely -- and the print statements show
that hWaitForInput has said there is more data on the Handle but
hGetLine blocks trying to read it.

The reason for this, as far as I can tell, is that there *is* more
data -- a character, for example -- but no newline, so hGetLine blocks
waiting for a newline.  However, if I'm reading the BufferMode
documentation [3] correctly, the fact that I've set my streams to
LineBuffering should mitigate that scenario.

Concretely, I know that ACL2 runs in a REPL and the last thing it
prints is in fact an incomplete line -- "ACL2 !>".  I'd rather not
have to read every line character by character just to detect the
uncommon case.

Should I just do it character by character?  Am I reading the
BufferMode docs wrong, and if so, what is the correct interpretation?
Is there better approach for the original problem I'm trying to solve?

Thanks for reading this far. =]

-- 
                              Denis

[0] http://www.cs.utexas.edu/users/moore/acl2/

[1]
import System.Process
import System.IO

type Proc = (Handle, Handle, Handle, ProcessHandle)

testThm = test "(equal x x)"    -- something acl2 can prove
testBad = test "(equal x (not x))" -- something it can't

-- | Pass a conjecture form to ACL2, attempt to prove it, and return a boolean
-- indicating whether ACL2 was able to prove it.
test :: String -> IO Bool
test thm =
    do i@(stdin, _, _, pid) <- setUpACL2
       success <- testProc i thm
       hPutStrLn stdin "(good-bye)"
       putStrLn "saying goodbye"
       exitCode <- waitForProcess pid
       case exitCode of
         ExitSuccess   -> return success
         ExitFailure i -> error ("ACL2 bad exit code: " ++ show i)

-- | Pass a conjecture vio the given process' input stream, and return whether
-- it is proved.
testProc :: Proc -> String -> IO Bool
testProc i@(stdin, stdout, _, pid) thm =
    do hSetBuffering stdout LineBuffering
       hSetBuffering stdin LineBuffering
       success <- testInACL2 ("(thm " ++ thm ++ ")") i
       putStrLn "found success value"
       return success


succeedRx = mkRegex "Proof succeeded[.]"
failedRx  = mkRegex "attempt has failed[.]"

-- create acl2 process and return handles
setUpACL2 :: IO Proc
setUpACL2 = runInteractiveCommand "acl2"



testInACL2 :: String -> Proc -> IO Bool
testInACL2 str (pin, pout, perr, pid) =
    do putStrLn "printing to acl2..."
       hPutStrLn pin str
       putStrLn "getting acl2 result..."
       readACL2Answer pout

-- | How long we should wait for ACL2 to start saying something.  Five
-- seconds, currently.
readTimeout = 100

readACL2Answer :: Handle -> IO Bool
-- I *should* be required *only* to check for *success* in the matchRegex
-- statement below, instead of checking for success and failure.  But if I do
-- that, and the theorem to be proved fails, this function blocks indefinitely
-- (at least I observe a much greater than 5 second wait period), even though
-- it should only block for `readTimeout' milliseconds.  I'm not sure why this
-- is, but at least there is an acceptable workaround.
readACL2Answer pout = hWaitForInput pout readTimeout >>= (\isReady ->
    if isReady
    then do putStrLn "getting line"
            line <- hGetLine pout
            putStrLn $ "read line: " ++ line
            -- Check for success or failure.
            case (matchRegex succeedRx line, matchRegex failedRx line) of
              (Nothing, Nothing) -> readACL2Answer pout
              (Nothing, Just _)  -> return False
              (Just _, _)        -> return True
    else do putStrLn "not ready"
            return False)


[3] http://haskell.org/ghc/docs/latest/html/libraries/base-3.0.0.0/System-IO.html#12