diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Dan Rosén
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Dan Rosén nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/executable/Main.hs b/executable/Main.hs
new file mode 100644
--- /dev/null
+++ b/executable/Main.hs
@@ -0,0 +1,80 @@
+module Main where
+
+import Tip.HaskellFrontend
+
+import Text.Show.Pretty hiding (Name)
+import System.Environment
+import qualified Data.Foldable as F
+import Data.Ord
+
+import Control.Monad
+
+import Tip.Core
+import Tip.Fresh
+import Tip.Simplify
+import Tip.Lint
+import Tip.Passes
+
+import Tip.Utils.Rename
+
+import Tip.Pretty
+import Tip.Pretty.SMT as SMT
+
+import Text.PrettyPrint
+
+main :: IO ()
+main = do
+    f:es <- getArgs
+    thy <- readHaskellFile Params
+      { file = f
+      , include = []
+      , flags = [] -- [PrintCore,PrintProps,PrintExtraIds,PrintInitialTip]
+      , only = es -- []
+      , extra = [] -- es
+      }
+    -- putStrLn (ppRender thy)
+    let renamed_thy = renameWith disambigId thy
+    let pipeline =
+          freshPass $
+            runPasses
+              [ SimplifyAggressively
+              , RemoveNewtype
+              , UncurryTheory
+              , CommuteMatch
+              , SimplifyGently
+              , IfToBoolOp
+              , RemoveAliases, CollapseEqual
+              , CommuteMatch
+              , SimplifyGently
+              , CSEMatch
+              , EliminateDeadCode
+              ]
+    print (SMT.ppTheory (pipeline renamed_thy))
+
+data Var = Var String | Refresh Var Int
+  deriving (Show,Eq,Ord)
+
+varMax :: Var -> Int
+varMax Var{}         = 0
+varMax (Refresh v i) = varMax v `max` i
+
+instance PrettyVar Var where
+  varStr (Var "")      = "x"
+  varStr (Var xs)      = xs
+  varStr (Refresh v i) = varStr v
+
+disambigId :: Id -> [Var]
+disambigId i = vs : [ Refresh vs x | x <- [0..] ]
+  where
+    vs = Var $ case varStr i of { [] -> "x"; xs -> xs }
+
+instance Name Var where
+  fresh     = refresh (Var "")
+  refresh (Refresh v _) = refresh v
+  refresh v@Var{}       = Refresh v `fmap` fresh
+
+  freshNamed s = refresh (Var s)
+
+  getUnique (Refresh _ i) = i
+  getUnique Var{}         = 0
+
diff --git a/src/Tip.hs b/src/Tip.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE TypeOperators, FlexibleInstances #-}
+-- | The language properties are expressed in in the Haskell source
+module Tip
+    ( Equality
+    , (:=>:)
+    , And
+    , Or
+    , Neg
+    , Forall
+    , Exists
+    , (===)
+    , (=/=)
+    , bool
+    , (==>)
+    , (.&&.)
+    , (.||.)
+    , neg
+    , forAll
+    , exists
+    , module Test.QuickCheck
+    ) where
+
+import Test.QuickCheck hiding ((===), (==>), (.&&.), (.||.), forAll)
+import qualified Test.QuickCheck as QC
+
+infix 3 ===
+infix 3 =/=
+infixr 2 .&&.
+infixr 1 .||.
+infixr 0 ==>
+infixr 0 :=>:
+
+-- | The property data type
+
+data Equality a = a :=: a
+data a :=>: b = Given a b
+data And a b = And a b
+data Or a b = Or a b
+data Neg a = Neg a
+data Forall a b = Forall (a -> b)
+data Exists a b = Exists (a -> b)
+
+-- | Equality
+(===) :: a -> a -> Equality a
+(===) = (:=:)
+
+-- | Inequality
+(=/=) :: a -> a -> Neg (Equality a)
+u =/= v = Neg (u === v)
+
+-- | A synonym for '===', but for booleans
+bool :: Bool -> Equality Bool
+bool lhs = lhs === True
+
+-- | Implication
+(==>) :: a -> b -> a :=>: b
+(==>) = Given
+
+-- | Conjunction
+(.&&.) :: a -> b -> And a b
+(.&&.) = And
+
+-- | Disjunction
+(.||.) :: a -> b -> Or a b
+(.||.) = Or
+
+-- | Negation
+neg :: a -> Neg a
+neg = Neg
+
+-- | Universal quantification
+forAll :: (a -> b) -> Forall a b
+forAll = Forall
+
+-- | Existential quantification
+exists :: (a -> b) -> Exists a b
+exists = Exists
+
+instance (Eq a, Show a) => Testable (Equality a) where
+  property (x :=: y) = x QC.=== y
+
+instance Testable b => Testable (Bool :=>: b) where
+  property (Given x p) = x QC.==> p
+
+instance Testable b => Testable (Neg Bool :=>: b) where
+  property (Given (Neg x) p) = not x QC.==> p
+
+instance Testable (Neg Bool) where
+  property (Neg x) = property (not x)
+
+instance (Eq a, Show a, Testable b) => Testable (Equality a :=>: b) where
+  property (Given (x :=: y) p) = x == y QC.==> p
+
+instance (Testable a, Testable b) => Testable (And a b) where
+  property (And p q) = p QC..&&. q
+
+instance (Testable a, Testable b) => Testable (Or a b) where
+  property (Or p q)  = p QC..||. q
+
+instance (Arbitrary a, Show a, Testable b) => Testable (Forall a b) where
+  property (Forall p) = property p
+
diff --git a/src/Tip/Calls.hs b/src/Tip/Calls.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Calls.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE NamedFieldPuns,ScopedTypeVariables #-}
+module Tip.Calls
+    ( module VarSet
+    , Constructors(..)
+    , exprCalls
+    , calls
+    , transCalls
+    , transFrom
+    ) where
+
+import CoreSyn
+import Id
+import VarSet
+import CoreFVs
+import DataCon
+import TyCon
+
+import Tip.GHCUtils
+import Tip.Unfoldings
+import Tip.FreeTyCons
+
+import qualified Data.Set as S
+
+data Constructors = With | Without deriving Eq
+
+-- | The vars this expression calls
+exprCalls :: Constructors -> CoreExpr -> VarSet
+exprCalls cons = exprSomeFreeVars $ \ v ->
+          (isLocalId v || isGlobalId v || (cons == With && isDataConId v && not (isNewtypeConId v)))
+       && (cons == With || not (isDataConId v))
+
+-- | The functions this functions calls (not transitively)
+calls :: Constructors -> Id -> VarSet
+calls c v = cons `unionVarSet` case maybeUnfolding v of
+    Just e -> exprCalls c e
+    _      -> emptyVarSet
+  where
+    cons | c == With = mkVarSet (concatMap (map dataConWorkId . tyConDataCons)
+                                           (filter (not . isClassTyCon) (S.toList (varTyCons v))))
+                                           -- NOTE: Ignore all class contexts
+         | otherwise = emptyVarSet
+
+-- | The functions this function calls transitively
+transCalls :: Constructors -> Id -> VarSet
+transCalls c = transFrom c . unitVarSet
+
+-- | The transitive closure of calls from this set
+transFrom :: Constructors -> VarSet -> VarSet
+transFrom c = go emptyVarSet
+  where
+    go visited queue
+        | isEmptyVarSet to_visit = visited
+        | otherwise = go (visited `unionVarSet` to_visit)
+                         (foldVarSet (\ i vs -> calls c i `unionVarSet` vs)
+                                     emptyVarSet
+                                     to_visit)
+      where to_visit = queue `minusVarSet` visited
+
diff --git a/src/Tip/Compile.hs b/src/Tip/Compile.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Compile.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE RecordWildCards, NamedFieldPuns, CPP #-}
+module Tip.Compile (compileHaskellFile) where
+
+import Tip.Calls
+import Tip.Dicts (inlineDicts)
+import Tip.GHCUtils
+import Tip.Params
+import Tip.ParseDSL
+import Tip.GHCScope
+import Tip.Unfoldings
+import Data.List.Split (splitOn)
+
+import Control.Monad
+import Data.List
+import Data.Maybe
+import qualified Data.Foldable as F
+import System.FilePath
+
+import CoreMonad (liftIO)
+import CoreSyn
+import CoreSyn (flattenBinds)
+import DynFlags
+import GHC
+import GHC.Paths
+import HscTypes
+import SimplCore
+import Var
+import VarSet
+#if __GLASGOW_HASKELL__ < 708
+import StaticFlags
+#endif
+
+compileHaskellFile :: Params  -> IO [Var]
+compileHaskellFile params@Params{..} = do
+
+    -- Notify ghc where ghc is installed
+    runGhc (Just libdir) $ do
+
+        -- Set interpreted so we can get the signature,
+        -- and expose all unfoldings
+        dflags0 <- getSessionDynFlags
+        let dflags =
+#if __GLASGOW_HASKELL__ >= 708
+                updateWays $
+                addWay' WayThreaded $
+#endif
+                     dflags0 { ghcMode = CompManager
+                             , optLevel = 0
+                             , profAuto = NoProfAuto
+                             , importPaths = include ++ includePaths dflags0 ++ ["."]
+                             }
+                        `wopt_unset` Opt_WarnOverlappingPatterns
+#if __GLASGOW_HASKELL__ >= 708
+                        `gopt_unset` Opt_IgnoreInterfacePragmas
+                        `gopt_unset` Opt_OmitInterfacePragmas
+                        `gopt_set` Opt_ExposeAllUnfoldings
+                        `gopt_set` Opt_BuildDynamicToo
+#else
+                        `dopt_unset` Opt_IgnoreInterfacePragmas
+                        `dopt_unset` Opt_OmitInterfacePragmas
+                        `dopt_set` Opt_ExposeAllUnfoldings
+#endif
+        _ <- setSessionDynFlags dflags
+
+            -- add .hs if it is not present (apparently not supporting lhs)
+        let file_with_ext = replaceExtension file ".hs"
+
+        target <- guessTarget file_with_ext Nothing
+        addTarget target
+        r <- load LoadAllTargets
+        when (failed r) $ error "Compilation failed!"
+
+        mod_graph <- getModuleGraph
+        let mod_sum = findModuleSum file_with_ext mod_graph
+
+        -- Parse, typecheck and desugar the module
+        p <- parseModule mod_sum
+        t <- typecheckModule p
+        d <- desugarModule t
+
+        let modguts = dm_core_module d
+
+        let binds = fixUnfoldings (inlineDicts (flattenBinds (mg_binds modguts)))
+
+        let fix_id :: Id -> Id
+            fix_id = fixId binds
+
+        liftIO $ when (PrintCore `elem` flags) $
+             putStrLn ("Tip.Compile, PrintCore:\n" ++ showOutputable binds)
+
+        -- Set the context for evaluation
+        setContext $
+            [ IIDecl (simpleImportDecl (moduleName (ms_mod mod_sum)))
+            , IIDecl (qualifiedImport "GHC.Types")
+            , IIDecl (qualifiedImport "GHC.Base")
+            , IIDecl (qualifiedImport "Prelude")
+            ]
+            -- Also include the imports the module is importing
+            ++ map (IIDecl . unLoc) (ms_textual_imps mod_sum)
+
+        ids_in_scope <- getIdsInScope fix_id
+
+        let only' :: [String]
+            only' = concatMap (splitOn ",") only
+
+            props :: [Var]
+            props =
+                [ fix_id i
+                | i <- ids_in_scope
+                , varWithPropType i
+                , not (varInTip i)
+                , null only || varToString i `elem` only'
+                ]
+
+        when (PrintProps `elem` flags)
+             (liftIO (putStrLn ("Tip.Compile, PrintProps:\n" ++ showOutputable props)))
+
+        extra_ids <- extraIds params props
+
+        -- Wrapping up
+        return (props `union` extra_ids)
+
+findModuleSum :: FilePath -> [ModSummary] -> ModSummary
+findModuleSum file
+    = fromMaybe (error $ "Cannot find module " ++ file)
+    . find (maybe False (== file) . summaryHsFile)
+
+summaryHsFile :: ModSummary -> Maybe FilePath
+summaryHsFile = ml_hs_file . ms_location
+
+parseToId :: String -> Ghc Id
+parseToId s = do
+    t <- lookupString s
+    case mapMaybe thingToId t of
+        []  -> error $ s ++ " not in scope!"
+        [x] -> return x
+        xs  -> error $ s ++ " in scope as too many things: " ++ showOutputable xs
+
+extraIds :: Params -> [Var] -> Ghc [Var]
+extraIds p@Params{..} prop_ids = do
+
+    extra_ids <- mapM parseToId (concatMap (splitOn ",") extra)
+
+    let trans_ids :: VarSet
+        trans_ids = unionVarSets $
+            map (transCalls With) (prop_ids ++ extra_ids)
+
+    let ids = varSetElems $ filterVarSet (\ x -> not (varInTip x || varWithPropType x) && not (hasClass (varType x)))
+            trans_ids
+
+    -- Filters out silly things like
+    -- Control.Exception.Base.patError and GHC.Prim.realWorld#
+    let in_scope = inScope . varToString
+
+    ids_in_scope <- filterM in_scope ids
+
+    liftIO $ when (PrintExtraIds `elem` flags) $ do
+        putStrLn "Tip.Compile, PrintExtraIds:"
+        let out :: String -> [Id] -> IO ()
+            out lbl os = putStrLn $ lbl ++ " =\n " ++ showOutputable [ (o{-,maybeUnfolding o-}) | o <- os ]
+#define OUT(i) out "i" (i)
+        OUT(prop_ids)
+        OUT(extra_ids)
+        OUT(ids)
+        OUT(ids_in_scope)
+#undef OUT
+
+    return ids_in_scope
+
+qualifiedImport :: String -> ImportDecl name
+qualifiedImport = qualifiedImportDecl . mkModuleName
+
+qualifiedImportDecl :: ModuleName -> ImportDecl name
+qualifiedImportDecl m = (simpleImportDecl m) { ideclQualified = True }
+
diff --git a/src/Tip/CoreToTip.hs b/src/Tip/CoreToTip.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/CoreToTip.hs
@@ -0,0 +1,380 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# LANGUAGE PatternGuards, TypeSynonymInstances, FlexibleInstances, CPP, RecordWildCards, FlexibleContexts, NamedFieldPuns, ScopedTypeVariables #-}
+
+-- | Translation from GHC Core to the Tip IR
+module Tip.CoreToTip where
+
+import Prelude hiding (log)
+
+import Control.Applicative
+import Control.Monad.Error
+import Control.Monad.Reader
+import Control.Monad.Writer
+
+#if __GLASGOW_HASKELL__ >= 708
+import Data.ByteString (unpack)
+import Data.Char (chr)
+#else
+import FastString (unpackFS)
+#endif
+
+import Tip.Core as Tip
+
+import CoreUtils as C
+import CoreSyn as C
+
+import Data.Char (ord)
+import Data.List ((\\),union)
+import Data.Maybe (fromMaybe)
+
+import PrimOp
+
+import Unique
+import DataCon
+import Literal
+import Var hiding (Id)
+import TyCon hiding (data_cons)
+import Type as C
+import GHC (dataConType)
+
+import TysWiredIn
+import PrelNames (gHC_REAL)
+
+import qualified TysPrim
+import qualified PrelNames
+
+import IdInfo
+import Name
+
+import Outputable
+
+import Tip.GHCUtils (showOutputable,rmClass)
+import Tip.DataConPattern
+import Tip.TyAppBeta
+import Tip.Id
+import Tip.Utils (usort)
+
+-- | The binders in our translated expressions.
+--
+--   We cannot use 'Var'/'Id' because 'TyCon's do not have them,
+--   and 'DataCon's does not necessarily have a unique.
+--   'Name's have, just as 'Var'/'Id', a 'Unique' in them.
+--
+--   The types need to be remembered so we used typed
+--
+--   The list of var is the variables in scope
+
+type TM = ReaderT [Var] (Either String)
+
+type TMW = WriterT [Function Id] TM
+
+runTM :: TM a -> Either String a
+runTM m = runReaderT m []
+
+msgUnsupportedLiteral l    = "Unsupported literal: " ++ showOutputable l
+msgIllegalType t           = "Illegal type: " ++ showOutputable t
+msgTypeApplicationToExpr e = "Type application to expression: " ++ showOutputable e
+msgTypeExpr e              = "Type expression: " ++ showOutputable e
+msgCoercionExpr e          = "Coercion expression: " ++ showOutputable e
+msgCastExpr e              = "Cast expression: " ++ showOutputable e
+msgHigherRankType v t      = showOutputable v ++ " has a higher-rank type: " ++ showOutputable t
+msgUnificationError t tvs dc e mu =
+       "Unification error on " ++ showOutputable t
+       ++ "\nWhen resolving type variables " ++ showOutputable tvs
+       ++ " for constructor " ++ showOutputable dc ++
+       (case mu of
+           Just u -> "\nObtained unifier: " ++ showOutputable u
+           Nothing -> " without unifier")
+       ++ "\nOriginating from expression: " ++ showOutputable e
+msgNonVanillaDataCon dc tc =
+       "Data constructor " ++ showOutputable dc ++
+
+       " from type constructor " ++ showOutputable tc ++
+       " is not Haskell 98!"
+msgNotAlgebraicTyCon tc =
+       "Type constructor " ++ showOutputable tc ++ " is not algebraic!"
+msgFail s = "Internal failure: " ++ s
+
+trTyCon :: TyCon -> Either String (Datatype Id)
+trTyCon tc = do
+    unless (isAlgTyCon tc) (throwError (msgNotAlgebraicTyCon tc))
+    dcs <- mapM tr_dc (tyConDataCons tc)
+    return Datatype
+        { data_name = idFromTyCon tc
+        , data_tvs  = map idFromTyVar tc_tvs
+        , data_cons = dcs
+        }
+  where
+    tc_tvs = tyConTyVars tc
+
+    tr_dc dc = do
+        unless
+            (isVanillaDataCon dc)
+            (throwError (msgNonVanillaDataCon dc tc))
+        let dc_tys = dataConInstArgTys dc (map mkTyVarTy tc_tvs)
+        ts <- mapM trType dc_tys
+        let cn = idFromDataCon dc
+        return Constructor
+            { con_name    = cn
+            , con_discrim = Discrim cn
+            , con_args    = map (Project cn) [0..] `zip` ts
+            }
+
+-- | Translate a definition
+trDefn :: Var -> CoreExpr -> TM [Function Id]
+trDefn v e = do
+    let (tvs,ty) = splitForAllTys (C.exprType e)
+    ty' <- lift (trType ty)
+    let (tvs',body) = collectTyBinders e
+    when (tvs /= tvs') (fail "Type variables do not match in type and lambda!")
+    (body',fns) <- runWriterT (trExpr (tyAppBeta body))
+    let v' = idFromVar v
+    let rn x | x `elem` map func_name fns = Just (x `LiftedFrom` v')
+             | otherwise                  = Nothing
+    return $ fmap (rename rn) $ [Function
+        { func_name    = v'
+        , func_tvs     = map idFromTyVar tvs
+        , func_args    = []
+        , func_res     = ty'
+        , func_body    = body'
+        }] ++ fns
+
+rename :: (Functor f,Ord a) => (a -> Maybe a) -> f a -> f a
+rename lk = fmap (\ x -> fromMaybe x (lk x))
+
+log :: Outputable a => a -> b -> b
+log x = trace (showOutputable x)
+-- | Translating variables
+--
+-- Need to conflate worker and wrapper data constructors otherwise
+-- they might differ from case alternatives
+-- (example: created tuples in partition's where clause)
+-- It is unclear what disasters this might bring.
+trVar :: Var -> [Tip.Type Id] -> TMW (Tip.Expr Id)
+trVar x [] | x == trueDataConId  = return (bool True)
+trVar x [] | x == falseDataConId = return (bool False)
+trVar x []
+  | nameModule_maybe (Var.varName x) == Just gHC_REAL
+  , Just bu <- case getOccString x of
+                "div" -> Just IntDiv
+                "mod" -> Just IntMod
+  = return
+      $ Tip.Lam [ghcInt 0]
+      $ Tip.Lam [ghcInt 1]
+      $ Match (Lcl (ghcInt 0))
+      [ Tip.Case (intPat [int 2])
+      $ Match (Lcl (ghcInt 1))
+      [ Tip.Case (intPat [int 3])
+      $ Gbl iHash :@: [Builtin bu :@: [Lcl (int 2),Lcl (int 3)]]
+      ]]
+ where
+  ghcInt i = Local (Eta i) ghcIntType
+  ghcIntType = Tip.TyCon (idFromTyCon intTyCon) []
+  int i = Local (Eta i) intType
+  iHash = trConstructor intDataCon (Tip.PolyType [] [intType] ghcIntType) []
+  intPat = ConPat iHash
+trVar x _
+  | tip:_ <- [ tip
+             | (ghc,tip) <- primops
+             , getUnique (getOccName x) == getUnique (primOpOcc ghc)
+             ] = return tip
+trVar x tys = do
+    ty <- ll (trPolyType (varType x))
+    lcl <- asks (x `elem`)
+    if lcl
+        then case ty of
+                PolyType [] [] tr -> return (Lcl (Local (idFromVar x) tr))
+                _                 -> fail ("Local identifier " ++ showOutputable x ++
+                                           " with forall-type: " ++ showOutputable (varType x))
+        else return $ case idDetails x of
+                DataConWorkId dc -> abstract $ trConstructor dc ty tys
+                DataConWrapId dc -> abstract $ trConstructor dc ty tys
+                _                -> Gbl (Global (idFromVar x) ty tys) :@: []
+    where
+      abstract gbl = foldr lam body etas
+        where
+          body = Gbl gbl :@: map Lcl etas
+          etas = zipWith (Local . Eta) [0..] args
+          (args, _) = applyPolyType (gbl_type gbl) tys
+          lam lcl body = Tip.Lam [lcl] body
+
+trPattern :: DataCon -> PolyType Id -> [Tip.Type Id] -> [Tip.Local Id] -> Pattern Id
+trPattern dc _ [] []
+  | dc == trueDataCon  = LitPat (Bool True)
+  | dc == falseDataCon = LitPat (Bool False)
+trPattern dc ty tys args = ConPat (trConstructor dc ty tys) args
+
+trConstructor :: DataCon -> PolyType Id -> [Tip.Type Id] -> Global Id
+trConstructor dc ty tys = Global (idFromName $ dataConName dc) (uncurryTy ty) tys
+  where
+    uncurryTy ty@PolyType{polytype_res = args :=>: res} =
+      ty' { polytype_args = args ++ polytype_args ty' }
+      where
+        ty' = uncurryTy ty { polytype_res = res }
+    uncurryTy ty = ty
+
+ll :: Either String a -> TMW a
+ll = lift . lift
+
+errorType :: PolyType Id
+errorType = PolyType [Eta 0] [] (TyVar (Eta 0))
+
+errorCall :: Tip.Type Id -> Tip.Expr Id
+errorCall ty = Gbl (Global Error errorType [ty]) :@: []
+
+-- | Translating expressions
+--
+-- GHC Core allows application of types to arbitrary expressions,
+-- but this language only allows application of types to variables.
+--
+-- The type variables applied to constructors in case patterns is
+-- not immediately available in GHC Core, so this has to be reconstructed.
+trExpr :: CoreExpr -> TMW (Tip.Expr Id)
+trExpr e0 = case collectTypeArgs e0 of
+    (C.App (C.App (C.Var patError) (C.Type ty)) (C.Lit _), _)
+      | varUnique patError == PrelNames.patErrorIdKey -> do
+          t <- ll (trType ty)
+          return (errorCall t)
+    (C.Var x, tys) -> mapM (ll . trType) tys >>= trVar x
+    (_, _:_) -> throw (msgTypeApplicationToExpr e0)
+    (C.Lit l, _) -> literal <$> trLit l
+
+    (C.App e1 e2, _) -> (\ x y -> Builtin At :@: [x,y]) <$> trExpr e1 <*> trExpr e2
+
+    (C.Lam x e, _) -> do
+        t <- ll (trType (varType x))
+        e' <- local (x:) (trExpr e)
+        return (Tip.Lam [Local (idFromVar x) t] e')
+
+    (C.Let (C.NonRec v b) e, _) -> do
+        vt <- ll (trType (varType v))
+        b' <- trExpr b
+        e' <- local (v:) (trExpr e)
+        return (Tip.Let (Local (idFromVar v) vt) b' e')
+
+    (C.Let (C.Rec vses) b, _) -> do
+        fns <- concat <$> mapM (lift . uncurry trDefn) vses
+        body <- trExpr b
+        let free_vars = usort $ concatMap fn_free_vars fns
+        let free_tvs  = usort $ concatMap fn_free_tvs fns
+
+        -- now each function in fns gets these fvs and vars and prepended
+        let map_body = su_globals
+                [ (func_name,\ ts es -> Gbl (Global func_name new_type (map TyVar free_tvs ++ ts)) :@: (map Lcl free_vars ++ es))
+                | fn@Function{func_name} <- fns
+                , let PolyType tvs args res = funcType fn
+                      new_type = PolyType (free_tvs ++ tvs) (map lcl_type free_vars ++ args) res
+                ]
+
+        tell [ Function func_name (free_tvs ++ func_tvs) (free_vars ++ func_args) func_res (map_body func_body)
+             | Function{..} <- fns
+             ]
+
+        return (map_body body)
+      where
+        fn_free_vars Function{func_args,func_body} = free func_body \\ func_args
+        fn_free_tvs fn@Function{func_body} =
+            (freeTyVars func_body `union` tyVars (args :=>: res)) \\ tvs
+          where
+            PolyType tvs args res = funcType fn
+
+        su_globals :: [(Id,[Tip.Type Id] -> [Tip.Expr Id] -> Tip.Expr Id)] -> Tip.Expr Id -> Tip.Expr Id
+        su_globals xks = transformExpr $ \ e0 -> case e0 of
+            Gbl (Global y _ ts) :@: es | Just k <- lookup y xks -> k ts es
+            _                                                   -> e0
+
+    (C.Case e x _ alts, _) -> do
+
+        e' <- trExpr e
+
+        let t = C.exprType e
+
+        t' <- ll (trType t)
+
+        let tr_alt :: CoreAlt -> TMW (Tip.Case Id)
+            tr_alt alt = case alt of
+                (DEFAULT   ,[],rhs) -> Tip.Case Default <$> trExpr rhs
+
+                (DataAlt dc,bs,rhs) -> do
+
+                    let (dc_tvs,mu) = dcAppliedTo t dc
+                        unif_err    = msgUnificationError t dc_tvs dc e0
+
+                    case mu of
+                        Just u -> case mapM (lookupTyVar u) dc_tvs of
+                            Just tys -> do
+                                tys' <- mapM (ll . trType) tys
+                                bs' <- forM bs $ \ b ->
+                                    (,) (idFromVar b) <$> ll (trType (varType b))
+                                rhs' <- local (bs++) (trExpr rhs)
+                                dct <- ll (trPolyType (dataConType dc))
+                                return $ Tip.Case
+                                    (trPattern dc dct tys' (map (uncurry Local) bs'))
+                                    rhs'
+                            Nothing -> throw (unif_err (Just u))
+                        Nothing -> throw (unif_err Nothing)
+
+                (LitAlt lit,[],rhs) -> do
+
+                    -- let TyCon v [] = t'
+                    lit' <- trLit lit
+                    rhs' <- trExpr rhs
+                    return (Tip.Case (LitPat lit') rhs')
+
+                _ -> fail "Default or LitAlt with variable bindings"
+
+        let scrut = Local (idFromVar x) t'
+
+        Tip.Let scrut e' . Match (Lcl scrut) <$> local (x:) (mapM tr_alt alts)
+
+    (C.Tick _ e, _) -> trExpr e
+    (C.Type{}, _) -> throw (msgTypeExpr e0)
+    (C.Coercion{}, _) -> throw (msgCoercionExpr e0)
+    (C.Cast{}, _) -> throw (msgCastExpr e0)
+    -- TODO:
+    --     Do we need to do something about newtype casts?
+
+collectTypeArgs :: CoreExpr -> (CoreExpr, [C.Type])
+collectTypeArgs (C.App e (Type t)) = (e', tys ++ [t])
+  where
+    (e', tys) = collectTypeArgs e
+collectTypeArgs e = (e, [])
+
+trLit :: Literal -> TMW Lit
+trLit (LitInteger x _type) = return (Int x)
+trLit (MachInt x)          = return (Int x)
+trLit (MachInt64 x)        = return (Int x)
+trLit (MachChar ch)        = return (Int (toInteger (ord ch)))
+#if __GLASGOW_HASKELL__ >= 708
+trLit (MachStr s) = return (String (map (chr . fromInteger . toInteger) (unpack s)))
+#else
+trLit (MachStr s) = return (String (unpackFS s))
+#endif
+trLit l           = throw (msgUnsupportedLiteral l)
+
+trPolyType :: C.Type -> Either String (Tip.PolyType Id)
+trPolyType t0 =
+    let (tv,t) = splitForAllTys (expandTypeSynonyms t0)
+    in  PolyType (map idFromTyVar tv) [] <$> trType (rmClass t)
+
+throw :: String -> TMW a
+throw = ll . throwError
+
+essentiallyInteger :: TyCon -> Bool
+essentiallyInteger tc = tc == TysPrim.intPrimTyCon {-
+                      || tc == TysPrim.charPrimTyCon
+                      || tyConUnique tc == PrelNames.integerTyConKey
+                      -}
+
+
+trType :: C.Type -> Either String (Tip.Type Id)
+trType = go . expandTypeSynonyms
+  where
+    go t0
+        | Just (t1,t2) <- splitFunTy_maybe t0    = (\ x y -> [x] :=>: y) <$> go t1 <*> go t2
+        | Just (tc,[]) <- splitTyConApp_maybe t0, essentiallyInteger tc = return intType
+        | Just (tc,[]) <- splitTyConApp_maybe t0, tc == boolTyCon       = return boolType
+        | Just (tc,ts) <- splitTyConApp_maybe t0 = TyCon (idFromTyCon tc) <$> mapM go ts
+        | Just tv <- getTyVar_maybe t0           = return (TyVar (idFromTyVar tv))
+        | otherwise                              = throwError (msgIllegalType t0)
+
diff --git a/src/Tip/DataConPattern.hs b/src/Tip/DataConPattern.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/DataConPattern.hs
@@ -0,0 +1,16 @@
+
+module Tip.DataConPattern where
+
+import DataCon
+import Var
+import Type
+
+import Unify
+
+dcAppliedTo :: Type -> DataCon -> ([TyVar],Maybe TvSubst)
+dcAppliedTo t dc = (dc_tvs,mu)
+  where
+    dc_tvs = dataConUnivTyVars dc
+    res_ty = dataConOrigResTy dc
+    mu = tcUnifyTys (const BindMe) [res_ty] [t]
+
diff --git a/src/Tip/Dicts.hs b/src/Tip/Dicts.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Dicts.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE PatternGuards, TypeSynonymInstances, FlexibleInstances, ViewPatterns, ExplicitForAll #-}
+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleContexts, NamedFieldPuns #-}
+{-# LANGUAGE CPP #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Tip.Dicts (inlineDicts,maybeUnfolding) where
+
+import Tip.GHCUtils (showOutputable)
+#if __GLASGOW_HASKELL__ >= 708
+import DynFlags (unsafeGlobalDynFlags)
+#endif
+import CoreSyn
+import CoreUtils()
+import IdInfo
+import Id
+import Var
+import Data.List (elemIndex)
+import VarEnv (emptyInScopeSet)
+
+import Data.Generics.Geniplate
+
+import Outputable
+import Type
+import Literal
+import Coercion
+
+import Name (getOccString,nameModule_maybe)
+import PrelNames (gHC_REAL)
+
+instanceTransformBiT
+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]
+    [t| forall a . (Expr a,Expr a) |]
+
+instanceTransformBiT
+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]
+    [t| forall a . (Expr a,[Bind a]) |]
+
+instanceTransformBiT
+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]
+    [t| forall a . (Expr a,[(a,Expr a)]) |]
+
+-- | Maybe the unfolding of an Id
+maybeUnfolding :: Id -> Maybe CoreExpr
+maybeUnfolding v = case ri of
+    CoreUnfolding{uf_tmpl} -> Just uf_tmpl
+    _                      -> Nothing
+  where
+    ri = realIdUnfolding v
+
+
+
+inlineDicts :: TransformBi (Expr Id) t => t -> t
+inlineDicts = transformBi $ \ e0 -> case e0 of
+    App (App (Var f) (Type t)) (Var d)
+        | getOccString f == "div" && nameModule_maybe (varName f) == Just gHC_REAL -> Var f
+        | getOccString f == "mod" && nameModule_maybe (varName f) == Just gHC_REAL -> Var f
+#if __GLASGOW_HASKELL__ >= 708
+        | [try] <- [ try | BuiltinRule _ _ 2 try <- idCoreRules f ]
+        , Just e <- try unsafeGlobalDynFlags (emptyInScopeSet,realIdUnfolding) f [Type t,Var d]
+        -> e
+#endif
+        | Just cl <- isClassOpId_maybe f
+        , DFunId{} <- idDetails d
+        -> case maybeUnfolding f of
+            Just (collectBinders -> (_,Case _ _ _ [(_,ss,Var s)]))
+              | Just i <- elemIndex s ss -> case realIdUnfolding d of
+#if __GLASGOW_HASKELL__ == 706
+                DFunUnfolding _ _ es -> drop (length es - length ss) (dfunArgExprs es) !! i
+#else
+                DFunUnfolding _ _ es -> drop (length es - length ss) es !! i
+#endif
+                CoreUnfolding{uf_tmpl} ->
+                    let (_,es) = collectArgs uf_tmpl
+                    in  drop (length es - length ss) es !! i
+                x -> e0 -- error $ showOutputable (e0,x)
+            x -> e0 -- error $ showOutputable (e0,x)
+    _ -> e0
+
+
diff --git a/src/Tip/FreeTyCons.hs b/src/Tip/FreeTyCons.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/FreeTyCons.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE PatternGuards #-}
+module Tip.FreeTyCons (bindsTyCons,bindsTyCons',varTyCons,tyTyCons) where
+
+import CoreSyn
+import CoreUtils (exprType)
+import DataCon
+import TyCon
+import Id
+import Type
+import Var
+
+import Data.Set (Set)
+import qualified Data.Set as S
+
+bindsTyCons :: [CoreBind] -> [TyCon]
+bindsTyCons = S.toList . S.unions . map bindTyCons . flattenBinds
+
+bindsTyCons' :: [(Var,CoreExpr)] -> [TyCon]
+bindsTyCons' = S.toList . S.unions . map bindTyCons
+
+bindTyCons :: (Var,CoreExpr) -> Set TyCon
+bindTyCons (v,e) = S.union (exprTyCons e) (varTyCons v)
+
+tyTyCons :: Type -> Set TyCon
+tyTyCons = go . expandTypeSynonyms
+  where
+    go t0
+        | Just (t1,t2) <- splitFunTy_maybe t0    = S.union (go t1) (go t2)
+        | Just (tc,ts) <- splitTyConApp_maybe t0 = S.insert tc (S.unions (map go ts))
+        | Just (_,t) <- splitForAllTy_maybe t0   = go t
+        | otherwise                              = S.empty
+
+varTyCons :: Var -> Set TyCon
+varTyCons = tyTyCons . varType
+
+-- | For all used constructors in expressions and patterns,
+--   return the TyCons they originate from
+exprTyCons :: CoreExpr -> Set TyCon
+exprTyCons e0 = case e0 of
+    Case e x t alts -> S.unions (varTyCons x:tyTyCons t:exprTyCons e:map altTyCons alts)
+    App e1 e2       -> S.union (exprTyCons e1) (exprTyCons e2)
+    Let bs e        -> S.unions (exprTyCons e:map exprTyCons (rhssOfBind bs))
+    Lam _ e         -> exprTyCons e
+    Cast e _        -> exprTyCons e
+    Tick _ e        -> exprTyCons e
+    Var x           -> varTyCons x
+    Type t          -> tyTyCons t
+    Coercion{}      -> S.empty
+    Lit{}           -> tyTyCons (exprType e0)
+
+altTyCons :: CoreAlt -> Set TyCon
+altTyCons (alt,_,rhs) = patTyCons alt `S.union` exprTyCons rhs
+
+patTyCons :: AltCon -> Set TyCon
+patTyCons p = case p of
+    DataAlt c -> S.singleton (dataConTyCon c)
+    LitAlt{}  -> S.empty
+    DEFAULT   -> S.empty
+
diff --git a/src/Tip/GHCScope.hs b/src/Tip/GHCScope.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/GHCScope.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE CPP #-}
+module Tip.GHCScope where
+
+import GHC hiding (Sig)
+
+import Control.Applicative
+import Data.Maybe
+
+import DataCon
+
+#if __GLASGOW_HASKELL__ >= 708
+import ConLike
+#endif
+
+getIdsInScope :: (Id -> Id) -> Ghc [Id]
+getIdsInScope fix_id = do
+
+    ns <- getNamesInScope
+
+    things <- catMaybes <$> mapM lookupName ns
+
+    return [ fix_id i | AnId i <- things ]
+
+parseName' :: String -> Ghc [Name]
+parseName' = handleSourceError (\ _ -> return []) . parseName
+
+inScope :: String -> Ghc Bool
+inScope s = do
+    xs <- parseName' s
+    return $ if null xs then False else True
+
+lookupString :: String -> Ghc [TyThing]
+lookupString s = do
+    xs <- parseName' s
+    catMaybes <$> mapM lookupName xs
+
+thingToId :: TyThing -> Maybe Id
+thingToId (AnId i)     = Just i
+#if __GLASGOW_HASKELL__ >= 708
+thingToId (AConLike (RealDataCon dc)) = Just (dataConWorkId dc)
+thingToId (AConLike (PatSynCon _pc))  = error "HipSpec.Sig.Scope: Pattern synonyms not supported"
+#else
+thingToId (ADataCon dc) = Just (dataConWorkId dc)
+#endif
+thingToId _            = Nothing
+
+mapJust :: (a -> Maybe b) -> [a] -> Maybe b
+mapJust k = listToMaybe . mapMaybe k
+
diff --git a/src/Tip/GHCUtils.hs b/src/Tip/GHCUtils.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/GHCUtils.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE CPP,PatternGuards #-}
+module Tip.GHCUtils where
+
+import Outputable
+
+import Var (varName)
+import Name (Name,getOccString)
+import DataCon
+import Id
+import TyCon
+import Type
+
+#if __GLASGOW_HASKELL__ >= 708
+import DynFlags (unsafeGlobalDynFlags)
+#elif __GLASGOW_HASKELL__ >= 706
+import DynFlags (tracingDynFlags)
+#endif
+
+portableShowSDoc :: SDoc -> String
+#if __GLASGOW_HASKELL__ >= 708
+portableShowSDoc = showSDoc unsafeGlobalDynFlags
+#elif __GLASGOW_HASKELL__ >= 706
+portableShowSDoc = showSDoc tracingDynFlags
+#else
+portableShowSDoc = showSDoc
+#endif
+
+-- | Shows something outputable
+showOutputable :: Outputable a => a -> String
+showOutputable = portableShowSDoc . ppr
+
+varToString :: Var -> String
+varToString = nameToString . varName
+
+nameToString :: Name -> String
+nameToString = getOccString
+
+-- | Is this Id a "constructor" to a newtype?
+--   This is the only way I have found to do it...
+isNewtypeConId :: Id -> Bool
+isNewtypeConId i
+    | Just dc <- isDataConId_maybe i = isNewTyCon (dataConTyCon dc)
+    | otherwise = False
+
+-- | Is this Id a data or newtype constructor?
+--
+--   Note: cannot run isDataConWorkId on things that aren't isId,
+--         then we get a panic from idDetails.
+--
+--         (mainly from type variables)
+isDataConId :: Id -> Bool
+isDataConId v = isId v && (isConLikeId v || isNewtypeConId v)
+
+-- Removes class constraints
+rmClass :: Type -> Type
+rmClass ty = case splitFunTy_maybe ty of
+    Just (t1,t2) | isPredTy t1 -> rmClass t2
+    _ -> ty
+
+-- Has class constraint?
+hasClass :: Type -> Bool
+hasClass ty = case splitFunTy_maybe (snd (splitForAllTys ty)) of
+    Just (t1,t2) -> isPredTy t1
+    _            -> False
+
diff --git a/src/Tip/HaskellFrontend.hs b/src/Tip/HaskellFrontend.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/HaskellFrontend.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE RecordWildCards, DisambiguateRecordFields, NamedFieldPuns #-}
+-- | The Haskell frontend to Tip
+module Tip.HaskellFrontend(readHaskellFile,Id(..),module Tip.Params) where
+
+import Tip.Core
+import Tip.Calls
+import Tip.Compile
+import Tip.CoreToTip
+import Tip.Dicts (inlineDicts)
+import Tip.FreeTyCons
+import Tip.Id
+import Tip.Params
+import Tip.ParseDSL
+import Tip.Property
+import Tip.RemoveDefault
+import Tip.Unfoldings
+import Tip.Uniquify
+import Tip.GHCUtils
+import Tip.Pretty
+
+import Control.Monad
+import Data.Char
+import Data.List (partition,union,delete)
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Maybe (isNothing)
+import System.Directory
+import System.Exit
+import Data.Generics.Geniplate
+
+import qualified Id as GHC
+import qualified CoreSubst as GHC
+import Var (Var)
+import TyCon (isAlgTyCon,isClassTyCon,tyConName)
+import TysWiredIn (boolTyCon)
+import UniqSupply
+
+-- | Transforms a Haskell file to a Tip Theory, crashing if unsuccessful
+readHaskellFile :: Params -> IO (Theory Id)
+readHaskellFile params@Params{..} = do
+
+    -- whenFlag params PrintParams $ putStrLn (ppShow params)
+
+    -- maybe (return ()) setCurrentDirectory directory
+
+    prop_ids <- compileHaskellFile params
+
+    let vars = filterVarSet (not . varInTip) $
+               unionVarSets (map (transCalls Without) prop_ids)
+
+    us0 <- mkSplitUniqSupply 'h'
+
+    let (binds,_us1) = initUs us0 $ sequence
+            [ fmap ((,) v) (runUQ . uqExpr <=< rmdExpr $ inlineDicts e)
+            | v <- varSetElems vars
+            , isNothing (GHC.isClassOpId_maybe v)
+            , Just e <- [maybeUnfolding v]
+            ]
+
+        tcs = filter (\ x -> isAlgTyCon x && not (nameInTip (tyConName x)) && not (isClassTyCon x))
+                     (delete boolTyCon (bindsTyCons' binds))
+
+    when (PrintCore `elem` flags) $ do
+        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"
+        putStrLn (showOutputable binds)
+
+    let tip_data =
+          [ case trTyCon tc of
+              Right tc' -> tc'
+              Left err -> error $ showOutputable tc ++ ": " ++ err
+          | tc <- tcs
+          ]
+
+    let tip_fns0 = concat
+          [ case runTM (trDefn v e) of
+              Right fn -> fn
+              Left err -> error $ showOutputable v ++ ": " ++ err
+          | (v,e) <- binds
+          ]
+
+        -- Now, split these into properties and non-properties
+    let (prop_fns,tip_fns) = partition (isPropType . func_res) tip_fns0
+
+        tip_props = either error id (mapM trProperty prop_fns)
+
+        thy = Theory tip_data [] [Signature Error errorType] tip_fns tip_props
+
+    when (PrintInitialTip `elem` flags) $ do
+        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"
+        putStrLn (ppRender thy)
+
+    return thy
+
diff --git a/src/Tip/Id.hs b/src/Tip/Id.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Id.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE PatternGuards,StandaloneDeriving,CPP #-}
+module Tip.Id where
+
+import Tip.Pretty
+import Tip.Core
+
+import Text.PrettyPrint (text)
+
+import Name hiding (varName)
+import OccName (occNameString)
+-- import BasicTypes (TupleSort(..))
+import PrelNames
+import Tip.GHCUtils
+import Var (Var,varName,idDetails,TyVar,tyVarName)
+import IdInfo (IdDetails(..))
+import TyCon (tyConName,TyCon)
+import DataCon (dataConName,DataCon)
+import Data.Char (toUpper)
+import PrimOp
+
+import TysWiredIn (trueDataCon,falseDataCon,boolTyCon)
+
+idFromName :: Name -> Id
+idFromName nm = GHCOrigin nm
+
+idFromDataCon :: DataCon -> Id
+idFromDataCon = idFromName . dataConName
+
+idFromVar :: Var -> Id
+idFromVar i = case idDetails i of
+    DataConWorkId dc -> idFromDataCon dc
+    DataConWrapId dc -> idFromDataCon dc
+    _                -> idFromName (varName i)
+
+idFromTyVar :: TyVar -> Id
+idFromTyVar = idFromName . tyVarName
+
+idFromTyCon :: TyCon -> Id
+idFromTyCon tc = idFromName (tyConName tc)
+
+tryGetGHCName :: Id -> Maybe Name
+tryGetGHCName (GHCOrigin nm) = Just nm
+tryGetGHCName _              = Nothing
+
+-- | A representation of identifiers that come from GHC.
+--
+-- The 'PrettyVar' instance is one way to print the names.
+data Id
+    = GHCOrigin Name
+    | Id `LiftedFrom` Id
+    | Eta Int
+    | Discrim Id
+    | Project Id Int
+    | Error
+  deriving (Eq,Ord)
+
+instance Show Id where
+    show (GHCOrigin n)      = show (showOutputable n)
+    show (Eta n)            = "eta" ++ show n
+    show (Discrim c)        = "is-" ++ show c
+    show (Project c i)      = show c ++ "_" ++ show i
+    show (i `LiftedFrom` j) = show i ++ " `LiftedFrom` " ++ show j
+    show Error              = "error"
+
+instance PrettyVar Id where
+    varStr = ppId
+
+ppId :: Id -> String
+ppId (GHCOrigin nm) = ppName nm
+ppId (Eta n)        = "eta" ++ show n
+ppId (Discrim c)    = "is-" ++ ppId c
+ppId ((i `LiftedFrom` j) `LiftedFrom` k) = ppId (i `LiftedFrom` (j `LiftedFrom` k))
+ppId (i `LiftedFrom` j)
+  | Just nm <- tryGetGHCName i, isSystemName nm    = ppId j
+  | ppId i /= ppId j && "prop_" /= take 5 (ppId j) = ppId j ++ "_" ++ ppId i
+  | otherwise                                      = ppId i
+ppId (Project c i)  = case (i,ppId c) of
+                        (0,"Pair") -> "first"
+                        (1,"Pair") -> "second"
+                        (0,"cons") -> "head"
+                        (1,"cons") -> "tail"
+                        (0,"S")    -> "p"
+                        (0,"Succ") -> "pred"
+                        _          -> ppId c ++ "_" ++ show i
+ppId Error = "error"
+
+ppName :: Name -> String
+ppName nm
+    | k == listTyConKey      = "list"
+    | k == nilDataConKey     = "nil"
+    | k == consDataConKey    = "cons"
+    | k == unitTyConKey      = "Unit"
+    | k == genUnitDataConKey = "tt"
+    | isSystemName nm        = "x"
+    | otherwise = case getOccString nm of
+        x | take 2 x == "ds"  -> "x"
+        x | take 3 x == "ipv" -> "x"
+        "(,)"  -> "Pair"
+        "(,,)" -> "Triple"
+        "+"   -> "plus"
+        "-"   -> "minus"
+        "/"   -> "div"
+        "*"   -> "mult"
+        "^"   -> "pow"
+        "++"  -> "append"
+        ">>=" -> "bind"
+        "=<<" -> "dnib"
+        ">=>" -> "dot_monadic"
+        "<=<" -> "monadic_dot"
+        "<*>" -> "ap"
+        "<$>" -> "fmap"
+        ">>"  -> "then"
+        "||"  -> "or"
+        "&&"  -> "and"
+        "."   -> "dot"
+        "=="  -> "equal"
+        "/="  -> "unequal"
+        ">"   -> "gt"
+        ">="  -> "ge"
+        "<"   -> "lt"
+        "<="  -> "le"
+        "$"   -> "apply"
+        "!!"  -> "index"
+        "\\\\" -> "difference"
+        s     -> s
+  where
+    k = getUnique nm
+
+primops :: [(PrimOp,Expr Id)]
+primops =
+  [ (ghc_op,Lam [int 0] (Lam [int 1] (Builtin tip_id :@: [Lcl (int 0),Lcl (int 1)])))
+  | (ghc_op,tip_id) <-
+    [ (IntAddOp, IntAdd)
+    , (IntSubOp, IntSub)
+    , (IntMulOp, IntMul)
+    ]
+  ] ++
+#if __GLASGOW_HASKELL__ <= 706
+  [ (ghc_op,Lam [int 0] (Lam [int 1] (Builtin tip_id :@: [Lcl (int 0),Lcl (int 1)])))
+  | (ghc_op,tip_id) <-
+    [ (IntEqOp, Equal)
+    , (IntNeOp, Distinct)
+    , (IntGtOp, IntGt)
+    , (IntGeOp, IntGe)
+    , (IntLtOp, IntLt)
+    , (IntLeOp, IntLe)
+    ]
+  ]
+#else
+  [ (ghc_op,Lam [int 0] (Lam [int 1]
+              (makeIf (Builtin tip_id :@: [Lcl (int 0),Lcl (int 1)])
+                      (literal (Int 1)) (literal (Int 0)))))
+  | (ghc_op,tip_id) <-
+    [ (IntEqOp, Equal)
+    , (IntNeOp, Distinct)
+    , (IntGtOp, IntGt)
+    , (IntGeOp, IntGe)
+    , (IntLtOp, IntLt)
+    , (IntLeOp, IntLe)
+    ]
+  ] ++
+  [ (TagToEnumOp,Lam [int 0] (Match (Lcl (int 0))
+                                [ Case Default          (bool False)
+                                , Case (LitPat (Int 1)) (bool True)
+                                ]))
+  ]
+#endif
+ where
+  int i = Local (Eta i) intType
+
diff --git a/src/Tip/Params.hs b/src/Tip/Params.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Params.hs
@@ -0,0 +1,31 @@
+module Tip.Params where
+
+-- | Parameters
+data Params = Params
+  { file        :: FilePath
+  -- ^ File to process
+  , include     :: [FilePath]
+  -- ^ Directories to include
+  , flags       :: [DebugFlags]
+  -- ^ Debugging flags
+  , only        :: [String]
+  -- ^ Only consider these properties
+  , extra       :: [String]
+  -- ^ Also translate these functions and its transitive dependencies
+  }
+  deriving Show
+
+-- | Default parameters, given the name of the file to process
+defaultParams :: FilePath -> Params
+defaultParams fp = Params
+  { file = fp
+  , include = []
+  , flags = []
+  , only = []
+  , extra = []
+  }
+
+-- | Debugging flags
+data DebugFlags = PrintCore | PrintProps | PrintExtraIds | PrintInitialTip
+  deriving (Eq,Show)
+
diff --git a/src/Tip/ParseDSL.hs b/src/Tip/ParseDSL.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/ParseDSL.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE ViewPatterns #-}
+module Tip.ParseDSL where
+
+import Tip.GHCUtils
+import Tip.Id
+import Tip.Core
+import qualified Tip.CoreToTip as CTT
+
+import qualified Data.Foldable as F
+
+import Name hiding (varName)
+import Data.List
+
+import Var hiding (Id,isId)
+import TyCon (TyCon)
+
+import Module
+
+nameInTip :: Name -> Bool
+nameInTip = F.any (\ n -> moduleNameString (moduleName n) == "Tip") . nameModule_maybe
+
+varInTip :: Var -> Bool
+varInTip = nameInTip . varName
+
+idInTip :: Id -> Bool
+idInTip = F.any nameInTip . tryGetGHCName
+
+isId :: String -> Id -> Bool
+isId s i = F.any (nameIs s) (tryGetGHCName i)
+
+oneOf :: String -> String -> Id -> Bool
+oneOf s1 s2 i = any (`isId` i) [s1,s2]
+
+nameIs :: String -> Name -> Bool
+nameIs s n = nameInTip n && s == occNameString (nameOccName n)
+
+varIs :: String -> Var -> Bool
+varIs s v = nameIs s (varName v)
+
+isPropType :: Type Id -> Bool
+isPropType = goo 0 . res
+  where
+  go = goo 1
+  goo i (BuiltinType Boolean) = i > 0
+  goo i (TyCon tc [t1]) =  isId "Equality" tc || (isId "Neg" tc && go t1)
+  goo i (TyCon tc [t1,t2]) =
+    let ok xs = or [ isId s tc | s <- xs ]
+    in     (ok ["And","Or",":=>:"] && go t1 && go t2)
+        || (ok ["Forall","Exists"] && go t2)
+  goo i _ = False
+
+  res (_ :=>: r) = res r
+  res r          = r
+
+isPropTyCon :: Var -> Bool
+isPropTyCon v =
+    or [ varIs s v
+       | s <- ["Equality","Neg","And","Or",":=>:","Forall","Exists"]
+       ]
+
+varWithPropType :: Var -> Bool
+varWithPropType x = case CTT.trPolyType (varType x) of
+    Right (PolyType _ _ t) -> isPropType t
+    _                      -> False
+
diff --git a/src/Tip/Property.hs b/src/Tip/Property.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Property.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE RecordWildCards, PatternGuards, ViewPatterns #-}
+module Tip.Property where
+
+import Tip.Core
+import Tip.Id
+import Tip.Pretty
+import Tip.Pretty.SMT
+
+import Tip.ParseDSL
+import Tip.GHCUtils
+
+import Control.Monad.Error
+import Control.Applicative
+import Data.Foldable (Foldable)
+import Data.List (intercalate,union)
+import Data.Map (Map)
+import Data.Maybe (mapMaybe)
+import Data.Traversable (Traversable)
+import qualified Data.Map as M
+-- import Text.PrettyPrint hiding (comma)
+
+import Var (Var)
+import TysWiredIn (trueDataCon,falseDataCon,boolTyCon)
+-- import DataCon (dataConName)
+
+-- | Translates a property that has been translated to a simple function earlier
+trProperty :: Function Id -> Either String (Formula Id)
+trProperty (Function _name tvs [] res_ty b) = case unLam b of
+  (args,e) -> do
+    pr <- parseProperty e
+    return (Formula Prove tvs (mkQuant Forall args pr))
+  where
+    unLam (Lam xs e) = let (ys,e') = unLam e in (xs ++ ys,e')
+    unLam e          = ([],e)
+
+-- | Tries to "parse" a property in the simple expression format
+parseProperty :: Expr Id -> Either String (Expr Id)
+parseProperty = goo 0
+  where
+  go = goo 1
+  goo i e0@(projAt -> Just (projGlobal -> Just x,Lam bs e))
+
+      | isId "forAll" x || isId "Forall" x = mkQuant Forall bs <$> go e
+
+      | isId "exists" x || isId "Exists" x = mkQuant Exists bs <$> go e
+
+  goo i e0@(projAt -> Just (projGlobal -> Just x,e))
+
+      | isId "bool" x = return e
+
+      | isId "Neg" x || isId "neg" x = neg <$> go e
+
+  goo i e0@(projAt -> Just (projAt -> Just (projGlobal -> Just x,e1),e2))
+
+      | isId "===" x || isId ":=:" x = return (e1 === e2)
+
+      | isId "=/=" x                 = return (e1 =/= e2)
+
+      | isId "==>" x || isId "Given" x = (==>) <$> go e1 <*> go e2
+
+      | isId ".&&." x || isId "And" x  = (/\) <$> go e1 <*> go e2
+
+      | isId ".||." x || isId "Or" x   = (\/) <$> go e1 <*> go e2
+
+  goo i e0 | i > 0 && exprType e0 == boolType = return e0
+
+  goo i e0 = throwError $ "Cannot parse property: " ++ ppRender e0
+
diff --git a/src/Tip/RemoveDefault.hs b/src/Tip/RemoveDefault.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/RemoveDefault.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE ScopedTypeVariables, PackageImports #-}
+{-
+
+    Annoyances with the Default branch:
+
+        * Functions that should be equal are not, such as f and g here:
+
+            f x = case x of
+                True -> e
+                _    -> e'
+
+            g x = case x of
+                True  -> e
+                False -> e'
+
+        * GHC Core likes to recase on a variable that is already known, such as here:
+
+            h x = case x of
+                True -> True
+                _ -> case x of
+                    False -> False
+                    _ -> undefined
+
+          The call to undefined can never be reached here. Such cases should be
+          removed. It also lead to a problem in the contracts checker:
+
+          The last branch to BAD will never happen, but the alternative
+          was translated to:
+
+             ! [X] : ((X != True & X != False & X != UNR & X != BAD) => h(X) = BAD)
+
+          I.e. for some untyped point *, we get h(*) = BAD, which is bad
+          because now the true contract h ::: CF --> CF is satisfiable.
+          Disaster!
+
+          By unrolling all constructors, we get this:
+
+              f = \ x -> case x of
+                  True -> True
+                  False -> case x of
+                      False -> False
+                      True -> BAD
+
+          Now, x can be inlined by known-case.
+
+    We need to do this in a m monad to put some variables in the
+    bound fields of alternatives.
+
+    TODO: We currently look at some data constructor's type constructor,
+    which means we can get a problem if we have
+
+        case e of { _ -> e' },
+
+    we could check the type of e instead. If it is a type constructor
+    with data constructors, we could unroll it.
+
+-}
+module Tip.RemoveDefault where
+
+import Tip.DataConPattern
+import Tip.GHCUtils
+
+import CoreSyn
+import CoreUtils hiding (findAlt)
+import DataCon
+import FastString
+import TyCon
+import Type
+import Unique
+import UniqSupply
+import Id
+
+import Control.Monad
+import Control.Applicative
+
+removeDefaults :: (Applicative m,MonadUnique m) => [CoreBind] -> m [CoreBind]
+removeDefaults = mapM rmdBind
+
+rmdBind :: (Applicative m,MonadUnique m) => CoreBind -> m CoreBind
+rmdBind (NonRec f e) = NonRec f <$> rmdExpr e
+rmdBind (Rec fses)   = Rec <$> mapM (\ (f,e) -> (,) f <$> rmdExpr e) fses
+
+rmdExpr :: (Applicative m,MonadUnique m) => CoreExpr -> m CoreExpr
+rmdExpr e0 = case e0 of
+    App e1 e2       -> App <$> rmdExpr e1 <*> rmdExpr e2
+    Lam x e         -> Lam x <$> rmdExpr e
+    Let b e         -> Let <$> rmdBind b <*> rmdExpr e
+    Case s t w alts -> Case <$> rmdExpr s <.> t <.> w
+                            <*> (mapM rmdAlt <=< unrollDefault (exprType s)) alts
+    Cast e c        -> Cast <$> rmdExpr e <.> c
+    Tick t e        -> Tick t <$> rmdExpr e
+
+    Type{}          -> return e0
+    Var{}           -> return e0
+    Lit{}           -> return e0
+    Coercion{}      -> return e0
+
+rmdAlt :: (Applicative m,MonadUnique m) => CoreAlt -> m CoreAlt
+rmdAlt (ac,bs,rhs) = (,,) ac bs <$> rmdExpr rhs
+
+infixl 4 <.>
+(<.>) :: Applicative f => f (a -> b) -> a -> f b
+f <.> x = f <*> pure x
+
+unrollDefault :: forall m . (Applicative m,MonadUnique m) => Type -> [CoreAlt] -> m [CoreAlt]
+unrollDefault t alts0 = case findDefault alts0 of
+    (alts,Just def_rhs) -> case alts of
+        (DataAlt dc,_,_):_ | missing (dataConTyCon dc) alts <= 1 -> unroll (dataConTyCon dc) alts def_rhs
+        (LitAlt _  ,_,_):_ -> return alts0
+        (DEFAULT   ,_,_):_ -> error "RemoveDefault.unrollDefault: duplicate DEFAULT"
+        _                  -> return alts0
+            -- only DEFAULT, this can be remedied by looking at the TyCon from
+            -- the case scrutinee expression's type
+    (alts,_)      -> return alts
+  where
+    missing :: TyCon -> [CoreAlt] -> Int
+    missing ty_con alts = case tyConDataCons_maybe ty_con of
+        Just dcs -> sum [ 1 | Nothing <- map (findAlt alts) dcs ]
+        Nothing  -> error "RemoveDefault.unrollDefault: non-data TyCon?"
+
+    unroll :: TyCon -> [CoreAlt] -> CoreExpr -> m [CoreAlt]
+    unroll ty_con alts rhs = case tyConDataCons_maybe ty_con of
+        Just dcs -> forM dcs $ \ dc ->
+            fromMaybeM (makeAlt t rhs dc) (findAlt alts dc)
+        Nothing  -> error "RemoveDefault.unrollDefault: non-data TyCon?"
+            -- This could be remedied by just returning alts here,
+            -- but it would be interesting what this ty_con really is,
+            -- maybe we can do something better
+
+findAlt :: [CoreAlt] -> DataCon -> Maybe CoreAlt
+findAlt (alt@(DataAlt dc',_,_):_) dc | dc' == dc = Just alt
+findAlt (_:alts) dc = findAlt alts dc
+findAlt []       _  = Nothing
+
+fromMaybeM :: (Applicative m,MonadUnique m) => Monad m => m a -> Maybe a -> m a
+fromMaybeM _ (Just x) = return x
+fromMaybeM m Nothing  = m
+
+makeAlt :: (Applicative m,MonadUnique m) => Type -> CoreExpr -> DataCon -> m CoreAlt
+makeAlt t rhs dc = case dcAppliedTo t dc of
+    (_,Just s) -> do
+        bound <- mapM (\ ty -> dummy_var (substTy s ty) <$> getUniqueM) (dataConRepArgTys dc)
+        return (DataAlt dc,bound,rhs)
+    _ -> error $ "RemoveDefault.makeAlt unification error:"
+                 ++ "\n\t" ++ showOutputable t
+                 ++ "\n\t" ++ showOutputable dc
+  where
+    dummy_var :: Type -> Unique -> Var
+    dummy_var ty u = mkSysLocal (fsLit "d") u ty
+
diff --git a/src/Tip/TyAppBeta.hs b/src/Tip/TyAppBeta.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/TyAppBeta.hs
@@ -0,0 +1,36 @@
+
+-- | Beta reduction for types (applied to lambdas)
+module Tip.TyAppBeta where
+
+import Type
+
+import CoreSyn
+import qualified CoreSubst as CS
+import qualified Outputable
+
+-- | Beta reduction for types (applied to lambdas)
+tyAppBeta :: CoreExpr -> CoreExpr
+tyAppBeta = go
+  where
+    go e0 = case e0 of
+        App e1 e2 -> case (go e1,go e2) of
+            (Lam x e,Type t) -> reduce x e t
+            (e1',e2')        -> App e1' e2'
+        Lam x e         -> Lam x (go e)
+        Tick tk e       -> Tick tk (go e)
+        Cast e co       -> Cast (go e) co
+        Case e x t alts -> Case (go e) x t [ (p,bs,go rhs) | (p,bs,rhs) <- alts ]
+        Let b e         -> Let (go' b) (go e)
+        Var{}           -> e0
+        Lit{}           -> e0
+        Coercion{}      -> e0
+        Type{}          -> e0
+
+    go' b = case b of
+        NonRec v e -> NonRec v (go e)
+        Rec vses   -> Rec [ (v,go e) | (v,e) <- vses ]
+
+-- | Reduces a type variable in an expression by applying it to a type
+reduce :: TyVar -> CoreExpr -> Type -> CoreExpr
+reduce x e t = CS.substExpr Outputable.empty su e
+  where su = CS.extendTvSubst CS.emptySubst x t
diff --git a/src/Tip/Unfoldings.hs b/src/Tip/Unfoldings.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Unfoldings.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Tip.Unfoldings (unfolding,maybeUnfolding,fixUnfoldings,fixId) where
+
+import qualified Data.Map as M
+
+import Control.Applicative
+import Data.Traversable (sequenceA)
+
+import Control.Monad.Reader
+
+import CoreSyn
+import CoreUnfold
+import Id
+
+import Data.Maybe
+
+import Tip.GHCUtils
+import Tip.Dicts
+
+-- | The unfolding of an Id
+unfolding :: Id -> CoreExpr
+unfolding i  = fromMaybe (error err) . maybeUnfolding $ i
+  where
+    err = "No unfolding for identifier " ++ showOutputable i ++
+          " (possible solution: Remove *.hi files and try again)"
+
+
+-- | Fixes identifiers according to some core binds
+fixId :: [(Var,CoreExpr)] -> Id -> Id
+fixId bs = \ i -> case M.lookup i bind_map of
+    Just rhs -> i `setIdUnfoldingLazily` mkInlineUnfolding Nothing rhs
+    Nothing  -> i
+  where
+    bind_map = M.fromList bs
+
+-- | Ties the knot, fixes all the unfoldings in these core binds
+fixUnfoldings :: [(Var,CoreExpr)] -> [(Var,CoreExpr)]
+fixUnfoldings bs = map (idMap lkup) bs'
+  where
+    bs' :: [(Var,CoreExpr)]
+    bs' = mapM (exprMap k) bs lkup
+
+    lkup :: Id -> Id
+    lkup = fixId bs'
+
+    h :: Id -> (Id -> Id) -> Id
+    h x = do
+        m <- ask
+        return (m x)
+
+    k :: CoreExpr -> (Id -> Id) -> CoreExpr
+    k = boringCases h k
+
+-- | Maps an expression fun over binds
+exprMap :: Applicative f => (CoreExpr -> f CoreExpr) -> (Var,CoreExpr) -> f (Var,CoreExpr)
+exprMap f (v,e) = (,) v <$> f e
+
+-- | Maps an identifier fun over binds
+idMap :: (Id -> Id) -> (Var,CoreExpr) -> (Var,CoreExpr)
+idMap f (v,e) = (f v,e)
+
+bindMap :: Applicative f => (CoreExpr -> f CoreExpr) -> CoreBind -> f CoreBind
+bindMap f (NonRec v e) = NonRec v <$> f e
+bindMap f (Rec vses)   = Rec <$> sequenceA [ (,) v <$> f e | (v,e) <- vses ]
+
+{-
+-- | Maps an expression fun over binds
+exprMap :: Applicative f => (CoreExpr -> f CoreExpr) -> CoreBind -> f CoreBind
+exprMap f (NonRec v e) = NonRec v <$> f e
+exprMap f (Rec vses)   = Rec <$> sequenceA [ (,) v <$> f e | (v,e) <- vses ]
+
+-- | Maps an identifier fun over binds
+idMap :: (Id -> Id) -> CoreBind -> CoreBind
+idMap f (NonRec v e) = NonRec (f v) e
+idMap f (Rec vses)   = Rec [ (f v,e) | (v,e) <- vses ]
+-}
+
+-- | Fills in all boring cases for you
+boringCases :: Applicative f => (Var -> f Var) -> (CoreExpr -> f CoreExpr) -> CoreExpr -> f CoreExpr
+boringCases h f t = case t of
+    Var x -> Var <$> h x
+    Lit{} -> pure t
+    App e1 e2 -> App <$> f e1 <*> f e2
+    Lam x e -> Lam x <$> f e
+    Let bs e -> Let <$> bindMap f bs <*> f e
+    Case s ty w alts ->
+        (\s' alts' -> Case s' ty w alts')
+            <$> f s
+            <*> sequenceA [ (,,) p bs <$> f e | (p,bs,e) <- alts ]
+    Cast e co -> (`Cast` co) <$> f e
+    Tick tk e -> Tick tk <$> f e
+    Type{} -> pure t
+    Coercion{} -> pure t
+
diff --git a/src/Tip/Uniquify.hs b/src/Tip/Uniquify.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Uniquify.hs
@@ -0,0 +1,67 @@
+-- | One could think that every identifier in GHC Core is supposed to be Unique,
+-- but this is not the case. This module cleans up this mess.
+--
+-- The targets are local lets that happily gets the same name, and also
+-- scrutinee vars that can get the same name if they are never used.
+module Tip.Uniquify where
+
+import CoreSyn
+
+import UniqSupply
+
+import Var
+
+import Control.Monad.Reader
+import Control.Applicative
+
+import Data.Map (Map)
+import qualified Data.Map as M
+
+import Data.Maybe (fromMaybe)
+
+type UQ m a = ReaderT (Map Var Var) m a
+
+runUQ :: (Applicative m,MonadUnique m) => UQ m a -> m a
+runUQ m = runReaderT m M.empty
+
+insertVar :: (Applicative m,MonadUnique m) => Var -> UQ m a -> UQ m a
+insertVar x m = do
+    my <- asks (M.lookup x)
+    x' <- case my of
+        Just{} -> do
+            u <- lift getUniqueM
+            return (setVarUnique x u)
+        Nothing -> return x
+    local (M.insert x x') m
+
+insertVars :: (Applicative m,MonadUnique m) => [Var] -> UQ m a -> UQ m a
+insertVars xs m = foldr insertVar m xs
+
+lookupVar :: (Applicative m,MonadUnique m) => Var -> UQ m Var
+lookupVar x = fromMaybe x <$> asks (M.lookup x)
+
+uqBind :: (Applicative m,MonadUnique m) => CoreBind -> (CoreBind -> UQ m a) -> UQ m a
+uqBind (NonRec v e) k = insertVar v (k =<< NonRec <$> lookupVar v <*> uqExpr e)
+uqBind (Rec vses)   k = insertVars (map fst vses) $ k . Rec =<< sequence
+    [ (,) <$> lookupVar v <*> uqExpr e | (v,e) <- vses ]
+
+uqExpr :: (Applicative m,MonadUnique m) => CoreExpr -> UQ m CoreExpr
+uqExpr e0 = case e0 of
+    Var x           -> Var <$> lookupVar x
+    App e1 e2       -> App <$> uqExpr e1 <*> uqExpr e2
+    Let bs e        -> uqBind bs $ \ bs' -> Let bs' <$> uqExpr e
+    Lam x e         -> insertVar x (Lam <$> lookupVar x <*> uqExpr e)
+    Case s x t alts -> do
+        s' <- uqExpr s
+        insertVar x $ do
+            x' <- lookupVar x
+            Case s' x' t <$> mapM uqAlt alts
+    Cast e c        -> (`Cast` c) <$> uqExpr e
+    Tick tk e       -> Tick tk <$> uqExpr e
+    Type{}          -> return e0
+    Lit{}           -> return e0
+    Coercion{}      -> return e0
+
+uqAlt :: (Applicative m,MonadUnique m) => CoreAlt -> UQ m CoreAlt
+uqAlt (pat,bs,e) = insertVars bs ((,,) pat <$> mapM lookupVar bs <*> uqExpr e)
+
diff --git a/tip-haskell-frontend.cabal b/tip-haskell-frontend.cabal
new file mode 100644
--- /dev/null
+++ b/tip-haskell-frontend.cabal
@@ -0,0 +1,64 @@
+name:                tip-haskell-frontend
+version:             0.1
+license:             BSD3
+license-file:        LICENSE
+author:              Dan Rosén
+maintainer:          danr@chalmers.se
+build-type:          Simple
+cabal-version:       >=1.10
+description:         Convert from Haskell to Tip
+synopsis:            Convert from Haskell to Tip
+homepage:            http://tip-org.github.io
+bug-reports:         http://github.com/tip-org/tools/issues
+category:            Theorem Provers
+
+source-repository head
+  type:     git
+  location: http://github.com/tip-org/tools
+
+library
+  exposed-modules:
+    Tip.HaskellFrontend
+    Tip
+  other-modules:
+    Tip.Params
+    Tip.Id
+    Tip.GHCUtils
+    Tip.Calls
+    Tip.Compile
+    Tip.CoreToTip
+    Tip.DataConPattern
+    Tip.Dicts
+    Tip.FreeTyCons
+    Tip.ParseDSL
+    Tip.Property
+    Tip.RemoveDefault
+    Tip.GHCScope
+    Tip.TyAppBeta
+    Tip.Unfoldings
+    Tip.Uniquify
+  hs-source-dirs:      src
+  include-dirs:        src
+  default-language:    Haskell2010
+  build-depends:       base >=4 && <5,
+                       ghc,
+                       ghc-paths >=0.1,
+                       containers >=0.4,
+                       filepath >=1.3,
+                       directory >=1.1,
+                       pretty >=1.1,
+                       mtl >=2.1,
+                       bytestring >=0.9.2,
+                       split >=0.2,
+                       geniplate-mirror >=0.7.1,
+                       tip-lib == 0.1,
+                       QuickCheck >= 2.8
+
+executable tip-ghc
+  main-is:             executable/Main.hs
+  default-language:    Haskell2010
+  build-depends:       base,
+                       tip-haskell-frontend,
+                       tip-lib,
+                       pretty-show,
+                       pretty