On Nov 7, 2007 5:12 AM, Denis Bueno
Ironically, this was my first problem. First of all, I don't think I want the semi-closed state -- I want to be able to read and write freely later on (I may be misunderstanding semi-closed, however).
I don't think that makes sense. First of all, pout is only the stdout of the program, so you can only read from it, not write to it. 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".
Second, when I used this approach, after the hGetContents call I did the regexp matching, and the program hung during matching.
That's not surprising. You first match for "Proof succeeded". So if the proof failed, the matcher will go past the "attempt has failed" message, looking for a later succeeded. Which means it will block waiting for more output from your subprocess, which will never produce more output until you give it another request. 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.