On Nov 7, 2007 4:44 PM, David Benbennick
And once you do hGetContents, you have read all the data that will ever exist on that handle, so there's nothing to read from it "later on".
I completely misunderstood how hGetContents works. This now makes sense. I first thought hGetContents would return "everything you could read from the stream right now" as a string. From reading the the haddock documentation for System.IO.hGetContents, I failed to understand that the string it returns will contain characters that haven't even been written to the (interactive) stream by the time of the call to hGetContents. I'm not sure if the hGetContents documentation could easily be made to make that fact more salient, but I'd be willing to submit a patch, if other people have been confused.
Assuming that each call to ACL2 produces exactly one of either "Proof succeeded" or "attempt has failed", you can get a list of results like this (where aclOutput :: String is the result of hGetContents):
let results = map (\l -> if l == "Proof succeeded" then True else False) $ filter (\l -> elem l ["Proof succeeded", "attempt has failed"]) $ lines aclOutput
Then results :: [Bool], and results !! n is True if the nth call succeeded. Just make sure not to inspect results !! n until after making the nth call to ACL2, or it will block.
I used a minor modification of this approach ("Proof succeeded" is not on a line by itself), and it worked famously. Thanks for the help, David! -- Denis