Hi everyone on haskell-cafe, I am wondering about how to give a correctness prove of a simple parsing algorithm. I tried to think of a simple example but even in this case I don't know how. I have an abstract syntax:
data Parens = Empty | Wrap Parens | Append Parens Parens
assumption (A), in Append x y, x and y are never Empty assumption (B), Strings only contain '(' and ')' characters and a printing function
print :: Parens -> String print Empty = "" print (Wrap m) = "(" ++ print m ++ ")" print (Append x y) = print x ++ print y
So the idea is that I would like to write parse :: String -> Maybe Parens, such that if it gives Nothing then the String was malformed, if it gives Just x then the string should be equal to print x. I think I can write such a function in a few different ways, but I don't know how to prove this code works, could anybody show me how? Thank you for any replies. -- View this message in context: http://www.nabble.com/Parsing-with-Proof-tp22814576p22814576.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.