packages feed

speculate 0.2.2 → 0.2.3

raw patch · 9 files changed

+113/−36 lines, 9 files

Files

speculate.cabal view
@@ -1,5 +1,5 @@ name:                speculate-version:             0.2.2+version:             0.2.3 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.2+  tag:             v0.2.3   library@@ -46,6 +46,7 @@                  , Test.Speculate.Expr.Ground                  , Test.Speculate.Expr.Match                  , Test.Speculate.Expr.TypeInfo+                 , Test.Speculate.Pretty                  , Test.Speculate.Reason                  , Test.Speculate.Reason.Order                  , Test.Speculate.SemiReason
src/Test/Speculate/Args.hs view
@@ -55,6 +55,7 @@                                --   maximum number of tests   , maxConstants :: Maybe Int  -- ^ __(intermediary)__ maximum nubmer of constants allowed when considering expressions   , maxDepth     :: Maybe Int  -- ^ __(intermediary)__ maximum depth of considered expressions+  , showCounts   :: Bool       -- ^ __(intermediary)__ show counts of equations, inequalities and conditional equations   , showTheory   :: Bool       -- ^ __(debug)__ whether to show raw theory   , showArgs     :: Bool       -- ^ __(debug)__ show _this_ args before running   , showHelp     :: Bool       -- ^ __(advanced)__ whether to show the command line help@@ -92,6 +93,7 @@   , showSemiequations    = True   , showConditions       = True   , showConstantLaws     = False+  , showCounts           = False   , showDot              = False   , quietDot             = False   , showClassesFor       = []@@ -243,6 +245,7 @@   , "cmax-constants"     --= \s a -> a {maxConstants = Just $ read s}   , "eeval-timeout"      --= \s a -> a {evalTimeout = Just $ read s}   , "ddepth"             --= \s a -> a {maxDepth = Just $ read s}+  , " counts"            --.   \a -> a {showCounts = True}   , "gsemi-digraph"      --.   \a -> a {showDot = True                                        ,quietDot = False                                        ,showConstants = False@@ -264,12 +267,11 @@   , "aall-foreground"    --.   \a -> a {constants = discard (== background) (constants a)}   ]   where-  (short:long) --= fun = flagReq  [[short],long] ((Right .) . fun) "X" ""-  (short:long) --. fun = flagNone [[short],long] fun                   ""+  (short:long) --= fun = flagReq  (filter (/= " ") [[short],long]) ((Right .) . fun) "X" ""+  (short:long) --. fun = flagNone (filter (/= " ") [[short],long]) fun                   ""   parseMinTests :: String -> Int -> Int   parseMinTests s | last s == '%' = \x -> read (init s) * x `div` 100                   | otherwise     = const (read s)--- TODO: implement space char semantics  getArgs :: Args -> IO Args getArgs = processArgs . prepareArgs
src/Test/Speculate/CondReason.hs view
@@ -126,13 +126,9 @@ canonicalCEqn :: (Expr -> Expr -> Ordering) -> (Expr,Expr,Expr) -> Bool canonicalCEqn cmp = canonicalCEqnBy cmp preludeInstances -prettyChy :: ((Expr,Expr,Expr) -> Bool) -> Chy -> String-prettyChy shouldShow =-    table "r r r l l"-  . map (\(pre,e1,e2) -> [ showOpExpr "==>" pre-                         , "==>", showOpExpr "==" e1-                         , "==",  showOpExpr "==" e2 ])-  . sortOn (typ . (\(c,x,y) -> x))+finalCondEquations :: ((Expr,Expr,Expr) -> Bool) -> Chy -> [(Expr,Expr,Expr)]+finalCondEquations shouldShow =+    sortOn (typ . (\(c,x,y) -> x))   . filter shouldShow   . cequations   . cfinalize
src/Test/Speculate/Engine.hs view
@@ -95,6 +95,19 @@ ---------------------------- -- * Enumerating expressions +-- | Computes a theory from atomic expressions.  Example:+--+-- > > theoryFromAtoms 5 compare (const True) (equal preludeInstances 100)+-- > >   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]+-- > Thy { rules = [ (x + y) + z == x + (y + z) ]+-- >     , equations = [ y + x == x + y+-- >                   , y + (x + z) == x + (y + z)+-- >                   , z + (x + y) == x + (y + z)+-- >                   , z + (y + x) == x + (y + z) ]+-- >     , canReduceTo = (|>)+-- >     , closureLimit = 2+-- >     , keepE = keepUpToLength 5+-- >     } theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> Thy theoryFromAtoms sz cmp keep (===) = fst . theoryAndRepresentativesFromAtoms sz cmp keep (===) @@ -108,6 +121,8 @@   where   fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes] +-- | Given atomic expressions, compute theory and representative schema+--   expressions. theoryAndRepresentativesFromAtoms :: Int                                   -> (Expr -> Expr -> Ordering)                                   -> (Expr -> Bool) -> (Expr -> Expr -> Bool)@@ -136,6 +151,14 @@ distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr] distinctFromSchemas ti nt nv thy = map C.rep . classesFromSchemas ti nt nv thy +-- > > classesFromSchemas preludeInstances 500 2 thy [_ + _, _ + (_ + _)]+-- > [ (x + x :: Int,[])+-- > , (x + y :: Int,[y + x :: Int])+-- > , (y + y :: Int,[])+-- > , (x + (x + x) :: Int,[])+-- > , (x + (x + y) :: Int,[x + (y + x) :: Int,y + (x + x) :: Int])+-- > , (x + (y + y) :: Int,[y + (x + y) :: Int,y + (y + x) :: Int])+-- > , (y + (y + y) :: Int,[]) ] classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr] classesFromSchemas ti nt nv thy = C.mergesThat (equal ti nt)                                 . C.mergesOn (normalizeE thy)@@ -144,6 +167,14 @@ -- won't detect all equivalences.  here we test the few remaining -- there shouldn't be that much overhead +-- | Returns all classes of expressions that can be build from expression+--   schemas (single variable expressions).  Examples:+--+-- > > classesFromSchema preludeInstances thy 2 (i_ -+- i_)+-- > [ (x + x :: Int,[])+-- > , (x + y :: Int,[])+-- > , (y + x :: Int,[])+-- > , (y + y :: Int,[]) ] classesFromSchema :: Instances -> Thy -> Int -> Expr -> [Class Expr] classesFromSchema ti thy n = C.mergesOn (normalizeE thy)                            . map C.fromRep
+ src/Test/Speculate/Pretty.hs view
@@ -0,0 +1,49 @@+-- | Pretty printing of Equations, Inequalities and Conditional Equations+module Test.Speculate.Pretty+  ( prettyThy, prettyEquations+  , prettyShy, prettySemiEquations+  , prettyChy, prettyCondEquations+  )+where++import Test.Speculate.Expr+import Test.Speculate.Utils.PrettyPrint+import Test.Speculate.Reason     (Thy, finalEquations)+import Test.Speculate.SemiReason (Shy, finalSemiEquations)+import Test.Speculate.CondReason (Chy, finalCondEquations)++type Equation = (Expr,Expr)+type CondEquation = (Expr,Expr,Expr)++prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String+prettyThy shouldShow ti = prettyEquations . finalEquations shouldShow ti++prettyChy :: (CondEquation -> Bool) -> Chy -> String+prettyChy shouldShow = prettyCondEquations . finalCondEquations shouldShow++prettyShy :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> String+prettyShy shouldShow insts equivalentInstanceOf =+  prettySemiEquations . finalSemiEquations shouldShow insts equivalentInstanceOf++prettyEquations :: [Equation] -> String+prettyEquations =+  table "r l l" . map showEquation+  where+  showEquation (e1,e2)+--  | typ e1 == boolTy = [showOpExpr "<==>" e1, "<==>", showOpExpr "<==>" e2]+    | otherwise        = [showOpExpr "==" e1, "==", showOpExpr "==" e2]++prettySemiEquations :: [Equation] -> String+prettySemiEquations =+  table "r l l" . map showSELine+  where+  showSELine (e1,e2) = showLineWithOp (if typ e1 == boolTy then "==>" else "<=") (e1,e2)+  showLineWithOp o (e1,e2) = [showOpExpr o e1, o, showOpExpr o e2]++prettyCondEquations :: [CondEquation] -> String+prettyCondEquations =+  table "r r r l l" . map showCELine+  where+  showCELine (ce,e1,e2) = [ showOpExpr "==>" ce+                          , "==>", showOpExpr "==" e1+                          , "==",  showOpExpr "==" e2 ]
src/Test/Speculate/Reason.hs view
@@ -15,7 +15,7 @@   , (|==|)   , theorize   , theorizeBy-  , prettyThy+  , finalEquations   , criticalPairs   , normalizedCriticalPairs   , append@@ -414,17 +414,13 @@   showEquations = unlines . map showEquation   showEquation (e1,e2) = showExpr e1 ++ " == " ++ showExpr e2 -prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String-prettyThy shouldShow ti thy =-    table "r l l" . map showEquation-  . sortOn (typ . fst) . sortBy (compareE thy `on` uncurry phonyEquation)+finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation]+finalEquations shouldShow ti thy =+    sortOn (typ . fst) . sortBy (compareE thy `on` uncurry phonyEquation)   . filter shouldShow   $ rules thy' ++ map swap (equations thy')   where   thy' = canonicalizeThyWith ti . discardRedundantRulesByEquations $ finalize thy-  showEquation (e1,e2)---  | typ e1 == boolTy = [showOpExpr "<==>" e1, "<==>", showOpExpr "<==>" e2]-    | otherwise        = [showOpExpr "==" e1, "==", showOpExpr "==" e2]  -- | Finalize a theory by discarding redundant equations.  If after finalizing --   you 'complete', redundant equations might pop-up again.
src/Test/Speculate/Report.hs view
@@ -12,6 +12,7 @@ import Test.Speculate.Args import Test.Speculate.Utils import Test.Speculate.Utils.Colour+import Test.Speculate.Pretty  import Data.Ratio ((%)) import Control.Monad (when,unless)@@ -38,15 +39,20 @@       putStrLn "Use `--force` or `args{force=true}` to ignore instance errors."       fail "exiting"   when (showTheory args)       . putStrLn $ showThy thy-  when (showEquations args) . putStrLn $ prettyThy (shouldShowEquation args) ti thy+  let shy = semiTheoryFromThyAndReps ti n (maxVars args) thy+          $ filter (\e -> lengthE e <= computeMaxSemiSize args) es+  let chy = conditionalTheoryFromThyAndReps ti (compareExpr args) n (maxVars args) (computeMaxCondSize args) thy es+  let equations     = finalEquations     (shouldShowEquation args) ti                          thy+  let semiEquations = finalSemiEquations (shouldShowEquation args) ti (equivalentInstance thy) shy+  let condEquations = finalCondEquations (shouldShowConditionalEquation args)                  chy+  when (showEquations args)        . putStrLn $ prettyEquations equations+  when (showSemiequations args)    . putStrLn $ prettySemiEquations semiEquations+  when (reallyShowConditions args) . putStrLn $ prettyCondEquations condEquations+  when (showCounts args) . putStrLn . unlines+    $  [ "#-equations      = " ++ show (length equations)     | showEquations        args ]+    ++ [ "#-semi-equations = " ++ show (length semiEquations) | showSemiequations    args ]+    ++ [ "#-cond-equations = " ++ show (length condEquations) | reallyShowConditions args ]   reportClassesFor ti n (showClassesFor args) thy es-  when (showSemiequations args) . putStrLn-    . prettyShy (shouldShowEquation args) ti (equivalentInstance thy)-    . semiTheoryFromThyAndReps ti n (maxVars args) thy-    $ filter (\e -> lengthE e <= computeMaxSemiSize args) es-  when (reallyShowConditions args) . putStrLn-    . prettyChy (shouldShowConditionalEquation args)-    $ conditionalTheoryFromThyAndReps ti (compareExpr args) n (maxVars args) (computeMaxCondSize args) thy es   when (showDot args) $     reportDot ti (onlyTypes args) (quietDot args) (maxVars args) n thy es
src/Test/Speculate/SemiReason.hs view
@@ -81,20 +81,15 @@           . concatMap (\(e1,e2) -> [e1,e2])           $ sequations shy -prettyShy :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> String-prettyShy shouldShow insts equivalentInstanceOf shy =-    table "r l l"-  . map showSELine-  . sortOn (typ . fst)+finalSemiEquations :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]+finalSemiEquations shouldShow insts equivalentInstanceOf shy =+    sortOn (typ . fst)   . filter shouldShow   . discardLater (equivalentInstanceOf `on` uncurry phonyEquation)   . discard (transConsequence shy)   . discardLater (isInstanceOf `on` uncurry phonyEquation)   . sequations   $ canonicalizeShyWith insts shy-  where-  showSELine (e1,e2) = showLineWithOp (if typ e1 == boolTy then "==>" else "<=") (e1,e2)-  showLineWithOp o (e1,e2) = [showOpExpr o e1, o, showOpExpr o e2]  canonicalizeShyWith :: Instances -> Shy -> Shy canonicalizeShyWith = mapSemiEquations . canonicalizeSemiEquationWith
tests/Test.hs view
@@ -116,6 +116,7 @@ import qualified Test.Speculate.Expr as E import Test.Speculate.Reason import Test.Speculate.Reason.Order+import Test.Speculate.Engine hiding (true, false)  import Data.Char (ord) import Data.Dynamic