speculate 0.2.9 → 0.2.10

raw patch · 8 files changed

+64/−32 lines, 8 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• TODO.md +0/−4
• speculate.cabal +2/−2
• src/Test/Speculate/Args.hs +20/−7
• src/Test/Speculate/Engine.hs +25/−15
• src/Test/Speculate/Report.hs +5/−3
• src/Test/Speculate/Sanity.hs +1/−1
• src/Test/Speculate/Utils/List.hs +8/−0
• tests/test-utils.hs +3/−0

@@ -17,10 +17,6 @@   Maybe a new field in args?  Or even things begining with capital letters and   ":". -* Implement expand by expanding tiers (more robust and flexible).  It-  will allow extraction of constant values from tiers.  This will also make it-  easy to amend a Thy: do theorization; add a bunch of atoms; do it again;-  stranger things (bugs?) -----------------------

@@ -1,5 +1,5 @@ name:                speculate-version:             0.2.9+version:             0.2.10 synopsis:            discovery of properties about Haskell functions description:   Speculate automatically discovers laws about Haskell functions.@@ -31,7 +31,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/speculate-  tag:             v0.2.9+  tag:             v0.2.10   library

@@ -38,6 +38,7 @@ import Test.Speculate.Utils import System.Console.CmdArgs.Explicit +import Test.LeanCheck ((\/)) import qualified Data.List as L (insert) import Data.List hiding (insert) import Data.Maybe (catMaybes)@@ -59,6 +60,7 @@   , showSemiequations :: Bool  -- ^ whether to show inequalties   , showConditions    :: Bool  -- ^ whether to show conditional equations   , showConstantLaws  :: Bool  -- ^ whether to show laws with no variables+  , autoConstants     :: Bool  -- ^ automatically include constants taken from tiers of values    , minTests    :: Int -> Int  -- ^ __(intermediary)__ minimum number of tests                                --   for passing postconditions in function of@@ -98,6 +100,7 @@   , maxDepth             = Nothing   , instances            = []   , showConstants        = True+  , autoConstants        = False   , showArgs             = True   , showTheory           = False   , showEquations        = True@@ -171,15 +174,21 @@ reallyShowConditions args = showConditions args                          && boolTy `elem` map (finalResultTy . typ) (allConstants args) -atoms :: Args -> [Expr]-atoms args = nubSort (map holeOfTy ts)-     `union` allConstants args-     `union` [showConstant True  | showConds || showDot args]-     `union` [showConstant False | showConds || showDot args]-     `union` (nubSort . catMaybes) [eqE (computeInstances args) t | t <- ts, showConds]+atoms :: Args -> [[Expr]]+atoms args = [ nubSort (map holeOfTy ts)+       `union` allConstants args+       `union` [showConstant True  | showConds || showDot args]+       `union` [showConstant False | showConds || showDot args]+       `union` (nubSort . catMaybes) [eqE is t | showConds, t <- ts] ]+         \-/ foldr (\/) [] [tiersE is t | autoConstants args, t <- ts]   where   ts = types args+  is = computeInstances args   showConds = reallyShowConditions args+  []  \-/ []   =  []+  xss \-/ []   =  xss+  []  \-/ yss  =  yss+  (xs:xss) \-/ (ys:yss)  =  xs `union` ys  :  xss \-/ yss  types :: Args -> [TypeRep] types = nubMergeMap (typesIn . typ) . allConstants@@ -218,7 +227,10 @@   where   e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT   e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT-  e1 `cmp` e2 = compareIndex (atoms args) e1 e2 <> e1 `compare` e2+  e1 `cmp` e2 = compareIndex (concat $ atoms args) e1 e2 <> e1 `compare` e2+-- NOTE: "concat $ atoms args" may be an infinite list.  This function assumes+-- that the symbols will appear on the list eventually for termination.  If I+-- am correct this ivariant is assured by the rest of the code.  -- | A special 'Expr' value. --   When provided on the 'constants' list, @@ -245,6 +257,7 @@   , "zsemisize"          --= \s a -> a {maxSemiSize = read s}   , "xcondsize"          --= \s a -> a {maxCondSize = read s}   , "Aconstants"         --.   \a -> a {showConstants = False} -- TODO: fix name+  , "Uauto-constants"    --.   \a -> a {autoConstants = True}   , "Ohide-args"         --.   \a -> a {showArgs = False}   , "Ttheory"            --.   \a -> a {showTheory = True}   , "Eno-equations"      --.   \a -> a {showEquations = False}

