Prerequisites

You need at least version 2011.4.0.0 of the Haskell platform, an installed Z3 and the package value-supply. If you have a working Haskell platform installed you can install value-supply by typing

cabal install value-supply

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 we do not want to prove that branch.