diff --git a/changelog b/changelog
--- a/changelog
+++ b/changelog
@@ -1,3 +1,9 @@
+tip-haskell-frontend 0.2 (released 2015-10-28):
+* Depend on ghc-simple by Anton Ekblad, and simplify the internals.
+* Export readHaskellOrTipFile.
+* Add Tip.Prelude
+* Add question (synonymous to neg)
+
 tip-haskell-frontend 0.1.1 (released 2015-06-11):
 * Relax dependency on tip-lib to >= 0.1.1 && <= 0.2.
 
diff --git a/executable/Main.hs b/executable/Main.hs
--- a/executable/Main.hs
+++ b/executable/Main.hs
@@ -20,36 +20,44 @@
 import Tip.Pretty
 import Tip.Pretty.SMT as SMT
 
-import Text.PrettyPrint
+import Text.PrettyPrint hiding ((<>))
 
+import Options.Applicative
+
 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))
+    (file,params) <-
+      execParser $
+        info (helper <*>
+                ((,) <$> strArgument (metavar "FILENAME" <> help "Haskell file to process")
+                     <*> parseParams))
+          (fullDesc <>
+           progDesc "Translate Haskell to TIP" <>
+           header "tip-ghc - translate Haskell to TIP")
+    mthy <- readHaskellFile file params
+    case mthy of
+      Left s -> error s
+      Right thy -> do
+        when (PrintInitialTheory `elem` debug_flags params) $ 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
+                  ]
+        case pipeline renamed_thy of
+          [thy'] -> print (SMT.ppTheory thy')
+          _      -> error "tip-ghc: not one theory!"
 
 data Var = Var String | Refresh Var Int
   deriving (Show,Eq,Ord)
diff --git a/src/Tip.hs b/src/Tip.hs
--- a/src/Tip.hs
+++ b/src/Tip.hs
@@ -15,6 +15,7 @@
     , (.&&.)
     , (.||.)
     , neg
+    , question
     , forAll
     , exists
     , module Test.QuickCheck
@@ -67,6 +68,10 @@
 -- | Negation
 neg :: a -> Neg a
 neg = Neg
+
+-- | Question (same as negation)
+question :: a -> Neg a
+question = Neg
 
 -- | Universal quantification
 forAll :: (a -> b) -> Forall a b
