diff --git a/Flite/Compile.hs b/Flite/Compile.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Compile.hs
@@ -0,0 +1,58 @@
+module Flite.Compile (compile) where
+
+import Flite.Syntax
+import Flite.Flatten
+import Flite.CompileFrontend
+import Flite.CompileBackend
+import Data.List
+import Flite.Inline
+
+compile :: InlineFlag -> Prog -> String
+compile i p = program (addBool cs, p2)
+  where
+    p0 = frontend i p
+    p1 = [(f, map getVar args, flatten rhs) | Func f args rhs <- p0]
+    cs = nub $ concat [ctrs b | (_, _, bs) <- p1, b <- map snd bs]
+    p2 = [ (funId f, length vs, [(v, map (toNode f p1) a) | (v, a) <- bs])
+         | (f, vs, bs) <- p1 ]
+
+addBool cs =
+  insertIf (notDefined "False") false
+    (insertIf (notDefined "True") true cs)
+  where
+    false = ("False", 0, 0)
+    true = ("True", 0, 1)
+    notDefined f cs = null [c | (c, _, _) <- cs, c == f]
+    insertIf p x xs = if p xs then x:xs else xs
+
+toNode f p (Fun g) = 
+  case arities of
+    [] -> FUN 2 (funId g)
+    n:_ -> FUN n (funId g)
+  where arities = [length args | (h, args, rhs) <- p, g == h]
+toNode f p (Var v) =
+  case v `elemIndex` args of
+    Nothing -> VAR v
+    Just i -> ARG i
+  where args = head [args | (g, args, rhs) <- p, f == g]
+toNode f p (Ctr c n i) = FUN (n+1) (funId c)
+toNode f p (Alts fs _) = FUN 0 (funId $ head fs)
+toNode f p (Int i) = INT i
+toNode f p Bottom = FUN 0 "_|_"
+
+funId f | '#' `elem` f = "ALT_" ++ map (tr '#' '_') f
+        | otherwise = f
+
+tr :: Eq a => a -> a -> a -> a
+tr a b x = if a == x then b else x
+
+
+ctr :: Exp -> [Cons]
+ctr (Ctr c n i) = [(funId c, n, i)]
+ctr _ = []
+
+ctrs :: [Exp] -> [Cons]
+ctrs = concatMap ctr
+
+getVar :: Exp -> String
+getVar (Var v) = v
diff --git a/Flite/CompileBackend.lhs b/Flite/CompileBackend.lhs
new file mode 100644
--- /dev/null
+++ b/Flite/CompileBackend.lhs
@@ -0,0 +1,588 @@
+========================
+REDUCERON MEMO 22
+Compiling F-lite to C
+Matthew N, 30 April 2009
+========================
+
+This memo defines a compiler from supercombinators to portable C.  It
+is intended as a back-end to the F-lite implementation.  The aim is to
+run F-lite programs on an FPGA soft-core, such as the Microblaze.
+
+> module Flite.CompileBackend where
+
+> import Data.List
+
+Heap layout
+-----------
+
+A node is a tagged pointer, storable in a single word of memory.
+
+> nodeType = "typedef unsigned long Node;"
+
+The least-significant bit of a node is a tag stating whether the node
+is an AP, containing a pointer to an application (a sequence of nodes)
+on the heap, or an OTHER, containing something else.
+
+  typedef enum {AP = 0, OTHER = 1} Tag;
+
+The 2nd least-significant bit of a node is a flag stating whether or
+not the node is the final node of an application.
+
+> macros = unlines
+>   [ "#define isFinal(n) ((n) & 2)"
+>   , "#define clearFinal(n) ((n) & (~2))"
+>   , "#define setFinal(n) ((n) | 2)"
+>   , "#define markFinal(n,final) ((final) ? setFinal(n) : clearFinal(n))"
+
+If a node is an AP, its remaining 30 bits is a word-aligned heap
+address.
+
+>   , "#define getAP(n) ((Node *) ((n) & (~3)))"
+
+If the node is an OTHER, its 3rd least-significant bit contains a
+sub-tag stating whether the the node is an INT or a FUN.
+
+  typedef enum {INT = 0, FUN = 1} Subtag;
+
+If a node is an INT, its remaining 29-bits is an unboxed integer.
+
+>   , "#define getINT(n) (((signed long) n) >> 3)"
+
+If a node is a FUN, its remaining 29-bits contains a 6-bit arity and a
+23-bit function identifier.
+
+>   , "#define getARITY(n) (((n) >> 3) & 63)"
+>   , "#define getFUN(n) ((n) >> 9)"
+
+More precisely:
+
+>   , "#define isAP(n) (((n) & 1) == 0)"
+>   , "#define isINT(n) (((n) & 5) == 1)"
+>   , "#define isFUN(n) (((n) & 5) == 5)"
+>   , "#define makeAP(a,final) ((unsigned long) (a) | ((final) << 1))"
+>   , "#define makeINT(i,final) (((i) << 3) | ((final) << 1) | 1)"
+>   , "#define makeFUN(arity,f,final) " ++
+>              "(((f) << 9) | ((arity) << 3) | ((final) << 1) | 5)"
+>   , "#define arity(n) (isFUN(n) ? getARITY(n) : 1)"
+>   ]
+
+Update records
+--------------
+
+An update record is a pair containing a stack pointer (to detect when
+a head normal form has been reached) and a heap pointer (stating where
+to write the head normal form).
+
+> updateType = "typedef struct { Node *s; Node *h; } Update;"
+
+Registers
+---------
+
+> registers = unlines
+>   [ "Node top;"           {- top of stack -}
+>   , "Node *sp;"           {- stack pointer -}
+>   , "Node *hp;"           {- heap pointer -}
+>   , "Node *tsp;"          {- to-space pointer -}
+>   , "Update *usp;"        {- update-stack pointer -}
+>   , "unsigned int dest;"  {- destination address for computed jumps -}
+>   ]
+
+Swapping
+--------
+
+The following code swaps the top two elements of the stack.  It is
+used in the evaluation of strict primitive functions.
+
+> swapCode = unlines
+>   [ "{"
+>   , "  Node tmp;"
+>   , "  tmp = top;"
+>   , "  top = sp[-1];"
+>   , "  sp[-1] = tmp;"
+>   , "}"
+>   ]
+
+Unwinding
+---------
+
+Unwinding copies an application from the heap onto the stack, and
+pushes an update record onto the update stack.
+
+> unwindCode = unlines
+>   [ "{"
+>   , "  Node *p;"
+>   , "  p = getAP(top);"
+>   , "  usp++; usp->s = sp; usp->h = p;"
+>   , "  for (;;) {"
+>   , "    top = *p++;"
+>   , "    if (isFinal(top)) break;"
+>   , "    *sp++ = top;"
+>   , "  }"
+>   , "}"
+>   ]
+
+Updating
+--------
+
+The following code determines if a normal form has been reached, and
+if so, performs an update.
+
+> updateCode = unlines
+>   [ "{"
+>   , "  unsigned int args, ari;"
+>   , "  Node *base;"
+>   , "  Node *p;"
+>   , "  ari = arity(top);"
+>   , "  if (sp - ari < stack) goto EXIT;"
+>   , "  DO_UPDATE:"
+>   , "  args = ((unsigned int) (sp - usp->s));"
+>   , "  if (ari > args && usp > ustack) {"
+>   , "    base = hp;"
+>   , "    p = sp - args;"
+>   , "    while (p < sp) *hp++ = clearFinal(*p++);"
+>   , "    *hp++ = setFinal(top);"
+>   , "    *(usp->h) = makeAP(base, 1);"
+>   , "    usp--;"
+>   , "    goto DO_UPDATE;"
+>   , "  }"
+>   , "}"
+>   ]
+
+Evaluation driver
+-----------------
+
+Evalution proceeds depedning on the element on top of the stack.
+
+> evalCode = unlines
+>   [ "EVAL:"
+>   , "if (isAP(top)) {"
+>   ,    unwindCode
+>   , "  goto EVAL;"
+>   , "}"
+>   , "else {"
+>   , "  EVAL_OTHER:"
+>   , "  if (hp > heapFull) collect();"
+>   ,    updateCode
+>   , "  if (isFUN(top)) {"
+>   , "    dest = getFUN(top);"
+>   , "    goto CALL;"
+>   , "  }"
+>   , "  else {"
+>   ,      swapCode
+>   , "    goto EVAL;"
+>   , "  }"
+>   , "}"
+>   ]
+
+Abstract syntax of source code
+------------------------------
+
+The body of a function is a list of identifier/application pairs.  The
+first element in the list contains the spine application of the
+function.
+
+> type Binding = (Id, App)
+
+> type Body = [Binding]
+
+An application is a list of nodes.
+
+> type App = [Node]
+
+> data Node
+>   = VAR Id        {- variable reference -}
+>   | ARG Int       {- argument reference -}
+>   | FUN Arity Id  {- function identifier -}
+>   | INT Int       {- integer -}
+>   deriving Show
+
+> type Id = String
+
+A function definition consists of an identifier, an arity, and a body.
+
+> type Defn = (Id, Arity, Body)
+
+> type Arity = Int
+
+For example, the F-lite function definition
+
+   s f g x = f x (g x);
+
+is represented in abstract syntax as follows.
+
+  ("s", 3, [ ("v0", [ARG 0, ARG 2, VAR "v1"])
+           , ("v1", [ARG 1, ARG 2])
+           ])
+
+A data constructor consists of identifier, an arity, and an index.
+
+> type Cons = (Id, Arity, Index)
+
+> type Index = Int
+
+A program consists of a list of constuctors and a list of function
+definitions.
+
+> type Program = ([Cons], [Defn])
+
+Function calling
+----------------
+
+Each function body is implemented as a case alternative in a large
+switch statement.  To jump to the code for a function, place the
+function's identifier in the 'dest' register and then 'goto CALL'.
+This double jump is not very efficient, but its not obvious how to do
+any better in C.
+
+> switchCode (cs, ds) = unlines
+>   [ "CALL:"
+>   , "switch (dest)"
+>   , "{"
+>   , prims          -- primitive definitions
+>   , constrs cs     -- constructor definitions
+>   , defns ds       -- function definitions
+>   , "}"
+>   ]
+
+Constructor compilation
+-----------------------
+
+Each constructor C used in the program is treated as a function with
+the following definition.
+
+  Ci v1 ... vn f = (f+i) v1 ... vn f
+
+where i is the index of the constructor, n is the artiy of the
+constructor, and (f+i) represents the function occuring i definitions
+after the definition of f in the program code.  It is assumed that
+case alternatives occur contiguously, ordered by index.  For example,
+the F-lite program
+
+  rev acc Nil = acc;
+  rev acc (Cons x xs) = rev (Cons x acc) xs;
+
+is transformed down to
+
+  rev acc xs = xs revCons acc;
+  revCons x xs acc = rev (Cons x acc) xs;
+  revNil acc = acc;
+
+if Cons has index 0 and Nil has index 1.
+
+(See Memo 13 for a more detailed explanation of how constructors and
+case expressions are treated.)
+
+> cons :: Cons -> String
+> cons (f, n, i) = unlines
+>   [ "case " ++ fun f ++ ":"
+>   , "{"
+>   , "dest = getFUN(sp[-" ++ show (n+1) ++ "]) + " ++ show i ++ ";"
+>   , "goto CALL;"
+>   , "}"
+>   , "break;"
+>   ]
+
+NB. No update is required because a case expression is not a normal form.
+
+> constrs :: [Cons] -> String
+> constrs = concatMap cons
+
+Function compilation
+--------------------
+
+> arg :: Int -> String
+> arg i = "ARG_" ++ show i
+
+> var :: Id -> String
+> var v = "VAR_" ++ v
+
+Map F-lite primitives to suitable C identifiers.
+
+> fun :: Id -> String
+> fun "(+)" = "PRIM_PLUS"
+> fun "(-)" = "PRIM_MINUS"
+> fun "(<=)" = "PRIM_LEQ"
+> fun "(==)" = "PRIM_EQ"
+> fun "(/=)" = "PRIM_NEQ"
+> fun "emit" = "PRIM_EMIT"
+> fun "emitInt" = "PRIM_EMITINT"
+> fun "_|_" = "PRIM_UNDEFINED"
+> fun f = "FUN_" ++ f
+
+> declareArgs :: Int -> String
+> declareArgs n = unlines $ map save [1..n]
+>   where save i = "Node " ++ arg i ++ " = sp[-" ++ show i ++ "];"
+
+> declareLocals :: String
+> declareLocals = "Node *base = hp;"
+
+> type Locs = [(Id, Int)]
+
+> node :: String -> Locs -> String -> Node -> String
+> node r vs final (INT i) =
+>   r ++ " = makeINT(" ++ show i ++ "," ++ final ++ ");"
+> node r vs final (ARG i) =
+>   r ++ " = markFinal(" ++ arg (i+1) ++ "," ++ final ++ ");"
+> node r vs final (VAR v) =
+>   r ++ " = makeAP(base+" ++ offset ++ "," ++ final ++ ");"
+>   where offset = show $ lookupVar v vs
+> node r vs final (FUN n f) = 
+>   r ++ " = makeFUN(" ++ show n ++ "," ++ fun f ++ "," ++ final ++ ");"
+
+> lookupVar v vs = case lookup v vs of { Nothing -> error msg ; Just i -> i }
+>   where msg = error ("Unknown identifier '" ++ v ++ "'")
+
+> app :: Locs -> App -> String
+> app vs app = unlines $ zipWith (node "*hp++" vs) finals app
+>   where finals = map (const "0") (init app) ++ ["1"]
+
+> spine :: Locs -> App -> String
+> spine vs ns = unlines
+>   [ unlines $ map (node "*sp++" vs "0") (init ns)
+>   , node "top" vs "0" (last ns)
+>   ]
+
+> varLocs :: Body -> Locs
+> varLocs body = zip vs (scanl (+) 0 (map length apps))
+>   where (vs, apps) = unzip body
+
+> body :: App -> Body -> String
+> body s b = unlines
+>   [ concatMap (app vs . snd) b
+>   , spine vs s
+>   , "goto EVAL;"
+>   ] where vs = varLocs b
+
+> defn :: Defn -> String
+> defn (f, n, bs) = unlines
+>   [ "case " ++ fun f ++ ":"
+>   , "{"
+>   , declareArgs n
+>   , declareLocals
+>   , "sp -= " ++ show n ++ ";"
+>   , body (snd s) b
+>   , "}"
+>   , "break;"
+>   ]
+>   where s:b = [(v, reverse a) | (v, a) <- bs]
+
+> defns :: [Defn] -> String
+> defns = concatMap defn
+
+Primitives
+----------
+
+> primIds :: [Id]
+> primIds =
+>   [ "(+)" , "(-)" , "(<=)" , "(==)", "(/=)", "emit", "emitInt", "_|_" ]
+
+Apply primitive arithmetic operator to 2nd and 3rd stack elements;
+store result in top.
+
+> arithPrim :: Id -> String -> String
+> arithPrim p op = unlines
+>   [ "case " ++ fun p ++ ":"
+>   , "{"
+>   , "top = makeINT(getINT(sp[-1]) " ++ op ++ " getINT(sp[-2]),0);"
+>   , "sp -= 2;"
+>   , "goto EVAL;"
+>   , "}"
+>   , "break;"
+>   ]
+
+Ditto for boolean operator.
+
+> boolPrim :: Id -> String -> String
+> boolPrim p op = unlines
+>   [ "case " ++ fun p ++ ":"
+>   , "{"
+>   , "top = (getINT(sp[-1]) " ++ op ++ " getINT(sp[-2])) ? "
+>       ++ "makeFUN(1," ++ fun "True"  ++ ",0) "
+>       ++ ": makeFUN(1," ++ fun "False" ++ ",0);"
+>   , "sp -= 2;"
+>   , "goto EVAL;"
+>   , "}"
+>   , "break;"
+>   ]
+
+Print the second stack element.
+
+> emitPrim :: Id -> String -> String
+> emitPrim p format = unlines
+>   [ "case " ++ fun p ++ ":"
+>   , "{"
+>   , "top = sp[-2];"
+>   , "printf(\"" ++ format ++ "\", getINT(sp[-1]));"
+>   , "sp -= 2;"
+>   , "goto EVAL;"
+>   , "}"
+>   , "break;"
+>   ]
+
+> undefPrim :: String
+> undefPrim = unlines
+>   [ "case " ++ fun "_|_" ++ ":"
+>   , "{"
+>   , "printf(\"ERROR: bottom!\\n\");"
+>   , "goto EXIT;"
+>   , "}"
+>   , "break;"
+>   ]
+
+> prims :: String
+> prims = unlines
+>   [ arithPrim "(+)" "+"
+>   , arithPrim "(-)" "-"
+>   , boolPrim "(<=)" "<="
+>   , boolPrim "(==)" "=="
+>   , boolPrim "(/=)" "!="
+>   , emitPrim "emit" "%c"
+>   , emitPrim "emitInt" "%i"
+>   , undefPrim
+>   ]
+
+Garbage collection
+------------------
+
+> copyAPCode = unlines
+>   [ "Node *copyAP(Node *src) {"
+>   , "  Node n;"
+>   , "  Node *from = src;"
+>   , "  Node *dst = tsp;"
+>   , "  n = *from;"
+>   , "  if (isAP(n)) {"
+>   , "    Node *loc = getAP(n);"
+>   , "    if (loc >= toSpace && loc < toSpaceEnd) return loc;"
+>   , "  }"
+>   , "  do {"
+>   , "    n = *from++; *tsp++ = n;"
+>   , "  } while (! isFinal(n));"
+>   , "  *src = (Node) dst;"
+>   , "  return dst;"
+>   , "}"
+>   ]
+
+> copyCode = unlines
+>   [ "void copy() {"
+>   , "  Node n;"
+>   , "  Node *low = toSpace;"
+>   , "  while (low < tsp) {"
+>   , "    n = *low;"
+>   , "    if (isAP(n)) {"
+>   , "      Node *loc = copyAP(getAP(n));"
+>   , "      *low = markFinal((Node) loc, isFinal(n));"
+>   , "    }"
+>   , "    low++;"
+>   , "  }"
+>   , "}"
+>   ]
+
+> collectCode = unlines
+>   [ "void collect () {"
+>   , "  Node n;"
+>   , "  Node *p1;"
+>   , "  Update *p2;"
+>   , "  Update *p3;"
+>   , "  tsp = toSpace;"
+>   , "  p1 = stack;"
+>   , "  while (p1 < sp) {"
+>   , "    n = *p1;"
+>   , "    if (isAP(n)) *p1 = (Node) copyAP(getAP(n));"
+>   , "    p1++;"
+>   , "  }"
+>   , "  if (isAP(top)) top = (Node) copyAP(getAP(top));"
+>   , "  copy();"
+>   , "  p2 = ustack+1;"
+>   , "  p3 = ustack;"
+>   , "  while (p2 <= usp) {"
+>   , "    n = *(p2->h);"
+>   , "    if (isAP(n) && getAP(n) >= toSpace && getAP(n) <= toSpaceEnd) {"
+>   , "      p3++;"
+>   , "      p3->s = p2->s;"
+>   , "      p3->h = getAP(n);"
+>   , "    }"
+>   , "    p2++;"
+>   , "  }"
+>   , "  usp = p3;"
+>   , "  hp = tsp;"
+>   , "  p1 = toSpace; toSpace = heap; heap = p1;"
+>   , "  p1 = toSpaceEnd; toSpaceEnd = heapEnd; heapEnd = p1;"
+>   , "  p1 = toSpaceFull; toSpaceFull = heapFull; heapFull = p1;"
+>   , "}"
+>   ]
+
+Global variables
+----------------
+
+We need to store the beginning and end address of each memory
+partition, to detect termination and exhaustion.
+
+> globals :: String
+> globals = unlines
+>   [ "Node *heap;"
+>   , "Node *heapEnd;"
+>   , "Node *heapFull;"
+>   , "Node *toSpace;"
+>   , "Node *toSpaceEnd;"
+>   , "Node *toSpaceFull;"
+>   , "Node *stack;"
+>   , "Node *stackEnd;"
+>   , "Update *ustack;"
+>   , "Update *ustackEnd;"
+>   ]
+
+Memory allocation
+-----------------
+
+> allocate :: Int -> Int -> String
+> allocate heapSize stackSize = unlines
+>   [ "heap = (Node *) malloc(sizeof(Node) * " ++ show heapSize ++ ");"
+>   , "hp = heap;"
+>   , "heapEnd = heap + " ++ show heapSize ++ ";"
+>   , "heapFull = heapEnd - 1000;"
+>   , "toSpace = (Node *) malloc(sizeof(Node) * " ++ show heapSize ++ ");"
+>   , "tsp = toSpace;"
+>   , "toSpaceEnd = toSpace + " ++ show heapSize ++ ";"
+>   , "toSpaceFull = toSpaceEnd - 1000;"
+>   , "stack = (Node *) malloc(sizeof(Node) * " ++ show stackSize ++ ");"
+>   , "sp = stack;"
+>   , "stackEnd = stack + " ++ show stackSize ++ ";"
+>   , "ustack = (Update *) malloc(sizeof(Update) * " ++ show stackSize ++ ");"
+>   , "usp = ustack;"
+>   , "ustackEnd = ustack + " ++ show stackSize ++ ";"
+>   ]
+
+Program compilation
+-------------------
+
+> funIds :: Program -> [String]
+> funIds (cs, ds) = map first cs ++ map first ds
+>   where first (x, y, z) = x
+
+> declareFuns :: Program -> String
+> declareFuns p =
+>   unlines $ [def f i | (f, i) <- zip (primIds ++ funIds p) [0..]]
+>   where def f i = "#define " ++ fun f ++ " " ++ show i
+
+> program :: Program -> String
+> program p = unlines
+>   [ "#include <stdio.h>"
+>   , "#include <stdlib.h>"
+>   , nodeType
+>   , updateType
+>   , macros
+>   , declareFuns p
+>   , registers
+>   , globals
+>   , copyAPCode
+>   , copyCode
+>   , collectCode
+>   , "int main(void) {"
+>   , allocate 8000000 1000000
+>   , "dest = " ++ fun "main" ++ ";"
+>   , switchCode p
+>   , evalCode
+>   , "EXIT:"
+>   , "return 0;"
+>   , "}"
+>   ]
diff --git a/Flite/CompileFrontend.hs b/Flite/CompileFrontend.hs
new file mode 100644
--- /dev/null
+++ b/Flite/CompileFrontend.hs
@@ -0,0 +1,28 @@
+module Flite.CompileFrontend (frontend) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Matching
+import Flite.Case
+import Flite.Let
+import Flite.Identify
+import Flite.Strictify
+import Flite.ConcatApp
+import Flite.Inline
+import Flite.Fresh
+import Control.Monad
+
+frontend :: InlineFlag -> Prog -> Prog
+frontend i p = snd (runFresh (frontendM i p) "$" 0)
+
+frontendM :: InlineFlag -> Prog -> Fresh Prog
+frontendM i p =
+      return (identifyFuncs p)
+  >>= desugarCase
+  >>= desugarEqn
+  >>= inlineLinearLet
+  >>= inlineSimpleLet
+  >>= return . caseElim
+  >>= return . concatApps
+  >>= inlineTop i
+  >>= return . strictifyPrim
diff --git a/Flite/Flatten.hs b/Flite/Flatten.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Flatten.hs
@@ -0,0 +1,66 @@
+module Flite.Flatten (flatten) where
+
+import Flite.Syntax
+import Flite.WriterState
+import Data.List
+import Flite.Traversals
+import Control.Monad
+
+expToApp :: Exp -> App
+expToApp (App e es) = e:es
+expToApp e = [e]
+
+type Flatten a = WriterState (Id, App) Int a
+
+intToId :: Int -> Id
+intToId i = "tmp_" ++ show i
+
+fresh :: Flatten Id
+fresh = do { i <- get ; set (i+1) ; return (intToId i) }
+
+flatten :: Exp -> [(Id, App)]
+flatten e
+  | length vs /= length (nub vs) = error "Flatten: the impossible happened"
+  | otherwise = (intToId i, spine) : binds
+  where
+    (i, binds, spine) = runWS (flattenSpine e) 0
+
+    vs = map fst binds
+
+flattenSpine :: Exp -> Flatten App
+flattenSpine (App e es) = mapM flattenExp (e:es)
+flattenSpine (PrimApp p es) = return (Prim p:) `ap` mapM flattenExp es
+flattenSpine (Let bs e) =
+  do (bs', e') <- freshLet (bs, e)
+     let (vs, es) = unzip bs'
+     mapM flattenSpine es >>= mapM write . zip vs
+     flattenSpine e'
+flattenSpine e = (:[]) `fmap` flattenExp e
+
+flattenExp :: Exp -> Flatten Exp
+flattenExp (App e es) =
+  do i <- fresh
+     app <- mapM flattenExp (e:es)
+     write (i, app)
+     return (Var i)
+flattenExp (PrimApp p es) =
+  do i <- fresh
+     app <- mapM flattenExp es
+     write (i, Prim p:app)
+     return (Var i)
+flattenExp (Let bs e) =
+  do (bs', e') <- freshLet (bs, e)
+     let (vs, es) = unzip bs'
+     mapM flattenSpine es >>= mapM write . zip vs
+     flattenExp e'
+flattenExp e = return e
+
+freshLet :: ([Binding], Exp) -> Flatten ([Binding], Exp)
+freshLet (bs, e) =
+  do ws <- mapM (\_ -> fresh) vs
+     let s = zip (map Var ws) vs
+     let e' = substMany e s
+     let es' = map (flip substMany s) es
+     return (zip ws es', e')
+  where
+    (vs, es) = unzip bs
diff --git a/Flite/Flite.hs b/Flite/Flite.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Flite.hs
@@ -0,0 +1,73 @@
+module Flite.Flite (main) where
+
+import Flite.Syntax
+import Flite.ParseLib
+import Flite.Parse
+import Flite.Pretty
+import Flite.Interp
+import Flite.Inline
+import Flite.Compile
+import Flite.RedCompile
+import Data.List
+import System
+import System.IO
+import System.Console.GetOpt
+
+data Flag =
+    Desugar
+  | CompileToC
+  | CompileToRed Int Int Int Int Int
+  | Inline (Maybe Int)
+
+isDisjoint (Inline i) = False
+isDisjoint flag = True
+
+options :: [OptDescr Flag]
+options =
+  [ Option ['d'] [] (NoArg Desugar) "desugar"
+  , Option ['c'] [] (NoArg CompileToC) "compile to C"
+  , Option ['r'] [] (OptArg red "MAXPUSH:APSIZE:MAXAPS:MAXLUTS:MAXREGS")
+                    "compile to Reduceron templates"
+  , Option ['i'] [] (OptArg (Inline . fmap read) "MAXAPS")
+                    "inline small function bodies"
+  ]
+  where
+    redDefaults = CompileToRed 6 4 2 1 0
+    red Nothing = redDefaults
+    red (Just s) =
+      case split ':' s of
+        [a, b, c, d, e] ->
+          CompileToRed (read a) (read b) (read c) (read d) (read e)
+        _ -> error (usageInfo header options)
+
+header = "Usage: Flite [OPTION...] FILE.hs"
+
+main =
+  do args <- getArgs
+     case getOpt Permute options args of
+       (flags, [fileName], []) -> run flags fileName
+       (_, _, errs) -> error (concat errs ++ usageInfo header options)
+
+run flags fileName =
+  do contents <- readFile fileName
+     let p = parse prog contents
+     let inlineFlag = head $ [InlineAll | Inline Nothing <- flags]
+                          ++ [InlineSmall i | Inline (Just i) <- flags]
+                          ++ [NoInline]
+     case filter isDisjoint flags of
+       [] -> interp inlineFlag p `seq` return ()
+       [Desugar] ->
+         putStrLn $ pretty $ frontend inlineFlag p
+       [CompileToC] -> putStrLn $ compile inlineFlag p
+       [CompileToRed slen alen napps nluts nregs] ->
+         mapM_ print $ redCompile inlineFlag slen alen napps nluts nregs p
+       _ -> error (usageInfo header options)
+
+-- Auxiliary
+
+split :: Eq a => a -> [a] -> [[a]]
+split x xs =
+  case elemIndex x xs of
+    Nothing -> [xs]
+    Just i -> let (first, rest) = splitAt i xs in
+                first : split x (dropWhile (== x) rest)
diff --git a/Flite/Interp.hs b/Flite/Interp.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Interp.hs
@@ -0,0 +1,159 @@
+module Flite.Interp (interp, frontend) where
+
+import Flite.Syntax hiding (Lam)
+import Data.Array
+import Flite.InterpFrontend
+import Flite.Inline
+import System.IO.Unsafe(unsafePerformIO)
+
+infixl :@
+
+data Val =
+    Error
+  | C Id Int Int [Val]
+  | F Id
+  | V Id
+  | N Int
+  | Lut (Array Int Val)
+  | Val :@ Val
+  | Lambda Id Val
+  | Lam (Val -> Val)
+
+instance Show Val where
+  show (Lam f) = "lambda!"
+  show (C n _ _ vs) = "(" ++ unwords (n:map show vs) ++ ")"
+  show (N i) = show i
+
+lut :: [Val] -> Val
+lut vs = Lut (listArray (0, length vs) vs)
+
+app :: [Val] -> Val
+app xs = foldl1 (:@) xs
+
+val :: Exp -> Val
+val (App e xs) = app (val e : map val xs)
+val (Var v) = V v
+val (Alts as _) = lut (map F as)
+val (Ctr s arity i) = C s arity i []
+val (Fun f) = F f
+val (Int n) = N n
+val Bottom = Error
+val (Let bs e) = elimLet vs (map val es) (val e)
+  where (vs, es) = unzip bs
+
+compile :: Prog -> [(Id, Val)]
+compile p = [(f, comp $ lambdify args $ val e) | Func f args e <- p]
+  where lambdify args e = foldr (\(Var v) -> Lambda v) e args
+
+comp :: Val -> Val
+comp (Lambda v x) = abstr v (comp x)
+comp (e1 :@ e2) = comp e1 :@ comp e2
+comp e = e
+
+abstr :: Id -> Val -> Val
+abstr v (e1 :@ e2) = opt (F "S" :@ abstr v e1 :@ abstr v e2)
+abstr v (V w)
+  | v == w = F "I"
+  | otherwise = F "K" :@ V w
+abstr v e = F "K" :@ e
+
+opt :: Val -> Val
+opt (F "S" :@ (F "K":@p) :@ (F "K" :@ q)) = F "K" :@ (p :@ q)
+opt (F "S" :@ (F "K":@p) :@ F "I") = p
+opt (F "S" :@ (F "K":@p) :@ (F "B" :@ q :@ r)) = F "B*" :@ p :@ q :@ r
+opt (F "S" :@ (F "K":@p) :@ q) = F "B" :@ p :@ q
+opt (F "S" :@ (F "B":@p:@q) :@ (F "K" :@ r)) = F "C'" :@ p :@ q :@ r
+opt (F "S" :@ p :@ (F "K":@q)) = F "C" :@ p :@ q
+opt (F "S" :@ (F "B":@p:@q) :@ r) = F "S'" :@ p :@ q :@ r
+opt e = e
+
+interp :: InlineFlag -> Prog -> Val
+interp i p = case lookup "main" bs of
+             Nothing -> error "No 'main' function defined"
+             Just e -> e
+  where bs = prims ++ map (\(f, e) -> (f, link bs e)) (compile p')
+        p' = frontend i p
+
+link :: [(Id, Val)] -> Val -> Val
+link bs (f :@ a) = link bs f @@ link bs a
+link bs (Lut a) = Lut (fmap (link bs) a)
+link bs (F f) = case lookup f bs of
+                  Nothing -> error ("Function '" ++ f ++ "' not defined")
+                  Just e -> e
+link bs Error = error "_|_"
+link bs (V v) = error ("Unknown identifier '" ++ v ++ "'")
+link bs e = e
+
+infixl 0 @@
+(@@) :: Val -> Val -> Val
+(Lam f) @@ x = f x
+(C s 0 i args) @@ (Lut alts) = run (alts ! i) args @@ Lut alts
+(C s arity i args) @@ x = C s (arity-1) i (x:args)
+
+run :: Val -> [Val] -> Val
+run e [] = e
+run e (x:xs) = run e xs @@ x
+
+prims :: [(Id, Val)]
+prims = let (-->) = (,) in
+ [ "I" --> (Lam $ \x -> x)
+ , "K" --> (Lam $ \x -> Lam $ \y ->  x)
+ , "S" --> (Lam $ \f -> Lam $ \g -> Lam $ \x -> f@@x@@(g@@x))
+ , "B" --> (Lam $ \f -> Lam $ \g -> Lam $ \x -> f@@(g@@x))
+ , "C" --> (Lam $ \f -> Lam $ \g -> Lam $ \x -> f@@x@@g)
+ , "S'" --> (Lam $ \c -> Lam $ \f -> Lam $ \g -> Lam $ \x -> c@@(f@@x)@@(g@@x))
+ , "B*" --> (Lam $ \c -> Lam $ \f -> Lam $ \g -> Lam $ \x -> c@@(f@@(g@@x)))
+ , "C'" --> (Lam $ \c -> Lam $ \f -> Lam $ \g -> Lam $ \x -> c@@(f@@x)@@g)
+ , "Y" --> (Lam $ \f -> fix f)
+ , "(+)" --> arith2 (+)
+ , "(-)" --> arith2 (-)
+ , "(==)" --> logical2 (==)
+ , "(/=)" --> logical2 (/=)
+ , "(<=)" --> logical2 (<=)
+ , "emit" --> (Lam $ \(N a) -> Lam $ \k -> emitStr [toEnum a] k)
+ , "emitInt" --> (Lam $ \(N a) -> Lam $ \k -> emitStr (show a) k)
+ ]
+
+fix :: Val -> Val
+fix f = let a = f @@ a in a
+
+arith2 :: (Int -> Int -> Int) -> Val
+arith2 op = Lam $ \(N a) -> Lam $ \(N b) -> N (op a b)
+
+logical2 :: (Int -> Int -> Bool) -> Val
+logical2 op =
+  Lam $ \(N a) -> Lam $ \(N b) -> if op a b then true else false
+
+false :: Val
+false = C "False" 0 0 []
+
+true :: Val
+true = C "True" 0 1 []
+
+emitStr :: String -> a -> a
+emitStr s k = unsafePerformIO (putStr s >> return k)
+
+-- Unfortunatly, handling recursive lets is a bit tricky.
+-- Here's SPJ's solution, more-or-less.
+
+elimLet :: [Id] -> [Val] -> Val -> Val
+elimLet vs es e = (Lambda "#" $ sub e) :@ (F "Y" :@ Lambda "#" t)
+  where
+    t = app (tuple (length vs):map sub es)
+    sels = [V "#" :@ select (length vs) i | i <- [0..]]
+    sub e = subst (zip vs sels) e
+
+tuple :: Int -> Val
+tuple n = foldr Lambda (app $ map (V . var) (n:[0..n-1])) (map var [0..n])
+  where var i = 'v':show i
+
+select :: Int -> Int -> Val
+select n i = foldr Lambda (V (var i)) (map var [0..n-1])
+  where var i = 'v':show i
+
+subst :: [(Id, Val)] -> Val -> Val
+subst s (e1 :@ e2) = subst s e1 :@ subst s e2
+subst s (V v) = case lookup v s of
+                  Nothing -> V v
+                  Just x -> x
+subst s e = e
diff --git a/Flite/InterpFrontend.hs b/Flite/InterpFrontend.hs
new file mode 100644
--- /dev/null
+++ b/Flite/InterpFrontend.hs
@@ -0,0 +1,51 @@
+module Flite.InterpFrontend (frontend) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.ConcatApp
+import Flite.Matching
+import Flite.Case
+import Flite.Let
+import Flite.Identify
+import Flite.Inline
+import Flite.Fresh
+import Control.Monad
+
+frontend :: InlineFlag -> Prog -> Prog
+frontend i p = snd (runFresh (frontendM i p) "$" 0)
+
+frontendM :: InlineFlag -> Prog -> Fresh Prog
+frontendM i p =
+      return (identifyFuncs p)
+  >>= desugarCase
+  >>= desugarEqn
+  >>= inlineLinearLet
+  >>= inlineSimpleLet
+  >>= return . caseElim
+  >>= return . concatApps
+  >>= inlineTop i
+  >>= liftLet
+  >>= return . finalPass
+
+finalPass :: Prog -> Prog
+finalPass = map freshen
+  where
+    freshen (Func f args rhs) = Func f (map Var args') (mkLet bs' e')
+      where n = length args
+            args' = map (('v':) . show) [0..n-1]
+            (bs, e) = body rhs
+            (vs, es) = unzip bs
+            ws = map (('v':) . show) [n..n+length vs-1]
+            from = map var args ++ vs
+            to = args' ++ ws
+            (e':es') = foldr (\(v, w) -> map (subst (Var w) v))
+                             (e:es) (zip from to)
+            bs' = zip ws es'
+
+    var (Var v) = v
+
+    body (Let bs e) = (bs, e)
+    body e = ([], e)
+
+    mkLet [] e = e
+    mkLet bs e = Let bs e
diff --git a/Flite/LambdaLift.hs b/Flite/LambdaLift.hs
new file mode 100644
--- /dev/null
+++ b/Flite/LambdaLift.hs
@@ -0,0 +1,33 @@
+module Flite.LambdaLift (lambdaLift) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+import Flite.WriterState
+import Control.Monad
+
+-- Introduces functions of the form "f^N" where is is a natural
+-- number.  Therefore assumes function identifiers do not already
+-- contain '^' character.
+
+lambdaLift :: Prog -> Prog
+lambdaLift = concatMap liftDecl
+
+type Lift a = WriterState Decl Int a
+
+liftDecl :: Decl -> [Decl]
+liftDecl (Func f args rhs) = Func f args rhs' : ds
+  where
+    (_, ds, rhs') = runWS (lift f rhs) 0
+
+lift :: Id -> Exp -> Lift Exp
+lift f (Lam [] e) = lift f e
+lift f (Lam vs e) =
+  do let ws = filter (`notElem` vs) (freeVars e)
+     i <- get
+     set (i+1)
+     let f' = f ++ "^" ++ show i
+     e' <- lift f e
+     write (Func f' (map Var (ws ++ vs)) e')
+     return (App (Fun f') (map Var ws))
+lift f e = descendM (lift f) e
diff --git a/Flite/Parse.hs b/Flite/Parse.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Parse.hs
@@ -0,0 +1,92 @@
+module Flite.Parse where
+
+import Flite.ParseLib
+import Flite.Syntax
+import Data.Char
+
+parseProg = parse prog
+
+keywords :: [String]
+keywords =
+  [ "case", "of", "let"
+  , "in", "emit", "emitInt"
+  , "if", "then", "else"
+  ]
+
+identifier :: Parser Char -> Parser String
+identifier begin = token (guarded g (pure (:) <*> begin <*> many alphanum))
+  where g s = s `notElem` keywords
+
+lowerIdent :: Parser String
+lowerIdent = identifier lower
+
+upperIdent :: Parser String
+upperIdent = identifier upper
+
+key :: String -> Parser String
+key s = token $ \input ->
+  [(rest, a) | (rest, a) <- string s input
+             , null rest || not (isAlphaNum (head rest))]
+
+prog :: Parser Prog
+prog = block defn
+
+block :: Parser a -> Parser [a]
+block p = tok "{" |> seq <| tok "}"
+  where seq = seq' <| (tok ";" <|> pure "")
+        seq' = pure (:) <*> p <*> many (tok ";" |> p)
+
+defn :: Parser Decl
+defn = pure Func <*> lowerIdent <*> many pat <*> tok "=" |> expr
+
+expr :: Parser Exp
+expr = pure App <*> expr' <*> many expr'
+
+expr' :: Parser Exp
+expr' = pure Case <*> (key "case" |> expr) <*> (key "of" |> block alt)
+    <|> pure Let  <*> (key "let" |> block bind) <*> (key "in" |> expr)
+    <|> pure Var  <*> lowerIdent
+    <|> pure Con  <*> upperIdent
+    <|> pure Int  <*> nat
+    <|> pure Fun  <*> prim
+    <|> ifte
+    <|> pure charList <*> token strLit
+    <|> pure oneChar <*> token charLit
+    <|> tok "(" |> expr <| tok ")"
+
+prim :: Parser String
+prim = tok "(+)" <|> tok "(-)" <|> tok "(==)" <|> tok "(/=)" <|> tok "(<=)"
+   <|> key "emit" <|> key "emitInt"
+
+pat :: Parser Pat
+pat = pure Var <*> lowerIdent
+  <|> pure (\s -> App (Con s) []) <*> upperIdent
+  <|> tok "(" |> pat' <| tok ")"
+
+pat' :: Parser Pat
+pat' = pure Var <*> lowerIdent
+   <|> pure App <*> (pure Con <*> upperIdent) <*> many pat
+
+bind :: Parser Binding
+bind = pure (,) <*> (lowerIdent <| tok "=") <*> expr
+
+alt :: Parser Alt
+alt = pure (,) <*> (pat' <| tok "->" ) <*> expr
+
+ifte :: Parser Exp
+ifte = pure cond <*> (key "if" |> expr)
+                 <*> (key "then" |> expr)
+                 <*> (key "else" |> expr)
+  where
+    cond e1 e2 e3 = Case e1 [ (App (Con "True") [], e2)
+                            , (App (Con "False") [], e3)
+                            ]
+
+charList :: String -> Exp
+charList s = charList' (read s)
+  where
+    charList' "" = Con "Nil"
+    charList' (c:cs) = App (Con "Cons") [Int (fromEnum c), charList' cs]
+
+oneChar :: String -> Exp
+oneChar s = Int (fromEnum (read s :: Char))
diff --git a/Flite/ParseLib.hs b/Flite/ParseLib.hs
new file mode 100644
--- /dev/null
+++ b/Flite/ParseLib.hs
@@ -0,0 +1,97 @@
+module Flite.ParseLib where
+
+import Data.Char
+
+infixr 3 <|>
+infixl 4 <*>
+infixl 5 <|
+infixl 6 |>
+
+type Parser a = String -> [(String, a)]
+
+pure :: a -> Parser a
+pure a = \s -> [(s, a)]
+
+(<*>) :: Parser (a -> b) -> Parser a -> Parser b
+f <*> a = \s -> [(s1, g b) | (s0, g) <- f s, (s1, b) <- a s0]
+
+(|>) :: Parser a -> Parser b -> Parser b
+a |> b = pure (\a b -> b) <*> a <*> b
+
+(<|) :: Parser a -> Parser b -> Parser a
+a <| b = pure (\a b -> a) <*> a <*> b
+
+(<|>) :: Parser a -> Parser a -> Parser a
+a <|> b = \s -> take 1 (a s ++ b s)
+
+guarded :: (a -> Bool) -> Parser a -> Parser a
+guarded f p = \s -> [(s', a) | (s', a) <- p s, f a]
+
+sat :: (Char -> Bool) -> Parser Char
+sat f "" = []
+sat f (c:s) = [(s, c) | f c]
+
+char :: Char -> Parser Char
+char c = sat (== c)
+
+string :: String -> Parser String
+string "" = pure ""
+string (c:cs) = pure (:) <*> char c <*> string cs
+
+alphanum :: Parser Char
+alphanum = sat isAlphaNum
+
+digit :: Parser Int
+digit = pure (\c -> ord c - ord '0') <*> sat isDigit
+
+lower :: Parser Char
+lower = sat isLower
+
+upper :: Parser Char
+upper = sat isUpper
+
+many :: Parser a -> Parser [a]
+many p = many1 p <|> pure []
+
+many1 :: Parser a -> Parser [a]
+many1 p = pure (:) <*> p <*> many p
+
+space :: Parser String
+space = many (sat isSpace)
+
+token :: Parser a -> Parser a
+token p = p <| space
+
+tok :: String -> Parser String
+tok = token . string
+
+nat :: Parser Int
+nat = token natural
+
+natural :: Parser Int
+natural = pure total <*> many1 digit
+  where total = foldl (\acc n -> 10*acc + n) 0
+
+int :: Parser Int
+int = token integer
+
+integer :: Parser Int
+integer = natural <|> pure negate <*> (char '-' |> natural)
+
+strLit :: Parser String
+strLit s@('"':_) = map swap (lex s)
+  where swap (a, b) = (b, a)
+strLit _ = []
+
+charLit :: Parser String
+charLit s@('\'':_) = map swap (lex s)
+  where swap (a, b) = (b, a)
+charLit _ = []
+
+parse :: Parser a -> String -> a
+parse p s =
+  case p s of
+    []        -> error "Parse error"
+    [("", x)] -> x
+    [(s, x)]  -> error "Parse error"
+    _         -> error "Ambiguous parse --- this shouldn't happen!"
diff --git a/Flite/Parsec/Flite.hs b/Flite/Parsec/Flite.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Parsec/Flite.hs
@@ -0,0 +1,71 @@
+module Flite.Parsec.Flite (main) where
+
+import Flite.Syntax
+import Flite.Parsec.Parse
+import Flite.Pretty
+import Flite.Interp
+import Flite.Inline
+import Flite.Compile
+import Flite.RedCompile
+import Data.List
+import System
+import System.IO
+import System.Console.GetOpt
+
+data Flag =
+    Desugar
+  | CompileToC
+  | CompileToRed Int Int Int Int Int
+  | Inline (Maybe Int)
+
+isDisjoint (Inline i) = False
+isDisjoint flag = True
+
+options :: [OptDescr Flag]
+options =
+  [ Option ['d'] [] (NoArg Desugar) "desugar"
+  , Option ['c'] [] (NoArg CompileToC) "compile to C"
+  , Option ['r'] [] (OptArg red "MAXPUSH:APSIZE:MAXAPS:MAXLUTS:MAXREGS")
+                    "compile to Reduceron templates"
+  , Option ['i'] [] (OptArg (Inline . fmap read) "MAXAPS")
+                    "inline small function bodies"
+  ]
+  where
+    redDefaults = CompileToRed 6 4 2 1 0
+    red Nothing = redDefaults
+    red (Just s) =
+      case split ':' s of
+        [a, b, c, d, e] ->
+          CompileToRed (read a) (read b) (read c) (read d) (read e)
+        _ -> error (usageInfo header options)
+
+header = "Usage: Flite [OPTION...] FILE.hs"
+
+main =
+  do args <- getArgs
+     case getOpt Permute options args of
+       (flags, [fileName], []) -> run flags fileName
+       (_, _, errs) -> error (concat errs ++ usageInfo header options)
+
+run flags fileName =
+  do p <- parseProgFile fileName
+     let inlineFlag = head $ [InlineAll | Inline Nothing <- flags]
+                          ++ [InlineSmall i | Inline (Just i) <- flags]
+                          ++ [NoInline]
+     case filter isDisjoint flags of
+       [] -> interp inlineFlag p `seq` return ()
+       [Desugar] ->
+         putStrLn $ pretty $ frontend inlineFlag p
+       [CompileToC] -> putStrLn $ compile inlineFlag p
+       [CompileToRed slen alen napps nluts nregs] ->
+         mapM_ print $ redCompile inlineFlag slen alen napps nluts nregs p
+       _ -> error (usageInfo header options)
+
+-- Auxiliary
+
+split :: Eq a => a -> [a] -> [[a]]
+split x xs =
+  case elemIndex x xs of
+    Nothing -> [xs]
+    Just i -> let (first, rest) = splitAt i xs in
+                first : split x (dropWhile (== x) rest)
diff --git a/Flite/Predex.hs b/Flite/Predex.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Predex.hs
@@ -0,0 +1,205 @@
+-- Compilation routines for speculative evaluation of primitive redexes
+
+-- Currently we only allow as many primitive applications in a
+-- function body as there are PRS registers in the machine.  This is
+-- overly-strong constraint that can be generalised (and lifted) in a
+-- range of ways with varying ease and efficiency.  (As the feature is
+-- experimental, we have taken a rather simple-minded approach to
+-- compilation.)
+
+module Flite.Predex where
+
+import Data.List
+import Flite.Syntax
+import Control.Monad
+import Flite.Traversals
+import qualified Flite.RedSyntax as R
+
+-- Identify candidates.
+identifyPredexCandidates :: Int -> Prog -> Prog
+identifyPredexCandidates nregs p = onExp (identify nregs) p
+
+identify :: Int -> Exp -> Exp
+identify 0 e = e
+identify nregs e =
+  case runCount (ident [] e) nregs of
+    (n, e') -> if n == 0 then e' else identify (nregs-n) e'
+
+--identSpine :: [(Id, Bool)] -> Exp -> Count Exp
+--identSpine scope e
+--  | isFlat e = return e
+--  | otherwise = ident scope e
+
+ident :: [(Id, Bool)] -> Exp -> Count Exp
+ident scope (App (Fun f) xs) | isPredexId f =
+  do xs' <- mapM (ident scope) xs
+     let e' = App (Fun f) xs'
+     if checkArgs scope xs' then one (PrimApp f xs') e' else return e'
+ident scope (App e es) =
+  return App `ap` ident scope e `ap` mapM (ident scope) es
+ident scope (Let bs e) =
+  do let (vs, es) = unzip bs
+     let scope' = zip vs (map isPrimApp es) ++ scope
+     e':es' <- mapM (ident scope') (e:es)
+     return (Let (zip vs es') e')
+{-
+ident scope (Case e alts) = 
+  do let (ps, es) = unzip alts
+     let pvs = concatMap patVars ps
+     let scope' = [(v, b) | (v, b) <- scope, notElem v pvs]
+     e' <- ident scope e
+     es' <- mapM (ident scope') es
+     return (Case e' (zip ps es'))
+-}
+ident scope (PrimApp p es) = return (PrimApp p es)
+ident scope e = return e
+  
+isPrimApp :: Exp -> Bool
+isPrimApp (PrimApp p es) = True
+isPrimApp _ = False
+
+checkArgs :: [(Id, Bool)] -> [Exp] -> Bool
+checkArgs scope es = all (checkArg scope) es
+
+checkArg :: [(Id, Bool)] -> Exp -> Bool
+checkArg scope (Int i) = True
+checkArg scope (PrimApp p xs) = True
+checkArg scope (Var v) = 
+  case lookup v scope of
+    Nothing -> True
+    Just b -> b
+checkArg scope e = False
+
+{-
+isFlat :: Exp -> Bool
+isFlat (Let bs e) = False
+isFlat (App e es) = isFlat e && all flat es
+isFlat e = True
+
+flat (Let bs e) = False
+flat (App e es) = False
+flat e = True
+-}
+
+
+-- A monad that allows one to count and bound the number of
+-- transformations that are applied during a computation.
+data Count a = Count { runCount :: Int -> (Int, a) }
+
+instance Monad Count where
+  return a = Count $ \n -> (n, a)
+  x >>= f = Count $ \n -> case runCount x n of (m, y) -> runCount (f y) m
+
+one :: a -> a -> Count a
+one a b = Count $ \n -> if n > 0 then (n-1, a) else (n, b)
+
+-- Given an expression, ensure that a primitive redex candidate does
+-- not occupy the spine
+removePredexSpine :: Exp -> Exp
+removePredexSpine (PrimApp p xs) = App (PrimApp p xs) []
+removePredexSpine e = e
+
+-- Given a flattened body, ensure primitive applications occur
+-- before their use, and before any non primitive applications.
+predexReorder :: Int -> [(Id, App)] -> [(Id, App)]
+predexReorder 0 apps = apps
+predexReorder maxRegs apps
+  | length prims > maxRegs =
+      error "Predex: too many primitive applications in body"
+  | otherwise = concat (groupApps prims) ++ nonPrims
+  where
+    (prims, nonPrims) = partition (isPrimitiveApp . snd) apps
+
+-- Detect primitive applications
+isPrimitiveApp :: App -> Bool
+isPrimitiveApp (Prim p:args) = True
+isPrimitiveApp app = False
+
+-- An application A depends on an application B if A refers to B's result.
+depends :: (Id, App) -> (Id, App) -> Bool
+depends (v, a) (w, b) = any (`refersTo` w) a
+
+refersTo (Var v) w = v == w
+refersTo _ _ = False
+
+-- Split applications into groups of independent applications, where
+-- each group has no dependencies on any later level.
+groupApps :: [(Id, App)] -> [[(Id, App)]]
+groupApps = levels depends
+
+levels :: (a -> a -> Bool) -> [a] -> [[a]]
+levels p [] = []
+levels p xs = this : levels p rest
+  where
+    this = [x | x <- xs, not (any (p x) xs)]
+    rest = [x | x <- xs, any (p x) xs]
+
+-- Associate every primitive application with a register.  Redirect
+-- all references to a primitive application to its register.
+predex :: Int -> ([R.Atom], [R.App]) -> ([R.Atom], [R.App])
+predex 0 (spine, apps) = (spine, apps)
+predex n (spine, apps) =
+  (map (redirect nprims) spine, map (redirectApp nprims) apps')
+  where
+    apps' = regAlloc apps
+    nprims = countPrims apps'
+
+redirectApp :: Int -> R.App -> R.App
+redirectApp n app = mapAtoms (redirect n) app
+
+redirect n (R.VAR s i) | i < n = R.REG s i
+redirect n a = a
+
+regAlloc :: [R.App] -> [R.App]
+regAlloc = snd . mapAccumL alloc 0
+
+alloc :: Int -> R.App -> (Int, R.App)
+alloc r (R.PRIM _ xs) = (r+1, R.PRIM r xs)
+alloc r app = (r, app)
+
+countPrims :: [R.App] -> Int
+countPrims = sum . map count
+  where
+    count (R.PRIM r as) = 1
+    count _ = 0
+
+mapAtoms :: (R.Atom -> R.Atom) -> R.App -> R.App
+mapAtoms f (R.APP n as) = R.APP n (map f as)
+mapAtoms f (R.PRIM r as) = R.PRIM r (map f as)
+mapAtoms f (R.CASE lut as) = R.CASE lut (map f as)
+
+-- Given a list of applications, return the initial portion that can
+-- be executed in the same clock-cycle, and the rest.
+splitPredexes :: [R.App] -> ([R.App], [R.App])
+splitPredexes apps
+  | null apps0 = (apps1, [])
+  | otherwise = (apps2, apps3 ++ apps1)
+  where
+    (apps0, apps1) = span isPRIM apps
+    (apps2, apps3) = split [] apps0
+
+    split rs [] = ([], [])
+    split rs apps@(R.PRIM r as:rest)
+      | any (`refersTo` rs) as = ([], R.PRIM r as:rest)
+      | otherwise = (R.PRIM r as:xs, ys)
+      where (xs, ys) = split (r:rs) rest
+
+    refersTo (R.REG _ r) rs = r `elem` rs
+    refersTo _ rs = False
+
+isPRIM :: R.App -> Bool
+isPRIM (R.PRIM r as) = True
+isPRIM _ = False
+
+-- Combinators for forcing evaluation of primitive arguments.
+force01 :: Decl
+force01 = Func "!force01" [Var "p", Var "a", Var "b"] $
+  App (Var "b") [App (Var "a") [Var "p"]]
+
+force0 :: Decl
+force0 = Func "!force0" [Var "p", Var "a", Var "b"] $
+  App (Var "a") [Var "p", Var "b"]
+
+force1 :: Decl
+force1 = Func "!force1" [Var "p", Var "a", Var "b"] $
+  App (Var "b") [App (Var "p") [Var "a"]]
diff --git a/Flite/RedCompile.hs b/Flite/RedCompile.hs
new file mode 100644
--- /dev/null
+++ b/Flite/RedCompile.hs
@@ -0,0 +1,226 @@
+module Flite.RedCompile where
+
+-- Parameterise app-length, spine-length and num apps per template,
+-- but not arity limit (for now).
+
+import Flite.Syntax
+import Flite.Flatten
+import Flite.RedFrontend
+import Data.List
+import Flite.Traversals
+import Flite.WriterState
+import Flite.Inline
+import Flite.Predex
+import qualified Flite.RedSyntax as R
+
+import Flite.Pretty
+import Debug.Trace
+
+-- Splits applications so that they contain no more than one 'Alts' node.
+
+splitCase :: App -> Bind App
+splitCase app
+  | length is <= 1 = return app
+  | otherwise = do i <- freshId ; write (i, app0) ; splitCase (Var i:rest)
+  where
+    is = findIndices isAlts app
+    (app0, rest) = splitAt (is !! 1) app
+
+-- Splits an application so that it has maximum length 'n'.
+
+splitApp :: Int -> App -> Bind App
+splitApp n app
+  | length app <= n = return app
+  | otherwise = do i <- freshId ; write (i, app0) ; splitApp n (Var i:rest)
+  where (app0, rest) = splitAt n app
+
+-- Splits a group of applications so that they each have maximum
+-- length 'n' and no more than one 'Alts' node.
+
+splitApps :: Int -> [(Id, App)] -> [(Id, App)]
+splitApps n apps = cs ++ ds
+  where
+    (i, as, bs) = runWS (mapM splitCase' apps) 0
+    (j, cs, ds) = runWS (mapM splitApp' (as ++ bs)) i
+    splitCase' (v, app) = (,) v `fmap` (splitCase app)
+    splitApp' (v, app) = (,) v `fmap` (splitApp n app)
+
+splitSpine :: Int -> [(Id, App)] -> (App, [(Id, App)], [Exp])
+splitSpine n ((v, app):rest)
+  | length spine <= n = (spine, rest, luts)
+  | otherwise = -- Needed????
+      ( Var v:takeBack (n-1) spine
+      , (v, dropBack (n-1) spine):rest
+      , luts
+      )
+  where
+    spine = filter (not . isAlts) app
+    luts = filter isAlts app
+
+-- Translates a program to Reduceron syntax.  Takes the max
+-- application length and max spine length as arguments.
+
+translate :: InlineFlag -> Int -> Int -> Int -> Prog -> R.Prog
+translate i n m nregs p = map (trDefn n m nregs p2) p2
+  where
+    p0 = frontend nregs i (force01:force0:force1:p)
+    p1 = [ (f, map getVar args, flatten $ removePredexSpine rhs)
+         | Func f args rhs <- p0
+         ]
+    p2 = lift "main" p1
+
+trDefn n m nregs p (f, args, xs) =
+  (f, length args, luts, pushs', apps')
+  where
+    (spine, body, ls) = splitSpine m xs
+    body' = predexReorder nregs $ splitApps n body
+    d = (f, args, spine, body')
+    luts = map (indexOf p) $ map getAlts ls
+    apps = map (trApp p d . snd) body'
+    pushs = map (tr p d) $ filter (not . isAlts) spine
+    (pushs', apps') = predex nregs (pushs, apps)
+
+trApp p d app
+   | isPrimitiveApp app = R.PRIM (-1) rest
+  -- | isPrimitiveApp app = R.PRIM (-1) (reverse rest) {- PV STACK -}
+  | null luts = R.APP (isNormal rest) rest
+  | otherwise = R.CASE (head luts) rest
+  where
+    app' = force app
+    --app' = app {- PV STACK -}
+    luts = map (indexOf p) $ map getAlts $ filter isAlts app'
+    rest = map (tr p d) $ filter (not . isAlts) app'
+
+force app@[Prim p,y,Int _] = Fun "!force0" : app
+force app@[Prim p,Int i,y] = Fun "!force1" : app
+force app
+  | isPrimitiveApp app = Fun "!force01" : app
+  | otherwise = app
+
+indexOf p f =
+  case [i | ((g, args, rhs), i) <- zip p [0..], f == g] of
+    [] -> error "RedCompile: indexOf"
+    i:_ -> i
+
+isNormal (R.CON n c:rest) = length rest <= n
+isNormal (R.FUN b n f:rest) = length rest < n
+isNormal _ = False
+
+tr p d (Int i) = R.INT i
+tr p d (Prim f) = R.PRI 2 f
+tr p d (Fun f) =
+  case xs of
+    [] -> R.PRI 2 f
+    (i, args):_ -> R.FUN False (length args) i
+  where xs = [(i, args) | ((g, args, rhs), i) <- zip p [0..], f == g]
+tr p (f, args, spine, body) (Var v) =
+  case v `elemIndex` args of
+    Nothing -> R.VAR shared idx
+    Just i -> R.ARG shared i
+  where
+    shared = (length $ filter (== v)
+                     $ concatMap (concatMap vars) (spine : map snd body)) > 1
+    idx = case [i | ((w, _), i) <- zip body [0..], v == w] of
+            [] -> error ("Unbound variable: " ++ v)
+            i:_ -> i
+tr p d (Ctr c n i) = R.CON n i
+tr p d Bottom = R.INT 0
+
+-- Set boolean 'original' flag on funtions; if true, function was
+-- originally defined, and if false, function was introduced in
+-- Reduceron compilation process.
+
+flagFuns :: Int -> R.Prog -> R.Prog
+flagFuns i p = map flag p
+  where
+    flag (f, pop, luts, push, apps) =
+      (f, pop, luts, map fl push, map (mapAtoms fl) apps)
+    fl (R.FUN _ n f) = R.FUN (f < i) n f
+    fl a = a
+
+-- Fragment a program such that: (1) each template contains at most
+-- 'n' applications; (2) each template contains at most 'm' LUTs; (3)
+-- each template pushes a maximum of 'm' atoms; (4) if a template
+-- pushes more than one atom, then it contains at most 'n-1'
+-- applications; (5) the first atom pushed by the final template does
+-- not refer to any of that template's applications (the 'refers
+-- check').
+
+fragment :: Int -> Int -> R.Prog -> R.Prog
+fragment n m p = flagFuns (length p) (p' ++ ts')
+  where
+    (_, ts, p') = runWS (mapM (frag n m) p) (length p)
+    ts' = map snd (sortBy cmp ts)
+    cmp (a, b) (c, d) = compare a c
+
+sub n m = m-n
+
+frag n m (f, pop, luts, push, apps)
+  | length apps >= n || any isPRIM apps = fr n m (f, pop, luts, push, apps)
+  | length luts > m =
+      do x <- newId
+         t <- frag n m (f, pop, dropBack m luts, push, apps)
+         write (x, t)
+         return (f, 0, takeBack m luts, [R.FUN False 0 x], [])
+  | refersCheck (head push) = fr n m (f, pop, luts, push, apps)
+  | otherwise = return (f, pop, luts, push, apps)
+
+fr n m (f, pop, luts, push, apps) =
+  do x <- newId
+     let offset = length (take n apps0)
+     let apps' = map (relocate (sub offset)) (drop n apps0 ++ apps1)
+     let push' = map (reloc (sub offset)) push
+     t <- frag n m (f, pop, dropBack m luts, push', apps')
+     write (x, t)
+     return (f, 0, takeBack m luts, [R.FUN False 0 x], take n apps0)
+  where
+    (apps0, apps1) = splitPredexes apps
+
+relocate f app = mapAtoms (reloc f) app
+
+reloc f (R.VAR sh i) = R.VAR sh (f i)
+reloc f x = x
+
+refersCheck (R.VAR sh i) = i >= 0
+refersCheck _ = False
+
+-- Top-level compilation
+
+redCompile :: InlineFlag -> Int -> Int -> Int -> Int -> Int -> Prog -> R.Prog
+redCompile i slen alen napps nluts nregs =
+  fragment napps nluts . translate i alen slen nregs
+
+-- Auxiliary functions
+
+takeBack n xs = reverse $ take n $ reverse xs
+
+dropBack n xs = reverse $ drop n $ reverse xs
+
+getVar :: Exp -> String
+getVar (Var v) = v
+
+vars :: Exp -> [Id]
+vars (Var v) = [v]
+vars e = []
+
+isAlts :: Exp -> Bool
+isAlts (Alts fs n) = True
+isAlts e = False
+
+getAlts :: Exp -> Id
+getAlts (Alts fs n)
+  | null fs = error "RedCompile: getAlts"
+  | otherwise = head fs
+
+lift f p = xs ++ ys
+  where (xs, ys) = partition (\(g, _, _) -> f == g) p
+
+type Bind a = WriterState (Id, [Exp]) Int a
+
+freshId :: Bind Id
+freshId = do n <- get ; set (n+1) ; return ("new_bind_" ++ show n)
+
+type Define a = WriterState (Int, R.Template) Int a
+
+newId :: Define Int
+newId = do n <- get ; set (n+1) ; return n
diff --git a/Flite/RedFrontend.hs b/Flite/RedFrontend.hs
new file mode 100644
--- /dev/null
+++ b/Flite/RedFrontend.hs
@@ -0,0 +1,46 @@
+module Flite.RedFrontend (frontend) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.ConcatApp
+import Flite.Matching
+import Flite.Case
+import Flite.Let
+import Flite.Identify
+import Flite.Strictify
+import Flite.Inline
+import Flite.Predex
+import Flite.Fresh
+import Control.Monad
+import Flite.Pretty
+
+frontend :: Int -> InlineFlag -> Prog -> Prog
+frontend nregs i p = snd (runFresh (frontendM nregs i p) "$" 0)
+
+concApps :: Int -> Prog -> Prog
+concApps 0 = concatApps
+concApps nregs = concatNonPrims
+
+frontendM :: Int -> InlineFlag -> Prog -> Fresh Prog
+frontendM nregs i p =
+      return (identifyFuncs p)
+  >>= desugarCase
+  >>= desugarEqn
+  >>= inlineLinearLet
+  >>= inlineSimpleLet
+  >>= return . concApps nregs
+  >>= inlineTop i
+  >>= return . concApps nregs
+ >>= inlineLinearLet
+ >>= inlineSimpleLet
+ >>= return . concApps nregs 
+ -- >>= return . forceAndRebind
+                  --  >>= return . identifyPredexCandidates nregs
+  >>= return . caseElimWithCaseStack
+  >>= inlineTop i
+  >>= return . concApps nregs
+  >>= return . identifyPredexCandidates nregs
+  >>= return . concatApps
+  >>= return . strictifyPrim
+  >>= return . concatApps
+--  >>= \p -> trace (pretty p) (return p)
diff --git a/Flite/RedSyntax.hs b/Flite/RedSyntax.hs
new file mode 100644
--- /dev/null
+++ b/Flite/RedSyntax.hs
@@ -0,0 +1,32 @@
+module Flite.RedSyntax where
+
+type Id = Int
+
+type Arity = Int
+
+type Index = Int
+
+type Shared = Bool
+
+data Atom =
+    INT Int
+  | ARG Shared Int
+  | VAR Shared Int
+  | REG Shared Int
+  | CON Arity Index
+  | FUN Bool Arity Id
+  | PRI Arity String
+  deriving (Show, Read)
+
+type Normal = Bool
+
+type RegId = Int
+
+data App = APP Normal [Atom] | CASE Id [Atom] | PRIM RegId [Atom]
+  deriving (Show, Read)
+
+type LUT = Int
+
+type Template = (String, Int, [LUT], [Atom], [App])
+
+type Prog = [Template]
diff --git a/Flite/State.hs b/Flite/State.hs
new file mode 100644
--- /dev/null
+++ b/Flite/State.hs
@@ -0,0 +1,8 @@
+module Flite.State where
+
+newtype State s a = S { runState :: s -> (s, a) }
+
+instance Monad (State s) where
+  return a = S (\s -> (s, a))
+  m >>= f = S (\s -> case runState m s of
+                       (s', a) -> runState (f a) s')
diff --git a/Flite/Strictify.hs b/Flite/Strictify.hs
new file mode 100644
--- /dev/null
+++ b/Flite/Strictify.hs
@@ -0,0 +1,190 @@
+module Flite.Strictify
+  ( strictifyPrim
+  , strictifyPrimWithPVStack
+  , forceAndRebind
+  ) where
+
+import Flite.Syntax
+import Flite.Traversals
+import Flite.Descend
+import Flite.CallGraph
+import Data.List
+import Flite.LambdaLift
+
+isInt (Int i) = True
+isInt _ = False
+
+mkApp f [] = f
+mkApp (App f es) fs = App f (es ++ fs)
+mkApp f es = App f es
+
+primSatErrMsg :: String
+primSatErrMsg = "Applications of primitives must be saturated"
+
+-- Makes sure that arguments to primitive functions are forced before
+-- the primitive is applied.
+strictifyPrim :: Prog -> Prog
+strictifyPrim = onExp prim
+  where
+    prim (App (Fun f) (a:rest))
+      | isUnaryPrim f = mkApp result (map prim rest)
+      where a' = prim a
+            result = case isInt a' of
+                       False -> App a' [Fun f]
+                       True  -> App (Fun f) [a']
+    prim (App (Fun f) (a:b:rest))
+      | isBinaryPrim f = mkApp result (map prim rest)
+      where (a', b') = (prim a, prim b)
+            result = case (isInt a', isInt b') of
+                       (False, False) -> App b' [App a' [Fun f]]
+                       (False, True ) -> App a' [Fun f, b']
+                       (True , False) -> App b' [App (Fun f) [a']]
+                       (True , True ) -> App (Fun f) [a', b']
+    prim (App (Fun f) es)
+      | isUnaryPrim f || isBinaryPrim f = error primSatErrMsg
+    prim (Fun f)
+      | isUnaryPrim f || isBinaryPrim f = error primSatErrMsg
+    prim e = descend prim e
+
+-- Same as above, except assuming that reduction machine has a
+-- special primitive-value (PV) stack available.
+strictifyPrimWithPVStack :: Prog -> Prog
+strictifyPrimWithPVStack = onExp prim
+  where
+    prim (App (Fun f) (a:rest))
+      | isUnaryPrim f = mkApp result (map prim rest)
+      where a' = prim a
+            result = catApp [a', Fun f]
+    prim (App (Fun f) (a:b:rest))
+      | isBinaryPrim f = mkApp result (map prim rest)
+      where (a', b') = (prim a, prim b)
+            result = catApp [b', a', Fun f]
+    prim (App (Fun f) es)
+      | isUnaryPrim f || isBinaryPrim f = error primSatErrMsg
+    prim (Fun f)
+      | isUnaryPrim f || isBinaryPrim f = error primSatErrMsg
+    prim e = descend prim e
+
+catApp :: [Exp] -> Exp
+catApp es = App x xs
+  where
+    x:xs = concatMap contents es
+    contents (App e es) = e:es
+    contents e = [e]
+
+{-
+
+Attempts to rebind strictly-needed variables (of type integer) so
+their evaluated forms can be viewed as unboxed integers.  The aim is
+to increase the scope of PRS.  The transformation proceeds as follows:
+
+STEP 1. Look for functions of the form
+
+  f ... = ... case p e1 e2 of { False -> alt1 ; True -> alt2 } ...
+
+where p is a primitive function strict in both arguments returning a
+boolean, and alt1 or alt2 can lead to another call of f.
+
+STEP 2. Take all the variables of type integer referred to in e1 or e2
+that also referred to in alt1 or alt2.  Call them v1..vn.  Proceed
+only if v1..vn is non-empty.
+
+STEP 3. Abstract the expression of interest into a function h:
+
+  f ... = ... h v1..vn w1..wn ...
+
+  h v1..vn w1..wn = case p e1 e2 of { False -> alt1 ; True -> alt2 };
+
+where w1..wn are the free variables, other than v1..vn, in the
+case expression.
+
+STEP 4. Create function f' like f but which forces evaluation of
+v1..vn before applying h:
+
+  f' ... = ... vn (..(v1 h)) w1..wn ...
+
+STEP 5. Now calls to f can be replaced by calls to f'.  However, as
+primed functions are meant to be wrappers, only calls to f which occur
+in a function that is NOT call-reachable from f should be replaced.
+
+-}
+
+forceAndRebind :: Prog -> Prog
+forceAndRebind p = map (wrap cg wrapperIds) p ++ wrappers
+  where
+    cg = callReachableGraph p
+    wrappers = lambdaLift $ concatMap (makeWrapper cg) p
+    wrapperIds = map funcName wrappers
+
+wrap :: CallGraph -> [Id] -> Decl -> Decl
+wrap cg ws (Func f args rhs) = Func f args (wrapExp f cg ws rhs)
+
+wrapExp :: Id -> CallGraph -> [Id] -> Exp -> Exp
+wrapExp f cg ws (Fun g)
+  | g' `elem` ws && f `notElem` reachable cg g = Fun g'
+  | otherwise = Fun g
+  where g' = g ++ "_W"
+wrapExp f cg ws e = descend (wrapExp f cg ws) e
+
+makeWrapper :: CallGraph -> Decl -> [Decl]
+makeWrapper cg (Func f args rhs)
+  | rhs == rhs' = []
+  | otherwise = [Func f' args rhs']
+  where
+    rhs' = abstract f cg rhs
+    f' = f ++ "_W"
+
+neededVars :: Exp -> [Id]
+neededVars (App (Fun p) es)
+  | isPrimId p = concatMap neededVars es
+neededVars (Var v) = [v]
+neededVars _ = []
+
+{-
+abstract :: Id -> CallGraph -> Exp -> Exp
+abstract f cg (Case subject@(App (Fun p) es) as)
+  | isPrimId p
+ && not (null vs)
+ && recursive = force (reverse vs) (Lam vs (Case (App (Fun p) es) as'))
+  where
+    nvs = neededVars subject
+    fvs = filter (`elem` nvs) $ concatMap (freeVars . snd) as
+    vs = dups (nvs ++ fvs)
+    recursive = f `elem` concatMap (reachable cg)
+                  (concatMap calls (subject:map snd as))
+    as' = [(p, abstract f cg e) | (p, e) <- as]
+abstract f cg e = descend (abstract f cg) e
+
+force :: [Id] -> Exp -> Exp
+force [] e = e
+force (v:vs) e = App (Var v) [force vs e]
+-}
+
+abstract :: Id -> CallGraph -> Exp -> Exp
+abstract f cg (Case subject@(App (Fun p) es) as)
+  | isPrimId p
+ && not (null vs)
+ && recursive = 
+  App (force (reverse vs) (Lam (vs ++ ws) (Case (App (Fun p) es) as')))
+      (map Var ws)
+  where
+    nvs = neededVars subject
+    fvs = filter (`elem` nvs) $ concatMap (freeVars . snd) as
+    vs = dups (nvs ++ fvs)
+    recursive = f `elem` concatMap (reachable cg)
+                  (concatMap calls (subject:map snd as))
+    as' = [(p, abstract f cg e) | (p, e) <- as]
+    ws = filter (`notElem` vs) $ nub $ concatMap freeVars $ (es ++ map snd as)
+abstract f cg e = descend (abstract f cg) e
+
+force :: [Id] -> Exp -> Exp
+force [] e = e
+force (v:vs) e = App (Var v) [force vs e]
+
+
+-- Return elements that occur more than once
+dups :: Eq a => [a] -> [a]
+dups [] = []
+dups (x:xs)
+  | x `elem` xs = x : dups (filter (/= x) xs)
+  | otherwise = dups xs
diff --git a/Flite/WriterState.hs b/Flite/WriterState.hs
new file mode 100644
--- /dev/null
+++ b/Flite/WriterState.hs
@@ -0,0 +1,24 @@
+module Flite.WriterState where
+
+import Control.Monad
+
+newtype WriterState w s a = WS { runWS :: s -> (s, [w], a) }
+
+instance Monad (WriterState w s) where
+  return a = WS $ \s -> (s, [], a)
+  m >>= f = WS $ \s -> let (s0, w0, a) = runWS m s
+                           (s1, w1, b) = runWS (f a) s0
+                       in  (s1, w0 ++ w1, b)
+
+
+instance Functor (WriterState w s) where
+  fmap = liftM
+
+write :: w -> WriterState w s ()
+write w = WS $ \s -> (s, [w], ())
+
+get :: WriterState w s s
+get = WS $ \s -> (s, [], s)
+
+set :: s -> WriterState w s ()
+set s = WS $ \_ -> (s, [], ())
diff --git a/flite.cabal b/flite.cabal
--- a/flite.cabal
+++ b/flite.cabal
@@ -1,5 +1,5 @@
 Name:               flite
-Version:            0.1
+Version:            0.1.1
 Synopsis:           f-lite compiler, interpreter and libraries
 License:            BSD3
 License-file:       LICENSE
@@ -13,7 +13,7 @@
                     definitions, pattern matching, limited let expressions, function applications and
                     constructor applications expressed in the explicit 'braces' layout-insensitive format.
                     
-                    See README for more information.
+                    See README for more information. Example flite programs included in source distribution.
 Category:           Compiler
 Extra-Source-Files: README examples/*.hs
 
@@ -23,6 +23,14 @@
 
 Executable flite-pure
     Main-is:       fl-pure.hs
+    Other-Modules:  Flite.CallGraph, Flite.Case, Flite.Compile, Flite.CompileBackend
+                    Flite.CompileFrontend, Flite.ConcatApp, Flite.Descend, Flite.Flatten, 
+                    Flite.Flite, Flite.Fresh, Flite.Identify, Flite.Identity, Flite.Inline, 
+                    Flite.Interp, Flite.InterpFrontend, Flite.LambdaLift, Flite.Let, 
+                    Flite.Matching, Flite.Parse, Flite.ParseLib, Flite.Predex, Flite.Pretty,
+                    Flite.RedCompile, Flite.RedFrontend, Flite.RedSyntax,
+                    Flite.State, Flite.Strictify, Flite.Syntax, Flite.Traversals, Flite.Writer,
+                    Flite.Writer, Flite.WriterState
     if flag(pure)
         Build-Depends: base >= 3 && < 5, haskell98 >= 1 && < 2,
                        array >= 0 && < 1, containers >= 0 && < 1
@@ -37,6 +45,14 @@
         Build-Depends: base >= 3 && < 5, haskell98 >= 1 && < 2,
                        array >= 0 && < 1, containers >= 0 && < 1,
                        parsec >= 2.1.0.1 && < 3
+        Other-Modules:  Flite.CallGraph, Flite.Case, Flite.Compile, Flite.CompileBackend
+                        Flite.CompileFrontend, Flite.ConcatApp, Flite.Descend, Flite.Flatten, 
+                        Flite.Fresh, Flite.Identify, Flite.Identity, Flite.Inline, Flite.Interp, 
+                        Flite.InterpFrontend, Flite.LambdaLift, Flite.Let, Flite.Matching, 
+                        Flite.Predex, Flite.Pretty, Flite.RedCompile, Flite.RedFrontend, 
+                        Flite.RedSyntax, Flite.State, Flite.Strictify, Flite.Syntax, 
+                        Flite.Traversals, Flite.Writer, Flite.Writer, Flite.WriterState,
+                        Flite.Parsec.Parse, Flite.Parsec.Flite
     
 Library
     Build-Depends:   base >= 3 && < 5, haskell98 >= 1 && < 2,
@@ -47,3 +63,8 @@
                      Flite.Inline, Flite.Let, Flite.Matching, Flite.Pretty,
                      Flite.Syntax, Flite.Traversals, Flite.Writer,
                      Flite.Parsec.Parse
+    Other-Modules:  Flite.Compile, Flite.CompileBackend
+                    Flite.CompileFrontend, Flite.Flatten, Flite.Interp,
+                    Flite.InterpFrontend, Flite.LambdaLift, Flite.Predex, 
+                    Flite.RedCompile, Flite.RedFrontend, Flite.RedSyntax,
+                    Flite.State, Flite.Strictify, Flite.WriterState