diff --git a/Flite/CallGraph.hs b/Flite/CallGraph.hs
new file mode 100644
--- /dev/null
+++ b/Flite/CallGraph.hs
@@ -0,0 +1,30 @@
+module Flite.CallGraph (CallGraph, callReachableGraph, reachable) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Data.List
+
+type CallGraph = [(Id, [Id])]
+
+-- For each function, determine all its call-reachable functions.
+callReachableGraph :: Prog -> CallGraph
+callReachableGraph p = fixPoint step (zip fs cs)
+  where
+    fs = map funcName p
+    cs = map (nub . calls . funcRhs) p
+
+reachable :: CallGraph -> Id -> [Id]
+reachable g f = case lookup f g of { Nothing -> [] ; Just gs -> gs }
+
+step :: CallGraph -> Maybe CallGraph
+step g
+  | any snd joined = Just (map fst joined)
+  | otherwise = Nothing
+  where joined = map (join g) g
+
+join :: CallGraph -> (Id, [Id]) -> ((Id, [Id]), Bool)
+join g (f, fs) = ((f, reached), length fs < length reached)
+  where reached = nub (fs ++ concatMap (reachable g) fs)
+
+fixPoint :: (a -> Maybe a) -> a -> a
+fixPoint f a = case f a of { Nothing -> a ; Just b -> fixPoint f b }
diff --git a/Flite/Case.hs b/Flite/Case.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Case.hs
@@ -0,0 +1,107 @@
+module Flite.Case (caseElim, caseElimWithCaseStack) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+import Flite.State
+import Control.Monad
+import Data.List as List
+import Data.Set as Set
+import Data.Map as Map
+
+-- Assumes that pattern matching has been desugared.
+
+caseElim :: Prog -> Prog
+caseElim = caseElim' False
+
+caseElimWithCaseStack :: Prog -> Prog
+caseElimWithCaseStack = caseElim' True
+
+caseElim' :: Bool -> Prog -> Prog
+caseElim' cstk p = elim cstk fs (expandCase ft p)
+  where
+    fs = families p
+    ft = familyTable fs
+
+type Family = Set (Id, Int)
+
+families :: Prog -> [Family]
+families p
+  | check = fams
+  | otherwise = error "A constructor cannot have different arities!"
+  where
+    check = let ids = [id | (id, _) <- Set.toList (Set.unions fams)]
+            in  length ids == length (nub ids)
+
+    fams = fixMerge (List.map Set.fromList ctrs)
+
+    merge [] = []
+    merge (f:fs) = Set.unions (f:same) : merge different
+      where (same, different) = List.partition (overlap f) fs
+
+    fixMerge fs = if length fs == length fs' then fs' else fixMerge fs'
+      where fs' = merge fs
+
+    overlap f0 f1 = not (Set.null (Set.intersection f0 f1))
+
+    ctrs = fromExp fam p
+
+    fam e = List.map (concatMap getCtr) (caseAlts e)
+
+    getCtr (App (Con c) ps, e) = [(c, length ps)]
+    getCtr (p, e) = []
+
+familyTable :: [Family] -> Map Id Family
+familyTable fams =
+  Map.fromList [(id, fam) | fam <- fams, (id, arity) <- Set.toList fam]
+
+expandCase :: Map Id Family -> Prog -> Prog
+expandCase table p = onExp expand p
+  where
+    expand (Case e ((Var v, rhs):as)) = expand (Let [(v, e)] rhs)
+    expand (Case e alts@((App (Con c) ps, rhs):as)) = Case (expand e) alts'
+      where alts' = [getAlt f n | (f, n) <- Set.toAscList (table Map.! c)]
+            getAlt f n = head ([ (App (Con c) args, expand rhs)
+                               | (App (Con c) args, rhs) <- alts
+                               , c == f ] ++ [bottom f n])
+            bottom f n = (App (Con f) (replicate n (Var "_")), Bottom)
+    expand e = descend expand e
+
+elim :: Bool -> [Family] -> Prog -> Prog
+elim cstk fams p = concatMap comp p
+  where
+    ctrInfo = [ (f, (arity, i))
+              | fs <- List.map Set.toAscList fams
+              , ((f, arity), i) <- zip fs [0..] ]
+
+    comp d =
+      let ((_, ds), e) = runState (compFun (funcName d) (funcRhs d)) (1, [])
+      in  (d { funcRhs = e } : ds)
+
+    compFun fun (Con c)
+      | Prelude.null cinfo = return Bottom
+      | otherwise = return (Ctr c (fst $ head cinfo) (snd $ head cinfo))
+      where cinfo = [ci | (d, ci) <- ctrInfo, c == d]
+    compFun fun (Case e as) =
+      return App `ap` compFun fun e `ap` calts fun as
+    compFun fun e = descendM (compFun fun) e
+
+    calts fun as = 
+      do es' <- mapM (compFun fun) es
+         let fvs = nub $ concat $ zipWith (freeVarsExcept) vss es'
+         fs <- zipWithM (calt fun fvs) vss es'
+         let alts = Alts fs (length fvs)
+         return ([alts] ++ [Int 0 | cstk && List.null fvs] ++ List.map Var fvs)
+      where (ps, es) = unzip as
+            vss = List.map (\(App _ args) -> [v | Var v <- args]) ps
+
+    calt fun fvs vs e =
+      do n <- newAlt
+         let name = fun ++ "#" ++ show n
+         let args = vs ++ ["$ct" | not cstk || (cstk && List.null fvs)] ++ fvs
+         addDecl (Func name (List.map Var args) e)
+         return name
+
+    newAlt = S (\(i, ds) -> ((i+1, ds), i))
+
+    addDecl d = S (\(i, ds) -> ((i, ds ++ [d]), ()))
diff --git a/Flite/ConcatApp.hs b/Flite/ConcatApp.hs
new file mode 100644
--- /dev/null
+++ b/Flite/ConcatApp.hs
@@ -0,0 +1,22 @@
+module Flite.ConcatApp where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+
+concatApps :: Prog -> Prog
+concatApps = onExp conc
+  where
+    conc (App e []) = conc e
+    conc (App (App f xs) ys) = descend conc (App f (xs ++ ys))
+    conc e = descend conc e
+
+concatNonPrims :: Prog -> Prog
+concatNonPrims = onExp conc
+  where
+    conc (App e []) = conc e
+    conc (App (Fun f) xs) | isPrimId f = App (Fun f) (map conc xs)
+    conc (App (App (Fun f) xs) ys) | isPrimId f =
+      App (App (Fun f) (map conc xs)) (map conc ys)
+    conc (App (App f xs) ys) = descend conc (App f (xs ++ ys))
+    conc e = descend conc e
diff --git a/Flite/Descend.hs b/Flite/Descend.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Descend.hs
@@ -0,0 +1,17 @@
+module Flite.Descend where
+
+import Control.Monad
+import Flite.Identity
+import Flite.Writer
+
+class Descend a where
+  descendM :: Monad m => (a -> m a) -> a -> m a
+
+descend :: Descend a => (a -> a) -> a -> a
+descend f a = runIdentity (descendM (return . f) a)
+
+extract :: Descend a => (a -> [b]) -> a -> [b]
+extract f = fst . runWriter . descendM (\a -> writeMany (f a) >> return a)
+
+universe :: Descend a => a -> [a]
+universe a = a : extract universe a
diff --git a/Flite/Fresh.hs b/Flite/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Fresh.hs
@@ -0,0 +1,11 @@
+module Flite.Fresh where
+
+data Fresh a = Fresh { runFresh :: String -> Int -> (Int, a) }
+
+instance Monad Fresh where
+  return a = Fresh (\s i -> (i, a))
+  m >>= f  = Fresh (\s i -> case runFresh m s i of
+                              (j, a) -> runFresh (f a) s j)
+
+fresh :: Fresh String
+fresh = Fresh (\s i -> (i+1, s ++ show i))
diff --git a/Flite/Identify.hs b/Flite/Identify.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Identify.hs
@@ -0,0 +1,21 @@
+module Flite.Identify where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+
+-- Rewrites (Var n) to (Fun n) where n refers to a function.
+
+identifyFuncs :: Prog -> Prog
+identifyFuncs p =
+  [Func f xs (fun (concatMap patVars xs) e) | Func f xs e <- p]
+  where
+    fs = funcs p
+
+    fun vs (Case e as) =
+      Case (fun vs e) [(p, fun (vs ++ patVars p) e) | (p, e) <- as]
+    fun vs (Let bs e) = 
+      let ws = vs ++ map fst bs
+      in  Let [(v, fun ws e) | (v, e) <- bs] (fun ws e)
+    fun vs (Var v) | v `elem` fs && v `notElem` vs = Fun v
+    fun vs e = descend (fun vs) e
diff --git a/Flite/Identity.hs b/Flite/Identity.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Identity.hs
@@ -0,0 +1,7 @@
+module Flite.Identity where
+
+newtype Identity a = I { runIdentity :: a }
+
+instance Monad Identity where
+  return a = I a
+  I a >>= f = f a
diff --git a/Flite/Inline.hs b/Flite/Inline.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Inline.hs
@@ -0,0 +1,60 @@
+module Flite.Inline (InlineFlag(..), inline, inlineTop) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.ConcatApp
+import Flite.Descend
+import Flite.Fresh
+import Control.Monad
+import Flite.Let
+
+data InlineFlag = NoInline | InlineAll | InlineSmall Int
+
+checkInline :: InlineFlag -> Int -> Bool
+checkInline NoInline n = False
+checkInline InlineAll n = True
+checkInline (InlineSmall bound) n = n <= bound
+
+inlineTop :: InlineFlag -> Prog -> Fresh Prog
+inlineTop NoInline p = return p
+inlineTop i p = inline i p
+            >>= inlineLinearLet
+            >>= inlineSimpleLet
+
+-- In-line saturated applications of small, non-primitive functions
+-- that do not have directly recursive definitions.
+
+inline :: InlineFlag -> Prog -> Fresh Prog
+inline i p = onExpM (inl []) p
+  where
+    inl tabu (Fun f)
+      | f `notElem` tabu =
+        case lookupFuncs f p of
+          Func f [] rhs:_ | checkInline i (numApps rhs) -> inl (f:tabu) rhs
+          _ -> return (Fun f)
+    inl tabu (App (Fun f) es)
+      | f `notElem` tabu =
+        case lookupFuncs f p of
+          Func f args rhs:_
+            | f `notElem` calls rhs
+           && length args <= length es
+           && checkInline i (numApps rhs) ->
+                do let vs = map (\(Var v) -> v) args
+                   ws <- mapM (\_ -> fresh) vs
+                   let rhs' = substMany rhs (zip (map Var ws) vs)
+                   inl (f:tabu)
+                       (mkApp (mkLet (zip ws es) rhs') (drop (length vs) es))
+          _ -> liftM (mkApp (Fun f)) (mapM (inl tabu) es)
+    inl tabu e = descendM (inl tabu) e
+
+
+mkApp f [] = f
+mkApp f es = App f es
+
+mkLet [] e = e
+mkLet bs e = Let bs e
+
+numApps (App f xs) = 1 + sum (map numApps (f:xs))
+numApps (Let bs e) = sum (map numApps (e:map snd bs))
+numApps (Case e as) = max 1 (numApps e) + sum (map (numApps . snd) as)
+numApps e = 0;
diff --git a/Flite/Let.hs b/Flite/Let.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Let.hs
@@ -0,0 +1,55 @@
+module Flite.Let(inlineLinearLet, inlineSimpleLet, liftLet) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+import Flite.Fresh
+import List
+
+mkLet :: [Binding] -> Exp -> Exp
+mkLet [] e = e
+mkLet bs e = Let bs e
+
+inlineLetWhen :: ([Binding] -> Exp -> Binding -> Bool) -> Prog -> Fresh Prog
+inlineLetWhen f p = onExpM freshen p >>= return . onExp inline
+  where
+    inline (Let bs e) = mkLet (zip vs1 (map inline es1')) (inline e')
+      where (vs, es) = unzip bs
+            (bs0, bs1) = partition (f bs e) bs
+            (vs1, es1) = unzip bs1
+            (e':es1') = foldr (\(v, e) -> map (subst e v)) (e:es1) bs0
+    inline e = descend inline e
+
+inlineLinearLet :: Prog -> Fresh Prog
+inlineLinearLet = inlineLetWhen linear
+  where
+    linear bs e (v, _) = refs v (e:map snd bs) <= 1
+    refs v es = sum (map (varRefs v) es)
+
+inlineSimpleLet :: Prog -> Fresh Prog
+inlineSimpleLet = inlineLetWhen simple
+  where
+    simple _ _ (_, rhs) = simp rhs
+    simp (App e []) = simp e
+    simp (App e es) = False
+    simp (Case e as) = False
+    simp _ = True
+
+liftLet :: Prog -> Fresh Prog
+liftLet p = do p' <- onExpM freshen p
+               return (onExp lift p')
+  where
+    lift e = mkLet [(v, liftInCase rhs) | (v, rhs) <- binds e]
+                   (liftInCase (dropBinds e))
+
+    liftInCase (Case e as) = Case e [(p, lift e) | (p, e) <- as]
+    liftInCase e = descend liftInCase e
+
+    dropBinds (Let bs e) = dropBinds e
+    dropBinds (Case e as) = Case (dropBinds e) as
+    dropBinds e = descend dropBinds e
+
+    binds (Let bs e) = binds e ++ [(v, dropBinds e) | (v, e) <- bs]
+                               ++ concatMap (binds . snd) bs
+    binds (Case e as) = binds e
+    binds e = extract binds e
diff --git a/Flite/Matching.hs b/Flite/Matching.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Matching.hs
@@ -0,0 +1,92 @@
+module Flite.Matching (desugarEqn, desugarCase) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+import Flite.Fresh
+import Data.List
+import Data.Maybe
+import Control.Monad
+
+desugarEqn :: Prog -> Fresh Prog
+desugarEqn p = mapM (\(f, arity, qs) -> 
+                      do us <- mapM (\_ -> fresh) [1..arity]
+                         rhs <- match us qs
+                         return (Func f (map Var us) rhs)
+                    ) (groupEqn p)
+
+groupEqn :: Prog -> [(String, Int, [Equation])]
+groupEqn p
+  | all (rect . map funcArgs) dss = map gr dss
+  | otherwise = error "Function equations cannot have different arities!"
+  where
+    dss = groupBy (\a b -> funcName a == funcName b) p
+
+    gr ds = ( funcName (head ds)
+            , length (funcArgs (head ds))
+            , zip (map funcArgs ds) (map funcRhs ds)
+            )
+
+    rect :: [[a]] -> Bool
+    rect = (== 1) . length . groupBy (==) . map length
+
+desugarCase :: Prog -> Fresh Prog
+desugarCase = onExpM (\e -> caseVar e >>= desugar)
+  where
+    desugar (Case (Var v) as) =
+      do as' <- mapM (\(p, e) -> do e' <- desugar e; return (p, e')) as
+         match [v] [([p], e) | (p, e) <- as']
+    desugar e = descendM desugar e
+
+caseVar :: Exp -> Fresh Exp
+caseVar (Case e as) =
+  case getVar e of
+    Nothing -> do v <- fresh
+                  caseVar (Let [(v, e)] (Case (Var v) as))
+    Just v -> descendM caseVar (Case (Var v) as)
+  where v = getVar e
+caseVar e = descendM caseVar e
+
+getVar :: Exp -> Maybe Id
+getVar (Var v) = Just v
+getVar (App e []) = getVar e
+getVar e = Nothing
+
+-- Wadler's algorithm for compilation of *uniform* pattern matching,
+-- from "The Implementation of Functional Programming Languages".
+
+type Equation = ([Pat], Exp)
+
+isVar :: Equation -> Bool
+isVar (Var v:ps, e) = True
+isVar (App (Con c) args:ps, e) = False
+
+isCon :: Equation -> Bool
+isCon e = not (isVar e)
+
+getCon :: Equation -> (Id, [Pat])
+getCon (App (Con c) args:ps, e) = (c, args)
+
+match :: [Id] -> [Equation] -> Fresh Exp
+match [] [q] = return (snd q)
+match (u:us) qs
+  | all isVar qs = match us [(ps, subst (Var u) v e) | (Var v:ps, e) <- qs]
+  | all isCon qs = do alts <- mapM (matchClause us) (groupEqns qs)
+                      return (Case (Var u) alts)
+match _ _ = error "Non-uniform pattern matching is disallowed!"
+
+groupEqns :: [Equation] -> [(Id, Int, [Equation])]
+groupEqns [] = []
+groupEqns (q:qs)
+  | all ((== arity) . length . snd . getCon) qs0 =
+      (name, arity, qs0) : groupEqns qs1
+  | otherwise = error ("Constructor `" ++ name ++ "` has different arities!")
+  where (qs0, qs1) = partition ((== name) . fst . getCon) (q:qs)
+        name = fst (getCon q)
+        arity = length (snd (getCon q))
+
+matchClause :: [Id] -> (Id, Int, [Equation]) -> Fresh Alt
+matchClause us (c, arity, qs) =
+  do us' <- mapM (\_ -> fresh) [1..arity]
+     alts <- match (us' ++ us) [(ps' ++ ps, e) | (App (Con c) ps':ps, e) <- qs]
+     return (App (Con c) (map Var us'), alts)
diff --git a/Flite/Parsec/Parse.hs b/Flite/Parsec/Parse.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Parsec/Parse.hs
@@ -0,0 +1,118 @@
+module Flite.Parsec.Parse where
+	import Flite.Syntax
+	import Flite.Pretty
+
+	import Control.Applicative
+	import Control.Monad
+	import Data.Char
+	import Text.ParserCombinators.Parsec hiding (many, option, (<|>))
+	import Text.ParserCombinators.Parsec.Language
+	import qualified Text.ParserCombinators.Parsec.Token as T
+	
+	flite = T.makeTokenParser $ emptyDef
+		{ commentLine 		= "--"
+		, nestedComments 	= False
+		, identStart		= letter
+		, identLetter		= alphaNum
+		, opStart			= opLetter haskellStyle
+		, opLetter			= oneOf "<=>-+/"
+		, reservedNames		= ["case", "of", "let", "in", "if", "then", "else"]
+		, caseSensitive		= True
+		}
+	
+	identifier = T.identifier flite
+	reservedOp = T.reservedOp flite
+	reserved = T.reserved flite
+	natural = T.natural flite
+	parens = T.parens flite
+	semi = T.semi flite
+	braces = T.braces flite
+	symbol = T.symbol flite
+	operator = T.operator flite
+	charLiteral = T.charLiteral flite
+	stringLiteral = T.stringLiteral flite
+	
+	instance Applicative (GenParser s a) where
+	    pure  = return
+	    (<*>) = ap
+	
+	instance Alternative (GenParser s a) where
+	    empty = mzero
+	    (<|>) = mplus
+	
+	prog :: Parser Prog
+	prog = block defn
+	
+	block :: Parser a -> Parser [a]
+	block p = braces (p `sepEndBy` semi) <?> "block"
+	
+	primitives = ["(+)", "(-)", "(==)", "(/=)", "(<=)", "emit", "emitInt"]
+	
+	prim :: Parser Id
+	prim = try $ do
+		v <- identifier
+		 <|> pure (++) <*> symbol "(" <*> (pure (++) <*> operator <*> symbol ")")
+		if v `elem` primitives
+			then return v
+			else unexpected (show v) <?> "primitive"
+	
+	var :: Parser Id
+	var = try $ do
+		v <- identifier
+		if isLower (head v)
+			then return v
+			else unexpected ("constructor " ++ show v) <?> "variable"
+	
+	con :: Parser Id
+	con = try $ do
+		c <- identifier
+		if isUpper (head c)
+			then return c
+			else unexpected ("variable " ++ show c) <?> "constructor"
+	
+	defn :: Parser Decl
+	defn = pure Func <*> var <*> many pat <*> (reservedOp "=" *> expr) <?> "definition"
+		
+	pat :: Parser Exp
+	pat = pure Var <*> var
+		<|> pure App <*> (pure Con <*> con) <*> pure []
+		<|> parens pat'
+		<?> "pattern"
+	
+	pat' :: Parser Exp
+	pat' = pure Var <*> var
+		<|> pure App <*> (pure Con <*> con) <*> many pat
+	
+	expr :: Parser Exp
+	expr = pure App <*> expr' <*> many expr'
+	
+	expr' :: Parser Exp
+	expr' = pure Case <*> (reserved "case" *> expr) <*> (reserved "of" *> block alt)
+		<|> pure Let <*> (reserved "let" *> block bind) <*> (reserved "in" *> expr)
+		<|> pure ifthenelse <*> (reserved "if" *> expr) <*> (reserved "then" *> expr) <*> (reserved "else" *> expr)
+		<|> pure Fun <*> prim
+		<|> pure Var <*> var
+		<|> pure Con <*> con
+		<|> pure Int <*> (pure fromInteger <*> natural)
+		<|> pure (Int . ord) <*> charLiteral
+		<|> pure stringExp <*> stringLiteral
+		<|> parens expr
+	
+	ifthenelse :: Exp -> Exp -> Exp -> Exp
+	ifthenelse x y z = Case x [(App (Con "True") [], y), (App (Con "False") [], z)]
+	
+	stringExp :: String -> Exp
+	stringExp [] = App (Con "Nil") []
+	stringExp (x:xs) = App (Con "Cons") [Int . ord $ x, stringExp xs]
+	
+	alt :: Parser Alt
+	alt = pure (,) <*> pat' <*> (reservedOp "->" *> expr)
+	
+	bind :: Parser Binding
+	bind = pure (,) <*> var <*> (reservedOp "=" *> expr)
+	
+	parseProgFile :: SourceName -> IO Prog
+	parseProgFile f = parseFromFile prog f >>= \result -> case result of
+															Left e	-> error . show $ e
+															Right p	-> return p
+															
diff --git a/Flite/Pretty.hs b/Flite/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Pretty.hs
@@ -0,0 +1,44 @@
+module Flite.Pretty where
+
+import Flite.Syntax
+import Data.List
+
+consperse :: [a] -> [[a]] -> [a]
+consperse x xs = concat (intersperse x xs)
+
+pretty :: Prog -> String
+pretty p = "{\n" ++ concatMap show p ++ "}"
+
+instance Show Decl where
+  show (Func name args rhs) = name ++ " "
+                           ++ consperse " " (map showArg args)
+                           ++ " = "
+                           ++ show rhs ++ ";\n"
+
+instance Show Exp where
+  show (App e es) = consperse " " (showArg e : map showArg es)
+  show (PrimApp p es) = "{" ++ show (App (Prim p) es) ++ "}"
+  show (Case e as) = "case " ++ show e ++ " of " ++ showBlock showAlt as
+  show (Let bs e) = "let " ++ showBlock showBind bs ++ " in " ++ show e
+  show (Var v) = v
+  show (Fun f) = f
+  show (Prim f) = f
+  show (Con c) = c
+  show (Int i) = show i
+  show (Alts as i) = "[" ++ consperse "," as ++ "]"
+  show Bottom = "_|_"
+  show (Ctr c arity i) = c
+
+showArg :: Exp -> String
+showArg (App e []) = showArg e
+showArg (App e es) = "(" ++ show (App e es) ++ ")"
+showArg e = show e
+
+showBlock :: (a -> String) -> [a] -> String
+showBlock f as = "{ " ++ consperse "; " (map f as) ++ " }"
+
+showAlt :: Alt -> String
+showAlt (p, e) = show p ++ " -> " ++ show e
+
+showBind :: Binding -> String
+showBind (v, e) = v ++ " = " ++ show e
diff --git a/Flite/Syntax.hs b/Flite/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Syntax.hs
@@ -0,0 +1,58 @@
+module Flite.Syntax where
+
+type Prog = [Decl]
+
+data Decl = Func { funcName :: Id
+                 , funcArgs :: [Pat]
+                 , funcRhs  :: Exp }
+
+type Id = String
+
+data Exp = App Exp [Exp]
+         | Case Exp [Alt]
+         | Let [Binding] Exp
+         | Var Id
+         | Con Id
+         | Fun Id
+         | Int Int
+
+           -- The following may be introduced by various transformations,
+           -- but not by the parser.
+         | Bottom
+         | Alts [Id] Int
+         | Ctr Id Int Int
+         | Lam [Id] Exp
+
+           -- For speculative evaluation of primitive redexes.
+         | PrimApp Id [Exp]
+         | Prim Id
+  deriving Eq
+
+type Pat = Exp
+
+type Alt = (Pat, Exp)
+
+type Binding = (Id, Exp)
+
+type App = [Exp]
+
+-- Primitive functions
+
+isPrimId :: Id -> Bool
+isPrimId p = isBinaryPrim p || isUnaryPrim p
+
+isBinaryPrim :: Id -> Bool
+isBinaryPrim "(+)"  = True
+isBinaryPrim "(-)"  = True
+isBinaryPrim "(==)" = True
+isBinaryPrim "(/=)" = True
+isBinaryPrim "(<=)" = True
+isBinaryPrim _      = False
+
+isUnaryPrim :: Id -> Bool
+isUnaryPrim "emit" = True
+isUnaryPrim "emitInt" = True
+isUnaryPrim _ = False
+
+isPredexId :: Id -> Bool
+isPredexId = isBinaryPrim
diff --git a/Flite/Traversals.hs b/Flite/Traversals.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Traversals.hs
@@ -0,0 +1,112 @@
+module Flite.Traversals where
+
+import Flite.Syntax
+import Flite.Descend
+import Control.Monad
+import Data.List
+import Flite.Fresh
+
+funcs :: Prog -> [String]
+funcs p = [f | Func f args rhs <- p]
+
+onExp :: (Exp -> Exp) -> Prog -> Prog
+onExp f p = [Func g args (f rhs) | Func g args rhs <- p]
+
+onExpM :: Monad m => (Exp -> m Exp) -> Prog -> m Prog
+onExpM f = mapM (\(Func g args rhs) ->
+             do rhs' <- f rhs
+                return (Func g args rhs'))
+
+fromExp :: (Exp -> [a]) -> Prog -> [a]
+fromExp f p = concat [f rhs | Func g args rhs <- p]
+
+instance Descend Exp where
+  descendM f (App e es) = return App `ap` f e `ap` mapM f es
+  descendM f (Case e as) = return Case `ap` f e `ap` mapM g as
+    where g (p, e) = return (,) `ap` return p `ap` f e
+  descendM f (Let bs e) = return Let `ap` mapM g bs `ap` f e
+    where g (v, e) = return (,) `ap` return v `ap` f e
+  descendM f (PrimApp p es) = return (PrimApp p) `ap` mapM f es
+  descendM f (Lam vs e) = return (Lam vs) `ap` f e
+  descendM f e = return e
+
+subst :: Exp -> Id -> Exp -> Exp
+subst x v = sub
+  where
+    sub (Var w) | v == w = x
+    sub (Let bs e) | v `elem` map fst bs = Let bs e
+    sub (Case e as) = Case (sub e)
+                           [ (p, if v `elem` patVars p then e else sub e)
+                           | (p, e) <- as ]
+    sub (Lam vs e) = if v `elem` vs then Lam vs e else Lam vs (sub e)
+    sub e = descend sub e
+
+substMany :: Exp -> [(Exp, Id)] -> Exp
+substMany = foldr (uncurry subst)
+
+patVars :: Pat -> [Id]
+patVars (App e es) = concatMap patVars (e:es)
+patVars (Var v) = [v]
+patVars p = []
+
+caseAlts :: Exp -> [[Alt]]
+caseAlts (Case exp alts) = alts : caseAlts exp ++ rest
+  where rest = concatMap (caseAlts . snd) alts
+caseAlts e = extract caseAlts e
+
+freeVarsExcept :: [Id] -> Exp -> [Id]
+freeVarsExcept vs e = nub (freeVarsExcept' vs e)
+
+freeVarsExcept' :: [Id] -> Exp -> [Id]
+freeVarsExcept' vs e = fv vs e
+  where
+    fv vs (Case e as) =
+      fv vs e ++ concat [fv (patVars p ++ vs) e | (p, e) <- as]
+    fv vs (Let bs e) = let ws = map fst bs ++ vs
+                       in  fv ws e ++ concatMap (fv ws . snd) bs
+    fv vs (Var w) = [w | w `notElem` vs]
+    fv vs (Lam ws e) = fv (ws ++ vs) e
+    fv vs e = extract (fv vs) e
+
+freeVars :: Exp -> [Id]
+freeVars e = nub (freeVarsExcept' [] e)
+
+varRefs :: Id -> Exp -> Int
+varRefs v = length . filter (== v) . freeVarsExcept' []
+
+calls :: Exp -> [Id]
+calls (Fun f) = [f]
+calls e = extract calls e
+
+lookupFuncs :: Id -> Prog -> [Decl]
+lookupFuncs f p = [Func g args rhs | Func g args rhs <- p, f == g]
+
+freshen :: Exp -> Fresh Exp
+freshen (Let bs e) =
+  do let (vs, es) = unzip bs
+     e' <- freshen e
+     es' <- mapM freshen es
+     ws <- mapM (\_ -> fresh) vs
+     let s = zip (map Var ws) vs
+     return $ Let (zip ws (map (flip substMany s) es'))
+                  (substMany e' s)
+freshen (Case e as) = return Case `ap` freshen e `ap` mapM freshenAlt as
+freshen e = descendM freshen e
+
+freshenPat :: Pat -> Fresh Pat
+freshenPat (Var _) = return Var `ap` fresh
+freshenPat p = descendM freshenPat p
+
+freshenAlt :: (Pat, Exp) -> Fresh (Pat, Exp)
+freshenAlt (p, e) =
+  do p' <- freshenPat p
+     e' <- freshen e
+     let s = zip (map Var (patVars p')) (patVars p)
+     return (p', substMany e' s)
+
+freshBody :: ([Id], Exp) -> Fresh ([Id], Exp)
+freshBody (vs, e) =
+  do ws <- mapM (\_ -> fresh) vs
+     e' <- freshen e
+     let s = zip (map Var ws) vs
+     return (ws, substMany e' s)
diff --git a/Flite/Writer.hs b/Flite/Writer.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Writer.hs
@@ -0,0 +1,16 @@
+module Flite.Writer where
+
+data Writer w a = W [w] a
+
+instance Monad (Writer w) where
+  return a = W [] a
+  W w0 a0 >>= f = case f a0 of W w1 a1 -> W (w0 ++ w1) a1
+
+runWriter :: Writer w a -> ([w], a)
+runWriter (W ws a) = (ws, a)
+
+write :: w -> Writer w ()
+write w = W [w] ()
+
+writeMany :: [w] -> Writer w ()
+writeMany ws = W ws ()
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,184 @@
+================================
+F-lite: a core subset of Haskell
+Matthew N, 26 November 2008
+================================
+
+F-lite is a core subset of Haskell.  Unlike GHC Core and Yhc Core,
+F-lite has a concrete syntax.  You can write F-lite programs in a
+file, and pass them to the F-lite interpreter or compiler.  Another
+way to view F-lite is as a minimalist lazy functional language.
+
+F-lite is untyped
+-----------------
+
+But as it is a subset of Haskell, you can use a Haskell implementation
+to type-check F-lite programs.  
+
+EXAMPLE 0: F-lite definition of 'append'.  Definitions of 'Nil' and
+'Cons' are not required - there is no need to define algebraic data
+types.
+
+  append Nil ys = ys;
+  append (Cons x xs) ys = Cons x (append xs ys);
+
+(The use of semi-colons to seperate equations is mandatory.)
+
+F-lite supports uniform pattern matching
+----------------------------------------
+
+Pattern matching is uniform if and only if the order of equations
+doesn't matter (Wadler '86).  Uniform pattern matching can be easily
+and efficiently compiled to core case expressions.  A core case
+expression is one whose patterns all have the form 'constructor
+applied to zero or more variables'.  The fact that the order of
+equations doesn't matter is also useful when transforming functional
+programs, for example by fold/unfold transformations.
+
+EXAMPLE 1: F-lite definition of 'zipWith', illustrating uniform
+pattern matching.
+
+  zipWith f Nil ys = Nil;
+  zipWith f (Cons x xs) Nil = Nil;
+  zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys);
+
+EXAMPLE 2: F-lite definition of 'init', illustrating nested,
+incomplete, uniform pattern matching.
+
+  init (Cons x Nil) = Nil;
+  init (Cons x (Cons y ys)) = Cons x (init (Cons y ys));
+
+EXAMPLE 3: F-lite definition of 'init', using a case expression.
+
+  init xs = case xs of {
+              Cons x Nil -> Nil;
+              Cons x (Cons y ys) -> Cons x (init (Cons y ys));
+            };
+
+(The use of semi-colons to seperate case alternatives is mandatory.)
+
+F-lite supports 'let'-expressions
+---------------------------------
+
+But they may only bind expressions to variables (not patterns).
+
+EXAMPLE 4: F-lite definition of 'pow', the power-list function,
+illustrating a let expression.
+
+  pow Nil = Cons Nil Nil;
+  pow (Cons x xs) = let { rest = pow xs } in
+                      append rest (map (Cons x) rest);
+
+EXAMPLE 5: F-lite definition of 'repeat', using a let expression to
+introduce a cyclic data structure.
+
+  repeat x = let { xs = Cons x xs } in xs;
+
+F-lite supports primitive integers
+----------------------------------
+
+Finite precision integers along with the following arithmetic
+functions are allowed: (+), (-), (<=), (==), (/=).  The latter three
+return 'True' or 'False' accordingly.  These operators must be written
+in prefix form and cannot be partially applied.
+
+EXAMPLE 6: F-lite definition of 'negate'.
+
+  negate n = (-) 0 n;
+
+(Negative literals are not supported.)
+
+EXAMPLE 7:  F-lite definition of 'fromTo'.
+
+  fromTo n m = case (<=) n m of {
+                 True -> Cons n (fromTo ((+) n 1) m);
+                 False -> Nil;
+               };
+
+F-lite supports printing
+------------------------
+
+Two primitives, 'emit' and 'emitInt', are provided for printing characters
+and integers respectively.
+
+EXAMPLE 8: Printing the string "hi!" in F-lite.
+
+  sayHi k = emit 'h' (emit 'i' (emit '!' k))
+
+When evaluated, 'sayHi k' will print "hi!" and return 'k' (the
+continuation).
+
+EXAMPLE 9: 'Hello world' in F-lite.
+
+  emitStr Nil k = k;
+  emitStr (Cons x xs) k = emit x (emitStr xs k);
+
+  main = emitStr "Hello world!\n" 0;
+
+String literals are internally translated to 'Nil'-'Cons' lists of
+characters.  The result of the 'main' function is expected to be an
+integer - the displaying of any output must be done explicitly by the
+programmer.
+
+EXAMPLE 10: Full F-lite program to display the 10th fibonacci number.
+
+  {
+
+  fib n = case (<=) n 1 of {
+            True  -> 1;
+            False -> (+) (fib ((-) n 2)) (fib ((-) n 1));
+          };
+
+  emitStr Nil k = k;
+  emitStr (Cons x xs) k = emit x (emitStr xs k);
+
+  main = emitStr "fib(10) = " (emitInt (fib 10) (emit '\n' 0));
+
+}
+
+The braces enclosing the program are indeed mandatory.  The primitive
+'emitInt' function is like 'emit' but prints an integer rather than a
+character.  Both 'emit' and 'emitInt' must be applied to at least one
+argument.
+
+Our implementation
+------------------
+
+Our F-lite implementation includes both an interpreter (written in
+Haskell) and a compiler (to C code - see Memo 22).  It works in both
+Hugs and GHC.  For example, in the source directory, using Hugs:
+
+  > runhugs fl-pure.hs examples/Fib.hs
+  fib(10) = 89
+
+and likewise using GHC:
+
+  > ghc -O2 --make fl-pure -o fl
+
+  > ./fl examples/Fib.hs
+  fib(10) = 89
+
+A Cabal script can be used to install the parsec version using GHC:
+
+  > cabal install
+  
+  > flite examples/Fib.hs
+  fib(10) = 89
+
+or even the pure version:
+
+  > cabal install -f "pure"
+
+  > flite-pure examples/Fib.hs
+  fib(10) = 89
+
+To compile F-lite programs, use the '-c' command-line option,
+and redirect the output to a C file of your choice.
+
+  > flite -c ../examples/Fib.hs > /tmp/Fib.c
+
+The resulting C file can be compiled (with optimisations) using GCC:
+
+  > gcc -O3 /tmp/Fib.c -o Fib
+
+  > ./Fib
+  fib(10) = 89
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/examples/Adjoxo.hs b/examples/Adjoxo.hs
new file mode 100644
--- /dev/null
+++ b/examples/Adjoxo.hs
@@ -0,0 +1,106 @@
+{
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+bestOf Win v = Win;
+bestOf Loss v = v;
+bestOf Draw Win = Win;
+bestOf Draw Draw = Draw;
+bestOf Draw Loss = Draw;
+
+inverse Loss = Win;
+inverse Draw = Draw;
+inverse Win  = Loss;
+
+fromTo n m = case (<=) n m of {
+               True -> Cons n (fromTo ((+) n 1) m);
+               False -> Nil;
+             };
+
+cmp a b = 
+  case (==) a b of {
+    True -> EQ;
+    False -> case (<=) a b of { True -> LT ; False -> GT };
+  };
+
+insert x Nil = Cons x Nil;
+insert x (Cons y ys) = case (<=) x y of {
+                         True -> Cons x (Cons y ys);
+                         False -> Cons y (insert x ys);
+                       };
+
+foldr1 f (Cons x Nil) = x;
+foldr1 f (Cons x (Cons y ys)) = f x (foldr1 f (Cons y ys));
+
+diff Nil ys = Nil;
+diff (Cons x xs) Nil = Cons x xs;
+diff (Cons x xs) (Cons y ys) =
+  case cmp x y of {
+    LT -> Cons x (diff xs (Cons y ys));
+    EQ -> diff xs ys;
+    GT -> diff (Cons x xs) ys;
+  };
+
+null Nil = True;
+null (Cons x xs) = False;
+
+subset xs ys = null (diff xs ys);
+
+or False x = x;
+or True x = True;
+
+hasLine p =
+  or (subset (Cons 1 (Cons 2 (Cons 3 Nil))) p)
+    (or (subset (Cons 4 (Cons 5 (Cons 6 Nil))) p)
+      (or (subset (Cons 7 (Cons 8 (Cons 9 Nil))) p)
+        (or (subset (Cons 1 (Cons 4 (Cons 7 Nil))) p)
+          (or (subset (Cons 2 (Cons 5 (Cons 8 Nil))) p)
+            (or (subset (Cons 3 (Cons 6 (Cons 9 Nil))) p)
+              (or (subset (Cons 1 (Cons 5 (Cons 9 Nil))) p)
+                (subset (Cons 3 (Cons 5 (Cons 7 Nil))) p)))))));
+
+length Nil = 0;
+length (Cons x xs) = (+) 1 (length xs);
+
+gridFull ap pp = (==) ((+) (length ap) (length pp)) 9;
+
+analysis ap pp =
+  case hasLine pp of {
+    True -> Loss;
+    False ->
+      case gridFull ap pp of {
+        True -> Draw;
+        False -> foldr1 bestOf (map (moveval ap pp)
+                   (diff (diff (fromTo 1 9) ap) pp));
+      };
+  };
+
+moveval ap pp m = inverse (analysis pp (insert m ap));
+
+adjudicate os xs =
+  case cmp (length os) (length xs) of {
+    GT -> report (analysis xs os) X;
+    EQ -> case hasLine xs of {
+            True -> report Win X;
+            False -> case hasLine os of {
+                       True -> report Win O;
+                       False -> report (analysis xs os) X;
+                     };
+          };
+    LT -> report (analysis os xs) O;
+  };
+
+report Loss s = side (opp s);
+report Win  s = side s;
+report Draw p = 'D';
+
+opp O = X;
+opp X = O;
+
+side O = 'O';
+side X = 'X';
+
+main = emit (adjudicate Nil Nil) 0;
+
+}
diff --git a/examples/Cichelli.hs b/examples/Cichelli.hs
new file mode 100644
--- /dev/null
+++ b/examples/Cichelli.hs
@@ -0,0 +1,200 @@
+{
+
+min m n = case ((<=) m n) of { True -> m ; False -> n ; } ;
+
+max m n = case ((<=) m n) of { True -> n ; False -> m ; } ;
+
+gt  m n = case ((<=) m n) of { True -> False ; False -> True ; } ;
+
+head (Cons x xs) = x ;
+
+last (Cons x xs) = case null xs of {
+                   True  -> x ;
+                   False -> last xs ;
+                   } ;
+
+null Nil         = True ;
+null (Cons x xs) = False ;
+
+length Nil         = 0 ;
+length (Cons x xs) = (+) 1 (length xs) ;
+
+append Nil         ys = ys ;
+append (Cons x xs) ys = Cons x (append xs ys) ;
+
+map f Nil         = Nil ;
+map f (Cons x xs) = Cons (f x) (map f xs) ;
+
+concatMap f Nil         = Nil ;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs) ;
+
+elem x Nil         = False ;
+elem x (Cons y ys) =
+  case (==) x y of { True -> True ; False -> elem x ys ; } ;
+
+foldr f z Nil         = z ;
+foldr f z (Cons x xs) = f x (foldr f z xs) ;
+
+filter p Nil         = Nil ;
+filter p (Cons x xs) =
+  case p x of { True -> Cons x (filter p xs) ; False -> filter p xs ; } ;
+
+enumFromTo m n = 
+  case (<=) m n of { True -> Cons m (enumFromTo ((+) m 1) n) ; False -> Nil ; } ;
+
+assoc x (Cons (Pair y z) yzs) =
+  case (==) x y of { True -> z ; False -> assoc x yzs ; } ;
+
+assocm x Nil                   = Nothing ;
+assocm x (Cons (Pair y z) yzs) =
+  case (==) x y of { True -> Just z ; False -> assocm x yzs ; } ;
+
+subset Nil         ys = True ;
+subset (Cons x xs) ys =
+  case elem x ys of { True -> subset xs ys ; False -> False ; } ;
+
+union xs ys = foldr ins xs ys ;
+
+ins x ys = case elem x ys of { True -> ys ; False -> Cons x ys ; } ;
+
+histo xs = foldr histins Nil xs ;
+
+histins x Nil           = Cons (Pair x 1) Nil ;
+histins x (Cons yn yns) =
+  case yn of {
+  Pair y n -> case (==) x y of {
+              True -> Cons (Pair y ((+) n 1)) yns ;
+              False -> Cons yn (histins x yns) ;
+              } ;
+  } ;
+
+sorted lt = foldr (ordins lt) Nil ;
+
+ordins lt x Nil         = Cons x Nil ;
+ordins lt x (Cons y ys) = 
+  case lt x y of {
+  True  -> Cons x (Cons y ys) ;
+  False -> Cons y (ordins lt x ys) ;
+  } ;
+
+ends (K s a z n) = Cons a (Cons z Nil) ;
+
+firstLetter (K s a z n) = a ;
+
+lastLetter (K s a z n) = z ;
+
+freqSorted ks =
+  let { ft = freqTabOf ks ; } in
+  Pair (sorted (decreasingFrequencyIn ft) ks) (length ft) ;
+
+decreasingFrequencyIn ft (K s0 a x n0) (K s1 b y n1) =
+  let { freq = flip assoc ft ; } in
+  gt ((+) (freq a) (freq x)) ((+) (freq b) (freq y)) ;
+
+flip f x y = f y x ;
+
+freqTabOf ks = histo (concatMap ends ks) ;
+
+blocked = blockedWith Nil ;
+
+blockedWith ds Nil         = Nil ;
+blockedWith ds (Cons k ks) = 
+  let { dsk = union ds (ends k) ;
+        eks = endsSubset dsk ;
+        det = filter eks ks ;
+        rest = filter (non eks) ks ; } in
+  Cons k (append det (blockedWith dsk rest)) ;
+
+non f x = case f x of { True  -> False ; False -> True ; } ;
+
+endsSubset ds k = subset (ends k) ds ;
+
+enKey k = K k (head k) (last k) (length k) ;
+
+hashAssoc (Hash hs hf) = hf ;
+
+findhash mv ks = 
+  case hashes mv (length ks) ks (Hash (H Nothing Nothing Nil) Nil) of {
+  Cons (Hash s f) hs -> Just f ;
+  Nil                -> Nothing ;
+  } ;
+
+hashes maxval nk Nil         h = Cons h Nil ;
+hashes maxval nk (Cons k ks) h =               
+  concatMap (hashes maxval nk ks) (
+  concatMap (insertKey nk k) (
+  concatMap (assignUpto maxval (lastLetter k))
+            (assignUpto maxval (firstLetter k) h))) ;
+
+assignUpto maxval c h =
+  case assocm c (hashAssoc h) of {
+  Nothing -> map (assign c h) (enumFromTo 0 maxval) ;
+  Just v  -> Cons h Nil ;
+  } ;
+
+insertKey nk k (Hash hs hf) =
+  case hinsert nk (hash hf k) hs of {
+  Nothing    -> Nil ;
+  Just hsNew -> Cons (Hash hsNew hf) Nil ;
+  } ;
+
+assign c (Hash hs hf) v = Hash hs (Cons (Pair c v) hf) ;
+           
+hinsert nk h (H lo hi hs) =
+    let { newlo = case lo of { Nothing -> h ; Just x -> min x h } ;
+          newhi = case hi of { Nothing -> h ; Just x -> max x h } ;
+        } in
+    case elem h hs of {
+    True  -> Nothing ;
+    False -> case (<=) ((-) ((+) 1 newhi) newlo) nk of {
+             False -> Nothing ;
+             True  -> Just (H (Just newlo) (Just newhi) (Cons h hs)) ;
+             } ;
+    } ;
+
+hash hf (K s a z n) = (+) n ((+) (assoc a hf) (assoc z hf)) ; 
+
+cichelli ss = case freqSorted (map enKey ss) of {
+              Pair ks mv -> findhash mv (blocked ks) ;
+              } ;
+
+emitStr Nil k = k;
+emitStr (Cons x xs) k = emit x (emitStr xs k);
+
+main = case cichelli keywords of {
+       Just hf -> emitHashFun hf ;
+       Nothing -> emitStr "no solution" 0 ;
+       } ;
+
+emitHashFun Nil = 0 ;
+emitHashFun (Cons (Pair c n) hf) =
+  emit c (emit '=' (emitInt n (emit ' ' (emitHashFun hf)))) ;
+
+keywords =
+  Cons "as" (
+  Cons "case" (
+  Cons "class" (
+  Cons "data" (
+  Cons "default" (
+  Cons "deriving" (
+  Cons "do" (
+  Cons "else" (
+  Cons "hiding" (
+  Cons "if" (
+  Cons "import" (
+  Cons "in" (
+  Cons "infix" (
+  Cons "infixl" (
+  Cons "infixr" (
+  Cons "instance" (
+  Cons "let" (
+  Cons "module" (
+  Cons "newtype" (
+  Cons "of" (
+  Cons "qualified" (
+  Cons "then" (
+  Cons "type" (
+  Cons "where"
+  Nil ))))))))))))))))))))))) ;
+
+}
diff --git a/examples/Clausify.hs b/examples/Clausify.hs
new file mode 100644
--- /dev/null
+++ b/examples/Clausify.hs
@@ -0,0 +1,133 @@
+{
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+clauses ps = map (clause (Pair Nil Nil)) ps;
+
+clause (Pair c a) (Dis p q)     = clause (clause (Pair c a) p) q;
+clause (Pair c a) (Sym s)       = Pair (ins s c) a;
+clause (Pair c a) (Neg (Sym s)) = Pair c (ins s a);
+
+or False x = x;
+or True x = True;
+
+contains eq0 Nil y = False;
+contains eq0 (Cons x xs) y = or (eq0 x y) (contains eq0 xs y);
+
+disin (Sym s) = Sym s;
+disin (Neg p) = Neg p;
+disin (Con p q) = Con (disin p) (disin q);
+disin (Dis p q) = din (disin p) (disin q);
+
+din (Con p q) r = Con (din p r) (din q r);
+din (Dis p q) r = din2 (Dis p q) r;
+din (Neg p) r = din2 (Neg p) r;
+din (Sym s) r = din2 (Sym s) r;
+
+din2 p (Con q r) = Con (din p q) (din p r);
+din2 p (Dis q r) = Dis p (Dis q r);
+din2 p (Neg q) = Dis p (Neg q);
+din2 p (Sym s) = Dis p (Sym s);
+
+ins x Nil = Cons x Nil;
+ins x (Cons y ys) =
+  case (==) x y of {
+    True -> Cons y ys;
+    False -> case (<=) x y of {
+               True -> Cons x (Cons y ys);
+               False -> Cons y (ins x ys);
+             };
+  };
+
+filter p Nil = Nil;
+filter p (Cons x xs) = case p x of {
+                         True -> Cons x (filter p xs);
+                         False -> filter p xs;
+                       };
+
+inter eq0 xs ys = filter (contains eq0 xs) ys;
+
+negin (Neg (Con p q)) = Dis (negin (Neg p)) (negin (Neg q));
+negin (Neg (Dis p q)) = Con (negin (Neg p)) (negin (Neg q));
+negin (Neg (Neg p))   = negin p;
+negin (Neg (Sym s))   = Neg (Sym s);
+negin (Dis p q)       = Dis (negin p) (negin q);
+negin (Con p q)       = Con (negin p) (negin q);
+negin (Sym s)         = Sym s;
+
+nonTaut cs = filter notTaut cs;
+
+and False x = False;
+and True x = x;
+
+eqList f Nil Nil = True;
+eqList f Nil (Cons y ys) = False;
+eqList f (Cons x xs) Nil = False;
+eqList f (Cons x xs) (Cons y ys) = and (f x y) (eqList f xs ys);
+
+eq a b = (==) a b;
+
+eqClause (Pair a b) (Pair c d) = and (eqList eq a c) (eqList eq b d);
+
+null Nil = True;
+null (Cons x xs) = False;
+
+notTaut (Pair c a) = null (inter eq c a);
+
+clausify p = uniq
+           ( nonTaut
+           ( clauses
+           ( split
+           ( disin
+           ( negin p )))));
+
+split p = spl Nil p;
+
+spl a (Con p q) = spl (spl a p) q;
+spl a (Dis p q) = Cons (Dis p q) a;
+spl a (Neg p) = Cons (Neg p) a;
+spl a (Sym s) = Cons (Sym s) a;
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+comp f g x = f (g x);
+
+not False = True;
+not True = False;
+
+union eq0 xs ys = append xs (filter (comp not (contains eq0 xs)) ys);
+
+singleton x = Cons x Nil;
+
+foldr f z Nil = z;
+foldr f z (Cons x xs) = f x (foldr f z xs);
+
+uniq xs = foldr (comp (union eqClause) singleton) Nil xs;
+
+display Nil = 0;
+display (Cons c cs) = (+) (emitClause c) (display cs);
+
+emitClause (Pair c a) = (+) (sum c) (sum a);
+
+sum xs = sumAcc 0 xs;
+
+sumAcc acc Nil = acc;
+sumAcc acc (Cons x xs) = sumAcc ((+) acc x) xs;
+
+eqv a b = Con (Dis (Neg a) b) (Dis (Neg b) a);
+
+replicate n a = case (==) n 0 of {
+                  True -> Nil;
+                  False -> Cons a (replicate ((-) n 1) a);
+                };
+
+main = let { p = eqv (eqv a (eqv a a))
+                             (eqv (eqv a (eqv a a))
+                                  (eqv a (eqv a a)))
+           ; a = Sym 0
+           } in display (clausify (foldr Con a (replicate 20 p)));
+
+}
+
diff --git a/examples/Countdown.hs b/examples/Countdown.hs
new file mode 100644
--- /dev/null
+++ b/examples/Countdown.hs
@@ -0,0 +1,115 @@
+{
+
+valid Add x y  =  True ;
+valid Sub x y  =  not ((<=) x y) ;
+valid Mul x y  =  True ;
+valid Div x y  =  (==) (mod x y) 0 ;
+
+apply Add x y  =  (+) x y ;
+apply Sub x y  =  (-) x y ;
+apply Mul x y  =  mul x y ;
+apply Div x y  =  div x y ;
+
+subs Nil         =  Cons Nil Nil ;
+subs (Cons x xs) =  let { yss = subs xs } in append yss (map (Cons x) yss) ;
+                                 
+interleave x Nil         =  Cons (Cons x Nil) Nil ;
+interleave x (Cons y ys) =  Cons (Cons x (Cons y ys))
+                                 (map (Cons y) (interleave x ys)) ;
+
+perms Nil         =  Cons Nil Nil ;
+perms (Cons x xs) =  concatMap (interleave x) (perms xs) ;
+
+choices xs  =  concatMap perms (subs xs) ;
+
+ops  =  Cons Add (Cons Sub (Cons Mul (Cons Div Nil))) ;
+
+split (Cons x xs)  =  case null xs of {
+                      True  -> Nil ;
+                      False -> Cons (Pair (Cons x Nil) xs)
+                                    (map (cross (Pair (Cons x) id)) (split xs)) ;
+                      } ;
+
+results Nil         =  Nil ;
+results (Cons n ns) =  case null ns of {
+                       True  -> Cons (Pair (Val n) n) Nil ;
+                       False -> concatMap combinedResults (split (Cons n ns)) ;
+                       } ;
+
+combinedResults (Pair ls rs)  = concatProdWith combine (results ls) (results rs) ;
+
+concatProdWith f Nil         ys = Nil ;
+concatProdWith f (Cons x xs) ys = append (concatMap (f x) ys) (concatProdWith f xs ys) ;
+
+combine (Pair l x) (Pair r y) =  concatMap (combi l x r y) ops ;
+ 
+combi l x r y o = case valid o x y of {
+                  True  -> Cons (Pair (App o l r) (apply o x y)) Nil ;
+                  False -> Nil ;
+                  } ; 
+
+solutions ns n = concatMap (solns n) (choices ns) ;
+
+solns n ns = let { ems = results ns } in preImage n (results ns) ;
+
+preImage n Nil                   = Nil ;
+preImage n (Cons (Pair e m) ems) = case (==) m n of {
+                                   True  -> Cons e (preImage n ems) ;
+                                   False -> preImage n ems ;
+                                   } ;
+
+not True   =  False ;
+not False  =  True ;
+
+div x y = case divMod x y of { Pair d m -> d ; } ;
+
+mod x y = case divMod x y of { Pair d m -> m ; } ;
+
+divMod x y = let { y2 = (+) y y } in
+             case (<=) y2 x of {
+             True  -> case divMod x y2 of {
+                      Pair d2 m2 -> case (<=) y m2 of {
+                                    True  -> Pair ((+) 1 ((+) d2 d2)) ((-) m2 y) ;
+                                    False -> Pair ((+) d2 d2) m2 ;
+                                    } ;
+                      } ;
+             False -> case (<=) y x of {
+                      True  -> Pair 1 ((-) x y) ;
+                      False -> Pair 0 x ;
+                      } ;
+             } ;
+
+mul x n = case (==) n 1 of {
+          True  -> x ;
+          False -> case divMod n 2 of {
+                   Pair d m -> (+) (mul ((+) x x) d)
+                                   (case (==) m 0 of {True -> 0; False -> x;}) ;
+                   } ;
+          } ;
+
+cross (Pair f g) (Pair x y) = Pair (f x) (g y) ;
+
+id x = x ;
+
+null Nil         = True ;
+null (Cons x xs) = False ;
+
+length Nil         = 0 ;
+length (Cons x xs) = (+) 1 (length xs) ;
+
+append Nil         ys = ys ;
+append (Cons x xs) ys = Cons x (append xs ys) ;
+
+map f Nil         = Nil ;
+map f (Cons x xs) = Cons (f x) (map f xs) ;
+
+concatMap f Nil         = Nil ;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs) ;
+
+givens = Cons 1 (Cons 3 (Cons 7 (Cons 10 (Cons 25 (Cons 50 Nil))))) ;
+
+target = 765 ;
+
+main = emitInt (length (solutions givens target)) 0 ;
+
+}
diff --git a/examples/Fib.hs b/examples/Fib.hs
new file mode 100644
--- /dev/null
+++ b/examples/Fib.hs
@@ -0,0 +1,10 @@
+{
+
+fib n = if (<=) n 1 then 1 else (+) (fib ((-) n 2)) (fib ((-) n 1));
+
+emitStr Nil k = k;
+emitStr (Cons x xs) k = emit x (emitStr xs k);
+
+main = emitStr "fib(10) = " (emitInt (fib 10) (emit '\n' 0));
+
+}
diff --git a/examples/MSS.hs b/examples/MSS.hs
new file mode 100644
--- /dev/null
+++ b/examples/MSS.hs
@@ -0,0 +1,42 @@
+{
+
+init (Cons x Nil) = Nil;
+init (Cons x (Cons y ys)) = Cons x (init (Cons y ys));
+
+inits xs = case xs of {
+             Nil -> Cons Nil Nil;
+             Cons y ys -> Cons xs (inits (init xs));
+           };
+
+tails Nil = Nil;
+tails (Cons x xs) = Cons (Cons x xs) (tails xs);
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+concatMap f Nil = Nil;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs);
+
+segments xs = concatMap tails (inits xs);
+
+maximum (Cons x xs) = max x xs;
+
+max m Nil = m;
+max m (Cons x xs) = case (<=) m x of { True -> max x xs ; False -> max m xs };
+
+sum Nil = 0;
+sum (Cons x xs) = (+) x (sum xs);
+
+mss xs = maximum (map sum (segments xs));
+
+fromTo n m = case (<=) n m of {
+               True -> Cons n (fromTo ((+) n 1) m);
+               False -> Nil;
+             };
+
+main = emitInt (mss (fromTo ((-) 0 150) 150)) 0;
+
+}
diff --git a/examples/Mate.hs b/examples/Mate.hs
new file mode 100644
--- /dev/null
+++ b/examples/Mate.hs
@@ -0,0 +1,393 @@
+{
+
+id x = x ;
+
+const c x = c ;
+
+inc n = (+) n 1 ;
+
+dec n = (-) n 1 ;
+
+min x y = case (<=) x y of { True -> x ; False -> y ; } ;
+
+max x y = case (<=) x y of { True -> y ; False -> x ; } ;
+
+abs n = case (<=) 0 n of { True  -> n ; False -> (-) 0 n ; } ;
+
+plus a b = (+) a b;
+
+minus a b = (-) a b;
+
+no Nothing = True ;
+no (Just x) = False ;
+
+maybe n j Nothing  = n ;
+maybe n j (Just x) = j x ; 
+
+con True  q = q ;
+con False q = False ;
+
+dis True  q = True ;
+dis False q = q ;
+
+fst (Pair x y) = x ;
+
+snd (Pair x y) = y ;
+
+cross (Pair f g) (Pair x y) = Pair (f x) (g y) ;
+
+null Nil         = True ;
+null (Cons x xs) = False ;
+
+append Nil         ys = ys ;
+append (Cons x xs) ys = Cons x (append xs ys) ;
+
+elemAt (Cons x xs) n =
+  case (==) n 0 of { True -> x ; False -> elemAt xs ((-) n 1) ; } ;
+
+map f Nil = Nil ;
+map f (Cons x xs) = Cons (f x) (map f xs) ;
+
+concatMap f Nil = Nil ;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs) ;
+
+any p Nil         = False ;
+any p (Cons x xs) = dis (p x) (any p xs) ;
+
+foldr f z Nil         = z ;
+foldr f z (Cons x xs) = f x (foldr f z xs) ;
+
+sum xs = foldr plus 0 xs ;
+
+unzip Nil                   = Pair Nil Nil ;
+unzip (Cons (Pair x y) xys) =
+  let { u = unzip xys ; } in  Pair (Cons x (fst u)) (Cons y (snd u)) ;
+
+kindToChar k =
+	case k of {
+	King	  -> 'K' ;
+	Queen	  -> 'Q' ;
+	Rook	  -> 'R' ;
+	Bishop	-> 'B' ;
+	Knight	-> 'N' ;
+	Pawn	  -> 'P' ;
+  } ;
+
+isKing k = (==) (kindToChar k) 'K' ;
+
+pieceAt (Board wkss bkss) sq =
+  pieceAtWith sq White (pieceAtWith sq Black Nothing bkss) wkss ;
+
+pieceAtWith sq c n Nil = n ;
+pieceAtWith sq c n (Cons (Pair k s) xs) =
+  case sameSquare s sq of {
+  True -> Just (Pair c k) ;
+  False -> pieceAtWith sq c n xs ;
+  } ;
+
+emptyAtAll (Board wkss bkss) e =
+	emptyAtAllAnd e (emptyAtAllAnd e True bkss) wkss ;
+
+emptyAtAllAnd e b Nil                  = b ;
+emptyAtAllAnd e b (Cons (Pair k s) xs) =
+  case e s of { True -> False ; False -> emptyAtAllAnd e b xs ; } ;
+
+rmPieceAt White sq (Board wkss bkss) = Board (rPa sq wkss) bkss ;
+rmPieceAt Black sq (Board wkss bkss) = Board wkss (rPa sq bkss) ;
+
+rPa sq (Cons ks kss) = 
+  case ks of {
+  Pair k s ->
+    case sameSquare s sq of { True -> kss ; False -> Cons ks (rPa sq kss) ; } ;
+  } ;
+
+putPieceAt sq (Pair c k) (Board wkss bkss) =
+  case c of {
+  White -> Board (Cons (Pair k sq) wkss) bkss ;
+  Black -> Board wkss (Cons (Pair k sq) bkss) ;
+  } ;
+
+kingSquare c b = kSq (forcesColoured c b) ;
+
+kSq (Cons (Pair k s) kss) =
+  case isKing k of { True  -> s ; False -> kSq kss ; } ;
+
+opponent Black = White ;
+opponent White = Black ;
+
+colourOf (Pair c k) = c ;
+kindOf   (Pair c k) = k ;
+
+sameColour White White = True ;
+sameColour White Black = False ;
+sameColour Black White = False ;
+sameColour Black Black = True ;
+
+rank (Pair f r) = r ;
+file (Pair f r) = f ;
+
+sameSquare (Pair f1 r1) (Pair f2 r2) = con ((==) f1 f2) ((==) r1 r2) ;
+
+onboard (Pair p q) =
+  con (con ((<=) 1 p) ((<=) p 8))
+      (con ((<=) 1 q) ((<=) q 8)) ;
+
+forcesColoured White (Board wkss bkss) = wkss ;
+forcesColoured Black (Board wkss bkss) = bkss ;
+
+problem =
+  Pair
+    ( Board
+      (Cons (Pair Knight (Pair 7 8))
+      (Cons (Pair Rook   (Pair 5 7))
+      (Cons (Pair King   (Pair 8 7))
+      (Cons (Pair Bishop (Pair 4 5))
+      (Cons (Pair Pawn   (Pair 8 4))
+      (Cons (Pair Pawn   (Pair 7 3))
+      (Cons (Pair Pawn   (Pair 5 2))
+      (Cons (Pair Pawn   (Pair 6 2))
+      (Cons (Pair Queen  (Pair 5 1))
+      Nil)))))))))
+      (Cons (Pair Knight (Pair 2 8))
+      (Cons (Pair Pawn   (Pair 7 7))
+      (Cons (Pair Pawn   (Pair 4 6))
+      (Cons (Pair Pawn   (Pair 3 5))
+      (Cons (Pair King   (Pair 6 5))
+      (Cons (Pair Pawn   (Pair 8 5))
+      (Cons (Pair Pawn   (Pair 4 4))
+      (Cons (Pair Pawn   (Pair 2 3))
+      (Cons (Pair Pawn   (Pair 5 3))
+      (Cons (Pair Pawn   (Pair 7 2))
+      (Cons (Pair Queen  (Pair 1 1))
+      (Cons (Pair Knight (Pair 2 1))
+      (Cons (Pair Bishop (Pair 8 1))
+      Nil)))))))))))))
+    )
+    (Pair White 3) ;
+
+moveDetailsFor c bd =
+  concatMap (movesForPiece c bd) (forcesColoured c bd) ;
+
+movesForPiece c bd p =
+  concatMap (tryMove c bd p) (rawmoves c p bd) ;
+
+tryMove c bd (Pair k sqFrom) (Move sqTo mcp mpp) =
+	let { p   = Pair c k ;
+        bd1 =	rmPieceAt c sqFrom bd ;
+        pp  =	maybe p id mpp ;
+        bd2 =	maybe (putPieceAt sqTo pp bd1)
+		                (const (putPieceAt sqTo pp
+                             (rmPieceAt (opponent c) sqTo bd1)))
+		                mcp ; }
+ 	in case kingincheck c bd2 of {
+     False -> Cons (Pair (MoveInFull p sqFrom (Move sqTo mcp mpp)) bd2) Nil ;
+	   True  -> Nil ;
+     } ;
+
+rawmoves c (Pair k sq) bd = 
+	let { m = case k of {
+	          King   -> kingmoves   ;
+	          Queen  -> queenmoves  ;
+	          Rook   -> rookmoves   ;
+	          Bishop -> bishopmoves ;
+	          Knight -> knightmoves ;
+	          Pawn   -> pawnmoves   ;
+            } ; }
+  in m c sq bd ;
+
+bishopmoves c sq bd =
+	append (moveLine bd c sq (cross (Pair dec inc))) (
+	append (moveLine bd c sq (cross (Pair inc inc))) (
+	append (moveLine bd c sq (cross (Pair dec dec)))
+	       (moveLine bd c sq (cross (Pair inc dec))) )) ;
+
+rookmoves c sq bd =
+	append (moveLine bd c sq (cross (Pair dec id))) (
+	append (moveLine bd c sq (cross (Pair inc id))) (
+	append (moveLine bd c sq (cross (Pair id dec))) 
+	       (moveLine bd c sq (cross (Pair id inc))) )) ;
+
+moveLine bd c sq inc = 
+	let { incsq = inc sq ; } in
+	case onboard incsq of {
+  True -> case pieceAt bd incsq of {
+		      Nothing -> Cons (Move incsq Nothing Nothing)
+                          (moveLine bd c incsq inc) ;
+		      Just p  -> case sameColour (colourOf p) c of {
+				             False -> Cons (Move incsq (Just p) Nothing) Nil ;
+                     True  -> Nil ;
+                     } ;
+          } ;
+	False -> Nil ;
+  } ;
+
+kingmoves c (Pair p q) bd =
+  let { pi = (+) p 1 ; pd = (-) p 1 ; qi = (+) q 1 ; qd = (-) q 1 ; }
+	in sift c bd Nil
+       (Cons (Pair pd qi) (Cons (Pair p qi) (Cons (Pair pi qi)
+       (Cons (Pair pd q )                   (Cons (Pair pi q )
+       (Cons (Pair pd qd) (Cons (Pair p qd) (Cons (Pair pi qd)
+       Nil)))))))) ;
+
+knightmoves c (Pair p q) bd =
+  let {pi  = (+) p 1 ; pd  = (-) p 1 ; qi  = (+) q 1 ; qd  = (-) q 1 ;
+       pi2 = (+) p 2 ; pd2 = (-) p 2 ; qi2 = (+) q 2 ; qd2 = (-) q 2 ; }
+	in sift c bd Nil
+                 (Cons (Pair pd qi2) (Cons (Pair pi qi2)
+       (Cons (Pair pd2 qi)                     (Cons (Pair pi2 qi)
+       (Cons (Pair pd2 qd)                     (Cons (Pair pi2 qd)
+                 (Cons (Pair pd qd2) (Cons (Pair pi qd2)
+       Nil)))))))) ;
+
+sift c bd ms Nil           = ms ;
+sift c bd ms (Cons sq sqs) =
+	case onboard sq of {
+	False -> sift c bd ms sqs ;
+  True  ->
+    case pieceAt bd sq of {
+    Nothing -> sift c bd (Cons (Move sq Nothing Nothing) ms) sqs ;
+    Just p  -> case sameColour (colourOf p) c of {
+               True  -> sift c bd ms sqs ;
+               False -> sift c bd (Cons (Move sq (Just p) Nothing) ms) sqs ;
+               } ;
+    } ;
+  } ;
+
+pawnmoves c (Pair p q) bd =
+  let { fwd  = case c of {	White -> 1 ; Black -> (-) 0 1 ; } ; 
+        on1  = Pair p ((+) q fwd) ;
+        on2  = Pair p ((+) ((+) q fwd) fwd) ;
+        mov2 = case con (secondRank c q) (no (pieceAt bd on2)) of {
+               True -> Cons (Move on2 Nothing Nothing) Nil ; 
+      			   False -> Nil ;
+               } ;
+      	movs = case no (pieceAt bd on1) of {
+               True ->
+            		 append
+                   (promote c on1 Nothing)
+        			     mov2 ;
+            	 False -> 
+                 Nil ;
+               } ;
+        dii  = Pair ((+) p 1) ((+) q fwd) ;
+        did  = Pair ((-) p 1) ((+) q fwd) ;
+        caps = append (promoteCap c dii bd) (promoteCap c did bd) ; }
+  in append movs caps ;
+
+promoteCap c sq bd =
+  let { mcp = pieceAt bd sq ; } in
+  case mcp of {
+  Nothing  -> Nil;
+  Just p   -> case sameColour (colourOf p) c of {
+              False -> promote c sq mcp ;
+              True  -> Nil ;
+              } ;
+  } ;
+
+promote c sq mcp =  
+	case lastRank c (rank sq) of {
+  True  -> map (Move sq mcp)
+		       (Cons (Just (Pair c Queen))
+           (Cons (Just (Pair c Rook))
+           (Cons (Just (Pair c Bishop))
+           (Cons (Just (Pair c Knight)) Nil)))) ;
+	False -> Cons (Move sq mcp Nothing) Nil ;
+  } ;
+
+secondRank White r = (==) r 2 ;
+secondRank Black r = (==) r 7 ;
+
+lastRank White r = (==) r 8 ;
+lastRank Black r = (==) r 1 ;
+
+queenmoves c sq bd = append (bishopmoves c sq bd) (rookmoves c sq bd) ;
+
+kingincheck c bd =
+	any (kingInCheckFrom c bd) (forcesColoured (opponent c) bd) ;
+
+kingInCheckFrom c bd (Pair f (Pair x y)) =
+  case kingSquare c bd of {
+  Pair xk yk -> 
+    case f of {
+		King   -> con ((<=) (abs ((-) x xk)) 1)
+                  ((<=) (abs ((-) y yk)) 1) ;
+		Queen  -> dis (kingInCheckFrom c bd (Pair Rook   (Pair x y)))
+                  (kingInCheckFrom c bd (Pair Bishop (Pair x y))) ;
+		Rook   -> dis (con ((==) x xk)
+                       (emptyAtAll bd (filePath xk y yk)))
+                  (con ((==) y yk)
+                       (emptyAtAll bd (rankPath yk x xk))) ;
+		Bishop -> dis (con ((==) ((-) x y) ((-) xk yk))
+                       (emptyAtAll bd (diagPath minus ((-) xk yk) x xk)))
+                  (con ((==) ((+) x y) ((+) xk yk))
+                       (emptyAtAll bd (diagPath plus ((+) xk yk) x xk))) ;
+		Knight -> dis (con ((==) (abs ((-) x xk)) 2) ((==) (abs ((-) y yk)) 1))
+                  (con ((==) (abs ((-) x xk)) 1) ((==) (abs ((-) y yk)) 2)) ;
+		Pawn   -> con ((==) (abs ((-) x xk)) 1)
+			            ((==) yk (onFor c y )) ;
+    } ;
+  } ;
+
+onFor Black = inc ;
+onFor White = dec ;
+
+filePath xk yFrom yTo (Pair x y) =
+  let { ylo = (+) (min yFrom yTo) 1 ; yhi = (-) (max yFrom yTo) 1 ; }
+  in  con ((==) x xk) (con ((<=) ylo y) ((<=) y yhi)) ; 
+
+rankPath yk xFrom xTo (Pair x y) =
+  let { xlo = (+) (min xFrom xTo) 1 ; xhi = (-) (max xFrom xTo) 1 ; }
+  in  con ((==) y yk) (con ((<=) xlo x) ((<=) x xhi)) ; 
+
+diagPath op d xFrom xTo (Pair x y) =
+  let { xlo = (+) (min xFrom xTo) 1 ; xhi = (-) (max xFrom xTo) 1 ; }
+  in  con ((==) (op x y) d) (con ((<=) xlo x) ((<=) x xhi)) ; 
+
+solve bd c n = showResult (solution bd c ((-) ((+) n n) 1)) ;
+
+solution bd c n  = 
+  let { mds = moveDetailsFor c bd ; } in
+	foldr (solnOr c n) Nothing mds ;
+
+solnOr c n (Pair mif b) other =
+	case replies b (opponent c) ((-) n 1) of {
+	Nothing -> other ;
+	Just rs -> case null rs of {
+             True -> case kingincheck (opponent c) b of {
+                     True  -> Just (Solution mif Nil) ;
+		                 False -> other ;
+                     } ;
+             False -> Just (Solution mif rs) ;
+             } ;
+  } ;
+
+replies bd c n =
+  let { mds = moveDetailsFor c bd ; } in
+  case (==) n 0 of {
+  True  -> case null mds of { True -> Just Nil ; False -> Nothing ; } ;
+	False -> foldr (solnAnd c n) (Just Nil) mds ;
+  } ;
+
+solnAnd c n (Pair mif b) rest =
+	case solution b (opponent c) ((-) n 1) of {
+	Nothing -> Nothing ;
+	Just s  -> case rest of {
+			       Nothing -> Nothing ;
+			       Just ms -> Just (Cons (Pair mif s) ms) ;
+             } ;
+  } ;
+
+emitStr Nil k = k;
+emitStr (Cons x xs) k = emit x (emitStr xs k);
+
+showResult Nothing  = emitStr "No solution!\n" 0 ;
+showResult (Just s) = emitStr "Solved!  Solution size = "
+                             (emitInt (size s) (emit '\n' 0)) ;
+
+size (Solution mif rs) = (+) 1 (sum (map size (snd (unzip rs)))) ;
+
+main = solveProblem problem ;
+
+solveProblem (Pair bd (Pair c n)) = solve bd c n ;
+
+}
diff --git a/examples/OrdList.hs b/examples/OrdList.hs
new file mode 100644
--- /dev/null
+++ b/examples/OrdList.hs
@@ -0,0 +1,46 @@
+{
+
+implies False x = True;
+implies True x = x;
+
+and False x = False;
+and True x = x;
+
+andList Nil = True;
+andList (Cons x xs) = and x (andList xs);
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+ord Nil = True;
+ord (Cons x Nil) = True;
+ord (Cons x (Cons y ys)) = and (implies x y) (ord (Cons y ys));
+
+insert x Nil = Cons x Nil;
+insert x (Cons y ys) =
+  case implies x y of {
+    True -> Cons x (Cons y ys);
+    False -> Cons y (insert x ys);
+  };
+
+prop x xs = implies (ord xs) (ord (insert x xs));
+
+boolList Z = Cons Nil Nil;
+boolList (S n) =
+  append (boolList n)
+         (append (map (Cons False) (boolList n))
+                 (map (Cons True) (boolList n)));
+
+top n = andList (append (map (prop True) (boolList n))
+                        (map (prop False) (boolList n)));
+
+main = let { eleven = S (S (S (S (S (S (S (S (S (S (S Z)))))))))) } in
+         case top eleven of {
+           False -> emitInt 0 0;
+           True  -> emitInt 1 0;
+         };
+
+}
diff --git a/examples/Parts.hs b/examples/Parts.hs
new file mode 100644
--- /dev/null
+++ b/examples/Parts.hs
@@ -0,0 +1,54 @@
+{
+
+p n = length (partitions n) ;
+
+partitions n = partitionsWith n (countDown n) ;
+ 
+partitionsWith n ns = case (==) n 0 of {
+                        True  -> Cons Nil Nil ;
+                        False -> concatMap (partitionsWith0 n ns) ns ;
+                      } ;
+
+and False x = False;
+and True x = x;
+
+lt n m = and ((/=) n m) ((<=) n m);
+
+partitionsWith0 n ns i =
+  let { n0 = (-) n i ; m  = min i n0 } in
+    map (Cons i) (partitionsWith n0 (dropWhile (lt m) ns)) ;
+
+length Nil = 0 ;
+length (Cons x xs) = (+) 1 (length xs) ;
+
+countDown n = case (<=) 1 n of {
+                True  -> Cons n (countDown ((-) n 1)) ;
+                False -> Nil ;
+              };
+
+concatMap f Nil = Nil ;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs) ;
+
+append Nil         ys = ys ;
+append (Cons x xs) ys = Cons x (append xs ys) ;
+
+min m n = case (<=) m n of {
+            True  -> m ;
+            False -> n ;
+          };
+
+map f Nil = Nil ;
+map f (Cons x xs) = Cons (f x) (map f xs) ;
+
+dropWhile p xs = case xs of {
+                   Nil        -> Nil ;
+                   Cons x xs0 -> case p x of {
+                                   True  -> dropWhile p xs0 ;
+                                   False -> xs ;
+                                 };
+                 } ;
+
+main = emitInt (p 20) 0;
+
+}
+
diff --git a/examples/PermSort.hs b/examples/PermSort.hs
new file mode 100644
--- /dev/null
+++ b/examples/PermSort.hs
@@ -0,0 +1,42 @@
+{
+
+and False x = False;
+and True x = x;
+
+head (Cons x xs) = x;
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+concatMap f Nil = Nil;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs);
+
+filter p Nil = Nil;
+filter p (Cons x xs) = case p x of {
+                         True -> Cons x (filter p xs);
+                         False -> filter p xs;
+                       };
+
+place x Nil = Cons (Cons x Nil) Nil;
+place x (Cons y ys) = Cons (Cons x (Cons y ys)) (map (Cons y) (place x ys));
+
+perm Nil = Cons Nil Nil;
+perm (Cons x xs) = concatMap (place x) (perm xs);
+
+ord Nil = True;
+ord (Cons x Nil) = True;
+ord (Cons x (Cons y ys)) = and ((<=) x y) (ord (Cons y ys));
+
+permSort xs = head (filter ord (perm xs));
+
+emitList Nil k = emit '\n' k;
+emitList (Cons x xs) k = emitInt x (emit ' ' (emitList xs k));
+
+main = emitList (permSort (Cons 9 (Cons 8 (Cons 7 (
+                          (Cons 6 (Cons 5 (Cons 4 (
+                          (Cons 3 (Cons 2 (Cons 1 Nil)))))))))))) 0;
+
+}
diff --git a/examples/Queens.hs b/examples/Queens.hs
new file mode 100644
--- /dev/null
+++ b/examples/Queens.hs
@@ -0,0 +1,47 @@
+{
+
+and False a = False;
+and True a = a;
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+concatMap f Nil = Nil;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs);
+
+length Nil = 0;
+length (Cons x xs) = (+) 1 (length xs);
+
+nsoln nq = length (gen nq nq);
+
+gen nq n =
+  case (==) n 0 of {
+    True -> Cons Nil Nil;
+    False -> concatMap (gen1 nq) (gen nq ((-) n 1));
+  };
+
+gen1 nq b = concatMap (gen2 b) (toOne nq);
+
+gen2 b q = case safe q 1 b of {
+             True -> Cons (Cons q b) Nil;
+             False -> Nil;
+           };
+
+safe x d Nil = True;
+safe x d (Cons q l) =
+  and ((/=) x q) (
+  and ((/=) x ((+) q d)) (
+  and ((/=) x ((-) q d)) (
+  safe x ((+) d 1) l)));       
+
+toOne n = case (==) n 1 of {
+            True -> Cons 1 Nil;
+            False -> Cons n (toOne ((-) n 1));
+          };
+
+main = emitInt (nsoln 10) 0;
+
+}
diff --git a/examples/Queens2.hs b/examples/Queens2.hs
new file mode 100644
--- /dev/null
+++ b/examples/Queens2.hs
@@ -0,0 +1,60 @@
+{
+
+tail (Cons x xs) = xs;
+
+one p Nil = Nil;
+one p (Cons x xs) = case p x of { True -> Cons x Nil ; False -> one p xs };
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+concatMap f Nil = Nil;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs);
+
+length Nil = 0;
+length (Cons x xs) = (+) 1 (length xs);
+
+replicate n x =
+  case (==) n 0 of {
+    True -> Nil;
+    False -> Cons x (replicate ((-) n 1) x);
+  };
+
+l = 0;
+r = 1;
+d = 2;
+
+eq x y = (==) x y;
+
+left  xs = map (one (eq l)) (tail xs);
+right xs = Cons Nil (map (one (eq r)) xs);
+down  xs = map (one (eq d)) xs;
+
+merge Nil ys = Nil;
+merge (Cons x xs) Nil = Cons x xs;
+merge (Cons x xs) (Cons y ys) = Cons (append x y) (merge xs ys);
+
+next mask = merge (merge (down mask) (left mask)) (right mask);
+
+fill Nil = Nil;
+fill (Cons x xs) = append (lrd x xs) (map (Cons x) (fill xs));
+
+lrd Nil ys = Cons (Cons (Cons l (Cons r (Cons d Nil))) ys) Nil;
+lrd (Cons x xs) ys = Nil;
+
+solve n mask =
+  case (==) n 0 of {
+    True -> Cons Nil Nil;
+    False -> concatMap (sol ((-) n 1)) (fill mask);
+  };
+
+sol n row = map (Cons row) (solve n (next row));
+
+nqueens n = length (solve n (replicate n Nil));
+
+main = emitInt (nqueens 10) 0;
+
+}
diff --git a/examples/Sudoku.hs b/examples/Sudoku.hs
new file mode 100644
--- /dev/null
+++ b/examples/Sudoku.hs
@@ -0,0 +1,209 @@
+{
+
+del x Nil = Nil;
+del x (Cons y ys) =
+  case (==) x y of { True -> ys ; False -> Cons y (del x ys) };
+
+diff xs Nil = xs;
+diff xs (Cons y ys) = diff (del y xs) ys;
+
+head (Cons x xs) = x;
+tail (Cons x xs) = xs;
+
+length Nil = 0;
+length (Cons x xs) = (+) 1 (length xs);
+
+sum Nil = 0;
+sum (Cons x xs) = (+) x (sum xs);
+
+null Nil = True;
+null (Cons x xs) = False;
+
+single Nil = False;
+single (Cons x xs) = null xs;
+
+minimum (Cons x xs) = min x xs;
+
+min m Nil = m;
+min m (Cons x xs) = case (<=) x m of { True -> min x xs ; False -> min m xs };
+
+break p Nil = Pair Nil Nil;
+break p (Cons x xs) =
+  case p x of {
+    True -> Pair Nil (Cons x xs);
+    False -> case break p xs of { Pair ys zs -> Pair (Cons x ys) zs };
+  };
+
+filter p Nil = Nil;
+filter p (Cons x xs) =
+  case p x of {
+    True -> Cons x (filter p xs);
+    False -> filter p xs;
+  };
+
+zipWith f Nil ys = Nil;
+zipWith f (Cons x xs) Nil = Nil;
+zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys);
+
+notElem x Nil = True;
+notElem x (Cons y ys) = and ((/=) x y) (notElem x ys);
+
+and False x = False;
+and True x = x;
+
+not False = True;
+not True = False;
+
+or False x = x;
+or True x = True;
+
+any p Nil = False;
+any p (Cons x xs) = or (p x) (any p xs);
+
+all p Nil = True;
+all p (Cons x xs) = and (p x) (all p xs);
+
+map f Nil = Nil;
+map f (Cons x xs) = Cons (f x) (map f xs);
+
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys);
+
+concat Nil = Nil;
+concat (Cons xs xss) = append xs (concat xss);
+
+concatMap f Nil = Nil;
+concatMap f (Cons x xs) = append (f x) (concatMap f xs);
+
+take n Nil = Nil;
+take n (Cons x xs) =
+  case (==) n 0 of {
+    True -> Nil;
+    False -> Cons x (take ((-) n 1) xs);
+  };
+
+drop n Nil = Nil;
+drop n (Cons x xs) =
+  case (==) n 0 of {
+    True -> Cons x xs;
+    False -> drop ((-) n 1) xs;
+  };
+
+groupBy n xs =
+  case null xs of {
+    True -> Nil;
+    False -> Cons (take n xs) (groupBy n (drop n xs));
+  };
+
+id x = x;
+
+comp f g x = f (g x);
+
+boardsize = 9;
+boxsize   = 3;
+cellvals  = Cons 1 (Cons 2 (Cons 3 (
+            Cons 4 (Cons 5 (Cons 6 (
+            Cons 7 (Cons 8 (Cons 9 Nil))))))));
+
+blank x = (==) x 0;
+
+nodups Nil = True;
+nodups (Cons x xs) = and (notElem x xs) (nodups xs);
+
+singleton x = Cons x Nil;
+
+cols (Cons xs Nil) = map singleton xs;
+cols (Cons xs (Cons ys yss)) = zipWith Cons xs (cols (Cons ys yss));
+
+boxs m = map concat (concatMap cols (groupBy 3 (map (groupBy 3) m)));
+
+choices b = map (map choose) b;
+
+choose e = case blank e of { True -> cellvals ; False -> Cons e Nil };
+
+fixed css = concat (filter single css);
+
+reduce css = map (remove (fixed css)) css;
+
+remove fs cs = case single cs of { True -> cs ; False -> diff cs fs };
+
+prune m = pruneBy boxs (pruneBy cols (pruneBy id m));
+
+pruneBy f m = f (map reduce (f m));
+
+blocked cm = or (void cm) (not (safe cm));
+
+void m = any (any null) m;
+
+safe cm = and (all (comp nodups fixed) cm)
+              (and (all (comp nodups fixed) (cols cm))
+                   (all (comp nodups fixed) (boxs cm)));
+
+best n cs = (==) (length cs) n;
+
+expand cm =
+  let { n = minchoice cm } in
+    case break (any (best n)) cm of {
+      Pair rows1 rows2 ->
+        case break (best n) (head rows2) of {
+          Pair row1 row2 -> map (exp row1 row2 rows1 rows2) (head row2);
+        };
+    };
+
+exp row1 row2 rows1 rows2 c =
+  append rows1 (append (Cons (append row1 (Cons (Cons c Nil)
+                             (tail row2))) Nil)
+                       (tail rows2));
+
+minchoice m = minimum (filter gte2 (concatMap (map length) m));
+
+gte2 x = (<=) 2 x;
+
+search cm =
+  case blocked cm of {
+    True -> Nil;
+    False -> case all (all single) cm of {
+               True -> Cons cm Nil;
+               False -> concatMap (comp search prune) (expand cm);
+             };
+  };
+
+sudoku b = map (map (map head)) (search (prune (choices b)));
+
+emitRow Nil k = emit '\n' k;
+emitRow (Cons x xs) k = emitInt x (emit ' ' (emitRow xs k));
+
+emitMatrix Nil k = k;
+emitMatrix (Cons x xs) k = emitRow x (emitMatrix xs k);
+
+main = emitMatrix (head (
+       sudoku (Cons (Cons 0 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 3
+                    (Cons 0 (Cons 6 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 1 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 9 (Cons 7
+                    (Cons 5 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 8 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 9 (Cons 0
+                    (Cons 2 (Cons 0 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 0 (Cons 8
+                    (Cons 0 (Cons 7 (Cons 0
+                    (Cons 4 (Cons 0 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 0 (Cons 3
+                    (Cons 0 (Cons 6 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 1 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 2
+                    (Cons 8 (Cons 9 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 4 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 0 Nil)))))))))
+              (Cons (Cons 0 (Cons 5 (Cons 0
+                    (Cons 1 (Cons 0 (Cons 0
+                    (Cons 0 (Cons 0 (Cons 0 Nil)))))))))
+               Nil))))))))))) 0;
+
+}
diff --git a/examples/Taut.hs b/examples/Taut.hs
new file mode 100644
--- /dev/null
+++ b/examples/Taut.hs
@@ -0,0 +1,95 @@
+{
+
+find key (Cons (Pair k v) t) = case (==) key k of {
+                               True  -> v ;
+                               False -> find key t ;
+                               } ;
+
+eval s (Const b)       = b ;
+eval s (Var x)         = find x s ;
+eval s (Not p)         = case eval s p of {
+                         True  -> False ;
+                         False -> True ;
+                         } ;
+eval s (And p q)       = case eval s p of {
+                         True  -> eval s q ;
+                         False -> False ;
+                         } ;
+eval s (Implies p q)   = case eval s p of {
+                         True  -> eval s q ;
+                         False -> True ;
+                         } ;
+
+vars (Const b)         = Nil ;
+vars (Var x)           = Cons x Nil ;
+vars (Not p)           = vars p ;
+vars (And p q)         = append (vars p) (vars q) ;
+vars (Implies p q)     = append (vars p) (vars q) ;
+
+bools n = case (==) n 0 of {
+          True  -> Cons Nil Nil ;
+          False -> let { bss = bools ((-) n 1) } in
+                   append (map (Cons False) bss)
+                          (map (Cons True)  bss) ;
+          } ;
+
+neq x y = (/=) x y;
+
+rmdups Nil         = Nil ;
+rmdups (Cons x xs) = Cons x (rmdups (filter (neq x) xs)) ;
+
+substs p = let { vs = rmdups (vars p) } in
+           map (zip vs) (bools (length vs)) ;
+
+isTaut p = and (map (flip eval p) (substs p)) ;
+
+flip f y x = f x y ;
+
+length Nil         = 0 ;
+length (Cons x xs) = (+) 1 (length xs) ;
+
+append Nil         ys = ys ;
+append (Cons x xs) ys = Cons x (append xs ys) ;
+
+map f Nil         = Nil ;
+map f (Cons x xs) = Cons (f x) (map f xs) ;
+
+and Nil         = True ;
+and (Cons b bs) = case b of {
+                  True  -> and bs ;
+                  False -> False ;
+                  } ;
+
+filter p Nil         = Nil ;
+filter p (Cons x xs) = case p x of {
+                       True  -> Cons x (filter p xs) ;
+                       False -> filter p xs ;
+                       } ;
+
+null Nil         = True ;
+null (Cons x xs) = False;
+
+zip Nil         ys          = Nil ;
+zip (Cons x xs) Nil         = Nil ; 
+zip (Cons x xs) (Cons y ys) = Cons (Pair x y) (zip xs ys) ;
+
+foldr1 f (Cons x xs) = case null xs of {
+                       True  -> x ;
+                       False -> f x (foldr1 f xs) ;
+                       } ;
+
+imp v = Implies (Var 'p') (Var v) ;
+
+names = "abcdefghijklmn" ;
+
+testProp = Implies
+             (foldr1 And (map imp names))
+             (Implies (Var 'p') (foldr1 And (map Var names))) ;
+
+main = case isTaut testProp of {
+       True  -> emit 'T' 1 ;
+       False -> emit 'F' 0 ;
+       } ;
+
+}
+
diff --git a/examples/While.hs b/examples/While.hs
new file mode 100644
--- /dev/null
+++ b/examples/While.hs
@@ -0,0 +1,91 @@
+{
+
+value (Cons (Pair x y) s) v k =
+  case (==) x v of { True -> k y ; False -> value s v k };
+
+update Nil v k i = k Nil;
+update (Cons (Pair x y) s) v k i =
+  update s v (case (==) x v of {
+                True -> upd k v i;
+                False -> upd k x y;
+              }) i;
+
+upd k x y s = k (Cons (Pair x y) s);
+
+int n k = case (==) n 0 of { True -> k 0 ; False -> k n };
+
+bool False k = k False;
+bool True k = k True;
+
+add k a b = k ((+) a b);
+sub k a b = k ((-) a b);
+eq k a b = k ((==) a b);
+leq k a b = k ((<=) a b);
+notk k False = k True;
+notk k True = k False;
+andk k False a = k False;
+andk k True a = k a;
+
+seq f g k = f (comp g k);
+comp f g x = f (g x);
+
+aval (N n) s k = k n;
+aval (V x) s k = value s x k;
+aval (Add a1 a2) s k = seq (aval a1 s) (aval a2 s) (add k);
+aval (Sub a1 a2) s k = seq (aval a1 s) (aval a2 s) (sub k);
+
+bval TRUE s k = k True;
+bval FALSE s k = k False;
+bval (Eq a1 a2) s k = seq (aval a1 s) (aval a2 s) (eq k);
+bval (Le a1 a2) s k = seq (aval a1 s) (aval a2 s) (leq k);
+bval (Neg b) s k = bval b s (notk k);
+bval (And a1 a2) s k = seq (bval a1 s) (bval a2 s) (andk k);
+
+sosstm (Ass x a) s = aval a s (update s x Final);
+sosstm Skip s = Final s;
+sosstm (Comp ss1 ss2) s =
+  case sosstm ss1 s of {
+    Inter ss10 s0 -> Inter (Comp ss10 ss2) s0;
+    Final s0 -> Inter ss2 s0;
+  };
+sosstm (If b ss1 ss2) s = bval b s (cond s ss1 ss2);
+sosstm (While b ss) s =
+  Inter (If b (Comp ss (While b ss)) Skip) s;
+
+cond s ss1 ss2 c = case c of { True -> Inter ss1 s ; False -> Inter ss2 s };
+
+run (Inter ss s) = run (sosstm ss s);
+run (Final s) = s;
+
+ssos ss s = run (Inter ss s);
+
+id x = x;
+
+example = 
+  let {
+    divide = While (Le (V 1) (V 0))
+               (Comp (Ass 0 (Sub (V 0) (V 1)))
+                     (Ass 2 (Add (V 2) (N 1))));
+
+    callDivide = Comp (Ass 0 (V 3))
+                      (Comp (Ass 1 (V 4)) divide);
+
+    ndivs = Comp (Ass 4 (V 3))
+              (While (Neg (Eq (V 4) (N 0))) (
+                Comp callDivide
+                     (Comp (If (Eq (V 0) (N 0)) (Ass 5 (Add (V 5) (N 1))) Skip)
+                           (Ass 4 (Sub (V 4) (N 1))))
+              ));
+
+    sinit = Cons (Pair 0 0) (
+             Cons (Pair 1 0) (
+             Cons (Pair 2 0) (
+             Cons (Pair 3 10000) (
+             Cons (Pair 4 0) (
+             Cons (Pair 5 0) Nil)))));
+
+    } in value (ssos ndivs sinit) 5 id;
+
+main = emitInt example 0;
+
+}
diff --git a/fl-parsec.hs b/fl-parsec.hs
new file mode 100644
--- /dev/null
+++ b/fl-parsec.hs
@@ -0,0 +1,2 @@
+module Main (module Flite.Parsec.Flite) where
+	import Flite.Parsec.Flite
diff --git a/fl-pure.hs b/fl-pure.hs
new file mode 100644
--- /dev/null
+++ b/fl-pure.hs
@@ -0,0 +1,2 @@
+module Main (module Flite.Flite) where
+	import Flite.Flite
diff --git a/flite.cabal b/flite.cabal
new file mode 100644
--- /dev/null
+++ b/flite.cabal
@@ -0,0 +1,49 @@
+Name:               flite
+Version:            0.1
+Synopsis:           f-lite compiler, interpreter and libraries
+License:            BSD3
+License-file:       LICENSE
+Author:             Matthew Naylor
+Maintainer:         Jason Reich <jason@cs.york.ac.uk>, Matthew Naylor <mfn@cs.york.ac.uk>
+Stability:          provisional
+Homepage:           http://www.cs.york.ac.uk/fp/reduceron/
+Build-Type:         Simple
+Cabal-Version:      >=1.6
+Description:        The f-lite language is a subset of Haskell 98 and Clean consisting of function
+                    definitions, pattern matching, limited let expressions, function applications and
+                    constructor applications expressed in the explicit 'braces' layout-insensitive format.
+                    
+                    See README for more information.
+Category:           Compiler
+Extra-Source-Files: README examples/*.hs
+
+Flag Pure
+    Description:   Use the pure parser instead of the Parsec
+    Default:       False
+
+Executable flite-pure
+    Main-is:       fl-pure.hs
+    if flag(pure)
+        Build-Depends: base >= 3 && < 5, haskell98 >= 1 && < 2,
+                       array >= 0 && < 1, containers >= 0 && < 1
+    else
+        buildable:     False
+
+Executable flite
+    Main-is:       fl-parsec.hs
+    if flag(pure)
+        buildable:     False
+    else
+        Build-Depends: base >= 3 && < 5, haskell98 >= 1 && < 2,
+                       array >= 0 && < 1, containers >= 0 && < 1,
+                       parsec >= 2.1.0.1 && < 3
+    
+Library
+    Build-Depends:   base >= 3 && < 5, haskell98 >= 1 && < 2,
+                     array >= 0 && < 1, containers >= 0 && < 1,
+                     parsec >= 2.1.0.1 && < 3
+    Exposed-modules: Flite.CallGraph, Flite.Case, Flite.ConcatApp,
+                     Flite.Descend, Flite.Fresh, Flite.Identify, Flite.Identity,
+                     Flite.Inline, Flite.Let, Flite.Matching, Flite.Pretty,
+                     Flite.Syntax, Flite.Traversals, Flite.Writer,
+                     Flite.Parsec.Parse