diff --git a/src/Tip/Calls.hs b/src/Tip/Calls.hs
deleted file mode 100644
--- a/src/Tip/Calls.hs
+++ /dev/null
@@ -1,58 +0,0 @@
-{-# 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
deleted file mode 100644
--- a/src/Tip/Compile.hs
+++ /dev/null
@@ -1,175 +0,0 @@
-{-# 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
--- a/src/Tip/CoreToTip.hs
+++ b/src/Tip/CoreToTip.hs
@@ -121,6 +121,11 @@
             }
 
 -- | Translate a definition
+--
+-- This does not work when
+-- f = g
+-- when it "should" be
+-- f = /\ a . g @a
 trDefn :: Var -> CoreExpr -> TM [Function Id]
 trDefn v e = do
     let (tvs,ty) = splitForAllTys (C.exprType e)
diff --git a/src/Tip/Dicts.hs b/src/Tip/Dicts.hs
--- a/src/Tip/Dicts.hs
+++ b/src/Tip/Dicts.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleContexts, NamedFieldPuns #-}
 {-# LANGUAGE CPP #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-module Tip.Dicts (inlineDicts,maybeUnfolding) where
+module Tip.Dicts (inlineDicts,maybeUnfolding,varFromRealModule) where
 
 import Tip.GHCUtils (showOutputable)
 #if __GLASGOW_HASKELL__ >= 708
@@ -26,18 +26,6 @@
 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
@@ -47,12 +35,13 @@
     ri = realIdUnfolding v
 
 
+varFromRealModule :: Var -> String -> Bool
+varFromRealModule x s = getOccString x == s && nameModule_maybe (varName x) == Just gHC_REAL
 
 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
+        | any (varFromRealModule f) ["mod","div"] -> Var f
 #if __GLASGOW_HASKELL__ >= 708
         | [try] <- [ try | BuiltinRule _ _ 2 try <- idCoreRules f ]
         , Just e <- try unsafeGlobalDynFlags (emptyInScopeSet,realIdUnfolding) f [Type t,Var d]
diff --git a/src/Tip/FreeTyCons.hs b/src/Tip/FreeTyCons.hs
--- a/src/Tip/FreeTyCons.hs
+++ b/src/Tip/FreeTyCons.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE PatternGuards #-}
-module Tip.FreeTyCons (bindsTyCons,bindsTyCons',varTyCons,tyTyCons) where
+{-# LANGUAGE ScopedTypeVariables #-}
+module Tip.FreeTyCons (bindsTyCons) where
 
 import CoreSyn
 import CoreUtils (exprType)
@@ -12,48 +13,36 @@
 import Data.Set (Set)
 import qualified Data.Set as S
 
-bindsTyCons :: [CoreBind] -> [TyCon]
-bindsTyCons = S.toList . S.unions . map bindTyCons . flattenBinds
+import Tip.GenericInstances
+import Data.Generics.Geniplate
 
-bindsTyCons' :: [(Var,CoreExpr)] -> [TyCon]
-bindsTyCons' = S.toList . S.unions . map bindTyCons
+import Tip.Utils
 
-bindTyCons :: (Var,CoreExpr) -> Set TyCon
-bindTyCons (v,e) = S.union (exprTyCons e) (varTyCons v)
+bindsTyCons :: [(Var,CoreExpr)] -> [TyCon]
+bindsTyCons vses = S.toList $ S.unions
+  [ varTyCons v `S.union` exprTyCons e
+  | (v,e) <- vses
+  ]
 
+varTyCons :: Var -> Set TyCon
+varTyCons = tyTyCons . varType
+
 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
+  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
 
 -- | 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
+exprTyCons e =
+  S.unions $
+    [ varTyCons x `S.union` tyTyCons t | Case _ x t _  <- universeBi e ] ++
+    [ varTyCons x                      | Var x :: CoreExpr <- universeBi e ] ++
+    [ tyTyCons t                       | Type t :: CoreExpr <- universeBi e ] ++
+    [ S.singleton (dataConTyCon c) | DataAlt c <- universeBi e ]
 
diff --git a/src/Tip/GHCScope.hs b/src/Tip/GHCScope.hs
deleted file mode 100644
--- a/src/Tip/GHCScope.hs
+++ /dev/null
@@ -1,49 +0,0 @@
-{-# 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/GenericInstances.hs b/src/Tip/GenericInstances.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/GenericInstances.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE PatternGuards, TypeSynonymInstances, FlexibleInstances, ViewPatterns, ExplicitForAll #-}
+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleContexts, NamedFieldPuns #-}
+-- | Data.Generic.Geniplate instances for GHC
+module Tip.GenericInstances (module Tip.GenericInstances, module Data.Generics.Geniplate) where
+
+import CoreSyn
+import Data.Generics.Geniplate
+
+import Var
+import Coercion
+import Id
+import Literal
+import Type
+import DataCon
+
+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)]) |]
+
+instanceUniverseBiT
+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|AltCon|] ]
+    [t| forall a . (Expr a,Expr a) |]
+
+instanceUniverseBiT
+    [ [t|Var|], [t|Coercion|] , [t|Tickish Id|], [t|Literal|], [t|Type|], [t|DataCon|] ]
+    [t| forall a . (Expr a,AltCon) |]
diff --git a/src/Tip/HaskellFrontend.hs b/src/Tip/HaskellFrontend.hs
--- a/src/Tip/HaskellFrontend.hs
+++ b/src/Tip/HaskellFrontend.hs
@@ -1,93 +1,188 @@
 {-# LANGUAGE RecordWildCards, DisambiguateRecordFields, NamedFieldPuns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
 -- | The Haskell frontend to Tip
-module Tip.HaskellFrontend(readHaskellFile,Id(..),module Tip.Params) where
+module Tip.HaskellFrontend(readHaskellFile,readHaskellOrTipFile,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 Language.Haskell.GHC.Simple hiding (Id) -- Thanks, Anton!
+import qualified Language.Haskell.GHC.Simple as Simple
+
+import Tip.Utils
 import Tip.Id
 import Tip.Params
+import Tip.Core
+import Tip.CoreToTip
+
 import Tip.ParseDSL
 import Tip.Property
-import Tip.RemoveDefault
-import Tip.Unfoldings
-import Tip.Uniquify
+
 import Tip.GHCUtils
-import Tip.Pretty
 
+import CoreFVs
+import VarSet
+import UniqSupply
+
+import Data.List
+import Data.Either
+
+import Tip.Dicts
+import Tip.Uniquify
+import Tip.RemoveDefault
+import Tip.FreeTyCons
+
+import TysWiredIn (boolTyCon,listTyCon)
+
 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 Tip.GenericInstances
 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
+import qualified Data.Foldable as F
 
--- | Transforms a Haskell file to a Tip Theory, crashing if unsuccessful
-readHaskellFile :: Params -> IO (Theory Id)
-readHaskellFile params@Params{..} = do
+import qualified Tip.Parser as TipP
 
-    -- whenFlag params PrintParams $ putStrLn (ppShow params)
+import System.FilePath
 
-    -- maybe (return ()) setCurrentDirectory directory
+-- | If the file cannot be read as a TIP file, it is instead read as a Haskell file.
+readHaskellOrTipFile :: FilePath -> Params -> IO (Either String (Theory (Either TipP.Id Id)))
+readHaskellOrTipFile file params =
+  let ext = takeExtension file in
+  if ext == ".smt2" then
+    fmap (fmap (fmap Left)) (TipP.parseFile file)
+  else if ext == ".hs" || ext == ".lhs" then
+    fmap (fmap (fmap Right)) (readHaskellFile file params)
+  else
+    do mthy1 <- TipP.parseFile file
+       case mthy1 of
+         Right thy -> return (Right (fmap Left thy))
+         Left err1 ->
+           do mthy2 <- readHaskellFile file params
+              case mthy2 of
+                Right thy -> return (Right (fmap Right thy))
+                Left err2 -> return (Left (err1 ++ "\n" ++ err2))
 
-    prop_ids <- compileHaskellFile params
+-- | Transforms a Haskell file to a Tip Theory or an error
+readHaskellFile :: FilePath -> Params -> IO (Either String (Theory Id))
+readHaskellFile file params@Params{..} = do
 
-    let vars = filterVarSet (not . varInTip) $
-               unionVarSets (map (transCalls Without) prop_ids)
+  let cfg :: CompConfig ModGuts
+      cfg = defaultConfig {
+          cfgUseGhcErrorLogger = True,
+          cfgGhcFlags =
+            ["-dynamic-too"
+            ,"-fno-ignore-interface-pragmas"
+            ,"-fno-omit-interface-pragmas"
+            ,"-fexpose-all-unfoldings"]
+            ++ include
+        }
 
-    us0 <- mkSplitUniqSupply 'h'
+  mres <- compileWith cfg [file]
 
-    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]
+  case mres of
+    Failure errs warns ->
+      return . Left . unlines $
+        [ showOutputable p ++ ":" ++ m ++ "\n" ++ l
+        | Simple.Error p m l <- errs
+        ]
+    Success cms warns _ ->
+      do {- putStrLn $ unlines
+            [ showOutputable p ++ ":" ++ m
+            | Simple.Warning p m <- warns
             ]
+         -}
+         readModules params cms
 
-        tcs = filter (\ x -> isAlgTyCon x && not (nameInTip (tyConName x)) && not (isClassTyCon x))
-                     (delete boolTyCon (bindsTyCons' binds))
+addUnfoldings :: [(Var,CoreExpr)] -> [(Var,CoreExpr)]
+addUnfoldings binds | null unfs = binds
+                    | otherwise = addUnfoldings (binds ++ unfs)
+  where
+    unfs = usortOn fst
+      [ (x,inlineDicts e')
+      | (_,e) <- binds
+      , Var x :: CoreExpr <- universeBi e
+      , x `notElem` map fst binds
+      , Just e' <- [maybeUnfolding x]
+      ]
 
-    when (PrintCore `elem` flags) $ do
-        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"
-        putStrLn (showOutputable binds)
+readModules :: Params -> [CompiledModule ModGuts] -> IO (Either String (Theory Id))
+readModules params@Params{..} cms = do
+  let mgs    = map modCompiledModule cms
+  let binds0 = addUnfoldings (map (fmap inlineDicts) (flattenBinds (concatMap mg_binds mgs)))
 
-    let tip_data =
+  us0 <- mkSplitUniqSupply 'h'
+
+  let (binds,_us1) = initUs us0 $ sequence
+         [ fmap ((,) v) (runUQ . uqExpr <=< rmdExpr $ e)
+         | (v,e) <- binds0
+         , not (varInTip v)
+         ]
+
+  let the_props  :: [(Var,CoreExpr)]
+      the_props =
+        [ ve
+        | ve@(v,_) <- binds
+        , not (varInTip v)
+        , varToString v `elem` extra_names
+          || (varWithPropType v && maybe True (varToString v `elem`) prop_names)
+        ]
+
+  let prop_ids = map fst the_props
+
+  -- Find all bindings transitively from props
+
+  let reachable = transFrom prop_ids binds
+
+  when (PrintCore `elem` debug_flags) $ putStrLn $ showOutputable reachable
+
+  let tycons =
+         filter (\ x -> isAlgTyCon x && not (nameInTip (tyConName x)) && not (isClassTyCon x))
+                (delete boolTyCon (bindsTyCons reachable))
+
+  let (data_errs,tip_data) =
+        partitionEithers
           [ case trTyCon tc of
-              Right tc' -> tc'
-              Left err -> error $ showOutputable tc ++ ": " ++ err
-          | tc <- tcs
+              Right tc' -> Right tc'
+              Left err  -> Left $ showOutputable tc ++ ": " ++ err
+          | tc <- tycons
           ]
 
-    let tip_fns0 = concat
+  let (fn_errs,concat -> tip_fns0) =
+        partitionEithers
           [ case runTM (trDefn v e) of
-              Right fn -> fn
-              Left err -> error $ showOutputable v ++ ": " ++ err
-          | (v,e) <- binds
+              Right fn -> Right fn
+              Left err -> Left $ showOutputable v ++ ": " ++ err
+          | (v,e) <- reachable
+          , all (not . varFromRealModule v) ["mod","div"]
           ]
 
-        -- Now, split these into properties and non-properties
-    let (prop_fns,tip_fns) = partition (isPropType . func_res) tip_fns0
+  let (prop_fns,tip_fns) = partition (isPropType . func_res) tip_fns0
 
-        tip_props = either error id (mapM trProperty prop_fns)
+      (prop_errs,tip_props) = partitionEithers (map trProperty prop_fns)
 
-        thy = Theory tip_data [] [Signature Error errorType] tip_fns tip_props
+      thy = Theory tip_data [] [ Signature Tip.Id.Error errorType
+                               | any (Tip.Id.Error `F.elem`) tip_fns ||
+                                 any (Tip.Id.Error `F.elem`) tip_props
+                               ] tip_fns tip_props
 
-    when (PrintInitialTip `elem` flags) $ do
-        putStrLn "Tip.HaskellFrontend, PrintInitialTip:"
-        putStrLn (ppRender thy)
+      errs = data_errs ++ fn_errs ++ prop_errs
 
-    return thy
+  return (if null errs then Right thy else Left (unlines errs))
+
+transFrom :: [Var] -> [(Var,CoreExpr)] -> [(Var,CoreExpr)]
+transFrom (mkVarSet -> s0) binds = filter (\ (v,_) -> v `elemVarSet` fin) binds
+  where
+  fin = go s0
+
+  go :: VarSet ->  VarSet
+  go visited | isEmptyVarSet new = visited
+             | otherwise         = go (new `unionVarSet` visited)
+    where
+    new :: VarSet
+    new =
+      unionVarSets
+        [ exprSomeFreeVars (\ _ -> True) rhs_start
+        | v_start <- varSetElems visited
+        , Just rhs_start <- [lookup v_start binds]
+        ]
+      `minusVarSet` visited
 
diff --git a/src/Tip/Params.hs b/src/Tip/Params.hs
--- a/src/Tip/Params.hs
+++ b/src/Tip/Params.hs
@@ -1,31 +1,53 @@
 module Tip.Params where
 
+import Options.Applicative
+
+import Tip.Utils
+
+import Data.List.Split
+
 -- | Parameters
 data Params = Params
-  { file        :: FilePath
-  -- ^ File to process
-  , include     :: [FilePath]
+  { include     :: [FilePath]
   -- ^ Directories to include
-  , flags       :: [DebugFlags]
+  , debug_flags :: [DebugFlag]
   -- ^ Debugging flags
-  , only        :: [String]
+  , prop_names :: Maybe [String]
   -- ^ Only consider these properties
-  , extra       :: [String]
-  -- ^ Also translate these functions and its transitive dependencies
+  , extra_names :: [String]
+  -- ^ Extra names to consider
   }
   deriving Show
 
--- | Default parameters, given the name of the file to process
-defaultParams :: FilePath -> Params
-defaultParams fp = Params
-  { file = fp
-  , include = []
-  , flags = []
-  , only = []
-  , extra = []
+commaSep :: [String] -> [String]
+commaSep = concatMap (splitOn ",")
+
+parseParams :: Parser Params
+parseParams = Params
+  <$> many (strOption (long "include" <> short 'i' <> metavar "PATH" <> help "Extra include directory"))
+  <*> many (foldr (<|>) empty [ flag' debug_flag (long (flagifyShow debug_flag) <> help (debugHelp debug_flag))
+                              | debug_flag <- [minBound..maxBound]
+                              ])
+  <*> (pure Nothing <|> fmap (Just . commaSep) (many (strOption prop_opt)))
+  <*> fmap commaSep (many (strOption (long "extra" <> short 'e' <> metavar "NAME" <> help "Function declaration to add to theory")))
+
+  where
+
+  prop_opt = long "only" <> long "prop" <> short 'p' <> metavar "NAME" <> help "Property declaration to consider (default all)"
+
+-- | Default (empty) parameters
+defaultParams :: Params
+defaultParams = Params
+  { include = []
+  , debug_flags = []
+  , prop_names = Nothing
+  , extra_names = []
   }
 
 -- | Debugging flags
-data DebugFlags = PrintCore | PrintProps | PrintExtraIds | PrintInitialTip
-  deriving (Eq,Show)
+data DebugFlag = PrintCore | PrintInitialTheory
+  deriving (Eq,Show,Enum,Bounded)
 
+debugHelp :: DebugFlag -> String
+debugHelp PrintCore          = "Print core bindings from GHC"
+debugHelp PrintInitialTheory = "Print initial theory"
diff --git a/src/Tip/Prelude.hs b/src/Tip/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Prelude.hs
@@ -0,0 +1,454 @@
+{-# LANGUAGE DeriveDataTypeable,FlexibleInstances #-}
+-- | A drop-in replacement for Prelude with unfoldings exported, oriented towards Nats
+module Tip.Prelude (module Tip, module Tip.Prelude, Bool(..), Maybe(..), Either(..), Int) where
+
+import Prelude (Eq,Ord,Show,Bool(..),Int,Either(..),Maybe(..))
+import qualified Prelude as P
+import Data.Typeable
+import Tip
+
+-- * Booleans
+
+otherwise :: Bool
+otherwise = True
+
+infixr 3 &&
+
+(&&) :: Bool -> Bool -> Bool
+True && x = x
+_    && _ = False
+
+infixr 2 ||
+
+(||) :: Bool -> Bool -> Bool
+False || x = x
+_     || _ = True
+
+not :: Bool -> Bool
+not True = False
+not False = True
+
+-- * Nat functions
+
+data Nat = Z | S Nat
+  deriving (Eq,Show,Typeable,Ord)
+
+even Z = True
+even (S Z) = False
+even (S (S x)) = even x
+
+double :: Nat -> Nat
+double Z     = Z
+double (S x) = S (S (double x))
+
+half :: Nat -> Nat
+half Z = Z
+half (S Z) = Z
+half (S (S n)) = S (half n)
+
+infixl 6 +
+infixl 6 -
+
+infixl 7 *
+
+infixr 8 ^
+
+(+) :: Nat -> Nat -> Nat
+S n + m = S (n + m)
+Z   + m = m
+
+(*) :: Nat -> Nat -> Nat
+S n * m = m + (n * m)
+Z   * m = Z
+
+(^) :: Nat -> Nat -> Nat
+n ^ (S m) = n * n ^ m
+n ^ Z     = S Z
+
+-- * Truncated subtraction
+(-) :: Nat -> Nat -> Nat
+S n - S m = n - m
+m   - Z   = m
+Z   - _   = Z
+
+infix 4 <
+infix 4 <=
+infix 4 >
+infix 4 >=
+infix 4 ==
+infix 4 /=
+
+(<) :: Nat -> Nat -> Bool
+_ < Z     = False
+Z < _     = True
+S n < S m = n < m
+
+(<=) :: Nat -> Nat -> Bool
+Z   <= _   = True
+_   <= Z   = False
+S x <= S y = x <= y
+
+(>) :: Nat -> Nat -> Bool
+Z > _     = False
+_ > Z     = True
+S n > S m = n > m
+
+(>=) :: Nat -> Nat -> Bool
+_   >= Z   = True
+Z   >= _   = False
+S x >= S y = x >= y
+
+(==) :: Nat -> Nat -> Bool
+Z   == Z   = True
+Z   == _   = False
+S _ == Z   = False
+S x == S y = x == y
+
+(/=) :: Nat -> Nat -> Bool
+x /= y = not (x == y)
+
+max :: Nat -> Nat -> Nat
+max Z n = n
+max m Z = m
+max (S n) (S m) = S (max n m)
+
+min :: Nat -> Nat -> Nat
+min Z _ = Z
+min _ Z = Z
+min (S n) (S m) = S (min n m)
+
+-- * List functions on nats
+
+take :: Nat -> [a] -> [a]
+take Z _ = []
+take _ [] = []
+take (S x) (y:ys) = y : (take x ys)
+
+drop :: Nat -> [a] -> [a]
+drop Z xs = xs
+drop _ [] = []
+drop (S x) (_:xs) = drop x xs
+
+splitAt :: Nat -> [a] -> ([a], [a])
+splitAt n xs = (take n xs, drop n xs)
+
+length :: [a] -> Nat
+length [] = Z
+length (_:xs) = S (length xs)
+
+delete :: Nat -> [Nat] -> [Nat]
+delete _ [] = []
+delete n (x:xs) =
+  case n == x of
+    True -> xs
+    False -> x : (delete n xs)
+
+deleteAll :: Nat -> [Nat] -> [Nat]
+deleteAll _ [] = []
+deleteAll n (x:xs) =
+  case n == x of
+    True -> deleteAll n xs
+    False -> x : (deleteAll n xs)
+
+count :: Nat -> [Nat] -> Nat
+count x [] = Z
+count x (y:ys) =
+  case x == y of
+    True -> S (count x ys)
+    _ -> count x ys
+
+nub :: [Nat] -> [Nat]
+nub (x:xs) = x:deleteAll x (nub xs)
+nub []     = []
+
+index :: [a] -> Nat -> Maybe a
+index (x:xs) Z     = Just x
+index (x:xs) (S n) = index xs n
+index []     _     = Nothing
+
+elem :: Nat -> [Nat] -> Bool
+x `elem` [] = False
+x `elem` (y:ys) = x == y || x `elem` ys
+
+isPermutation :: [Nat] -> [Nat] -> Bool
+[]     `isPermutation` ys = null ys
+(x:xs) `isPermutation` ys = x `elem` ys && xs `isPermutation` delete x ys
+
+sorted,ordered,uniqsorted :: [Nat] -> Bool
+sorted = ordered
+ordered []       = True
+ordered [x]      = True
+ordered (x:y:xs) = x <= y && ordered (y:xs)
+uniqsorted []       = True
+uniqsorted [x]      = True
+uniqsorted (x:y:xs) = x < y && uniqsorted (y:xs)
+
+unique :: [Nat] -> Bool
+unique []     = True
+unique (x:xs) = if x `elem` xs then False else unique xs
+
+insert :: Nat -> [Nat] -> [Nat]
+insert n [] = [n]
+insert n (x:xs) =
+  case n <= x of
+    True -> n : x : xs
+    _    -> x : (insert n xs)
+
+isort :: [Nat] -> [Nat]
+isort [] = []
+isort (x:xs) = insert x (isort xs)
+
+eqList :: [Nat] -> [Nat] -> Bool
+eqList (x:xs) (y:ys) = (x == y) && (xs `eqList` ys)
+eqList []     []     = True
+eqList _      _      = False
+
+sum :: [Nat] -> Nat
+sum [] = Z
+sum (x:xs) = x + sum xs
+
+product :: [Nat] -> Nat
+product [] = S Z
+product (x:xs) = x * product xs
+
+lookup :: Nat -> [(Nat,b)] -> Maybe b
+lookup x ((y,b):ys) | x == y    = Just b
+                    | otherwise = lookup x ys
+lookup x [] = Nothing
+
+-- * Int functions
+
+zeq,zne,zle,zlt,zgt,zge :: Int -> Int -> Bool
+zeq = (P.==)
+zne = (P./=)
+zle = (P.<=)
+zlt = (P.<)
+zgt = (P.>)
+zge = (P.>=)
+
+zplus,zmult,zminus,zmax,zmin :: Int -> Int -> Int
+zplus = (P.+)
+zmult = (P.*)
+zminus = (P.-)
+zmax = P.max
+zmin = P.min
+
+-- * List functions on Ints
+
+{-# NOINLINE ztake #-}
+ztake :: Int -> [a] -> [a]
+ztake 0 _      = []
+ztake _ []     = []
+ztake n (x:xs) = x:ztake (n `zminus` 1) xs
+
+{-# NOINLINE zdrop #-}
+zdrop :: Int -> [a] -> [a]
+zdrop 0 xs     = xs
+zdrop _ []     = []
+zdrop n (x:xs) = zdrop (n `zminus` 1) xs
+
+zsplitAt :: Int -> [a] -> ([a], [a])
+zsplitAt n xs = (ztake n xs, zdrop n xs)
+
+{-# NOINLINE zlength #-}
+zlength :: [a] -> Int
+zlength []     = 0
+zlength (x:xs) = 1 `zplus` zlength xs
+
+zdelete :: Int -> [Int] -> [Int]
+zdelete x [] = []
+zdelete x (y:ys)
+  | x `zeq` y = ys
+  | otherwise = y:zdelete x ys
+
+zdeleteAll :: Int -> [Int] -> [Int]
+zdeleteAll _ [] = []
+zdeleteAll n (x:xs) =
+  case n `zeq` x of
+    True -> zdeleteAll n xs
+    False -> x : (zdeleteAll n xs)
+
+
+zcount :: Int -> [Int] -> Nat
+zcount x []                 = Z
+zcount x (y:xs) | x `zeq` y  = S (zcount x xs)
+                | otherwise = zcount x xs
+
+zzcount :: Int -> [Int] -> Int
+zzcount x []                 = 0
+zzcount x (y:xs) | x `zeq` y = 1 `zplus` zzcount x xs
+                 | otherwise = zzcount x xs
+
+znub :: [Int] -> [Int]
+znub (x:xs) = x:zdeleteAll x (znub xs)
+znub []     = []
+
+zindex :: [a] -> Int -> Maybe a
+zindex (x:xs) 0 = Just x
+zindex (x:xs) n = zindex xs (n `zminus` 1)
+zindex []     _ = Nothing
+
+zelem :: Int -> [Int] -> Bool
+x `zelem` [] = False
+x `zelem` (y:ys) = x `zeq` y || x `zelem` ys
+
+zisPermutation :: [Int] -> [Int] -> Bool
+[]     `zisPermutation` ys = null ys
+(x:xs) `zisPermutation` ys = x `zelem` ys && xs `zisPermutation` zdelete x ys
+
+zsorted,zordered,zuniqsorted :: [Int] -> Bool
+zordered []       = True
+zordered [x]      = True
+zordered (x:y:xs) = x `zle` y && zordered (y:xs)
+
+zsorted = zordered
+
+zuniqsorted []       = True
+zuniqsorted [x]      = True
+zuniqsorted (x:y:xs) = x `zlt` y && zuniqsorted (y:xs)
+
+zunique :: [Int] -> Bool
+zunique []     = True
+zunique (x:xs) = if x `zelem` xs then False else zunique xs
+
+zinsert :: Int -> [Int] -> [Int]
+zinsert n [] = [n]
+zinsert n (x:xs) =
+  case n `zle` x of
+    True -> n : x : xs
+    _    -> x : (zinsert n xs)
+
+zisort :: [Int] -> [Int]
+zisort [] = []
+zisort (x:xs) = zinsert x (zisort xs)
+
+zeqList :: [Int] -> [Int] -> Bool
+zeqList (x:xs) (y:ys) = (x `zeq` y) && (xs `zeqList` ys)
+zeqList []     []     = True
+zeqList _      _      = False
+
+zsum :: [Int] -> Int
+zsum [] = 0
+zsum (x:xs) = x `zplus` zsum xs
+
+zproduct :: [Int] -> Int
+zproduct [] = 1
+zproduct (x:xs) = x `zmult` zproduct xs
+
+zlookup :: Int -> [(Int,b)] -> Maybe b
+zlookup x ((y,b):ys) | x `zeq` y    = Just b
+                     | otherwise = zlookup x ys
+zlookup x [] = Nothing
+
+-- * Polymorphic lists functions
+
+{-# NOINLINE null #-}
+null :: [a] -> Bool
+null [] = True
+null _  = False
+
+(++) :: [a] -> [a] -> [a]
+[]     ++ ys = ys
+(x:xs) ++ ys = x : (xs ++ ys)
+
+reverse :: [a] -> [a]
+reverse []     = []
+reverse (x:xs) = reverse xs ++ [x]
+
+zip :: [a] -> [b] -> [(a, b)]
+zip [] _ = []
+zip _ [] = []
+zip (x:xs) (y:ys) = (x, y) : (zip xs ys)
+
+filter :: (a -> Bool) -> [a] -> [a]
+filter p [] = []
+filter p (x:xs) | p x = x:filter p xs
+filter p (x:xs) = filter p xs
+
+
+map :: (a -> b) -> [a] -> [b]
+map f []     = []
+map f (x:xs) = f x:map f xs
+
+concat :: [[a]] -> [a]
+concat (xs:xss) = xs ++ concat xss
+concat []       = []
+
+concatMap :: (a -> [b]) -> [a] -> [b]
+concatMap f (x:xs) = f x ++ concatMap f xs
+concatMap _ []     = []
+
+foldl :: (b -> a -> b) -> b -> [a] -> b
+foldl f z []     = z
+foldl f z (x:xs) = foldl f (f z x) xs
+
+foldr :: (a -> b -> b) -> b -> [a] -> b
+foldr f z []     = z
+foldr f z (x:xs) = f x (foldr f z xs)
+
+-- * Lists and booleans
+
+and :: [Bool] -> Bool
+and (x:xs) = x && and xs
+and []     = True
+
+or :: [Bool] -> Bool
+or (x:xs) = x || or xs
+or []     = False
+
+all :: (a -> Bool) -> [a] -> Bool
+all p []     = True
+all p (x:xs) = p x && all p xs
+
+any :: (a -> Bool) -> [a] -> Bool
+any p []     = False
+any p (x:xs) = p x || any p xs
+
+takeWhile :: (a -> Bool) -> [a] -> [a]
+takeWhile _ [] = []
+takeWhile p (x:xs) =
+  case p x of
+    True -> x : (takeWhile p xs)
+    _ -> []
+
+dropWhile :: (a -> Bool) -> [a] -> [a]
+dropWhile _ [] = []
+dropWhile p (x:xs) =
+  case p x of
+    True -> dropWhile p xs
+    _ -> x:xs
+
+-- | Miscellaneous
+
+id :: a -> a
+id x = x
+
+const :: a -> b -> a
+const x _ = x
+
+infixr 9 .
+
+(.) :: (b -> c) -> (a -> b) -> a -> c
+f . g = \ x -> f (g x)
+
+flip :: (a -> b -> c) -> (b -> a -> c)
+flip f x y = f y x
+
+infixr 0 $
+($) :: (a -> b) -> a -> b
+f $ x = f x
+
+maybe :: b -> (a -> b) -> Maybe a -> b
+maybe n _ Nothing  = n
+maybe _ j (Just x) = j x
+
+either :: (a -> c) -> (b -> c) -> Either a b -> c
+either f _ (Left x)  = f x
+either _ g (Right y) = g y
+
+fst :: (a,b) -> a
+fst (x,_) = x
+
+snd :: (a,b) -> b
+snd (_,y) = y
+
diff --git a/src/Tip/Property.hs b/src/Tip/Property.hs
--- a/src/Tip/Property.hs
+++ b/src/Tip/Property.hs
@@ -28,7 +28,7 @@
 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))
+    return (Formula Prove UserAsserted tvs (mkQuant Forall args pr))
   where
     unLam (Lam xs e) = let (ys,e') = unLam e in (xs ++ ys,e')
     unLam e          = ([],e)
@@ -48,7 +48,7 @@
 
       | isId "bool" x = return e
 
-      | isId "Neg" x || isId "neg" x = neg <$> go e
+      | isId "Neg" x || isId "neg" x || isId "question" x = neg <$> go e
 
   goo i e0@(projAt -> Just (projAt -> Just (projGlobal -> Just x,e1),e2))
 
diff --git a/src/Tip/Unfoldings.hs b/src/Tip/Unfoldings.hs
deleted file mode 100644
--- a/src/Tip/Unfoldings.hs
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# 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/tip-haskell-frontend.cabal b/tip-haskell-frontend.cabal
--- a/tip-haskell-frontend.cabal
+++ b/tip-haskell-frontend.cabal
@@ -1,5 +1,5 @@
 name:                tip-haskell-frontend
-version:             0.1.1
+version:             0.2
 license:             BSD3
 license-file:        LICENSE
 author:              Dan Rosén
@@ -22,13 +22,12 @@
 library
   exposed-modules:
     Tip.HaskellFrontend
+    Tip.Prelude
     Tip
   other-modules:
     Tip.Params
     Tip.Id
     Tip.GHCUtils
-    Tip.Calls
-    Tip.Compile
     Tip.CoreToTip
     Tip.DataConPattern
     Tip.Dicts
@@ -36,10 +35,10 @@
     Tip.ParseDSL
     Tip.Property
     Tip.RemoveDefault
-    Tip.GHCScope
     Tip.TyAppBeta
-    Tip.Unfoldings
     Tip.Uniquify
+    Tip.GenericInstances
+  ghc-options:         -fexpose-all-unfoldings
   hs-source-dirs:      src
   include-dirs:        src
   default-language:    Haskell2010
@@ -54,7 +53,9 @@
                        bytestring >=0.9.2,
                        split >=0.2,
                        geniplate-mirror >=0.7.1,
-                       tip-lib >= 0.1.1 && < 0.2,
+                       tip-lib >= 0.2 && < 0.3,
+                       ghc-simple >= 0.1.2.0 && < 0.2,
+                       optparse-applicative,
                        QuickCheck >= 2.8
 
 executable tip-ghc
@@ -64,4 +65,5 @@
                        tip-haskell-frontend,
                        tip-lib,
                        pretty-show,
+                       optparse-applicative,
                        pretty