@@ -14,6 +14,7 @@   , mostSpecific    , theoryAndRepresentativesFromAtoms+  , representativesFromAtoms   , theoryFromAtoms   , equivalencesBetween @@ -39,6 +40,7 @@ import Data.Function (on) import Data.Monoid ((<>)) +import Test.LeanCheck ((\/)) import Test.Speculate.Utils import Test.Speculate.Expr import Test.Speculate.Reason@@ -117,16 +119,19 @@ -- >     , closureLimit = 2 -- >     , keepE = keepUpToLength 5 -- >     }-theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> Thy+theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> Thy theoryFromAtoms sz cmp keep (===) = fst . theoryAndRepresentativesFromAtoms sz cmp keep (===) -representativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> [Expr]+representativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]] representativesFromAtoms sz cmp keep (===) = snd . theoryAndRepresentativesFromAtoms sz cmp keep (===) -expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> (Thy,[Expr]) -> (Thy,[Expr])-expand keep (===) (thy,ss) = foldl (flip $ consider (===)) (thy,ss)-                           . concat . zipWithReverse (*$*)-                           $ collectOn lengthE ss+expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [Expr] -> (Thy,[[Expr]]) -> (Thy,[[Expr]])+expand keep (===) sz ss (thy,sss) = (complete *** id)+                                  . foldl (flip $ consider (===) sz) (thy,sss)+                                  . concat+                                  . (ss:)+                                  . zipWithReverse (*$*)+                                  $ take sz sss   where   fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes] @@ -135,11 +140,10 @@ theoryAndRepresentativesFromAtoms :: Int                                   -> (Expr -> Expr -> Ordering)                                   -> (Expr -> Bool) -> (Expr -> Expr -> Bool)-                                  -> [Expr] -> (Thy,[Expr])-theoryAndRepresentativesFromAtoms sz cmp keep (===) ds =-  iterate ((complete *** id) . expand keep (===)) dsThy !! (sz-1)+                                  -> [[Expr]] -> (Thy,[[Expr]])+theoryAndRepresentativesFromAtoms sz cmp keep (===) dss =+  chain [expand keep (===) sz' (dss ! (sz'-1)) | sz' <- reverse [1..sz]] (iniThy,[])   where-  dsThy = (complete *** id) $ foldl (flip $ consider (===)) (iniThy,[]) ds   iniThy = emptyThy { keepE = keepUpToLength sz                     , closureLimit = 2                     , canReduceTo = dwoBy (\e1 e2 -> e1 `cmp` e2 == GT)@@ -147,15 +151,21 @@                     }  -- considers a schema-consider :: (Expr -> Expr -> Bool) -> Expr -> (Thy,[Expr]) -> (Thy,[Expr])-consider (===) s (thy,ss)-  | not (s === s) = (thy,ss++[s])  -- uncomparable type-  | rehole (normalizeE thy (mostGeneral s)) `elem` ss = (thy,ss)+consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy,[[Expr]]) -> (Thy,[[Expr]])+consider (===) sz s (thy,sss)+  | not (s === s) = (thy,sssWs)  -- uncomparable type+  | rehole (normalizeE thy (mostGeneral s)) `elem` ss = (thy,sss)   | otherwise =     ( append thy $ equivalencesBetween (===) s s ++ eqs-    , ss ++ [s | not $ any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs])+    , if any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs+        then sss+        else sssWs )     where+    ss = uptoT sz sss+    sssWs = sss \/ wcons0 sz s     eqs = concatMap (equivalencesBetween (===) s) $ filter (s ===) ss+    wcons0 :: Int -> a -> [[a]]+    wcons0 n s = replicate (n-1) [] ++ [[s]]  distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr] distinctFromSchemas ti nt nv thy = map C.rep . classesFromSchemas ti nt nv thy

@@ -33,10 +33,12 @@   let ti = computeInstances args   let ats = types args   let ts = filter (isListable ti) ats-  let ds' = atoms args-  let (thy,es) = theoryAndRepresentativesFromAtoms sz (compareExpr args) (keepExpr args) (timeout args .: equal ti n) ds'+  let dss = atoms args+  let (thy,ess) = theoryAndRepresentativesFromAtoms sz (compareExpr args) (keepExpr args) (timeout args .: equal ti n) dss+  let es = uptoT sz ess   putArgs args-  when (showConstants args)    . putStrLn . unlines $ map show ds'+  -- TODO: somehow show the tail of dss, maybe use "..."+  when (showConstants args) . putStrLn . unlines $ map show (head dss)   warnMissingInstances ti ats   let ies = instanceErrors ti n ats   unless (null ies) $ do

@@ -64,7 +64,7 @@   ++ [ "(<=) :: " ++ ty ++ "  is not an ordering ("     ++ intercalate ", " es ++ ")"      | let es = ordErrors is n t, isOrd is t, not (null es) ]   ++ [ "(==) and (<=) :: " ++ ty ++ " are inconsistent: (x == y) /= (x <= y && y <= x)"-     | f $ (x -==- y) -==- (x -<=- y -&&- y -<=- x)]+     | f $ (x -==- y) -==- (x -<=- y -&&- y -<=- x), isEq is t, isOrd is t ]   where   f = not . true is n   x = Var "x" t

@@ -30,6 +30,7 @@   , takeGreaterHalf   , accum   , partitionByMarkers+  , (!)   ) where @@ -215,3 +216,10 @@       | x == y -> let (ys',zs') = partitionByMarkers y z zs in (ys++ys',zs')       | x == z -> let (zs',ys') = partitionByMarkers z y zs in (ys++ys',zs')       | otherwise -> error "partitionByMarkers: the impossible happened, this is definitely a bug.  See source."++-- Total version of !! that works on lists of lists (returning [] for index not+-- found).+(!) :: [[a]] -> Int -> [a]+(xs:xss) ! 0  =  xs+(xs:xss) ! n  =  xss ! (n-1)+[]       ! n  =  []

@@ -126,4 +126,7 @@   , holds n $ \xs ys -> xs +++ ys == ys +++ (xs :: [Int])   , holds n $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys                     ==> xs +++ ys == nubSort (xs ++ ys :: [Int])++  , holds n $ \n xss -> 0 <  n && n <  length xss ==> xss ! n == (xss !! n :: [Int])+  , holds n $ \n xss -> 0 >= n && n >= length xss ==> xss ! n == ([] :: [Int])   ]