diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2014 Eric Seidel
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
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/bench/Main.hs b/bench/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/Main.hs
@@ -0,0 +1,227 @@
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings     #-}
+{-# LANGUAGE RecordWildCards       #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+module Main where
+
+import           Test.Target
+import qualified Test.QuickCheck            as QC
+import qualified Test.SmallCheck            as SC
+import qualified Test.SmallCheck.Drivers    as SC
+
+import           Control.Applicative
+import           Control.Concurrent.Timeout
+import           Control.Exception
+import           Control.Monad
+import qualified Data.ByteString            as B
+import qualified Data.ByteString.Char8      as B8
+import qualified Data.ByteString.Lazy       as LB
+import           Data.Csv
+import qualified Data.List                  as L
+import           Data.IORef
+import           Data.Monoid
+import           Data.Time.Clock.POSIX
+import           Data.Timeout
+import qualified Data.Vector                as V
+import           System.IO
+import           Text.Printf
+
+-- import qualified Expr
+-- import qualified ExprBench                  as Expr
+import qualified List
+import qualified ListBench                  as List
+import qualified Map                        as Map
+import qualified MapBench                   as Map
+import qualified RBTree
+import qualified RBTreeBench                as RBTree
+import qualified XMonad.Properties          as XMonad
+
+import qualified LazySmallCheck             as LSC
+
+data Outcome = TimeOut
+             | Complete !Int
+             | GaveUp !Int
+             deriving (Read, Show)
+
+data TestResult
+  = TestResult { testName :: !String
+               , liquid :: ![(Int,Double,Outcome)]
+               , small  :: ![(Int,Double,Outcome)]
+               , lazysmall  :: ![(Int,Double,Outcome)]
+               , lazysmall_slow :: !(Maybe [(Int,Double,Outcome)])
+               , quick  :: !(Double,Outcome)
+               } deriving (Read, Show)
+
+testResultRecords :: TestResult -> [NamedRecord]
+testResultRecords (TestResult name l s ls lss _)
+  = [ namedRecord $ [ "Benchmark" .= B8.pack name
+                    , "Tool"      .= B8.pack "Target" ]
+                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d l ]
+    , namedRecord $ [ "Benchmark" .= B8.pack name
+                    , "Tool"      .= B8.pack "SmallCheck" ]
+                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d s ]
+    , namedRecord $ [ "Benchmark" .= B8.pack name
+                    , "Tool"      .= B8.pack "Lazy-SmallCheck" ]
+                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ls ]
+    ]
+   ++ maybe [] (\ss ->
+    [ namedRecord $ [ "Benchmark" .= B8.pack name
+                    , "Tool"      .= B8.pack "Lazy-SmallCheck-slow" ]
+                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ss ]
+    ]) lss
+
+bshow :: Show a => a -> B.ByteString
+bshow = B8.pack . show
+
+lookup3 :: Int -> [(Int,Double,Outcome)] -> (Double,Outcome)
+lookup3 x xs = case L.find (\(a,b,c) -> a == x) xs of
+                 Nothing -> (0, TimeOut)
+                 Just (i,d,o) -> (d,o)
+
+toResult :: Double -> Outcome -> B.ByteString
+toResult d TimeOut      = "X"
+toResult d (Complete i) = bshow d
+
+header :: V.Vector B.ByteString
+header = V.fromList $ ["Benchmark", "Tool"] ++ [bshow d | d <- [2..20]]
+
+logCsv f r = withFile f WriteMode $ \h -> do
+  LB.hPutStr h $ encodeByName header $ testResultRecords r
+  return r
+
+main :: IO ()
+main = do
+  print =<< logCsv "bench/List.insert.csv"       =<< listInsertTests
+  print =<< logCsv "bench/RBTree.add.csv"        =<< rbTreeAddTests
+  -- print =<< logCsv "bench/Expr.subst.csv"        =<< exprSubstTests
+  print =<< logCsv "bench/Map.delete.csv"        =<< mapDeleteTests
+  print =<< logCsv "bench/Map.difference.csv"    =<< mapDifferenceTests
+  print =<< logCsv "bench/XMonad.focus_left.csv" =<< xmonadFocusLeftTests
+
+listInsertTests = do
+  let n = 'List.insert
+  l <- checkTarget List.insert         n "examples/List.hs"
+  s <- checkSmall  List.prop_insert_sc n
+  ls <- checkLazySmall  List.prop_insert_lsc n
+  q <- checkQuick  List.prop_insert_qc n
+  return $ TestResult (show n) l s ls Nothing q
+
+rbTreeAddTests = do
+  let n = 'RBTree.add
+  l <- checkTarget RBTree.prop_add_lc n "examples/RBTree.hs"
+  s <- checkSmall  RBTree.prop_add_sc n
+  ls <- checkLazySmall  RBTree.prop_add_lsc n
+  lss <- checkLazySmall  RBTree.prop_add_lsc_slow n
+  q <- checkQuick  RBTree.prop_add_qc n
+  return $ TestResult (show n) l s ls (Just lss) q
+
+-- exprSubstTests = do
+--   l <- checkTarget Expr.subst         "Expr.subst" "examples/Expr.hs"
+--   s <- checkSmall  Expr.prop_subst_sc "Expr.subst"
+--   ls <- checkLazySmall  Expr.prop_subst_lsc "Expr.subst"
+--   q <- checkQuick  Expr.prop_subst_qc "Expr.subst"
+--   return $ TestResult "Expr.subst" l s ls Nothing q
+
+mapDeleteTests = do
+  let n = 'Map.delete
+  l <- checkTarget Map.prop_delete_lc n "examples/Map.hs"
+  s <- checkSmall  Map.prop_delete_sc n
+  ls <- checkLazySmall  Map.prop_delete_lsc n
+  lss <- checkLazySmall  Map.prop_delete_lsc_slow n
+  q <- checkQuick  Map.prop_delete_qc n
+  return $ TestResult (show n) l s ls (Just lss) q
+
+mapDifferenceTests = do
+  let n = 'Map.difference
+  l <- checkTarget Map.prop_difference_lc n "examples/Map.hs"
+  s <- checkSmall  Map.prop_difference_sc n
+  ls <- checkLazySmall  Map.prop_difference_lsc n
+  lss <- checkLazySmall  Map.prop_difference_lsc_slow n
+  q <- checkQuick  Map.prop_difference_qc n
+  return $ TestResult (show n) l s ls (Just lss) q
+
+xmonadFocusLeftTests = do
+  let n = 'XMonad.prop_focus_left_master_lc
+  l <- checkTarget XMonad.prop_focus_left_master_lc n "examples/XMonad/Properties.hs"
+  s <- checkSmall  XMonad.prop_focus_left_master_sc n
+  ls <- checkLazySmall  XMonad.prop_focus_left_master_lsc n
+  q <- checkQuick  XMonad.prop_focus_left_master_qc n
+  return $ TestResult (show n) l s ls Nothing q
+
+
+myTimeout :: IO a -> IO (Maybe a)
+myTimeout = timeout (60 # Minute)
+
+getTime :: IO Double
+getTime = realToFrac `fmap` getPOSIXTime
+
+timed x = do start <- getTime
+             v     <- x
+             end   <- getTime
+             return (end-start, v)
+
+resultPassed (Passed i) = i
+
+-- checkTarget :: CanTest f => f -> String -> FilePath -> IO [(Int,Double,Outcome)]
+checkTarget f n m = checkMany (show n++"/Target")
+                              (\d max -> resultPassed <$>
+                                         targetResultWith f n m (mkOpts d max))
+  where mkOpts d max = defaultOpts { depth = d, maxSuccess = Just max, scDepth = True }
+
+checkSmall p n = checkMany (show n++"/SmallCheck")
+                           (\d n -> fromIntegral.fst.fst <$> runTestWithStats d n (p d))
+
+checkLazySmall p n = checkMany (show n++"/LazySmallCheck")
+                               (\d n -> LSC.depthCheckResult d n (p d))
+
+-- checkQuick :: QC.Testable f => f -> String -> IO (Double,Outcome)
+checkQuick p n = timed $ do
+  putStrNow $ printf "Testing %s/QuickCheck.. " (show n)
+  r <- QC.quickCheckWithResult (QC.stdArgs {QC.chatty = False}) p
+  putStrNow "done!\n"
+  return $ case r of
+             QC.Success {..} -> Complete numTests
+             QC.GaveUp {..}  -> GaveUp numTests
+
+checkMany :: String -> (Int -> Int -> IO Int) -> IO [(Int, Double, Outcome)]
+checkMany name bench = do
+  putStrNow $ printf "Testing %s.. " name
+  r <- go 2
+  putStrNow "done!\n"
+  return r
+  where
+    go n  
+      | n > 20
+      = return []
+      | otherwise
+      = putStrNow (printf "%d " n) >> timed (myTimeout (bench n 1000)) >>= \case
+              (d,Nothing) -> return [(n,d,TimeOut)]
+              (d,Just i)  -> ((n,d,Complete i):) <$> go (n+1)
+
+
+putStrNow s = putStr s >> hFlush stdout
+
+runTestWithStats :: SC.Testable IO a => SC.Depth -> Int -> a
+                 -> IO ((Integer,Integer), Maybe SC.PropertyFailure)
+runTestWithStats d n prop = do
+  good <- newIORef 0
+  bad <- newIORef 0
+
+  let
+    hook SC.GoodTest = do modifyIORef' good (+1)
+                          n' <- readIORef good
+                          when (n' == fromIntegral n) $ throw ()
+    hook SC.BadTest  = modifyIORef' bad (+1)
+
+  r <- SC.smallCheckWithHook d hook prop `catch` \() -> return Nothing
+
+  goodN <- readIORef good
+  badN  <- readIORef bad
+
+  return ((goodN, badN), r)
+
+-- instance Exception ()
diff --git a/cbits/fpstring.c b/cbits/fpstring.c
new file mode 100644
--- /dev/null
+++ b/cbits/fpstring.c
@@ -0,0 +1,82 @@
+/*
+ * Copyright (c) 2003 David Roundy
+ * Copyright (c) 2005-6 Don Stewart
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. 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.
+ * 3. Neither the names of the authors or the names of any contributors
+ *    may be used to endorse or promote products derived from this software
+ *    without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE REGENTS 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 AUTHORS 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.
+ */
+
+#include "fpstring.h"
+
+/* copy a string in reverse */
+void fps_reverse(unsigned char *q, unsigned char *p, unsigned long n) {
+    p += n-1;
+    while (n-- != 0)
+        *q++ = *p--;
+}
+
+/* duplicate a string, interspersing the character through the elements
+   of the duplicated string */
+void fps_intersperse(unsigned char *q,
+                     unsigned char *p,
+                     unsigned long n,
+                     unsigned char c) {
+
+    while (n > 1) {
+        *q++ = *p++;
+        *q++ = c;
+        n--;
+    }
+    if (n == 1)
+        *q = *p;
+}
+
+/* find maximum char in a packed string */
+unsigned char fps_maximum(unsigned char *p, unsigned long len) {
+    unsigned char *q, c = *p;
+    for (q = p; q < p + len; q++)
+        if (*q > c)
+            c = *q;
+    return c;
+}
+
+/* find minimum char in a packed string */
+unsigned char fps_minimum(unsigned char *p, unsigned long  len) {
+    unsigned char *q, c = *p;
+    for (q = p; q < p + len; q++)
+        if (*q < c)
+            c = *q;
+    return c;
+}
+
+/* count the number of occurences of a char in a string */
+unsigned long fps_count(unsigned char *p, unsigned long len, unsigned char w) {
+    unsigned long c;
+    for (c = 0; len-- != 0; ++p)
+        if (*p == w)
+            ++c;
+    return c;
+}
diff --git a/src/Test/Target.hs b/src/Test/Target.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE ViewPatterns #-}
+module Test.Target
+  ( target, targetResult, targetWith, targetResultWith
+  -- , targetTH
+  , Result(..), Testable
+  , TargetOpts(..), defaultOpts
+  , Test(..)
+  ) where
+
+import           Control.Applicative
+import           Control.Monad
+import           Control.Monad.Catch
+import           Control.Monad.State
+import qualified Language.Haskell.TH             as TH
+import           System.Process                  (terminateProcess)
+import           Text.Printf                     (printf)
+
+import           Language.Fixpoint.Names
+import           Language.Fixpoint.SmtLib2       hiding (verbose)
+
+import           Test.Target.Monad
+import           Test.Target.Targetable ()
+import           Test.Target.Targetable.Function ()
+import           Test.Target.Testable
+import           Test.Target.Types
+import           Test.Target.Util
+
+-- | Test whether a function inhabits its refinement type by enumerating valid
+-- inputs and calling the function.
+target :: Testable f
+       => f -- ^ the function
+       -> TH.Name -- ^ the name of the function
+       -> FilePath -- ^ the path to the module that defines the function
+       -> IO ()
+target f name path
+  = targetWith f name path defaultOpts
+
+-- targetTH :: TH.ExpQ -- (TH.TExp (Testable f => f -> TH.Name -> IO ()))
+-- targetTH = TH.location >>= \TH.Loc {..} ->
+--   [| \ f n -> target f (show n) loc_filename |]
+
+-- | Like 'target', but returns the 'Result' instead of printing to standard out.
+targetResult :: Testable f => f -> TH.Name -> FilePath -> IO Result
+targetResult f name path
+  = targetResultWith f name path defaultOpts
+
+-- | Like 'target', but accepts options to control the enumeration depth,
+-- solver, and verbosity.
+targetWith :: Testable f => f -> TH.Name -> FilePath -> TargetOpts -> IO ()
+targetWith f name path opts
+  = do res <- targetResultWith f name path opts
+       case res of
+         Passed n -> printf "OK. Passed %d tests\n\n" n
+         Failed x -> printf "Found counter-example: %s\n\n" x
+         Errored x -> printf "Error! %s\n\n" x
+
+-- | Like 'targetWith', but returns the 'Result' instead of printing to standard out.
+targetResultWith :: Testable f => f -> TH.Name -> FilePath -> TargetOpts -> IO Result
+targetResultWith f (show -> name) path opts
+  = do when (verbose opts) $
+         printf "Testing %s\n" name
+       sp  <- getSpec path
+       ctx <- mkContext (solver opts)
+       runTarget opts (initState path sp ctx) (do
+         ty <- safeFromJust "targetResultWith" . lookup (symbol name) <$> gets sigs
+         test f ty)
+        `finally` killContext ctx
+  where
+    mkContext = if logging opts then makeContext else makeContextNoLog
+    killContext ctx = terminateProcess (pId ctx) >> cleanupContext ctx
+
+data Test = forall t. Testable t => T t
diff --git a/src/Test/Target/Eval.hs b/src/Test/Target/Eval.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Eval.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Test.Target.Eval ( eval, evalWith ) where
+
+import           Control.Arrow                   (second)
+import           Control.Applicative
+import           Control.Monad.Catch
+import           Control.Monad.State
+import qualified Data.HashMap.Strict             as M
+import           Data.List
+import           Data.Maybe
+import           Text.Printf
+
+import qualified GHC
+import           Language.Fixpoint.SmtLib2
+import           Language.Fixpoint.Types         hiding (R)
+import           Language.Haskell.Liquid.Types   hiding (var)
+
+import           Test.Target.Expr
+import           Test.Target.Monad
+import           Test.Target.Types
+
+-- import           Debug.Trace
+
+-- | Evaluate a refinement with the given expression substituted for the value
+-- variable.
+eval :: Reft -> Expr -> Target Bool
+eval r e = do
+  cts <- gets freesyms
+  evalWith (M.fromList $ map (second (`app` [])) cts) r e
+
+-- | Evaluate a refinement with the given expression substituted for the value
+-- variable, in the given environment of free symbols.
+evalWith :: M.HashMap Symbol Expr -> Reft -> Expr -> Target Bool
+evalWith m (Reft (v, rs)) x
+  = and <$> sequence [ evalPred p (M.insert v x m) | RConc p <- rs ]
+
+evalPred :: Pred -> M.HashMap Symbol Expr -> Target Bool
+evalPred PTrue           _ = return True
+evalPred PFalse          _ = return False
+evalPred (PAnd ps)       m = and <$> sequence [evalPred p m | p <- ps]
+evalPred (POr ps)        m = or  <$> sequence [evalPred p m | p <- ps]
+evalPred (PNot p)        m = not <$> evalPred p m
+evalPred (PImp p q)      m = do pv <- evalPred p m
+                                if pv
+                                   then evalPred q m
+                                   else return True
+evalPred (PIff p q)      m = and <$> sequence [ evalPred (p `imp` q) m
+                                              , evalPred (q `imp` p) m
+                                              ]
+evalPred (PAtom b e1 e2) m = evalBrel b <$> evalExpr e1 m <*> evalExpr e2 m
+evalPred (PBexp e)       m = (==0) <$> evalExpr e m
+evalPred p               _ = throwM $ EvalError $ "evalPred: " ++ show p
+-- evalPred (PAll ss p)     m = undefined
+-- evalPred PTop            m = undefined
+
+evalBrel :: Brel -> Expr -> Expr -> Bool
+evalBrel Eq = (==)
+evalBrel Ne = (/=)
+evalBrel Ueq = (==)
+evalBrel Une = (/=)
+evalBrel Gt = (>)
+evalBrel Ge = (>=)
+evalBrel Lt = (<)
+evalBrel Le = (<=)
+
+applyMeasure :: Measure SpecType GHC.DataCon -> Expr -> M.HashMap Symbol Expr -> Target Expr
+applyMeasure m (EApp c xs) env
+  = meq >>= \eq -> evalBody eq xs env
+  where
+    ct = symbolString $ case val c of
+      "GHC.Types.[]" -> "[]"
+      "GHC.Types.:"  -> ":"
+      "GHC.Tuple.(,)" -> "(,)"
+      "GHC.Tuple.(,,)" -> "(,,)"
+      "GHC.Tuple.(,,,)" -> "(,,,)"
+      "GHC.Tuple.(,,,,)" -> "(,,,,)"
+      x -> x
+    meq = case find ((==ct) . show . ctor) $ eqns m of
+           Nothing -> throwM $ EvalError $ printf "applyMeasure(%s): no equation for %s" (show m) (show ct)
+           Just x -> return x
+
+applyMeasure m e           _
+  = throwM $ EvalError $ printf "applyMeasure(%s, %s)" (showpp m) (showpp e)
+
+setSym :: Symbol
+setSym = "LC_SET"
+
+nubSort :: [Expr] -> [Expr]
+nubSort = nub . Data.List.sort
+
+mkSet :: [Expr] -> Expr
+mkSet = app setSym . nubSort
+
+evalSet :: Symbol -> [Expr] -> Target Expr
+evalSet "Set_emp" [e]
+  = return $ if e == app setSym [] then 0 else 1
+evalSet "Set_sng" [e]
+  = return $ mkSet [e]
+evalSet "Set_add" [e1, EApp _ e2]
+  = return $ mkSet $ e1:e2
+evalSet "Set_cap" [EApp _ e1, EApp _ e2]
+  = return $ mkSet $ intersect e1 e2
+evalSet "Set_cup" [EApp _ e1, EApp _ e2]
+  = return $ mkSet $ e1 ++ e2
+evalSet "Set_dif" [EApp _ e1, EApp _ e2]
+  = return $ mkSet $ e1 \\ e2
+evalSet "Set_sub" [EApp _ e1, EApp _ e2]
+  = return $ if null (e1 \\ e2) then 0 else 1
+evalSet "Set_mem" [e1, EApp f e2] | val f == setSym
+  = return $ if e1 `elem` e2 then 0 else 1
+evalSet f es = throwM $ EvalError $ printf "evalSet(%s, %s)" (show f) (show es)
+
+evalBody
+  :: Language.Haskell.Liquid.Types.Def ctor
+     -> [Expr] -> M.HashMap Symbol Expr -> Target Expr
+evalBody eq xs env = go $ body eq
+  where
+    go (E e) = evalExpr (subst su e) env
+    go (P p) = evalPred (subst su p) env >>= \b -> return $ if b then 0 else 1
+    go (R v p) = do e <- evalRel v (subst su p) env
+                    case e of
+                      Nothing -> throwM $ EvalError $ "evalBody can't handle: " ++ show (R v p)
+                      Just e  -> return e
+    --go (R v (PBexp (EApp f e))) | val f == "Set_emp" = return $ app setSym []
+    ----FIXME: figure out how to handle the general case..
+    --go (R v p) = return (ECon (I 0))
+    su = mkSubst $ zip (binds eq) xs
+
+evalRel :: Symbol -> Pred -> M.HashMap Symbol Expr -> Target (Maybe Expr)
+evalRel v (PAnd ps)       m = Just . head . catMaybes <$> sequence [evalRel v p m | p <- ps]
+evalRel v (PImp p q)      m = do pv <- evalPred p m
+                                 if pv
+                                    then evalRel v q m
+                                    else return Nothing
+evalRel v (PAtom Eq (EVar v') e2) m
+  | v == v'
+  = Just <$> evalExpr e2 m
+evalRel v (PBexp (EApp f [EVar v'])) _
+  | v == v' && val f == "Set_emp"
+  = return $ Just $ app setSym []
+evalRel _ p               _
+  = throwM $ EvalError $ "evalRel: " ++ show p
+
+evalExpr :: Expr -> M.HashMap Symbol Expr -> Target Expr
+evalExpr (ECon i)       _ = return $ ECon i
+evalExpr (EVar x)       m = return $ m M.! x
+evalExpr (ESym s)       _ = return $ ESym s
+evalExpr (EBin b e1 e2) m = evalBop b <$> evalExpr e1 m <*> evalExpr e2 m
+evalExpr (EApp f es)    m
+  | val f == "Set_emp" || val f == "Set_sng" || val f `M.member` smt_set_funs
+  = mapM (`evalExpr` m) es >>= \es' -> evalSet (val f) es'
+  | otherwise
+  = find ((==f) . name) <$> gets measEnv >>= \case
+      Nothing -> EApp f <$> mapM (`evalExpr` m) es
+                    --FIXME: should really extend this to multi-param measures..
+      Just ms -> do e' <- evalExpr (head es) m
+                    applyMeasure ms e' m
+evalExpr (EIte p e1 e2) m
+  = do b <- evalPred p m
+       if b
+         then evalExpr e1 m
+         else evalExpr e2 m
+evalExpr e              _ = throwM $ EvalError $ printf "evalExpr(%s)" (show e)
+
+evalBop :: Bop -> Expr -> Expr -> Expr
+evalBop Plus  (ECon (I x)) (ECon (I y)) = ECon . I $ x + y
+evalBop Minus (ECon (I x)) (ECon (I y)) = ECon . I $ x - y
+evalBop Times (ECon (I x)) (ECon (I y)) = ECon . I $ x * y
+evalBop Div   (ECon (I x)) (ECon (I y)) = ECon . I $ x `div` y
+evalBop Mod   (ECon (I x)) (ECon (I y)) = ECon . I $ x `mod` y
+evalBop b     e1           e2           = error $ printf "evalBop(%s, %s, %s)" (show b) (show e1) (show e2)
diff --git a/src/Test/Target/Expr.hs b/src/Test/Target/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Expr.hs
@@ -0,0 +1,68 @@
+module Test.Target.Expr where
+
+import Language.Fixpoint.Types
+
+
+eq :: Expr -> Expr -> Pred
+eq  = PAtom Eq
+infix 4 `eq`
+
+ge :: Expr -> Expr -> Pred
+ge  = PAtom Ge
+infix 5 `ge`
+
+le :: Expr -> Expr -> Pred
+le  = PAtom Le
+infix 5 `le`
+
+gt :: Expr -> Expr -> Pred
+gt  = PAtom Gt
+infix 5 `gt`
+
+lt :: Expr -> Expr -> Pred
+lt  = PAtom Lt
+infix 5 `lt`
+
+iff :: Pred -> Pred -> Pred
+iff = PIff
+infix 3 `iff`
+
+imp :: Pred -> Pred -> Pred
+imp = PImp
+infix 3 `imp`
+
+
+app :: Symbolic a => a -> [Expr] -> Expr
+app f es = EApp (dummyLoc $ symbol f) es
+
+var :: Symbolic a => a -> Expr
+var = EVar . symbol
+
+-- prop :: Symbolic a => a -> Pred
+-- prop = PBexp . EVar . symbol
+prop :: Expr -> Pred
+prop = PBexp
+
+instance Num Expr where
+  fromInteger = ECon . I . fromInteger
+  (+) = EBin Plus
+  (-) = EBin Minus
+  (*) = EBin Times
+  abs = error "abs of Liquid.Fixpoint.Types.Expr"
+  signum = error "signum of Liquid.Fixpoint.Types.Expr"
+
+instance Real Expr where
+  toRational (ECon (I i)) = fromIntegral i
+  toRational x            = error $ "toRational: " ++ show x
+
+instance Enum Expr where
+  toEnum = ECon . I . fromIntegral
+  fromEnum (ECon (I i)) = fromInteger i
+  fromEnum x            = error $ "fromEnum: " ++ show x
+
+instance Integral Expr where
+  div = EBin Div
+  mod = EBin Mod
+  quotRem x y = (x `div` y, x `mod` y)
+  toInteger (ECon (I i)) = i
+  toInteger x            = error $ "toInteger: " ++ show x
diff --git a/src/Test/Target/Monad.hs b/src/Test/Target/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Monad.hs
@@ -0,0 +1,270 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RecordWildCards            #-}
+module Test.Target.Monad
+  ( whenVerbose
+  , noteUsed
+  , addDep
+  , addConstraint
+  , addConstructor
+  , inModule
+  , making
+  , lookupCtor
+  , guarded
+  , fresh
+  , freshChoice
+  , freshInt
+  , getValue
+  , Target, runTarget
+  , TargetState(..), initState
+  , TargetOpts(..), defaultOpts
+  ) where
+
+import           Control.Applicative
+import           Control.Arrow                    (first, (***))
+import qualified Control.Exception                as Ex
+import           Control.Monad
+import           Control.Monad.Catch
+import           Control.Monad.Reader
+import           Control.Monad.State
+import           Data.Generics                    (Data, everywhere, mkT)
+import qualified Data.HashMap.Strict              as M
+import qualified Data.HashSet                     as S
+import           Data.IORef
+import           Data.List                        hiding (sort)
+import           Data.Monoid
+import qualified Data.Text.Lazy                   as LT
+import           System.IO.Unsafe
+import           Text.Printf
+
+import           Language.Fixpoint.Config         (SMTSolver (..))
+import           Language.Fixpoint.Names
+import           Language.Fixpoint.SmtLib2        hiding (verbose)
+import           Language.Fixpoint.Types
+import           Language.Haskell.Liquid.PredType
+import           Language.Haskell.Liquid.RefType
+import           Language.Haskell.Liquid.Tidy
+import           Language.Haskell.Liquid.Types    hiding (var, Target)
+
+import qualified GHC
+
+import           Test.Target.Types
+import           Test.Target.Util
+
+-- import           Debug.Trace
+
+
+instance Symbolic LT.Text where
+  symbol = symbol . LT.toStrict
+
+newtype Target a = Target (StateT TargetState (ReaderT TargetOpts IO) a)
+  deriving ( Functor, Applicative, Monad, MonadIO, Alternative
+           , MonadState TargetState, MonadCatch, MonadReader TargetOpts )
+instance MonadThrow Target where
+  throwM = Ex.throw
+
+runTarget :: TargetOpts -> TargetState -> Target a -> IO a
+runTarget opts st (Target x) = runReaderT (evalStateT x st) opts
+
+-- evalTarget :: TargetOpts -> TargetState -> Target a -> IO a
+-- evalTarget o s (Target x) = runReaderT (evalStateT x s) o
+
+-- execTarget :: GhcSpec -> Target a -> IO TargetState
+-- execTarget e (Target x) = execStateT x (initGS e)
+
+seed :: IORef Int
+seed = unsafePerformIO $ newIORef 0
+{-# NOINLINE seed #-}
+
+freshInt :: Target Int
+freshInt = liftIO $ do
+  n <- readIORef seed
+  modifyIORef' seed (+1)
+  return n
+
+data TargetOpts = TargetOpts
+  { depth      :: !Int
+  , solver     :: !SMTSolver
+  , verbose    :: !Bool
+  , logging    :: !Bool
+  , keepGoing  :: !Bool
+    -- ^ whether to keep going after finding a counter-example, useful for
+    -- checking coverage
+  , maxSuccess :: !(Maybe Int)
+    -- ^ whether to stop after a certain number of successful tests, or
+    -- enumerate the whole input space
+  , scDepth    :: !Bool
+    -- ^ whether to use SmallCheck's notion of depth
+  }
+
+defaultOpts :: TargetOpts
+defaultOpts = TargetOpts
+  { depth = 5
+  , solver = Z3
+  , verbose = False
+  , logging = True
+  , keepGoing = False
+  , maxSuccess = Nothing
+  , scDepth = False
+  }
+
+data TargetState = TargetState
+  { variables    :: ![Variable]
+  , choices      :: ![Variable]
+  , constraints  :: !Constraint
+  , deps         :: !(M.HashMap Symbol [Symbol])
+  , realized     :: ![(Symbol, Value)]
+  , dconEnv      :: ![(Symbol, DataConP)]
+  , ctorEnv      :: !DataConEnv
+  , measEnv      :: !MeasureEnv
+  , embEnv       :: !(TCEmb GHC.TyCon)
+  , tyconInfo    :: !(M.HashMap GHC.TyCon RTyCon)
+  , freesyms     :: ![(Symbol,Symbol)]
+  , constructors :: ![Variable] -- (S.HashSet Variable)  --[(String, String)]
+  , sigs         :: ![(Symbol, SpecType)]
+  , chosen       :: !(Maybe Symbol)
+  , sorts        :: !(S.HashSet Sort)
+  , modName      :: !Symbol
+  , filePath     :: !FilePath
+  , makingTy     :: !Sort
+  , smtContext   :: !Context
+  }
+
+initState :: FilePath -> GhcSpec -> Context -> TargetState
+initState fp sp ctx = TargetState
+  { variables    = []
+  , choices      = []
+  , constraints  = []
+  , deps         = mempty
+  , realized     = []
+  , dconEnv      = dcons
+  , ctorEnv      = cts
+  , measEnv      = meas
+  , embEnv       = tcEmbeds sp
+  , tyconInfo    = tyi
+  , freesyms     = free
+  , constructors = []
+  , sigs         = sigs
+  , chosen       = Nothing
+  , sorts        = S.empty
+  , modName      = ""
+  , filePath     = fp
+  , makingTy     = FObj ""
+  , smtContext   = ctx
+  }
+  where
+    dcons = tidy $ map (first symbol) (dconsP sp)
+    cts   = tidy $ map (symbol *** val) (ctors sp)
+    tyi   = tidy $ makeTyConInfo (tconsP sp)
+    free  = tidy $ map (symbol *** symbol) $ freeSyms sp
+    sigs  = tidy $ map (symbol *** val) $ tySigs sp
+    meas  = tidy $ measures sp
+    tidy :: forall a. Data a => a -> a
+    tidy  = everywhere (mkT tidySymbol)
+
+whenVerbose :: Target () -> Target ()
+whenVerbose x
+  = do v <- asks verbose
+       when v x
+
+noteUsed :: (Symbol, Value) -> Target ()
+noteUsed (v,x) = modify $ \s@(TargetState {..}) -> s { realized = (v,x) : realized }
+
+-- TODO: does this type make sense? should it be Symbol -> Symbol -> Target ()?
+addDep :: Symbol -> Expr -> Target ()
+addDep from (EVar to) = modify $ \s@(TargetState {..}) ->
+  s { deps = M.insertWith (flip (++)) from [to] deps }
+addDep _ _ = return ()
+
+addConstraint :: Pred -> Target ()
+addConstraint p = modify $ \s@(TargetState {..}) -> s { constraints = p:constraints }
+
+addConstructor :: Variable -> Target ()
+addConstructor c
+  = do -- modify $ \s@(TargetState {..}) -> s { constructors = S.insert c constructors }
+       modify $ \s@(TargetState {..}) -> s { constructors = nub $ c:constructors }
+
+inModule :: Symbol -> Target a -> Target a
+inModule m act
+  = do m' <- gets modName
+       modify $ \s -> s { modName = m }
+       r <- act
+       modify $ \s -> s { modName = m' }
+       return r
+
+making :: Sort -> Target a -> Target a
+making ty act
+  = do ty' <- gets makingTy
+       modify $ \s -> s { makingTy = ty }
+       r <- act
+       modify $ \s -> s { makingTy = ty' }
+       return r
+
+-- | Find the refined type of a data constructor.
+lookupCtor :: Symbol -> Target SpecType
+lookupCtor c
+  = do mt <- lookup c <$> gets ctorEnv
+       m  <- gets filePath
+       case mt of
+         Just t -> return t
+         Nothing -> do
+           t <- io $ runGhc $ do
+                  _ <- loadModule m
+                  t <- GHC.exprType (printf "(%s)" (symbolString c))
+                  return (ofType t)
+           modify $ \s@(TargetState {..}) -> s { ctorEnv = (c,t) : ctorEnv }
+           return t
+
+-- | Given a data constructor @d@ and an action, create a new choice variable
+-- @c@ and execute the action while guarding any generated constraints with
+-- @c@. Returns @(action-result, c)@.
+guarded :: String -> Target Expr -> Target (Expr, Expr)
+guarded cn act
+  = do c  <- freshChoice cn
+       mc <- gets chosen
+       modify $ \s -> s { chosen = Just c }
+       x <- act
+       modify $ \s -> s { chosen = mc }
+       return (x, EVar c)
+
+-- | Generate a fresh variable of the given 'Sort'.
+fresh :: Sort -> Target Symbol
+fresh sort
+  = do n <- freshInt
+       let sorts' = sortTys sort
+       modify $ \s@(TargetState {..}) -> s { sorts = S.union (S.fromList (arrowize sort : sorts')) sorts }
+       let x = symbol $ LT.unpack (LT.intercalate "->" $ map (LT.fromStrict.symbolText.unObj) sorts') ++ show n
+       modify $ \s@(TargetState {..}) -> s { variables = (x,sort) : variables }
+       return x
+
+sortTys :: Sort -> [Sort]
+sortTys (FFunc _ ts) = concatMap sortTys ts
+sortTys t            = [t]
+
+arrowize :: Sort -> Sort
+arrowize = FObj . symbol . LT.intercalate "->" . map (LT.fromStrict . symbolText . unObj) . sortTys
+
+unObj :: Sort -> Symbol
+unObj FInt     = "Int"
+unObj (FObj s) = s
+unObj s        = error $ "unObj: " ++ show s
+
+-- | Given a data constructor @d@, create a new choice variable corresponding to
+-- @d@.
+freshChoice :: String -> Target Symbol
+freshChoice cn
+  = do n <- freshInt
+       modify $ \s@(TargetState {..}) -> s { sorts = S.insert choicesort sorts }
+       let x = symbol $ LT.unpack (smt2 choicesort) ++ "-" ++ cn ++ "-" ++ show n
+       modify $ \s@(TargetState {..}) -> s { variables = (x,choicesort) : variables }
+       return x
+
+-- | Ask the SMT solver for the 'Value' of the given variable.
+getValue :: Symbol -> Target Value
+getValue v = do
+  ctx <- gets smtContext
+  Values [x] <- io $ ensureValues $ command ctx (GetValue [v])
+  noteUsed x
+  return (snd x)
+
diff --git a/src/Test/Target/Targetable.hs b/src/Test/Target/Targetable.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Targetable.hs
@@ -0,0 +1,543 @@
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE DefaultSignatures    #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+module Test.Target.Targetable
+  ( Targetable(..)
+  , unfold, apply, unapply
+  , oneOf, whichOf
+  , constrain, ofReft
+  ) where
+
+import           Control.Applicative
+import           Control.Arrow                   (second)
+import qualified Control.Monad.Catch           as Ex
+import           Control.Monad.Reader
+import           Control.Monad.State
+import           Data.Char
+import qualified Data.HashMap.Strict             as M
+import           Data.List
+import           Data.Maybe
+import           Data.Monoid
+import           Data.Proxy
+import qualified Data.Text                       as T
+import           Data.Word                       (Word8)
+import           GHC.Generics
+
+import           Language.Fixpoint.Types         hiding (prop, ofReft)
+import           Language.Haskell.Liquid.RefType
+import           Language.Haskell.Liquid.Types   hiding (var)
+
+import           Test.Target.Expr
+import           Test.Target.Eval
+import           Test.Target.Monad
+import           Test.Target.Types
+import           Test.Target.Util
+
+-- import Debug.Trace
+
+--------------------------------------------------------------------------------
+--- Constrainable Data
+--------------------------------------------------------------------------------
+-- | A class of datatypes for which we can efficiently generate constrained
+-- values by querying an SMT solver.
+--
+-- If possible, instances should not be written by hand, but rather by using the
+-- default implementations via "GHC.Generics", e.g.
+--
+-- > import GHC.Generics
+-- > import Test.Target.Targetable
+-- >
+-- > data Foo = ... deriving Generic
+-- > instance Targetable Foo
+class Targetable a where
+  -- | Construct an SMT query describing all values of the given type up to the
+  -- given 'Depth'.
+  query   :: Proxy a -> Depth -> SpecType -> Target Symbol
+
+  -- | Reconstruct a Haskell value from the SMT model.
+  decode  :: Symbol
+             -- ^ the symbolic variable corresponding to the root of the value
+          -> SpecType
+             -- ^ the type of values we're generating (you can probably ignore this)
+          -> Target a
+
+  -- | Check whether a Haskell value inhabits the given type. Also returns a
+  -- logical expression corresponding to the Haskell value.
+  check   :: a -> SpecType -> Target (Bool, Expr)
+
+  -- | Translate a Haskell value into a logical expression.
+  toExpr  :: a -> Expr
+
+  -- | What is the Haskell type? (Mainly used to make the SMT queries more
+  -- readable).
+  getType :: Proxy a -> Sort
+
+  default getType :: (Generic a, Rep a ~ D1 d f, Datatype d)
+                  => Proxy a -> Sort
+  getType _ = FObj $ qualifiedDatatypeName (undefined :: Rep a a)
+
+  default query :: (Generic a, GQuery (Rep a))
+                => Proxy a -> Int -> SpecType -> Target Symbol
+  query p = gquery (reproxyRep p)
+
+  default toExpr :: (Generic a, GToExpr (Rep a))
+                 => a -> Expr
+  toExpr = gtoExpr . from
+
+  default decode :: (Generic a, GDecode (Rep a))
+                 => Symbol -> SpecType -> Target a
+  decode v _ = do
+    x <- whichOf v
+    (c, fs) <- unapply x
+    to <$> gdecode c fs
+
+  default check :: (Generic a, GCheck (Rep a))
+                => a -> SpecType -> Target (Bool, Expr)
+  check v t = gcheck (from v) t
+
+reproxy :: proxy a -> Proxy b
+reproxy _ = Proxy
+{-# INLINE reproxy #-}
+
+-- | Given a data constuctor @d@ and a refined type for @d@s output,
+-- return a list of types representing suitable arguments for @d@.
+unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)]
+unfold cn t = do
+  dcp <- lookupCtor cn
+  tyi <- gets tyconInfo
+  emb <- gets embEnv
+  let ts = applyPreds (addTyConInfo emb tyi t) dcp
+  return ts
+
+-- | Given a data constructor @d@ and a list of expressions @xs@, construct a
+-- new expression corresponding to @d xs@.
+apply :: Symbol -> [Expr] -> Target Expr
+apply c vs = do 
+  mc <- gets chosen
+  case mc of
+    Just ch -> mapM_ (addDep ch) vs
+    Nothing -> return ()
+  let x = app c vs
+  t <- lookupCtor c
+  let (xs, _, rt) = bkArrowDeep t
+      su          = mkSubst $ zip (map symbol xs) vs
+  addConstructor (c, rTypeSort mempty t)
+  constrain $ ofReft (subst su $ reft rt) x
+  return x
+
+-- | Split a symbolic variable representing the application of a data
+-- constructor into a pair of the data constructor and the sub-variables.
+unapply :: Symbol -> Target (Symbol, [Symbol])
+unapply c = do
+  let [_,cn,_] = T.splitOn "-" $ symbolText c
+  deps <- gets deps
+  return (symbol cn, M.lookupDefault [] c deps)
+
+-- | Given a symbolic variable and a list of @(choice, var)@ pairs,
+-- @oneOf x choices@ asserts that @x@ must equal one of the @var@s in
+-- @choices@.
+oneOf :: Symbol -> [(Expr,Expr)] -> Target ()
+oneOf x cs
+  = do cs <- forM cs $ \(y,c) -> do
+               addDep x c
+               constrain $ prop c `imp` (var x `eq` y)
+               return $ prop c
+       constrain $ pOr cs
+       constrain $ pAnd [ PNot $ pAnd [x, y]
+                        | [x, y] <- filter ((==2) . length) $ subsequences cs ]
+
+-- | Given a symbolic variable @x@, figure out which of @x@s choice varaibles
+-- was picked and return it.
+whichOf :: Symbol -> Target Symbol
+whichOf v = do
+  deps <- gets deps
+  let Just cs = M.lookup v deps
+  [c]  <- catMaybes <$> forM cs (\c -> do
+    val <- getValue c
+    if val == "true"
+      then return (Just c)
+      else return Nothing)
+  return c
+
+
+-- | Assert a logical predicate, guarded by the current choice variable.
+constrain :: Pred -> Target ()
+constrain p = do
+  mc <- gets chosen
+  case mc of
+    Nothing -> addConstraint p
+    Just c  -> let p' = prop (var c) `imp` p
+               in addConstraint p'
+
+-- | Given a refinement @{v | p}@ and an expression @e@, construct
+-- the predicate @p[e/v]@.
+ofReft :: Reft -> Expr -> Pred
+ofReft (Reft (v, rs)) e
+  = let x = mkSubst [(v, e)]
+    in pAnd [subst x p | RConc p <- rs]
+
+--------------------------------------------------------------------------------
+--- Instances
+--------------------------------------------------------------------------------
+instance Targetable () where
+  getType _ = FObj "GHC.Tuple.()"
+  query _ _ _ = fresh (FObj "GHC.Tuple.()")
+  -- this is super fiddly, but seemingly required since GHC.exprType chokes on "GHC.Tuple.()"
+  toExpr _   = app ("()" :: Symbol) []
+
+  decode _ _ = return ()
+  check _ t = do
+    let e = app ("()" :: Symbol) []
+    b <- eval (reft t) e
+    return (b,e)
+
+instance Targetable Int where
+  getType _ = FObj "GHC.Types.Int"
+  query _ d t = fresh FInt >>= \x ->
+    do constrain $ ofReft (reft t) (var x)
+       -- use the unfolding depth to constrain the range of Ints, like QuickCheck
+       constrain $ var x `ge` fromIntegral (negate d)
+       constrain $ var x `le` fromIntegral d
+       return x
+  toExpr i = ECon $ I $ fromIntegral i
+
+  decode v _ = read . T.unpack <$> getValue v
+
+  check v t = do
+    let e = fromIntegral v
+    b <- eval (reft t) e
+    return (b, e)
+
+instance Targetable Integer where
+  getType _ = FObj "GHC.Integer.Type.Integer"
+  query _ d t = query (Proxy :: Proxy Int) d t
+  toExpr  x = toExpr (fromIntegral x :: Int)
+
+  decode v t = decode v t >>= \(x::Int) -> return . fromIntegral $ x
+
+  check v t = do
+    let e = fromIntegral v
+    b <- eval (reft t) e
+    return (b, e)
+
+instance Targetable Char where
+  getType _ = FObj "GHC.Types.Char"
+  query _ d t = fresh FInt >>= \x ->
+    do constrain $ var x `ge` 0
+       constrain $ var x `le` fromIntegral d
+       constrain $ ofReft (reft t) (var x)
+       return x
+  toExpr  c = ESym $ SL $ T.singleton c
+
+  decode v t = decode v t >>= \(x::Int) -> return . chr $ x + ord 'a'
+
+  check v t = do
+    let e = ESym $ SL $ T.singleton v
+    b <- eval (reft t) e
+    return (b, e)
+
+instance Targetable Word8 where
+  getType _ = FObj "GHC.Word.Word8"
+  query _ d t = fresh FInt >>= \x ->
+    do _ <- asks depth
+       constrain $ var x `ge` 0
+       constrain $ var x `le` fromIntegral d
+       constrain $ ofReft (reft t) (var x)
+       return x
+  toExpr i   = ECon $ I $ fromIntegral i
+
+  decode v t = decode v t >>= \(x::Int) -> return $ fromIntegral x
+
+  check v t = do
+    let e = fromIntegral v
+    b <- eval (reft t) e
+    return (b, e)
+
+instance Targetable Bool where
+  getType _ = FObj "GHC.Types.Bool"
+  query _ _ t = fresh boolsort >>= \x ->
+    do constrain $ ofReft (reft t) (var x)
+       return x
+
+  decode v _ = getValue v >>= \case
+    "true"  -> return True
+    "false" -> return False
+    x       -> Ex.throwM (SmtError $ "expected boolean, got: " ++ T.unpack x)
+
+
+instance Targetable a => Targetable [a]
+instance Targetable a => Targetable (Maybe a)
+instance (Targetable a, Targetable b) => Targetable (Either a b)
+instance (Targetable a, Targetable b) => Targetable (a,b)
+instance (Targetable a, Targetable b, Targetable c) => Targetable (a,b,c)
+instance (Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a,b,c,d)
+
+
+-- instance (Num a, Integral a, Targetable a) => Targetable (Ratio a) where
+--   getType _ = FObj "GHC.Real.Ratio"
+--   query _ d t = query (Proxy :: Proxy Int) d t
+--   decode v t= decode v t >>= \ (x::Int) -> return (fromIntegral x)
+--   -- query _ d t = fresh (FObj "GHC.Real.Ratio") >>= \x ->
+--   --   do query (Proxy :: Proxy Int) d t
+--   --      query (Proxy :: Proxy Int) d t
+--   --      return x
+--   -- stitch d t = do x :: Int <- stitch d t
+--   --                 y' :: Int <- stitch d t
+--   --                 -- we should really modify `t' above to have Z3 generate non-zero denoms
+--   --                 let y = if y' == 0 then 1 else y'
+--   --                 let toA z = fromIntegral z :: a
+--   --                 return $ toA x % toA y
+--   toExpr x = EApp (dummyLoc "GHC.Real.:%") [toExpr (numerator x), toExpr (denominator x)]
+--   check = undefined
+
+
+reproxyRep :: Proxy a -> Proxy (Rep a a)
+reproxyRep = reproxy
+
+
+--------------------------------------------------------------------------------
+--- Sums of Products
+--------------------------------------------------------------------------------
+class GToExpr f where
+  gtoExpr      :: f a -> Expr
+
+class GQuery f where
+  gquery       :: Proxy (f a) -> Int -> SpecType -> Target Symbol
+
+class GDecode f where
+  gdecode      :: Symbol -> [Symbol] -> Target (f a)
+
+class GCheck f where
+  gcheck       :: f a -> SpecType -> Target (Bool, Expr)
+
+reproxyGElem :: Proxy (M1 d c f a) -> Proxy (f a)
+reproxyGElem = reproxy
+
+instance (Datatype c, GToExprCtor f) => GToExpr (D1 c f) where
+  gtoExpr (M1 x) = app (qualify mod (symbolString $ val d)) xs
+    where
+      mod  = GHC.Generics.moduleName (undefined :: D1 c f a)
+      (EApp d xs) = gtoExprCtor x
+
+instance (Datatype c, GQueryCtors f) => GQuery (D1 c f) where
+  gquery p d t = inModule mod . making sort $ do
+    xs <- gqueryCtors (reproxyGElem p) d t
+    x  <- fresh sort
+    oneOf x xs
+    constrain $ ofReft (reft t) (var x)
+    return x
+   where
+     mod  = symbol $ GHC.Generics.moduleName (undefined :: D1 c f a)
+     sort = FObj $ qualifiedDatatypeName (undefined :: D1 c f a)
+
+instance (Datatype c, GDecode f) => GDecode (D1 c f) where
+  gdecode c vs = M1 <$> making sort (gdecode c vs)
+    where
+      sort = FObj $ qualifiedDatatypeName (undefined :: D1 c f a)
+
+instance (Datatype c, GCheck f) => GCheck (D1 c f) where
+  gcheck (M1 x) t = inModule mod . making sort $ gcheck x t
+    where
+      mod  = symbol $ GHC.Generics.moduleName (undefined :: D1 c f a)
+      sort = FObj $ qualifiedDatatypeName (undefined :: D1 c f a)
+
+
+instance (Targetable a) => GToExpr (K1 i a) where
+  gtoExpr (K1 x) = toExpr x
+
+instance (Targetable a) => GQuery (K1 i a) where
+  gquery p d t = do 
+    let p' = reproxy p :: Proxy a
+    ty <- gets makingTy
+    depth <- asks depth
+    sc <- asks scDepth
+    let d' = if getType p' == ty || sc
+                then d
+                else depth
+    query p' d' t
+
+instance Targetable a => GDecodeFields (K1 i a) where
+  gdecodeFields (v:vs) = do
+    x <- decode v undefined
+    return (vs, K1 x)
+  gdecodeFields _ = error "gdecodeFields []"
+
+instance Targetable a => GCheckFields (K1 i a) where
+  gcheckFields (K1 x) ((f,t):ts) = do
+    (b, v) <- check x t
+    return (b, [v], subst (mkSubst [(f, v)]) ts)
+  gcheckFields _ _ = error "gcheckFields _ []"
+
+qualify :: String -> String -> String
+qualify m x = m ++ ('.':x)
+{-# INLINE qualify #-}
+
+qualifiedDatatypeName :: Datatype d => D1 d f a -> Symbol
+qualifiedDatatypeName d = symbol $ qualify m (datatypeName d)
+  where m = GHC.Generics.moduleName d
+{-# INLINE qualifiedDatatypeName #-}
+
+--------------------------------------------------------------------------------
+--- Sums
+--------------------------------------------------------------------------------
+class GToExprCtor f where
+  gtoExprCtor   :: f a -> Expr
+
+class GQueryCtors f where
+  gqueryCtors :: Proxy (f a) -> Int -> SpecType -> Target [(Expr, Expr)]
+
+reproxyLeft :: Proxy ((c (f :: * -> *) (g :: * -> *)) a) -> Proxy (f a)
+reproxyLeft = reproxy
+
+reproxyRight :: Proxy ((c (f :: * -> *) (g :: * -> *)) a) -> Proxy (g a)
+reproxyRight = reproxy
+
+instance (GToExprCtor f, GToExprCtor g) => GToExprCtor (f :+: g) where
+  gtoExprCtor (L1 x) = gtoExprCtor x
+  gtoExprCtor (R1 x) = gtoExprCtor x
+
+instance (GQueryCtors f, GQueryCtors g) => GQueryCtors (f :+: g) where
+  gqueryCtors p d t = do 
+    xs <- gqueryCtors (reproxyLeft p) d t
+    ys <- gqueryCtors (reproxyRight p) d t
+    return $! xs++ys
+
+instance (GDecode f, GDecode g) => GDecode (f :+: g) where
+  gdecode c vs =  L1 <$> gdecode c vs
+              <|> R1 <$> gdecode c vs
+
+instance (GCheck f, GCheck g) => GCheck (f :+: g) where
+  gcheck (L1 x) t = gcheck x t
+  gcheck (R1 x) t = gcheck x t
+
+
+instance (Constructor c, GToExprFields f) => GToExprCtor (C1 c f) where
+  gtoExprCtor c@(M1 x)  = app (symbol $ conName c) (gtoExprFields x)
+
+instance (Constructor c, GRecursive f, GQueryFields f) => GQueryCtors (C1 c f) where
+  gqueryCtors p d t | d <= 0
+    = do ty <- gets makingTy
+         if gisRecursive p ty
+           then return []
+           else pure <$> gqueryCtor p 0 t
+  gqueryCtors p d t = pure <$> gqueryCtor p d t
+
+instance (Constructor c, GDecodeFields f) => GDecode (C1 c f) where
+  gdecode c vs
+    | c == symbol (conName (undefined :: C1 c f a))
+    = M1 . snd <$> gdecodeFields vs
+    | otherwise
+    = empty
+
+instance (Constructor c, GCheckFields f) => GCheck (C1 c f) where
+  gcheck (M1 x) t = do
+    mod <- symbolString <$> gets modName
+    let cn = symbol $ qualify mod (conName (undefined :: C1 c f a))
+    ts <- unfold cn t
+    (b, vs, _) <- gcheckFields x ts
+    let v = app cn vs
+    b'  <- eval (reft t) v
+    return (b && b', v)
+
+gisRecursive :: (Constructor c, GRecursive f)
+             => Proxy (C1 c f a) -> Sort -> Bool
+gisRecursive (p :: Proxy (C1 c f a)) t
+  = t `elem` gconArgTys (reproxyGElem p)
+
+gqueryCtor :: (Constructor c, GQueryFields f)
+           => Proxy (C1 c f a) -> Int -> SpecType -> Target (Expr, Expr)
+gqueryCtor (p :: Proxy (C1 c f a)) d t
+  = guarded cn $ do
+      mod <- symbolString <$> gets modName
+      ts  <- unfold (symbol $ qualify mod cn) t
+      xs  <- gqueryFields (reproxyGElem p) d ts
+      apply (symbol $ qualify mod cn) xs
+  where
+    cn = conName (undefined :: C1 c f a)
+
+--------------------------------------------------------------------------------
+--- Products
+--------------------------------------------------------------------------------
+class GToExprFields f where
+  gtoExprFields :: f a -> [Expr]
+
+class GRecursive f where
+  gconArgTys  :: Proxy (f a) -> [Sort]
+
+class GQueryFields f where
+  gqueryFields  :: Proxy (f a) -> Int -> [(Symbol,SpecType)] -> Target [Expr]
+
+class GDecodeFields f where
+  gdecodeFields :: [Symbol] -> Target ([Symbol], f a)
+
+class GCheckFields f where
+  gcheckFields :: f a -> [(Symbol, SpecType)]
+               -> Target (Bool, [Expr], [(Symbol, SpecType)])
+
+
+instance (GToExprFields f, GToExprFields g) => GToExprFields (f :*: g) where
+  gtoExprFields (f :*: g) = gtoExprFields f ++ gtoExprFields g
+
+instance (GRecursive f, GRecursive g) => GRecursive (f :*: g) where
+  gconArgTys p = gconArgTys (reproxyLeft p) ++ gconArgTys (reproxyRight p)
+
+instance (GQueryFields f, GQueryFields g) => GQueryFields (f :*: g) where
+  gqueryFields p d ts = do 
+    xs <- gqueryFields (reproxyLeft p) d ts
+    let su = mkSubst $ zipWith (\x t -> (fst t, x)) xs ts
+    let ts' = drop (length xs) ts
+    ys <- gqueryFields (reproxyRight p) d (map (second (subst su)) ts')
+    return $ xs ++ ys
+
+instance (GDecodeFields f, GDecodeFields g) => GDecodeFields (f :*: g) where
+  gdecodeFields vs = do
+    (vs', ls)  <- gdecodeFields vs
+    (vs'', rs) <- gdecodeFields vs'
+    return (vs'', ls :*: rs)
+
+instance (GCheckFields f, GCheckFields g) => GCheckFields (f :*: g) where
+  gcheckFields (f :*: g) ts = do
+    (bl,fs,ts')  <- gcheckFields f ts
+    (br,gs,ts'') <- gcheckFields g ts'
+    return (bl && br, fs ++ gs, ts'')
+
+
+instance (GToExpr f) => GToExprFields (S1 c f) where
+  gtoExprFields (M1 x)     = [gtoExpr x]
+
+instance Targetable a => GRecursive (S1 c (K1 i a)) where
+  gconArgTys _ = [getType (Proxy :: Proxy a)]
+
+instance (GQuery f) => GQueryFields (S1 c f) where
+  gqueryFields p d (t:_) = sequence [var <$> gquery (reproxyGElem p) (d-1) (snd t)]
+  gqueryFields _ _ _     = error "gqueryfields _ _ []"
+
+instance GDecodeFields f => GDecodeFields (S1 c f) where
+  gdecodeFields vs = do
+    (vs', x) <- gdecodeFields vs
+    return (vs', M1 x)
+
+instance (GCheckFields f) => GCheckFields (S1 c f) where
+  gcheckFields (M1 x) ts = gcheckFields x ts
+
+instance GToExprFields U1 where
+  gtoExprFields _ = []
+
+instance GRecursive U1 where
+  gconArgTys _    = []
+
+instance GQueryFields U1 where
+  gqueryFields _ _ _ = return []
+
+instance GDecodeFields U1 where
+  gdecodeFields vs = return (vs, U1)
+
+instance GCheckFields U1 where
+  gcheckFields _ ts = return (True, [], ts)
diff --git a/src/Test/Target/Targetable/Function.hs b/src/Test/Target/Targetable/Function.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Targetable/Function.hs
@@ -0,0 +1,177 @@
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE ViewPatterns         #-}
+
+module Test.Target.Targetable.Function () where
+
+import           Control.Applicative
+import           Control.Arrow                   (second)
+import           Control.Monad
+import qualified Control.Monad.Catch             as Ex
+import           Control.Monad.Reader
+import           Control.Monad.State
+import           Data.Char
+import qualified Data.HashMap.Strict             as M
+import           Data.IORef
+import           Data.Monoid
+import           Data.Proxy
+import qualified Data.Text                       as T
+import qualified GHC
+import           Language.Fixpoint.SmtLib2
+import           Language.Fixpoint.Types         hiding (ofReft)
+import           Language.Haskell.Liquid.GhcMisc (qualifiedNameSymbol)
+import           Language.Haskell.Liquid.RefType (addTyConInfo, rTypeSort)
+import           Language.Haskell.Liquid.Types   hiding (var)
+import           System.IO.Unsafe
+
+import           Test.Target.Targetable
+import           Test.Target.Eval
+import           Test.Target.Expr
+import           Test.Target.Monad
+import           Test.Target.Types
+import           Test.Target.Util
+
+
+getCtors :: SpecType -> [GHC.DataCon]
+getCtors (RApp c _ _ _) = GHC.tyConDataCons $ rtc_tc c
+getCtors (RAppTy t _ _) = getCtors t
+getCtors (RFun _ i o _) = getCtors i ++ getCtors o
+getCtors (RVar _ _)     = []
+getCtors t              = error $ "getCtors: " ++ showpp t
+
+dataConSymbol_noUnique :: GHC.DataCon -> Symbol
+dataConSymbol_noUnique = qualifiedNameSymbol . GHC.getName
+
+genFun :: Targetable a => Proxy a -> t -> SpecType -> Target Symbol
+genFun p _ (stripQuals -> t)
+  = do forM_ (getCtors t) $ \dc -> do
+         let c = dataConSymbol_noUnique dc
+         t <- lookupCtor c
+         addConstructor (c, rTypeSort mempty t)
+       fresh (getType p)
+
+stitchFun :: forall f. (Targetable (Res f))
+          => Proxy f -> SpecType -> Target ([Expr] -> Res f)
+stitchFun _ (bkArrowDeep . stripQuals -> (vs, tis, to))
+  = do mref <- io $ newIORef []
+       d <- asks depth
+       state' <- get
+       opts   <- ask
+       let st = state' { variables = [], choices = [], constraints = []
+                       , deps = mempty, constructors = [] }
+       return $ \es -> unsafePerformIO $ runTarget opts st $ do
+         -- let es = map toExpr xs
+         mv <- lookup es <$> io (readIORef mref)
+         case mv of
+           Just v  -> return v
+           Nothing -> do
+             cts <- gets freesyms
+             let env = map (second (`app` [])) cts
+             bs <- zipWithM (evalType (M.fromList env)) tis es
+             case and bs of
+               --FIXME: better error message
+               False -> Ex.throwM $ PreconditionCheckFailed $ show $ zip es tis
+               True  -> do
+                 ctx <- gets smtContext
+                 _ <- io $ command ctx Push
+                 xes <- mapM genExpr es
+                 let su = mkSubst $ zipWith (\v e -> (v, var e)) vs xes
+                 xo <- query (Proxy :: Proxy (Res f)) d (subst su to)
+                 vs <- gets variables
+                 mapM_ (\x -> io . command ctx $ Declare (symbol x) [] (snd x)) vs
+                 cs <- gets constraints
+                 mapM_ (\c -> io . command ctx $ Assert Nothing c) cs
+
+                 resp <- io $ command ctx CheckSat
+                 when (resp == Unsat) $ Ex.throwM SmtFailedToProduceOutput
+
+                 o <- decode xo to
+                 -- whenVerbose $ io $ printf "%s -> %s\n" (show es) (show o)
+                 io (modifyIORef' mref ((es,o):))
+                 _ <- io $ command ctx Pop
+                 return o
+    
+genExpr :: Expr -> Target Symbol
+genExpr (EApp (val -> c) es)
+  = do xes <- mapM genExpr es
+       (xs, _, to) <- bkArrowDeep . stripQuals <$> lookupCtor c
+       let su  = mkSubst $ zip xs $ map var xes
+           to' = subst su to
+       x <- fresh $ FObj $ symbol $ rtc_tc $ rt_tycon to'
+       addConstraint $ ofReft (reft to') (var x)
+       return x
+genExpr (ECon (I i))
+  = do x <- fresh FInt
+       addConstraint $ var x `eq` expr i
+       return x
+genExpr (ESym (SL s)) | T.length s == 1
+  -- This is a Char, so encode it as an Int
+  = do x <- fresh FInt
+       addConstraint $ var x `eq` expr (ord $ T.head s)
+       return x
+genExpr e = error $ "genExpr: " ++ show e
+
+evalType :: M.HashMap Symbol Expr -> SpecType -> Expr -> Target Bool
+evalType m t e@(EApp c xs)
+  = do dcp <- lookupCtor (val c)
+       tyi <- gets tyconInfo
+       vts <- freshen $ applyPreds (addTyConInfo M.empty tyi t) dcp
+       liftM2 (&&) (evalWith m (toReft $ rt_reft t) e) (evalTypes m vts xs)
+evalType m t e
+  = evalWith m (toReft $ rt_reft t) e
+
+freshen :: [(Symbol, SpecType)] -> Target [(Symbol, SpecType)]
+freshen [] = return []
+freshen ((v,t):vts)
+  = do n <- freshInt
+       let v' = symbol . (++show n) . symbolString $ v
+           su = mkSubst [(v,var v')]
+           t' = subst su t
+       vts' <- freshen $ subst su vts
+       return ((v',t'):vts')
+
+evalTypes
+  :: M.HashMap Symbol Expr
+     -> [(Symbol, SpecType)] -> [Expr] -> Target Bool
+evalTypes _ []         []     = return True
+evalTypes m ((v,t):ts) (x:xs)
+  = liftM2 (&&) (evalType m' t x) (evalTypes m' ts xs)
+  where
+    m' = M.insert v x m
+evalTypes _ _ _ = error "evalTypes called with lists of unequal length!"
+
+instance (Targetable a, Targetable b, b ~ Res (a -> b))
+  => Targetable (a -> b) where
+  getType _ = FFunc 0 [getType (Proxy :: Proxy a), getType (Proxy :: Proxy b)]
+  query = genFun
+  decode _ t
+    = do f <- stitchFun (Proxy :: Proxy (a -> b)) t
+         return $ \a -> f [toExpr a]
+  toExpr  _ = var ("FUNCTION" :: Symbol)
+  check _ _ = error "can't check a function!"
+
+instance (Targetable a, Targetable b, Targetable c, c ~ Res (a -> b -> c))
+  => Targetable (a -> b -> c) where
+  getType _ = FFunc 0 [getType (Proxy :: Proxy a), getType (Proxy :: Proxy b)
+                      ,getType (Proxy :: Proxy c)]
+  query = genFun
+  decode _ t
+    = do f <- stitchFun (Proxy :: Proxy (a -> b -> c)) t
+         return $ \a b -> f [toExpr a, toExpr b]
+  toExpr  _ = var ("FUNCTION" :: Symbol)
+  check _ _ = error "can't check a function!"
+
+instance (Targetable a, Targetable b, Targetable c, Targetable d, d ~ Res (a -> b -> c -> d))
+  => Targetable (a -> b -> c -> d) where
+  getType _ = FFunc 0 [getType (Proxy :: Proxy a), getType (Proxy :: Proxy b)
+                      ,getType (Proxy :: Proxy c), getType (Proxy :: Proxy d)]
+  query = genFun
+  decode _ t
+    = do f <- stitchFun (Proxy :: Proxy (a -> b -> c -> d)) t
+         return $ \a b c -> f [toExpr a, toExpr b, toExpr c]
+  toExpr  _ = var ("FUNCTION" :: Symbol)
+  check _ _ = error "can't check a function!"
diff --git a/src/Test/Target/Testable.hs b/src/Test/Target/Testable.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Testable.hs
@@ -0,0 +1,197 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE BangPatterns         #-}
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE DoAndIfThenElse      #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE ViewPatterns         #-}
+module Test.Target.Testable (test, Testable) where
+
+import           Control.Applicative
+import           Control.Exception               (AsyncException, evaluate)
+import           Control.Monad
+import           Control.Monad.Catch
+import           Control.Monad.Reader
+import           Control.Monad.State
+import qualified Data.HashMap.Strict             as M
+import qualified Data.HashSet                    as S
+import           Data.Proxy
+import qualified Data.Text                       as T
+import           Data.Text.Format                hiding (print)
+import qualified Data.Text.Lazy                  as LT
+import           Text.Printf
+
+import           Language.Fixpoint.SmtLib2
+import           Language.Fixpoint.Types
+import           Language.Haskell.Liquid.RefType
+import           Language.Haskell.Liquid.Types   hiding (Result (..), env, var)
+
+import           Test.Target.Targetable          hiding (apply)
+-- import           Test.Target.Eval
+import           Test.Target.Expr
+import           Test.Target.Monad
+import           Test.Target.Types
+import           Test.Target.Util
+
+-- import Debug.Trace
+
+-- | Test that a function inhabits the given refinement type by enumerating
+-- valid inputs and calling the function on the inputs.
+test :: Testable f => f -> SpecType -> Target Result
+test f t
+  = do d <- asks depth
+       vs <- queryArgs f d t
+       setup
+       let (xs, tis, to) = bkArrowDeep $ stripQuals t
+       ctx <- gets smtContext
+       try (process f ctx vs (zip xs tis) to) >>= \case
+         Left  (e :: TargetException) -> return $ Errored $ show e
+         Right r                      -> return r
+
+process :: Testable f
+        => f -> Context -> [Symbol] -> [(Symbol,SpecType)] -> SpecType
+        -> Target Result
+process f ctx vs xts to = go 0 =<< io (command ctx CheckSat)
+  where
+    go !n Unsat    = return $ Passed n
+    go _  (Error e)= throwM $ SmtError $ T.unpack e
+    go !n Sat      = do
+      when (n `mod` 100 == 0) $ whenVerbose $ io $ printf "Checked %d inputs\n" n
+      let n' = n + 1
+      xs <- decodeArgs f vs (map snd xts)
+      whenVerbose $ io $ print xs
+      er <- io $ try $ evaluate (apply f xs)
+      -- whenVerbose $ io $ print er
+      case er of
+        Left (e :: SomeException)
+          -- DON'T catch AsyncExceptions since they are used by @timeout@
+          | Just (_ :: AsyncException) <- fromException e -> throwM e
+          | Just (SmtError _) <- fromException e -> throwM e
+          | Just (ExpectedValues _) <- fromException e -> throwM e
+          | otherwise -> mbKeepGoing xs n
+        Right r -> do
+          real <- gets realized
+          modify $ \s@(TargetState {..}) -> s { realized = [] }
+          let su = mkSubst $ mkExprs f (map fst xts) xs
+          (sat, _) <- check r (subst su to)
+
+          -- refute model *after* checking output in case we have HOFs, which
+          -- need to query the solver. if this is the last set of inputs, e.g.
+          -- refuting the current model forces the solver to return unsat next
+          -- time, the solver will return unsat when the HOF queries for an output,
+          -- causing us to return a spurious error
+          _ <- io $ command ctx $ Assert Nothing $ PNot $ pAnd
+                [ ESym (SL $ symbolText x) `eq` ESym (SL v) | (x,v) <- real ]
+          -- let env = map (second (`app` [])) cts ++ mkExprs f (map fst xts) xs
+          -- sat <- evalType (M.fromList env) to (toExpr r)
+          case sat of
+            False -> mbKeepGoing xs n'
+            True ->
+              asks maxSuccess >>= \case
+                Nothing -> go n' =<< io (command ctx CheckSat)
+                Just m | m == n' -> return $ Passed m
+                       | otherwise -> go n' =<< io (command ctx CheckSat)
+    go _ r = error $ "go _ " ++ show r
+    mbKeepGoing xs n = do
+      kg <- asks keepGoing
+      if kg
+        then go n =<< io (command ctx CheckSat)
+        else return (Failed $ show xs)
+
+-- | A class of functions that Target can test. A function is @Testable@ /iff/
+-- all of its component types are 'Targetable' and all of its argument types are
+-- 'Show'able.
+--
+-- You should __never__ have to define a new 'Testable' instance.
+class (AllHave Targetable (Args f), Targetable (Res f)
+      ,AllHave Show (Args f)) => Testable f where
+  queryArgs  :: f -> Int -> SpecType -> Target [Symbol]
+  decodeArgs :: f -> [Symbol] -> [SpecType] -> Target (HList (Args f))
+  apply      :: f -> HList (Args f) -> Res f
+  mkExprs    :: f -> [Symbol] -> HList (Args f) -> [(Symbol,Expr)]
+
+instance (Show a, Targetable a, Testable b) => Testable (a -> b) where
+  queryArgs f d (stripQuals -> (RFun _ i o _))
+    = liftM2 (:) (query (Proxy :: Proxy a) d i) (queryArgs (f undefined) d o)
+  queryArgs _ _ t = error $ "queryArgs called with non-function type: " ++ show t
+  decodeArgs f (v:vs) (t:ts)
+    = liftM2 (:::) (decode v t) (decodeArgs (f undefined) vs ts)
+  decodeArgs _ _ _ = error "decodeArgs called with empty list"
+  apply f (x ::: xs)
+    = apply (f x) xs
+  apply _ _ = error "apply called with empty list"
+  mkExprs f (v:vs) (x ::: xs)
+    = (v, toExpr x) : mkExprs (f undefined) vs xs
+  mkExprs _ _ _ = error "mkExprs called with empty list"
+
+instance (Targetable a, Args a ~ '[], Res a ~ a) => Testable a where
+  queryArgs _ _ _  = return []
+  decodeArgs _ _ _ = return Nil
+  apply f _        = f
+  mkExprs _ _ _    = []
+
+
+makeDecl :: Symbol -> Sort -> Command
+-- FIXME: hack..
+makeDecl x _ | x `M.member` smt_set_funs = Assert Nothing PTrue
+makeDecl x (FFunc _ ts) = Declare x (init ts) (last ts)
+makeDecl x t            = Declare x []        t
+
+func :: Sort -> Bool
+func (FFunc _ _) = True
+func _           = False
+
+setup :: Target ()
+setup = {-# SCC "setup" #-} do
+   ctx <- gets smtContext
+   emb <- gets embEnv
+   -- declare sorts
+   ss  <- S.toList <$> gets sorts
+   let defSort b e = io $ smtWrite ctx (format "(define-sort {} () {})" (b,e))
+   -- FIXME: combine this with the code in `fresh`
+   forM_ ss $ \case
+     FObj "Int" -> return ()
+     FInt       -> return ()
+     FObj "GHC.Types.Bool"   -> defSort ("GHC.Types.Bool" :: T.Text) ("Bool" :: T.Text)
+     FObj "CHOICE" -> defSort ("CHOICE" :: T.Text) ("Bool" :: T.Text)
+     s        -> defSort (LT.toStrict $ smt2 s) ("Int" :: T.Text)
+   -- declare constructors
+   cts <- gets constructors
+   mapM_ (\ (c,t) -> io . command ctx $ makeDecl (symbol c) t) cts
+   let nullary = [var c | (c,t) <- cts, not (func t)]
+   unless (null nullary) $
+     void $ io $ command ctx $ Distinct nullary
+   -- declare variables
+   vs <- gets variables
+   mapM_ (\ x -> io . command ctx $ Declare (symbol x) [] (arrowize $ snd x)) vs
+   -- declare measures
+   ms <- gets measEnv
+   mapM_ (\m -> io . command ctx $ makeDecl (val $ name m) (rTypeSort emb $ sort m)) ms
+   -- assert constraints
+   cs <- gets constraints
+   --mapM_ (\c -> do {i <- gets seed; modify $ \s@(GS {..}) -> s { seed = seed + 1 };
+   --                 io . command ctx $ Assert (Just i) c})
+   --  cs
+   mapM_ (\c -> io . command ctx $ Assert Nothing c) cs
+   -- deps <- V.fromList . map (symbol *** symbol) <$> gets deps
+   -- io $ generateDepGraph "deps" deps cs
+   -- return (ctx,vs,deps)
+
+sortTys :: Sort -> [Sort]
+sortTys (FFunc _ ts) = concatMap sortTys ts
+sortTys t            = [t]
+
+arrowize :: Sort -> Sort
+arrowize = FObj . symbol . LT.intercalate "->" . map (LT.fromStrict . symbolText . unObj) . sortTys
+
+unObj :: Sort -> Symbol
+unObj FInt     = "Int"
+unObj (FObj s) = s
+unObj s        = error $ "unObj: " ++ show s
diff --git a/src/Test/Target/Types.hs b/src/Test/Target/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Types.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+module Test.Target.Types where
+
+import qualified Control.Monad.Catch           as Ex
+import qualified Data.Text                     as T
+import           Data.Typeable
+
+import           Language.Fixpoint.SmtLib2
+import           Language.Fixpoint.Types
+import           Language.Haskell.Liquid.Types
+
+import           GHC
+
+
+data TargetException
+  = SmtFailedToProduceOutput
+  | SmtError String
+  | ExpectedValues Response
+  | PreconditionCheckFailed String
+  | EvalError String
+  deriving Typeable
+
+instance Show TargetException where
+  show SmtFailedToProduceOutput
+    = "The SMT solver was unable to produce an output value."
+  show (SmtError s)
+    = "Unexpected error from the solver: " ++ s
+  show (ExpectedValues r)
+    = "Expected a Values response from the solver, got: " ++ show r
+  show (PreconditionCheckFailed e)
+    = "The pre-condition check for a generated function failed: " ++ e
+  show (EvalError s)
+    = "Couldn't evaluate a concrete refinement: " ++ s
+
+instance Ex.Exception TargetException
+
+ensureValues :: Ex.MonadThrow m => m Response -> m Response
+ensureValues x = do
+  a <- x
+  case a of
+    Values _ -> return a
+    r        -> Ex.throwM $ ExpectedValues r
+
+type Constraint = [Pred]
+type Variable   = ( Symbol -- the name
+                  , Sort   -- the `Sort'
+                  )
+type Value      = T.Text
+
+instance Symbolic Variable where
+  symbol (x, _) = symbol x
+
+instance SMTLIB2 Constraint where
+  smt2 = smt2 . PAnd
+
+type DataConEnv = [(Symbol, SpecType)]
+type MeasureEnv = [Measure SpecType DataCon]
+
+boolsort, choicesort :: Sort
+boolsort   = FObj "Bool"
+choicesort = FObj "CHOICE"
+
+data Result = Passed !Int
+            | Failed !String
+            | Errored !String
+            deriving (Show)
+
+-- resultPassed (Passed i) = i
diff --git a/src/Test/Target/Util.hs b/src/Test/Target/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Target/Util.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ParallelListComp #-}
+module Test.Target.Util where
+
+import           Control.Applicative
+import           Control.Monad.IO.Class
+import           Data.List
+import           Data.Maybe
+import           Data.Monoid
+import           Data.Generics                    (everywhere, mkT)
+import           Debug.Trace
+
+import qualified DynFlags as GHC
+import qualified GhcMonad as GHC
+import qualified GHC
+import qualified GHC.Exts as GHC
+import qualified GHC.Paths
+import qualified HscTypes as GHC
+
+import           Language.Fixpoint.Types          hiding (prop)
+import           Language.Haskell.Liquid.CmdLine
+import           Language.Haskell.Liquid.GhcInterface
+import           Language.Haskell.Liquid.PredType
+import           Language.Haskell.Liquid.RefType
+import           Language.Haskell.Liquid.Types    hiding (var)
+
+type Depth = Int
+
+io ::  MonadIO m => IO a -> m a
+io = liftIO
+
+myTrace :: Show a => String -> a -> a
+myTrace s x = trace (s ++ ": " ++ show x) x
+
+reft :: SpecType -> Reft
+reft = toReft . rt_reft
+
+data HList (a :: [*]) where
+  Nil   :: HList '[]
+  (:::) :: a -> HList bs -> HList (a ': bs)
+
+instance AllHave Show as => Show (HList as) where
+  show Nil         = "()"
+  show (x ::: Nil) = show x
+  show (x ::: xs)  = show x ++ ", " ++ show xs
+
+type family Map (f :: a -> b) (xs :: [a]) :: [b] where
+  Map f '[]       = '[]
+  Map f (x ': xs) = f x ': Map f xs
+
+type family Constraints (cs :: [GHC.Constraint]) :: GHC.Constraint
+type instance Constraints '[]       = ()
+type instance Constraints (c ': cs) = (c, Constraints cs)
+
+type AllHave (c :: k -> GHC.Constraint) (xs :: [k]) = Constraints (Map c xs)
+
+type family Args a where
+  Args (a -> b) = a ': Args b
+  Args a        = '[]
+
+type family Res a where
+  Res (a -> b) = Res b
+  Res a        = a
+
+safeFromJust :: String -> Maybe a -> a
+safeFromJust msg Nothing  = error $ "safeFromJust: " ++ msg
+safeFromJust _   (Just x) = x
+
+applyPreds :: SpecType -> SpecType -> [(Symbol,SpecType)]
+applyPreds sp' dc = zip xs (map tx ts)
+  where
+    sp = removePreds <$> sp'
+    removePreds (U r _ _) = U r mempty mempty
+    (as, ps, _, t) = bkUniv dc
+    (xs, ts, _)    = bkArrow . snd $ bkClass t
+    -- args  = reverse tyArgs
+    su    = [(tv, toRSort t, t) | tv <- as | t <- rt_args sp]
+    sup   = [(p, r) | p <- ps | r <- rt_pargs sp]
+    tx    = (\t -> replacePreds "applyPreds" t sup) . everywhere (mkT $ propPsToProp sup) . subsTyVars_meet su
+
+propPsToProp
+  :: [(PVar t3, Ref t (UReft t2) t1)]
+     -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1
+propPsToProp su r = foldr propPToProp r su
+
+propPToProp
+  :: (PVar t3, Ref t (UReft t2) t1)
+     -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1
+propPToProp (p, r) (RPropP _ (U _ (Pr [up]) _))
+  | pname p == pname up
+  = r
+propPToProp _ m = m
+
+
+stripQuals :: SpecType -> SpecType
+stripQuals = snd . bkClass . fourth4 . bkUniv
+
+fourth4 :: (t, t1, t2, t3) -> t3
+fourth4 (_,_,_,d) = d
+
+getSpec :: FilePath -> IO GhcSpec
+getSpec target
+  = do cfg  <- mkOpts mempty
+       info <- getGhcInfo cfg target
+       case info of
+         Left err -> error $ show err
+         Right i  -> return $ spec i
+
+runGhc :: GHC.Ghc a -> IO a
+runGhc x = GHC.runGhc (Just GHC.Paths.libdir) $ do
+             df <- GHC.getSessionDynFlags
+             let df' = df { GHC.ghcMode   = GHC.CompManager
+                          , GHC.ghcLink   = GHC.NoLink --GHC.LinkInMemory
+                          , GHC.hscTarget = GHC.HscNothing --GHC.HscInterpreted
+                          -- , GHC.optLevel  = 0 --2
+                          , GHC.log_action = \_ _ _ _ _ -> return ()
+                          , GHC.importPaths = GHC.importPaths df
+                          } `GHC.gopt_set` GHC.Opt_ImplicitImportQualified
+                            `GHC.xopt_set` GHC.Opt_MagicHash
+             _ <- GHC.setSessionDynFlags df'
+             x
+
+loadModule :: FilePath -> GHC.Ghc GHC.ModSummary
+loadModule f = do target <- GHC.guessTarget f Nothing
+                  --lcheck <- GHC.guessTarget "src/Test/Target.hs" Nothing
+                  GHC.setTargets [target] -- [target,lcheck]
+                  _ <- GHC.load GHC.LoadAllTargets
+                  modGraph <- GHC.getModuleGraph
+                  let m = fromJust $ find ((==f) . GHC.msHsFilePath) modGraph
+                  GHC.setContext [ GHC.IIModule (GHC.ms_mod_name m)
+                                 --, GHC.IIDecl $ GHC.simpleImportDecl
+                                 --             $ GHC.mkModuleName "Test.Target"
+                                 ]
+                  return m
diff --git a/target.cabal b/target.cabal
new file mode 100644
--- /dev/null
+++ b/target.cabal
@@ -0,0 +1,161 @@
+name:                target
+version:             0.1.0.0
+synopsis:            Generate test-suites from refinement types.
+
+description:         Target is a library for testing Haskell functions based on
+                     properties encoded as refinement types.
+                     .
+                     The programmer specifies the expected behavior of a
+                     function with a refinement type, and Target then checks
+                     that the function satisfies the specification by
+                     enumerating valid inputs up to some size, calling the
+                     function, and validating the output. Target excels when the
+                     space of valid inputs is a sparse subset of all possible
+                     inputs, e.g. when dealing with dataypes with complex
+                     invariants like red-black trees.
+                     .
+                     "Test.Target" is the main entry point and should contain
+                     everything you need to use Target with types from the
+                     "Prelude". "Test.Target.Targetable" will also be useful if
+                     you want to test functions that use other types.
+                     .
+                     For information on how to /specify/ interesting properties
+                     with refinement types, we have a series of
+                     <http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/categories/basic/ blog posts>
+                     as well as an
+                     <http://github.com/ucsd-progsys/liquidhaskell/tree/master/docs/tutorial evolving tutorial>.
+                     Target uses the same specification language as LiquidHaskell,
+                     so the examples should carry over.
+                     .
+                     Finally, Target requires either <https://z3.codeplex.com/ Z3> 
+                     (@>=4.3@) or <http://cvc4.cs.nyu.edu/web/ CVC4> (@>=1.4@) to 
+                     be present in your @PATH@.
+
+license:             MIT
+license-file:        LICENSE
+author:              Eric Seidel
+maintainer:          eseidel@cs.ucsd.edu
+category:            Testing
+build-type:          Simple
+cabal-version:       >=1.10
+
+source-repository head
+  type:     git
+  location: git://github.com/gridaphobe/target.git
+
+library
+  default-language:    Haskell2010
+  hs-source-dirs:      src
+  ghc-options:         -Wall -fno-warn-name-shadowing -fno-warn-orphans
+  ghc-prof-options:    -fprof-auto
+  exposed-modules:     Test.Target,
+                       Test.Target.Eval,
+                       Test.Target.Expr,
+                       Test.Target.Monad,
+                       Test.Target.Targetable,
+                       Test.Target.Targetable.Function,
+                       Test.Target.Testable,
+                       Test.Target.Types,
+                       Test.Target.Util
+
+  build-depends:       base >=4.6 && <5
+                     , containers >= 0.5.0.0
+                     , directory >= 1.2.0.1
+                     , exceptions >= 0.6
+                     , filepath >= 1.3.0.1
+                     , ghc >= 7.8.3
+                     , ghc-paths
+                     , liquid-fixpoint >= 0.2.1.1
+                     , liquidhaskell >= 0.2
+                     , mtl >= 2.1.2
+                     , pretty
+                     , process
+                     , syb >= 0.4.2
+                     , tagged >= 0.7
+                     , template-haskell
+                     , text >= 1.0
+                     , text-format
+                     , transformers >= 0.3
+                     , unordered-containers >= 0.2.3.0
+                     , vector
+
+benchmark bench
+  type:                exitcode-stdio-1.0
+  default-language:    Haskell2010
+  hs-source-dirs:      bench
+  ghc-options:         -O2
+  ghc-prof-options:    -fprof-auto
+  main-is:             Main.hs
+  build-depends:       base,
+                       aeson,
+                       bytestring,
+                       cassava,
+                       SafeSemaphore,
+                       vector,
+                       xml-conduit,
+                       data-timeout >= 0.3,
+                       -- for XMonad
+                       -- X11,
+                       containers,
+                       random,
+                       tagged,
+                       ghc,
+                       unordered-containers,
+                       mtl,
+                       -- for Data.Map
+                       deepseq,
+                       --
+                       --criterion,
+                       --hastache,
+                       --statistics,
+                       time,
+                       target,
+                       template-haskell,
+                       liquidhaskell >= 0.2,
+                       liquid-fixpoint,
+                       QuickCheck >= 2.6,
+                       smallcheck >= 1.1
+
+test-suite test
+  type:                exitcode-stdio-1.0
+  default-language:    Haskell2010
+  hs-source-dirs:      test
+  ghc-options:         -O2
+  main-is:             Main.hs
+  c-sources:           cbits/fpstring.c
+  include-dirs:        include
+  includes:            fpstring.h
+  build-depends:       base,
+                       target,
+                       ghc,
+                       tasty >= 0.8,
+                       tasty-hunit >= 0.8,
+                       -- for Data.Map
+                       containers,
+                       deepseq,
+                       -- for ByteString
+                       array,
+                       tagged,
+                       mtl,
+                       ghc-prim,
+                       liquid-fixpoint,
+                       liquidhaskell,
+                       template-haskell,
+                       unordered-containers
+
+-- executable liquid-check
+--   default-language: Haskell2010
+--   hs-source-dirs: bin
+--   main-is:        Target.hs
+--   build-depends:  base,
+--                   Target,
+--                   liquid-fixpoint,
+--                   data-timeout >= 0.3,
+--                   ghc,
+--                   ghc-paths,
+--                   directory,
+--                   filepath,
+--                   process,
+--                   text,
+--                   time,
+--                   transformers
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Main where
+
+import           Control.Exception
+import           GHC.IO.Handle
+import qualified Language.Haskell.TH as TH
+import           System.IO
+import           Test.Tasty
+import           Test.Tasty.HUnit
+
+import           Test.Target
+
+-- import qualified Data.ByteString.Internal as ByteString
+import qualified HOFs
+import           List                     (List)
+import qualified List
+import qualified MapTest                  as Map
+import qualified RBTree
+import qualified RBTreeTest               as RBTree
+
+
+main = defaultMain tests
+
+tests, pos, neg :: TestTree
+
+tests = testGroup "Tests" [pos, neg]
+
+pos = testGroup "Pos" $
+  [ mkSuccess (List.insert :: Int -> List Int -> List Int)
+      'List.insert "test/List.hs" 3
+  -- FIXME: doesn't work with SMT-based checking of post-condition
+  , mkSuccess List.mymap 'List.mymap "test/List.hs" 3
+  ]
+  ++ [ mkSuccess f name "test/HOFs.hs" 3   | (name, T f) <- hofsTests]
+  ++ [ mkSuccess f name "test/RBTree.hs" 5 | (name, T f) <- RBTree.liquidTests]
+  ++ [ mkSuccess f name "test/Map.hs" 4    | (name, T f) <- Map.liquidTests]
+  --FIXME: need a better solution for checking equality that respects custom Eq instances
+  -- ++ [ mkSuccess f ("Data.ByteString.Internal."++name) "test/Data/ByteString/Internal.hs" 4 | (name, T f) <- ByteString.liquidTests]
+
+neg = testGroup "Neg" $
+  [ mkFailure (List.insert_bad :: Int -> List Int -> List Int)
+      'List.insert "test/List.hs" 3
+  ]
+  ++ [ mkFailure f name "test/HOFs.hs" 3   | (name, T f) <- hofsTests_bad]
+  ++ [ mkFailure f name "test/RBTree.hs" 5 | (name, T f) <- RBTree.liquidTests_bad]
+  ++ [ mkFailure f name "test/Map.hs" 4    | (name, T f) <- Map.liquidTests_bad]
+
+-- liquidTests, liquidTests_bad :: [(String,Test)]
+hofsTests     = [('HOFs.foo, T HOFs.foo), ('HOFs.list_foo, T HOFs.list_foo)]
+hofsTests_bad = [('HOFs.foo, T HOFs.foo_bad), ('HOFs.list_foo, T HOFs.list_foo_bad)]
+
+mkSuccess :: Testable f => f -> TH.Name -> String -> Int -> TestTree
+mkSuccess f n fp d
+  = testCase (show n ++ "/" ++ show d) $ shouldSucceed d f n fp
+
+mkFailure :: Testable f => f -> TH.Name -> String -> Int -> TestTree
+mkFailure f n fp d
+  = testCase (show n ++ "/" ++ show d) $ shouldFail d f n fp
+
+shouldSucceed d f name file
+  = do r <- targetResultWith f name file (defaultOpts {depth = d})
+       assertString $ case r of
+                       Passed _ -> ""
+                       Failed s -> "Unexpected counter-example: " ++ s
+                       Errored s -> "Unexpected error: " ++ s
+
+shouldFail d f name file
+  = do r <- targetResultWith f name file (defaultOpts {depth = d})
+       assertBool "Expected counter-example" $ case r of
+                                               Passed _ -> False
+                                               _        -> True
+