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,78 @@
+module Main where
+
+import System.Environment
+
+import Tip.Parser
+import Tip.Pretty.SMT as SMT
+import Tip.Pretty.Why3 as Why3
+import Tip.Pretty.Isabelle as Isabelle
+import Tip.Pretty.Haskell as HS
+import Tip.Pretty
+import Tip.CallGraph
+
+import Tip.Passes
+import Tip.Lint
+import Tip.Fresh
+import Tip.Core
+import Options.Applicative
+
+import Control.Monad
+
+data OutputMode = Haskell | Why3 | CVC4 | Isabelle | TIP
+
+parseOutputMode :: Parser OutputMode
+parseOutputMode =
+      flag' Haskell (long "haskell" <> help "Haskell output")
+  <|> flag' Why3 (long "why" <> help "WhyML output")
+  <|> flag' CVC4 (long "smtlib" <> help "SMTLIB output (CVC4-compatible)")
+  <|> flag' Isabelle (long "isabelle" <> help "Isabelle output")
+  <|> flag  TIP TIP (long "tip" <> help "TIP output (default)")
+
+optionParser :: Parser ([StandardPass], Maybe String, OutputMode)
+optionParser =
+  (,,) <$> parsePasses <*> parseFile <*> parseOutputMode
+  where
+    parseFile =
+      fmap Just (strArgument (metavar "FILENAME")) <|> pure Nothing
+
+main :: IO ()
+main = do
+  (passes, files, mode) <-
+    execParser $
+      info (helper <*> optionParser)
+        (fullDesc <>
+         progDesc "Transform a TIP problem" <>
+         header "tip - a tool for processing TIP problems")
+  case files of
+    Nothing ->
+      handle passes mode =<< getContents
+    Just f ->
+      handle passes mode =<< readFile f
+
+handle :: [StandardPass] -> OutputMode -> String -> IO ()
+handle passes mode s =
+  case parse s of
+    Left err  -> error $ "Parse failed: " ++ err
+    Right thy -> do
+      let fmap_pp f = fmap (show . f)
+      let show_passes c = fmap (\ s -> c ++ show passes ++ "\n" ++ s)
+      let pipeline =
+            case mode of
+              CVC4 ->
+                fmap_pp SMT.ppTheory . runPasses
+                  (passes ++
+                  [ LambdaLift, AxiomatizeLambdas
+                  , CollapseEqual, RemoveAliases
+                  , SimplifyGently, RemoveMatch
+                  , SimplifyGently, NegateConjecture
+                  , SimplifyGently
+                  ])
+              Haskell ->
+                fmap_pp HS.ppTheory . runPasses passes
+              Why3 ->
+                fmap_pp Why3.ppTheory . runPasses (passes ++ [CSEMatchWhy3])
+              Isabelle ->
+                fmap_pp Isabelle.ppTheory . runPasses passes
+              TIP ->
+                show_passes "; " . fmap_pp SMT.ppTheory . runPasses passes
+      putStrLn (freshPass pipeline (lint "parse" thy))
diff --git a/src/Tip/CallGraph.hs b/src/Tip/CallGraph.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/CallGraph.hs
@@ -0,0 +1,61 @@
+-- | Calculate the call graph of a theory.
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE RecordWildCards, CPP, DeriveFunctor #-}
+module Tip.CallGraph where
+
+#include "errors.h"
+import Tip.Scope
+import Tip.Utils
+import Tip.Core
+import Tip.Pretty
+import qualified Data.Map as Map
+import Data.List
+
+type FS = Function :+: Signature
+
+data Block a =
+  Block {
+    callers :: [FS a],
+    callees :: [FS a] }
+  deriving (Show, Functor)
+
+flattenBlock :: Block a -> [FS a]
+flattenBlock block = callers block ++ callees block
+
+theoryStuff :: Theory a -> [FS a]
+theoryStuff Theory{..} = map InL thy_funcs ++ map InR thy_sigs
+
+callGraph :: (PrettyVar a, Ord a) => Theory a -> [Block a]
+callGraph thy@Theory{..} =
+  [ Map.findWithDefault __ xs m | xs <- top ]
+  where
+    stuff = theoryStuff thy
+    top   = topsort stuff
+    tops  = Map.fromList [(x, xs) | xs <- top, x <- xs]
+    m     = foldl op Map.empty top
+    funcs = Map.fromList [(defines func, func) | func <- stuff]
+    op m xs =
+      Map.insert xs (Block xs (usort ys \\ xs)) m
+      where
+        ys =
+          concat
+            [ flattenBlock (Map.findWithDefault (Block [] []) ys m)
+            | x <- xs,
+              y <- uses x,
+              Just func <- [Map.lookup y funcs],
+              Just ys   <- [Map.lookup func tops]]
+
+data CallGraphOpts =
+  CallGraphOpts {
+    exploreSingleFunctions :: Bool,
+    exploreCalleesFirst    :: Bool }
+
+flatCallGraph :: (PrettyVar a, Ord a) => CallGraphOpts -> Theory a -> [[FS a]]
+flatCallGraph CallGraphOpts{..} thy =
+  nub . filter (not . null) $
+  concat [ map callers blocks | exploreSingleFunctions ] ++ concatMap flatten blocks ++
+  [concat (topsort (theoryStuff thy))]
+  where
+    blocks = callGraph thy
+    flatten block@Block{..} =
+      [ callees | exploreCalleesFirst ] ++ [flattenBlock block]
diff --git a/src/Tip/Core.hs b/src/Tip/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Core.hs
@@ -0,0 +1,441 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, PatternGuards #-}
+{-# LANGUAGE ExplicitForAll, FlexibleContexts, FlexibleInstances, TemplateHaskell, MultiParamTypeClasses #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | General functions for constructing and examining Tip syntax.
+module Tip.Core(module Tip.Types, module Tip.Core) where
+
+#include "errors.h"
+import Tip.Types
+import Tip.Fresh
+import Tip.Utils
+import Tip.Pretty
+import Data.Traversable (Traversable)
+import Data.Foldable (Foldable)
+import qualified Data.Foldable as F
+import Data.Generics.Geniplate
+import Data.List ((\\))
+import Data.Ord
+import Control.Monad
+import qualified Data.Map as Map
+import Control.Applicative ((<|>))
+
+infix  4 ===
+-- infixr 3 /\
+infixr 2 \/
+infixr 1 ==>
+infixr 0 ===>
+
+-- * Constructing expressions
+
+(===) :: Expr a -> Expr a -> Expr a
+e1 === e2 = Builtin Equal :@: [e1,e2]
+
+(=/=) :: Expr a -> Expr a -> Expr a
+e1 =/= e2 = Builtin Distinct :@: [e1,e2]
+
+neg :: Expr a -> Expr a
+neg (Builtin op :@: [e1,e2])
+  | Equal    <- op = e1 =/= e2
+  | Distinct <- op = e1 === e2
+neg e
+  | Just b <- boolView e = if b then falseExpr else trueExpr
+  | otherwise = Builtin Not :@: [e]
+
+(/\) :: Expr a -> Expr a -> Expr a
+e1 /\ e2
+  | Just b <- boolView e1 = if b then e2 else falseExpr
+  | Just b <- boolView e2 = if b then e1 else falseExpr
+  | otherwise = Builtin And :@: [e1,e2]
+
+(\/) :: Expr a -> Expr a -> Expr a
+e1 \/ e2
+  | Just b <- boolView e1 = if b then trueExpr else e2
+  | Just b <- boolView e2 = if b then trueExpr else e1
+  | otherwise = Builtin Or :@: [e1,e2]
+
+ands :: [Expr a] -> Expr a
+ands xs = foldl (/\) trueExpr xs
+
+ors :: [Expr a] -> Expr a
+ors xs = foldl (\/) falseExpr xs
+
+(==>) :: Expr a -> Expr a -> Expr a
+e1 ==> e2
+  | Just a <- boolView e1 = if a then e2 else trueExpr
+  | Just b <- boolView e2 = if b then trueExpr else neg e1
+  | otherwise = Builtin Implies :@: [e1,e2]
+
+(===>) :: [Expr a] -> Expr a -> Expr a
+xs ===> y = foldr (==>) y xs
+
+mkQuant :: Quant -> [Local a] -> Expr a -> Expr a
+mkQuant q [] e = e
+mkQuant q xs e = Quant NoInfo q xs e
+
+bool :: Bool -> Expr a
+bool = literal . Bool
+
+trueExpr :: Expr a
+trueExpr  = bool True
+
+falseExpr :: Expr a
+falseExpr = bool False
+
+makeIf :: Expr a -> Expr a -> Expr a -> Expr a
+makeIf c t f
+  | Just b <- boolView c = if b then t else f
+  | otherwise = Match c [Case (LitPat (Bool True)) t,Case (LitPat (Bool False)) f]
+
+intLit :: Integer -> Expr a
+intLit = literal . Int
+
+literal :: Lit -> Expr a
+literal lit = Builtin (Lit lit) :@: []
+
+intType :: Type a
+intType = BuiltinType Integer
+
+boolType :: Type a
+boolType = BuiltinType Boolean
+
+applyFunction :: Function a -> [Type a] -> [Expr a] -> Expr a
+applyFunction fn@Function{..} tyargs args
+  = Gbl (Global func_name (funcType fn) tyargs) :@: args
+
+applySignature :: Signature a -> [Type a] -> [Expr a] -> Expr a
+applySignature Signature{..} tyargs args
+  = Gbl (Global sig_name sig_type tyargs) :@: args
+
+apply :: Expr a -> [Expr a] -> Expr a
+apply e es@(_:_) = Builtin At :@: (e:es)
+apply _ [] = ERROR("tried to construct nullary lambda function")
+
+applyType :: Ord a => [a] -> [Type a] -> Type a -> Type a
+applyType tvs tys ty
+  | length tvs == length tys =
+      flip transformType ty $ \ty' ->
+        case ty' of
+          TyVar x ->
+            Map.findWithDefault ty' x m
+          _ -> ty'
+  | otherwise = ERROR("wrong number of type arguments")
+  where
+    m = Map.fromList (zip tvs tys)
+
+applyPolyType :: Ord a => PolyType a -> [Type a] -> ([Type a], Type a)
+applyPolyType PolyType{..} tys =
+  (map (applyType polytype_tvs tys) polytype_args,
+   applyType polytype_tvs tys polytype_res)
+
+-- * Predicates and examinations on expressions
+
+litView :: Expr a -> Maybe Lit
+litView (Builtin (Lit l) :@: []) = Just l
+litView _ = Nothing
+
+boolView :: Expr a -> Maybe Bool
+boolView e = case litView e of Just (Bool b) -> Just b
+                               _             -> Nothing
+
+-- | A representation of Nested patterns, used in 'patternMatchingView'
+data DeepPattern a
+  = DeepConPat (Global a) [DeepPattern a]
+  | DeepVarPat (Local a)
+  | DeepLitPat Lit
+
+-- | Match as left-hand side pattern-matching definitions
+--
+-- Stops at default patterns, for simplicity
+patternMatchingView :: Ord a => [Local a] -> Expr a -> [([DeepPattern a],Expr a)]
+patternMatchingView = go . map DeepVarPat
+  where
+  go ps (Match (Lcl l) brs)
+    | null [ () | Case Default _ <- brs ]
+    , Just k <- modDeepPatterns l ps
+    = concat [ go (k (deep p)) ((patToExpr p `unsafeSubst` l) rhs) | Case p rhs <- brs ]
+  go ps e = [(ps,e)]
+
+  (<$$>) :: (Functor f,Functor g) => (a -> b) -> f (g a) -> f (g b)
+  (<$$>) = fmap . fmap
+
+  -- Variable not in pattern: returns Nothing
+  modDeepPattern :: Eq a => Local a -> DeepPattern a -> Maybe (DeepPattern a -> DeepPattern a)
+  modDeepPattern l (DeepConPat g nps) = DeepConPat g <$$> modDeepPatterns l nps
+  modDeepPattern l (DeepVarPat l') | l == l'   = Just id
+                                   | otherwise = Nothing
+  modDeepPattern l (DeepLitPat lit) = Nothing
+
+  -- Variable not in patterns: returns Nothing
+  modDeepPatterns :: Eq a => Local a -> [DeepPattern a] -> Maybe (DeepPattern a -> [DeepPattern a])
+  modDeepPatterns l (np:nps) = ((:nps) <$$> modDeepPattern l np) <|> ((np:) <$$> modDeepPatterns l nps)
+  modDeepPatterns l []       = Nothing
+
+  deep :: Pattern a -> DeepPattern a
+  deep (ConPat g ls) = DeepConPat g (map DeepVarPat ls)
+  deep (LitPat lit)  = DeepLitPat lit
+  deep Default       = error "patternMatchingView.deep: Default"
+
+  patToExpr :: Pattern a -> Expr a
+  patToExpr (ConPat g ls) = Gbl g :@: map Lcl ls
+  patToExpr (LitPat lit)  = literal lit
+  patToExpr Default       = error "patternMatchingView.patToExpr: Default"
+
+ifView :: Expr a -> Maybe (Expr a,Expr a,Expr a)
+ifView (Match c [Case _ e1,Case (LitPat (Bool b)) e2])
+  | b         = Just (c,e2,e1)
+  | otherwise = Just (c,e1,e2)
+ifView (Match c [Case Default e1,Case (LitPat i@Int{}) e2])    = Just (c === literal i,e2,e1)
+ifView (Match c (Case Default e1:Case (LitPat i@Int{}) e2:es)) = Just (c === literal i,e2,Match c (Case Default e1:es))
+ifView _ = Nothing
+
+projAt :: Expr a -> Maybe (Expr a,Expr a)
+projAt (Builtin At :@: [a,b]) = Just (a,b)
+projAt _                          = Nothing
+
+projGlobal :: Expr a -> Maybe a
+projGlobal (Gbl (Global x _ _) :@: []) = Just x
+projGlobal _                           = Nothing
+
+atomic :: Expr a -> Bool
+atomic (_ :@: []) = True
+atomic Lcl{}      = True
+atomic _          = False
+
+occurrences :: Eq a => Local a -> Expr a -> Int
+occurrences var body = length (filter (== var) (universeBi body))
+
+-- | The signature of a function
+signature :: Function a -> Signature a
+signature func@Function{..} = Signature func_name (funcType func)
+
+-- | The type of a function
+funcType :: Function a -> PolyType a
+funcType (Function _ tvs lcls res _) = PolyType tvs (map lcl_type lcls) res
+
+bound, free, locals :: Ord a => Expr a -> [Local a]
+bound e =
+  usort $
+    concat [ lcls | Lam lcls _       <- universeBi e ] ++
+           [ lcl  | Let lcl _ _      <- universeBi e ] ++
+    concat [ lcls | Quant _ _ lcls _ <- universeBi e ] ++
+    concat [ lcls | ConPat _ lcls    <- universeBi e ]
+locals = usort . universeBi
+free e = locals e \\ bound e
+
+globals :: (UniverseBi (t a) (Global a),UniverseBi (t a) (Type a),Ord a)
+        => t a -> [a]
+globals e =
+  usort $
+    [ gbl_name | Global{..} <- universeBi e ] ++
+    [ tc | TyCon tc _ <- universeBi e ]
+
+tyVars :: Ord a => Type a -> [a]
+tyVars t = usort $ [ a | TyVar a <- universeBi t ]
+
+-- The free type variables are in the locals, and the globals:
+-- but only in the types applied to the global variable.
+freeTyVars :: Ord a => Expr a -> [a]
+freeTyVars e =
+  usort $
+    concatMap tyVars $
+             [ lcl_type | Local{..} <- universeBi e ] ++
+      concat [ gbl_args | Global{..} <- universeBi e ]
+
+-- | The type of an expression
+exprType :: Ord a => Expr a -> Type a
+exprType (Gbl (Global{..}) :@: _) = res
+  where
+    (_, res) = applyPolyType gbl_type gbl_args
+exprType (Builtin blt :@: es) = builtinType blt (map exprType es)
+exprType (Lcl lcl) = lcl_type lcl
+exprType (Lam args body) = map lcl_type args :=>: exprType body
+exprType (Match _ (Case _ body:_)) = exprType body
+exprType (Match _ []) = ERROR("empty case expression")
+exprType (Let _ _ body) = exprType body
+exprType Quant{} = boolType
+
+-- | The result type of a built in function, applied to some types
+builtinType :: Ord a => Builtin -> [Type a] -> Type a
+builtinType (Lit Int{}) _ = intType
+builtinType (Lit Bool{}) _ = boolType
+builtinType (Lit String{}) _ = ERROR("strings are not really here")
+builtinType And _ = boolType
+builtinType Or _ = boolType
+builtinType Not _ = boolType
+builtinType Implies _ = boolType
+builtinType Equal _ = boolType
+builtinType Distinct _ = boolType
+builtinType IntAdd _ = intType
+builtinType IntSub _ = intType
+builtinType IntMul _ = intType
+builtinType IntDiv _ = intType
+builtinType IntMod _ = intType
+builtinType IntGt _ = boolType
+builtinType IntGe _ = boolType
+builtinType IntLt _ = boolType
+builtinType IntLe _ = boolType
+builtinType At ((_  :=>: res):_) = res
+builtinType At _ = ERROR("ill-typed lambda application")
+
+
+-- * Substition and refreshing
+
+freshLocal :: Name a => Type a -> Fresh (Local a)
+freshLocal ty = liftM2 Local fresh (return ty)
+
+freshArgs :: Name a => Global a -> Fresh [Local a]
+freshArgs gbl = mapM freshLocal (polytype_args (gbl_type gbl))
+
+refreshLocal :: Name a => Local a -> Fresh (Local a)
+refreshLocal (Local name ty) = liftM2 Local (refresh name) (return ty)
+
+-- Rename bound variables in an expression to fresh variables.
+freshen :: Name a => Expr a -> Fresh (Expr a)
+freshen e = freshenNames (map lcl_name (bound e)) e
+
+freshenNames :: (TransformBi a (f a), Name a) =>
+  [a] -> f a -> Fresh (f a)
+freshenNames names e = do
+  sub <- fmap (Map.fromList . zip names) (mapM refresh names)
+  return . flip transformBi e $ \x ->
+    case Map.lookup x sub of
+      Nothing -> x
+      Just y -> y
+
+-- | Substitution, of local variables
+--
+-- Since there are only rank-1 types, bound variables from lambdas and
+-- case never have a forall type and thus are not applied to any types.
+(//) :: Name a => Expr a -> Local a -> Expr a -> Fresh (Expr a)
+e // x = transformExprM $ \ e0 -> case e0 of
+  Lcl y | x == y -> freshen e
+  _              -> return e0
+
+substMany :: Name a => [(Local a, Expr a)] -> Expr a -> Fresh (Expr a)
+substMany xs e0 = foldM (\e (x,xe) -> (xe // x) e) e0 xs
+
+letExpr :: Name a => Expr a -> (Local a -> Fresh (Expr a)) -> Fresh (Expr a)
+letExpr (Lcl x) k = k x
+letExpr b k =
+  do v <- freshLocal (exprType b)
+     rest <- k v
+     return (Let v b rest)
+
+-- | Substitution, but without refreshing. Only use when the replacement
+-- expression contains no binders (i.e. no lambdas, no lets, no quantifiers),
+-- since the binders are not refreshed at every insertion point.
+unsafeSubst :: Ord a => Expr a -> Local a -> Expr a -> Expr a
+e `unsafeSubst` _ | not (null (bound e)) = error "Tip.unsafeSubst: contains binders"
+e `unsafeSubst` x = transformExpr $ \ e0 -> case e0 of
+  Lcl y | x == y -> e
+  _              -> e0
+
+-- * Making new locals and functions
+
+updateLocalType :: Type a -> Local a -> Local a
+updateLocalType ty (Local name _) = Local name ty
+
+updateFuncType :: PolyType a -> Function a -> Function a
+updateFuncType (PolyType tvs lclTys res) (Function name _ lcls _ body)
+  | length lcls == length lclTys =
+      Function name tvs (zipWith updateLocalType lclTys lcls) res body
+  | otherwise = ERROR("non-matching type")
+
+
+-- * Matching
+
+matchTypesIn :: Ord a => [a] -> [(Type a, Type a)] -> Maybe [Type a]
+matchTypesIn tvs tys = do
+  sub <- matchTypes tys
+  forM tvs $ \tv -> lookup tv sub
+
+matchTypes :: Ord a => [(Type a, Type a)] -> Maybe [(a, Type a)]
+matchTypes tys = mapM (uncurry match) tys >>= collect . usort . concat
+  where
+    match (TyVar x) ty = Just [(x, ty)]
+    match (TyCon x tys1) (TyCon y tys2)
+      | x == y && length tys1 == length tys2 =
+        fmap concat (zipWithM match tys1 tys2)
+    match (args1 :=>: res1) (args2 :=>: res2)
+      | length args1 == length args2 =
+        fmap concat (zipWithM match (res1:args1) (res2:args2))
+    match ty1 ty2 | ty1 == ty2 = Just []
+    match _ _ = Nothing
+
+    collect [] = Just []
+    collect [x] = Just [x]
+    collect ((x, _):(y, _):_) | x == y = Nothing
+    collect (x:xs) = fmap (x:) (collect xs)
+
+makeGlobal :: Ord a => a -> PolyType a -> [Type a] -> Maybe (Type a) -> Maybe (Global a)
+makeGlobal name polyty@PolyType{..} args mres = do
+  vars <- matchTypesIn polytype_tvs tys
+  return (Global name polyty vars)
+  where
+    tys =
+      (case mres of Nothing -> []; Just res -> [(polytype_res, res)]) ++
+      zip polytype_args args
+
+-- * Data types
+
+constructorType :: Datatype a -> Constructor a -> PolyType a
+constructorType Datatype{..} Constructor{..} =
+  PolyType data_tvs (map snd con_args) (TyCon data_name (map TyVar data_tvs))
+
+destructorType :: Datatype a -> Type a -> PolyType a
+destructorType Datatype{..} ty =
+  PolyType data_tvs [TyCon data_name (map TyVar data_tvs)] ty
+
+constructor :: Datatype a -> Constructor a -> [Type a] -> Global a
+constructor dt con@Constructor{..} tys =
+  Global con_name (constructorType dt con) tys
+
+projector :: Datatype a -> Constructor a -> Int -> [Type a] -> Global a
+projector dt Constructor{..} i tys =
+  Global proj_name (destructorType dt proj_ty) tys
+  where
+    (proj_name, proj_ty) = con_args !! i
+
+discriminator :: Datatype a -> Constructor a -> [Type a] -> Global a
+discriminator dt Constructor{..} tys =
+  Global con_discrim (destructorType dt (BuiltinType Boolean)) tys
+
+-- * Operations on theories
+
+mapDecls :: forall a b . (forall t . Traversable t => t a -> t b) -> Theory a -> Theory b
+mapDecls k (Theory a b c d e) = Theory (map k a) (map k b) (map k c) (map k d) (map k e)
+
+-- * Topologically sorting definitions
+
+topsort :: (Ord a,Definition f) => [f a] -> [[f a]]
+topsort = sortThings defines uses
+
+class Definition f where
+  defines :: f a -> a
+  uses    :: f a -> [a]
+
+data (f :+: g) a = InL (f a) | InR (g a)
+  deriving (Eq,Ord,Show,Functor)
+
+instance (Definition f,Definition g) => Definition (f :+: g) where
+  defines (InL x) = defines x
+  defines (InR y) = defines y
+  uses (InL x) = uses x
+  uses (InR y) = uses y
+
+instance Definition Signature where
+  defines = sig_name
+  uses _  = []
+
+instance Definition Function where
+  defines = func_name
+  uses    = F.toList . func_body
+
+instance Definition Datatype where
+  defines = data_name
+  uses    = concatMap F.toList . data_cons
+
diff --git a/src/Tip/Fresh.hs b/src/Tip/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Fresh.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Fresh monad and the Name type class
+module Tip.Fresh where
+
+import Tip.Utils
+import Tip.Pretty
+import Control.Applicative hiding (empty)
+import Control.Monad.State
+import Control.Arrow ((&&&))
+
+import Data.Foldable (Foldable)
+
+-- | The Fresh monad
+newtype Fresh a = Fresh (State Int a)
+  deriving (Monad, Applicative, Functor, MonadFix)
+
+-- | Continues making unique names after the highest
+--   numbered name in a foldable value.
+freshPass :: (Foldable f,Name a) => (f a -> Fresh b) -> f a -> b
+f `freshPass` x = f x `freshFrom` x
+
+-- | Run fresh from starting from the greatest unique in a structure
+freshFrom :: (Foldable f,Name b) => Fresh a -> f b -> a
+freshFrom m x = runFreshFrom (succ (maximumOn getUnique x)) m
+
+-- | Run fresh, starting from zero
+runFresh :: Fresh a -> a
+runFresh (Fresh m) = evalState m 0
+
+-- | Run fresh from some starting value
+runFreshFrom :: Int -> Fresh a -> a
+runFreshFrom n (Fresh m) = evalState m (n+1)
+
+-- | The Name type class
+class (PrettyVar a, Ord a) => Name a where
+  -- | Make a fresh name
+  fresh   :: Fresh a
+
+  -- | Refresh a name, which could have some resemblance to the original
+  -- name
+  refresh :: a -> Fresh a
+  refresh _ = fresh
+
+  -- | Make a fresh name that can incorporate the given string
+  freshNamed :: String -> Fresh a
+  freshNamed _ = fresh
+
+  -- | Refresh a name with an additional hint string
+  refreshNamed :: String -> a -> Fresh a
+  refreshNamed s n = freshNamed (s ++ varStr n)
+
+  -- | Gets the unique associated with a name.
+  getUnique :: a -> Int
+
+instance Name Int where
+  fresh     = Fresh (state (id &&& succ))
+  getUnique = id
+
diff --git a/src/Tip/Haskell/Rename.hs b/src/Tip/Haskell/Rename.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Haskell/Rename.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP #-}
+module Tip.Haskell.Rename (renameDecls, isOperator, RenameMap) where
+
+#include "errors.h"
+import Tip.Haskell.Repr
+import Tip.Haskell.Translate
+import Tip.Utils.Rename
+import Tip.Pretty
+
+import Data.Set (Set)
+import qualified Data.Set as S
+
+import Data.Map (Map)
+import qualified Data.Map as M
+
+import Data.Char
+
+import qualified Data.Foldable as F
+
+type RenameMap a = Map (HsId a) (HsId String)
+
+renameDecls :: forall a . (Ord a,PrettyVar a) => Decls (HsId a) -> (Decls (HsId String),RenameMap a)
+renameDecls ds = runRenameM suggest blocks M.empty (rename ds)
+  where
+  blocks = map Other (keywords ++ map snd hsBuiltins ++ exacts)
+
+  exacts :: [String]
+  exacts = [ s | Exact s <- F.toList ds ]
+        ++ [ s | Qualified _ _ s <- F.toList ds ]
+
+  suggest :: HsId a -> [HsId String]
+  suggest (Qualified m ms s) = Qualified m ms s:__
+  suggest (Exact s) = Exact s:__
+  suggest i
+    | i `S.member` us = map (Other . upper) (disambigHs (makeUniform (varStr i)))
+    | otherwise       = map (Other . lower) (disambigHs (makeUniform (varStr i)))
+
+  us = uppercase ds
+
+uppercase :: Ord a => Decls a -> Set a
+uppercase (Decls ds) = S.fromList $
+    [ x | TypeDef (TyCon x _) _ <- ds ] ++
+    [ x | DataDecl x _ _ _ <- ds ] ++
+    [ x | DataDecl _ _ cons _ <- ds, (x,_) <- cons ]
+
+makeUniform :: String -> String
+makeUniform s
+    | couldBeOperator s = filter (`elem` opSyms) s
+    | otherwise    = initialAlpha (filter isAlphaNum s)
+
+initialAlpha :: String -> String
+initialAlpha s@(c:_) | isAlpha c = s
+                     | otherwise = 'x':s
+
+disambigHs :: String -> [String]
+disambigHs s
+    | isOperator s = s : [ s ++ replicate n '.' | n <- [1..] ]
+    | otherwise    = disambig id s
+
+upper :: String -> String
+upper s@(c:r)
+    | isOperator s = if c == ':' then s else ':':s
+    | otherwise    = if isUpper c then s else toUpper c:r
+
+lower :: String -> String
+lower s@(c:r)
+    | isOperator s = if c == ':' then r else s
+    | otherwise    = if isLower c then s else toLower c:r
+
+isOperator :: String -> Bool
+isOperator = all (`elem` opSyms)
+
+couldBeOperator :: String -> Bool
+couldBeOperator s = i2d (numOps s) / i2d (length s) >= 0.5
+  where
+  i2d :: Int -> Double
+  i2d = fromInteger . toInteger
+
+numOps :: String -> Int
+numOps = length . filter (`elem` opSyms)
+
+opSyms :: String
+opSyms = "!#$%&*+./<=>?@\\^|-~:"
+
+keywords :: [String]
+keywords =
+  [ "!"
+  , "'"
+  , "''"
+  , "-"
+  , "--"
+  , "-<"
+  , "-<<"
+  , "->"
+  , "::"
+  , ";"
+  , "<-"
+  , ","
+  , "="
+  , "=>"
+  , ">"
+  , "?"
+  , "#"
+  , "*"
+  , "@"
+  , "\\"
+  , "_"
+  , "`"
+  , "|"
+  , "~"
+  , "as"
+  , "case", "of"
+  , "class"
+  , "data"
+  , "family"
+  , "instance"
+  , "default"
+  , "deriving"
+  , "do"
+  , "forall"
+  , "foreign"
+  , "hiding"
+  , "if", "then", "else"
+  , "import"
+  , "infix", "infixl", "infixr"
+  , "let", "in"
+  , "mdo"
+  , "module"
+  , "newtype"
+  , "proc"
+  , "qualified"
+  , "rec"
+  , "type"
+  , "family"
+  , "where"
+  ]
diff --git a/src/Tip/Haskell/Repr.hs b/src/Tip/Haskell/Repr.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Haskell/Repr.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+-- | A representation of Haskell programs
+module Tip.Haskell.Repr where
+
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable)
+
+data Decls a = Decls [Decl a]
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
+data Decl a
+  = TySig a
+          [Type a] {- class contexts -}
+          (Type a)
+  | FunDecl a [([Pat a],Expr a)]
+  | DataDecl a               {- type constructor name -}
+             [a]             {- type variables -}
+             [(a,[Type a])]  {- constructors -}
+             [a]             {- instance derivings -}
+  | InstDecl [Type a] {- context -}
+             (Type a) {- head -}
+             [Decl a] {- declarations (associated types and fun decls) -}
+  | TypeDef (Type a) (Type a)
+  | Decl a `Where` [Decl a]
+  | TH (Expr a)
+  | Module String
+  | LANGUAGE String
+  | QualImport String (Maybe String)
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
+funDecl :: a -> [a] -> Expr a -> Decl a
+funDecl f xs b = FunDecl f [(map VarPat xs,b)]
+
+data Type a
+  = TyCon a [Type a]
+  | TyVar a
+  | TyTup [Type a]
+  | TyArr (Type a) (Type a)
+  | TyForall [a] (Type a)
+  | TyCtx [Type a] (Type a)
+  | TyImp a (Type a)
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
+modTyCon :: (a -> a) -> Type a -> Type a
+modTyCon f t0 =
+  case t0 of
+    TyCon t ts  -> TyCon (f t) (map (modTyCon f) ts)
+    TyVar x     -> TyVar x
+    TyTup ts    -> TyTup (map (modTyCon f) ts)
+    TyArr t1 t2 -> TyArr (modTyCon f t1) (modTyCon f t2)
+
+data Expr a
+  = Apply a [Expr a]
+  | ImpVar a
+  | Do [Stmt a] (Expr a)
+  | Lam [Pat a] (Expr a)
+  | Let a (Expr a) (Expr a)
+  | ImpLet a (Expr a) (Expr a)
+  | List [Expr a] -- a literal list
+  | Tup [Expr a]  -- a literal tuple
+  | String a      -- string from a name...
+  | Noop          -- | @return ()@
+  | Case (Expr a) [(Pat a,Expr a)]
+  | Int Integer
+  | QuoteTyCon a -- Template Haskell ''
+  | QuoteName a  -- Template Haskell '
+  | THSplice (Expr a) -- Template Haskell $(..)
+  | Record (Expr a) [(a,Expr a)] -- record update
+  | Expr a ::: Type a
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
+nestedTyTup :: [Type a] -> Type a
+nestedTyTup []     = TyTup []
+nestedTyTup (t:ts) = TyTup [t,nestedTyTup ts]
+
+nestedTup :: [Expr a] -> Expr a
+nestedTup [] = Tup []
+nestedTup (d:ds) = Tup [d,nestedTup ds]
+
+nestedTupPat :: [Pat a] -> Pat a
+nestedTupPat []     = TupPat []
+nestedTupPat (d:ds) = TupPat [d,nestedTupPat ds]
+
+mkDo []      x = x
+mkDo ss1 (Do ss2 e) = mkDo (ss1 ++ ss2) e
+mkDo ss Noop = case (init ss,last ss) of
+  (i,Stmt e)   -> mkDo i e
+  (i,Bind x e) -> mkDo i e
+mkDo ss e = Do ss e
+
+var :: a -> Expr a
+var x = Apply x []
+
+data Pat a = VarPat a | ConPat a [Pat a] | TupPat [Pat a] | WildPat | IntPat Integer
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
+data Stmt a = Bind a (Expr a) | BindTyped a (Type a) (Expr a) | Stmt (Expr a)
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
diff --git a/src/Tip/Haskell/Translate.hs b/src/Tip/Haskell/Translate.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Haskell/Translate.hs
@@ -0,0 +1,509 @@
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP #-}
+module Tip.Haskell.Translate where
+
+#include "errors.h"
+import Tip.Haskell.Repr as H
+import Tip.Core as T hiding (Formula(..),globals,Type(..))
+import Tip.Core (Type((:=>:),BuiltinType))
+import qualified Tip.Core as T
+import Tip.Pretty
+import Tip.Utils
+import Tip.Scope
+
+import Tip.CallGraph
+
+import Control.Monad
+
+import qualified Data.Foldable as F
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable)
+
+import qualified Data.Map as M
+
+import Data.Generics.Geniplate
+
+import Data.List (nub,partition)
+
+prelude :: String -> HsId a
+prelude = Qualified "Prelude" (Just "P")
+
+tipDSL :: String -> HsId a
+tipDSL = Qualified "Tip" Nothing
+
+quickCheck :: String -> HsId a
+quickCheck = Qualified "Test.QuickCheck" (Just "QC")
+
+quickCheckUnsafe :: String -> HsId a
+quickCheckUnsafe = Qualified "Test.QuickCheck.Gen.Unsafe" (Just "QU")
+
+quickCheckAll :: String -> HsId a
+quickCheckAll = Qualified "Test.QuickCheck.All" (Just "QC")
+
+quickSpec :: String -> HsId a
+quickSpec = Qualified "QuickSpec" (Just "QS")
+
+feat :: String -> HsId a
+feat = Qualified "Test.Feat" (Just "F")
+
+typeable :: String -> HsId a
+typeable = Qualified "Data.Typeable" (Just "T")
+
+data HsId a
+    = Qualified
+         { qual_module       :: String
+         , qual_module_short :: Maybe String
+         , qual_func         :: String
+         }
+    -- ^ A qualified import
+    | Exact String
+    -- ^ The current module defines something with this very important name
+    | Other a
+    -- ^ From the theory
+    | Derived (HsId a) String
+    -- ^ For various purposes...
+  deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
+
+instance PrettyVar a => PrettyVar (HsId a) where
+  varStr (Qualified _ (Just m) s) = m ++ "." ++ s
+  varStr (Qualified m Nothing  s) = m ++ "." ++ s
+  varStr (Exact s) = s
+  varStr (Other x) = varStr x
+  varStr (Derived o s) = s ++ varStr o
+
+addHeader :: Decls a -> Decls a
+addHeader (Decls ds) =
+    Decls (map LANGUAGE ["TemplateHaskell","DeriveDataTypeable","TypeOperators","ImplicitParams","RankNTypes"] ++ Module "A" : ds)
+
+addImports :: Ord a => Decls (HsId a) -> Decls (HsId a)
+addImports d@(Decls ds) = Decls (QualImport "Text.Show.Functions" Nothing : imps ++ ds)
+  where
+  imps = usort [ QualImport m short | Qualified m short _ <- F.toList d ]
+
+trTheory :: (Ord a,PrettyVar a) => Theory a -> Decls (HsId a)
+trTheory = trTheory' . fmap Other
+
+data Kind = Expr | Formula deriving Eq
+
+theorySigs :: Theory (HsId a) -> [HsId a]
+theorySigs Theory{..} = map sig_name thy_sigs
+
+ufInfo :: Theory (HsId a) -> (Bool,[H.Type (HsId a)])
+ufInfo Theory{thy_sigs} = (not (null imps),imps)
+  where
+  imps = [TyImp (Derived f "imp") (H.TyCon (Derived f "") []) | Signature f _ <- thy_sigs]
+
+trTheory' :: forall a b . (a ~ HsId b,Ord b,PrettyVar b) => Theory a -> Decls a
+trTheory' thy@Theory{..} =
+  Decls $
+    concatMap tr_datatype thy_datatypes ++
+    map tr_sort thy_sorts ++
+    concatMap tr_sig thy_sigs ++
+    concatMap tr_func thy_funcs ++
+    tr_asserts thy_asserts ++
+    [makeSig thy]
+  where
+  (translate_UFs,imps) = ufInfo thy
+
+  tr_datatype :: Datatype a -> [Decl a]
+  tr_datatype (Datatype tc tvs cons) =
+    [ DataDecl tc tvs
+        [ (c,map (trType . snd) args) | Constructor c _ args <- cons ]
+        (map prelude ["Eq","Ord","Show"] ++ [typeable "Typeable"])
+    , TH (Apply (feat "deriveEnumerable") [QuoteTyCon tc])
+    , InstDecl [H.TyCon (feat "Enumerable") [H.TyVar a] | a <- tvs]
+               (H.TyCon (quickCheck "Arbitrary") [H.TyCon tc (map H.TyVar tvs)])
+               [funDecl
+                  (quickCheck "arbitrary") []
+                  (Apply (quickCheck "sized") [Apply (feat "uniform") []])]
+    ]
+
+  tr_sort :: Sort a -> Decl a
+  tr_sort (Sort _ i) | i /= 0 = error "Higher-kinded abstract sort"
+  tr_sort (Sort s i) = TypeDef (TyCon s []) (TyCon (prelude "Int") [])
+
+  tr_sig :: Signature a -> [Decl a]
+  tr_sig (Signature f pt) =
+    -- newtype f_NT = f_Mk (forall tvs . (Arbitrary a, CoArbitrary a) => T)
+    [ DataDecl (Derived f "") [] [ (Derived f "Mk",[tr_polyTypeArbitrary pt]) ] []
+    , FunDecl (Derived f "get")
+       [( [H.ConPat (Derived f "Mk") [VarPat (Derived f "x")]]
+        , var (Derived f "x")
+        )]
+
+    -- f :: (?f_imp :: f_NT) => T
+    -- f = f_get ?f_imp
+    , TySig f [] (tr_polyType pt)
+    , funDecl f [] (Apply (Derived f "get") [ImpVar (Derived f "imp")])
+
+    -- instance Arbitrary f_NT where
+    --   arbitrary = do
+    --      Capture x <- capture
+    --      return (f_Mk (x arbitrary))
+    , InstDecl [] (TyCon (quickCheck "Arbitrary") [TyCon (Derived f "") []])
+        [ funDecl (quickCheck "arbitrary") []
+          (mkDo [Bind (Derived f "x") (Apply (quickCheckUnsafe "capture") [])]
+                (H.Case (var (Derived f "x"))
+                   [(H.ConPat (quickCheckUnsafe "Capture") [VarPat (Derived f "y")]
+                    ,Apply (prelude "return")
+                    [Apply (Derived f "Mk")
+                    [Apply (Derived f "y")
+                    [Apply (quickCheck "arbitrary") []]]]
+                    )]
+                )
+          )
+        ]
+
+    -- gen :: Gen (Dict (?f_imp :: f_NT))
+    -- gen = do
+    --   x <- arbitrary
+    --   let ?f_imp = x
+    --   return Dict
+    , TySig (Derived f "gen") []
+        (TyCon (quickCheck "Gen")
+          [TyCon (quickSpec "Dict")
+            [TyImp (Derived f "imp") (TyCon (Derived f "") [])]])
+    , funDecl (Derived f "gen") []
+        (mkDo [Bind (Derived f "x") (Apply (quickCheck "arbitrary") [])]
+              (ImpLet (Derived f "imp") (var (Derived f "x"))
+                (Apply (prelude "return") [Apply (quickSpec "Dict") []])))
+    ]
+
+  tr_func :: Function a -> [Decl a]
+  tr_func fn@Function{..} =
+    [ TySig func_name [] (tr_polyType (funcType fn))
+    , FunDecl
+        func_name
+        [ (map tr_deepPattern dps,tr_expr Expr rhs)
+        | (dps,rhs) <- patternMatchingView func_args func_body
+        ]
+    ]
+
+  tr_asserts :: [T.Formula a] -> [Decl a]
+  tr_asserts fms =
+    let (names,decls) = unzip (zipWith tr_assert [1..] fms)
+    in  decls {- ++
+          [ TH (Apply (prelude "return") [List []])
+          , funDecl (Exact "main") []
+              (mkDo [ Stmt (THSplice (Apply (quickCheckAll "polyQuickCheck")
+                                            [QuoteName name]))
+                    | name <- names ]
+                    Noop)
+          ] -}
+
+  tr_assert :: Int -> T.Formula a -> (a,Decl a)
+  tr_assert i (T.Formula r _ b) =
+    (prop_name,funDecl prop_name args (assume (tr_expr Formula body)))
+    where
+    prop_name | i == 1    = Exact "prop"
+              | otherwise = Exact ("prop" ++ show i)
+    (args,body) =
+      case b of
+        Quant _ Forall lcls term -> (map lcl_name lcls,term)
+        _                        -> ([],b)
+
+    assume e =
+      case r of
+        Prove  -> e
+        Assert -> Apply (tipDSL "assume") [e]
+
+  tr_deepPattern :: DeepPattern a -> H.Pat a
+  tr_deepPattern (DeepConPat Global{..} dps) = H.ConPat gbl_name (map tr_deepPattern dps)
+  tr_deepPattern (DeepVarPat Local{..})      = VarPat lcl_name
+  tr_deepPattern (DeepLitPat (T.Int i))      = IntPat i
+  tr_deepPattern (DeepLitPat (Bool b))       = withBool H.ConPat b
+
+  tr_pattern :: T.Pattern a -> H.Pat a
+  tr_pattern Default = WildPat
+  tr_pattern (T.ConPat Global{..} xs) = H.ConPat gbl_name (map (VarPat . lcl_name) xs)
+  tr_pattern (T.LitPat (T.Int i))     = H.IntPat i
+  tr_pattern (T.LitPat (Bool b))      = withBool H.ConPat b
+
+  tr_expr :: Kind -> T.Expr a -> H.Expr a
+  tr_expr k e0 =
+    case e0 of
+      Builtin (Lit (T.Int i)) :@: [] -> H.Int i
+      Builtin (Lit (Bool b)) :@: []  -> withBool Apply b
+      hd :@: es -> let (f,k') = tr_head k hd
+                   in Apply f (map (tr_expr k') es)
+      Lcl x -> var (lcl_name x)
+      T.Lam xs b  -> H.Lam (map (VarPat . lcl_name) xs) (tr_expr Expr b)
+      Match e alts -> H.Case (tr_expr Expr e) [ (tr_pattern p,tr_expr Expr rhs) | T.Case p rhs <- default_last alts ]
+      T.Let x e b -> H.Let (lcl_name x) (tr_expr Expr e) (tr_expr k b)
+      T.Quant _ q xs b ->
+        foldr
+          (\ x e ->
+              Apply (tipDSL (case q of Forall -> "forAll"; Exists -> "exists"))
+                [H.Lam [VarPat (lcl_name x)] e])
+          (tr_expr Formula b)
+          xs
+
+    where
+    default_last (def@(T.Case Default _):alts) = alts ++ [def]
+    default_last alts = alts
+
+  tr_head :: Kind -> T.Head a -> (a,Kind)
+  tr_head k (Gbl Global{..}) = (gbl_name,Expr)
+  tr_head k (Builtin b)      = tr_builtin k b
+
+  tr_builtin :: Kind -> T.Builtin -> (a,Kind)
+  tr_builtin k b =
+    case b of
+      At        -> (prelude "id",Expr)
+      Lit{}     -> error "tr_builtin"
+      And       -> case_kind ".&&."
+      Or        -> case_kind ".||."
+      Not       -> case_kind "neg"
+      Implies   -> case_kind "==>"
+      Equal     -> case_kind "==="
+      Distinct  -> case_kind "=/="
+      _         -> prelude_fn
+    where
+    Just prelude_str_ = lookup b hsBuiltins
+    prelude_fn = (prelude prelude_str_,Expr)
+
+    case_kind sf =
+      case k of
+        Expr    -> prelude_fn
+        Formula -> (tipDSL sf,Formula)
+
+  -- ignores the type variables
+  tr_polyType_inner :: T.PolyType a -> H.Type a
+  tr_polyType_inner (PolyType _ ts t) = trType (ts :=>: t)
+
+  tr_polyType :: T.PolyType a -> H.Type a
+  tr_polyType pt@(PolyType tvs _ _)
+    | translate_UFs = TyForall tvs (TyCtx (arb tvs ++ imps) (tr_polyType_inner pt))
+    | otherwise     = tr_polyType_inner pt
+
+  -- translate type and add Arbitrary a, CoArbitrary a in the context for
+  -- all type variables a
+  tr_polyTypeArbitrary :: T.PolyType a -> H.Type a
+  tr_polyTypeArbitrary pt@(PolyType tvs _ _) = TyForall tvs (TyCtx (arb tvs) (tr_polyType_inner pt))
+
+  arb = arbitrary . map H.TyVar
+
+arbitrary :: [H.Type (HsId a)] -> [H.Type (HsId a)]
+arbitrary ts =
+  [ TyCon (quickCheck tc) [t]
+  | t <- ts
+  , tc <- ["Arbitrary","CoArbitrary"]
+  ]
+
+trType :: (a ~ HsId b) => T.Type a -> H.Type a
+trType (T.TyVar x)     = H.TyVar x
+trType (T.TyCon tc ts) = H.TyCon tc (map trType ts)
+trType (ts :=>: t)     = foldr TyArr (trType t) (map trType ts)
+trType (BuiltinType b) = trBuiltinType b
+
+trBuiltinType :: BuiltinType -> H.Type (HsId a)
+trBuiltinType t | Just s <- lookup t hsBuiltinTys = H.TyCon (prelude s) []
+
+withBool :: (a ~ HsId b) => (a -> [c] -> d) -> Bool -> d
+withBool k b = k (prelude (show b)) []
+
+-- * Builtins
+
+hsBuiltinTys :: [(T.BuiltinType,String)]
+hsBuiltinTys =
+  [ (Integer, "Int")
+  , (Boolean, "Bool")
+  ]
+
+hsBuiltins :: [(T.Builtin,String)]
+hsBuiltins =
+  [ (And      , "&&" )
+  , (Or       , "||" )
+  , (Not      , "not")
+  , (Implies  , "<=" )
+  , (Equal    , "==" )
+  , (Distinct , "/=" )
+  , (IntAdd   , "+"  )
+  , (IntSub   , "-"  )
+  , (IntMul   , "*"  )
+  , (IntDiv   , "div")
+  , (IntMod   , "mod")
+  , (IntGt    , ">"  )
+  , (IntGe    , ">=" )
+  , (IntLt    , "<"  )
+  , (IntLe    , "<=" )
+  ]
+
+typeOfBuiltin :: Builtin -> T.Type a
+typeOfBuiltin b = case b of
+  And      -> bbb
+  Or       -> bbb
+  Not      -> bb
+  Implies  -> bbb
+  Equal    -> iib -- TODO: equality could be used on other types than int
+  Distinct -> iib -- ditto
+  IntAdd   -> iii
+  IntSub   -> iii
+  IntMul   -> iii
+  IntDiv   -> iii
+  IntMod   -> iii
+  IntGt    -> iib
+  IntGe    -> iib
+  IntLt    -> iib
+  IntLe    -> iib
+  _        -> __
+  where
+  bb  = [boolType] :=>: boolType
+  bbb = [boolType,boolType] :=>: boolType
+  iii = [intType,intType] :=>: intType
+  iib = [intType,intType] :=>: boolType
+
+
+-- * QuickSpec signatures
+
+makeSig :: forall a . (PrettyVar a,Ord a) => Theory (HsId a) -> Decl (HsId a)
+makeSig thy@Theory{..} =
+  funDecl (Exact "sig") [] $
+    Tup
+      [ List
+          [ Tup
+              [ constant_decl ft
+              , List $
+                  if use_cg
+                    then
+                      [ int_lit num
+                      | (members,num) <- cg `zip` [0..]
+                      , f `elem` members
+                      ]
+                    else
+                      [int_lit 0]
+
+              ]
+          | ft@(f,_) <- func_constants
+          ]
+      , Apply (quickSpec "signature") [] `Record`
+          [ (quickSpec "constants",
+               List $
+                 builtin_decls ++
+                 map constant_decl
+                   (ctor_constants ++ builtin_constants))
+          , (quickSpec "instances", List $
+               [ mk_inst [] (mk_class (feat "Enumerable") (H.TyCon (prelude "Int") [])) ] ++
+               [ mk_inst (map (mk_class c1) tys) (mk_class c2 (H.TyCon t tys))
+               | (t,n) <- type_univ
+               , (c1, c2) <- [(prelude "Ord", prelude "Ord"),
+                              (feat "Enumerable", feat "Enumerable"),
+                              (feat "Enumerable",quickCheck "Arbitrary")]
+               , let tys = map trType (qsTvs n)
+               ] ++
+               [ Apply (quickSpec "makeInstance") [H.Lam [TupPat []] (Apply (Derived f "gen") [])]
+               | Signature f _ <- thy_sigs
+               ])
+          , (quickSpec "maxTermSize", Apply (prelude "Just") [H.Int (if translate_UFs then 15 else 7)])
+          , (quickSpec "testTimeout", Apply (prelude "Just") [H.Int 100000])
+          ]
+      ]
+  where
+  (translate_UFs,imps) = ufInfo thy
+
+  use_cg = True
+
+  int_lit x = H.Int x ::: H.TyCon (prelude "Int") []
+
+  mk_inst ctx res =
+    Apply (quickSpec ("inst" ++ concat [ show (length ctx) | length ctx >= 2 ]))
+                 [ Apply (quickSpec "Sub") [Apply (quickSpec "Dict") []] :::
+                   H.TyCon (quickSpec ":-") [TyTup ctx,res] ]
+
+  mk_class c x = H.TyCon c [x]
+
+  scp = scope thy
+
+  cg = map (map defines) (flatCallGraph (CallGraphOpts True False) thy)
+
+  poly_type (PolyType _ args res) = args :=>: res
+
+  constant_decl (f,t) =
+    Apply (quickSpec "constant") [H.String f,lam (Apply f []) ::: qs_type]
+    where
+    (pre,qs_type) = qsType t
+    lam | null pre  = id
+        | otherwise = H.Lam (replicate (length pre) (H.ConPat (quickSpec "Dict") []))
+
+  int_lit_decl x =
+    Apply (quickSpec "constant") [H.String (Exact (show x)),int_lit x]
+
+  bool_lit_decl b =
+    Apply (quickSpec "constant") [H.String (prelude (show b)),withBool Apply b]
+
+  ctor_constants =
+    [ (f,poly_type (globalType g))
+    | (f,g@ConstructorInfo{}) <- M.toList (globals scp)
+    ]
+
+  func_constants =
+    [ (f,poly_type (globalType g))
+    | (f,g@FunctionInfo{}) <- M.toList (globals scp)
+    ]
+
+  type_univ =
+    [ (data_name, length data_tvs)
+    | (_,DatatypeInfo Datatype{..}) <- M.toList (types scp)
+    ]
+
+  -- builtins
+
+  (builtin_lits,builtin_funs) =
+    partition litBuiltin $
+      usort
+        [ b
+        | Builtin b :@: args <- universeBi thy
+
+        -- only count equality if argument is int:
+        , let is_int = case args of
+                         a1:_ -> exprType a1 == (intType :: T.Type (HsId a))
+                         _    -> __
+        , case b of
+            Equal    -> is_int
+            Distinct -> is_int
+            _         -> True
+        ]
+
+  used_builtin_types :: [BuiltinType]
+  used_builtin_types =
+    usort [ t | BuiltinType t :: T.Type (HsId a) <- universeBi thy ]
+
+  bool_used = Boolean `elem` used_builtin_types
+  int_used  = -- Integer `elem` used_builtin_types
+              or [ op `elem` builtin_funs | op <- [IntAdd,IntSub,IntMul,IntDiv,IntMod] ]
+
+  builtin_decls
+    =  [ bool_lit_decl b | bool_used, b <- [False,True] ]
+    ++ [ int_lit_decl x  | int_used,  x <- [0,1] ++
+                                           [ x
+                                           | Lit (T.Int x) <- builtin_lits ]]
+
+  builtin_constants
+    =  [ (prelude s,typeOfBuiltin b)
+       | b <- nub $
+              [ b      | bool_used, b <- [And,Or,Not] ]
+           -- [ IntAdd | int_used ]
+           -- [ Equal  | bool_used && int_used ]
+           ++ [ b | b <- builtin_funs, intBuiltin b || eqRelatedBuiltin b ]
+       , Just s <- [lookup b hsBuiltins]
+       ]
+
+  qsType :: Ord a => T.Type (HsId a) -> ([H.Type (HsId a)],H.Type (HsId a))
+  qsType t = (pre,foldr TyArr inner [ TyCon (quickSpec "Dict") [p] | p <- pre ])
+    where
+    pre | translate_UFs = arbitrary (map trType qtvs) ++ imps
+        | otherwise     = []
+    inner = trType (applyType tvs qtvs t)
+    qtvs = qsTvs (length tvs)
+    tvs = tyVars t
+
+  qsTvs :: Int -> [T.Type (HsId a)]
+  qsTvs n = take n (cycle [ T.TyCon (quickSpec qs_tv) [] | qs_tv <- ["A","B","C","D","E"] ])
+
+theoryBuiltins :: Ord a => Theory a -> [T.Builtin]
+theoryBuiltins = usort . universeBi
+
diff --git a/src/Tip/Lint.hs b/src/Tip/Lint.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Lint.hs
@@ -0,0 +1,259 @@
+{-# LANGUAGE CPP, RecordWildCards, OverloadedStrings, FlexibleContexts, ViewPatterns #-}
+-- | Check that a theory is well-typed.
+--
+-- Invariants:
+--
+--  * No shadowing---checked by scope monad.
+--
+--  * Each local is bound before it's used.
+--
+--  * All expressions are well-typed.
+--
+--  * The result of each constructor should be a value of that datatype.
+--
+--  * Default case comes first. No duplicate cases.
+--
+--  * Expressions and formulas not mixed.
+module Tip.Lint (lint, lintM, lintTheory) where
+
+#include "errors.h"
+import Tip.Core
+import Tip.Scope
+import Tip.Pretty
+import Tip.Rename
+import Control.Monad
+import Control.Monad.Error
+import Control.Monad.State
+import Data.Maybe
+import Text.PrettyPrint
+import Tip.Pretty.SMT
+import Data.List
+--import Debug.Trace
+
+-- | Crashes if the theory is malformed
+lint :: (PrettyVar a, Ord a) => String -> Theory a -> Theory a
+lint pass thy0@(renameAvoiding [] return -> thy) =
+  -- trace ("Linting:" ++ pass ++ ":\n" ++ ppRender thy) $
+  case lintTheory thy0 of
+    Nothing -> thy0
+    Just doc ->
+      case lintTheory thy of
+        Just doc ->
+          error ("Lint failed after " ++ pass ++ ":\n" ++ show doc ++ "\n!!!")
+        Nothing ->
+          error ("Non-renamed linting pass failed!? " ++ pass ++ ":\n" ++ show doc ++ "\n!!!")
+
+-- | Same as 'lint', but returns in a monad, for convenience
+lintM :: (PrettyVar a, Ord a, Monad m) => String -> Theory a -> m (Theory a)
+lintM pass = return . lint pass
+
+check :: (PrettyVar a, Ord a) => Doc -> (Scope a -> Bool) -> ScopeM a ()
+check x p = check' x (guard . p)
+
+check' :: (PrettyVar a, Ord a) => Doc -> (Scope a -> Maybe b) -> ScopeM a b
+check' x p = do
+  scp <- get
+  case p scp of
+    Nothing -> throwError x
+    Just y  -> return y
+
+-- | Returns the error if the theory is malformed
+lintTheory :: (PrettyVar a, Ord a) => Theory a -> Maybe Doc
+lintTheory thy@Theory{..} =
+  either Just (const Nothing) .
+  runScope . withTheory thy $ inContext thy $ do
+    mapM_ lintDatatype thy_datatypes
+    mapM_ lintSignature thy_sigs
+    mapM_ lintFunction thy_funcs
+    mapM_ lintFormula thy_asserts
+
+lintDatatype :: (PrettyVar a, Ord a) => Datatype a -> ScopeM a ()
+lintDatatype dt@Datatype{..} =
+  local $ inContext dt $ do
+    mapM_ newTyVar data_tvs
+    forM_ data_cons $ \Constructor{..} -> do
+      forM_ con_args $ \(_, ty) ->
+        lintType ty
+
+lintPolyType :: (PrettyVar a, Ord a) => PolyType a -> ScopeM a ()
+lintPolyType polyty@PolyType{..} =
+  newScope $ inContext polyty $ do
+    mapM_ newTyVar polytype_tvs
+    mapM_ lintType polytype_args
+    lintType polytype_res
+
+lintType :: (PrettyVar a, Ord a) => Type a -> ScopeM a ()
+lintType (TyVar x) =
+  check (fsep ["Type variable", nest 2 (ppVar x), "not in scope"])
+    (isTyVar x)
+lintType (TyCon x tys) = do
+  info <- check' (fsep ["Type constructor", nest 2 (ppVar x), "not in scope"])
+    (lookupType x)
+  let checkArity n =
+        unless (n == length tys) $
+          throwError $ fsep [
+            "Type constructor", nest 2 (ppVar x),
+            "of arity" <+> int n,
+            "applied to" <+> int (length tys) <+> "type arguments"]
+  case info of
+    TyVarInfo ->
+      throwError (fsep ["Type variable", nest 2 (ppVar x), "used as type constructor"])
+    SortInfo n -> checkArity n
+    DatatypeInfo Datatype{..} -> checkArity (length data_tvs)
+  mapM_ lintType tys
+lintType (args :=>: res) = do
+  mapM_ lintType args
+  lintType res
+lintType BuiltinType{} = return ()
+
+lintSignature :: (PrettyVar a, Ord a) => Signature a -> ScopeM a ()
+lintSignature func@Signature{..} =
+  inContext func (lintPolyType sig_type)
+
+lintFunction :: (PrettyVar a, Ord a) => Function a -> ScopeM a ()
+lintFunction func@Function{..} =
+  local $ inContext func $ do
+    mapM_ newTyVar func_tvs
+    mapM_ lintBinder func_args
+    lintType func_res
+    lintExpr ExprKind func_body
+    unless (func_res == exprType func_body) $
+      throwError (fsep [
+        "Declared return type", nest 2 (pp func_res),
+        "does not match actual return type", nest 2 (pp (exprType func_body))])
+
+lintBinder :: (PrettyVar a, Ord a) => Local a -> ScopeM a ()
+lintBinder lcl@Local{..} = do
+  lintType lcl_type
+  newLocal lcl
+
+lintFormula :: (PrettyVar a, Ord a) => Formula a -> ScopeM a ()
+lintFormula form@(Formula _ tvs expr) =
+  local $ inContext form $ do
+    mapM_ newTyVar tvs
+    lintExpr FormulaKind expr
+    unless (exprType expr == boolType) $
+      throwError $
+        fsep ["Formula has non-boolean type", nest 2 (pp (exprType expr))]
+
+data ExprKind = ExprKind | FormulaKind deriving Eq
+
+lintExpr :: (PrettyVar a, Ord a) => ExprKind -> Expr a -> ScopeM a ()
+lintExpr _ (Gbl gbl@Global{..} :@: exprs) = do
+  lintGlobal gbl
+  mapM_ (lintExpr ExprKind) exprs
+  let (args, _) = applyPolyType gbl_type gbl_args
+  lintCall (Gbl gbl) exprs args
+lintExpr kind (Builtin bltin :@: exprs) = do
+  mapM_ (lintExpr (if isExpression bltin then ExprKind else kind)) exprs
+  tys <- lintBuiltin bltin (map exprType exprs)
+  lintCall (Builtin bltin) exprs tys
+lintExpr _ (Lcl lcl@Local{..}) = do
+  check ("Unbound variable" <+> pp lcl) (isLocal lcl_name)
+  check ("Inconsistent type for local" <+> pp lcl) $
+    \scp -> whichLocal lcl_name scp == lcl_type
+lintExpr kind (Lam lcls expr) =
+  local $ do
+    mapM_ lintBinder lcls
+    lintExpr ExprKind expr
+lintExpr kind (Match expr cases) = do
+  lintExpr (if kind == FormulaKind && exprType expr /= boolType then ExprKind else kind)
+    expr
+  when (null cases) $
+    throwError "Case with no alternatives"
+  mapM_ (lintCase kind expr) cases
+
+  when (Default `elem` drop 1 (map case_pat cases)) $
+    throwError "Default case is in wrong position"
+  unless (Default `elem` map case_pat cases) $ do
+    let strip (ConPat gbl _) = ConPat gbl []
+        strip x = x
+        stripped = map (strip . case_pat) cases
+    unless (nub stripped == stripped) $
+      throwError "The same constructor appears several times"
+  unless (length (nub (map (exprType . case_rhs) cases)) == 1) $
+    throwError "Not all case clauses have the same type"
+lintExpr kind (Let lcl@Local{..} expr body) = do
+  lintExpr ExprKind expr
+  local $ do
+    lintBinder lcl
+    lintExpr kind body
+  unless (lcl_type == exprType expr) $
+    throwError (fsep [
+      "Expression of type", nest 2 (pp (exprType expr)),
+      "bound to variable" <+> pp lcl,
+      "of type", nest 2 (pp lcl_type)])
+lintExpr ExprKind (Quant NoInfo _ lcls expr) =
+  throwError "Quantifier found in expression"
+lintExpr FormulaKind (Quant NoInfo _ lcls expr) =
+  local $ do
+    mapM_ lintBinder lcls
+    lintExpr FormulaKind expr
+
+lintGlobal :: (PrettyVar a, Ord a) => Global a -> ScopeM a ()
+lintGlobal gbl@Global{..} = do
+  lintPolyType gbl_type
+  mapM_ lintType gbl_args
+  unless (length gbl_args == length (polytype_tvs gbl_type)) $
+    throwError (fsep ["Global" <+> pp gbl, "applied to type arguments", nest 2 (vcat (map pp gbl_args)), "but expects" <+> int (length (polytype_tvs gbl_type))])
+  check ("Unbound global" <+> pp gbl) (isGlobal gbl_name)
+
+  scp <- get
+  check (fsep ["Global" <+> pp gbl, "occurs with type", nest 2 (ppPolyType gbl_type), "but was declared with type", nest 2 (ppPolyType (globalType (whichGlobal gbl_name scp)))]) $
+    \scp -> globalType (whichGlobal gbl_name scp) `polyEq` gbl_type
+    where
+      t `polyEq` PolyType{..} =
+        applyPolyType t (map TyVar polytype_tvs) == (polytype_args, polytype_res)
+
+lintCall :: (PrettyVar a, Ord a) => Head a -> [Expr a] -> [Type a] -> ScopeM a ()
+lintCall hd exprs args =
+  unless (args == map exprType exprs) $
+    throwError (fsep ["Function" <+> pp hd, "which expects arguments of type", nest 2 (vcat (map pp args)), "applied to arguments of type", nest 2 (vcat (map pp (map exprType exprs))), "in", nest 2 (pp (hd :@: exprs))])
+
+lintBuiltin :: (PrettyVar a, Ord a) => Builtin -> [Type a] -> ScopeM a [Type a]
+lintBuiltin At [] = throwError "@ cannot have arity 0"
+lintBuiltin At ((args :=>: res):_) =
+  return ((args :=>: res):args)
+lintBuiltin At (ty:_) =
+  throwError (fsep ["First argument of @ has non-function type", nest 2 (pp ty)])
+lintBuiltin Lit{} _ = return []
+lintBuiltin And tys = return (replicate (length tys) boolType)
+lintBuiltin Or tys = return (replicate (length tys) boolType)
+lintBuiltin Not _ = return [boolType]
+lintBuiltin Implies _ = return [boolType, boolType]
+lintBuiltin Equal [] = throwError "Nullary ="
+lintBuiltin Equal tys@(ty:_) = return (replicate (length tys) ty)
+lintBuiltin Distinct [] = throwError "Nullary distinct"
+lintBuiltin Distinct tys@(ty:_) = return (replicate (length tys) ty)
+lintBuiltin IntAdd tys = return (replicate (length tys) intType)
+lintBuiltin IntSub _ = return [intType, intType]
+lintBuiltin IntMul _ = return [intType, intType]
+lintBuiltin IntDiv _ = return [intType, intType]
+lintBuiltin IntMod _ = return [intType, intType]
+lintBuiltin IntGt _ = return [intType, intType]
+lintBuiltin IntGe _ = return [intType, intType]
+lintBuiltin IntLt _ = return [intType, intType]
+lintBuiltin IntLe _ = return [intType, intType]
+
+isExpression :: Builtin -> Bool
+isExpression Equal = True
+isExpression Distinct = True
+isExpression IntGt = True
+isExpression IntGe = True
+isExpression IntLt = True
+isExpression IntLe = True
+isExpression _ = False
+
+lintCase :: (PrettyVar a, Ord a) => ExprKind -> Expr a -> Case a -> ScopeM a ()
+lintCase kind _ (Case Default body) = lintExpr kind body
+lintCase kind _ (Case LitPat{} body) = lintExpr kind body
+lintCase kind expr (Case (ConPat gbl@Global{..} args) body) =
+  local $ do
+    mapM_ lintBinder args
+    lintExpr kind (Gbl gbl :@: map Lcl args)
+    lintExpr kind body
+    check ("Global" <+> pp gbl <+> "used as constructor")
+      (isJust . lookupConstructor gbl_name)
+    let (_, res) = applyPolyType gbl_type gbl_args
+    unless (res == exprType expr) $
+      throwError (fsep ["Constructor", nest 2 (pp (Gbl gbl :@: map Lcl args)), "has type", nest 2 (pp res), "but should be", nest 2 (pp (exprType expr))])
diff --git a/src/Tip/Parser.hs b/src/Tip/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Parser.hs
@@ -0,0 +1,19 @@
+-- | Parses the TIP format
+module Tip.Parser(parse,Id,idPos) where
+
+import Data.Monoid
+
+import Tip.Parser.ParTIP
+import Tip.Parser.AbsTIP (Start(..))
+import Tip.Parser.ErrM
+
+import Tip.Parser.Convert
+import Tip.Core
+
+-- | Parse, and get either an error or the string's theory
+parse :: String -> Either String (Theory Id)
+parse s =
+  case pStart . myLexer $ s of
+    Ok (Start ds) -> runCM (trDecls ds)
+    Bad err       -> Left err
+
diff --git a/src/Tip/Parser/AbsTIP.hs b/src/Tip/Parser/AbsTIP.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Parser/AbsTIP.hs
@@ -0,0 +1,119 @@
+
+
+module Tip.Parser.AbsTIP where
+
+-- Haskell module generated by the BNF converter
+
+
+
+
+newtype Symbol = Symbol ((Int,Int),String) deriving (Eq,Ord,Show,Read)
+data Start =
+   Start [Decl]
+  deriving (Eq,Ord,Show,Read)
+
+data Decl =
+   DeclareDatatypes [Symbol] [Datatype]
+ | DeclareSort Symbol Integer
+ | DeclareFun FunDecl
+ | DefineFunsRec [FunDef] [Expr]
+ | MonoAssert Assertion Expr
+ | ParAssert Assertion [Symbol] Expr
+  deriving (Eq,Ord,Show,Read)
+
+data Assertion =
+   AssertIt
+ | AssertNot
+  deriving (Eq,Ord,Show,Read)
+
+data FunDef =
+   ParFunDef [Symbol] InnerFunDef
+ | MonoFunDef InnerFunDef
+  deriving (Eq,Ord,Show,Read)
+
+data InnerFunDef =
+   InnerFunDef Symbol [Binding] Type
+  deriving (Eq,Ord,Show,Read)
+
+data FunDecl =
+   ParFunDecl [Symbol] InnerFunDecl
+ | MonoFunDecl InnerFunDecl
+  deriving (Eq,Ord,Show,Read)
+
+data InnerFunDecl =
+   InnerFunDecl Symbol [Type] Type
+  deriving (Eq,Ord,Show,Read)
+
+data Datatype =
+   Datatype Symbol [Constructor]
+  deriving (Eq,Ord,Show,Read)
+
+data Constructor =
+   Constructor Symbol [Binding]
+  deriving (Eq,Ord,Show,Read)
+
+data Binding =
+   Binding Symbol Type
+  deriving (Eq,Ord,Show,Read)
+
+data LetDecl =
+   LetDecl Binding Expr
+  deriving (Eq,Ord,Show,Read)
+
+data Type =
+   TyVar Symbol
+ | TyApp Symbol [Type]
+ | ArrowTy [Type]
+ | IntTy
+ | BoolTy
+  deriving (Eq,Ord,Show,Read)
+
+data Expr =
+   Var Symbol
+ | As Expr Type
+ | App Head [Expr]
+ | Match Expr [Case]
+ | Let [LetDecl] Expr
+ | Binder Binder [Binding] Expr
+ | LitInt Integer
+ | LitTrue
+ | LitFalse
+  deriving (Eq,Ord,Show,Read)
+
+data Binder =
+   Lambda
+ | Forall
+ | Exists
+  deriving (Eq,Ord,Show,Read)
+
+data Case =
+   Case Pattern Expr
+  deriving (Eq,Ord,Show,Read)
+
+data Pattern =
+   Default
+ | ConPat Symbol [Symbol]
+ | SimplePat Symbol
+  deriving (Eq,Ord,Show,Read)
+
+data Head =
+   Const Symbol
+ | At
+ | IfThenElse
+ | And
+ | Or
+ | Not
+ | Implies
+ | Equal
+ | Distinct
+ | IntAdd
+ | IntSub
+ | IntMul
+ | IntDiv
+ | IntMod
+ | IntGt
+ | IntGe
+ | IntLt
+ | IntLe
+  deriving (Eq,Ord,Show,Read)
+
diff --git a/src/Tip/Parser/Convert.hs b/src/Tip/Parser/Convert.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Parser/Convert.hs
@@ -0,0 +1,302 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Tip.Parser.Convert where
+
+import Tip.Parser.AbsTIP as A -- from A ...
+import Tip.Core          as T -- ... to T
+import Tip.Pretty
+import Tip.Pretty.SMT
+
+import Text.PrettyPrint
+import Control.Applicative
+import Control.Monad.State
+import Control.Monad.Error
+import Data.Foldable (foldrM)
+
+import qualified Tip.Scope
+import Tip.Scope
+import Tip.Fresh
+
+import Data.List
+import Data.Function
+
+import Data.Map (Map)
+import qualified Data.Map as M
+
+data IdKind = LocalId | GlobalId
+  deriving Eq
+
+type CM a = ScopeT Id (StateT (Map String (Id,IdKind)) Fresh) a
+
+runCM :: CM a -> Either String a
+runCM m = either (Left . show) Right $ runFresh (evalStateT (runScopeT m) M.empty)
+
+-- | Identifiers from parsed Tip syntax
+data Id = Id
+  { idString :: String
+  , idUnique :: Int
+  , idPos    :: Maybe (Int,Int)
+  -- ^ A source position of the identifier, if available
+  }
+  deriving Show
+
+instance Eq Id where
+  (==) = (==) `on` idUnique
+
+instance Ord Id where
+  compare = compare `on` idUnique
+
+instance PrettyVar Id where
+  varStr (Id s _ _) = s
+
+instance Name Id where
+  freshNamed n
+    = do u <- fresh
+         return (Id n u Nothing)
+
+  fresh = freshNamed "x"
+
+  refresh = refreshNamed ""
+
+  getUnique (Id _ u _) = u
+
+ppSym :: Symbol -> Doc
+ppSym (Symbol ((x,y),s)) = text s <+> "(" <> int x <> ":" <> int y <> ")"
+
+lkSym :: Symbol -> CM Id
+lkSym sym@(Symbol (p,s)) =
+  do mik <- lift $ gets (M.lookup s)
+     case mik of
+       Just (i,_) -> return $ i { idPos = Just p }
+       Nothing    -> throwError $ "Symbol" <+> ppSym sym <+> "not bound"
+
+addSym :: IdKind -> Symbol -> CM Id
+addSym ik sym@(Symbol (p,s)) =
+  do mik <- lift $ gets (M.lookup s)
+     case mik of
+       Just (_,GlobalId)       -> throwError $ "Symbol" <+> ppSym sym <+> "is already globally bound"
+       Just _ | ik == GlobalId -> throwError $ "Symbol" <+> ppSym sym <+> "is locally bound, and cannot be overwritten by a global"
+       _                       -> return ()
+     u <- lift (lift fresh)
+     let i = Id s u (Just p)
+     lift $ modify (M.insert s (i,ik))
+     return i
+
+trDecls :: [Decl] -> CM (Theory Id)
+trDecls [] = return emptyTheory
+trDecls (d:ds) =
+  do thy <- trDecl d
+     withTheory thy $
+       do thy_rest <- trDecls ds
+          return (thy `joinTheories` thy_rest)
+
+trDecl :: Decl -> CM (Theory Id)
+trDecl x =
+  local $
+    case x of
+      DeclareDatatypes tvs datatypes ->
+        do -- add their types, abstractly
+           forM_ datatypes $ \dt -> do
+             sym <- addSym GlobalId (dataSym dt)
+             newSort (Sort sym (length tvs))
+           newScope $
+             do tvi <- mapM (addSym LocalId) tvs
+                mapM newTyVar tvi
+                ds <- mapM (trDatatype tvi) datatypes
+                return emptyTheory{ thy_datatypes = ds }
+
+      DeclareSort s n ->
+        do i <- addSym GlobalId s
+           return emptyTheory{ thy_sorts = [Sort i (fromIntegral n)] }
+
+      DeclareFun fundecl ->
+        do d <- trFunDecl fundecl
+           return emptyTheory{ thy_sigs = [d] }
+
+      DefineFunsRec fundefs bodies ->
+        do -- add their correct types, abstractly
+           fds <- mapM (trFunDecl . defToDecl) fundefs
+           withTheory emptyTheory{ thy_sigs = fds } $ do
+             fns <- zipWithM trFunDef fundefs bodies
+             return emptyTheory{ thy_funcs = fns }
+
+      MonoAssert role expr    -> trDecl (ParAssert role [] expr)
+      ParAssert role tvs expr ->
+        do tvi <- mapM (addSym LocalId) tvs
+           mapM newTyVar tvi
+           let toRole AssertIt  = Assert
+               toRole AssertNot = Prove
+           fm <- Formula (toRole role) tvi <$> trExpr expr
+           return emptyTheory{ thy_asserts = [fm] }
+
+
+
+defToDecl :: FunDef -> FunDecl
+defToDecl x = case x of
+  MonoFunDef inner -> defToDecl (ParFunDef [] inner)
+  ParFunDef tvs (InnerFunDef fsym bindings res_type) ->
+    ParFunDecl tvs (InnerFunDecl fsym (map bindingType bindings) res_type)
+
+trFunDef :: FunDef -> A.Expr -> CM (T.Function Id)
+trFunDef x body = case x of
+  MonoFunDef inner -> trFunDef (ParFunDef [] inner) body
+  ParFunDef tvs (InnerFunDef fsym bindings res_type) ->
+    newScope $
+      do f <- lkSym fsym
+         tvi <- mapM (addSym LocalId) tvs
+         mapM newTyVar tvi
+         args <- mapM trLocalBinding bindings
+         Function f tvi args <$> trType res_type <*> trExpr body
+
+trFunDecl :: FunDecl -> CM (T.Signature Id)
+trFunDecl x = case x of
+  MonoFunDecl inner -> trFunDecl (ParFunDecl [] inner)
+  ParFunDecl tvs (InnerFunDecl fsym args res) ->
+    newScope $
+      do f <- addSym GlobalId fsym
+         tvi <- mapM (addSym LocalId) tvs
+         mapM newTyVar tvi
+         pt <- PolyType tvi <$> mapM trType args <*> trType res
+         return (Signature f pt)
+
+dataSym :: A.Datatype -> Symbol
+dataSym (A.Datatype sym _) = sym
+
+trDatatype :: [Id] -> A.Datatype -> CM (T.Datatype Id)
+trDatatype tvs (A.Datatype sym constructors) =
+  do x <- lkSym sym
+     T.Datatype x tvs <$> mapM trConstructor constructors
+
+trConstructor :: A.Constructor -> CM (T.Constructor Id)
+trConstructor (A.Constructor name@(Symbol (p,s)) args) =
+  do c <- addSym GlobalId name
+     is_c <- addSym GlobalId (Symbol (p,"is-" ++ s))
+     T.Constructor c is_c <$> mapM (trBinding GlobalId) args
+
+bindingType :: Binding -> A.Type
+bindingType (Binding _ t) = t
+
+-- adds to the symbol map
+trBinding :: IdKind -> Binding -> CM (Id,T.Type Id)
+trBinding ik (Binding s t) =
+  do i <- addSym ik s
+     t' <- trType t
+     return (i,t')
+
+-- adds to the symbol map and to the local scope
+trLocalBinding :: Binding -> CM (Local Id)
+trLocalBinding b =
+  do (x,t) <- trBinding LocalId b
+     let l = Local x t
+     newLocal l
+     return l
+
+trLetDecls :: [LetDecl] -> A.Expr -> CM (T.Expr Id)
+trLetDecls [] e = trExpr e
+trLetDecls (LetDecl binding expr:bs) e
+  = newScope $ T.Let <$> trLocalBinding binding <*> trExpr expr <*> trLetDecls bs e
+
+trExpr :: A.Expr -> CM (T.Expr Id)
+trExpr e0 = case e0 of
+  A.Var sym ->
+    do x <- lkSym sym
+       ml <- gets (lookupLocal x)
+       case ml of
+         Just t -> return (Lcl (Local x t))
+         _      -> trExpr (A.App (A.Const sym) [])
+
+  A.As (A.Var sym) ty -> trExpr (A.As (A.App (A.Const sym) []) ty)
+  A.As (A.App head exprs) ty -> do ty' <- trType ty
+                                   trHead (Just ty') head =<< mapM trExpr exprs
+  A.As e _ -> trExpr e
+
+  A.App head exprs           -> trHead Nothing head =<< mapM trExpr exprs
+
+  A.Match expr cases  -> do e <- trExpr expr
+                            cases' <- sort <$> mapM (trCase (exprType e)) cases
+                            return (T.Match e cases')
+  A.Let letdecls expr -> trLetDecls letdecls expr
+  A.Binder binder bindings expr -> newScope $ trBinder binder <$> mapM trLocalBinding bindings <*> trExpr expr
+  A.LitInt n -> return $ intLit n
+  A.LitTrue  -> return $ bool True
+  A.LitFalse -> return $ bool False
+
+trHead :: Maybe (T.Type Id) -> A.Head -> [T.Expr Id] -> CM (T.Expr Id)
+trHead mgt A.IfThenElse  [c,t,f] = return (makeIf c t f)
+trHead mgt A.IfThenElse  args    = throwError $ "if-then-else with " <+> int (length args) <+> " arguments!"
+trHead mgt (A.Const sym) args    =
+  do x <- lkSym sym
+     mt <- gets (fmap globalType . lookupGlobal x)
+     case mt of
+       Just pt
+         | Just gbl <- makeGlobal x pt (map exprType args) mgt
+         -> return (Gbl gbl :@: args)
+         | otherwise
+         -> throwError $ "Not a well-applied global:" <+> ppSym sym
+                      $$ " with goal type " <+> case mgt of Nothing -> "Nothing"; Just t -> pp t
+                      $$ " with argument types " <+> fsep (punctuate "," (map (pp . exprType) args))
+                      $$ " with polymorphic type " <+> pp pt
+       _ -> throwError $ "No type information for:" <+> ppSym sym
+
+trHead _ x args = return (Builtin b :@: args)
+ where
+  b = case x of
+    A.At       -> T.At
+    A.And      -> T.And
+    A.Or       -> T.Or
+    A.Not      -> T.Not
+    A.Implies  -> T.Implies
+    A.Equal    -> T.Equal
+    A.Distinct -> T.Distinct
+    A.IntAdd   -> T.IntAdd
+    A.IntSub   -> T.IntSub
+    A.IntMul   -> T.IntMul
+    A.IntDiv   -> T.IntDiv
+    A.IntMod   -> T.IntMod
+    A.IntGt    -> T.IntGt
+    A.IntGe    -> T.IntGe
+    A.IntLt    -> T.IntLt
+    A.IntLe    -> T.IntLe
+
+
+trBinder :: A.Binder -> [Local Id] -> T.Expr Id -> T.Expr Id
+trBinder b = case b of
+  A.Lambda -> T.Lam
+  A.Forall -> mkQuant T.Forall
+  A.Exists -> mkQuant T.Exists
+
+trCase :: T.Type Id -> A.Case -> CM (T.Case Id)
+trCase goal_type (A.Case pattern expr) =
+  newScope $ T.Case <$> trPattern goal_type pattern <*> trExpr expr
+
+trPattern :: T.Type Id -> A.Pattern -> CM (T.Pattern Id)
+trPattern goal_type p = case p of
+  A.Default          -> return T.Default
+  A.SimplePat sym    -> trPattern goal_type (A.ConPat sym [])
+  A.ConPat sym bound ->
+    do x <- lkSym sym
+       mt <- gets (fmap globalType . lookupGlobal x)
+       case mt of
+         Just pt@(PolyType tvs arg res)
+           | Just ty_app <- matchTypesIn tvs [(res,goal_type)] ->
+             do let (var_types, _) = applyPolyType pt ty_app
+                ls <- sequence
+                   [ do b <- addSym LocalId b_sym
+                        let l = Local b t
+                        newLocal l
+                        return l
+                   | (b_sym,t) <- bound `zip` var_types
+                   ]
+                return (T.ConPat (Global x pt ty_app) ls)
+         _ -> throwError $ "type-incorrect case"
+
+trType :: A.Type -> CM (T.Type Id)
+trType t0 = case t0 of
+  A.TyVar s -> do x <- lkSym s
+                  mtv <- gets (isTyVar x)
+                  if mtv then return (T.TyVar x)
+                         else trType (A.TyApp s [])
+  A.TyApp s ts -> T.TyCon <$> lkSym s <*> mapM trType ts
+  A.ArrowTy ts -> (:=>:) <$> mapM trType (init ts) <*> trType (last ts)
+  A.IntTy      -> return intType
+  A.BoolTy     -> return boolType
+
diff --git a/src/Tip/Parser/ErrM.hs b/src/Tip/Parser/ErrM.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Parser/ErrM.hs
@@ -0,0 +1,37 @@
+-- BNF Converter: Error Monad
+-- Copyright (C) 2004  Author:  Aarne Ranta
+
+-- This file comes with NO WARRANTY and may be used FOR ANY PURPOSE.
+module Tip.Parser.ErrM where
+
+-- the Error monad: like Maybe type with error msgs
+
+import Control.Monad (MonadPlus(..), liftM)
+import Control.Applicative (Applicative(..), Alternative(..))
+
+data Err a = Ok a | Bad String
+  deriving (Read, Show, Eq, Ord)
+
+instance Monad Err where
+  return      = Ok
+  fail        = Bad
+  Ok a  >>= f = f a
+  Bad s >>= _ = Bad s
+
+instance Applicative Err where
+  pure = Ok
+  (Bad s) <*> _ = Bad s
+  (Ok f) <*> o  = liftM f o
+
+
+instance Functor Err where
+  fmap = liftM
+
+instance MonadPlus Err where
+  mzero = Bad "Err.mzero"
+  mplus (Bad _) y = y
+  mplus x       _ = x
+
+instance Alternative Err where
+  empty = mzero
+  (<|>) = mplus
diff --git a/src/Tip/Parser/LexTIP.x b/src/Tip/Parser/LexTIP.x
new file mode 100644
--- /dev/null
+++ b/src/Tip/Parser/LexTIP.x
@@ -0,0 +1,183 @@
+-- -*- haskell -*-
+-- This Alex file was machine-generated by the BNF converter
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+module Tip.Parser.LexTIP where
+
+
+
+import qualified Data.Bits
+import Data.Word (Word8)
+}
+
+
+$l = [a-zA-Z\192 - \255] # [\215 \247]    -- isolatin1 letter FIXME
+$c = [A-Z\192-\221] # [\215]    -- capital isolatin1 letter FIXME
+$s = [a-z\222-\255] # [\247]    -- small isolatin1 letter FIXME
+$d = [0-9]                -- digit
+$i = [$l $d _ ']          -- identifier character
+$u = [\0-\255]          -- universal: any character
+
+@rsyms =    -- symbols and non-identifier-like reserved words
+   \( | "check" \- "sat" | \) | "declare" \- "datatypes" | "declare" \- "sort" | "declare" \- "fun" | "define" \- "funs" \- "rec" | "assert" \- "not" | \= \> | \@ | \= | \+ | \- | \* | \> | \> \= | \< | \< \=
+
+:-
+";" [.]* ; -- Toss single line comments
+
+$white+ ;
+@rsyms { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
+($l | [\~ \! \@ \$ \% \^ \& \* \_ \- \+ \= \< \> \. \? \/]) ($l | $d | [\~ \! \@ \$ \% \^ \& \* \_ \- \+ \= \< \> \. \? \/]) * { tok (\p s -> PT p (eitherResIdent (T_Symbol . share) s)) }
+
+$l $i*   { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
+
+
+$d+      { tok (\p s -> PT p (TI $ share s))    }
+
+
+{
+
+tok :: (Posn -> String -> Token) -> (Posn -> String -> Token)
+tok f p s = f p s
+
+share :: String -> String
+share = id
+
+data Tok =
+   TS !String !Int    -- reserved words and symbols
+ | TL !String         -- string literals
+ | TI !String         -- integer literals
+ | TV !String         -- identifiers
+ | TD !String         -- double precision float literals
+ | TC !String         -- character literals
+ | T_Symbol !String
+
+ deriving (Eq,Show,Ord)
+
+data Token =
+   PT  Posn Tok
+ | Err Posn
+  deriving (Eq,Show,Ord)
+
+tokenPos :: [Token] -> String
+tokenPos (PT (Pn _ l _) _ :_) = "line " ++ show l
+tokenPos (Err (Pn _ l _) :_) = "line " ++ show l
+tokenPos _ = "end of file"
+
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p) = p
+
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t@(PT p _) = (posLineCol p, prToken t)
+
+prToken :: Token -> String
+prToken t = case t of
+  PT _ (TS s _) -> s
+  PT _ (TL s)   -> s
+  PT _ (TI s)   -> s
+  PT _ (TV s)   -> s
+  PT _ (TD s)   -> s
+  PT _ (TC s)   -> s
+  PT _ (T_Symbol s) -> s
+
+
+data BTree = N | B String Tok BTree BTree deriving (Show)
+
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+  where
+  treeFind N = tv s
+  treeFind (B a t left right) | s < a  = treeFind left
+                              | s > a  = treeFind right
+                              | s == a = t
+
+resWords :: BTree
+resWords = b "check-sat" 20 (b ">" 10 (b "-" 5 (b "*" 3 (b ")" 2 (b "(" 1 N N) N) (b "+" 4 N N)) (b "=" 8 (b "<=" 7 (b "<" 6 N N) N) (b "=>" 9 N N))) (b "and" 15 (b "Bool" 13 (b "@" 12 (b ">=" 11 N N) N) (b "Int" 14 N N)) (b "assert-not" 18 (b "assert" 17 (b "as" 16 N N) N) (b "case" 19 N N)))) (b "forall" 30 (b "define-funs-rec" 25 (b "declare-sort" 23 (b "declare-fun" 22 (b "declare-datatypes" 21 N N) N) (b "default" 24 N N)) (b "exists" 28 (b "div" 27 (b "distinct" 26 N N) N) (b "false" 29 N N))) (b "mod" 35 (b "let" 33 (b "lambda" 32 (b "ite" 31 N N) N) (b "match" 34 N N)) (b "par" 38 (b "or" 37 (b "not" 36 N N) N) (b "true" 39 N N))))
+   where b s n = let bs = id s
+                  in B bs (TS bs n)
+
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id where
+  unesc s = case s of
+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+    '\\':'n':cs  -> '\n' : unesc cs
+    '\\':'t':cs  -> '\t' : unesc cs
+    '"':[]    -> []
+    c:cs      -> c : unesc cs
+    _         -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+      deriving (Eq, Show,Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1
+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn,     -- current position,
+                  Char,     -- previous char
+                  [Byte],   -- pending bytes on the current char
+                  String)   -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+    where
+      go :: AlexInput -> [Token]
+      go inp@(pos, _, _, str) =
+               case alexScan inp 0 of
+                AlexEOF                   -> []
+                AlexError (pos, _, _, _)  -> [Err pos]
+                AlexSkip  inp' len        -> go inp'
+                AlexToken inp' len act    -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+  case  s of
+    []  -> Nothing
+    (c:s) ->
+             let p'     = alexMove p c
+                 (b:bs) = utf8Encode c
+              in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+ where
+  go oc
+   | oc <= 0x7f       = [oc]
+
+   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+
+   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+}
diff --git a/src/Tip/Parser/ParTIP.y b/src/Tip/Parser/ParTIP.y
new file mode 100644
--- /dev/null
+++ b/src/Tip/Parser/ParTIP.y
@@ -0,0 +1,277 @@
+-- This Happy file was machine-generated by the BNF converter
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+module Tip.Parser.ParTIP where
+import Tip.Parser.AbsTIP
+import Tip.Parser.LexTIP
+import Tip.Parser.ErrM
+
+}
+
+%name pStart Start
+%name pListDecl ListDecl
+%name pDecl Decl
+%name pAssertion Assertion
+%name pFunDef FunDef
+%name pInnerFunDef InnerFunDef
+%name pFunDecl FunDecl
+%name pInnerFunDecl InnerFunDecl
+%name pDatatype Datatype
+%name pConstructor Constructor
+%name pBinding Binding
+%name pLetDecl LetDecl
+%name pType Type
+%name pExpr Expr
+%name pBinder Binder
+%name pCase Case
+%name pPattern Pattern
+%name pHead Head
+%name pListLetDecl ListLetDecl
+%name pListCase ListCase
+%name pListExpr ListExpr
+%name pListDatatype ListDatatype
+%name pListConstructor ListConstructor
+%name pListBinding ListBinding
+%name pListSymbol ListSymbol
+%name pListType ListType
+%name pListFunDecl ListFunDecl
+%name pListFunDef ListFunDef
+
+-- no lexer declaration
+%monad { Err } { thenM } { returnM }
+%tokentype { Token }
+
+%token
+  '(' { PT _ (TS _ 1) }
+  ')' { PT _ (TS _ 2) }
+  '*' { PT _ (TS _ 3) }
+  '+' { PT _ (TS _ 4) }
+  '-' { PT _ (TS _ 5) }
+  '<' { PT _ (TS _ 6) }
+  '<=' { PT _ (TS _ 7) }
+  '=' { PT _ (TS _ 8) }
+  '=>' { PT _ (TS _ 9) }
+  '>' { PT _ (TS _ 10) }
+  '>=' { PT _ (TS _ 11) }
+  '@' { PT _ (TS _ 12) }
+  'Bool' { PT _ (TS _ 13) }
+  'Int' { PT _ (TS _ 14) }
+  'and' { PT _ (TS _ 15) }
+  'as' { PT _ (TS _ 16) }
+  'assert' { PT _ (TS _ 17) }
+  'assert-not' { PT _ (TS _ 18) }
+  'case' { PT _ (TS _ 19) }
+  'check-sat' { PT _ (TS _ 20) }
+  'declare-datatypes' { PT _ (TS _ 21) }
+  'declare-fun' { PT _ (TS _ 22) }
+  'declare-sort' { PT _ (TS _ 23) }
+  'default' { PT _ (TS _ 24) }
+  'define-funs-rec' { PT _ (TS _ 25) }
+  'distinct' { PT _ (TS _ 26) }
+  'div' { PT _ (TS _ 27) }
+  'exists' { PT _ (TS _ 28) }
+  'false' { PT _ (TS _ 29) }
+  'forall' { PT _ (TS _ 30) }
+  'ite' { PT _ (TS _ 31) }
+  'lambda' { PT _ (TS _ 32) }
+  'let' { PT _ (TS _ 33) }
+  'match' { PT _ (TS _ 34) }
+  'mod' { PT _ (TS _ 35) }
+  'not' { PT _ (TS _ 36) }
+  'or' { PT _ (TS _ 37) }
+  'par' { PT _ (TS _ 38) }
+  'true' { PT _ (TS _ 39) }
+
+L_integ  { PT _ (TI $$) }
+L_Symbol { PT _ (T_Symbol _) }
+
+
+%%
+
+Integer :: { Integer } : L_integ  { (read ( $1)) :: Integer }
+Symbol    :: { Symbol} : L_Symbol { Symbol (mkPosToken $1)}
+
+Start :: { Start }
+Start : ListDecl { Start $1 } 
+
+
+ListDecl :: { [Decl] }
+ListDecl : '(' 'check-sat' ')' { [] } 
+  | '(' Decl ')' ListDecl { (:) $2 $4 }
+
+
+Decl :: { Decl }
+Decl : 'declare-datatypes' '(' ListSymbol ')' '(' ListDatatype ')' { DeclareDatatypes (reverse $3) (reverse $6) } 
+  | 'declare-sort' Symbol Integer { DeclareSort $2 $3 }
+  | 'declare-fun' FunDecl { DeclareFun $2 }
+  | 'define-funs-rec' '(' ListFunDef ')' '(' ListExpr ')' { DefineFunsRec (reverse $3) (reverse $6) }
+  | Assertion Expr { MonoAssert $1 $2 }
+  | Assertion '(' 'par' '(' ListSymbol ')' Expr ')' { ParAssert $1 (reverse $5) $7 }
+
+
+Assertion :: { Assertion }
+Assertion : 'assert' { AssertIt } 
+  | 'assert-not' { AssertNot }
+
+
+FunDef :: { FunDef }
+FunDef : '(' 'par' '(' ListSymbol ')' InnerFunDef ')' { ParFunDef (reverse $4) $6 } 
+  | InnerFunDef { MonoFunDef $1 }
+
+
+InnerFunDef :: { InnerFunDef }
+InnerFunDef : '(' Symbol '(' ListBinding ')' Type ')' { InnerFunDef $2 (reverse $4) $6 } 
+
+
+FunDecl :: { FunDecl }
+FunDecl : '(' 'par' '(' ListSymbol ')' '(' InnerFunDecl ')' ')' { ParFunDecl (reverse $4) $7 } 
+  | InnerFunDecl { MonoFunDecl $1 }
+
+
+InnerFunDecl :: { InnerFunDecl }
+InnerFunDecl : Symbol '(' ListType ')' Type { InnerFunDecl $1 (reverse $3) $5 } 
+
+
+Datatype :: { Datatype }
+Datatype : '(' Symbol ListConstructor ')' { Datatype $2 (reverse $3) } 
+
+
+Constructor :: { Constructor }
+Constructor : '(' Symbol ListBinding ')' { Constructor $2 (reverse $3) } 
+
+
+Binding :: { Binding }
+Binding : '(' Symbol Type ')' { Binding $2 $3 } 
+
+
+LetDecl :: { LetDecl }
+LetDecl : '(' Binding Expr ')' { LetDecl $2 $3 } 
+
+
+Type :: { Type }
+Type : Symbol { TyVar $1 } 
+  | '(' Symbol ListType ')' { TyApp $2 (reverse $3) }
+  | '(' '=>' ListType ')' { ArrowTy (reverse $3) }
+  | 'Int' { IntTy }
+  | 'Bool' { BoolTy }
+
+
+Expr :: { Expr }
+Expr : Symbol { Var $1 } 
+  | '(' 'as' Expr Type ')' { As $3 $4 }
+  | '(' Head ListExpr ')' { App $2 (reverse $3) }
+  | '(' 'match' Expr ListCase ')' { Match $3 (reverse $4) }
+  | '(' 'let' '(' ListLetDecl ')' Expr ')' { Let (reverse $4) $6 }
+  | '(' Binder '(' ListBinding ')' Expr ')' { Binder $2 (reverse $4) $6 }
+  | Integer { LitInt $1 }
+  | 'true' { LitTrue }
+  | 'false' { LitFalse }
+
+
+Binder :: { Binder }
+Binder : 'lambda' { Lambda } 
+  | 'forall' { Forall }
+  | 'exists' { Exists }
+
+
+Case :: { Case }
+Case : '(' 'case' Pattern Expr ')' { Case $3 $4 } 
+
+
+Pattern :: { Pattern }
+Pattern : 'default' { Default } 
+  | '(' Symbol ListSymbol ')' { ConPat $2 (reverse $3) }
+  | Symbol { SimplePat $1 }
+
+
+Head :: { Head }
+Head : Symbol { Const $1 } 
+  | '@' { At }
+  | 'ite' { IfThenElse }
+  | 'and' { And }
+  | 'or' { Or }
+  | 'not' { Not }
+  | '=>' { Implies }
+  | '=' { Equal }
+  | 'distinct' { Distinct }
+  | '+' { IntAdd }
+  | '-' { IntSub }
+  | '*' { IntMul }
+  | 'div' { IntDiv }
+  | 'mod' { IntMod }
+  | '>' { IntGt }
+  | '>=' { IntGe }
+  | '<' { IntLt }
+  | '<=' { IntLe }
+
+
+ListLetDecl :: { [LetDecl] }
+ListLetDecl : {- empty -} { [] } 
+  | ListLetDecl LetDecl { flip (:) $1 $2 }
+
+
+ListCase :: { [Case] }
+ListCase : {- empty -} { [] } 
+  | ListCase Case { flip (:) $1 $2 }
+
+
+ListExpr :: { [Expr] }
+ListExpr : {- empty -} { [] } 
+  | ListExpr Expr { flip (:) $1 $2 }
+
+
+ListDatatype :: { [Datatype] }
+ListDatatype : {- empty -} { [] } 
+  | ListDatatype Datatype { flip (:) $1 $2 }
+
+
+ListConstructor :: { [Constructor] }
+ListConstructor : {- empty -} { [] } 
+  | ListConstructor Constructor { flip (:) $1 $2 }
+
+
+ListBinding :: { [Binding] }
+ListBinding : {- empty -} { [] } 
+  | ListBinding Binding { flip (:) $1 $2 }
+
+
+ListSymbol :: { [Symbol] }
+ListSymbol : {- empty -} { [] } 
+  | ListSymbol Symbol { flip (:) $1 $2 }
+
+
+ListType :: { [Type] }
+ListType : {- empty -} { [] } 
+  | ListType Type { flip (:) $1 $2 }
+
+
+ListFunDecl :: { [FunDecl] }
+ListFunDecl : {- empty -} { [] } 
+  | ListFunDecl FunDecl { flip (:) $1 $2 }
+
+
+ListFunDef :: { [FunDef] }
+ListFunDef : {- empty -} { [] } 
+  | ListFunDef FunDef { flip (:) $1 $2 }
+
+
+
+{
+
+returnM :: a -> Err a
+returnM = return
+
+thenM :: Err a -> (a -> Err b) -> Err b
+thenM = (>>=)
+
+happyError :: [Token] -> Err a
+happyError ts =
+  Bad $ "syntax error at " ++ tokenPos ts ++ 
+  case ts of
+    [] -> []
+    [Err _] -> " due to lexer error"
+    _ -> " before " ++ unwords (map (id . prToken) (take 4 ts))
+
+myLexer = tokens
+}
+
diff --git a/src/Tip/Pass/AddMatch.hs b/src/Tip/Pass/AddMatch.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/AddMatch.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE PatternGuards, RecordWildCards #-}
+module Tip.Pass.AddMatch where
+
+import Tip.Core
+import Tip.Fresh
+import Tip.Scope
+import qualified Data.Map as Map
+import Data.Map(Map)
+
+-- | Replace SMTLIB-style selector and discriminator functions
+--   (@is-nil@, @head@, @tail@) with case expressions.
+addMatch :: Name a => Theory a -> Fresh (Theory a)
+addMatch thy =
+  flip transformExprInM thy $ \e ->
+    case e of
+      Gbl Global{..} :@: [t] | Just (d, c) <- lookupDiscriminator gbl_name scp -> do
+        let con = constructor d c gbl_args
+        args <- freshArgs con
+        return $
+          Match t [
+            Case Default (bool False),
+            Case (ConPat con args) (bool True) ]
+      Gbl Global{..} :@: [t] | Just (d, c, i, _) <- lookupProjector gbl_name scp -> do
+        let con = constructor d c gbl_args
+        args <- freshArgs con
+        return $
+          Match t [
+            Case (ConPat con args) (Lcl (args !! i)) ]
+      _ -> return e
+  where
+    scp = scope thy
diff --git a/src/Tip/Pass/AxiomatizeFuncdefs.hs b/src/Tip/Pass/AxiomatizeFuncdefs.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/AxiomatizeFuncdefs.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Tip.Pass.AxiomatizeFuncdefs where
+
+#include "errors.h"
+import Tip.Core
+import Tip.Fresh
+
+import Data.Generics.Geniplate
+import Control.Applicative
+
+--conProjs :: Project a => Global a -> [Global a]
+conProjs = undefined
+{- (Global k (PolyType tvs arg_tys res_ty) ts _)
+  = [ Global (project k i) (PolyType tvs [res_ty] arg_ty) ts ProjectNS
+    | (i,arg_ty) <- zip [0..] arg_tys
+    ]
+    -}
+
+axiomatizeFuncdefs :: Theory a -> Theory a
+axiomatizeFuncdefs thy@Theory{..} =
+  thy{
+    thy_funcs   = [],
+    thy_sigs    = thy_sigs ++ abs,
+    thy_asserts = fms ++ thy_asserts
+  }
+ where
+  (abs,fms) = unzip (map axiomatize thy_funcs)
+
+-- Passes needed afterwards:
+--
+-- 1)  x = e ==> F[x] ~~> F[e]
+--
+-- 2)
+--     all x (D => (all y . E) /\ (all z . F))
+-- ~~>
+--     all x ((D => all y . E) /\ (D => all z . F))
+-- ~~>
+--     (all x y (D => E)) /\ (all x z (D => F))
+--
+-- (TODO)
+
+axiomatize :: forall a . Function a -> (Signature a, Formula a)
+axiomatize fn@Function{..} =
+  ( Signature func_name (funcType fn)
+  , Formula Assert func_tvs (ax func_body)
+  )
+ where
+  lhs = applyFunction fn (map TyVar func_tvs) (map Lcl func_args)
+
+  ax :: Expr a -> Expr a
+  ax e0 = case e0 of
+    Match s (Case Default def_rhs:alts) -> invert_alts s alts def_rhs /\ ax_alts s alts
+    Match s alts -> ax_alts s alts
+    Let{}        -> __ -- could use ==> while Let is neither recursive nor polymorphic
+    Lam{}        -> __
+    Quant{}      -> __
+    _            -> lhs === e0 -- e0 should now only be (:@:) and Lcl
+   where
+    invert_alts :: Expr a -> [Case a] -> Expr a -> Expr a
+    invert_alts _ []                def_rhs = def_rhs
+    invert_alts s (Case pat _:alts) def_rhs = s === invert_pat s pat \/
+                                              invert_alts s alts def_rhs
+     where
+      invert_pat :: Expr a -> Pattern a -> Expr a
+      invert_pat _ Default      = __
+      invert_pat _ (LitPat lit) = literal lit
+      invert_pat s (ConPat k _) = Gbl k :@: [ Gbl p :@: [s] | p <- conProjs k ]
+
+    ax_alts :: Expr a -> [Case a] -> Expr a
+    ax_alts s alts = ands [ ax_pat s pat rhs | Case pat rhs <- alts ]
+     where
+      ax_pat :: Expr a -> Pattern a -> Expr a -> Expr a
+      ax_pat _ Default       _   = __
+      ax_pat s (LitPat lit)  rhs = s === literal lit ==> ax rhs
+      ax_pat s (ConPat k bs) rhs = mkQuant Forall bs
+                                     (s === Gbl k :@: map Lcl bs ==> ax rhs)
+
diff --git a/src/Tip/Pass/Booleans.hs b/src/Tip/Pass/Booleans.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/Booleans.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE FlexibleContexts, ViewPatterns, RecordWildCards #-}
+module Tip.Pass.Booleans where
+
+import Tip.Core
+
+import Data.Generics.Geniplate
+
+-- | Transforms boolean operators to if, but not in expression contexts.
+theoryBoolOpToIf :: Ord a => Theory a -> Theory a
+theoryBoolOpToIf Theory{..} =
+  Theory{
+    thy_funcs   = map boolOpToIf thy_funcs,
+    thy_asserts =
+      let k fm@Formula{..} = fm { fm_body = formulaBoolOpToIf fm_body }
+      in  map k thy_asserts,
+    ..
+  }
+
+formulaBoolOpToIf :: Ord a => Expr a -> Expr a
+formulaBoolOpToIf e0 =
+  case e0 of
+    Builtin op :@: args@(a:_)
+      | op `elem` [And,Or,Not,Implies] ||
+        op `elem` [Equal,Distinct] && hasBoolType a ->
+        Builtin op :@: map formulaBoolOpToIf args
+    Quant qi q as e -> Quant qi q as (formulaBoolOpToIf e)
+    _ -> boolOpToIf e0
+
+hasBoolType :: Ord a => Expr a -> Bool
+hasBoolType e = exprType e == boolType
+
+-- | Transforms @and@, @or@, @=>@, @not@ and @=@ and @distict@ on @Bool@
+--   into @ite@ (i.e. @match@)
+boolOpToIf :: (Ord a,TransformBi (Expr a) (f a)) => f a -> f a
+boolOpToIf = transformExprIn $
+  \ e0 -> case e0 of
+    Builtin And :@: [a,b]     -> makeIf a b falseExpr
+    Builtin Or  :@: [a,b]     -> makeIf a trueExpr b
+    Builtin Not :@: [a]       -> makeIf a falseExpr trueExpr
+    Builtin Implies :@: [a,b] -> makeIf a b trueExpr
+    Builtin Equal    :@: [a,b] | hasBoolType a -> makeIf a b (neg_if b)
+    Builtin Distinct :@: [a,b] | hasBoolType a -> makeIf a (neg_if b) b
+    _ -> e0
+  where
+    neg_if a = makeIf a falseExpr trueExpr
+
+-- | Transforms @ite@ (@match@) on boolean literals in the branches
+--   into the corresponding builtin boolean function.
+ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a
+ifToBoolOp = transformExprIn $
+  \ e0 -> case ifView e0 of
+    Just (b,t,f)
+      | Just True  <- boolView t -> b \/ f
+      | Just False <- boolView t -> neg b /\ f
+      | Just True  <- boolView f -> b ==> t -- neg b \/ t
+      | Just False <- boolView f -> b /\ t
+    _ -> e0
+
diff --git a/src/Tip/Pass/CSEMatch.hs b/src/Tip/Pass/CSEMatch.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/CSEMatch.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE PatternGuards, RecordWildCards #-}
+module Tip.Pass.CSEMatch where
+
+import Tip.Core
+import Tip.Fresh
+
+data CSEMatchOpts =
+  CSEMatchOpts {
+    cse_nullary :: Bool
+    -- ^ Also do CSE for nullary constructors
+  }
+
+cseMatchNormal, cseMatchWhy3 :: CSEMatchOpts
+cseMatchNormal = CSEMatchOpts False
+cseMatchWhy3   = CSEMatchOpts True
+
+-- | Look for expressions of the form
+--   @(match x (case P ...P...) ...)@
+-- and replace them with
+--   @(match x (case P ...x...) ...)@.
+-- This helps Why3's termination checker in some cases.
+cseMatch :: Name a => CSEMatchOpts -> Theory a -> Theory a
+cseMatch CSEMatchOpts{..} =
+  transformExprIn $ \e ->
+    case e of
+      Match (Lcl x) pats ->
+        Match (Lcl x) (map (replaceWith x) pats)
+      _ -> e
+  where
+    replaceWith x (Case (ConPat con args) body)
+      | length args > 0 || cse_nullary =
+        Case (ConPat con args) $
+        flip transformExpr body $ \e ->
+          if e == Gbl con :@: map Lcl args
+          then Lcl x
+          else e
+    replaceWith x case_ = case_
diff --git a/src/Tip/Pass/CommuteMatch.hs b/src/Tip/Pass/CommuteMatch.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/CommuteMatch.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Tip.Pass.CommuteMatch where
+
+#include "errors.h"
+import Tip.Core
+import Tip.Fresh
+
+import Data.Generics.Geniplate
+import Control.Applicative
+
+-- | Makes an effort to move match statements upwards: moves match above
+-- function applications, and moves matches inside scrutinees outside.
+--
+-- Does not move past quantifiers, lets, and lambdas.
+commuteMatch :: (Name a, TransformBiM Fresh (Expr a) (f a)) => f a -> Fresh (f a)
+commuteMatch = transformExprInM $ \ e0 ->
+  case e0 of
+    Match (Match e inner_alts) outer_alts ->
+      commuteMatch =<< do
+        Match e <$> sequence
+          [ Case lhs <$> freshen (Match rhs outer_alts)
+          | Case lhs rhs <- inner_alts
+          ]
+
+    hd :@: args
+      | and [ not (logicalBuiltin b) | Builtin b <- [hd] ]
+      , let isMatch Match{} = True
+            isMatch _       = False
+      , (left, Match e alts:right) <- break isMatch args
+      -> commuteMatch =<< do
+           Match e <$> sequence
+             [ Case lhs <$> freshen (hd :@: (left ++ [rhs] ++ right))
+             | Case lhs rhs <- alts
+             ]
+
+    Lam bs e  -> Lam bs <$> commuteMatch e
+
+    Quant qi q bs e -> Quant qi q bs <$> commuteMatch e
+
+    Let x b e -> Let x b <$> commuteMatch e
+
+    _ -> return e0
+
diff --git a/src/Tip/Pass/EliminateDeadCode.hs b/src/Tip/Pass/EliminateDeadCode.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/EliminateDeadCode.hs
@@ -0,0 +1,25 @@
+-- Very bad dead code elimination (doesn't detect dead recursive functions).
+
+{-# LANGUAGE RecordWildCards #-}
+module Tip.Pass.EliminateDeadCode where
+
+import Tip.Core
+import qualified Data.Set as Set
+import Data.Generics.Geniplate
+
+eliminateDeadCode :: Ord a => Theory a -> Theory a
+eliminateDeadCode = fixpoint elim
+  where
+    elim thy@Theory{..} =
+      thy {
+        thy_sigs = filter (flip Set.member alive . sig_name) thy_sigs,
+        thy_funcs = filter (flip Set.member alive . func_name) thy_funcs }
+      where
+        alive = Set.fromList (map gbl_name (universeBi thy))
+
+fixpoint :: Eq a => (a -> a) -> a -> a
+fixpoint f x
+  | x == y = x
+  | otherwise = fixpoint f y
+  where
+    y = f x
diff --git a/src/Tip/Pass/EqualFunctions.hs b/src/Tip/Pass/EqualFunctions.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/EqualFunctions.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PatternGuards #-}
+module Tip.Pass.EqualFunctions(collapseEqual, removeAliases) where
+
+import Tip.Core
+import Tip.Fresh
+
+import Data.Traversable
+import Control.Applicative
+import Data.Either
+import Data.List (delete, inits)
+
+import Data.Map (Map)
+import qualified Data.Map as M
+
+import Control.Monad.State
+
+import Data.Generics.Geniplate
+
+renameVars :: forall f a . (Ord a,Traversable f) => (a -> Bool) -> f a -> f (Either a Int)
+renameVars is_var t = runFresh (evalStateT (traverse rename t) M.empty)
+  where
+    rename :: a -> StateT (Map a Int) Fresh (Either a Int)
+    rename x | is_var x = do my <- gets (M.lookup x)
+                             case my of
+                               Just y  -> do return (Right y)
+                               Nothing -> do y <- lift fresh
+                                             modify (M.insert x y)
+                                             return (Right y)
+    rename x = return (Left x)
+
+renameFn :: Ord a => Function a -> Function (Either a Int)
+renameFn fn = renameVars (`notElem` gbls) fn
+  where
+    gbls = delete (func_name fn) (globals fn)
+
+rename :: Eq a => [(a,a)] -> a -> a
+rename d x = case lookup x d of
+    Just y  -> y
+    Nothing -> x
+
+-- | If we have
+--
+-- > f x = E[x]
+-- > g y = E[y]
+--
+-- then we remove @g@ and replace it with @f@ everywhere
+collapseEqual :: forall a . Ord a => Theory a -> Theory a
+collapseEqual thy@(Theory{ thy_funcs = fns0 })
+    = fmap (rename renamings) thy{ thy_funcs = survivors }
+  where
+    rfs :: [(Function a,Function (Either a Int))]
+    rfs = [ (f,renameFn f) | f <- fns0 ]
+
+    renamings :: [(a,a)]
+    survivors :: [Function a]
+    (renamings,survivors) = partitionEithers
+        [ case [ (func_name f,func_name g) | (g,rg) <- prev , rf == rg ] of
+            []   -> Right f -- f is better
+            fg:_ -> Left fg -- g is better
+        | ((f,rf),prev) <- withPrevious rfs
+        ]
+
+-- | Pair up a list with its previous elements
+--
+-- > withPrevious "abc" = [('a',""),('b',"a"),('c',"ab")]
+withPrevious :: [a] -> [(a,[a])]
+withPrevious xs = zip xs (inits xs)
+
+renameGlobals :: Eq a => [(a,[Type a] -> Head a)] -> Theory a -> Theory a
+renameGlobals rns = transformBi $ \ h0 ->
+  case h0 of
+    Gbl (Global g _ ts) | Just hd <- lookup g rns -> hd ts
+    _ -> h0
+
+-- | If we have
+--
+-- > g x y = f x y
+--
+-- then we remove @g@ and replace it with @f@ everywhere
+removeAliases :: Eq a => Theory a -> Theory a
+removeAliases thy@(Theory{thy_funcs=fns0})
+    | null renamings = thy
+    | otherwise = removeAliases $ renameGlobals renamings thy{ thy_funcs = survivors }
+  where
+    renamings = take 1
+      [ (g,k)
+      | Function g ty_vars vars _res_ty (hd :@: args) <- fns0
+      , map Lcl vars == args
+      , let (ok,k) = case hd of
+              Gbl (Global f pty ty_args) -> (map TyVar ty_vars == ty_args, \ ts -> Gbl (Global f pty ts))
+              Builtin{}                  -> (True, \ _ -> hd)
+      , ok
+      ]
+
+    remove = map fst renamings
+
+    survivors = filter ((`notElem` remove) . func_name) fns0
+
diff --git a/src/Tip/Pass/FillInCases.hs b/src/Tip/Pass/FillInCases.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/FillInCases.hs
@@ -0,0 +1,35 @@
+-- Fill in any missing cases with a default value.
+
+{-# LANGUAGE RecordWildCards #-}
+module Tip.Pass.FillInCases where
+
+import Tip.Core
+import Tip.Scope
+import Tip.Utils
+import Tip.Fresh
+import Tip.Pretty
+import Tip.Pretty.SMT
+import Debug.Trace
+import Text.PrettyPrint
+
+fillInCases :: (Ord a, PrettyVar a) => (Type a -> Expr a) -> Theory a -> Theory a
+fillInCases def thy =
+  flip transformExprIn thy $ \e ->
+    case e of
+      Match val cases
+        | not (exhaustive (exprType val) (map case_pat cases)) ->
+          Match val (Case Default (def (exprType e)):cases)
+      _ -> e
+  where
+    exhaustive _ (Default:_) = True
+    exhaustive (TyCon ty _) pats =
+      case lookupType ty scp of
+        Just (DatatypeInfo Datatype{..}) ->
+          usort (map con_name data_cons) ==
+          usort [ gbl_name pat_con | ConPat{..} <- pats ]
+        _ -> False
+    exhaustive (BuiltinType Boolean) pats =
+      usort pats == usort [LitPat (Bool False), LitPat (Bool True)]
+    exhaustive _ _ = False
+
+    scp = scope thy
diff --git a/src/Tip/Pass/Lift.hs b/src/Tip/Pass/Lift.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/Lift.hs
@@ -0,0 +1,163 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE CPP #-}
+module Tip.Pass.Lift (lambdaLift, letLift, axiomatizeLambdas) where
+
+#include "errors.h"
+import Tip.Core
+import Tip.Fresh
+import Tip.Utils
+
+import Data.Either
+import Data.List
+import Data.Generics.Geniplate
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Writer
+import qualified Data.Map as Map
+
+type LiftM a = WriterT [Function a] Fresh
+
+type TopLift a = Expr a -> LiftM a (Expr a)
+
+liftAnywhere :: (Name a,TransformBiM (LiftM a) (Expr a) (t a)) =>
+                TopLift a -> t a -> Fresh (t a,[Function a])
+liftAnywhere top = runWriterT . transformExprInM top
+
+liftTheory :: Name a => TopLift a -> Theory a -> Fresh (Theory a)
+liftTheory top thy0 =
+  do (Theory{..},new_func_decls) <- liftAnywhere top thy0
+     return Theory{thy_funcs = new_func_decls ++ thy_funcs,..}
+
+lambdaLiftTop :: Name a => TopLift a
+lambdaLiftTop e0 =
+  case e0 of
+    Lam lam_args lam_body ->
+      do g_name <- lift (freshNamed "lam")
+         let g_args = free e0
+         let g_tvs  = freeTyVars e0
+         let g_type = map lcl_type lam_args :=>: exprType lam_body
+         let g = Function g_name g_tvs g_args g_type (Lam lam_args lam_body)
+         tell [g]
+         return (applyFunction g (map TyVar g_tvs) (map Lcl g_args))
+    _ -> return e0
+
+-- | Defunctionalization.
+--
+-- > f x = ... \ y -> e [ x ] ...
+--
+-- becomes
+--
+-- > f x = ... g x ...
+-- > g x = \ y -> e [ x ]
+--
+-- where @g@ is a fresh function.
+--
+-- After this pass, lambdas only exist at the top level of functions.
+lambdaLift :: Name a => Theory a -> Fresh (Theory a)
+lambdaLift = liftTheory lambdaLiftTop
+
+letLiftTop :: Name a => TopLift a
+letLiftTop e0 =
+  case e0 of
+    Let xl@(Local x xt) b e ->
+      do let fvs = free b
+         let tvs = freeTyVars b
+         let xfn = Function x tvs fvs (exprType b) b
+         tell [xfn]
+         lift ((applyFunction xfn (map TyVar tvs) (map Lcl fvs) // xl) e)
+    _ -> return e0
+
+-- | Lift lets to the top level.
+--
+-- > let x = b[fvs] in e[x]
+--
+-- becomes
+--
+-- > e[f fvs]
+-- > f fvs = b[fvs]
+letLift :: Name a => Theory a -> Fresh (Theory a)
+letLift = liftTheory letLiftTop
+
+axLamFunc :: Function a -> Maybe (Signature a,Formula a)
+axLamFunc Function{..} =
+  case func_body of
+    Lam lam_args e ->
+      let abs = Signature func_name (PolyType func_tvs (map lcl_type func_args) func_res)
+          fm  = Formula Assert func_tvs
+                  (mkQuant
+                    Forall
+                    (func_args ++ lam_args)
+                    (apply
+                      (applySignature abs (map TyVar func_tvs) (map Lcl func_args))
+                      (map Lcl lam_args)
+                     === e))
+      in  Just (abs,fm)
+    _ -> Nothing
+
+-- | Axiomatize lambdas.
+--
+-- > f x = \ y -> E[x,y]
+--
+-- becomes
+--
+-- > declare-fun f ...
+-- > assert (forall x y . @ (f x) y = E[x,y])
+axiomatizeLambdas :: forall a. Name a => Theory a -> Fresh (Theory a)
+axiomatizeLambdas thy0 = do
+  arrows <- fmap Map.fromList (mapM makeArrow arities)
+  ats    <- fmap Map.fromList (mapM (makeAt arrows) arities)
+  return $
+    transformBi (eliminateArrows arrows) $
+    transformBi (eliminateAts ats)
+    thy {
+      thy_sigs = Map.elems ats    ++ thy_sigs thy,
+      thy_sorts = Map.elems arrows ++ thy_sorts thy
+    }
+  where
+    thy =
+      thy0 {
+        thy_sigs = new_abs ++ thy_sigs thy0,
+        thy_funcs = survivors,
+        thy_asserts = new_form ++ thy_asserts thy0
+      }
+    (survivors,new) =
+      partitionEithers
+        [ maybe (Left fn) Right (axLamFunc fn)
+        | fn <- thy_funcs thy0
+        ]
+
+    (new_abs,new_form) = unzip new
+
+    arities = usort [ length args | args :=>: _ <- universeBi thy :: [Type a] ]
+    makeArrow n = do
+      ty <- freshNamed ("fun" ++ show n)
+      return (n, Sort ty (n+1))
+    makeAt arrows n = do
+      name <- freshNamed ("apply" ++ show n)
+      tvs <- mapM (freshNamed . mkTyVarName) [0..(n-1)]
+      tv  <- freshNamed (mkTyVarName n)
+      let Sort{..} = Map.findWithDefault __ n arrows
+          ty          = TyCon sort_name (map TyVar (tvs ++ [tv]))
+      return $
+        (n, Signature name (PolyType (tvs ++ [tv]) (ty:map TyVar tvs) (TyVar tv)))
+
+    eliminateArrows arrows (args :=>: res) =
+      TyCon sort_name (map (eliminateArrows arrows) (args ++ [res]))
+      where
+        Sort{..} = Map.findWithDefault __ (length args) arrows
+    eliminateArrows _ ty = ty
+
+    eliminateAts ats (Builtin At :@: (e:es)) =
+      Gbl (Global sig_name sig_type (args ++ [res])) :@:
+      map (eliminateAts ats) (e:es)
+      where
+        args :=>: res = exprType e
+        Signature{..} = Map.findWithDefault __ (length args) ats
+    eliminateAts _ e = e
+
+mkTyVarName :: Int -> String
+mkTyVarName x = vars !! x
+  where vars = ["a","b","c","d"] ++ ["t" ++ show i | i <- [0..]]
+
diff --git a/src/Tip/Pass/NegateConjecture.hs b/src/Tip/Pass/NegateConjecture.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/NegateConjecture.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE PatternGuards #-}
+module Tip.Pass.NegateConjecture where
+
+import Tip.Core
+import Tip.Fresh
+import Control.Monad
+import Data.Generics.Geniplate
+
+-- | Negates the conjecture: changes assert-not into assert, and
+--   introduce skolem types in case the goal is polymorphic.
+negateConjecture :: Name a => Theory a -> Fresh (Theory a)
+negateConjecture thy =
+  foldM negateConjecture1
+    thy { thy_asserts = filter (not . isProve) (thy_asserts thy) }
+    (filter isProve (thy_asserts thy))
+  where
+    isProve (Formula Prove _ form) = True
+    isProve _ = False
+
+    negateConjecture1 thy (Formula Prove tvs form) = do
+      tvs' <- mapM (refreshNamed "sk_") tvs
+      return thy {
+        thy_asserts = Formula Assert [] (neg (makeTyCons (zip tvs tvs') form)):thy_asserts thy,
+        thy_sorts = [ Sort tv 0 | tv <- tvs' ] ++ thy_sorts thy }
+
+    makeTyCons tvs =
+      transformTypeInExpr $ \ty ->
+        case ty of
+          TyVar tv | Just tv' <- lookup tv tvs -> TyCon tv' []
+          _ -> ty
diff --git a/src/Tip/Pass/Pipeline.hs b/src/Tip/Pass/Pipeline.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/Pipeline.hs
@@ -0,0 +1,51 @@
+module Tip.Pass.Pipeline where
+
+import Tip.Lint
+import Tip.Types (Theory)
+
+import Tip.Utils
+
+import Tip.Fresh
+
+
+import Data.List (intercalate)
+import Data.Either (partitionEithers)
+import Control.Monad ((>=>))
+import Options.Applicative
+
+class Pass p where
+  runPass   :: Name a => p -> Theory a -> Fresh (Theory a)
+  passName  :: p -> String
+  parsePass :: Parser p
+
+unitPass :: Pass p => p -> Mod FlagFields () -> Parser p
+unitPass p mod = flag' () (long (flagify (passName p)) <> mod) *> pure p
+
+runPassLinted :: (Pass p, Name a) => p -> Theory a -> Fresh (Theory a)
+runPassLinted p = runPass p >=> lintM (passName p)
+
+-- | A sum type that supports 'Enum' and 'Bounded'
+data Choice a b = First a | Second b
+  deriving (Eq,Ord,Show)
+
+-- | 'either' for 'Choice'
+choice :: (a -> c) -> (b -> c) -> Choice a b -> c
+choice f _ (First x)  = f x
+choice _ g (Second y) = g y
+
+instance (Pass a, Pass b) => Pass (Choice a b) where
+  passName  = choice passName passName
+  runPass   = choice runPass runPass
+  parsePass = (First <$> parsePass) <|> (Second <$> parsePass)
+
+runPasses :: (Pass p,Name a) => [p] -> Theory a -> Fresh (Theory a)
+runPasses = go []
+ where
+  go _    [] = return
+  go past (p:ps) =
+        runPass p
+    >=> lintM (passName p ++ "(and " ++ intercalate "," past ++ ")")
+    >=> go (passName p:past) ps
+
+parsePasses :: Pass p => Parser [p]
+parsePasses = many parsePass
diff --git a/src/Tip/Pass/RemoveMatch.hs b/src/Tip/Pass/RemoveMatch.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/RemoveMatch.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE RecordWildCards, CPP #-}
+module Tip.Pass.RemoveMatch where
+
+#include "errors.h"
+import Tip.Core
+import Tip.Fresh
+import Tip.Scope
+import qualified Data.Map as Map
+import Data.Generics.Geniplate
+
+-- | Turn case expressions into @is-Cons@, @head@, @tail@ etc.
+removeMatch :: Name a => Theory a -> Fresh (Theory a)
+removeMatch thy@Theory{..} = transformBiM go thy
+  where
+    scp = scope thy
+    go = transformBiM $ \e0 ->
+      case e0 of
+        Match e cs | all acceptable (map case_pat cs) ->
+          letExpr e $ \x ->
+            match x (reverse cs) >>= go
+        _ -> return e0
+
+    acceptable Default = True
+    acceptable ConPat{} = True
+    acceptable _ = False
+
+    match x [Case (ConPat c xs) body] = caseBody x (gbl_name c) xs body
+    match x [Case Default body] = return body
+    match x (Case (ConPat c xs) body:cs) = do
+      clause <- caseBody x (gbl_name c) xs body
+      rest <- match x cs
+      return $
+        Match (matches x (gbl_name c))
+          [Case Default rest,
+           Case (LitPat (Bool True)) clause]
+
+    matches x c =
+      Gbl (uncurry discriminator (whichConstructor c scp) args) :@: [Lcl x]
+      where
+        TyCon _ args = lcl_type x
+
+    caseBody x c lcls body = substMany sub body
+      where
+        sub = [(lcl, Gbl (uncurry projector (whichConstructor c scp) i args) :@: [Lcl x]) | (i, lcl) <- zip [0..] lcls]
+        TyCon _ args = lcl_type x
diff --git a/src/Tip/Pass/RemoveNewtype.hs b/src/Tip/Pass/RemoveNewtype.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/RemoveNewtype.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE RecordWildCards, PatternGuards, CPP #-}
+module Tip.Pass.RemoveNewtype where
+
+#include "errors.h"
+import Tip.Core
+import Tip.Fresh
+import Tip.Scope
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Data.Generics.Geniplate
+import Data.Maybe
+
+-- | Remove datatypes that have only one constructor with one field.
+--   Can only be run after the @addMatch@ pass.
+removeNewtype :: Name a => Theory a -> Theory a
+removeNewtype thy@Theory{..} =
+  -- Replace e.g.:
+  -- I# x -> x
+  -- (case x of _ -> e) -> e
+  -- (case x of (I# y) -> e) -> let y = x in e
+  -- Int -> Int#
+  transformBi replaceTypes (replaceCons thy')
+  where
+    replaceTypes (TyCon ty []) =
+      case lookupNewtype ty of
+        Just ty' -> ty'
+        Nothing -> TyCon ty []
+    replaceTypes (args :=>: res) =
+      map replaceTypes args :=>: replaceTypes res
+    replaceTypes ty = ty
+
+    replaceCons =
+      transformBi $ \e0 ->
+        case e0 of
+          Match e cs | TyCon ty [] <- exprType e, isJust (lookupNewtype ty) ->
+            case cs of
+              Case Default body:_ -> body
+              Case (ConPat _ [x]) body:_ -> Let x e body
+              _ -> ERROR("type-incorrect pattern?")
+          Gbl con :@: [e]
+            | Just (dt, _) <- lookupConstructor (gbl_name con) scp
+            , isJust (lookupNewtype (data_name dt)) ->
+            e
+          _ -> e0
+
+    thy' =
+      thy {
+        thy_datatypes = [ d | d <- thy_datatypes, isNothing (lookupNewtype (data_name d)) ]}
+    lookupNewtype ty = do
+      Datatype{data_cons = [Constructor{con_args = [(_, ty')]}]} <- lookupDatatype ty scp
+      return ty'
+    scp = scope thy
diff --git a/src/Tip/Pass/Uncurry.hs b/src/Tip/Pass/Uncurry.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pass/Uncurry.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE RecordWildCards #-}
+module Tip.Pass.Uncurry(uncurryTheory) where
+
+import Tip.Core
+import Tip.Fresh
+import Tip.WorkerWrapper
+
+-- | Replace "fat arrow", @=>@, functions with normal functions wherever possible.
+uncurryTheory :: Name a => Theory a -> Fresh (Theory a)
+uncurryTheory thy =
+  workerWrapperFunctions outerUncurryWW thy >>=
+  workerWrapperFunctions innerUncurryWW
+
+-- Transform A -> B => C into A B -> C.
+outerUncurryWW :: Name a => Function a -> Maybe (Fresh (WorkerWrapper a))
+outerUncurryWW func@Function{func_res = args :=>: res, ..} = Just $ do
+  lcls <- mapM freshLocal args
+  return WorkerWrapper {
+    ww_func = func,
+    ww_args = func_args ++ lcls,
+    ww_res  = res,
+    ww_def  = \e -> apply e (map Lcl lcls),
+    ww_use  =
+      \hd@(Gbl Global{..}) orig_args -> do
+        new_args <- mapM (freshLocal . applyType func_tvs gbl_args) args
+        return (Lam new_args (hd :@: (orig_args ++ map Lcl new_args)))
+  }
+outerUncurryWW _ = Nothing
+
+-- Transform A => B => C into A B => C.
+innerUncurryWW :: Name a => Function a -> Maybe (Fresh (WorkerWrapper a))
+innerUncurryWW _func = Nothing
diff --git a/src/Tip/Passes.hs b/src/Tip/Passes.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Passes.hs
@@ -0,0 +1,142 @@
+-- | Passes
+module Tip.Passes
+  (
+  -- * Running passes in the Fresh monad
+    freshPass
+
+  -- * Simplifications
+  , simplifyTheory, gently, aggressively, SimplifyOpts(..)
+  , removeNewtype
+  , uncurryTheory
+  , negateConjecture
+
+  -- * Boolean builtins
+  , ifToBoolOp
+  , boolOpToIf
+  , theoryBoolOpToIf
+
+  -- * Match expressions
+  , addMatch
+  , commuteMatch
+  , removeMatch
+  , cseMatch
+  , cseMatchNormal
+  , cseMatchWhy3
+  , fillInCases
+
+  -- * Duplicated functions
+  , collapseEqual
+  , removeAliases
+
+  -- * Lambda and let lifting
+  , lambdaLift
+  , letLift
+  , axiomatizeLambdas
+
+  -- * Building pass pipelines
+  , StandardPass(..)
+  , module Tip.Pass.Pipeline
+  ) where
+
+import Tip.Simplify
+
+import Tip.Pass.AddMatch
+import Tip.Pass.CommuteMatch
+import Tip.Pass.RemoveMatch
+import Tip.Pass.CSEMatch
+import Tip.Pass.Uncurry
+import Tip.Pass.RemoveNewtype
+import Tip.Pass.NegateConjecture
+import Tip.Pass.EqualFunctions
+import Tip.Pass.Lift
+import Tip.Pass.Booleans
+import Tip.Pass.EliminateDeadCode
+import Tip.Pass.FillInCases
+
+import Tip.Fresh
+
+import Tip.Pass.Pipeline
+
+import Options.Applicative
+
+-- | The passes in the standard Tip distribution
+data StandardPass
+  = SimplifyGently
+  | SimplifyAggressively
+  | RemoveNewtype
+  | UncurryTheory
+  | NegateConjecture
+  | IfToBoolOp
+  | BoolOpToIf
+  | AddMatch
+  | CommuteMatch
+  | RemoveMatch
+  | CollapseEqual
+  | RemoveAliases
+  | LambdaLift
+  | LetLift
+  | AxiomatizeLambdas
+  | CSEMatch
+  | CSEMatchWhy3
+  | EliminateDeadCode
+ deriving (Eq,Ord,Show,Read,Enum,Bounded)
+
+instance Pass StandardPass where
+  passName = show
+  runPass p = case p of
+    SimplifyGently       -> simplifyTheory gently
+    SimplifyAggressively -> simplifyTheory aggressively
+    RemoveNewtype        -> return . removeNewtype
+    UncurryTheory        -> uncurryTheory
+    NegateConjecture     -> negateConjecture
+    IfToBoolOp           -> return . ifToBoolOp
+    BoolOpToIf           -> return . theoryBoolOpToIf
+    AddMatch             -> addMatch
+    CommuteMatch         -> commuteMatch
+    RemoveMatch          -> removeMatch
+    CollapseEqual        -> return . collapseEqual
+    RemoveAliases        -> return . removeAliases
+    LambdaLift           -> lambdaLift
+    LetLift              -> letLift
+    AxiomatizeLambdas    -> axiomatizeLambdas
+    CSEMatch             -> return . cseMatch cseMatchNormal
+    CSEMatchWhy3         -> return . cseMatch cseMatchWhy3
+    EliminateDeadCode    -> return . eliminateDeadCode
+  parsePass =
+    foldr (<|>) empty [
+      unitPass SimplifyGently $
+        help "Simplify the problem, trying not to increase its size",
+      unitPass SimplifyAggressively $
+        help "Simplify the problem even at the cost of making it bigger",
+      unitPass RemoveNewtype $
+        help "Eliminate single-constructor, single-argument datatypes",
+      unitPass UncurryTheory $
+        help "Eliminate unnecessary use of higher-order functions",
+      unitPass NegateConjecture $
+        help "Transform the goal into a negated conjecture",
+      unitPass IfToBoolOp $
+        help "Replace if-then-else by and/or where appropriate",
+      unitPass BoolOpToIf $
+        help "Replace and/or by if-then-else",
+      unitPass AddMatch $
+        help "Transform SMTLIB-style datatype access into pattern matching",
+      unitPass CommuteMatch $
+        help "Eliminate matches that occur in weird positions (e.g. as arguments to function calls)",
+      unitPass RemoveMatch $
+        help "Replace pattern matching with SMTLIB-style datatype access",
+      unitPass CollapseEqual $
+        help "Merge functions with equal definitions",
+      unitPass RemoveAliases $
+        help "Eliminate any function defined simply as f(x) = g(x)",
+      unitPass LambdaLift $
+        help "Lift lambdas to the top level",
+      unitPass LetLift $
+        help "Lift let-expressions to the top level.",
+      unitPass AxiomatizeLambdas $
+        help "Eliminate lambdas by axiomatisation (requires --lambda-lift)",
+      unitPass CSEMatch $
+        help "Perform CSE on match scrutinees",
+      unitPass CSEMatchWhy3 $
+        help "Aggressively perform CSE on match scrutinees (helps Why3's termination checker)",
+      unitPass EliminateDeadCode $
+        help "Dead code elimination (doesn't work on dead recursive functions)"]
diff --git a/src/Tip/Pretty.hs b/src/Tip/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pretty.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE RecordWildCards, OverloadedStrings #-}
+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
+module Tip.Pretty where
+
+import Text.PrettyPrint
+
+import Tip.Types
+
+infixl 1 $\
+
+-- | Typeclass for pretty things
+class Pretty a where
+  pp :: a -> Doc
+
+-- | Pretty to string
+ppRender :: Pretty a => a -> String
+ppRender = render . pp
+
+-- | Print something pretty
+pprint :: Pretty a => a -> IO ()
+pprint = putStrLn . ppRender
+
+instance PrettyVar String where
+  varStr = id
+
+instance PrettyVar Int where
+  varStr = show
+
+-- | Typeclass for variables
+class PrettyVar a where
+  -- | The string in a variable
+  varStr :: a -> String
+
+-- | Variable to 'Doc'
+ppVar :: PrettyVar a => a -> Doc
+ppVar = text . varStr
+
+-- * Utilities on Docs
+
+-- | Infix 'hang'
+($\) :: Doc -> Doc -> Doc
+d1 $\ d2 = hang d1 2 d2
+
+
+-- | Conditional parentheses
+parIf :: Bool -> Doc -> Doc
+parIf True  = parens
+parIf False = id
+
diff --git a/src/Tip/Pretty/Haskell.hs b/src/Tip/Pretty/Haskell.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pretty/Haskell.hs
@@ -0,0 +1,165 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Tip.Pretty.Haskell (module Tip.Pretty.Haskell, RenameMap) where
+
+import Tip.Haskell.Repr
+import Tip.Haskell.Translate
+import Tip.Haskell.Rename
+import qualified Tip.Core as T
+import Tip.Pretty
+import Tip.Fresh
+import Text.PrettyPrint
+
+import Data.Map (Map)
+
+ppTheory :: Name a => T.Theory a -> Doc
+ppTheory = fst . ppTheoryWithRenamings
+
+ppTheoryWithRenamings :: Name a => T.Theory a -> (Doc,RenameMap a)
+ppTheoryWithRenamings = fst_pp . renameDecls . addHeader . addImports . trTheory
+  where fst_pp (x,y) = (pp x,y)
+
+-- * Pretty printing
+
+-- | In instance declarations, you cannot write qualified variables,
+--   but need to write them unqualified. As an example, the mempty part
+--   here is incorrect:
+--
+-- @
+-- instance Data.Monoid.Monoid T where
+--   Data.Monoid.mempty = K
+-- @
+--
+-- Thus, instance function declarations will be pretty printed with ppUnqual.
+class PrettyVar a => PrettyHsVar a where
+  varUnqual :: a -> String
+
+ppUnqual :: PrettyHsVar a => a -> Doc
+ppUnqual = text . varUnqual
+
+ppHsVar :: PrettyHsVar a => a -> Doc
+ppHsVar x = parIf (isOp x) (ppVar x)
+
+ppOperQ :: PrettyHsVar a => Bool -> a -> [Doc] -> Doc
+ppOperQ qual x ds =
+  case ds of
+    d1:d2:ds | isOp x -> parIf (not (null ds)) (d1 <+> pp_x $\ d2) $\ fsep ds
+    _ -> parIf (isOp x) (pp_x $\ fsep ds)
+  where
+  pp_x | qual = ppVar x
+       | otherwise = ppUnqual x
+
+ppOper :: PrettyHsVar a => a -> [Doc] -> Doc
+ppOper = ppOperQ True
+
+isOp :: PrettyHsVar a => a -> Bool
+isOp = isOperator . varUnqual
+
+instance PrettyVar a => PrettyHsVar (HsId a) where
+  varUnqual (Qualified _ _ s) = s
+  varUnqual v                 = varStr v
+
+tuple ds = parens (fsep (punctuate "," ds))
+
+csv = sep . punctuate ","
+
+instance PrettyHsVar a => Pretty (Expr a) where
+  pp e =
+    case e of
+      Apply x [] -> ppHsVar x
+      Apply x es | Lam ps b <- last es -> ((ppHsVar x $\ fsep (map pp_par (init es))) $\ "(\\" <+> fsep (map (ppPat 1) ps) <+> "->") $\ pp b <> ")"
+      Apply x es -> ppOper x (map pp_par es)
+      ImpVar x   -> "?" <> ppHsVar x
+      Do ss e    -> "do" <+> (vcat (map pp (ss ++ [Stmt e])))
+      Let x e b  -> "let" <+> (ppHsVar x <+> "=" $\ pp e) $\ "in" <+> pp b
+      ImpLet x e b  -> "let" <+> ("?" <> ppHsVar x <+> "=" $\ pp e) $\ "in" <+> pp b
+      Lam ps e   -> "\\" <+> fsep (map pp ps) <+> "->" $\ pp e
+      List es    -> brackets (csv (map pp es))
+      Tup es     -> tuple (map pp es)
+      String s   -> "\"" <> ppUnqual s <> "\""
+      Case e brs -> ("case" <+> pp e <+> "of") $\ vcat [ (ppPat 0 p <+> "->") $\ pp rhs | (p,rhs) <- brs ]
+      Int i      -> integer i
+      Noop       -> "Prelude.return ()"
+      QuoteTyCon tc -> "''" <> ppHsVar tc
+      QuoteName x   -> "'" <> ppHsVar x
+      THSplice e    -> "$" <> parens (pp e)
+      Record e upd  -> pp_par e $\ braces (sep (punctuate "," [ ppHsVar f <+> "=" $\ pp rhs | (f,rhs) <- upd ]))
+      e ::: t       -> pp_par e <+> "::" $\ pp t
+   where
+    pp_par e0 =
+      case e0 of
+        Apply x []  -> pp e0
+        List{}      -> pp e0
+        Tup{}       -> pp e0
+        String{}    -> pp e0
+        _           -> parens (pp e0)
+
+instance PrettyHsVar a => Pretty (Stmt a) where
+  pp (Bind x e)        = ppHsVar x <+> "<-" $\ pp e
+  pp (BindTyped x t e) = (ppHsVar x <+> "::" $\ pp t <+> "<-") $\ pp e
+  pp (Stmt e)          = pp e
+
+instance PrettyHsVar a => Pretty (Pat a) where
+  pp = ppPat 0
+
+ppPat :: PrettyHsVar a => Int -> Pat a -> Doc
+ppPat i p =
+  case p of
+    VarPat x    -> ppHsVar x
+    ConPat k [] -> ppHsVar k
+    ConPat k ps -> parIf (i >= 1) (ppOper k (map (ppPat 1) ps))
+    TupPat ps   -> tuple (map (ppPat 0) ps)
+    WildPat     -> "_"
+
+instance PrettyHsVar a => Pretty (Decl a) where
+  pp = go 0
+    where
+    pp_ctx [] = empty
+    pp_ctx ctx = pp (TyTup ctx) <+> "=>"
+    go i d =
+      case d of
+        TySig f ctx t -> (ppHsVar f <+> "::" $\ pp_ctx ctx) $\ pp t
+        FunDecl f xs ->
+          vcat
+            [ (ppOperQ (i == 0) f (map (ppPat 1) ps) <+> "=") $\ pp b
+            | (ps,b) <- xs
+            ]
+        DataDecl tc tvs cons derivs ->
+          let dat = case cons of
+               [(_,[_])] -> "newtype"
+               _         -> "data"
+          in ((dat $\ ppOper tc (map ppHsVar tvs) <+> "=") $\
+              fsep (punctuate " |" [ ppOper c (map (ppType True 2) ts) | (c,ts) <- cons ])) $\
+              (if null derivs then empty
+               else "deriving" $\ tuple (map ppHsVar derivs))
+        InstDecl ctx head ds ->
+          (("instance" $\
+            (pp_ctx ctx $\ pp head)) $\
+               "where") $\ vcat (map (go 1) ds)
+        TypeDef lhs rhs -> "type" <+> ppType False 0 lhs <+> "=" $\ pp rhs
+        decl `Where` ds -> go i decl $\ "where" $\ vcat (map (go 1) ds)
+        TH e -> pp e
+        Module s -> "module" <+> text s <+> "where"
+        LANGUAGE s -> "{-#" <+> "LANGUAGE" <+> text s <+> "#-}"
+        QualImport m ms -> "import" <+> "qualified" <+> text m $\
+                             case ms of
+                                Nothing -> empty
+                                Just s  -> "as" <+> text s
+
+instance PrettyHsVar a => Pretty (Decls a) where
+  pp (Decls ds) = vcat (map pp ds)
+
+instance PrettyHsVar a => Pretty (Type a) where
+  pp = ppType True 0
+
+ppType :: PrettyHsVar a => Bool -> Int -> Type a -> Doc
+ppType qual i t0 =
+  case t0 of
+    TyCon t []  -> ppHsVar t
+    TyCon t ts  -> parIf (i >= 2) (ppOperQ qual t (map (ppType True 2) ts))
+    TyVar x     -> ppHsVar x
+    TyTup ts    -> tuple (map (ppType True 0) ts)
+    TyArr t1 t2 -> parIf (i >= 1) (ppType True 1 t1 <+> "->" $\ ppType True 0 t2)
+    TyCtx ctx t -> parIf (i >= 1) (pp (TyTup ctx) <+> "=>" $\ ppType qual 0 t)
+    TyForall tvs t  -> parIf (i >= 1) ("forall" <+> fsep (map ppVar tvs) <+> "." $\ ppType qual 0 t)
+    TyImp x t       -> parIf (i >= 1) ("?" <> ppVar x <+> "::" $\ ppType qual 0 t)
+
diff --git a/src/Tip/Pretty/Isabelle.hs b/src/Tip/Pretty/Isabelle.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pretty/Isabelle.hs
@@ -0,0 +1,286 @@
+{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ScopedTypeVariables, ViewPatterns #-}
+module Tip.Pretty.Isabelle where
+
+import Text.PrettyPrint
+
+import Tip.Pretty
+import Tip.Types
+import Tip.Utils.Rename (renameWith,disambig)
+import Tip.Rename
+import Tip.Core (ifView, DeepPattern(..), patternMatchingView, topsort, makeGlobal, exprType)
+
+import Data.Char
+import Data.Maybe
+import Data.List (intersperse, partition)
+
+import Data.Generics.Geniplate
+
+import qualified Data.Set as S
+
+
+($-$), block :: Doc -> Doc -> Doc
+d $-$ b = vcat [d,"",b]
+
+block d c = (d $\ c)
+
+pcsv, csv, csv1 :: [Doc] -> Doc
+csv = fsep . punctuate ","
+
+csv1 [x] = x
+csv1 xs  = pcsv xs
+
+pcsv = parens . csv
+
+separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc
+separating comb seps docs = comb (go seps docs)
+  where
+    go (s:ss) (d:ds) = s <+> d : go ss ds
+    go _      []     = []
+    go []     _      = error "separating: ran out of separators!"
+
+escape :: Char -> String
+escape x | isAlphaNum x = [x]
+escape _                = []
+
+intersperseWithPre :: (a -> a -> a) -> a -> [a] -> [a]
+intersperseWithPre f  s (t1:t2:ts) = t1:map (f s) (t2:ts)
+intersperseWithPre _f _s ts        = ts
+
+quote :: Doc -> Doc
+quote d = "\""<> d <> "\""
+
+quoteWhen :: (a -> Bool) -> a -> (Doc -> Doc)
+quoteWhen p t | p t       = quote
+              | otherwise = id
+
+ppAsTuple :: [a] -> (a -> Doc) -> Doc
+ppAsTuple ts toDoc = parIf (length ts > 1) ((sep.punctuate ",") (map toDoc ts))
+
+ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc
+ppTheory (renameAvoiding isabelleKeywords escape -> Theory{..})
+  = vcat ["theory" <+> "A",
+          --"imports $HIPSTER_HOME/IsaHipster",
+          "imports Main",
+          --"        \"../../IsaHipster\"",  -- convenience
+          "begin"] $$
+    foldl ($-$) empty (
+      map ppSort thy_sorts ++
+      map ppDatas (topsort thy_datatypes) ++
+      map ppUninterp thy_sigs ++
+      map ppFuncs (topsort thy_funcs) ++
+      -- ["(*hipster" <+> sep (map (ppVar.func_name) thy_funcs) <+> "*)"] ++   -- convenience
+      zipWith ppFormula thy_asserts [0..])
+    $-$
+    "end"
+
+ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc
+--ppSort (Sort sort 0) = "type" $\ ppVar sort
+ppSort (Sort sort n) =
+  error $ "Can't translate abstract sort " ++ show (ppVar sort) ++ " of arity " ++ show n ++ " to Isabelle"
+
+ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc
+ppDatas []  = empty
+ppDatas dts = "datatype" <+>
+    vcat (intersperseWithPre ($\) "and" (map ppData dts))
+
+ppData :: (PrettyVar a, Ord a) => Datatype a -> Doc
+ppData (Datatype tc tvs cons) =
+  ppAsTuple tvs ppTyVar $\
+    ppVar tc $\ separating fsep ("=":repeat "|") (map ppCon cons)
+--ppDatas (d:ds) = ppData "datatype" d
+        -- FIXME: No mutual recusion for now...
+        --vcat (ppData "type" d:map (ppData "with") ds)
+
+ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc
+ppCon (Constructor c _d as) = ppVar c <+> fsep (map (quote . ppType 0 . snd) as)
+
+ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc -> Doc
+ppQuant _name [] _to d = d
+ppQuant name  ls to  d = (name $\ fsep (map (parens . ppLocalBinder) ls) <+> to) $\ d
+
+ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc
+ppBinder x t = ppVar x <+> "::" $\ ppType 0 t
+
+ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc
+ppLocalBinder (Local x t) = ppBinder x t
+
+ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc
+ppUninterp (Signature f (PolyType _ arg_types result_type)) =
+  --"function" $\ ppVar f $\ fsep (map (ppType 1) arg_types) $\ (":" <+> ppType 1 result_type)
+  -- XXX: consts maybe?
+  error $ "Can't translate uninterpreted function " ++ varStr f
+
+ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc
+ppFuncs []       = empty
+ppFuncs (fn:fns) = header <+>
+    vcat (intersperseWithPre ($\) "and" fTys) <+> "where" $$
+    vcat (intersperseWithPre ($\) "|" fDefs) $$
+    termination
+  where (header,termination) | null fns  = ("fun",empty)
+                             | otherwise = ("function","by pat_completeness auto")
+        (fTys, fDefs) = foldr (\(ppFunc -> (pf,pds)) (ftys,fdefs) ->
+                                  (pf:ftys, pds++fdefs))
+                        ([],[]) (fn:fns)
+
+ppFunc :: (PrettyVar a, Ord a) => Function a -> (Doc,[Doc])
+ppFunc (Function f _tvs xts t e) =
+     (ppVar f <+> "::" <+> quote (ppType (-1) (map lcl_type xts :=>: t)),
+      [ quote $ ppVar f $\ fsep (map ppDeepPattern dps) <+> "=" $\ ppExpr 0 rhs
+                  | (dps,rhs) <- patternMatchingView xts e ])
+
+   -- (header $\ ppVar f $\ fsep (map (parens . ppLocalBinder) xts) $\ (":" <+> ppType 0 t <+> "="))
+   --  $\ ppExpr 0 e
+
+ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc
+ppDeepPattern (DeepConPat (Global k _ _) dps) = parens (ppVar k <+> fsep (map ppDeepPattern dps))
+ppDeepPattern (DeepVarPat (Local x _)) = ppVar x
+ppDeepPattern (DeepLitPat lit) = ppLit lit
+
+
+ppFormula :: (PrettyVar a, Ord a) => Formula a -> Int -> Doc
+ppFormula (Formula role _tvs term) i =
+  (ppRole role <+> ("x" <> int i) <+> ":") $\ quote (ppExpr 0 term) $$ "oops"
+  -- "by (tactic {* Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1 *})" convenience
+
+ppRole :: Role -> Doc
+ppRole Assert = "lemma" --Better with lemma and sorry-proof here. Then need to insert 'sorry' on the line below somehow.
+ppRole Prove  = "theorem"
+
+ppExpr :: (PrettyVar a, Ord a) => Int -> Expr a -> Doc
+ppExpr i e | Just (c,t,f) <- ifView e = parens $ "if" $\ ppExpr 0 c $\ "then" $\ ppExpr 0 t $\ "else" $\ ppExpr 0 f
+ppExpr i e@(hd@(Gbl Global{..}) :@: es)
+  | isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing) =
+    parIf (i > 0) $
+    ppHead hd (map (ppExpr 1) es)-- $\ "::" $\ ppType 0 (exprType e)
+ppExpr i (hd :@: es)  = parIf ((i > 0 && not (null es)) || isLogB hd) $
+                          ppHead hd (map (ppExpr 1) es)
+  where isLogB (Builtin b) = logicalBuiltin b
+        isLogB _           = False
+ppExpr _ (Lcl l)      = ppVar (lcl_name l)
+ppExpr i (Lam ls e)   = parIf (i > 0) $ ppQuant "%" ls "=>" (ppExpr 0 e)
+ppExpr i (Let x b e)  = parIf (i > 0) $ sep ["let" $\ ppLocalBinder x <+> "=" $\ ppExpr 0 b, "in" <+> ppExpr 0 e]
+ppExpr i (Quant _ q ls e) = parIf (i > 0) $ ppQuant (ppQuantName q) ls "." (ppExpr 0 e)
+ppExpr i (Match e alts) =
+  parIf (i <= 0) $ block ("case" $\ ppExpr 0 e $\ "of")
+                         (vcat (intersperseWithPre ($\) "|" (map ppCase
+                                  (uncurry (++) (partition ((/= Default).case_pat) alts)))))
+
+ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc
+ppHead (Gbl gbl)      args                        = ppVar (gbl_name gbl) $\ fsep args
+ppHead (Builtin b)    [u,v] | Just d <- ppBinOp b = u <+> d $\ v
+ppHead (Builtin At{}) args                        = fsep args
+ppHead (Builtin b)    args                        = ppBuiltin b $\ fsep args
+
+ppBuiltin :: Builtin -> Doc
+ppBuiltin (Lit lit) = ppLit lit
+ppBuiltin IntDiv    = "(op div)"
+ppBuiltin IntMod    = "mod"
+ppBuiltin Not       = "~"
+ppBuiltin b         = error $ "Isabelle.ppBuiltin: " ++ show b
+
+ppBinOp :: Builtin -> Maybe Doc
+ppBinOp And       = Just "&"
+ppBinOp Or        = Just "|"
+ppBinOp Implies   = Just "==>"
+ppBinOp Equal     = Just "="
+ppBinOp Distinct  = Just "~="
+ppBinOp IntAdd    = Just "+"
+ppBinOp IntSub    = Just "-"
+ppBinOp IntMul    = Just "*"
+ppBinOp IntGt     = Just ">"
+ppBinOp IntGe     = Just ">="
+ppBinOp IntLt     = Just "<"
+ppBinOp IntLe     = Just "<="
+ppBinOp _         = Nothing
+
+ppLit :: Lit -> Doc
+ppLit (Int i)      = integer i
+ppLit (Bool True)  = "True"
+ppLit (Bool False) = "False"
+ppLit (String s)   = text (show s)
+
+ppQuantName :: Quant -> Doc
+ppQuantName Forall = "!!"
+ppQuantName Exists = "??"
+
+ppCase :: (PrettyVar a, Ord a) => Case a -> Doc
+ppCase (Case pat rhs) = ppPat pat <+> "=>" $\ ppExpr 0 rhs
+
+ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc
+ppPat pat = case pat of
+  Default     -> "other"
+  ConPat g ls -> ppVar (gbl_name g) $\ fsep (map (ppVar . lcl_name) ls)
+  LitPat l    -> ppLit l
+
+ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc
+ppType _ (TyVar x)     = ppTyVar x
+ppType i (TyCon tc ts) = parIf (i > 0 && (not . null) ts) $
+                           ppAsTuple ts (ppType 2 {-1-}) $\ ppVar tc
+ppType i (ts :=>: r)   = parIf (i >= 0) $ fsep (punctuate " =>" (map (ppType 0) (ts ++ [r])))
+ppType _ (BuiltinType Integer) = "int"
+ppType _ (BuiltinType Boolean) = "bool"
+
+ppTyVar :: (PrettyVar a, Ord a) => a -> Doc
+ppTyVar x = "'" <> ppVar x
+
+-- FIXME: THESE are just copied from the Why3-file
+isabelleKeywords :: [String]
+isabelleKeywords = (words . unlines)
+    [ "equal not use import goal int"
+    , "and or"
+    , "forall exists"
+    , "module theory"
+    , "ac"
+    , "and"
+    , "axiom"
+    , "inversion"
+    , "bitv"
+    , "check"
+    , "cut"
+    , "distinct"
+    , "else"
+    , "exists"
+    , "false"
+    , "forall"
+    , "function"
+    , "goal"
+    , "if"
+    , "in"
+    , "include"
+    , "int"
+    , "let"
+    , "logic"
+    , "not"
+    , "or"
+    , "predicate"
+    , "prop"
+    , "real"
+    , "rewriting"
+    , "then"
+    , "true"
+    , "type"
+    , "unit"
+    , "void"
+    , "with"
+    , "sign Nil Cons"
+    , "div"
+    , "mod"
+    ] ++
+    [ "theorem lemma declare axiomatization"
+    , "prefer def thm term typ"
+    , "fun primrec definition value where infixl infixr abbreviation notation for"
+    , "datatype type_synonym option consts typedecl inductive_set inductive_cases"
+    , "True False None Some abs"
+    , "class instantiation fixes instance assumes shows proof fix show have obtain"
+    , "unfolding qed from"
+    , "begin end imports ML using"
+    , "apply done oops sorry by back"
+    , "text header chapter section subsection subsubsection sect subsect subsubsect"
+    , "nil cons Nil Cons"
+    , "nil"
+    , "cons"
+    , "Nil"
+    , "Cons"
+    , "EX ALL"
+    ]
+
diff --git a/src/Tip/Pretty/SMT.hs b/src/Tip/Pretty/SMT.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pretty/SMT.hs
@@ -0,0 +1,252 @@
+{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ViewPatterns #-}
+module Tip.Pretty.SMT where
+
+import Text.PrettyPrint
+
+import Tip.Pretty
+import Tip.Types
+import Tip.Core (ifView, topsort, neg, exprType, makeGlobal)
+import Tip.Rename
+import Data.Maybe
+import Data.Char (isAlphaNum)
+
+expr,parExpr,parExprSep :: Doc -> [Doc] -> Doc
+parExpr s [] = parens s
+parExpr s xs = ("(" <> s) $\ (fsep xs <> ")")
+
+parExprSep s [x]    = ("(" <> s) $\ (x <> ")")
+parExprSep s (x:xs) = (("(" <> s) $\ x) $\ (fsep xs <> ")")
+parExprSep s xs     = parExpr s xs
+
+expr s [] = s
+expr s xs = parExpr s xs
+
+exprSep s [] = s
+exprSep s xs = parExprSep s xs
+
+apply :: Doc -> Doc -> Doc
+apply s x = parExpr s [x]
+
+validSMTChar :: Char -> String
+validSMTChar x
+  | isAlphaNum x                             = [x]
+  | x `elem` ("~!@$%^&*_-+=<>.?/" :: String) = [x]
+  | otherwise                                = ""
+
+ppTheory :: (Ord a,PrettyVar a) => Theory a -> Doc
+ppTheory (renameAvoiding smtKeywords validSMTChar -> Theory{..})
+  = vcat
+     (map ppSort thy_sorts ++
+      map ppDatas (topsort thy_datatypes) ++
+      map ppUninterp thy_sigs ++
+      map ppFuncs (topsort thy_funcs) ++
+      map ppFormula thy_asserts ++
+      ["(check-sat)"])
+
+ppSort :: PrettyVar a => Sort a -> Doc
+ppSort (Sort sort n) = parExpr "declare-sort" [ppVar sort, int n]
+
+ppDatas :: PrettyVar a => [Datatype a] -> Doc
+ppDatas datatypes@(Datatype _ tyvars _:_) =
+  parExprSep "declare-datatypes" [parens (fsep (map ppVar tyvars)), parens (fsep (map ppData datatypes))]
+
+ppData :: PrettyVar a => Datatype a -> Doc
+ppData (Datatype tycon _ datacons) =
+  parExprSep (ppVar tycon) (map ppCon datacons)
+
+ppCon :: PrettyVar a => Constructor a -> Doc
+ppCon (Constructor datacon selector args) =
+  parExprSep (ppVar datacon) [apply (ppVar p) (ppType t) | (p,t) <- args]
+
+
+par :: (PrettyVar a) => [a] -> Doc -> Doc
+par [] d = d
+par xs d = parExprSep "par" [parens (fsep (map ppVar xs)), parens d]
+
+par' :: (PrettyVar a) => [a] -> Doc -> Doc
+par' [] d = d
+par' xs d = parExprSep "par" [parens (fsep (map ppVar xs)), d]
+
+ppUninterp :: PrettyVar a => Signature a -> Doc
+ppUninterp (Signature f (PolyType tyvars arg_types result_type)) =
+  apply "declare-fun"
+    (par' tyvars
+      (apply (ppVar f)
+        (sep [parens (fsep (map ppType arg_types)), ppType result_type])))
+
+ppFuncs :: (Ord a, PrettyVar a) => [Function a] -> Doc
+ppFuncs fs = expr "define-funs-rec"
+  [ parens (vcat (map ppFuncSig fs))
+  , parens (vcat (map (ppExpr . func_body) fs))
+  ]
+
+ppFuncSig :: PrettyVar a => Function a -> Doc
+ppFuncSig (Function f tyvars args res_ty body) =
+  (par' tyvars
+    (parens
+      (ppVar f $\ fsep [ppLocals args, ppType res_ty])))
+
+ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc
+ppFormula (Formula Prove tvs term)  = apply "assert-not" (par' tvs (ppExpr term))
+ppFormula (Formula Assert tvs term) = apply "assert"     (par' tvs (ppExpr term))
+
+ppExpr :: (Ord a, PrettyVar a) => Expr a -> Doc
+ppExpr e | Just (c,t,f) <- ifView e = parExpr "ite" (map ppExpr [c,t,f])
+ppExpr e@(hd@(Gbl Global{..}) :@: es)
+  | isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing)
+      = exprSep "as" [exprSep (ppHead hd) (map ppExpr es), ppType (exprType e)]
+ppExpr (hd :@: es)  = exprSep (ppHead hd) (map ppExpr es)
+ppExpr (Lcl l)      = ppVar (lcl_name l)
+ppExpr (Lam ls e)   = parExprSep "lambda" [ppLocals ls,ppExpr e]
+ppExpr (Match e as) = "(match" $\ ppExpr e $\ (vcat (map ppCase as) <> ")")
+ppExpr (Let x b e)  = parExprSep "let" [parens (parens (ppLocal x $\ ppExpr b)), ppExpr e]
+ppExpr (Quant _ q ls e) = parExprSep (ppQuant q) [ppLocals ls, ppExpr e]
+
+ppLocals :: PrettyVar a => [Local a] -> Doc
+ppLocals ls = parens (fsep (map ppLocal ls))
+
+ppLocal :: PrettyVar a => Local a -> Doc
+ppLocal (Local l t) = expr (ppVar l) [ppType t]
+
+ppHead :: PrettyVar a => Head a -> Doc
+ppHead (Builtin b) = ppBuiltin b
+ppHead (Gbl gbl)   = ppVar (gbl_name gbl) {- -- $$ ";" <> ppPolyType (gbl_type gbl)
+                                             -- $$ ";" <> fsep (map ppType (gbl_args gbl))
+                                             -- $$ text ""
+                                          -}
+
+ppBuiltin :: Builtin -> Doc
+ppBuiltin (Lit lit) = ppLit lit
+ppBuiltin Not       = "not"
+ppBuiltin And       = "and"
+ppBuiltin Or        = "or"
+ppBuiltin Implies   = "=>"
+ppBuiltin Equal     = "="
+ppBuiltin Distinct  = "distinct"
+ppBuiltin IntAdd    = "+"
+ppBuiltin IntSub    = "-"
+ppBuiltin IntMul    = "*"
+ppBuiltin IntDiv    = "div"
+ppBuiltin IntMod    = "mod"
+ppBuiltin IntGt     = ">"
+ppBuiltin IntGe     = ">="
+ppBuiltin IntLt     = "<"
+ppBuiltin IntLe     = "<="
+ppBuiltin At{}      = "@"
+
+ppLit :: Lit -> Doc
+ppLit (Int i)      = integer i
+ppLit (Bool True)  = "true"
+ppLit (Bool False) = "false"
+ppLit (String s)   = text (show s)
+
+ppQuant :: Quant -> Doc
+ppQuant Forall = "forall"
+ppQuant Exists = "exists"
+
+ppCase :: (Ord a, PrettyVar a) => Case a -> Doc
+ppCase (Case pat rhs) = parExprSep "case" [ppPat pat,ppExpr rhs]
+
+ppPat :: PrettyVar a => Pattern a -> Doc
+ppPat Default         = "default"
+ppPat (ConPat g args) = expr (ppVar (gbl_name g)) [ppVar (lcl_name arg) | arg <- args]
+ppPat (LitPat lit)    = ppLit lit
+
+ppType :: PrettyVar a => Type a -> Doc
+ppType (TyVar x)     = ppVar x
+ppType (TyCon tc ts) = expr (ppVar tc) (map ppType ts)
+ppType (ts :=>: r)   = parExpr "=>" (map ppType (ts ++ [r]))
+ppType (BuiltinType Integer) = "Int"
+ppType (BuiltinType Boolean) = "Bool"
+
+-- Temporary use SMTLIB as the pretty printer:
+
+instance (Ord a,PrettyVar a) => Pretty (Theory a) where
+  pp = ppTheory
+
+instance (Ord a, PrettyVar a) => Pretty (Expr a) where
+  pp = ppExpr
+
+ppPolyType :: PrettyVar a => PolyType a -> Doc
+ppPolyType (PolyType tyvars arg_types result_type) =
+  par tyvars
+    (parens
+      (sep [parens (fsep (map ppType arg_types)), ppType result_type]))
+
+instance PrettyVar a => Pretty (PolyType a) where
+  pp = ppPolyType
+
+instance PrettyVar a => Pretty (Type a) where
+  pp = ppType
+
+instance (Ord a, PrettyVar a) => Pretty (Function a) where
+  pp = ppFuncs . return
+
+instance (Ord a, PrettyVar a) => Pretty (Formula a) where
+  pp = ppFormula
+
+instance PrettyVar a => Pretty (Datatype a) where
+  pp = ppDatas . return
+
+instance PrettyVar a => Pretty (Signature a) where
+  pp = ppUninterp
+
+instance PrettyVar a => Pretty (Local a) where
+  pp = ppLocal
+
+instance PrettyVar a => Pretty (Global a) where
+  pp = ppHead . Gbl
+
+instance PrettyVar a => Pretty (Head a) where
+  pp = ppHead
+
+instance PrettyVar a => Pretty (Pattern a) where
+  pp = ppPat
+
+smtKeywords :: [String]
+smtKeywords =
+    [ "ac"
+    , "and"
+    , "axiom"
+    , "inversion"
+    , "bitv"
+    , "bool"
+    , "check"
+    , "cut"
+    , "distinct"
+    , "else"
+    , "exists"
+    , "false"
+    , "forall"
+    , "function"
+    , "goal"
+    , "if"
+    , "in"
+    , "include"
+    , "int"
+    , "let"
+    , "logic"
+    , "not"
+    , "or"
+    , "predicate"
+    , "prop"
+    , "real"
+    , "rewriting"
+    , "then"
+    , "true"
+    , "type"
+    , "unit"
+    , "void"
+    , "with"
+    , "assert", "check-sat"
+    , "abs", "min", "max", "const"
+    , "mod", "div"
+    , "=", "=>", "+", "-", "*", ">", ">=", "<", "<=", "@", "!"
+    -- Z3:
+    , "Bool", "Int", "Array", "List", "insert"
+    , "isZero"
+    , "map"
+    -- CVC4:
+    , "as", "concat"
+    ]
+
diff --git a/src/Tip/Pretty/Why3.hs b/src/Tip/Pretty/Why3.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Pretty/Why3.hs
@@ -0,0 +1,241 @@
+{-# LANGUAGE RecordWildCards, OverloadedStrings, PatternGuards, ScopedTypeVariables, ViewPatterns #-}
+module Tip.Pretty.Why3 where
+
+import Text.PrettyPrint
+
+import Tip.Pretty
+import Tip.Types
+import Tip.Utils.Rename (renameWith,disambig)
+import Tip.Rename
+import Tip.Core (ifView, DeepPattern(..), patternMatchingView, topsort, makeGlobal, exprType)
+
+import Data.Char
+import Data.Maybe
+
+import Data.Generics.Geniplate
+
+import qualified Data.Set as S
+
+data Why3Var a = Why3Var Bool {- is constructor -} a
+  deriving (Eq,Ord,Show)
+
+instance PrettyVar a => PrettyVar (Why3Var a) where
+  varStr (Why3Var b x) = (if b then toUpper else toLower) `mapHead` addAlpha (varStr x)
+   where
+    mapHead :: (Char -> Char) -> String -> String
+    f `mapHead` []     = [f 'x']
+    f `mapHead` (x:xs) = f x:xs
+
+    addAlpha :: String -> String
+    addAlpha s@(x:_) | isAlpha x = s
+    addAlpha s                   = "x" ++ s
+
+why3VarTheory :: forall a . Ord a => Theory a -> Theory (Why3Var a)
+why3VarTheory thy = fmap mk thy
+ where
+  cons = S.fromList [ c | Constructor c _ _ <- universeBi thy ]
+  mk x = Why3Var (x `S.member` cons) x
+
+block :: Doc -> Doc -> Doc
+block d c = (d $\ c) $$ "end"
+
+pcsv, csv, csv1 :: [Doc] -> Doc
+csv = fsep . punctuate ","
+
+csv1 [x] = x
+csv1 xs  = pcsv xs
+
+pcsv = parens . csv
+
+separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc
+separating comb seps docs = comb (go seps docs)
+  where
+    go (s:ss) (d:ds) = s <+> d : go ss ds
+    go _      []     = []
+    go []     _      = error "separating: ran out of separators!"
+
+escape :: Char -> String
+escape x | isAlphaNum x = [x]
+escape _                = []
+
+ppTheory :: (Ord a,PrettyVar a) => Theory a -> Doc
+ppTheory (renameAvoiding why3Keywords escape . why3VarTheory -> Theory{..})
+  = block ("module" <+> "A") $
+    vcat (
+      "use HighOrd" :
+      "use import int.Int" :
+      "use import int.EuclideanDivision" :
+      map ppSort thy_sorts ++
+      map ppDatas (topsort thy_datatypes) ++
+      map ppUninterp thy_sigs ++
+      map ppFuncs (topsort thy_funcs) ++
+      zipWith ppFormula thy_asserts [0..])
+
+ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc
+ppSort (Sort sort 0) = "type" $\ ppVar sort
+ppSort (Sort sort n) =
+  error $ "Can't translate abstract sort " ++ show (ppVar sort) ++ " of arity " ++ show n ++ " to Why3"
+
+ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc
+ppDatas (d:ds) = vcat (ppData "type" d:map (ppData "with") ds)
+
+ppData :: (PrettyVar a, Ord a) => Doc -> Datatype a -> Doc
+ppData header (Datatype tc tvs cons) =
+  header $\ (ppVar tc $\ sep (map ppTyVar tvs) $\
+    separating fsep ("=":repeat "|") (map ppCon cons))
+
+ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc
+ppCon (Constructor c _d as) = ppVar c <+> fsep (map (ppType 1 . snd) as)
+
+ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc
+ppQuant _name [] d = d
+ppQuant name  ls d = (name $\ fsep (punctuate "," (map ppLocalBinder ls)) <+> ".") $\ d
+
+ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc
+ppBinder x t = ppVar x <+> ":" $\ ppType 0 t
+
+ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc
+ppLocalBinder (Local x t) = ppBinder x t
+
+ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc
+ppUninterp (Signature f (PolyType _ arg_types result_type)) =
+  "function" $\ ppVar f $\ fsep (map (ppType 1) arg_types) $\ (":" <+> ppType 1 result_type)
+
+ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc
+ppFuncs (fn:fns) = vcat (ppFunc "function" fn:map (ppFunc "with") fns)
+
+ppFunc :: (PrettyVar a, Ord a) => Doc -> Function a -> Doc
+ppFunc header (Function f _tvs xts t e) =
+   ((header $\ ppVar f $\ fsep (map (parens . ppLocalBinder) xts) $\ (":" <+> ppType 0 t <+> "="))
+     $\ ppExpr 0 e
+   ) $$
+   ("(*" <+> vcat [ ppVar f $\ fsep (map ppDeepPattern dps) <+> "=" $\ ppExpr 0 rhs
+                  | (dps,rhs) <- patternMatchingView xts e ] <+> "*)")
+
+ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc
+ppDeepPattern (DeepConPat (Global k _ _) dps) = parens (ppVar k <+> fsep (map ppDeepPattern dps))
+ppDeepPattern (DeepVarPat (Local x _)) = ppVar x
+ppDeepPattern (DeepLitPat lit) = ppLit lit
+
+ppFormula :: (PrettyVar a, Ord a) => Formula a -> Int -> Doc
+ppFormula (Formula role _tvs term) i =
+  (ppRole role <+> ("x" <> int i) <+> ":") $\ (ppExpr 0 term)
+
+ppRole :: Role -> Doc
+ppRole Assert = "lemma"
+ppRole Prove  = "goal"
+
+ppExpr :: (PrettyVar a, Ord a) => Int -> Expr a -> Doc
+ppExpr i e | Just (c,t,f) <- ifView e = parIf (i > 0) $ "if" $\ ppExpr 0 c $\ "then" $\ ppExpr 0 t $\ "else" $\ ppExpr 0 f
+ppExpr i e@(hd@(Gbl Global{..}) :@: es)
+  | isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing) =
+    parIf (i > 0) $
+    ppHead hd (map (ppExpr 1) es) $\ ":" $\ ppType 0 (exprType e)
+ppExpr i (hd :@: es)  = parIf (i > 0 && not (null es)) $ ppHead hd (map (ppExpr 1) es)
+ppExpr _ (Lcl l)      = ppVar (lcl_name l)
+ppExpr i (Lam ls e)   = parIf (i > 0) $ ppQuant "\\" ls (ppExpr 0 e)
+ppExpr i (Let x b e)  = parIf (i > 0) $ sep ["let" $\ ppVar (lcl_name x) <+> "=" $\ ppExpr 0 b <+> ":" $\ ppType 0 (lcl_type x), "in" <+> ppExpr 0 e]
+ppExpr i (Quant _ q ls e) = parIf (i > 0) $ ppQuant (ppQuantName q) ls (ppExpr 0 e)
+ppExpr i (Match e alts) =
+  parIf (i > 0) $ block ("match" $\ ppExpr 0 e $\ "with")
+                        (separating vcat (repeat "|") (map ppCase alts))
+
+ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc
+ppHead (Gbl gbl)   args = ppVar (gbl_name gbl) $\ fsep args
+ppHead (Builtin b) [u,v] | Just d <- ppBinOp b = u <+> d $\ v
+ppHead (Builtin At{}) args = fsep args
+ppHead (Builtin b) args = ppBuiltin b $\ fsep args
+
+ppBuiltin :: Builtin -> Doc
+ppBuiltin (Lit lit) = ppLit lit
+ppBuiltin IntDiv    = "div"
+ppBuiltin IntMod    = "mod"
+ppBuiltin Not       = "not"
+ppBuiltin b         = error $ "Why3.ppBuiltin: " ++ show b
+
+ppBinOp :: Builtin -> Maybe Doc
+ppBinOp And       = Just "&&"
+ppBinOp Or        = Just "||"
+ppBinOp Implies   = Just "->"
+ppBinOp Equal     = Just "="
+ppBinOp Distinct  = Just "<>"
+ppBinOp IntAdd    = Just "+"
+ppBinOp IntSub    = Just "-"
+ppBinOp IntMul    = Just "*"
+ppBinOp IntGt     = Just ">"
+ppBinOp IntGe     = Just ">="
+ppBinOp IntLt     = Just "<"
+ppBinOp IntLe     = Just "<="
+ppBinOp _         = Nothing
+
+ppLit :: Lit -> Doc
+ppLit (Int i)      = integer i
+ppLit (Bool True)  = "true"
+ppLit (Bool False) = "false"
+ppLit (String s)   = text (show s)
+
+ppQuantName :: Quant -> Doc
+ppQuantName Forall = "forall"
+ppQuantName Exists = "exists"
+
+ppCase :: (PrettyVar a, Ord a) => Case a -> Doc
+ppCase (Case pat rhs) = ppPat pat <+> "->" $\ ppExpr 0 rhs
+
+ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc
+ppPat pat = case pat of
+  Default     -> "_"
+  ConPat g ls -> ppVar (gbl_name g) $\ fsep (map (ppVar . lcl_name) ls)
+  LitPat l    -> ppLit l
+
+ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc
+ppType _ (TyVar x)     = ppTyVar x
+ppType i (TyCon tc ts) = parIf (i > 0) $ ppVar tc $\ fsep (map (ppType 1) ts)
+ppType i (ts :=>: r)   = parIf (i > 0) $ fsep (punctuate " ->" (map (ppType 1) (ts ++ [r])))
+ppType _ (BuiltinType Integer) = "int"
+ppType _ (BuiltinType Boolean) = "bool"
+
+ppTyVar :: (PrettyVar a, Ord a) => a -> Doc
+ppTyVar x = "'" <> ppVar x
+
+why3Keywords :: [String]
+why3Keywords = words $ unlines
+    [ "equal not function use import goal int"
+    , "and or"
+    , "forall exists"
+    , "module theory"
+    , "ac"
+    , "and"
+    , "axiom"
+    , "inversion"
+    , "bitv"
+    , "check"
+    , "cut"
+    , "distinct"
+    , "else"
+    , "exists"
+    , "false"
+    , "forall"
+    , "function"
+    , "goal"
+    , "if"
+    , "in"
+    , "include"
+    , "int"
+    , "let"
+    , "logic"
+    , "not"
+    , "or"
+    , "predicate"
+    , "prop"
+    , "real"
+    , "rewriting"
+    , "then"
+    , "true"
+    , "type"
+    , "unit"
+    , "void"
+    , "with"
+    , "sign Nil Cons"
+    , "div"
+    , "mod"
+    ]
diff --git a/src/Tip/Rename.hs b/src/Tip/Rename.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Rename.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Tip.Rename(renameAvoiding,RenamedId(..)) where
+
+#include "errors.h"
+import Data.Char (isDigit)
+import Tip.Core hiding (globals)
+import Tip.Scope
+import Tip.Pretty
+import Tip.Utils.Rename
+import Data.Traversable (Traversable)
+import Data.Foldable (Foldable)
+import qualified Data.Foldable as F
+import qualified Data.Map as M
+
+-- | The representation of renamed Ids.
+newtype RenamedId = RenamedId String
+  deriving (Eq,Ord,Show)
+
+instance PrettyVar RenamedId where
+  varStr (RenamedId x) = x
+
+data TwoStage a = Remain a | Renamed String
+ deriving (Eq,Ord)
+
+instance PrettyVar a => Show (TwoStage a) where
+  show (Remain x)  = "Remain " ++ varStr x
+  show (Renamed s) = "Renamed " ++ s
+
+renameSome
+  :: (Traversable t,Ord a,PrettyVar a)
+  => (a -> Bool) -> [String] -> (a -> [String]) -> t a -> t (TwoStage a)
+renameSome p_rename kwds mk_name =
+  renameWithBlocks
+    (map Renamed kwds)
+    (\ v ->
+      if p_rename v then map Renamed (mk_name v)
+                    else Remain v:__)
+
+renameRest
+  :: (Traversable t,Ord a,PrettyVar a)
+  => [String] -> (a -> [String]) -> t (TwoStage a) -> t RenamedId
+renameRest kwds mk_name =
+  renameWithBlocks
+    (map RenamedId kwds)
+    (\ v ->
+       case v of
+         Renamed s -> RenamedId s:__
+         Remain a  -> map RenamedId (mk_name a))
+
+-- | Renames a theory
+renameAvoiding :: forall a . (Ord a,PrettyVar a) =>
+       [String]         -- ^ Keywords to avoid
+    -> (Char -> String) -- ^ Escaping
+    -> Theory a         -- ^ Theory to be renamed
+    -> Theory RenamedId -- ^ The renamed theory
+renameAvoiding kwds repl thy
+   = mapDecls (renameRest kwds (filter (`notElem` assigned_gbl_names) . disambig rn)) first_pass
+ where
+  first_pass :: Theory (TwoStage a)
+  first_pass = renameSome (`elem` gbls0) kwds (disambig rn) thy
+    where gbls0 = M.keys (globals (scope thy)) ++ M.keys (types (scope thy))
+
+  assigned_gbl_names   = [ s | Renamed s <- F.toList first_pass ]
+
+  rn :: a -> String
+  rn = concatMap repl . varStr
+
diff --git a/src/Tip/Scope.hs b/src/Tip/Scope.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Scope.hs
@@ -0,0 +1,220 @@
+-- | A monad for keeping track of variable scope.
+{-# LANGUAGE CPP, RecordWildCards, GeneralizedNewtypeDeriving, FlexibleContexts #-}
+module Tip.Scope where
+
+#include "errors.h"
+import Tip.Core hiding (globals, locals)
+import Tip.Pretty
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Error
+import Data.Map (Map)
+import Data.Set (Set)
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Text.PrettyPrint
+import Control.Monad.Identity
+import Data.Maybe
+
+-- | The scope of a theory
+scope :: (PrettyVar a, Ord a) => Theory a -> Scope a
+scope thy = checkScope (withTheory thy get)
+
+data Scope a = Scope
+  { inner   :: Set a
+  , types   :: Map a (TypeInfo a)
+  , locals  :: Map a (Type a)
+  , globals :: Map a (GlobalInfo a) }
+  deriving Show
+
+-- * Querying the scope
+
+data TypeInfo a =
+    TyVarInfo
+  | DatatypeInfo (Datatype a)
+  | SortInfo Int
+  deriving (Eq, Show)
+
+data GlobalInfo a =
+    FunctionInfo      (PolyType a)
+  | ConstructorInfo   (Datatype a) (Constructor a)
+  | ProjectorInfo     (Datatype a) (Constructor a) Int (Type a)
+  | DiscriminatorInfo (Datatype a) (Constructor a)
+  deriving Show
+
+globalType :: GlobalInfo a -> PolyType a
+globalType (FunctionInfo ty) = ty
+globalType (ConstructorInfo dt con) = constructorType dt con
+globalType (ProjectorInfo dt _ _ ty) = destructorType dt ty
+globalType (DiscriminatorInfo dt _) = destructorType dt (BuiltinType Boolean)
+
+
+isType, isTyVar, isSort, isLocal, isGlobal :: Ord a => a -> Scope a -> Bool
+isType x s = M.member x (types s)
+isLocal x s = M.member x (locals s)
+isGlobal x s = M.member x (globals s)
+isTyVar x s = M.lookup x (types s) == Just TyVarInfo
+isSort x s = case M.lookup x (types s) of Just SortInfo{} -> True
+                                          _               -> False
+
+lookupType :: Ord a => a -> Scope a -> Maybe (TypeInfo a)
+lookupType x s = M.lookup x (types s)
+
+lookupLocal :: Ord a => a -> Scope a -> Maybe (Type a)
+lookupLocal x s = M.lookup x (locals s)
+
+lookupGlobal :: Ord a => a -> Scope a -> Maybe (GlobalInfo a)
+lookupGlobal x s = M.lookup x (globals s)
+
+lookupDatatype :: Ord a => a -> Scope a -> Maybe (Datatype a)
+lookupDatatype x s = do
+  DatatypeInfo dt <- M.lookup x (types s)
+  return dt
+
+lookupFunction :: Ord a => a -> Scope a -> Maybe (PolyType a)
+lookupFunction x s = do
+  FunctionInfo ty <- M.lookup x (globals s)
+  return ty
+
+lookupConstructor :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)
+lookupConstructor x s = do
+  ConstructorInfo dt con <- M.lookup x (globals s)
+  return (dt, con)
+
+lookupDiscriminator :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)
+lookupDiscriminator x s = do
+  DiscriminatorInfo dt con <- M.lookup x (globals s)
+  return (dt, con)
+
+lookupProjector :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a, Int, Type a)
+lookupProjector x s = do
+  ProjectorInfo dt con i ty <- M.lookup x (globals s)
+  return (dt, con, i, ty)
+
+whichDatatype :: Ord a => a -> Scope a -> Datatype a
+whichDatatype s = fromMaybe __ . lookupDatatype s
+whichLocal :: Ord a => a -> Scope a -> Type a
+whichLocal s = fromMaybe __ . lookupLocal s
+whichGlobal :: Ord a => a -> Scope a -> GlobalInfo a
+whichGlobal s = fromMaybe __ . lookupGlobal s
+whichFunction :: Ord a => a -> Scope a -> PolyType a
+whichFunction s = fromMaybe __ . lookupFunction s
+whichConstructor :: Ord a => a -> Scope a -> (Datatype a, Constructor a)
+whichConstructor s = fromMaybe __ . lookupConstructor s
+whichDiscriminator :: Ord a => a -> Scope a -> (Datatype a, Constructor a)
+whichDiscriminator s = fromMaybe __ . lookupDiscriminator s
+whichProjector :: Ord a => a -> Scope a -> (Datatype a, Constructor a, Int, Type a)
+whichProjector s = fromMaybe __ . lookupProjector s
+
+-- * The scope monad
+
+newtype ScopeT a m b = ScopeT { unScopeT :: StateT (Scope a) (ErrorT Doc m) b }
+  deriving (Functor, Applicative, Monad, MonadPlus, Alternative, MonadState (Scope a), MonadError Doc)
+
+instance MonadTrans (ScopeT a) where
+  lift = ScopeT . lift . lift
+
+instance Error Doc where
+  strMsg = text
+
+runScopeT :: Monad m => ScopeT a m b -> m (Either Doc b)
+runScopeT (ScopeT m) = runErrorT (evalStateT m emptyScope)
+
+checkScopeT :: Monad m => ScopeT a m b -> m b
+checkScopeT m = runScopeT m >>= check
+  where
+    check (Left err) = fail (show err)
+    check (Right x)  = return x
+
+type ScopeM a = ScopeT a Identity
+
+runScope :: ScopeM a b -> Either Doc b
+runScope = runIdentity . runScopeT
+
+checkScope :: ScopeM a b -> b
+checkScope = runIdentity . checkScopeT
+
+emptyScope :: Scope a
+emptyScope = Scope S.empty M.empty M.empty M.empty
+
+inContext :: Pretty a => a -> ScopeM b c -> ScopeM b c
+inContext x m =
+  catchError m (\e -> throwError (sep [e, text "in context", nest 2 (pp x)]))
+
+local :: Monad m => ScopeT a m b -> ScopeT a m b
+local m = do
+  s <- get
+  x <- m
+  put s
+  return x
+
+-- * Adding things to the scope in the scope monad
+
+newScope :: Monad m => ScopeT a m b -> ScopeT a m b
+newScope m = local $ do
+  modify (\s -> s { inner = S.empty })
+  m
+
+newName :: (PrettyVar a, Ord a, Monad m) => a -> ScopeT a m ()
+newName x = do
+  s <- gets inner
+  case S.member x s of
+    True ->
+      throwError $
+        fsep [text "Name", ppVar x, text "rebound"]
+    False ->
+      modify (\s -> s { inner = S.insert x (inner s) })
+
+newTyVar :: (Monad m, Ord a, PrettyVar a) => a -> ScopeT a m ()
+newTyVar ty = do
+  newName ty
+  modify $ \s -> s {
+    types = M.insert ty TyVarInfo (types s) }
+
+newSort :: (Monad m, Ord a, PrettyVar a) => Sort a -> ScopeT a m ()
+newSort Sort{..} = do
+  newName sort_name
+  modify $ \s -> s {
+    types = M.insert sort_name (SortInfo sort_arity) (types s) }
+
+newDatatype :: (Monad m, Ord a, PrettyVar a) => Datatype a -> ScopeT a m ()
+newDatatype dt@Datatype{..} = do
+  newName data_name
+  modify $ \s -> s {
+    types = M.insert data_name (DatatypeInfo dt) (types s) }
+  mapM_ (newConstructor dt) data_cons
+
+newConstructor :: (Monad m, Ord a, PrettyVar a) => Datatype a -> Constructor a -> ScopeT a m ()
+newConstructor dt con@Constructor{..} = do
+  mapM_ (newName . fst) funcs
+  modify $ \s -> s {
+    -- OBS entries from left argument take precedence
+    globals = M.union (M.fromList funcs) (globals s) }
+  where
+    funcs =
+      (con_name, ConstructorInfo dt con):
+      (con_discrim, DiscriminatorInfo dt con):
+      [(name, ProjectorInfo dt con i ty) | (i, (name, ty)) <- zip [0..] con_args]
+
+newFunction :: (Monad m, Ord a, PrettyVar a) => Signature a -> ScopeT a m ()
+newFunction Signature{..} = do
+  newName sig_name
+  modify $ \s -> s {
+    globals = M.insert sig_name (FunctionInfo sig_type) (globals s) }
+
+newLocal :: (Monad m, Ord a, PrettyVar a) => Local a -> ScopeT a m ()
+newLocal Local{..} = do
+  newName lcl_name
+  modify $ \s -> s {
+    locals = M.insert lcl_name lcl_type (locals s) }
+
+-- | Add everything in a theory
+withTheory :: (Monad m, Ord a, PrettyVar a) => Theory a -> ScopeT a m b -> ScopeT a m b
+withTheory Theory{..} m = do
+  mapM_ newDatatype thy_datatypes
+  mapM_ newSort thy_sorts
+  mapM_ (newFunction . signature) thy_funcs
+  mapM_ newFunction thy_sigs
+  m
+
diff --git a/src/Tip/Simplify.hs b/src/Tip/Simplify.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Simplify.hs
@@ -0,0 +1,184 @@
+{-# LANGUAGE FlexibleContexts, RecordWildCards, ScopedTypeVariables, ViewPatterns, PatternGuards #-}
+module Tip.Simplify where
+
+import Tip.Core
+import Tip.Scope
+import Tip.Fresh
+import Data.Generics.Geniplate
+import Data.List
+import Data.Maybe
+import Data.Monoid
+import Control.Applicative
+import Control.Monad
+import qualified Data.Map as Map
+import Tip.Writer
+
+-- | Options for the simplifier
+data SimplifyOpts a =
+  SimplifyOpts {
+    touch_lets    :: Bool,
+    -- ^ Allow simplifications on lets
+    should_inline :: Maybe (Scope a) -> Expr a -> Bool,
+    -- ^ Inlining predicate
+    inline_match  :: Bool
+    -- ^ Allow function inlining to introduce match
+  }
+
+-- | Gentle options: if there is risk for code duplication, only inline atomic expressions
+gently :: SimplifyOpts a
+gently       = SimplifyOpts True (const atomic) True
+
+-- | Aggressive options: inline everything that might plausibly lead to simplification
+aggressively :: Name a => SimplifyOpts a
+aggressively = SimplifyOpts True useful True
+  where
+    useful _ Lam{} = True
+    useful mscp (f :@: _) = isConstructor mscp f
+    useful _ _ = False
+
+-- | Simplify an entire theory
+simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a)
+simplifyTheory opts thy@Theory{..} = do
+  thy_funcs   <- mapM (simplifyExprIn (Just thy) opts) thy_funcs
+  thy_asserts <- mapM (simplifyExprIn (Just thy) opts{inline_match = False}) thy_asserts
+  return Theory{..}
+
+-- | Simplify an expression, without knowing its theory
+simplifyExpr :: forall f a. (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => SimplifyOpts a -> f a -> Fresh (f a)
+simplifyExpr opts = simplifyExprIn Nothing opts
+
+-- | Simplify an expression within a theory
+simplifyExprIn :: forall f a. (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => Maybe (Theory a) -> SimplifyOpts a -> f a -> Fresh (f a)
+simplifyExprIn mthy opts@SimplifyOpts{..} = fmap fst . runWriterT . aux
+  where
+    {-# SPECIALISE aux :: Expr a -> WriterT Any Fresh (Expr a) #-}
+    aux :: forall f. TransformBiM (WriterT Any Fresh) (Expr a) (f a) => f a -> WriterT Any Fresh (f a)
+    aux = transformBiM $ \e0 ->
+      let
+        share e1 | e1 /= e0  = return e1
+                 | otherwise = return e0 in
+      case e0 of
+        Builtin At :@: (Lam vars body:args) ->
+          hooray $
+          aux (foldr (uncurry Let) body (zip vars args))
+
+        Let x e body | touch_lets && (atomic e || occurrences x body <= 1) ->
+          lift ((e // x) body) >>= aux
+
+        Let x e body | touch_lets && inlineable body x e ->
+          do e1 <- lift ((e // x) body)
+             (e2, Any simplified) <- lift (runWriterT (aux e1))
+             if simplified then hooray $ return e2 else return e0
+
+        Match e [Case _ e1,Case (LitPat (Bool b)) e2]
+          | e1 == bool (not b) && e2 == bool b -> hooray $ return e
+          | e1 == bool b && e2 == bool (not b) -> hooray $ return (neg e)
+
+        Match (Let x e body) alts | touch_lets ->
+          aux (Let x e (Match body alts))
+
+        Match _ [Case Default body] -> hooray $ return body
+
+        Match (hd :@: args) alts | isConstructor mscp hd ->
+          -- We use reverse because the default case comes first and we want it last
+          case filter (matches hd . case_pat) (reverse alts) of
+            [] -> return e0
+            Case (ConPat _ lcls) body:_ ->
+              hooray $
+              aux $
+                foldr (uncurry Let) body (zip lcls args)
+            Case _ body:_ -> hooray $ return body
+          where
+            matches (Gbl gbl) (ConPat gbl' _) = gbl == gbl'
+            matches (Builtin (Lit lit)) (LitPat lit') = lit == lit'
+            matches _ Default = True
+            matches _ _ = False
+
+        Match (Lcl x) alts ->
+          Match (Lcl x) <$> sequence
+          [ Case pat <$> case pat of
+              ConPat g bs -> subst ((Gbl g :@: map Lcl bs) /// x) rhs
+              LitPat l    -> subst (literal l /// x) rhs
+              _           -> return rhs
+          | Case pat rhs <- alts
+          ]
+          where
+            subst f e = do
+              (e', Any successful) <- lift (runWriterT (f e))
+              if successful then aux e' else return e
+
+        Builtin Equal :@: [Builtin (Lit (Bool x)) :@: [], t]
+          | x -> hooray $ return t
+          | otherwise -> hooray $ return $ neg t
+
+        Builtin Equal :@: [t, Builtin (Lit (Bool x)) :@: []]
+          | x -> hooray $ return t
+          | otherwise -> hooray $ return $ neg t
+
+        Builtin Equal :@: [litView -> Just s,litView -> Just t] -> hooray $ return (bool (s == t))
+
+        Builtin Distinct :@: [litView -> Just s,litView -> Just t] -> hooray $ return (bool (s /= t))
+
+        Builtin Not     :@: [e]      -> share (neg e)
+        Builtin And     :@: [e1, e2] -> share (e1 /\ e2)
+        Builtin Or      :@: [e1, e2] -> share (e1 \/ e2)
+        Builtin Implies :@: [e1, e2] -> share (e1 ==> e2)
+
+        Builtin Equal :@: [e1, e2] ->
+          case exprType e1 of
+            t@(_ :=>: _) -> hooray $ go t e1 e2 []
+              where
+              go (args :=>: rest) u v lcls =
+                do more <- lift (mapM freshLocal args)
+                   go rest (apply u (map Lcl more))
+                           (apply v (map Lcl more))
+                           (lcls ++ more)
+              go _ u v lcls = return (mkQuant Forall lcls (u === v))
+            _ -> return e0
+
+        Gbl gbl@Global{..} :@: ts ->
+          case Map.lookup gbl_name inlinings of
+            Just func@Function{..}
+              | and [ inlineable func_body x t | (x, t) <- zip func_args ts ] -> do
+                  func_body <- boo $ aux func_body
+                  e1 <-
+                    transformTypeInExpr (applyType func_tvs gbl_args) <$>
+                      lift (substMany (zip func_args ts) func_body)
+                  (e2, Any simplified) <- lift (runWriterT (aux e1))
+                  if (simplified && (inline_match || not (containsMatch e2))) || atomic func_body
+                  then hooray $ return e2
+                  else return (Gbl gbl :@: ts)
+            _ -> return (Gbl gbl :@: ts)
+
+        _ -> return e0
+
+    inlineable body var val = should_inline mscp val || occurrences var body <= 1
+    mscp = fmap scope mthy
+
+    isRecursiveGroup [fun] = defines fun `elem` uses fun
+    isRecursiveGroup _     = True
+
+    inlinings =
+      case mthy of
+        Nothing -> Map.empty
+        Just Theory{..} ->
+          Map.fromList . map (\fun -> (func_name fun, fun)) .
+          concat . filter (not . isRecursiveGroup) . topsort $ thy_funcs
+
+    containsMatch e = not (null [ e' | e'@Match{} <- universe e ])
+
+    new /// old = transformExprM $ \e ->
+      if e == Lcl old then hooray $ lift (freshen new) else return e
+
+    hooray x = do
+      tell (Any True)
+      x
+
+    boo x = censor (const (Any False)) x
+
+isConstructor :: Name a => Maybe (Scope a) -> Head a -> Bool
+isConstructor _ (Builtin Lit{}) = True
+isConstructor mscp (Gbl gbl) = isJust $ do
+  scp <- mscp
+  lookupConstructor (gbl_name gbl) scp
+isConstructor _ _ = False
diff --git a/src/Tip/Types.hs b/src/Tip/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Types.hs
@@ -0,0 +1,256 @@
+-- | The abstract syntax
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, PatternGuards #-}
+{-# LANGUAGE ExplicitForAll, FlexibleContexts, FlexibleInstances, TemplateHaskell, MultiParamTypeClasses #-}
+module Tip.Types where
+
+import Data.Generics.Geniplate
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable)
+import Data.Monoid
+
+data Head a
+  = Gbl (Global a)
+  | Builtin Builtin
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Local a = Local { lcl_name :: a, lcl_type :: Type a }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Global a = Global
+  { gbl_name      :: a
+  , gbl_type      :: PolyType a
+  , gbl_args      :: [Type a]
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+infix 5 :@:
+
+data Expr a
+  -- maybe move Lit from Builtin under Head to straight here
+  = Head a :@: [Expr a]
+  | Lcl (Local a)
+  | Lam [Local a] (Expr a)
+  -- Merge with Quant?
+  | Match (Expr a) [Case a]
+  -- ^ The default case comes first if there is one
+  | Let (Local a) (Expr a) (Expr a)
+  -- Allow a list of bound variables, like in SMT-LIB?
+  | Quant QuantInfo Quant [Local a] (Expr a)
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Quant = Forall | Exists
+  deriving (Eq,Ord,Show)
+
+data QuantInfo = NoInfo
+  deriving (Eq,Ord,Show)
+
+data Case a = Case { case_pat :: Pattern a, case_rhs :: Expr a }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Builtin
+  = At
+  | Lit Lit
+  | And
+  | Or
+  | Not
+  | Implies
+  | Equal
+  | Distinct
+  | IntAdd
+  | IntSub
+  | IntMul
+  | IntDiv
+  | IntMod
+  | IntGt
+  | IntGe
+  | IntLt
+  | IntLe
+  deriving (Eq,Ord,Show)
+
+intBuiltin :: Builtin -> Bool
+intBuiltin b = b `elem` [IntAdd,IntSub,IntMul,IntDiv,IntMod,IntGt,IntGe,IntLt,IntLe]
+
+litBuiltin :: Builtin -> Bool
+litBuiltin Lit{} = True
+litBuiltin _     = False
+
+eqRelatedBuiltin :: Builtin -> Bool
+eqRelatedBuiltin b = b `elem` [Equal,Distinct]
+
+logicalBuiltin :: Builtin -> Bool
+logicalBuiltin b = b `elem` [And,Or,Implies,Equal,Distinct,Not]
+
+data Lit
+  = Int Integer
+  | Bool Bool
+  | String String -- Not really here but might come from GHC
+  deriving (Eq,Ord,Show)
+
+-- | Patterns in branches
+data Pattern a
+  = Default
+  | ConPat { pat_con  :: Global a, pat_args :: [Local a] }
+  | LitPat Lit
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+-- | Polymorphic types
+data PolyType a =
+  PolyType
+    { polytype_tvs  :: [a]
+    , polytype_args :: [Type a]
+    , polytype_res  :: Type a
+    }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+-- | Types
+data Type a
+  = TyVar a
+  | TyCon a [Type a]
+  | [Type a] :=>: Type a
+  | BuiltinType BuiltinType
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data BuiltinType
+  = Integer | Boolean
+  deriving (Eq,Ord,Show)
+
+data Function a = Function
+  { func_name :: a
+  , func_tvs  :: [a]
+  , func_args :: [Local a]
+  , func_res  :: Type a
+  , func_body :: Expr a
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+-- | Uninterpreted function
+data Signature a = Signature
+  { sig_name :: a
+  , sig_type :: PolyType a
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+-- | Uninterpreted sort
+data Sort a = Sort
+  { sort_name :: a
+  , sort_arity :: Int }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+-- | Data definition
+data Datatype a = Datatype
+  { data_name :: a
+  , data_tvs  :: [a]
+  , data_cons :: [Constructor a]
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Constructor a = Constructor
+  { con_name    :: a
+  , con_discrim :: a
+  , con_args    :: [(a,Type a)]
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Theory a = Theory
+  { thy_datatypes   :: [Datatype a]
+  , thy_sorts       :: [Sort a]
+  , thy_sigs        :: [Signature a]
+  , thy_funcs       :: [Function a]
+  , thy_asserts     :: [Formula a]
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+emptyTheory :: Theory a
+emptyTheory = Theory [] [] [] [] []
+
+joinTheories :: Theory a -> Theory a -> Theory a
+joinTheories (Theory a o e u i) (Theory s n t h d) = Theory (a++s) (o++n) (e++t) (u++h) (i++d)
+
+instance Monoid (Theory a) where
+  mempty  = emptyTheory
+  mappend = joinTheories
+
+data Formula a = Formula
+  { fm_role :: Role
+  , fm_tvs  :: [a]
+  -- ^ top-level quantified type variables
+  , fm_body :: Expr a
+  }
+  deriving (Eq,Ord,Show,Functor,Foldable,Traversable)
+
+data Role = Assert | Prove
+  deriving (Eq,Ord,Show)
+
+instanceUniverseBi [t| forall a . (Expr a,Expr a) |]
+instanceUniverseBi [t| forall a . (Function a,Expr a) |]
+instanceUniverseBi [t| forall a . (Function a,Global a) |]
+instanceUniverseBi [t| forall a . (Function a,Type a) |]
+instanceUniverseBi [t| forall a . (Datatype a,Type a) |]
+instanceUniverseBi [t| forall a . (Expr a,Pattern a) |]
+instanceUniverseBi [t| forall a . (Expr a,Local a) |]
+instanceUniverseBi [t| forall a . (Expr a,Global a) |]
+instanceUniverseBi [t| forall a . (Theory a,Expr a) |]
+instanceUniverseBi [t| forall a . (Theory a,Type a) |]
+instanceUniverseBi [t| forall a . (Type a,Type a) |]
+instanceUniverseBi [t| forall a . (Theory a,Constructor a) |]
+instanceUniverseBi [t| forall a . (Theory a,Global a) |]
+instanceUniverseBi [t| forall a . (Theory a,Builtin) |]
+instanceTransformBi [t| forall a . (Expr a,Expr a) |]
+instanceTransformBi [t| forall a . (a,Expr a) |]
+instanceTransformBi [t| forall a . (a,Formula a) |]
+instanceTransformBi [t| forall a . (Expr a,Function a) |]
+instanceTransformBi [t| forall a . (Expr a,Theory a) |]
+instanceTransformBi [t| forall a . (Head a,Expr a) |]
+instanceTransformBi [t| forall a . (Head a,Theory a) |]
+instanceTransformBi [t| forall a . (Local a,Expr a) |]
+instanceTransformBi [t| forall a . (Pattern a,Expr a) |]
+instanceTransformBi [t| forall a . (Pattern a,Theory a) |]
+instanceTransformBi [t| forall a . (Type a,Theory a) |]
+instanceTransformBi [t| forall a . (Type a,Expr a) |]
+instanceTransformBi [t| forall a . (Type a,Type a) |]
+instance Monad m => TransformBiM m (Expr a) (Expr a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Expr a -> m (Expr a) |])
+instance Monad m => TransformBiM m (Expr a) (Function a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Function a -> m (Function a) |])
+instance Monad m => TransformBiM m (Pattern a) (Expr a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Pattern a -> m (Pattern a)) -> Expr a -> m (Expr a) |])
+instance Monad m => TransformBiM m (Local a) (Expr a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Local a -> m (Local a)) -> Expr a -> m (Expr a) |])
+instance Monad m => TransformBiM m (Expr a) (Theory a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Theory a -> m (Theory a) |])
+instance Monad m => TransformBiM m (Expr a) (Formula a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Expr a -> m (Expr a)) -> Formula a -> m (Formula a) |])
+instance Monad m => TransformBiM m (Type a) (Type a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Type a -> m (Type a)) -> Type a -> m (Type a) |])
+instance Monad m => TransformBiM m (Function a) (Theory a) where
+  {-# INLINE transformBiM #-}
+  transformBiM = $(genTransformBiM' [t| forall m a . (Function a -> m (Function a)) -> Theory a -> m (Theory a) |])
+
+transformExpr :: (Expr a -> Expr a) -> Expr a -> Expr a
+transformExpr = transformBi
+
+transformExprM :: Monad m => (Expr a -> m (Expr a)) -> Expr a -> m (Expr a)
+transformExprM = transformBiM
+
+transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a
+transformExprIn = transformBi
+
+transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a)
+transformExprInM = transformBiM
+
+transformType :: (Type a -> Type a) -> Type a -> Type a
+transformType = transformBi
+
+transformTypeInExpr :: (Type a -> Type a) -> Expr a -> Expr a
+transformTypeInExpr =
+  $(genTransformBiT' [[t|PolyType|]] [t|forall a. (Type a -> Type a) -> Expr a -> Expr a|])
+
+
+
diff --git a/src/Tip/Utils.hs b/src/Tip/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Utils.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Handy utilities
+module Tip.Utils where
+
+import Data.List
+import Data.Graph
+import Data.List.Split
+import Data.Char
+import Data.Foldable (Foldable)
+import qualified Data.Foldable as F
+import Data.Ord
+
+-- | Sort and remove duplicates
+usort :: Ord a => [a] -> [a]
+usort = map head . group . sort
+
+-- | Sort things in topologically in strongly connected components
+sortThings :: Ord name => (thing -> name) -> (thing -> [name]) -> [thing] -> [[thing]]
+sortThings name refers things =
+    map flattenSCC $ stronglyConnComp
+        [ (thing,name thing,filter (`elem` names) (refers thing))
+        | thing <- things
+        ]
+  where
+    names = map name things
+
+-- | Makes a nice flag from a constructor string
+--
+-- > > flagify "PrintPolyFOL"
+-- > "print-poly-fol"
+flagify :: String -> String
+flagify
+    = map toLower . intercalate "-"
+    . split (condense $ dropInitBlank $ keepDelimsL $ whenElt (\x -> isUpper x || isSpace x))
+
+-- | Makes a flag from something @Show@-able
+flagifyShow :: Show a => a -> String
+flagifyShow = flagify . show
+
+-- | Calculates the maximum value of a foldable value.
+--
+-- Useful to find the highest unique in a structure
+maximumOn :: forall f a b . (F.Foldable f,Ord b) => (a -> b) -> f a -> b
+maximumOn f = f . F.maximumBy (comparing f)
+
diff --git a/src/Tip/Utils/Rename.hs b/src/Tip/Utils/Rename.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Utils/Rename.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE ViewPatterns, FlexibleContexts #-}
+module Tip.Utils.Rename where
+
+import Control.Monad.State
+import Control.Monad.Reader
+
+import Data.Traversable (Traversable)
+import qualified Data.Traversable as T
+
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+
+import Data.Maybe (fromMaybe)
+import Data.List (find)
+
+import Control.Arrow
+
+import Unsafe.Coerce
+
+type RenameM a b = ReaderT (Suggestor a b) (State (Map a b,Set b))
+
+type Suggestor a b = a -> [b]
+
+disambig :: (a -> String) -> Suggestor a String
+disambig f (f -> x) = x : extra x ++ [ x ++ show (i :: Int) | i <- [2..] ]
+  where
+    extra x = fromMaybe [] (find (x `elem`) families)
+
+    families =
+       [ ["a","b","c"]
+       , ["f","g","h"]
+       , ["p","q"]
+       , ["n","m","o"]
+       , ["x","y","z"]
+       , ["xs","ys","zs"]
+       ]
+
+disambig2 :: (a -> String) -> (b -> String) -> Suggestor (Either a b) String
+disambig2 f _ (Left a)  = disambig f a
+disambig2 _ g (Right b) = disambig g b
+
+evalRenameM :: (Ord b) => Suggestor a b -> [b] -> RenameM a b r -> r
+evalRenameM f block m = fst (runRenameM f block M.empty m)
+
+runRenameM :: (Ord b) => Suggestor a b -> [b] -> Map a b -> RenameM a b r -> (r,Map a b)
+runRenameM f block alloc m = second fst (runState (runReaderT m f) s0)
+  where s0 = (alloc,S.fromList (block ++ M.elems alloc))
+
+insert :: (Ord a,Ord b) => a -> RenameM a b b
+insert n = go 0 =<< asks ($ n)
+  where
+    go i (s:ss) = do
+        u <- gets snd
+        if s `S.member` u then go (i+1) ss else do
+            modify (M.insert n s *** S.insert s)
+            return s
+    go i [] = error "ran out of names!?"
+
+insertMany :: (Ord a,Ord b) => [a] -> RenameM a b [b]
+insertMany = mapM insert
+
+lkup :: (Ord a,Ord b) => a -> RenameM a b b
+lkup n = do
+    m_s <- gets (M.lookup n . fst)
+    case m_s of
+        Just s  -> return s
+        Nothing -> insert n
+
+rename :: (Ord a,Ord b,Traversable t) => t a -> RenameM a b (t b)
+rename = T.mapM lkup
+
+renameWith :: (Ord a,Ord b,Traversable t) => Suggestor a b -> t a -> t b
+renameWith = renameWithBlocks []
+
+renameWithBlocks :: (Ord a,Ord b,Traversable t) => [b] -> Suggestor a b -> t a -> t b
+renameWithBlocks bs f = evalRenameM f bs . rename
+
diff --git a/src/Tip/WorkerWrapper.hs b/src/Tip/WorkerWrapper.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/WorkerWrapper.hs
@@ -0,0 +1,50 @@
+-- Generic support for the worker-wrapper transform.
+{-# LANGUAGE PatternGuards, RecordWildCards #-}
+module Tip.WorkerWrapper where
+
+import Tip.Core
+import Tip.Fresh
+import Tip.Simplify
+import qualified Data.Map as Map
+import Data.Maybe
+
+data WorkerWrapper a = WorkerWrapper
+  { ww_func :: Function a                           -- ^ The function to transform
+  , ww_args :: [Local a]                            -- ^ New function argument type
+  , ww_res  :: Type a                               -- ^ New function result type
+  , ww_def  :: Expr a -> Expr a                     -- ^ Transform function body
+  , ww_use  :: Head a -> [Expr a] -> Fresh (Expr a) -- ^ Transform call to function
+  }
+
+workerWrapperTheory :: Name a => (Theory a -> Fresh [WorkerWrapper a]) -> Theory a -> Fresh (Theory a)
+workerWrapperTheory f thy = do
+  ww <- f thy
+  case ww of
+    [] -> return thy
+    _ -> workerWrapper ww thy >>= workerWrapperTheory f
+
+workerWrapperFunctions :: Name a => (Function a -> Maybe (Fresh (WorkerWrapper a))) -> Theory a -> Fresh (Theory a)
+workerWrapperFunctions f =
+  workerWrapperTheory (sequence . catMaybes . map f . thy_funcs)
+
+workerWrapper :: Name a => [WorkerWrapper a] -> Theory a -> Fresh (Theory a)
+workerWrapper wws thy@Theory{..} =
+  transformExprInM updateUse thy' >>= simplifyTheory gently
+  where
+    thy' = thy { thy_funcs = map updateDef thy_funcs }
+    m = Map.fromList [(func_name (ww_func ww), ww) | ww <- wws]
+    updateDef func@Function{..} =
+      case Map.lookup func_name m of
+        Nothing -> func
+        Just WorkerWrapper{..} ->
+          func {
+            func_args = ww_args, func_res = ww_res,
+            func_body = ww_def func_body
+          }
+    updateUse (Gbl gbl :@: args)
+      | Just WorkerWrapper{ww_func=Function{..}, ..} <- Map.lookup (gbl_name gbl) m =
+          let gbl_type = PolyType { polytype_tvs = func_tvs,
+                                    polytype_args = map lcl_type ww_args,
+                                    polytype_res = ww_res}
+          in ww_use (Gbl gbl{gbl_type = gbl_type}) args
+    updateUse e = return e
diff --git a/src/Tip/Writer.hs b/src/Tip/Writer.hs
new file mode 100644
--- /dev/null
+++ b/src/Tip/Writer.hs
@@ -0,0 +1,46 @@
+-- A faster implementation of the writer monad.
+
+{-# LANGUAGE Rank2Types #-}
+module Tip.Writer where
+
+import Data.Monoid
+
+import Control.Monad
+import Control.Applicative
+
+newtype WriterT w m a = WriterT { unWriterT :: forall b. (w -> a -> m b) -> m b }
+
+instance (Monoid w, Monad m) => Functor (WriterT w m) where
+  {-# INLINE fmap #-}
+  fmap f x = x >>= return . f
+
+instance (Monoid w, Monad m) => Applicative (WriterT w m) where
+  {-# INLINE pure #-}
+  pure = return
+  {-# INLINE (<*>) #-}
+  (<*>) = liftM2 ($)
+
+instance (Monoid w, Monad m) => Monad (WriterT w m) where
+  {-# INLINE return #-}
+  return x = WriterT (\k -> k mempty x)
+
+  {-# INLINE (>>=) #-}
+  WriterT m >>= f =
+    WriterT $ \k ->
+      m (\w x -> unWriterT (f x) (\w' y -> k (w `mappend` w') y))
+
+{-# INLINE runWriterT #-}
+runWriterT :: (Monoid w, Monad m) => WriterT w m a -> m (a, w)
+runWriterT (WriterT f) = f (\w x -> return (x, w))
+
+{-# INLINE tell #-}
+tell :: (Monoid w, Monad m) => w -> WriterT w m ()
+tell w = WriterT (\k -> k w ())
+
+{-# INLINE lift #-}
+lift :: (Monoid w, Monad m) => m a -> WriterT w m a
+lift x = WriterT (\k -> x >>= \y -> k mempty y)
+
+{-# INLINE censor #-}
+censor :: (Monoid w, Monad m) => (w -> w) -> WriterT w m a -> WriterT w m a
+censor f (WriterT m) = WriterT (\k -> m (\w x -> k (f w) x))
diff --git a/tip-lib.cabal b/tip-lib.cabal
new file mode 100644
--- /dev/null
+++ b/tip-lib.cabal
@@ -0,0 +1,88 @@
+name:                tip-lib
+version:             0.1
+synopsis:            tons of inductive problems - support library and tools
+description:         This package provides a tool for processing inductive theorem proving problems in TIP format (see the homepage for details).
+homepage:            http://tip-org.github.io
+bug-reports:         http://github.com/tip-org/tools/issues
+license:             BSD3
+license-file:        LICENSE
+author:              Dan Rosén, Nick Smallbone
+maintainer:          danr@chalmers.se
+category:            Theorem Provers
+build-type:          Simple
+cabal-version:       >=1.10
+
+source-repository head
+  type:     git
+  location: http://github.com/tip-org/tools
+
+library
+  exposed-modules:
+    Tip.Core
+    Tip.Lint
+    Tip.Types
+    Tip.Scope
+    Tip.Fresh
+    Tip.WorkerWrapper
+    Tip.Simplify
+    Tip.Passes
+    Tip.Pretty
+    Tip.Pretty.SMT
+    Tip.Pretty.Why3
+    Tip.Pretty.Isabelle
+    Tip.Pretty.Haskell
+
+    Tip.Parser
+
+    Tip.Utils
+    Tip.Writer
+
+    Tip.Rename
+    Tip.Utils.Rename
+    Tip.Haskell.Repr
+    Tip.Haskell.Translate
+    Tip.Haskell.Rename
+    Tip.CallGraph
+  other-modules:
+    Tip.Pass.AxiomatizeFuncdefs
+    Tip.Pass.Lift
+    Tip.Pass.Booleans
+    Tip.Pass.CommuteMatch
+    Tip.Pass.AddMatch
+    Tip.Pass.CSEMatch
+    Tip.Pass.RemoveNewtype
+    Tip.Pass.RemoveMatch
+    Tip.Pass.NegateConjecture
+    Tip.Pass.EqualFunctions
+    Tip.Pass.Uncurry
+    Tip.Pass.Pipeline
+    Tip.Pass.EliminateDeadCode
+    Tip.Pass.FillInCases
+
+    Tip.Parser.ErrM
+    Tip.Parser.AbsTIP
+    Tip.Parser.LexTIP
+    Tip.Parser.ParTIP
+    Tip.Parser.Convert
+
+  hs-source-dirs:      src
+  include-dirs:        src
+  ghc-options:         -w
+  default-language:    Haskell2010
+  build-depends:       base >=4 && <5,
+                       geniplate-mirror >=0.7.1,
+                       split,
+                       containers,
+                       mtl,
+                       pretty,
+                       array,
+                       optparse-applicative
+
+executable tip
+  main-is:             executable/Main.hs
+  default-language:    Haskell2010
+  build-depends:       base,
+                       tip-lib,
+                       pretty-show,
+                       pretty,
+                       optparse-applicative