Assignment 3

This assignment introduces MiniDafny and focuses on pretty printing and parsing.

You should download PrintParse.zip. This contains the template for the exercise - the standard stack/cabal boilerplate, as well as a few Haskell files.

• The Syntax.hs file describes the Syntax of MiniDafny.
• The ParserLib.hs file is the Parser Combinator library, just like the one we used in class.
• Printer.hs contains the first bit of your homework: pretty printing.
• Parser.hs contains the second bit of your homework: parsing.
• Main.hs offers a convenient way of parsing a dafny file into a syntax tree and then pretty printing it. Feel free to change it to run your own tests or even QuickCheck.

The zip file also contains two directories with dafny programs: dafny and more-programs. All programs should parse and print correctly—but you can (and should) test your code more thoroughly as there will be more tests on Gradescope.

Your job is to fill in Printer.hs and Parser.hs following their instructions, and submit just those files through Gradescope.

The deadline for this is Tuesday, March 25th, 11:59PM. That said, practice with applicatives in the parser module will be helpful for the midterm, so start early!