diff --git a/Test/Feat/Driver.hs b/Test/Feat/Driver.hs --- a/Test/Feat/Driver.hs +++ b/Test/Feat/Driver.hs @@ -5,14 +5,13 @@ module Test.Feat.Driver( -- * Simple test driver test - , Result - , counterexamples -- * Test driver with show/readable options , testOptions , Options(..) , defOptions -- * Extremely flexible test driver , testFlex + , Result(..) , FlexibleOptions(..) , FlexOptions(..) , defFlex @@ -44,22 +43,18 @@ -- | FlexOptions data FlexOptions a = FlexOptions - { fIO :: IO Bool -> IO (Result a) -- ^ The whole execution of the test is sent through this function. + { fIO :: IO Bool -> IO (Result,[a]) -- ^ The whole execution of the test is sent through this function. , fReport :: a -> IO Bool -- ^ Applied to each found counterexample, return False to stop testing , fOutput :: String -> IO () -- ^ Print text , fProcess :: Enumerate a -> Enumerate a -- ^ Applied to the enumeration before running , fEnum :: Enumerate a -- ^ The base enumeration to use, before applying @fProcess@. } -data Result a = Exhausted [a] -- ^ Reached max size - | Quota [a] -- ^ Reached max number of counterexamples - | TimedOut [a] - deriving Show - -counterexamples :: Result a -> [a] -counterexamples (Exhausted xs) = xs -counterexamples (Quota xs) = xs -counterexamples (TimedOut xs) = xs +data Result = Exhausted -- ^ Reached max size + | Quota -- ^ Reached max number of counterexamples + | TimedOut + | Other + deriving Show -- | 60 seconds timeout, maximum size of 100, bound of 100000 tests per size defOptions :: Options @@ -96,7 +91,7 @@ doIO io = do mb <- maybe (fmap Just io) (\t -> timeout (t*1000000) io) (oTimeoutSec o) res <- readIORef res - return $ maybe (TimedOut res) (\b -> if b then Exhausted res else Quota res) mb + return $ maybe (TimedOut,res) (\b -> if b then (Exhausted,res) else (Quota,res)) mb skip = maybe id (\(i,n) e -> skipping e i n) (oSkipping o) bound = maybe id (\n e -> bounded e n) (oBounded o) sizes = maybe id (\bs e -> sizeRange e bs) (oSizeFromTo o) @@ -108,16 +103,18 @@ , fEnum = e } --- | Test with default options ('defOptions'). -test :: Enumerable a => (a -> Bool) -> IO (Result a) -test = testFlex defFlex +-- | Test with default options ('defOptions'). Returns a list of counterexamples +test :: Enumerable a => (a -> Bool) -> IO [a] +test = testOptions defOptions --- | Test with basic options. -testOptions :: Enumerable a => Options -> (a -> Bool) -> IO (Result a) -testOptions = testFlex . toFlex +-- | Test with basic options. Returns a list of counterexamples. +testOptions :: Enumerable a => Options -> (a -> Bool) -> IO [a] +testOptions o p = fmap snd $ testFlex fo p + where + fo = toFlex o -- | The most flexible test driver, can be configured to behave in almost any way. -testFlex :: FlexibleOptions a -> (a -> Bool) -> IO (Result a) +testFlex :: FlexibleOptions a -> (a -> Bool) -> IO (Result, [a]) testFlex ioOp p = do op <- ioOp let e = fProcess op (fEnum op) @@ -125,7 +122,13 @@ runSize k (n,cs) = do fOutput op $ "*** Searching in " ++ show n ++ " values of size " ++ show k ++ "\n" doWhile (map (\x -> fOutput op "Counterexample found!\n" >> fReport op x) cs) - fIO op ((doWhile $ zipWith runSize [0..] lazyResult)) + rxs@(r,_) <- fIO op ((doWhile $ zipWith runSize [0..] lazyResult)) + case r of + Exhausted -> fOutput op "Search space exhausted\n" + TimedOut -> fOutput op "Timed out\n" + _ -> return () + return rxs + doWhile :: [IO Bool] -> IO Bool doWhile [] = return True diff --git a/examples/haskell-src-exts/hse.hs b/examples/haskell-src-exts/hse.hs --- a/examples/haskell-src-exts/hse.hs +++ b/examples/haskell-src-exts/hse.hs @@ -13,53 +13,33 @@ -- Welcome to the automatic HSE tester! -- Things to try while youre here: --- switch between Exp/Module/Decl etc. as testing types (e.g. TestRoundtrip) +-- switch between Exp/Module/Decl etc. as TestParse -- to discover bugs in the various entry-points of the grammar. -- TODOs: add some newtypes and modifiers to deal with syntax type invariants --- (such as only enumerating non-empty do-expressions with a statement as last --- expression). +-- (such as only enumerating non-empty do-expressions with a statement as last expression). -- -- Catalogue and report all the bugs found. - - -main = main_parse 100 - -run n = main_parse n - - --- Everything which is produced by the pretty printer and is parseable is --- semantically euivalent to the original. -type TestRoundtrip = Exp -main_round n = undefined - -rep_round :: (Eq a,Parseable a, Show a, Pretty a) => a -> IO () -rep_round e = case myParse $ prettyPrint e of - ParseOk e' -> if e == e' || prettyPrint e == prettyPrint e' then return () else do - putStrLn $ "------ Error ------" - putStrLn $ "e: "++ (show e) - putStrLn $ "e(Pretty): "++(prettyPrint e) - putStrLn $ "e': "++ (show e') - putStrLn $ "e'(Pretty): "++(prettyPrint e') - putStrLn "" - ParseFailed _ err -> return () +-- +-- Fix the round-trip -instance Enumerable SrcSpanInfo where - enumerate = datatype [c0 $ SrcSpanInfo (SrcSpan "M.hs" 0 0 0 0) []] +main = do + main_parse -- Test the parsable property + main_round -- Test the round-trip property -- Everything produced by the pretty printer is parseable. -type TestParse = Module SrcSpanInfo -main_parse n = do +type TestParse = Exp SrcSpanInfo -- Type to be tested +main_parse = do res <- test prop_parse - mapM (putStr . rep_parse) (counterexamples res) + mapM (putStr . rep_parse) res -rep_parse :: (Parseable a, Show a, Pretty a) => a -> String +rep_parse :: TestParse -> String rep_parse e = case myParse $ prettyPrint e of ParseOk e' -> const "" (e' `asTypeOf` e) ParseFailed _ err -> unlines - [(show e) + [(show $ fmap (const ()) e) ,(prettyPrint e) ,err] @@ -69,7 +49,58 @@ ParseFailed _ err -> False +-- Everything which is produced by the pretty printer parses back to itself +type TestRoundtrip = Exp SrcSpanInfo +main_round = do + res <- testOptions defOptions{oBounded = (Just 10000)} prop_trip + mapM (putStr . rep_trip) res + +-- Tests a "roundtrip and a half" +-- parse (print e) == parse (print (parse (print e))) +-- Ignores parsing errors +prop_trip :: TestRoundtrip -> Bool +prop_trip e = case roundAndAhalf e of + ParseOk (e', e'') -> eq e' e'' + ParseFailed _ err -> True + +eq :: TestRoundtrip -> TestRoundtrip -> Bool +eq a b = fmap (const ()) a == fmap (const ()) b + + +rep_trip :: TestRoundtrip -> String +rep_trip e = case roundAndAhalf e of + ParseOk (e', e'') -> unlines [ + "Original:", + show (fmap (const ()) e), + prettyPrint e, + "", + "One print/parse round:", + show (fmap (const ()) e'), + prettyPrint e', + "", + "Two print/parse round:", + show (fmap (const ()) e''), + prettyPrint e'' + ] + ParseFailed _ err -> unlines + [(show $ fmap (const ()) e) + ,(prettyPrint e) + ,err] + + +roundAndAhalf :: TestRoundtrip -> ParseResult (TestRoundtrip, TestRoundtrip) +roundAndAhalf e = do + e' <- myParse $ prettyPrint e + e'' <- myParse $ prettyPrint e' + return (e', e'') + {- + +-- Everything which is produced by the pretty printer and is parseable is +-- semantically euivalent to the original. + + + -- The pretty printer doesnt fail, for testing the enumerators. type TestPrint = Module @@ -87,21 +118,12 @@ putStrLn "") -} +-- Parse with all extensions myParse :: Parseable a => String -> ParseResult a myParse = parseWithMode defaultParseMode{ - extensions = ge' + extensions = [ e |e@(EnableExtension _) <- knownExtensions] } -ge' = map EnableExtension - [ TypeFamilies - , TemplateHaskell - , MagicHash - , ParallelArrays - , LambdaCase - , ExplicitNamespaces - ] - - sureParse :: Parseable a => String -> a sureParse s = case myParse s of ParseOk a -> a @@ -111,9 +133,8 @@ parse_print s = let a = sureParse s in (a,prettyPrint a) - - - +instance Enumerable SrcSpanInfo where + enumerate = datatype [c0 $ SrcSpanInfo (SrcSpan "M.hs" 0 0 0 0) []] -- Uncomment the dExcluding line to enable known bugs (let @@ -125,28 +146,60 @@ dExcluding 'PQuasiQuote . dAll buggy3 = + dExcept 'Tuple [| c3 (\a b c -> Tuple a b (nonEmpty c))|] . + dExcept 'TupleSection [| c3 (\a b c -> TupleSection a b (nonEmpty c))|] . dExcept 'LCase [| c2 (\a -> LCase a . nonEmpty) |] . dExcept 'Do [| c3 $ \a ss e -> Do a (ss ++ [Qualifier a e]) |] . - + dExcept 'Var [| c2 (\a b -> Var a (nonSpecial b)) |] . + dExcept 'Con [| c2 (\a b -> Con a (nonSpecial b)) |] . + + dExcept 'Lambda [| c3 (\a b c -> Lambda a (nonEmpty b) c) |] . + + dExcept 'RecUpdate [| c3 (\a b c -> RecUpdate a b (nonEmpty c)) |] . + + dExcept 'ListComp [| c3 (\a b c -> ListComp a b (nonEmpty c)) |] . + + dExcluding 'TypeApp . + dExcluding 'GenPragma . -- Seems genuinly buggy + dExcluding 'TypQuote . + dExcluding 'VarQuote . + dExcluding 'BracketExp . + dExcluding 'MDo . + dExcluding 'IPVar . -- What is this? + dExcluding 'QuasiQuote . dExcluding 'XPcdata . dExcluding 'XExpTag . dExcluding 'XChildTag . + dExcluding 'OverloadedLabel . dExcept 'XPcdata [| c2 $ \a -> XPcdata a . nonEmpty |] . dExcept 'MultiIf [| c2 $ \a -> MultiIf a . nonEmpty |] . dAll fixdecs = + dExcluding 'DeprPragmaDecl . + dExcluding 'WarnPragmaDecl . + dExcluding 'SpliceDecl . + dExcept 'TypeSig [| c3 (\a b c -> TypeSig a (nonEmpty b) c) |] . dExcept 'InfixDecl [| c4 $ \a b c -> InfixDecl a b c . nonEmpty |] . + dExcept 'CompletePragma [| c3 $ \a b c -> CompletePragma a (nonEmpty b) c|] . dAll fixlit = - dExcept 'PrimWord [| c2 (\a x -> PrimWord a (toInteger (x :: Word)) (show x)) |] . + dExcluding 'PrimWord . + dExcluding 'PrimInt . -- Buggy? + --dExcept 'PrimWord [| c2 (\a x -> PrimWord a (toInteger (x :: Word)) (show x)) |] . + dExcept 'Int [| c2 (\a x -> Int a (toInteger (x :: Word)) (show x)) |] . dAll + fixType = + dExcept 'TyUnboxedSum [| c2 (\a b -> TyUnboxedSum a (nonEmpty b))|] . + + dExcluding 'TyQuasiQuote . + dAll in fmap concat $ mapM deriveEnumerable' [ - dAll ''Module, + dExcluding 'XmlHybrid $ dExcluding 'XmlPage $ dAll ''Module, -- dAll ''SrcLoc, dExcluding 'AnnModulePragma $ dExcluding 'LanguagePragma -- dExcept 'LanguagePragma [|c2 $ \x -> LanguagePragma x . nonEmpty|] @@ -157,7 +210,7 @@ dAll ''QName, dAll ''ImportSpec, dAll ''Annotation, - dAll ''Type, + fixType ''Type, dAll ''Activation, dAll ''Rule, dAll ''CallConv, @@ -188,7 +241,7 @@ dAll ''GuardedRhs, dAll ''IPBind, dAll ''XAttr, - dAll ''Splice, + dExcluding 'IdSplice $ dAll ''Splice, dAll ''Bracket, dAll ''QualStmt, dAll ''FieldUpdate, @@ -219,7 +272,9 @@ dAll ''InstRule, dAll ''Unpackedness, dAll ''FieldDecl, - dAll ''InstHead + dAll ''InstHead, + dAll ''DerivStrategy, + dAll ''MaybePromotedName ]) diff --git a/examples/lambda-terms/lambdas.hs b/examples/lambda-terms/lambdas.hs --- a/examples/lambda-terms/lambdas.hs +++ b/examples/lambda-terms/lambdas.hs @@ -6,14 +6,26 @@ import Test.Feat.Access import Test.Feat +-- Shows off a bit +main = do + putStr "There are this many closed lambda terms with 100 lambdas/applications: " + let n = count 100 + print n + putStr $ "Here is one of them: " + putStrLn $ pretty (selectTerm 100 (n `div` 2)) + putStrLn "Here are all the terms of size 3:" + mapM_ (putStrLn . pretty) (snd $ vs !! 3) + + data Term scope = Lam (Term (FinS scope)) | App (Term scope) (Term scope) | Var scope deriving (Show, Typeable) instance Enumerable a => Enumerable (Term a) where - enumerate = datatype [ c1 Var -- Variables are size 0, add pay to make size 1 - , pay (c1 Lam) -- "Irregular constructor" - , pay (c2 App)] + enumerate = share $ aconcat + [ c1 Var -- Variables are size 0, add pay to make size 1 + , pay (c1 Lam) -- "Irregular constructor" + , pay (c2 App)] -- Finite numeric types data FinZ deriving Typeable @@ -23,7 +35,7 @@ enumerate = datatype [] data FinS n = Z | S n deriving (Typeable, Show) instance Enumerable n => Enumerable (FinS n) where - enumerate = datatype [c0 Z, c1 S] + enumerate = share $ aconcat [c0 Z, c1 S] -- All closed lambda expressions closed = global :: Enumerate (Term FinZ) @@ -34,3 +46,31 @@ -- Select any term of a given size selectTerm = selectWith closed + + + + + + + + +-- The rest is just pretty-printing stuff +pretty :: Fin a => Term a -> String +pretty t = prettyPar 0 0 t where + -- p: 0-never 1-lambda 2-always + prettyPar :: Fin a => Int -> Int -> Term a -> String + prettyPar _ _ (Var s) = "x"++show (toInt s) + prettyPar n p (Lam t) = par 1 p $ "\\x"++show n++"->"++prettyPar (n+1) 0 t + prettyPar n p (App t1 t2) = par 2 p $ + prettyPar n 1 t1 ++ " " ++ prettyPar n 2 t2 + par p p' s = if p <= p' then "(" ++ s ++ ")" else s + +class Fin a where + toInt :: a -> Int + +instance Fin FinZ where + toInt a = a `seq` error "toInt FinZ" + +instance Fin n => Fin (FinS n) where + toInt Z = 0 + toInt (S n) = toInt n + 1 diff --git a/testing-feat.cabal b/testing-feat.cabal --- a/testing-feat.cabal +++ b/testing-feat.cabal @@ -1,5 +1,5 @@ Name: testing-feat -Version: 1.0.1.0 +Version: 1.1.0.0 Synopsis: Functional Enumeration of Algebraic Types Description: Feat (Functional Enumeration of Algebraic Types) provides enumerations as functions from natural numbers to values