diff --git a/Optimus/CallGraph.hs b/Optimus/CallGraph.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/CallGraph.hs
@@ -0,0 +1,149 @@
+module Optimus.CallGraph where
+	import Flite.Pretty
+	import Flite.Syntax
+	import Flite.Traversals
+	import Optimus.Uniplate
+	import Optimus.Util
+	
+	import Control.Monad
+	import Control.Monad.Fix
+	import Control.Monad.State
+	import qualified Data.Map as Map
+	import qualified Data.Set as Set
+	import Data.Generics.Uniplate
+	import Data.Graph.Inductive.Graph
+	import Data.Graph.Inductive.PatriciaTree
+	import Data.GraphViz hiding (Int)
+	import Data.List
+	import Data.Maybe
+	import Debug.Trace
+	
+	callGraph :: Prog -> Gr Id Id
+	callGraph p = mkGraph (zip [1..] nodes) edges
+		where
+			nodes = nub $ [ f | Func f _ _ <- p ]
+			lookupNodes = flip lookup (zip nodes [1..])
+			edges = nub . catMaybes $ [ liftM2 (\x y -> (x, y, "")) (lookupNodes f) (lookupNodes g) | Func f _ r <- p, Fun g <- universe r ]
+	
+	conGraph :: Prog -> Gr Id [Id]
+	conGraph p = mkGraph (zip [1..] nodes) edges
+		where
+			nodes = nub $ [ f | Func f _ _ <- p ]
+			lookupNodes = flip lookup (zip nodes [1..])
+			edges = nub . catMaybes $ [ liftM2 (\x y -> (x, y, consUsed r)) (lookupNodes f) (lookupNodes g) | Func f _ r <- p, Fun g <- universe r ]
+			consUsed e = nub $ [ c | Con c <- universe e ] ++ [ c | Case _ as <- universe e, (p', _) <- as, Con c <- universe p' ]
+	
+	produceDot :: (Graph gr, Show b) => gr Id b -> String
+	produceDot g = printDotGraph $ graphToDot True g [] labelNode labelEdge
+		where
+			labelNode (_, l) = [Label (StrLabel l), Color [ColorName $ if words l !! 0 `elem` primitives then "black" else "red"]]
+			labelEdge (_, _, l) = if show l == "\"\"" then [] else [Label (StrLabel $ show l)]
+			
+	-----------------------
+	
+	arityGraph :: Prog -> Gr Id Id
+	arityGraph p = mkGraph (zip [1..] nodes) edges
+		where
+			nodes = nub $ [ f | Func f _ _ <- p ]
+			lookupNodes = flip lookup (zip nodes [1..])
+			arities = [ (f, length a) | Func f a _ <- p ] ++ map (flip (,) 2) primitives
+			arity f = fromMaybe (error "Missing function definition") $ lookup f arities
+			edges = nub . catMaybes $ [ liftM2 (\x y -> (x, y, "")) (lookupNodes f) (lookupNodes g) | Func f _ r <- p, App (Fun g) ys <- universe r, arity f <= length ys ]
+	
+	hofGraph :: Prog -> Gr Id Id
+	hofGraph p = mkGraph (zip [1..] nodes) edges
+		where
+			nodes = nub $ [ f | Func f _ _ <- p ]
+						 ++ [ concat $ intersperse " " $ g : [ if hof e then showArg e else "_" | e <- ys ]
+							| Func f _ r <- p, App (Fun g) ys <- universe r, arity f <= length ys, any hof ys ]
+			lookupNodes = flip lookup (zip nodes [1..])
+			arities = [ (f, length a) | Func f a _ <- p ] ++ map (flip (,) 2) primitives
+			arity f = fromMaybe (error "Missing function definition") $ lookup f arities
+			edges = nub . catMaybes $ [ if any hof ys then Nothing else Just ()
+										>> liftM2 (\x y -> (x, y, "")) (lookupNodes f) (lookupNodes g)
+										| Func f _ r <- p, App (Fun g) ys <- universe r, arity f <= length ys ]
+			hof (App (Fun f) ys) = arity f > length ys
+			hof (Fun f) = arity f > 0
+			hof _ = False
+	
+	data TravArcType = Call | Composition
+	
+	travGraph :: Prog -> Gr Id TravArcType
+	travGraph p = mkGraph (zip [1..] nodes) edges
+		where
+			edgesRaw = trav p
+			nodes = nub . uncurry (++) . (\(_, x, y) -> (x, y)) . unzip3 $ edgesRaw
+			lookupNodes = fromJust . flip lookup (zip nodes [1..])
+			edges = [ (lookupNodes f, lookupNodes g, t) | (t@(Call), f, g) <- edgesRaw ]
+	
+	produceDotTrav :: Gr Id TravArcType -> String
+	produceDotTrav g = printDotGraph $ graphToDot True g [] labelNode labelEdge
+		where
+			labelNode (_, l) = [Label (StrLabel l)] ++ if words l !! 0 `elem` primitives then [Style [SItem Dotted []]] else []
+			labelEdge (_, _, t) = case t of { Call -> [] ; Composition -> [Style [SItem Dashed []], ArrowHead emptyArr] }
+	
+	trav :: Prog -> [(TravArcType, Id, Id)]
+	trav p = fst $ execState (t [] "main" (body "main")) ([], [])
+		where
+			m = byFuncName (p ++ [ Func f [Var "_", Var "_"] Bottom | f <- primitives ])
+			body f = fromMaybe (error "Missing function definition") $ Map.lookup f m >>= return . funcRhs
+			arity = length . args
+			args f = fromMaybe (error "Missing function definition") $ Map.lookup f m >>= return . concatMap patVars . funcArgs
+			unsat (App (Fun f) ys) = arity f > length ys
+			unsat (Fun f) = arity f > 0
+			unsat _ = False
+			t :: [(Id, Exp)] -> Id -> Exp -> State ([(TravArcType, Id, Id)], [Id]) Exp
+			t env f (App (App x ys) zs) = t env f (App x $ ys ++ zs)
+			t env f (Var v) = return $ fromMaybe (Con "") $ lookup v env
+			t env f (App (Fun g) ys) | arity g <= length ys = do
+										(oldEdges, oldNames) <- get
+										put (oldEdges, [])
+										bs <- sequence [ t env f e >>= \e' -> return $ if unsat e' then Just (v, e') else Nothing | (v, e) <- zip (args g) ys ]
+										g' <- return . concat . intersperse " " $ g : (map (\x -> fromMaybe "_" (return . show . snd =<< x)) $ bs)
+										(newEdges, newNames) <- get
+										put ((Call, f, g'): map ((,,) Composition g') newNames ++ newEdges, [])
+										e' <- if g' `notElem` [ x | (Call, _, x) <- newEdges]
+											then t (catMaybes bs) g' (body g)
+											else return Bottom
+										(newerEdges, _) <- get
+										put (newerEdges, g':oldNames)
+										return e'
+			t env f (App x ys) = do
+							x' <- t env f x
+							if x' == x || x' == Bottom then mapM (t env f) ys >>= return . App x' else t env f (App x' ys)
+			t env f (Let bs x) = do
+							bs' <- sequence [ liftM ((,) v) (t env f e) | (v, e) <- bs ]
+							t (bs ++ env) f x
+			t env f (Case x as) = do
+							x <- t env f x
+							ys <- sequence [ t (map (flip (,) Bottom) (patVars p) ++ env) f y | (p, y) <- as ]
+							return $ head (ys ++ [x])
+			t env f e = return e
+	
+	selectFuncs n p = nub $ selectFuncs2 n p ++ ["main"]
+	
+	selectFuncs1 :: Prog -> [Id]
+	selectFuncs1 p = (evalState (traverse "main") Set.empty)
+		where
+			m = byFuncName p
+			body f = fromMaybe Bottom (Map.lookup f m >>= return . funcRhs)
+			traverse :: Id -> State (Set.Set Id) [Id]
+			traverse f = let
+				cs = filter (flip notElem $ f : primitives) . calls . body $ f
+				csSet = Set.fromList cs in do
+					visited <- get
+					put $ csSet `Set.union` visited
+					rest <- mapM traverse . Set.toList $ csSet `Set.difference` visited
+					return $ if length cs > 1 then concat rest ++ [f] else concat rest
+					
+	selectFuncs2 :: Int -> Prog -> [Id]
+	selectFuncs2 n p = take n [ f | (f, n) <- selected, n >= limit ]
+		where
+			selected :: [(Id, Int)]
+			selected = map (\f -> maybe (f, -1) ((,) f) $ lookup f call_count) $ selectFuncs1 p
+			call_count :: [(Id, Int)]
+			call_count = map (\xs@(x:_) -> (x, length xs)) . group . sort . concatMap (calls . funcRhs) $ p
+			limit :: Int
+			limit | length selected > n = (reverse . sort . map snd $ selected) !! n
+				  | otherwise			= 0
+	
diff --git a/Optimus/Generalise.hs b/Optimus/Generalise.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Generalise.hs
@@ -0,0 +1,84 @@
+module Optimus.Generalise where
+	import Flite.Fresh
+	import Flite.Syntax
+	import Flite.Traversals
+	import Optimus.Homeo
+	import Optimus.Trace
+	import Optimus.Uniplate
+	
+	import Control.Monad
+	import Data.Generics.Uniplate
+	import Data.List
+	import Data.Maybe
+
+	type GenBinding = (GenFlag, Id, Exp)
+	data GenFlag 	= Safe | Unsafe
+		deriving Show
+
+	generalise :: Exp -> Exp -> Fresh Exp
+	generalise s t 	| couple t s = do
+			v <- fresh
+			(x', bind, _) <- msg (Var v, [(v, s)], [(v, t)])
+			return $ Let bind x'
+					| otherwise = return s
+		where
+			msg :: (Exp, [Binding], [Binding]) -> Fresh (Exp, [Binding], [Binding])
+			msg m					| null vsts	= return m
+									| otherwise	= do
+										ys <- mapM (const fresh) ss 
+										msg (subst (y_ $ map Var ys) v tg, th0' ++ zip ys ss, th1' ++ zip ys ts)
+				where
+					vsts = [ (v, s, t) | (v, s) <- th0, (w, t) <- th1, v == w, s =~ t ]
+					th0' = [ b | b@(v', _) <- th0, v /= v' ]
+					th1' = [ b | b@(w', _) <- th1, v /= w' ]
+					(v, s, t) = head vsts
+					(ss, y_) = uniplate s
+					ts = children t
+					(tg, th0, th1) = t_G (show m) m
+					
+	generalise1 :: Exp -> Exp -> Fresh Exp
+	generalise1 s t	| couple t s = do
+			v <- fresh
+			(x', bind, _) <- msg (Var v, [(Safe, v, s)], [(v, t)])
+			return $ case null [ undefined | (Safe, _, _) <- bind ] of
+						True 	-> s
+						False 	-> Let [ (v, y) | (Safe, v, y) <- bind ] (substMany x' [ (y, v) | (Unsafe, v, y) <- bind ])
+					| otherwise = return s
+		where
+			msg :: (Exp, [GenBinding], [Binding]) -> Fresh (Exp, [GenBinding], [Binding])
+			msg m					| null vsts	= return m
+									| otherwise	= do
+										ys <- mapM (const fresh) ss 
+										msg (subst (y_ $ map Var ys) v tg, th0' ++ zip3 sFlags ys ss, th1' ++ zip ys ts)
+				where
+					vsts = [ (v, s, t) | (_, v, s) <- th0, (w, t) <- th1, v == w, s =~ t ]
+					th0' = [ gb | gb@(_, v', _) <- th0, v /= v' ]
+					th1' = [ b | b@(w', _) <- th1, v /= w' ]
+					(v, s, t) = head vsts
+					(ss, y_) = uniplate s
+					ts = children t
+					sFlags = map flag (zipWith inaccessibleVars ss (map (\ms -> subst (y_ ms) v tg) (markers ss)))
+					(tg, th0, th1) = t_G (show m) m
+					flag xs | null xs	= Safe
+							| otherwise	= Unsafe
+	
+	markers :: [a] -> [[Exp]]
+	markers [] = []
+	markers xs = nub . permutations $ Var "%" : replicate (length xs - 1) (Var "")
+	
+	inaccessibleVars :: Exp -> Exp -> [Id]
+	inaccessibleVars x y = freeVars x `intersect` bindingsAtMarker y
+	
+	bindingsAtContext :: (Exp -> Exp) -> [Id]
+	bindingsAtContext ctx = bindingsAtMarker (ctx $ Var "%")
+	
+	bindingsAtMarker :: Exp -> [Id]
+	bindingsAtMarker x	| isJust vs	= nub . fromJust $ vs
+						| otherwise	= error "Never reached marker."
+		where
+			vs = f x
+			f e@(Var "%")	= Just []
+			f e@(Let bs _) 	= (listToMaybe . catMaybes . map f) (children e) >>= return . (++) (map fst bs)
+			f e@(Case _ as)	= (listToMaybe . catMaybes . zipWith (\p x -> x >>= (return . (++) p)) ([] : map (patVars . fst) as) . map f) (children e)
+			f e@(App _ _)	= (listToMaybe . catMaybes . map f) (children e)
+			f _				= Nothing
diff --git a/Optimus/Homeo.hs b/Optimus/Homeo.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Homeo.hs
@@ -0,0 +1,42 @@
+module Optimus.Homeo where
+	import Flite.Syntax
+	import Optimus.Uniplate
+	
+	import Data.Generics.Uniplate
+	
+	(<||) :: Exp -> Exp -> Bool
+	x <|| y = dive x y || couple x y
+	
+	dive :: Exp -> Exp -> Bool
+	dive x y = any (x <||) (children y)
+	
+	couple :: Exp -> Exp -> Bool
+	couple x y 	= x =~ y && length x_ == length y_
+				&& and (zipWith (<||) x_ y_)
+		where
+			x_ = children x
+			y_ = children y
+			
+	-- Must alpha first
+	(=~) :: Exp -> Exp -> Bool
+	(Bottom) =~ (Bottom) = True
+	(Int i) =~ (Int j) = i == j
+	(Fun f) =~ (Fun h) = f == h
+	(Con c) =~ (Con d) = c == d
+	(Var _) =~ (Var _) = True
+	(App _ xs) =~ (App _ ys) = length xs == length ys
+	(Let bs_x _) =~ (Let bs_y _) = length bs_x == length bs_y
+								-- && and (zipFst (==) bs_x bs_y)
+	(Case _ alts_x) =~ (Case _ alts_y) = length alts_x == length alts_y
+								--	&& and (zipFst (==~) alts_x alts_y)
+	_ =~ _ = False
+										
+	(==~) :: Exp -> Exp -> Bool
+	(App _ xs) ==~ (App _ ys) = length xs == length ys
+							&& and (zipWith (==~) xs ys)
+	(Con c) ==~ (Con d) = c == d
+	(Var v) ==~ (Var w) = v == w
+	_ ==~ _ = False
+	
+	zipFst :: (a -> b -> c) -> [(a, d)] -> [(b, e)] -> [c]
+	zipFst f = zipWith (\(x, _) (y, _) -> f x y)
diff --git a/Optimus/Inline.hs b/Optimus/Inline.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Inline.hs
@@ -0,0 +1,78 @@
+-- |Handles the inlining of single function applications and inlining
+-- residuals through a whole program
+module Optimus.Inline (
+			maybeInline,
+			progInline
+		) where
+	import Control.Monad
+	import Data.List
+	import qualified Data.Map as Map
+	import qualified Data.Set as Set
+	import Data.Maybe
+
+	import Flite.Fresh
+	import Flite.Syntax
+	import Flite.Traversals
+	
+	import Optimus.Uniplate
+	import Optimus.Util
+	
+	-- |Build an inlined form of a saturated function application given
+	-- the correct function definition. Assumes that equations have
+	-- been desugared. Simplify afterwards for efficiency.
+	maybeInline :: [Exp] -> Decl -> Maybe (Fresh Exp)
+	maybeInline ys (Func _ args rhs)
+		| length_args > length_ys = fail "Unsaturated application."
+		| otherwise = Just $ do
+				vs <- mapM (const fresh) args
+				let (bound, remaining) = splitAt (length args) ys
+				let rhs' = substMany rhs (zip (map Var vs) (concatMap patVars args))
+				return $ mkApp (mkLet (zip vs bound) rhs') remaining
+		where
+			length_ys = length ys
+			length_args = length args
+			
+	-- |Make an Application only if there are arguments.
+	mkApp :: Exp -> [Exp] -> Exp
+	mkApp x [] = x
+	mkApp x ys = App x ys
+	
+	-- |Make a Let only if there are bindings.
+	mkLet :: [Binding] -> Exp -> Exp
+	mkLet [] y = y
+	mkLet bs y = Let bs y
+			
+	-- |Inline all non-recursive function applications.
+	progInline :: Prog -> Fresh Prog
+	progInline p = progInline' (byFuncName p) p
+		where
+			callCounts = map (\xs@(x:_) -> (x, length xs)) . group . sort . concatMap (calls . funcRhs) $ p
+			highlyCalled = Set.fromList [ f | (f, n) <- callCounts, n > 10 ]
+			progInline' :: Map.Map Id Decl -> Prog -> Fresh Prog
+			progInline' m [] = return $ Map.elems m
+			progInline' m (d:ds) = do
+				d'@(Func f _ _) <- declInline (`Map.lookup` m) highlyCalled d
+				progInline' (Map.insert f d' m) ds
+	
+	-- |Given a mapping of function names to declarations, inline
+	-- all non-recursive function applications
+	declInline :: (Id -> Maybe Decl) -> Set.Set Id -> Decl -> Fresh Decl
+	declInline progmap base (Func f a r) = liftM (Func f a) (expInline (f `Set.insert` base) r)
+		where
+			-- |Given a trace of functions visited, inline all non-
+			-- recursive function applications.
+			expInline :: Set.Set Id -> Exp -> Fresh Exp
+			expInline fs (Fun f) | f `Set.notMember` fs && isJust inlined
+				= fromJust inlined >>= descendM (expInline $ f `Set.insert` fs)
+				where
+					inlined = progmap f >>= notRecursive >>= maybeInline []
+			expInline fs (App (Fun f) xs) | f `Set.notMember` fs && isJust inlined
+				= fromJust inlined >>= descendM (expInline $ f `Set.insert` fs)
+				where
+					inlined = progmap f >>= notRecursive >>= maybeInline xs
+			expInline fs e = descendM (expInline fs) e
+			
+	-- |Only return functions that are not immediately recursive.
+	notRecursive :: Decl -> Maybe Decl
+	notRecursive d@(Func f _ r) | f `elem` calls r 	= Nothing
+								| otherwise			= Just d
diff --git a/Optimus/Pretty.hs b/Optimus/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Pretty.hs
@@ -0,0 +1,49 @@
+module Optimus.Pretty where
+	import Flite.Syntax
+	import Text.PrettyPrint.Leijen
+	
+	putProg :: Prog -> IO ()
+	putProg = putDoc . braces . enclose line line . indent 2 . vsep . punctuate (semi <> line) . map pretty
+	
+	prettyProg :: Prog -> String
+	prettyProg = show . braces . enclose line line . indent 2 . vsep . punctuate (semi <> line) . map pretty
+	
+	instance Pretty Decl where
+		pretty (Func f a r) = nest 2 $ text f
+							<+> hsep (map prettyArg a)
+							</> char '='
+							<+> pretty r
+							
+	instance Pretty Exp where
+		pretty (App x ys) 	= hsep (pretty x : map prettyArg ys)
+		pretty (Case x as)	= nest 2 (text "case" </> prettyArg x)
+							</> nest 2 (text "of" </> prettyBlock prettyAlt as)
+		pretty (Let bs y)	= nest 2 (text "let" </> prettyBlock prettyBind bs)
+							</> nest 2 (text "in" </> prettyArg y)
+		pretty (Var v)		= text v
+		pretty (Fun f)		= text f
+		pretty (Con c)		= text c
+		pretty (Int i)		= int i
+		pretty (Bottom)		= text "_|_"
+	
+	prettyBlock :: (a -> Doc) -> [a] -> Doc
+	prettyBlock f = braces . enclose line line . vsep . punctuate semi . map f
+	
+	prettyAlt :: Alt -> Doc
+	prettyAlt (p, x) = nest 2 $ pretty p <+> text "->" </> pretty x
+	
+	prettyBind :: Binding -> Doc
+	prettyBind (v, x) = text v <+> text "=" <+> pretty x
+	
+	prettyArg :: Exp -> Doc
+	prettyArg (App e []) = prettyArg e
+	prettyArg e@(App _ _) = parens . pretty $ e
+	prettyArg e@(Case _ _) = parens . pretty $ e
+	prettyArg e@(Let _ _) = parens . pretty $ e
+	prettyArg e = pretty e
+	
+	instance Show Decl where
+		show = ('\n':) . show  . pretty
+		
+	instance Show Exp where
+		show = ('\n':) . show . pretty
diff --git a/Optimus/Simplify.hs b/Optimus/Simplify.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Simplify.hs
@@ -0,0 +1,134 @@
+module Optimus.Simplify where -- (simplify) where
+	import Flite.Syntax
+	import Flite.Traversals hiding (freshen)
+	import Flite.Descend
+	import Flite.Fresh
+	import Optimus.Util
+	import Data.List
+	import Data.Maybe
+	import Control.Monad
+	import Optimus.Trace
+	
+	-- Issues are going to be with additional Apps in places
+	
+	-- |Not traced as too common and simply.
+	stripApp :: Exp -> Exp
+	stripApp e@(App (Fun _) []) = e
+	stripApp (App x []) = stripApp x
+	stripApp e = descend stripApp e
+	
+	-- |Not traced as too common and simply.
+	appOfApp :: Exp -> Exp
+	appOfApp (App (App x xs) ys) = appOfApp $ App x (xs ++ ys)
+	appOfApp e = descend appOfApp e
+			
+	caseOfCons :: Exp -> Fresh Exp
+	caseOfCons (Case (App (Con c) xs) ps) | isJust y' = fromJust y' >>= (caseOfCons . t_S "caseOfCons")
+		where
+			y' = listToMaybe [ mapM (const fresh) vs' >>=
+							   \ws -> return $ Let (zip ws xs) (substMany y $ zipWith (\w v -> (Var w, v)) ws vs')
+							| ( App (Con c') vs , y ) <- ps, c == c', length xs == length vs, let vs' = concatMap patVars vs ]
+	caseOfCons (Case (Con c) ps) = caseOfCons $ Case (App (Con c) []) ps
+	caseOfCons e = descendM caseOfCons e
+			
+	appToCase :: Exp -> Fresh Exp
+	appToCase (App e@(Case _ _) zs) = do
+		Case x ps <- freshenMany e (concatMap freeVars zs)
+		appToCase $ t_S "appToCase" $ Case x [ (p, App y zs) | (p, y) <- ps ]
+	appToCase e = descendM appToCase e
+			
+	appToLet :: Exp -> Fresh Exp
+	appToLet (App e@(Let _ _) zs) = do
+		Let bs y <- freshenMany e (concatMap freeVars zs)
+		appToLet $ t_S "appToLet" $ Let bs (App y zs)
+	appToLet e = descendM appToLet e
+			
+	caseOfLet :: Exp -> Fresh Exp
+	caseOfLet (Case e@(Let _ _) as) = do
+		Let bs y <- freshenMany e $ concat [ freeVarsExcept (patVars p) x | (p, x) <- as ]
+		caseOfLet $ t_S "caseOfLet" $ Let bs (Case y as)
+	caseOfLet e = descendM caseOfLet e
+			
+	caseOfCase :: Exp -> Fresh Exp
+	caseOfCase (Case e@(Case _ _) as') = do
+		Case x as <- freshenMany e $ concat [ freeVarsExcept (freeVars p) y | (p, y) <- as' ]
+		caseOfCase $ t_S "caseOfCase" $ Case x [ (p, Case y as') | (p, y) <- as]
+	caseOfCase e = descendM caseOfCase e
+			
+	substituteVar :: Exp -> Fresh Exp
+	substituteVar e@(Case (Var v) as_) | v `elem` (freeVars $ Case Bottom as_) = do
+		Case _ as <- freshen e v
+		as' <- sequence [ liftM ((,) p) $ freshenMD y $ patVars p | (p, y) <- as ]
+		--freshenMany e $ v : concat [ patVars p | Case _ as' <- extract universe e, (p, _) <- as' ]
+		substituteVar $ t_S "substituteVar" $ Case (Var v) [ (p, subst p v y) | (p, y) <- as' ]
+	substituteVar e = descendM substituteVar e
+			
+	letInCase :: Exp -> Fresh Exp
+	letInCase (Let bs e@(Case y _)) | (not . null) safe_bs = do
+			Case _ as <- freshenMany e (v:freeVars x)
+			letInCase $ t_S "letInCase" $ Let rem_bs (Case y [ (p, Let [(v, x)] z) | (p, z) <- as ])
+		where
+			yFree = freeVars y
+			bsFrees = [ (v, freeVars x) | (v, x) <- bs ]
+			safe_bs = [ (v, x) | (v, x) <- bs, v `notElem` (yFree ++ concat [ ws | (w, ws) <- bsFrees, v /= w ]) ]
+			(v, x) = head safe_bs
+			rem_bs = [ (v', x') | (v', x') <- bs, v /= v' ]
+	letInCase e = descendM letInCase e
+			
+	inlineLet :: Exp -> Fresh Exp
+	inlineLet (Let bs y) | (not . null) safe_bs = do
+			y' <- freshenMD y $ freeVars x_i
+			inlineLet $ t_S "inlineLet" $ subst x_i v_i (Let rem_bs y')
+		where
+			(_, xs) = unzip bs
+			(v_i, x_i) = head safe_bs
+			rem_bs = [ b | b@(v_j, _) <- bs, v_j /= v_i ]
+			safe_bs = 	[ b |
+						  b@(v_j, x_j) <- bs
+						, v_j `notElem` freeVars x_j
+						, (sum . map (varRefs v_j)) (y:xs) <= 1 || isOk x_j ]
+			isOk (Var _) = True
+			isOk (Con _) = True
+			isOk (Int _) = True
+			isOk (Fun _) = True
+			isOk (App e []) = isOk e
+			isOk _ = False
+	inlineLet e = descendM inlineLet e
+			
+	splitLet :: Exp -> Fresh Exp
+	splitLet (Let bs y) | (not . null) safe_bs
+		= do
+			new_bs <- mapM build args
+			splitLet $ t_S "splitLet" $ subst (App (Con c) (map Var (fst . unzip $ new_bs))) v_i (Let (rem_bs ++ new_bs) y)
+		where
+			(v_i, App (Con c) args) = head safe_bs
+			rem_bs = [ b | b@(v_j, _) <- bs, v_j /= v_i ]
+			safe_bs = [ b | b@(v_j, x_j@(App (Con _) _)) <- bs, v_j `notElem` freeVars x_j ]
+			build x_j = fresh >>= \vF -> return (vF, x_j)
+	splitLet e = descendM splitLet e
+	
+	removeLet :: Exp -> Exp
+	removeLet (Let [] x) = descend removeLet x
+	removeLet e = descend removeLet e
+			
+	letInLet :: Exp -> Fresh Exp
+	letInLet (Let bs1 e@(Let _ _)) = do
+			Let bs2 x <- freshenMany e (concatMap (freeVars . snd) bs1 ++ map fst bs1)
+			letInLet $ t_S "letInLet" $ Let (bs1 ++ bs2) x
+	letInLet e = descendM letInLet e
+			
+	simplify :: Exp -> Fresh Exp
+	simplify p = do
+			p' <- (return . stripApp . appOfApp . removeLet) =<< appToCase =<< appToLet =<< caseOfLet =<< caseOfCons
+				=<< caseOfCase =<< substituteVar =<< letInCase
+				=<< inlineLet =<< letInLet =<< ( splitLet . appOfApp
+					. removeLet . stripApp ) p
+			if p == p' then return p else simplify p'
+	
+	simplifyInlines :: Exp -> Fresh Exp
+	simplifyInlines e = do
+		e' <- (return . removeLet <=< inlineLet <=< return . stripApp) e
+		if e == e' then return e else simplifyInlines e'
+		
+	simplifyProg :: Prog -> Fresh Prog
+	simplifyProg p = sequence [ return . Func f a =<< (\x -> t_S' (show x) (simplify x)) =<< simplifyInlines (t_S' ("Simplifying " ++ f) r) | Func f a r <- p]
diff --git a/Optimus/Strategy.hs b/Optimus/Strategy.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Strategy.hs
@@ -0,0 +1,185 @@
+module Optimus.Strategy where
+	import Control.Monad.Identity
+	import Control.Monad.State
+	import Data.Char
+	import Data.List
+	import qualified Data.Map as Map
+	import qualified Data.Set as Set
+	import Data.Maybe
+	import Optimus.Trace
+	
+	import Flite.Identify
+	import Flite.Fresh
+	--import Flite.Inline
+	--import Flite.Pretty
+	import Optimus.Pretty
+	import Flite.Syntax
+	import Flite.Traversals
+
+	import Optimus.Generalise
+	import Optimus.Homeo
+	import Optimus.Inline
+	import Optimus.Simplify
+	import Optimus.Uniplate
+	import Optimus.Util
+	
+	import Data.Generics.Uniplate
+	
+	--------------------------------------------------
+	--------------------------------------------------
+	reachable :: Prog -> Id -> Set.Set Id
+	reachable p = reachable' (Set.empty)
+		where
+			reachable' :: Set.Set Id -> Id -> Set.Set Id
+			reachable' fs f | f `Set.member` fs = fs
+							| otherwise			= foldl reachable' (f `Set.insert` fs) (reach f)
+			reach f = [ g | d <- lookupFuncs f p, g <- (calls . funcRhs) d ]
+			
+	onlyReachable :: Prog -> Id -> Prog
+	onlyReachable p f = [ d | d <- p, funcName d `Set.member` reachable p f ]
+	
+	supercompileFunc :: String -> Prog -> Prog
+	supercompileFunc f_ p_ = onlyReachable p'' f_ ++ [ d | d@(Func f _ _) <- p, f /= f_ ]
+		where
+			p = t_S "Desugar program" $ freshProg (desugar . funcReuse) p_
+			p'' = Func f a main : p'
+			Func f a r = fromMaybe (error $ "Could not find '" ++ f_ ++ "'") $ Map.lookup (t_sc f_ f_) m
+			(main, SCState _ p' m' _) = snd (runFresh (runStateT (tie r) (SCState ((+) 1 $ maximum $ -1 : [ read rest | 'f':rest <- funcs p, all isNumber rest ]) [] m [])) "v" $ (+) 1 $ maximum $ -1 : [ read rest | 'v':rest <- allNames p, (not . null) rest, all isNumber rest ])
+			m = t_M $ byFuncName p
+	
+	supercompileMany :: [String] -> Prog -> Prog
+	supercompileMany fs p = flip onlyReachable (last fs) $ freshProg (finalSimplification simplifyProg . flip onlyReachable (last fs) <=< finalInlining progInline) (foldl (flip supercompileFunc) p fs)
+	
+	supercompile :: Prog -> Prog
+	supercompile = flip onlyReachable "main" . freshProg (finalSimplification simplifyProg . flip onlyReachable "main"  <=< finalInlining progInline) . supercompileFunc "main"
+	
+	type SCStateT m a = StateT SCState m a
+
+	data SCState = SCState { scCount :: Int,
+							 scResidual :: Prog,
+							 scFuncMap :: (Map.Map Id Decl),
+							 scRho :: [Decl] }
+	
+	scIncCount :: StateT SCState Fresh ()
+	scIncCount = do
+		SCState count prog m rho <- get
+		put (SCState (count+1) prog m rho)
+	
+	scAddDecl :: Decl -> StateT SCState Fresh Exp
+	scAddDecl d@(Func fId fArgs _) = do
+		SCState count prog m rho <- get
+		put (SCState count (d:prog) (t_M $ Map.insert fId d m) rho)
+		return $ App (Fun fId) fArgs
+	
+	scAddRho :: Decl -> StateT SCState Fresh ()
+	scAddRho d = do
+		SCState count prog m rho <- get
+		put (SCState count prog m (d:rho))
+	
+	buildSig :: Id -> Exp -> Exp -> Decl
+	buildSig i q r = Func i (map Var $ sort $ freeVars q) (autoAlphaExp r)
+	
+	tie :: Exp -> SCStateT Fresh Exp
+	tie x 	| simpleExpr x = return x
+			| otherwise	= do
+		SCState count prog m rho <- get
+		let fHead = buildSig ('f' : show count) x in
+			case findExp x $ t_Rho (show rho) rho of
+				Just e 	-> (t_T $ "Seen!" ++ show e) return e
+				Nothing	-> (t_T $ "Making f" ++ show count) (do
+							scIncCount
+							fRhs <- (drive fHead . isTerm rho) x
+							scAddDecl (fHead fRhs))
+	
+	tieOrGen :: (Exp -> Decl) -> Exp -> Exp -> SCStateT Fresh Exp
+	tieOrGen s x y = do
+		SCState _ _ _ rho <- get
+		case findExp x rho of
+			Just e	-> (t_T $ "Seen!" ++ show e) return e
+			Nothing	-> scAddRho (s x) >> lift (generalise1 x y) >>= \x' -> scAddRho (s x') >> let (cs, gen) = uniplate $ t_D ("generalised to " ++ show x') x' in liftM gen (mapM tie cs)
+	
+	drive :: (Exp -> Decl) -> Unfold -> SCStateT Fresh Exp
+	drive s (NonTerm x)		= t_D (show x) $ scAddRho (s x) >> get >>= \(SCState _ _ m rho) -> lift (unfoldT (flip Map.lookup m) rho x) >>= drive s
+	drive s (SimplTerm x)	= t_D ("Simple Termination" ++ show x) $ scAddRho (s x) >> let (cs, gen) = uniplate x in liftM gen (mapM tie cs)
+	drive s (HomeoTerm x y)	= t_D ("Homeomorphic Embedding of" ++ show x ++ "\nto" ++ show y) $ tieOrGen s x y
+	drive s (NoUnfold x)	= t_D ("No Unfolds Remaining" ++ show x) $ scAddRho (s x) >> return x
+	
+	data Unfold = NonTerm { ntExp :: Exp }
+				| SimplTerm { stExp :: Exp }
+				| HomeoTerm { htExp :: Exp, htHomeo :: Exp }
+				| NoUnfold { nuExp :: Exp }
+				deriving Show
+	
+	isTerm :: [Decl] -> Exp -> Unfold
+	isTerm rho x	| simpleTerm x	= SimplTerm x
+					| isHomeoTerm	= HomeoTerm x y
+					| otherwise		= NonTerm x
+		where
+			ht = homeoTerm rho x
+			isHomeoTerm = isJust ht
+			Just y = ht
+	
+	filterTerms :: Exp -> [Fresh Unfold] -> Fresh Unfold
+	filterTerms def ufs = filterTerms' ufs
+		where
+			filterTerms' :: [Fresh Unfold] -> Fresh Unfold
+			filterTerms' [] 	| null ufs 	= return (NoUnfold def)
+								| otherwise	= t_U ("No non-terminating expression found.") $ head ufs
+			filterTerms' (x:xs) = x >>= \x' -> case x' of
+									NonTerm _	-> t_U ("Found a non-terminating unfold.") (return x')
+									otherwise	-> t_U ("Skipped as " ++ case x' of { SimplTerm _ -> "Simple Termination."; HomeoTerm _ _ -> "Simple Termination."; otherwise -> "Unknown Problem." }) filterTerms' xs
+	
+											-- Move simplify down here \/. And freshen those variables!
+	unfoldT :: (Id -> Maybe Decl) -> [Decl] -> Exp -> Fresh Unfold
+	unfoldT m rho e = t_U "\nChecking unfold of: " $ filterTerms e unfolds
+		where							-- Should this be holes? Should freshen anything that redefines a global variable or just block it.
+			unfolds :: [Fresh Unfold]
+			unfolds = [ c' >>= simplify . h >>= return . isTerm rho | (c, h) <- ((e, id) : holes e), c' <- maybeToList (unfold c) ]
+			unfold :: Exp -> Maybe (Fresh Exp)
+			unfold e@(App (Fun f) xs) = m f >>= maybeInline xs
+			unfold (Fun f) = unfold $ App (Fun f) []
+			unfold _ = Nothing
+	
+	findExp :: Exp -> [Decl] -> Maybe Exp -- Slowdown here. Do properly
+	findExp e ds = listToMaybe $ mapMaybe (matchExp (autoAlphaExp e)) ds
+	
+	-- Must be linear and alphaed
+	matchExp :: Exp -> Decl -> Maybe Exp
+	matchExp e (Func f a r) | success	= sequence [ join (Map.lookup v mapping) | Var v <- a ] >>= Just . App (Fun f)
+							| otherwise	= Nothing
+		where
+			(success, mapping) = runState (matchExp' e (autoAlphaExp r)) (Map.fromList $ [ (v, Nothing) | Var v <- a ])
+			matchExp' :: Exp -> Exp -> State (Map.Map Id (Maybe Exp)) Bool
+			matchExp' e (Var v) = get >>= \a -> case v `Map.lookup` a of
+													Nothing	-> case e of { Var v' -> return (v == v'); otherwise -> return False }
+													Just (Nothing) -> put (Map.insert v (Just e) a) >> return True
+													Just (Just e') -> return $ e == e'
+			-- maybe deal with variable bindings
+			matchExp' e e' = liftM ((&&) (e =~ e') . and) $ zipWithM matchExp' (children e) (children e')
+	
+	--------------------------------------------------
+	--------------------------------------------------
+
+	simpleExpr :: Exp -> Bool
+	simpleExpr (Var _) = True
+	simpleExpr (Con _) = True
+	simpleExpr (Int _) = True
+	-- simpleExpr (Fun _) = True
+	simpleExpr (Fun f) = f `elem` primitives
+	simpleExpr _ = False
+
+	simpleTerm :: Exp -> Bool
+	simpleTerm (Var _) = True
+	simpleTerm (App (Con _) _) = True
+	simpleTerm (App (Fun f) _) = f `elem` primitives
+	simpleTerm (Case (Var _) _) = True
+	simpleTerm (Case (App (Con _) _) _) = True
+	simpleTerm (Case (App (Fun f) _) _) = f `elem` primitives
+	simpleTerm _ = False
+	
+	homeoTerm :: [Decl] -> Exp -> Maybe Exp
+	homeoTerm es y = listToMaybe (concatMap homeo es)
+		where
+			homeo :: Decl -> [Exp]
+			homeo (Func _ _ rhs) = if rhs <|| y then [rhs] else []
+	
diff --git a/Optimus/Trace.hs b/Optimus/Trace.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Trace.hs
@@ -0,0 +1,36 @@
+module Optimus.Trace where
+	import qualified Debug.Trace as Trace
+	import Optimus.Pretty
+	import Flite.Syntax
+	import Flite.Fresh
+	import Control.Monad
+	
+	trace :: String -> String -> a -> a
+	trace prefix suffix x = Trace.trace (prefix ++ suffix) x
+	
+	dummy :: String -> a -> a
+	dummy _ = id
+	
+	finalInlining f p = trace "\nFinal inlining of:\n" (prettyProg p) (f p)
+	finalSimplification f p = trace "\nFinal simplification of:\n" (prettyProg p) (f p)
+	
+	t_sc = trace "\nSupercompile: "
+	
+	--t_S = trace "Simplification: "
+	t_S' = trace "Simplification: "
+	t_S = dummy
+	
+	t_D = trace "\n+ Drive: "
+	
+	t_T = trace "\n}{ Tie: "
+	
+	t_U = trace ""
+	
+	-- t_M m = trace "\nMap:\n" (show m) m
+	t_M = id
+	
+	-- t_Rho = trace "\nrho:\n"
+	t_Rho = dummy
+	
+	-- t_G = trace "\n MSG: \n"
+	t_G = dummy
diff --git a/Optimus/Uniplate.hs b/Optimus/Uniplate.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Uniplate.hs
@@ -0,0 +1,30 @@
+-- |This module provides a Uniplate instance for the f-lite syntax. It also
+-- re-exports the Uniplate library.
+module Optimus.Uniplate(
+			module Data.Generics.Uniplate,
+			extract
+		) where
+	
+	import Flite.Syntax
+	import Flite.Writer
+
+	import Data.Generics.Uniplate
+	
+	instance Uniplate Exp where
+		uniplate (Case x as) = (x:ys,	\(x:ys) -> Case x (zip ps ys))
+			where
+				(ps, ys) = unzip as
+		uniplate (Let bs x)	= (x:ys,	\(x:ys)	-> Let (zip vs ys) x)
+			where
+				(vs, ys) = unzip bs
+		uniplate (App x ys) = (x:ys,	\(x:ys) -> App x ys)
+		uniplate (Var i) 	= ([],		\[]		-> Var i)
+		uniplate (Con i)	= ([],		\[]		-> Con i)
+		uniplate (Fun i) 	= ([],		\[]		-> Fun i)
+		uniplate (Int i) 	= ([],		\[]		-> Int i)
+		uniplate (Bottom) 	= ([],		\[]		-> Bottom)
+		
+	-- |Given a 'Uniplate' traversable tree and a function that extracts information
+	-- from tree nodes, extract all the information in the tree.
+	extract :: Uniplate a => (a -> [b]) -> a -> [b]
+	extract f = fst . runWriter . descendM (\a -> writeMany (f a) >> return a)
diff --git a/Optimus/Util.hs b/Optimus/Util.hs
new file mode 100644
--- /dev/null
+++ b/Optimus/Util.hs
@@ -0,0 +1,104 @@
+module Optimus.Util where
+	import Flite.Fresh
+	import Flite.Syntax
+	import Flite.Traversals hiding (freshen)
+	import Optimus.Uniplate
+	import Flite.Let
+	import Flite.Matching
+	
+	import Data.Char
+	import Data.List
+	import Control.Monad
+	import Data.Generics.Uniplate
+	import qualified Data.Map as Map
+	import Data.Maybe
+	
+	primitives = ["(+)", "(-)", "(==)", "(/=)", "(<=)", "emit", "emitInt"]
+	
+	freshen :: Exp -> Id -> Fresh Exp
+	freshen e v = fresh >>= return . fix e . Var
+		where
+			fix (Case x as) w = Case x [ if (Var v `elem` universe p) then (subst w v p, subst w v y) else (p, y) | (p, y) <- as]
+			fix (Let bs x) w@(Var w_) | v `elem` map fst bs = Let [ (if v == v_ then w_ else v_, subst w v y) | (v_, y) <- bs ] (subst w v x)
+									  | otherwise			 = Let bs x
+			fix _ _ = error "Not designed to freshen this."
+	
+	freshenMany :: Exp -> [Id] -> Fresh Exp
+	freshenMany = foldM freshen
+	
+	freshenDescend :: Exp -> Id -> Fresh Exp
+	freshenDescend e@(Case _ _) v = freshen e v >>= descendM (flip freshenDescend v)
+	freshenDescend e@(Let _ _) v = freshen e v >>= descendM (flip freshenDescend v)
+	freshenDescend e v = descendM (flip freshenDescend v) e
+	
+	freshenMD :: Exp -> [Id] -> Fresh Exp
+	freshenMD = foldM freshenDescend
+	
+	autoFresh :: Fresh a -> a
+	autoFresh x = snd $ runFresh x "v" 0
+	
+	freshProg :: (Prog -> Fresh Prog) -> Prog -> Prog
+	freshProg f x = snd $ runFresh (f x) "v" $ (+) 1 $ maximum $ -1 : [ read rest | 'v':rest <- allNames x, (not . null) rest, all isDigit rest ]
+	
+	allNames :: Prog -> [Id]
+	allNames p = nub $ concat [ [f] ++ concatMap patVars a ++ allnames r | Func f a r <- p ]
+		where
+			allnames (Var v) = [v]
+			allnames (Fun f) = [f]
+			allnames e@(Case _ as) = concatMap (patVars . fst) as ++ extract allnames e
+			allnames e@(Let bs _) = map fst bs ++ extract allnames e
+			allnames e = extract allnames e
+
+	-- allNames p = concat [ [f] ++ (concatMap patVars a) ++ [ v | Var v <- universe r ] ++ (concat [ patVars p | Case _ as <- universe r, (p, _) <- as ]) | Func f a r <- p ]
+		
+	alphaExp :: Exp -> Fresh Exp
+	alphaExp e = (alpha . Func "NOVAR" []) e >>= return . funcRhs
+	
+	autoAlphaExp :: Exp -> Exp
+	autoAlphaExp e = snd $ runFresh (alphaExp e) "v" $ (+) 1 $ maximum $ -1 : [ read rest | 'v':rest <- freeVars e, (not . null) rest, all isDigit rest ]
+	
+	insertMany :: Ord k => Map.Map k a -> [(k, a)] -> Map.Map k a
+	insertMany = foldr (uncurry Map.insert)
+	
+	alpha :: Decl -> Fresh Decl
+	alpha (Func i a r) = alphaM
+		where
+			alphaM = do
+				l <- assocFresh ([ v | Var v <- concatMap universe a ] ++ [i]) >>= return . Map.fromList
+				r' <- freshSubst l r
+				a' <- mapM (freshSubst l) a
+				return $ Func (fromJust $ Map.lookup i l) a' r'
+			assocFresh :: [Id] -> Fresh [(Id, Id)]
+			assocFresh = mapM (\v -> fresh >>= \v' -> return (v, v'))
+			freshSubst :: Map.Map Id Id -> Exp -> Fresh Exp
+			freshSubst l (Var v) 	| isJust v' = return . Var . fromJust $ v'
+									| otherwise	= return . Var $ v
+				where
+					v' = Map.lookup v l
+			freshSubst l (Let bs x) = let (vs, ys) = unzip bs in do
+				m <- assocFresh vs
+				descendM (freshSubst $ insertMany l m) (Let (zip (map snd m) ys) x)
+			freshSubst l (Case x as) = do
+				x' <- freshSubst l x
+				as' <- sequence [ assocFresh [v | Var v <- universe p] >>= \m -> let fS' = freshSubst $ insertMany l m in liftM2 (,) (fS' p) (fS' y) | (p, y) <- as]
+				return (Case x' as')
+			freshSubst l e = descendM (freshSubst l) e
+			
+	desugar :: Prog -> Fresh Prog
+	desugar p = return p >>= desugarCase >>= desugarEqn >>= inlineLinearLet >>= inlineSimpleLet
+	
+	funcReuse :: Prog -> Prog
+	funcReuse p = if null reused then p else error $ "Reused the name of a function as a local variable. " ++ show reused
+		where
+			reused = funcs p `intersect` (nub . concatMap (\d -> (concatMap patVars . funcArgs) d ++ (boundVars . funcRhs) d) $ p)
+	
+	byFuncName :: Prog -> Map.Map Id Decl
+	byFuncName []					= Map.empty
+	byFuncName (d@(Func f _ _):ds)	= Map.insert f d (byFuncName ds)
+	
+	boundVars :: Exp -> [Id]
+	boundVars = nub . bv
+		where
+			bv e@(Case _ as) = concatMap (patVars . fst) as ++ extract bv e
+			bv e@(Let bs _) = map fst bs ++ extract bv e
+			bv e = extract bv e
diff --git a/optimusprime.cabal b/optimusprime.cabal
--- a/optimusprime.cabal
+++ b/optimusprime.cabal
@@ -1,5 +1,5 @@
 Name:              optimusprime
-version: 0.0.1.20091113
+version: 0.0.1.20091114
 Synopsis:          A supercompiler for f-lite
 License:           BSD3
 License-file:      LICENSE
@@ -14,8 +14,12 @@
 
 Executable optimusprime
     Main-is:       OptimusPrime.hs
+    Other-modules: Optimus.CallGraph, Optimus.Generalise, Optimus.Homeo,
+                   Optimus.Inline, Optimus.Pretty, Optimus.Simplify,
+                   Optimus.Strategy, Optimus.Trace, Optimus.Uniplate,
+                   Optimus.Util
     Build-Depends: base >= 3 && < 5, containers >= 0 && < 1,
-                   parsec >= 2.1.0.1 && < 3, flite >= 0 && < 1,
+                   parsec >= 2.1.0.1 && < 3, flite >= 0.1.1 && < 1,
                    uniplate >= 1.2.0.3 && < 2, wl-pprint >= 1 && < 2,
                    mtl >= 1.1.0.2 && < 2, fgl >= 5.4.2.2 && < 6,
                    graphviz >= 2999.6.0.0, haskell98 >= 1 && < 2,