A simple Haskell-subset to Dafny translator

	Duncan C. White, April 2014

INTRO:

Derived from parts of two C-Tools lectures,
in which I built a series of libraries and tools
ending up building a Haskell-subset to C translator,
written in C, using Yacc, Lex, and my own tool
datadec.

Datadec gives C the ability to use Inductive
(or Recursive) Data Types a la functional programming
languages - and Dafny too of course.  One extra cute
feature in Datadec is that you can easily define how
these data types are printed by "print hints" after
the constructors.  The translator used these print hints
to make printing the AST emit valid C code!

This "translate to Dafny (not C)" version was hacked quickly
on Friday 28th March 2014 by modifying print statements in
codegen.c and all the print hints in types.in (which contains
the definition of the main AST inductive data types).

BUILDING THE CODE

To build "haskell2dafny", in this directory, with an environment
variable ARCH set to your processor architecture, simply:

	make install

- this creates ./bin/(architecture)/datadec and
  ./bin/(architecture)/haskell2dafny

- add ./bin/(architecture) to your path eg

    set path = ( $cwd/bin/$ARCH $path )
    rehash

  for c-shell users, and

    export PATH=`pwd`/bin/$ARCH:$PATH

  for benighted heathens (bash users)

- Test it out via
  haskell2dafny 3 < 06.haskell-egs/input6
  haskell2dafny 4 < 06.haskell-egs/input6
  haskell2dafny 5 < 06.haskell-egs/input6


UNDERSTANDING THE CODE:

Sequence through the following directories,
reading each directory's README.

- 01.libmem
	- malloc() and free() sanity checker from Dr Dobbs
	 Journal way back in the 1980s.  this could be
	 removed relatively easily from the rest if desired.

- 02.hash-final
	- the optimized version of the hash table.
	- installs into lib via 'make install'
	  for you to use in your own projects, like libmem.

- 03.datadec
	- my Haskell-style recursive data type generator
	  for C.  generate C ADT modules automatically.
	- installs into bin via 'make install'
	  for you to use.

- 04.datadec-eg
	- an example of how to use datadec once you've
	  installed it

- 05.haskell2dafny
	- tiny 'Int->Int functions' subset of Haskell:
	  parse, perform semantic checks + then generate valid Dafny code!

- 06.haskell-egs
	- a collection of tiny Haskell examples for you to try.
	  Some use "arg1" in the main call, define this value by
	  giving haskell2dafny a command line argument (as in the
	  "test it out" examples above showed).

- h2d.cgi
	- a quick Perl CGI script which wraps haskell2dafny up
	  behind a web form.  Simply decide where to permanently
	  install haskell2dafny and edit the $h2d variable in h2d.cgi
	  (value shown as: /homes/dcw/bin/haskell2dafny)
	- then copy h2d.cgi into some web server's document tree,
	  where the web server is configured to run ".cgi" scripts
	  as, well, CGI scripts.
