target 0.1.1.0 → 0.1.2.0
raw patch · 12 files changed
+180/−156 lines, 12 filesdep +th-liftdep ~liquid-fixpointdep ~liquidhaskell
Dependencies added: th-lift
Dependency ranges changed: liquid-fixpoint, liquidhaskell
Files
- bench/Main.hs +1/−1
- cbits/fpstring.c +0/−82
- src/Test/Target.hs +28/−14
- src/Test/Target/Eval.hs +4/−4
- src/Test/Target/Monad.hs +16/−3
- src/Test/Target/TH.hs +52/−0
- src/Test/Target/Targetable.hs +5/−5
- src/Test/Target/Targetable/Function.hs +4/−4
- src/Test/Target/Testable.hs +12/−12
- src/Test/Target/Util.hs +41/−17
- target.cabal +8/−6
- test/Main.hs +9/−8
bench/Main.hs view
@@ -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")
− cbits/fpstring.c
@@ -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;-}
src/Test/Target.hs view
@@ -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
src/Test/Target/Eval.hs view
@@ -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]
src/Test/Target/Monad.hs view
@@ -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]
+ src/Test/Target/TH.hs view
@@ -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
src/Test/Target/Targetable.hs view
@@ -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
src/Test/Target/Targetable/Function.hs view
@@ -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'
src/Test/Target/Testable.hs view
@@ -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 };
src/Test/Target/Util.hs view
@@ -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
target.cabal view
@@ -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,
test/Main.hs view
@@ -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"]}