diff --git a/bench/Main.hs b/bench/Main.hs --- a/bench/Main.hs +++ b/bench/Main.hs @@ -178,7 +178,7 @@ -- 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)) + targetResultWith f (show n) m (mkOpts d max)) where mkOpts d max = defaultOpts { logging = False, depth = d, maxSuccess = Just max, scDepth = True } checkSmall p n = checkMany (show n++"/SmallCheck") diff --git a/cbits/fpstring.c b/cbits/fpstring.c deleted file mode 100644 --- a/cbits/fpstring.c +++ /dev/null @@ -1,82 +0,0 @@ -/* - * 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 --- a/src/Test/Target.hs +++ b/src/Test/Target.hs @@ -1,13 +1,17 @@ {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE ViewPatterns #-} module Test.Target - ( target, targetResult, targetWith, targetResultWith, targetResultWithStr - -- , targetTH - , Result(..), Testable + ( target, targetResult, targetWith, targetResultWith + , targetTH, targetResultTH, targetWithTH, targetResultWithTH + , Result(..), Testable, Targetable(..) , TargetOpts(..), defaultOpts , Test(..) + , monomorphic ) where + import Control.Applicative import Control.Monad import Control.Monad.Catch @@ -20,9 +24,10 @@ import Language.Fixpoint.SmtLib2 hiding (verbose) import Test.Target.Monad -import Test.Target.Targetable () +import Test.Target.Targetable (Targetable(..)) import Test.Target.Targetable.Function () import Test.Target.Testable +import Test.Target.TH import Test.Target.Types import Test.Target.Util @@ -30,24 +35,30 @@ -- inputs and calling the function. target :: Testable f => f -- ^ the function - -> TH.Name -- ^ the name of the function + -> String -- ^ 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.Name -> FilePath -> TH.ExpQ +targetTH f m = [| target $(monomorphic f) $(TH.stringE $ show f) m |] + -- 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 :: Testable f => f -> String -> FilePath -> IO Result targetResult f name path = targetResultWith f name path defaultOpts +targetResultTH :: TH.Name -> FilePath -> TH.ExpQ +targetResultTH f m = [| targetResult $(monomorphic f) $(TH.stringE $ show f) m |] + -- | Like 'target', but accepts options to control the enumeration depth, -- solver, and verbosity. -targetWith :: Testable f => f -> TH.Name -> FilePath -> TargetOpts -> IO () +targetWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO () targetWith f name path opts = do res <- targetResultWith f name path opts case res of @@ -55,22 +66,25 @@ 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 = targetResultWithStr f name path opts +targetWithTH :: TH.Name -> FilePath -> TargetOpts -> TH.ExpQ +targetWithTH f m opts = [| targetWith $(monomorphic f) $(TH.stringE $ show f) m opts |] -targetResultWithStr :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result -targetResultWithStr f name path opts +-- | Like 'targetWith', but returns the 'Result' instead of printing to standard out. +targetResultWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result +targetResultWith f name path opts = do when (verbose opts) $ printf "Testing %s\n" name - sp <- getSpec path + sp <- getSpec (ghcOpts opts) 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 + mkContext = if logging opts then flip makeContext (".target/" ++ name) else makeContextNoLog killContext ctx = terminateProcess (pId ctx) >> cleanupContext ctx + +targetResultWithTH :: TH.Name -> FilePath -> TargetOpts -> TH.ExpQ +targetResultWithTH f m opts = [| targetResultWith $(monomorphic f) $(TH.stringE $ show f) m opts |] data Test = forall t. Testable t => T t diff --git a/src/Test/Target/Eval.hs b/src/Test/Target/Eval.hs --- a/src/Test/Target/Eval.hs +++ b/src/Test/Target/Eval.hs @@ -32,8 +32,8 @@ -- | 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 ] +evalWith m (Reft (v, Refa p)) x + = evalPred p (M.insert v x m) evalPred :: Pred -> M.HashMap Symbol Expr -> Target Bool evalPred PTrue _ = return True @@ -112,7 +112,7 @@ evalSet f es = throwM $ EvalError $ printf "evalSet(%s, %s)" (show f) (show es) evalBody - :: Language.Haskell.Liquid.Types.Def ctor + :: Language.Haskell.Liquid.Types.Def ty ctor -> [Expr] -> M.HashMap Symbol Expr -> Target Expr evalBody eq xs env = go $ body eq where @@ -125,7 +125,7 @@ --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 + su = mkSubst $ zip (map fst (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] diff --git a/src/Test/Target/Monad.hs b/src/Test/Target/Monad.hs --- a/src/Test/Target/Monad.hs +++ b/src/Test/Target/Monad.hs @@ -2,6 +2,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TemplateHaskell #-} module Test.Target.Monad ( whenVerbose , noteUsed @@ -35,6 +36,7 @@ import Data.List hiding (sort) import Data.Monoid import qualified Data.Text.Lazy as LT +import Language.Haskell.TH.Lift import System.IO.Unsafe import Text.Printf @@ -96,17 +98,20 @@ -- enumerate the whole input space , scDepth :: !Bool -- ^ whether to use SmallCheck's notion of depth + , ghcOpts :: ![String] + -- ^ extra options to pass to GHC } defaultOpts :: TargetOpts defaultOpts = TargetOpts - { depth = 5 + { depth = 3 , solver = Z3 , verbose = False , logging = True , keepGoing = False , maxSuccess = Nothing - , scDepth = False + , scDepth = True + , ghcOpts = [] } data TargetState = TargetState @@ -206,10 +211,11 @@ lookupCtor c = do mt <- lookup c <$> gets ctorEnv m <- gets filePath + o <- asks ghcOpts case mt of Just t -> return t Nothing -> do - t <- io $ runGhc $ do + t <- io $ runGhc o $ do _ <- loadModule m t <- GHC.exprType (printf "(%s)" (symbolString c)) return (ofType t) @@ -268,3 +274,10 @@ noteUsed x return (snd x) + + +---------------------------------------------------------------------- +-- Template Haskell nonsense, MUST be at the bottom of the file +---------------------------------------------------------------------- + +deriveLiftMany [''SMTSolver, ''TargetOpts] diff --git a/src/Test/Target/TH.hs b/src/Test/Target/TH.hs new file mode 100644 --- /dev/null +++ b/src/Test/Target/TH.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} + +module Test.Target.TH where + +import Control.Monad +import qualified Language.Haskell.TH as TH + +---------------------------------------------------------------------- +-- Testing Polymorphic Functions (courtesy of QuickCheck) +---------------------------------------------------------------------- + +type Error = forall a. String -> a + +-- | Monomorphise an arbitrary property by defaulting all type variables to 'Integer'. +-- +-- For example, if @f@ has type @'Ord' a => [a] -> [a]@ +-- then @$('monomorphic' 'f)@ has type @['Integer'] -> ['Integer']@. +-- +-- If you want to use 'monomorphic' in the same file where you defined the +-- property, the same scoping problems pop up as in 'quickCheckAll': +-- see the note there about @return []@. +monomorphic :: TH.Name -> TH.ExpQ +monomorphic t = do + ty0 <- fmap infoType (TH.reify t) + let err msg = error $ msg ++ ": " ++ TH.pprint ty0 + (polys, ctx, ty) <- deconstructType err ty0 + case polys of + [] -> return (TH.VarE t) + _ -> do + integer <- [t| Integer |] + ty' <- monomorphiseType err integer ty + return (TH.SigE (TH.VarE t) ty') + +infoType :: TH.Info -> TH.Type +infoType (TH.ClassOpI _ ty _ _) = ty +infoType (TH.DataConI _ ty _ _) = ty +infoType (TH.VarI _ ty _ _) = ty + +deconstructType :: Error -> TH.Type -> TH.Q ([TH.Name], TH.Cxt, TH.Type) +deconstructType err ty0@(TH.ForallT xs ctx ty) = do + let plain (TH.PlainTV _) = True + plain _ = False + unless (all plain xs) $ err "Higher-kinded type variables in type" + return (map (\(TH.PlainTV x) -> x) xs, ctx, ty) +deconstructType _ ty = return ([], [], ty) + +monomorphiseType :: Error -> TH.Type -> TH.Type -> TH.TypeQ +monomorphiseType err mono ty@(TH.VarT n) = return mono +monomorphiseType err mono (TH.AppT t1 t2) = liftM2 TH.AppT (monomorphiseType err mono t1) (monomorphiseType err mono t2) +monomorphiseType err mono ty@(TH.ForallT _ _ _) = err $ "Higher-ranked type" +monomorphiseType err mono ty = return ty diff --git a/src/Test/Target/Targetable.hs b/src/Test/Target/Targetable.hs --- a/src/Test/Target/Targetable.hs +++ b/src/Test/Target/Targetable.hs @@ -30,7 +30,7 @@ import Data.Word (Word8) import GHC.Generics -import Language.Fixpoint.Types hiding (prop, ofReft) +import Language.Fixpoint.Types hiding (prop, ofReft, reft) import Language.Haskell.Liquid.RefType import Language.Haskell.Liquid.Types hiding (var) @@ -126,8 +126,8 @@ Nothing -> return () let x = app c vs t <- lookupCtor c - let (xs, _, rt) = bkArrowDeep t - su = mkSubst $ zip (map symbol xs) vs + 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 @@ -179,9 +179,9 @@ -- | Given a refinement @{v | p}@ and an expression @e@, construct -- the predicate @p[e/v]@. ofReft :: Reft -> Expr -> Pred -ofReft (Reft (v, rs)) e +ofReft (Reft (v, Refa p)) e = let x = mkSubst [(v, e)] - in pAnd [subst x p | RConc p <- rs] + in subst x p -------------------------------------------------------------------------------- --- Instances diff --git a/src/Test/Target/Targetable/Function.hs b/src/Test/Target/Targetable/Function.hs --- a/src/Test/Target/Targetable/Function.hs +++ b/src/Test/Target/Targetable/Function.hs @@ -22,7 +22,7 @@ import qualified Data.Text as T import qualified GHC import Language.Fixpoint.SmtLib2 -import Language.Fixpoint.Types hiding (ofReft) +import Language.Fixpoint.Types hiding (ofReft, reft) import Language.Haskell.Liquid.GhcMisc (qualifiedNameSymbol) import Language.Haskell.Liquid.RefType (addTyConInfo, rTypeSort) import Language.Haskell.Liquid.Types hiding (var) @@ -56,7 +56,7 @@ stitchFun :: forall f. (Targetable (Res f)) => Proxy f -> SpecType -> Target ([Expr] -> Res f) -stitchFun _ (bkArrowDeep . stripQuals -> (vs, tis, to)) +stitchFun _ (bkArrowDeep . stripQuals -> (vs, tis, _, to)) = do mref <- io $ newIORef [] d <- asks depth state' <- get @@ -82,7 +82,7 @@ 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 + mapM_ (\x -> io . smtWrite ctx $ makeDecl (symbol x) (snd x)) vs cs <- gets constraints mapM_ (\c -> io . command ctx $ Assert Nothing c) cs @@ -98,7 +98,7 @@ genExpr :: Expr -> Target Symbol genExpr (EApp (val -> c) es) = do xes <- mapM genExpr es - (xs, _, to) <- bkArrowDeep . stripQuals <$> lookupCtor c + (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' diff --git a/src/Test/Target/Testable.hs b/src/Test/Target/Testable.hs --- a/src/Test/Target/Testable.hs +++ b/src/Test/Target/Testable.hs @@ -29,7 +29,7 @@ import Text.Printf import Language.Fixpoint.SmtLib2 -import Language.Fixpoint.Types +import Language.Fixpoint.Types hiding (Result) import Language.Haskell.Liquid.RefType import Language.Haskell.Liquid.Types hiding (Result (..), env, var) @@ -49,7 +49,7 @@ = do d <- asks depth vs <- queryArgs f d t setup - let (xs, tis, to) = bkArrowDeep $ stripQuals t + 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 @@ -146,12 +146,6 @@ 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 @@ -169,19 +163,25 @@ 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) + s -> defSort (LT.toStrict $ smt2Sort s) ("Int" :: T.Text) -- declare constructors cts <- gets constructors - mapM_ (\ (c,t) -> io . command ctx $ makeDecl (symbol c) t) cts + mapM_ (\ (c,t) -> io $ smtWrite 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 + let defVar (x,t) = io $ smtWrite ctx (makeDecl x (arrowize t)) + mapM_ defVar vs -- declare measures ms <- gets measEnv - mapM_ (\m -> io . command ctx $ makeDecl (val $ name m) (rTypeSort emb $ sort m)) ms + let defFun x t = io $ smtWrite ctx (makeDecl x t) + forM_ ms $ \m -> do + let x = val (name m) + if x `M.member` smt_set_funs + then return () + else defFun x (rTypeSort emb (sort m)) -- assert constraints cs <- gets constraints --mapM_ (\c -> do {i <- gets seed; modify $ \s@(GS {..}) -> s { seed = seed + 1 }; diff --git a/src/Test/Target/Util.hs b/src/Test/Target/Util.hs --- a/src/Test/Target/Util.hs +++ b/src/Test/Target/Util.hs @@ -6,6 +6,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ParallelListComp #-} +{-# LANGUAGE OverloadedStrings #-} module Test.Target.Util where import Control.Applicative @@ -14,6 +15,8 @@ import Data.Maybe import Data.Monoid import Data.Generics (everywhere, mkT) +import Data.Text.Format hiding (print) +import qualified Data.Text.Lazy as LT import Debug.Trace import qualified DynFlags as GHC @@ -23,6 +26,7 @@ import qualified GHC.Paths import qualified HscTypes as GHC +import Language.Fixpoint.SmtLib2 import Language.Fixpoint.Types hiding (prop) import Language.Haskell.Liquid.CmdLine import Language.Haskell.Liquid.GhcInterface @@ -68,6 +72,26 @@ Res (a -> b) = Res b Res a = a +-- liquid-fixpoint started encoding `FObj s` as `Int` in 0.3.0.0, but we +-- want to preserve the type aliases for easier debugging.. so here's a +-- copy of the SMTLIB2 Sort instance.. +smt2Sort :: Sort -> LT.Text +smt2Sort FInt = "Int" +smt2Sort (FApp t []) | t == intFTyCon = "Int" +smt2Sort (FApp t []) | t == boolFTyCon = "Bool" +smt2Sort (FApp t [FApp ts _,_]) | t == appFTyCon && fTyconSymbol ts == "Set_Set" = "Set" +smt2Sort (FObj s) = smt2 s +smt2Sort s@(FFunc _ _) = error $ "smt2 FFunc: " ++ show s +smt2Sort _ = "Int" + +makeDecl :: Symbol -> Sort -> LT.Text +-- FIXME: hack.. +makeDecl x (FFunc _ ts) + = format "(declare-fun {} ({}) {})" + (smt2 x, LT.unwords (map smt2Sort (init ts)), smt2Sort (last ts)) +makeDecl x t + = format "(declare-const {} {})" (smt2 x, smt2Sort t) + safeFromJust :: String -> Maybe a -> a safeFromJust msg Nothing = error $ "safeFromJust: " ++ msg safeFromJust _ (Just x) = x @@ -78,7 +102,7 @@ sp = removePreds <$> sp' removePreds (U r _ _) = U r mempty mempty (as, ps, _, t) = bkUniv dc - (xs, ts, _) = bkArrow . snd $ bkClass t + (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] @@ -104,27 +128,27 @@ fourth4 :: (t, t1, t2, t3) -> t3 fourth4 (_,_,_,d) = d -getSpec :: FilePath -> IO GhcSpec -getSpec target +getSpec :: [String] -> FilePath -> IO GhcSpec +getSpec opts target = do cfg <- mkOpts mempty - info <- getGhcInfo cfg target + info <- getGhcInfo (cfg {ghcOptions = opts}) 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 = "bench" : GHC.importPaths df - } `GHC.gopt_set` GHC.Opt_ImplicitImportQualified - `GHC.xopt_set` GHC.Opt_MagicHash - _ <- GHC.setSessionDynFlags df' - x +runGhc :: [String] -> GHC.Ghc a -> IO a +runGhc o 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.gopt_set` GHC.Opt_ImplicitImportQualified + `GHC.xopt_set` GHC.Opt_MagicHash + (df'',_,_) <- GHC.parseDynamicFlags df' (map GHC.noLoc o) + _ <- GHC.setSessionDynFlags df'' + x loadModule :: FilePath -> GHC.Ghc GHC.ModSummary loadModule f = do target <- GHC.guessTarget f Nothing diff --git a/target.cabal b/target.cabal --- a/target.cabal +++ b/target.cabal @@ -1,5 +1,5 @@ name: target -version: 0.1.1.0 +version: 0.1.2.0 synopsis: Generate test-suites from refinement types. description: Target is a library for testing Haskell functions based on @@ -55,6 +55,7 @@ Test.Target.Targetable, Test.Target.Targetable.Function, Test.Target.Testable, + Test.Target.TH, Test.Target.Types, Test.Target.Util @@ -65,8 +66,8 @@ , filepath >= 1.3.0.1 , ghc >= 7.8.3 , ghc-paths - , liquid-fixpoint >= 0.2.1.1 - , liquidhaskell >= 0.2 + , liquid-fixpoint >= 0.3 + , liquidhaskell >= 0.4 , mtl >= 2.1.2 , pretty , process @@ -75,6 +76,7 @@ , template-haskell , text >= 1.0 , text-format + , th-lift , transformers >= 0.3 , unordered-containers >= 0.2.3.0 , vector @@ -122,9 +124,9 @@ hs-source-dirs: test ghc-options: -O2 main-is: Main.hs - c-sources: cbits/fpstring.c - include-dirs: include - includes: fpstring.h + --c-sources: cbits/fpstring.c + --include-dirs: include + --includes: fpstring.h build-depends: base, target, ghc, diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -32,8 +32,8 @@ , 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] + ++ [ mkSuccess f name "test/RBTree.hs" 7 | (name, T f) <- RBTree.liquidTests] + ++ [ mkSuccess f name "test/Map.hs" 5 | (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] @@ -42,8 +42,8 @@ '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] + ++ [ mkFailure f name "test/RBTree.hs" 7 | (name, T f) <- RBTree.liquidTests_bad] + ++ [ mkFailure f name "test/Map.hs" 5 | (name, T f) <- Map.liquidTests_bad] -- liquidTests, liquidTests_bad :: [(String,Test)] hofsTests = [('HOFs.foo, T HOFs.foo), ('HOFs.list_foo, T HOFs.list_foo)] @@ -51,22 +51,23 @@ mkSuccess :: Testable f => f -> TH.Name -> String -> Int -> TestTree mkSuccess f n fp d - = testCase (show n ++ "/" ++ show d) $ shouldSucceed d f n fp + = testCase (show n ++ "/" ++ show d) $ shouldSucceed d f (show 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 + = testCase (show n ++ "/" ++ show d) $ shouldFail d f (show n) fp shouldSucceed d f name file - = do r <- targetResultWith f name file (defaultOpts {depth = d}) + = do r <- targetResultWith f name file (testOpts {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}) + = do r <- targetResultWith f name file (testOpts {depth = d}) assertBool "Expected counter-example" $ case r of Passed _ -> False _ -> True +testOpts = defaultOpts {ghcOpts = ["-isrc", "-package", "ghc"]}