[Haskell-cafe] Parsing with Proof

[muad]

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.