source: sizechecking/README.txt @ 13

Prerequisites
-------------

You need at least version 2011.4.0.0 of the Haskell platform, an installed
[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/)
and the packages `sbv` and `value-supply`. If you have a working Haskell platform installed you can
install value-supply by typing

        cabal install value-supply sbv


Source files
------------

Examples.hs
  ~ Some examples
SizedExp.hs
  ~ Embedded language to prove size expressions
Lambda.hs
  ~ Size expressions
Constraints.hs
  ~ Constraint solver

Using the examples
------------------

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
$ ghci Examples.hs
GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
[1 of 4] Compiling Lambda           ( Lambda.hs, interpreted )
[2 of 4] Compiling Constraints      ( Constraints.hs, interpreted )
[3 of 4] Compiling SizedExp         ( SizedExp.hs, interpreted )
[4 of 4] Compiling Main             ( Examples.hs, interpreted )
Ok, modules loaded: Lambda, SizedExp, Constraints, Main.
*Main>
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Type "`runTests`" to run all test cases or type "`prove map`" to prove the
function named map.

Under Windows
-------------
It is not perfect, and you will see a box after every special character, but at
least it works.

 - Open a console by running the program `cmd`
 - Issue the command `chcp 65001`
 - In the console cd to the trunk directory
 - Now, you can run `ghci Examples.hs`


Introduction to Haskell syntax
------------------------------

Haskell syntax is very much like Clean, however there are some expressions you
cannot find in Clean.

### Backtick ###

Every haskell function can be used as infix operator. For example the
following two expressions are the same.

~~~~~~~~~~~
func a b
a `func` b
~~~~~~~~~~~

### Dollar ###

Dollar sign is just explicit application (but with different precedence), so it
can be used as a backward pipe operator. The following expressions are the
same.

~~~~~~~~~~~~~~
func (a b)
func $ a b
~~~~~~~~~~~~~~


The Embedded Language
---------------------

As an example the function `map` is examined.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1 smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
2 map :: (SizedExp se)  => Size se ( (a->b) -> [a] -> [b] )
3 map = bind smap body
4     where body f l = match l (nil)
5             ( \x xs ->  cons `app` (f `app` x) `app` (map `app` f `app` xs ))
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Here line 3 tells us map is a top-level binding, where the body of the function is
defined in line 4--5 and its size expression is in line 1. Unfortunately the
size expression language has not yet been embedded, so it is a bit difficult to
read. Type `smap` in the GHC console to get a pretty printed form.

~~~~~~~~~~~~~~~~~
*Main> smap
λf.Λs,g.List s (λi.f (g i))
~~~~~~~~~~~~~~~~~

The type of the function tells us the underlying type, ie. `(a->b) -> [a] -> [b]`.

The body of map corresponds to the following expression

~~~~~~~~~~~~~~~~~~~~~~~
match l of
   nil       -> nil
   cons x xs -> cons (f x) (map f xs)
~~~~~~~~~~~~~~~~~~~~~~~


In the embedded language `bind`, `match` and `app` are supercombinators.

`bind sexp exp`

  : combines a size and an expression and creates a top-level binding

`match list nilexp consexp`

  : embedding of the match operator of our language to haskell

`app exp1 exp2`

  : embedding of the function application of our language to haskell

There is also a function called `true` to denote that we do not want to prove that
branch.