diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Matthew Naylor 2006-2007.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Neil Mitchell nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/benchmarks/Benchmark.hs b/benchmarks/Benchmark.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Benchmark.hs
@@ -0,0 +1,35 @@
+import System
+import Data.List
+
+main :: IO ()
+main = do args <- getArgs
+          case args of
+            [checker, file] -> benchmark checker file
+            _ -> error usage
+
+usage = "Usage: runhugs Benchmark.hs "
+        ++ "[SmallCheck|LazySmallCheck|LazySmallCheck.Generic] FILE"
+
+benchmark checker file =
+  do extra <-
+      case checker of
+       "SmallCheck" -> return ""
+       "LazySmallCheck" -> return ""
+       "LazySmallCheck.Generic" -> return "import Data.Generics\n"
+       _ -> error usage
+     if '.' `elem` file then error "Filename should not contain '.'"
+                        else return ()
+     contents <- readFile (file ++ ".hs")
+     let props = nub $ filter ("prop_" `isPrefixOf`) (words contents)
+     writeFile (file ++ "2.hs") $  extra
+                                ++ "import System\n"
+                                ++ "import " ++ checker ++ "\n\n"
+                                ++ contents ++ "\n\n"
+                                ++ "main = do { [p, d] <- getArgs"
+                                ++ "          ; case p of { "
+                                ++ concatMap propAlt props
+                                ++ "_ -> error \"Unknown property\"}}"
+     system $ "ghc -fglasgow-exts -O2 --make " ++ file ++ "2.hs -o " ++ file
+     return ()
+
+propAlt p = "\"" ++ p ++ "\" -> " ++ "depthCheck (read d) " ++ p ++ ";"
diff --git a/benchmarks/Countdown.hs b/benchmarks/Countdown.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Countdown.hs
@@ -0,0 +1,187 @@
+-----------------------------------------------------------------------------
+--
+--                           The Countdown Problem
+--
+--                               Graham Hutton
+--                         University of Nottingham
+--
+--                               November 2001
+--
+-----------------------------------------------------------------------------
+
+-----------------------------------------------------------------------------
+-- Formally specifying the problem
+-----------------------------------------------------------------------------
+
+data Op               = Add | Sub | Mul | Div
+  deriving Eq
+
+valid                :: Op -> Int -> Int -> Bool
+valid Add _ _         = True
+valid Sub x y         = x > y
+valid Mul _ _         = True
+valid Div x y         = x `mod` y == 0
+ 
+apply                :: Op -> Int -> Int -> Int
+apply Add x y         = x + y
+apply Sub x y         = x - y
+apply Mul x y         = x * y
+apply Div x y         = x `div` y
+
+data Expr             = Val Int | App Op Expr Expr
+  deriving Eq
+
+values               :: Expr -> [Int]
+values (Val n)        = [n]
+values (App _ l r)    = values l ++ values r
+
+eval                 :: Expr -> [Int]
+eval (Val n)          = [n | n > 0]
+eval (App o l r)      = [apply o x y | x <- eval l, y <- eval r, valid o x y]
+
+subbags              :: [a] -> [[a]]
+subbags xs            = [zs | ys <- subs xs, zs <- perms ys]
+
+subs                 :: [a] -> [[a]]
+subs []               = [[]]
+subs (x:xs)           = ys ++ map (x:) ys
+                        where
+                           ys = subs xs
+
+perms                :: [a] -> [[a]]
+perms []              = [[]]
+perms (x:xs)          = concat (map (interleave x) (perms xs))
+
+interleave           :: a -> [a] -> [[a]]
+interleave x []       = [[x]]
+interleave x (y:ys)   = (x:y:ys) : map (y:) (interleave x ys)
+
+solution             :: Expr -> [Int] -> Int -> Bool
+solution e ns n       = elem (values e) (subbags ns) && eval e == [n]
+
+-----------------------------------------------------------------------------
+-- Brute force implementation
+-----------------------------------------------------------------------------
+
+split                :: [a] -> [([a],[a])]
+split []              = [([],[])]
+split (x:xs)          = ([],x:xs) : [(x:ls,rs) | (ls,rs) <- split xs]
+
+nesplit              :: [a] -> [([a],[a])]
+nesplit               = filter ne . split
+
+ne                   :: ([a],[b]) -> Bool
+ne (xs,ys)            = not (null xs || null ys)
+
+exprs                :: [Int] -> [Expr]
+exprs []              = []
+exprs [n]             = [Val n]
+exprs ns              = [e | (ls,rs) <- nesplit ns
+                           , l       <- exprs ls
+                           , r       <- exprs rs
+                           , e       <- combine l r]
+
+combine              :: Expr -> Expr -> [Expr]
+combine l r           = [App o l r | o <- ops]
+ 
+ops                  :: [Op]
+ops                   = [Add,Sub,Mul,Div]
+
+solutions            :: [Int] -> Int -> [Expr]
+solutions ns n        = [e | ns' <- subbags ns, e <- exprs ns', eval e == [n]]
+
+-----------------------------------------------------------------------------
+-- Fusing generation and evaluation
+-----------------------------------------------------------------------------
+
+type Result           = (Expr,Int)
+
+results              :: [Int] -> [Result]
+results []            = []
+results [n]           = [(Val n,n) | n > 0]
+results ns            = [res | (ls,rs) <- nesplit ns
+                             , lx      <- results ls
+                             , ry      <- results rs
+                             , res     <- combine' lx ry]
+
+combine'             :: Result -> Result -> [Result]
+combine' (l,x) (r,y)  = [(App o l r, apply o x y) | o <- ops, valid o x y]
+
+solutions'           :: [Int] -> Int -> [Expr]
+solutions' ns n       = [e | ns' <- subbags ns, (e,m) <- results ns', m == n]
+
+-----------------------------------------------------------------------------
+-- Exploiting arithmetic properties
+-----------------------------------------------------------------------------
+
+valid'               :: Op -> Int -> Int -> Bool
+valid' Add x y        = x <= y
+valid' Sub x y        = x > y
+valid' Mul x y        = x /= 1 && y /= 1 && x <= y
+valid' Div x y        = y /= 1 && x `mod` y == 0
+
+eval'                :: Expr -> [Int]
+eval' (Val n)         = [n | n > 0]
+eval' (App o l r)     = [apply o x y | x <- eval' l, y <- eval' r, valid' o x y]
+
+solution'            :: Expr -> [Int] -> Int -> Bool
+solution' e ns n      = elem (values e) (subbags ns) && eval' e == [n]
+
+results'             :: [Int] -> [Result]
+results' []           = []
+results' [n]          = [(Val n,n) | n > 0]
+results' ns           = [res | (ls,rs) <- nesplit ns
+                             , lx      <- results' ls
+                             , ry      <- results' rs
+                             , res     <- combine'' lx ry]
+
+combine''            :: Result -> Result -> [Result]
+combine'' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid' o x y]
+
+solutions''          :: [Int] -> Int -> [Expr]
+solutions'' ns n      = [e | ns' <- subbags ns, (e,m) <- results' ns', m == n]
+
+-----------------------------------------------------------------------------
+-- Interactive version for testing
+-----------------------------------------------------------------------------
+
+instance Show Op where
+   show Add           = "+"
+   show Sub           = "-"
+   show Mul           = "*"
+   show Div           = "/"
+
+instance Show Expr where
+   show (Val n)       = show n
+   show (App o l r)   = bracket l ++ show o ++ bracket r
+                        where
+                           bracket (Val n) = show n
+                           bracket e       = "(" ++ show e ++ ")"
+
+display              :: [Expr] -> IO ()
+display []            = putStr "\nThere are no solutions.\n\n"
+display (e:es)        = do putStr "\nOne possible solution is "
+                           putStr (show e)
+	                   putStr ".\n\nPress return to continue searching..."
+                           getLine
+                           putStr "\n"
+                           if null es then
+                               putStr "There are no more solutions.\n\n"
+                            else
+                               do sequence [print e | e <- es]
+                                  putStr "\nThere were "
+                                  putStr (show (length (e:es)))
+                                  putStr " solutions in total.\n\n"
+
+prop_lemma1 :: ([Int], [Int], [Int]) -> Bool
+prop_lemma1 (xs, ys, zs) = ((xs,ys) `elem` split zs) == (xs ++ ys == zs)
+
+prop_lemma3 :: ([Int], [Int], [Int]) -> Bool
+prop_lemma3 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs)
+                             == (xs ++ ys == zs && ne (xs, ys))
+
+prop_lemma4 :: ([Int], [Int], [Int]) -> Bool
+prop_lemma4 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs) ==>
+                             (length xs < length zs && length ys < length zs)
+
+prop_solutions (ns, m) = solutions ns m == solutions' ns m
diff --git a/benchmarks/List.hs b/benchmarks/List.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/List.hs
@@ -0,0 +1,20 @@
+ord [] = True
+ord [x] = True
+ord (x:y:ys) = x <= y && ord (y:ys)
+
+insert x [] = [x]
+insert x (y:ys)
+  | x <= y = x:y:ys
+  | otherwise = y:insert x ys
+
+merge [] ys = ys
+merge xs [] = xs
+merge (x:xs) (y:ys)
+  | x <= y = x : merge xs (y:ys)
+  | otherwise = y : merge (x:xs) ys
+
+prop_ordInsert :: (Char, [Char]) -> Bool
+prop_ordInsert (x, xs) = ord xs ==> ord (insert x xs)
+
+prop_ordMerge :: ([Char], [Char]) -> Bool
+prop_ordMerge (xs, ys) = ord xs && ord ys ==> ord (merge xs ys)
diff --git a/benchmarks/Mux.hs b/benchmarks/Mux.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Mux.hs
@@ -0,0 +1,33 @@
+import Data.List
+
+-- Binary multiplexor
+
+tree              :: (a -> a -> a) -> [a] -> a
+tree f [x]        =  x
+tree f (x:y:ys)   =  tree f (ys ++ [f x y])
+
+unaryMux          :: [Bool] -> [[Bool]] -> [Bool]
+unaryMux sel xs   =  map (tree (||))
+                  $  transpose
+                  $  zipWith (\s x -> map (s &&) x) sel xs
+
+decode []         =  [True]
+decode [x]        =  [not x,x]
+decode (x:xs)     =  concatMap (\y -> [not x && y,x && y]) rest
+  where
+    rest          =  decode xs
+
+binaryMux         :: [Bool] -> [[Bool]] -> [Bool]
+binaryMux sel xs  =  unaryMux (decode sel) xs
+
+num               :: [Bool] -> Int
+num []            =  0
+num (a:as)        =  (if a then 1 else 0) + 2 * num as
+
+-- Property
+
+prop_binMux :: ([Bool], [[Bool]]) -> Bool
+prop_binMux (sel, xs) =
+     ((length xs == 2 ^ length sel)
+  && all ((== length (head xs)) . length) xs)
+  ==> (binaryMux sel xs == xs !! num sel)
diff --git a/benchmarks/RegExp.hs b/benchmarks/RegExp.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/RegExp.hs
@@ -0,0 +1,124 @@
+(<==>) :: Bool -> Bool -> Bool
+a <==> b = (a ==> b) && (b ==> a)
+
+-- ---------------------
+
+data Nat = Zer
+         | Suc Nat
+  deriving Show
+--  deriving (Show,Data, Typeable)
+
+
+instance Serial Nat where
+  series = cons0 Zer \/ cons1 Suc
+
+sub :: Nat -> Nat -> Nat
+sub x y =
+ case y of
+  Zer -> x
+  Suc y' -> case x of
+   Zer -> Zer
+   Suc x' -> sub x' y'
+
+data Sym = N0
+         | N1 Sym
+ deriving (Eq, Show)
+-- deriving (Eq, Show, Data, Typeable)
+
+instance Serial Sym where
+  series = cons0 N0 \/ cons1 N1
+
+-- deriving Eq
+
+data RE = Sym Sym
+        | Or RE RE
+        | Seq RE RE
+        | And RE RE
+        | Star RE
+        | Empty
+  deriving Show
+--  deriving (Data, Typeable, Show)
+
+{-
+instance Serial RE where
+  series =  cons0 Empty
+         \/ cons1 Star
+         \/ cons2 And
+         \/ cons2 Seq
+         \/ cons2 Or
+         \/ cons1 Sym
+-}
+
+instance Serial RE where
+  series = cons1 Sym
+        \/ cons2 Or
+        \/ cons2 Seq
+        \/ cons2 And
+        \/ cons1 Star
+        \/ cons0 Empty
+
+
+
+accepts :: RE -> [Sym] -> Bool
+accepts re ss =
+ case re of
+  Sym n -> case ss of
+   [] -> False
+   (n':ss') -> n == n' && null ss'
+  Or re1 re2 -> accepts re1 ss || accepts re2 ss
+  Seq re1 re2 -> seqSplit re1 re2 [] ss
+  And re1 re2 -> accepts re1 ss && accepts re2 ss
+  Star re' -> case ss of
+   [] -> True
+   (s:ss') -> seqSplit re' re (s:[]) ss'
+    -- accepts Empty ss || accepts (Seq re' re) ss
+  Empty -> null ss
+
+seqSplit :: RE -> RE -> [Sym] -> [Sym] -> Bool
+seqSplit re1 re2 ss2 ss =
+ seqSplit'' re1 re2 ss2 ss || seqSplit' re1 re2 ss2 ss
+
+seqSplit'' :: RE -> RE -> [Sym] -> [Sym] -> Bool
+seqSplit'' re1 re2 ss2 ss = accepts re1 ss2 && accepts re2 ss
+
+seqSplit' :: RE -> RE -> [Sym] -> [Sym] -> Bool
+seqSplit' re1 re2 ss2 ss =
+ case ss of
+  [] -> False
+  (n:ss') ->
+   seqSplit re1 re2 (ss2 ++ [n]) ss'
+
+rep :: Nat -> RE -> RE
+rep n re =
+ case n of
+  Zer -> Empty
+  Suc n' -> Seq re (rep n' re)
+
+repMax :: Nat -> RE -> RE
+repMax n re =
+ case n of
+  Zer -> Empty
+  Suc n' -> Or (rep n re) (repMax n' re)
+
+repInt' :: Nat -> Nat -> RE -> RE
+repInt' n k re =
+ case k of
+  Zer -> rep n re
+  Suc k' -> Or (rep n re) (repInt' (Suc n) k' re)
+
+repInt :: Nat -> Nat -> RE -> RE
+repInt n k re = repInt' n (sub k n) re
+
+-- ---------------------
+
+
+-- main_1
+prop_regex :: (Nat, Nat, RE, RE, [Sym]) -> Bool
+prop_regex (n, k, p, q, s) =  r -- if r then True else True
+  where
+    r = (accepts (repInt n k (And p q)) s)
+          <==> (accepts (And (repInt n k p) (repInt n k q)) s)
+--(accepts (And (repInt n k p) (repInt n k q)) s) <==> (accepts (repInt n k (And p q)) s)
+
+a_sol = (Zer, Suc (Suc Zer), Sym N0, Seq (Sym N0) (Sym N0), [N0, N0])
+
diff --git a/benchmarks/Sad.hs b/benchmarks/Sad.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Sad.hs
@@ -0,0 +1,92 @@
+-- We take the following specification for the sum of absolute
+-- differences, and develop a program that generates circuits that
+-- have the same behaviour
+
+sad                            ::  [Int] -> [Int] -> Int
+sad xs ys                      =   sum (map abs (zipWith (-) xs ys))
+
+type Bit                       =   Bool
+
+low                            ::  Bit
+low                            =   False
+
+high                           ::  Bit
+high                           =   True
+
+inv                            ::  Bit -> Bit
+inv a                          =   not a
+
+and2                           ::  Bit -> Bit -> Bit
+and2 a b                       =   a && b
+or2 a b                        =   a || b
+xor2 a b                       =   a /= b
+xnor2 a b                      =   a == b
+
+mux2                           ::  Bit -> Bit -> Bit -> Bit
+mux2 sel a b                   =   (sel && b) || (not sel && a)
+
+bitAdd                         ::  Bit -> [Bit] -> [Bit]
+bitAdd x []                    =   [x]
+bitAdd x (y:ys)                =   let  (sum,carry) = halfAdd x y
+                                   in   sum:bitAdd carry ys
+
+halfAdd x y                    =   (xor2 x y,and2 x y)
+
+binAdd                         ::  [Bit] -> [Bit] -> [Bit]
+binAdd xs ys                   =   binAdd' low xs ys
+
+binAdd' cin   []       []      =   [cin]
+binAdd' cin   (x:xs)   []      =   bitAdd cin (x:xs)
+binAdd' cin   []       (y:ys)  =   bitAdd cin (y:ys)
+binAdd' cin   (x:xs)   (y:ys)  =   let  (sum,cout) = fullAdd cin x y
+                                   in   sum:binAdd' cout xs ys
+
+fullAdd cin a b                =   let  (s0,c0)  =  halfAdd a b
+                                        (s1,c1)  =  halfAdd cin s0
+                                   in   (s1,xor2 c0 c1)
+
+binGte                         ::  [Bit] -> [Bit] -> Bit
+binGte xs ys                   =   binGte' high xs ys
+
+binGte' gin  []      []        =   gin
+binGte' gin  (x:xs)  []        =   orl (gin:x:xs)
+binGte' gin  []      (y:ys)    =   and2 gin (orl (y:ys))
+binGte' gin  (x:xs)  (y:ys)    =   let  gout = gteCell gin x y
+                                   in   binGte' gout xs ys
+
+gteCell gin x y                =   mux2 (xnor2 x y) x gin
+
+orl                            ::  [Bit] -> Bit
+orl xs                         =   tree or2 low xs
+
+binDiff                        ::  [Bit] -> [Bit] -> [Bit]
+binDiff xs ys                  =   let  xs'   =  pad (length ys) xs
+                                        ys'   =  pad (length xs) ys
+                                        gte   =  binGte xs' ys'
+                                        xs''  =  map (xor2 (inv gte)) xs'
+                                        ys''  =  map (xor2 gte) ys'
+                                   in   init (binAdd' high xs'' ys'')
+  
+pad                            ::  Int -> [Bit] -> [Bit]
+pad n xs | m > n               =   xs
+         | otherwise           =   xs ++ replicate (n-m) False
+  where
+    m                          =   length xs
+
+tree                           ::  (a -> a -> a) -> a -> [a] -> a
+tree f z []                    =   z
+tree f z [x]                   =   x
+tree f z (x:y:ys)              =   tree f z (ys ++ [f x y])
+
+binSum                         ::  [[Bit]] -> [Bit]
+binSum xs                      =   tree binAdd [] xs
+
+binSad                         ::  [[Bit]] -> [[Bit]] -> [Bit]
+binSad xs ys                   =   binSum (zipWith binDiff xs ys)
+
+num                            ::  [Bit] -> Int
+num []                         =   0
+num (a:as)                     =   fromEnum a + 2 * num as
+
+prop_binSad (xs, ys)           =   sad (map num xs) (map num ys)
+                                     == num (binSad xs ys)
diff --git a/benchmarks/SumPuz.hs b/benchmarks/SumPuz.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/SumPuz.hs
@@ -0,0 +1,68 @@
+import Data.List((\\))
+import Char(isAlpha, chr, ord)
+import Maybe(fromJust)
+
+type Soln = [(Char, Int)]
+
+solve :: String -> String
+solve p =
+  display p (solutions xs ys zs 0 [])
+  where
+  [xs,ys,zs] = map reverse (words (filter (`notElem` "+=") p))
+
+display :: String -> [Soln] -> String
+display p []    = "No solution!"
+display p (s:_) =
+  map soln p
+  where
+  soln c = if isAlpha c then chr (ord '0' + img s c) else c
+
+rng :: Soln -> [Int]
+rng = map snd
+
+img :: Soln -> Char -> Int
+img lds l = fromJust (lookup l lds)
+
+bindings :: Char -> [Int] -> Soln -> [Soln]
+bindings l ds lds =
+  case lookup l lds of
+  Nothing  -> map (:lds) (zip (repeat l) (ds \\ rng lds))
+  Just d -> if d `elem` ds then [lds] else []
+
+solutions :: String -> String -> String -> Int -> Soln -> [Soln]
+solutions [] [] []  c lds = if c==0 then [lds] else []
+solutions [] [] [z] c lds = if c==1 then bindings z [1] lds else []
+solutions (x:xs) (y:ys) (z:zs) c lds =
+  solns `ofAll`
+  bindings y [(if null ys then 1 else 0)..9] `ofAll`
+  bindings x [(if null xs then 1 else 0)..9] lds
+  where  
+  solns s = 
+    solutions xs ys zs (xy `div` 10) `ofAll` bindings z [xy `mod` 10] s
+    where    
+    xy = img s x + img s y + c
+
+infixr 5 `ofAll`
+ofAll :: (a -> [b]) -> [a] -> [b]
+ofAll = concatMap
+
+-- Property
+
+find :: String -> String -> String -> [Soln]
+find xs ys zs = solutions (reverse xs) (reverse ys) (reverse zs) 0 []
+
+val :: Soln -> String -> Int
+val s "" = 0
+val s xs = read (concatMap (show . img s) xs)
+
+prop_Sound :: (String, String, String) -> Bool
+prop_Sound (xs, ys, zs) =
+      length xs == length ys
+   && (diff == 0 || diff == 1)
+   && not (null sols)
+  ==> and [ val s xs + val s ys == val s zs
+          | s <- sols
+          ]
+  where
+    sols = find xs ys zs
+    diff = length zs - length xs
diff --git a/benchmarks/clean.sh b/benchmarks/clean.sh
new file mode 100644
--- /dev/null
+++ b/benchmarks/clean.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+rm -f *.hi *.o List Countdown *2.hs RegExp Mux SumPuz Sad
+cd LazySmallCheck
+rm -f *.hi *.o
diff --git a/lazysmallcheck.cabal b/lazysmallcheck.cabal
new file mode 100644
--- /dev/null
+++ b/lazysmallcheck.cabal
@@ -0,0 +1,34 @@
+Name:               lazysmallcheck
+Version:            0.1
+Copyright:          2007, Matthew Naylor
+Maintainer:         mfn@cs.york.ac.uk
+Homepage:           http://www.cs.york.ac.uk/~mfn/lazysmallcheck/
+Build-Depends:      base, haskell98, random
+Build-Type:         Simple
+License:            BSD3
+License-File:       LICENSE
+Author:             Matthew Naylor and Fredrik Lindblad
+Synopsis:           A library for demand-driven testing of Haskell programs
+Description:
+    Lazy SmallCheck is a library for exhaustive, demand-driven testing of
+    Haskell programs.  It is based on the idea that if a property holds
+    for a partially-defined input then it must also hold for all
+    fully-defined instantiations of the that input.  Compared to ``eager''
+    input generation as in SmallCheck, Lazy SmallCheck may require
+    significantly fewer test-cases to verify a property for all inputs up
+    to a given depth.
+Category:           Testing
+Hs-Source-dirs:
+    source
+Extra-Source-Files:
+    benchmarks/Benchmark.hs
+    benchmarks/Countdown.hs
+    benchmarks/List.hs
+    benchmarks/Mux.hs
+    benchmarks/RegExp.hs
+    benchmarks/Sad.hs
+    benchmarks/SumPuz.hs
+    benchmarks/clean.sh
+Exposed-modules:
+    LazySmallCheck
+    LazySmallCheck.Generic
diff --git a/source/LazySmallCheck.hs b/source/LazySmallCheck.hs
new file mode 100644
--- /dev/null
+++ b/source/LazySmallCheck.hs
@@ -0,0 +1,262 @@
+module LazySmallCheck
+  ( Serial(series) -- class Serial
+  , (\/)           -- :: Series a -> Series a -> Series a
+  , cons0          -- :: a -> Series a
+  , cons1          -- :: Serial a => (a -> b) -> Series b
+  , cons2          -- :: (Serial a, Serial b) =>
+                   --    (a -> b -> c) -> Series c
+  , cons3          -- :: (Serial a, Serial b, Serial c) =>
+                   --    (a -> b -> c -> d) -> Series d
+  , cons4          -- :: (Serial a, Serial b, Serial c, Serial d) =>
+                   --    (a -> b -> c -> d -> e) -> Series e
+  , cons5          -- :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
+                   --    (a -> b -> c -> d -> e -> f) -> Series f
+  , Testable       -- class Testable
+  , depthCheck     -- :: Testable a => Int -> a -> IO ()
+  , (==>)          -- :: Bool -> Bool -> Bool
+  ) where
+
+import Control.Monad
+import Control.Exception
+import System.Exit
+
+infixr 3 \/
+infixr 0 ==>
+
+-- Type class and instance helpers
+
+data Family = Algebraic [(Int, [Family])] | Builtin (Int -> [Value])
+
+data Value = Var Family Int String | Ctr Int [Value] | Prim Prim
+
+data Prim = Char Char | Int Int | Integer Integer
+
+type Series a = Int -> (Family, [[Value] -> a])
+
+class Serial a where
+  series :: Series a
+
+genSeries :: Serial a => (Family, [[Value] -> a])
+genSeries = series 0
+
+convert :: [[Value] -> a] -> Value -> a
+convert alts (Var _ _ v) = error v
+convert alts (Prim p) = head alts [Prim p]
+convert alts (Ctr n as) = (alts !! n) as
+
+(\/) :: Series a -> Series a -> Series a
+(c0 \/ c1) n = (Algebraic (cs0 ++ cs1), alts0 ++ alts1)
+  where
+    (Algebraic cs0, alts0) = c0 n
+    (Algebraic cs1, alts1) = c1 (n + 1)
+
+cons0 :: a -> Series a
+cons0 c n = (Algebraic [(n, [])], alts)
+  where
+    alts = [\_ -> c]
+
+cons1 :: Serial a => (a -> b) -> Series b
+cons1 c n = (Algebraic [(n, [fam0])], alts)
+  where
+    alts = [\(a0:_) -> c (convert alts0 a0)]
+    (fam0, alts0) = genSeries
+
+cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
+cons2 c n = (Algebraic [(n, [fam0, fam1])], alts)
+  where
+    alts = [\(a0:a1:_) -> c (convert alts0 a0) (convert alts1 a1)]
+    (fam0, alts0) = genSeries
+    (fam1, alts1) = genSeries
+
+cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
+cons3 c n = (Algebraic [(n, [fam0, fam1, fam2])], alts)
+  where
+    alts = [\(a0:a1:a2:_) -> c (convert alts0 a0)
+                               (convert alts1 a1)
+                               (convert alts2 a2)]
+    (fam0, alts0) = genSeries
+    (fam1, alts1) = genSeries
+    (fam2, alts2) = genSeries
+
+cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
+         (a -> b -> c -> d -> e) -> Series e
+cons4 c n = (Algebraic [(n, [fam0, fam1, fam2, fam3])], alts)
+  where
+    alts = [\(a0:a1:a2:a3:_) -> c (convert alts0 a0)
+                                  (convert alts1 a1)
+                                  (convert alts2 a2)
+                                  (convert alts3 a3)]
+    (fam0, alts0) = genSeries
+    (fam1, alts1) = genSeries
+    (fam2, alts2) = genSeries
+    (fam3, alts3) = genSeries
+
+
+cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
+         (a -> b -> c -> d -> e -> f) -> Series f
+cons5 c n = (Algebraic [(n, [fam0, fam1, fam2, fam3, fam4])], alts)
+  where
+    alts = [\(a0:a1:a2:a3:a4:_) -> c (convert alts0 a0)
+                                     (convert alts1 a1)
+                                     (convert alts2 a2)
+                                     (convert alts3 a3)
+                                     (convert alts4 a4)]
+    (fam0, alts0) = genSeries
+    (fam1, alts1) = genSeries
+    (fam2, alts2) = genSeries
+    (fam3, alts3) = genSeries
+    (fam4, alts4) = genSeries
+
+
+-- Useful Serial instances
+
+instance Serial Bool where
+  series = cons0 False \/ cons0 True
+
+instance Serial a => Serial (Maybe a) where
+  series = cons0 Nothing \/ cons1 Just
+
+instance (Serial a, Serial b) => Serial (Either a b) where
+  series = cons1 Left \/ cons1 Right
+
+instance Serial a => Serial [a] where
+  series = cons0 [] \/ cons2 (:)
+
+instance (Serial a, Serial b) => Serial (a, b) where
+  series = cons2 (,)
+
+instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
+  series = cons3 (,,)
+
+instance (Serial a, Serial b, Serial c, Serial d) => Serial (a, b, c, d) where
+  series = cons4 (,,,)
+
+instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
+           Serial (a, b, c, d, e) where
+  series = cons5 (,,,,)
+
+-- Primitive Serial instances
+
+instance Serial Int where
+  series _ = (fam, alts)
+    where
+      fam = Builtin (\d -> map (Prim . Int) [-d .. d])
+      alts = [\(Prim (Int i):_) -> i]
+
+instance Serial Integer where
+  series _ = (fam, alts)
+    where
+      fam = Builtin (\d -> map (Prim . Integer . toInteger) [-d .. d])
+      alts = [\(Prim (Integer i):_) -> i]
+
+instance Serial Char where
+  series _ = (fam, alts)
+    where
+      fam = Builtin (\d -> map (Prim . Char) (take (d+1) ['a'..'z']))
+      alts = [\(Prim (Char c):_) -> c]
+
+-- Refinement of partial values
+
+uniquePrefix = "UP:"
+
+lenUniquePrefix = length uniquePrefix
+
+type Position = String
+
+inst :: Int -> String -> (Int, [Family]) -> Value
+inst d s (n, fs) = Ctr n (zipWith mkVar fs ['\NUL'..])
+  where
+    mkVar fam c = Var fam d (s++[c])
+
+refine :: Position -> Value -> [Value]
+refine [] (Var (Algebraic cs) d s) = map (inst (d-1) s) cs'
+  where
+    cs' = if d == 0 then filter (null . snd) cs else cs
+refine [] (Var (Builtin f) d s) = f d
+refine (p:ps) (Ctr n as) = map (Ctr n) (refineMany p ps as)
+
+refineMany :: Char -> Position -> [Value] -> [[Value]]
+refineMany p ps as = [(xs ++ a':ys) | a' <- refine ps a]
+  where
+    (xs, a:ys) = splitAt (fromEnum p) as
+
+-- Find total instantiations of a partial value, by iterative deepening
+
+total :: Int -> Value -> [Value]
+total d val = tot d val ++ total (d-1) val
+
+tot :: Int -> Value -> [Value]
+tot lim (Prim p) = [Prim p]
+tot lim (Ctr n as) = [Ctr n as' | as' <- mapM (tot lim) as]
+tot lim (Var fam d s)
+  | d < lim = []
+  | otherwise = case fam of
+                  Builtin f -> f (d - lim)
+                  Algebraic cs -> concatMap (tot lim . inst (d-1) s) cs
+
+-- General
+
+False ==> _ = True
+True ==> a = a
+
+-- Testable class machinery
+
+data Info = Info { arguments :: [Value]
+                 , showFuncs :: [Value -> String]
+                 , apply     :: ([Value] -> Bool)
+                 }
+
+newtype Property = Prop (Int -> Int -> Info)
+
+eval :: Testable a => ([Value] -> a) -> Int -> Int -> Info
+eval a = gen where Prop gen = property a
+
+class Testable a where
+  property :: ([Value] -> a) -> Property
+
+instance Testable Bool where
+  property apply = Prop $ \depth n -> Info [] [] (apply . reverse)
+
+instance (Show a, Serial a, Testable b) => Testable (a -> b) where
+  property f =
+    Prop $ \depth n ->
+      let (fam, alts) = genSeries
+          initial = Var fam depth (uniquePrefix ++ [toEnum n])
+          val = convert alts initial
+          g (x:xs) = f xs (convert alts x)
+          info = eval g depth (n+1)
+      in  info { arguments = initial : arguments info
+               , showFuncs = (show . convert alts) : showFuncs info
+               }
+
+-- Refute
+
+refute :: Info -> IO Int
+refute info = r (arguments info)
+  where
+    r args = do res <- try (evaluate (prop args))
+                case res of
+                  Right True -> return 1
+                  Right False -> stop args "Counter example found:"
+                  Left (ErrorCall s)
+                    | take (lenUniquePrefix) s == uniquePrefix ->
+                        let (c:pos) = drop lenUniquePrefix s
+                        in  do ns <- mapM r (refineMany c pos args)
+                               return (1 + sum ns)
+                  Left e -> stop args $ "Property crashed on input:"
+
+    prop = apply info
+    disp as = zipWith ($) (showFuncs info) as
+    stop args s = do putStrLn s
+                     let args' = head [as | as <- mapM (total 0) args]
+                     mapM putStrLn (disp args')
+                     exitWith ExitSuccess
+
+depthCheck :: Testable a => Int -> a -> IO ()
+depthCheck d p =
+  do count <- refute info
+     putStrLn $  "Completed " ++ show count
+              ++ " tests without finding a counter example."
+  where
+    Prop f = property (const p)
+    info = f d 0
diff --git a/source/LazySmallCheck/Generic.hs b/source/LazySmallCheck/Generic.hs
new file mode 100644
--- /dev/null
+++ b/source/LazySmallCheck/Generic.hs
@@ -0,0 +1,144 @@
+{-# OPTIONS -fglasgow-exts #-}
+
+module LazySmallCheck.Generic
+  ( depthCheck  -- :: (Data a, Show a) => Int -> (a -> Bool) -> IO [a]
+  , (==>)       -- :: Bool -> Bool -> Bool
+  ) where
+
+import Data.Maybe
+import Data.Generics
+import Control.Exception
+import Control.Monad
+import System.Random
+import System.Exit
+
+uniquePrefix = "UP:"
+
+lenUniquePrefix = length uniquePrefix
+
+type Position = String
+
+initPData :: a
+initPData = error uniquePrefix
+
+data HLP a = HLP Int (Either a [a])
+
+refinePData :: Data a => String -> Int -> Position -> a -> [a]
+refinePData s d = r
+ where
+  depleft = d - (length s - lenUniquePrefix)
+  r :: Data a => Position -> a -> [a]
+  r [] x =
+    let dt = dataTypeOf x
+    in case dataTypeRep dt of
+         AlgRep cons ->
+           let cons = dataTypeConstrs dt
+               z x = (0, x)
+               k (i, g) = (i + 1, g (error $ s ++ [toEnum i]))
+               xs' = map (gunfold k z) cons
+           in  if   depleft > 0
+               then map snd xs'
+               else mapMaybe (\(ncon, x') ->
+                                 if   ncon == 0
+                                 then Just x'
+                                 else Nothing) xs'
+         IntRep -> mkPrim dt (mkIntConstr dt . toInteger)
+                             [-depleft .. depleft]
+         StringRep -> mkPrim dt (mkStringConstr dt . (:[]))
+                                (take (depleft+1) ['a' .. 'z'])
+         _ -> error $ "LazySmallCheck.Generic: Can't generate type "
+                   ++ dataTypeName dt
+  r (c:ps) x =
+   let p = fromEnum c
+       z y = HLP 0 (Left y)
+       k (HLP i (Left xs)) y | i == p = HLP (i + 1) (Right $ map xs (r ps y))
+       k (HLP i (Left xs)) y = HLP (i + 1) (Left $ xs y)
+       k (HLP i (Right xss)) y = HLP (i + 1) (Right $ map (\xs -> xs y) xss)
+       HLP _ (Right x') = gfoldl k z x
+   in  x'
+
+mkPrim dt mk vs = map (\i -> fromJust $ gunfold undefined Just $ mk i) vs
+
+--
+
+mapVars :: Data a => (forall b . Data b => b -> IO b) -> a -> IO a
+mapVars f = gmapM (\x -> Control.Exception.catch
+  (mapVars f x)
+  (\exc -> case exc of
+    ErrorCall s | take (length uniquePrefix) s == uniquePrefix ->
+     f x
+    _ -> throw exc
+  )
+ )
+
+-- Taken from Ralf Laemmel, SYB website
+-- Generate all terms of a given depth
+enumerate :: Data a => Int -> [a]
+enumerate 0 = []
+enumerate d = result
+   where
+     -- Getting hold of the result (type)
+     result = concat (map recurse cons')
+
+     -- Find all terms headed by a specific Constr
+     recurse :: Data a => Constr -> [a]
+     recurse con = gmapM (\_ -> enumerate (d-1)) 
+                         (fromConstr con)
+
+     -- We could also deal with primitive types easily.
+     -- Then we had to use cons' instead of cons.
+     --
+     cons' :: [Constr]
+     cons' = case dataTypeRep ty of
+              AlgRep cons -> cons
+              IntRep      -> map (mkIntConstr ty . toInteger) [-d .. d]
+              StringRep   -> map (mkStringConstr ty . (:[])) (take d ['a'..'z'])
+              --FloatRep  ->
+      where
+        ty = dataTypeOf (head result)     
+
+smallValue :: Data a => a
+smallValue = f 1
+ where
+  f d = case enumerate d of
+   [] -> f (d + 1)
+   (x:_) -> x
+
+smallInstance :: Data a => a -> IO a
+smallInstance = mapVars (\_ -> return smallValue)
+
+--
+
+refute :: (Show a, Data a) => Int -> (a -> Bool) -> IO Int
+refute d p = r initPData
+  where
+    r x = do res <- try (evaluate (p x))
+             case res of
+               Right True -> return 1
+               Right False -> stop x "Counter example found:"
+               Left (ErrorCall s)
+                 | take (lenUniquePrefix) s == uniquePrefix ->
+                     let pos = drop lenUniquePrefix s
+                     in  do ns <- mapM r (refinePData s d pos x)
+                            return (1 + sum ns)
+               Left e -> stop x "Property crashed on input:"
+
+    stop x s = do putStrLn s
+                  x' <- smallInstance x
+                  putStrLn (show x')
+                  exitWith ExitSuccess
+                     
+--
+
+depthCheck :: (Show a, Data a) => Int -> (a -> Bool) -> IO ()
+depthCheck d f = do count <- refute d f
+                    putStrLn $ "Completed " ++ show count
+                            ++  " tests without finding a counter example."
+
+--
+
+infixr 0 ==>
+
+(==>) :: Bool -> Bool -> Bool
+False ==> a = True
+True ==> a = a