speculate 0.2.7 → 0.2.8
raw patch · 16 files changed
+1062/−88 lines, 16 filesdep +speculatedep ~leancheck
Dependencies added: speculate
Dependency ranges changed: leancheck
Files
- README.md +8/−1
- TODO.md +11/−55
- speculate.cabal +84/−12
- src/Test/Speculate/Expr/Core.hs +17/−14
- src/Test/Speculate/Utils.hs +4/−0
- tests/Test.hs +39/−4
- tests/test-creason.hs +61/−0
- tests/test-engine.hs +87/−0
- tests/test-eval.hs +53/−0
- tests/test-expr.hs +19/−2
- tests/test-match.hs +92/−0
- tests/test-misc.hs +91/−0
- tests/test-order.hs +91/−0
- tests/test-reason.hs +230/−0
- tests/test-stats.hs +46/−0
- tests/test-utils.hs +129/−0
README.md view
@@ -3,6 +3,8 @@ [![Speculate Build Status][build-status]][build-log] [![Speculate on Hackage][hackage-version]][speculate-on-hackage]+[![Speculate on Stackage LTS][stackage-lts-badge]][speculate-on-stackage-lts]+[![Speculate on Stackage Nightly][stackage-nightly-badge]][speculate-on-stackage-nightly] Speculate automatically discovers laws about [Haskell] functions. Give Speculate a bunch of Haskell functions and it will discover laws like:@@ -136,5 +138,10 @@ [build-status]: https://travis-ci.org/rudymatela/speculate.svg?branch=master [build-log]: https://travis-ci.org/rudymatela/speculate [hackage-version]: https://img.shields.io/hackage/v/speculate.svg-[speculate-on-hackage]: https://hackage.haskell.org/package/speculate [latest Speculate version from Hackage]: https://hackage.haskell.org/package/speculate+[speculate-on-hackage]: https://hackage.haskell.org/package/speculate+[stackage-lts-badge]: http://stackage.org/package/speculate/badge/lts+[stackage-nightly-badge]: http://stackage.org/package/speculate/badge/nightly+[speculate-on-stackage]: http://stackage.org/package/speculate+[speculate-on-stackage-lts]: http://stackage.org/lts/package/speculate+[speculate-on-stackage-nightly]: http://stackage.org/nightly/package/speculate
TODO.md view
@@ -9,13 +9,7 @@ current ------- -* automatically detect and use orders. algorithm sketch:- 1. list everything of the type a -> a -> Bool- 2. check and filter everything that is an order- 3. parameterize semiTheoryFromEtc so that it takes an order re-run for- several different types--* consistency: rename semi to inequations everywhere.+* consistency: rename semi to inqualities everywhere. * improve printing by separating variables, constants and background constants. @@ -23,33 +17,13 @@ Maybe a new field in args? Or even things begining with capital letters and ":". --isolate most of the Expr module----------------------------------Maybe most of the `Expr` module could be isolated from the rest of Speculate-and released as a separate package.--I'll have to see how it goes in other modules, specially the `grounds`-function. Which could be interesting to include in the "expr" package but-would still depend on Listable and LeanCheck (maybe make it depend on it-anyway...)---later------- * 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; -* make regex work on qs1 and qs2. -* check if equivalences (==) are congruences (s == s' ==> f s == f s')---stranger things----------------+stranger things (bugs?)+----------------------- * after adding: @@ -123,6 +97,14 @@ Later Later ----------- +* check if equivalences (==) are congruences (s == s' ==> f s == f s')++* automatically detect and use orders. algorithm sketch:+ 1. list everything of the type a -> a -> Bool+ 2. check and filter everything that is an order+ 3. parameterize semiTheoryFromEtc so that it takes an order re-run for+ several different types+ * improve performance of inequality generation by using the following algorithm: @@ -143,8 +125,6 @@ * improve error message for missing typeInfo. Maybe add full suggestion. -* include Colin's list module example- * (for performance and interface): actually compute what happens with undefined values. e.g.: head [] == undefined. This will/may make things faster as we can prune foo (head []) or head [] ++ head [], which are also@@ -156,8 +136,6 @@ testing x + y = y + x. The second needs to hold for the first to hold. And, it will be far more common! -* (for performance) hardcode laws about `<=`, `<` and `==`? nah!- * (for interface) I actually do not need to provide 0-argument constants in the background algebra. Since I am using an enumerative strategy, I can actually enumerate those from `Instances`. This way, background will look nicer,@@ -171,10 +149,6 @@ I think it can be composed. Just make everything in the list "smaller" than whatever is not in the list. -* (for performance) This one is a maybe. When generating preconditions, do not- consider (<=), only consider (<), because I can always weaken the- precondition later. (update: nah!)- * (performance) Improve the performance of KBCompletion. In the process of generating equivalences, the slowest function is complete, accounting for 88 percent of runtime. Of that:@@ -195,21 +169,3 @@ * require _some_ cases of `e1 == e2` before considering `ce ==> e1 == e2`. 10% by default?---### Properties I want--From:- 1. ` i <= abs i `- 2. `negate (abs i) <= negate i`-Remove 2 because of:- 3. `x < y ==> negate y < negate x`--In the list example, I want:- * ` x < y ==> x:xs < y:ys`- * `xs < ys ==> x:xs < x:ys`--In the graph, instead of:- 1. `isNode x (addNode y emptyDigraph) == isNode y (addNode x emptyDigraph)`-have:- 2. `x /= y ==> isNode x (addNode y emptyDigraph) == False`
speculate.cabal view
@@ -1,5 +1,5 @@ name: speculate-version: 0.2.7+version: 0.2.8 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.7+ tag: v0.2.8 library@@ -53,8 +53,8 @@ , Test.Speculate.CondReason , Test.Speculate.Sanity , Test.Speculate.Misc- other-modules: Test.Speculate.Utils- , Test.Speculate.Utils.Class+ , Test.Speculate.Utils+ other-modules: Test.Speculate.Utils.Class , Test.Speculate.Utils.Colour , Test.Speculate.Utils.Digraph , Test.Speculate.Utils.List@@ -71,17 +71,89 @@ hs-source-dirs: src default-language: Haskell2010 +test-suite creason+ main-is: test-creason.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++test-suite engine+ main-is: test-engine.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++test-suite eval+ main-is: test-eval.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ test-suite expr- type: exitcode-stdio-1.0- main-is: test-expr.hs- other-modules: Test- hs-source-dirs: src, tests- build-depends: base >= 4 && < 5, leancheck, cmdargs, containers- default-language: Haskell2010+ main-is: test-expr.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0 +test-suite match+ main-is: test-match.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++test-suite misc+ main-is: test-misc.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++test-suite order+ main-is: test-order.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++test-suite reason+ main-is: test-reason.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++test-suite utils+ main-is: test-utils.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ benchmark plus-abs main-is: plus-abs.hs- build-depends: base >= 4 && < 5, leancheck, cmdargs, containers- hs-source-dirs: src, eg+ hs-source-dirs: eg+ build-depends: base >= 4 && < 5, speculate+ default-language: Haskell2010+ type: exitcode-stdio-1.0++benchmark test-stats+ main-is: test-stats.hs+ other-modules: Test+ hs-source-dirs: tests+ build-depends: base >= 4 && < 5, leancheck, speculate default-language: Haskell2010 type: exitcode-stdio-1.0
src/Test/Speculate/Expr/Core.hs view
@@ -36,6 +36,8 @@ , isSub , hasVar , unfoldApp+ , isTuple+ , unfoldTuple , isConstantNamed -- * Properties of expressions@@ -160,20 +162,10 @@ '[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs cs -> showParen (d > prec ":") $ showsOpExpr ":" e1 . showString ":" . showString cs-showsPrecExpr d ((Constant "," _ :$ e1) :$ e2) =- showString "(" . showsPrecExpr 0 e1- . showString "," . showsPrecExpr 0 e2- . showString ")"-showsPrecExpr d (((Constant ",," _ :$ e1) :$ e2) :$ e3) =- showString "(" . showsPrecExpr 0 e1- . showString "," . showsPrecExpr 0 e2- . showString "," . showsPrecExpr 0 e3- . showString ")"-showsPrecExpr d ((((Constant ",,," _ :$ e1) :$ e2) :$ e3) :$ e4) =- showString "(" . showsPrecExpr 0 e1- . showString "," . showsPrecExpr 0 e2- . showString "," . showsPrecExpr 0 e3- . showString "," . showsPrecExpr 0 e4+showsPrecExpr d ee | isTuple ee = id+ showString "("+ . foldr1 (\s1 s2 -> s1 . showString "," . s2)+ (showsPrecExpr 0 `map` unfoldTuple ee) . showString ")" showsPrecExpr d ((Constant f _ :$ e1) :$ e2) | isInfix f = showParen (d > prec f)@@ -191,6 +183,17 @@ $ showsPrecExpr (prec " ") e1 . showString " " . showsPrecExpr (prec " " + 1) e2+-- TODO: the above show instance is getting big. Move it into a separate file?++isTuple :: Expr -> Bool+isTuple = not . null . unfoldTuple++unfoldTuple :: Expr -> [Expr]+unfoldTuple = u . unfoldApp+ where+ u (Constant cs _:es) | not (null es) && cs == replicate (length es - 1) ','+ = es+ u _ = [] -- bad smell here, repeated code! showsTailExpr :: Expr -> String -> String
src/Test/Speculate/Utils.hs view
@@ -7,6 +7,10 @@ -- This module is part of Speculate. -- -- Exports utility functions of all utils sub-modules.+--+-- This is not intended to be used by users of Speculate, only by modules of+-- Speculate itself. Expect symbols exported here to come and go with every+-- minor version. module Test.Speculate.Utils ( module Test.Speculate.Utils.Misc , module Test.Speculate.Utils.PrettyPrint
tests/Test.hs view
@@ -42,10 +42,10 @@ -- Operators are surrounded by dashes. -- ** Integers- , zero, one, two, minusOne, minusTwo+ , zero, one, two, three, minusOne, minusTwo , xx, yy, zz, xx' , id', abs'- , (-+-), (-*-), (.-.), (-.-)+ , (-+-), (-*-), (.-.) , ii, jj, kk, ii' , negate' , ff, gg@@ -53,6 +53,12 @@ , succ' , (-$-) + , (-|-), pair, duple -- synonyms+ , triple+ , quadruple+ , quintuple+ , sixtuple+ , idE , absE , succE@@ -288,6 +294,9 @@ two :: Expr two = showConstant (2 :: Int) +three :: Expr+three = showConstant (3 :: Int)+ minusOne :: Expr minusOne = showConstant (-1 :: Int) @@ -349,11 +358,37 @@ minusE :: Expr minusE = constant "-" ((-) :: Int -> Int -> Int) -(-.-) :: Expr -> Expr -> Expr-e1 -.- e2 = commaE :$ e1 :$ e2+(-|-) :: Expr -> Expr -> Expr+e1 -|- e2 = commaE :$ e1 :$ e2 commaE :: Expr commaE = constant "," ((,) :: Int -> Int -> (Int,Int))++pair :: Expr -> Expr -> Expr+pair = (-|-)++duple :: Expr -> Expr -> Expr+duple = (-|-)++triple :: Expr -> Expr -> Expr -> Expr+triple e1 e2 e3 = ccE :$ e1 :$ e2 :$ e3+ where+ ccE = constant ",," ((,,) :: Int -> Int -> Int -> (Int,Int,Int))++quadruple :: Expr -> Expr -> Expr -> Expr -> Expr+quadruple e1 e2 e3 e4 = cccE :$ e1 :$ e2 :$ e3 :$ e4+ where+ cccE = constant ",,," ((,,,) :: Int -> Int -> Int -> Int -> (Int,Int,Int,Int))++quintuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr+quintuple e1 e2 e3 e4 e5 = ccccE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5+ where+ ccccE = constant ",,,," ((,,,,) :: Int -> Int -> Int -> Int -> Int -> (Int,Int,Int,Int,Int))++sixtuple :: Expr -> Expr -> Expr -> Expr -> Expr -> Expr -> Expr+sixtuple e1 e2 e3 e4 e5 e6 = cccccE :$ e1 :$ e2 :$ e3 :$ e4 :$ e5 :$ e6+ where+ cccccE = constant ",,,,," ((,,,,,) :: Int -> Int -> Int -> Int -> Int -> Int -> (Int,Int,Int,Int,Int,Int)) (-$-) :: Expr -> Expr -> Expr e1 -$- e2 = applyE :$ e1 :$ e2
+ tests/test-creason.hs view
@@ -0,0 +1,61 @@+-- Test library+import Test++-- Functions under test+import Test.Speculate.CondReason++-- Utils+import Test.Speculate.Reason (canonicalEqn, canonicalizeEqn, emptyThy)+import Test.Speculate.Expr (falseE)++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+ [ True++ , creductions1 (zero -<=- yy) (yy -+- abs' yy) (zero -<=- xx, abs' xx, xx)+ == [yy -+- yy]++ , creductions1 (zero -<=- yy) (abs' yy -+- abs' yy) (zero -<=- xx, abs' xx, xx)+ == [yy -+- abs' yy, abs' yy -+- yy]++ , cnormalize+ emptyChy{cequations = [(zero -<=- xx, abs' xx, xx)]}+ (zero -<=- yy) (abs' yy -+- abs' yy)+ == yy -+- yy++ , not+ $ cequivalent+ emptyChy{cequations = []}+ (zero -<=- yy) (abs' yy -+- yy) (yy -+- yy)++ , cequivalent+ emptyChy{cequations = [(zero -<=- xx, abs' xx, xx)]}+ (zero -<=- yy) (abs' yy -+- yy) (yy -+- yy)++ , holds n $ \e1 e2 -> canonicalCEqn compare (falseE,e1,e2) == canonicalEqn emptyThy (e1,e2)+ , holds n $ \e1 e2 -> sndTrd (canonicalizeCEqn compare (falseE,e1,e2))+ == canonicalizeEqn emptyThy (e1,e2)+ , holds n $ \e1 e2 ce -> sndTrd (canonicalizeCEqn compare (falseE,e1,e2))+ == sndTrd (canonicalizeCEqn compare (ce, e1,e2))++ , const True -- TODO: make the following test pass!+ $ let chy = cinsert ( elem' xx xxs+ , insert' xx (xxs -++- yys)+ , insert' xx xxs -++- yys+ )+ emptyChy+ in cnormalize chy (elem' xx xxs) (insert' xx (xxs -++- yys)) == insert' xx xxs -++- yys++ , const True -- TODO: make the following test pass!+ $ creductions1 (elem' xx xxs) (insert' xx (xxs -++- yys))+ ( elem' xx xxs, insert' xx (xxs -++- yys), insert' xx xxs -++- yys)+ == [insert' xx xxs -++- yys]++ , const True -- TODO: make the following test pass!+ $ holds n $ \(BoolE ce) (SameTypeE e1 e2) -> creductions1 ce e1 (ce,e1,e2) == [e2]+ ]+ where+ sndTrd (_,y,z) = (y,z)
+ tests/test-engine.hs view
@@ -0,0 +1,87 @@+-- Test library+import Test++-- Functions under test+import Test.Speculate.Engine++-- Helper functions+import Test.Speculate.Reason (emptyThy)+import Test.Speculate.Utils+import Data.List+import Data.Maybe++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+ [ True+ + , tiersExprTypeCorrect (n*2)++ , holds n $ \e -> mostGeneral e == head (vassignments e)+ , holds n $ \e -> mostSpecific e == last (vassignments e)++ , vassignments (zero -+- xx) == [zero -+- xx]+ , vassignments (zero -+- i_) == [zero -+- xx]+ , vassignments (i_ -+- i_) == [xx -+- yy, xx -+- xx]+ , map canonicalize (vassignments (i_ -+- (i_ -+- ord' c_)))+ == [ xx -+- (yy -+- ord' cc)+ , xx -+- (xx -+- ord' cc) ]++ , vassignments (ii -+- i_) == [ii -+- xx]+ , map canonicalize (vassignments ((i_ -+- i_) -+- (ord' c_ -+- ord' c_)))+ == [ (xx -+- yy) -+- (ord' cc -+- ord' dd)+ , (xx -+- yy) -+- (ord' cc -+- ord' cc)+ , (xx -+- xx) -+- (ord' cc -+- ord' dd)+ , (xx -+- xx) -+- (ord' cc -+- ord' cc) ]++ , holds n $ \e -> all (null . snd) (vars e)+ ==> let xs = map (length . vars) $ vassignments e+ in (head xs >) `all` tail xs+ && (last xs <) `all` init xs+ , holds n $ \e -> all null (map snd $ vars e)+ ==> unrepeatedVars (head (vassignments e))+ , holds n $ \e -> all (null . snd) (vars e)+ ==> let es = vassignments e+ in (`isInstanceOf` head es) `all` tail es+ && (last es `isInstanceOf`) `all` init es+ , holds n $ \e -> allLater (\e1 e0 -> not (e0 `isInstanceOf` e1))+ $ vassignments e+ , holds n $ \e -> let es = vassignments e+ in length (nub (sort es)) == length es+ , holds n $ \e -> length (vassignments e)+ == product (map (bell . snd) . counts $ holes e)++ , equivalencesBetween (===) (i_ -+- i_) (i_ -+- i_)+ == [ ( xx -+- yy, yy -+- xx ) ]++ , equivalencesBetween (===) (i_ -+- (i_ -+- i_)) ((i_ -+- i_) -+- i_)+ == [ ( xx -+- (yy -+- zz), (xx -+- yy) -+- zz )+ , ( xx -+- (yy -+- zz), (xx -+- zz) -+- yy )+ , ( xx -+- (yy -+- zz), (yy -+- xx) -+- zz )+ , ( xx -+- (yy -+- zz), (yy -+- zz) -+- xx )+ , ( xx -+- (yy -+- zz), (zz -+- xx) -+- yy )+ , ( xx -+- (yy -+- zz), (zz -+- yy) -+- xx ) ]++ , holds n $ \(SameTypeE e1 e2) -> unEquation (phonyEquation e1 e2) == (e1,e2)++-- TODO: make the following pass (add ValueE and SameTypeValueE to Test)+--, holds n $ \(SameTypeE e1 e2) (SameTypeE e3 e4)+-- -> subConsequence emptyThy (e1 -==- e2) e3 e4+-- == subConsequence emptyThy (e2 -==- e1) e3 e4+--, holds n $ \(SameTypeE e1 e2) (SameTypeE e3 e4)+-- -> subConsequence emptyThy (e1 -==- e2) e3 e4+-- == subConsequence emptyThy (e1 -==- e2) e4 e3+--, holds n $ \...+-- -> not $ subConsequence emptyThy (e1 -<=- e2) e3 e4+ , subConsequence emptyThy [] (xx -==- yy) (xx -+- yy) (xx -+- xx)+ , not $ subConsequence emptyThy [] (xx -<=- yy) (xx -+- yy) (xx -+- xx)+ , subConsequence emptyThy [(xx -<=- yy, [xx -==- yy])]+ (xx -<=- yy) (xx -+- yy) (xx -+- xx)+ , subConsequence emptyThy [] (abs' xx -==- abs' yy) (abs' xx) (abs' yy)+ , not $ subConsequence emptyThy [] (abs' xx -<=- abs' yy) (abs' xx) (abs' yy)+ , not $ subConsequence emptyThy [] (abs' xx -==- one) (xx -+- abs' xx) zero+ ]+ where+ x === y = equal preludeInstances 1000 x y
+ tests/test-eval.hs view
@@ -0,0 +1,53 @@+-- Test library+import Test++-- Functions under test+import Test.Speculate.Expr.Ground+import Test.Speculate.Utils+import Test.Speculate.Expr++import Data.Maybe++-- TODO: rename test-eval to test-ground++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+ [ True++ , holds n' $ \e -> if isEqE preludeInstances e+ then e === e+ else e =/= e+ , xx -+- yy === yy -+- xx+ , holds n' $ \(IntE e1) (IntE e2) -> e1 -+- e2 === e2 -+- e1+ , xx -+- yy =/= xx -+- xx+ , abs' xx === abs' (abs' xx)+ , abs' (xx -+- abs' xx) === (xx -+- abs' xx) -- 2*x or 0+ , holds n' $ \e1 e2 -> typ e1 /= typ e2 ==> e1 =/= e2++ , holds n' $ zero //= one+ , holds n' $ not $ xx //= yy++ , holds n' $ \e1 e2 -> case equation preludeInstances e1 e2 of+ Just e1e2 -> condEqual preludeInstances 500 e1e2 e1 e2+ Nothing -> True+ , holds n' $ \e1 e2 -> case equation preludeInstances e1 e2 of+ Just e1e2 -> condEqualM preludeInstances 500 0 e1e2 e1 e2+ Nothing -> True+ , fails n' $ \e1 e2 -> case equation preludeInstances e1 e2 of+ Just e1e2 -> condEqualM preludeInstances 500 500 e1e2 e1 e2+ Nothing -> True++ , trueBinds preludeInstances 500 (xx -==- zero) == [[("x",zero)]]+ , trueBinds preludeInstances 500 (xx -==- one) == [[("x",one)]]+ , trueBinds preludeInstances 500 ((xx -==- one) -&&- (yy -==- zero)) == [[("x",one),("y",zero)]]+ ]+ where+ n' = n `div` 50+ x === y = equal preludeInstances 500 x y+ infix 4 ===+ x =/= y = not (x === y)+ infix 4 =/=+ x //= y = inequal preludeInstances 500 x y
tests/test-expr.hs view
@@ -197,6 +197,19 @@ #endif -} + , holds n $ \(IntE e1) (IntE e2) -> isTuple (pair e1 e2)+ && unfoldTuple (pair e1 e2) == [e1,e2]+ , holds n $ \(IntE e1) (IntE e2) (IntE e3) ->+ isTuple (triple e1 e2 e3) && unfoldTuple (triple e1 e2 e3) == [e1,e2,e3]+ , holds n $ \(IntE e1) (IntE e2) (IntE e3) (IntE e4) ->+ isTuple (quadruple e1 e2 e3 e4) &&+ unfoldTuple (quadruple e1 e2 e3 e4) == [e1,e2,e3,e4]+ , holds n $ \(IntE e) -> not (isTuple e) && unfoldTuple e == []+ , holds n $ \(CharE e) -> not (isTuple e) && unfoldTuple e == []+ , holds n $ \(BoolE e) -> not (isTuple e) && unfoldTuple e == []+ , holds n $ \(ListE e) -> not (isTuple e) && unfoldTuple e == []+ , holds n $ \(FunE e) -> not (isTuple e) && unfoldTuple e == []+ , holds n $ \e1 e2 -> e1 `isSub` e2 == (e1 `elem` subexprsV e2) , show (emptyString) == "\"\" :: [Char]"@@ -215,8 +228,12 @@ , show (one -+- one) == "1 + 1 :: Int" , show (minusOne -+- minusOne) == "(-1) + (-1) :: Int" - , show (zero -.- one) == "(0,1) :: (Int,Int)"- , show (minusOne -.- minusOne) == "(-1,-1) :: (Int,Int)"+ , show (zero -|- one) == "(0,1) :: (Int,Int)"+ , show (minusOne -|- minusOne) == "(-1,-1) :: (Int,Int)"+ , show (triple zero one two) == "(0,1,2) :: (Int,Int,Int)"+ , show (quadruple minusOne zero one two) == "(-1,0,1,2) :: (Int,Int,Int,Int)"+ , show (quintuple minusOne zero one two three) == "(-1,0,1,2,3) :: (Int,Int,Int,Int,Int)"+ , show (sixtuple minusTwo minusOne zero one two three) == "(-2,-1,0,1,2,3) :: (Int,Int,Int,Int,Int,Int)" , show (one -:- ll) == "[1] :: [Int]" , show (zero -:- one -:- ll) == "[0,1] :: [Int]"
+ tests/test-match.hs view
@@ -0,0 +1,92 @@+-- Test library+import Test++-- Functions under test+import Test.Speculate.Expr.Match+import Test.Speculate.Expr++-- Helper functions+import Test.Speculate.Utils+import Data.List+import Data.Maybe+import Data.Functor ((<$>)) -- for GHC < 7.10++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+ [ True++ , holds n $ \(IntE e1) (IntE e2) -> match (e1 -+- e2) (xx -+- yy) == Just [("y",e2),("x",e1)]+ , holds n $ \(IntE e) -> match (e -+- e) (xx -+- xx) == Just [("x",e)]+ , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> match (e1 -+- e2) (xx -+- xx) == Nothing+ , holds n $ \(IntE e1) (IntE e2) (IntE e3) -> e2 /= e3+ ==> match ((e1 -+- e1) -+- (e2 -+- e3)) (xx -+- (yy -+- yy)) == Nothing+ , holds n $ \(IntE e1) (IntE e2) -> matchWith [("x",e1)] (e1 -+- e2) (xx -+- yy) == Just [("y",e2),("x",e1)]+ , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> matchWith [("x",e2)] (e1 -+- e2) (xx -+- yy) == Nothing+ , holds n $ \e1 e2 -> e1 `match` e2 == matchWith [] e1 e2+ , holds n $ \(SameTypeE e1 e2) (SameTypeE e3 e4) ->+ not (isFunTy $ typ e1) && not (isFunTy $ typ e3)+ ==>+ (e1 -==- e2) `match` (e3 -==- e4) == (e1,e2) `match2` (e3,e4)+++ , assign "y" (yy -+- zz) ((xx -+- yy) -+- (yy -+- zz))+ == (xx -+- (yy -+- zz)) -+- ((yy -+- zz) -+- zz)++ , ((xx -+- yy) -+- (yy -+- zz)) `assigning` [("y",yy -+- zz)]+ == (xx -+- (yy -+- zz)) -+- ((yy -+- zz) -+- zz)++ , (xx -+- yy) `assigning` [("y",yy -+- zz),("x",xx -+- yy)]+ == (xx -+- yy) -+- (yy -+- zz)++ , sub (xx -+- yy) zero ((xx -+- yy) -+- zz) == (zero -+- zz)+ , sub (xx -+- yy) zero (xx -+- (yy -+- zz)) == (xx -+- (yy -+- zz))++ , holds n $ \(SameTypeE e1 e2) -> sub e1 e2 e1 == e2+ , holds n $ \(IntE e1) (IntE e2) -> sub e1 e2 (e1 -+- e1) == (e2 -+- e2)++ , holds n $ \(SameTypeE e1 e2) -> unify e1 e2 =$ fmap canonicalize $= unify e2 e1++ , unification xx yy == Just [("x",yy)]+ , (canonicalize <$> unify xx yy) == Just xx+ , unification zero zero == Just []+ , unification zero one == Nothing+ , unification xx one == Just [("x",one)]+ , unification (zero -+- xx) (zero -+- one) == Just [("x",one)]+ , unification (zero -+- xx) (yy -+- one) == Just [("x",one),("y",zero)]+ , unify (zero -+- xx) (yy -+- one) == Just (zero -+- one)+ , unification (ff xx) (ff (gg yy)) == Just [("x",gg yy)]+ , unification (ff xx -+- xx) (yy -+- zero) == Just [("x",zero),("y",ff zero)]+ , unify (ff xx -+- xx) (yy -+- zero) == Just (ff zero -+- zero)+ , unification (ff xx) (gg yy) == Nothing+ , unification (ff xx) (ff yy) == unification xx yy+ , (canonicalize <$> unify (negate' (negate' xx) -+- yy) (zz -+- zero))+ == Just (negate' (negate' xx) -+- zero)+ , unification (xx -+- one) (one -+- xx) == Just [("x",one)]+ , unification (xx -+- xx) (one -+- one) == Just [("x",one)]+ , unification (zz -+- zz) (xx -+- yy) == Just [("x",yy),("z",yy)]+ , unification (xx -*- (-+-) xx xx)+ (ff zz -*- (-+-) xx yy) == Just [("y",ff zz),("x",ff zz)]++ -- The following two tests are adapted from Baader and Snyder:+ -- Example 2.8, Chapter 8, Handbook of Automated Reasoning (page 453).+ , unification (hh5 yy zz (ff2 ii ii) (ff2 jj jj) kk) (hh5 (ff2 xx xx) (ff2 yy yy) jj kk zz)+ == Just [ ("i",xx)+ , ("k",ff2 (ff2 xx xx) (ff2 xx xx))+ , ("j",ff2 xx xx)+ , ("z",ff2 (ff2 xx xx) (ff2 xx xx))+ , ("y",ff2 xx xx)+ ]+ , unification (hh7 yy zz xx' (ff2 ii ii) (ff2 jj jj) (ff2 kk kk) ii')+ (hh7 (ff2 xx xx) (ff2 yy yy) (ff2 zz zz) jj kk ii' xx')+ == Just [ ("i",xx)+ , ("i'",ff2 (ff2 (ff2 xx xx) (ff2 xx xx)) (ff2 (ff2 xx xx) (ff2 xx xx)))+ , ("k",ff2 (ff2 xx xx) (ff2 xx xx))+ , ("j",ff2 xx xx)+ , ("x'",ff2 (ff2 (ff2 xx xx) (ff2 xx xx)) (ff2 (ff2 xx xx) (ff2 xx xx)))+ , ("z",ff2 (ff2 xx xx) (ff2 xx xx))+ , ("y",ff2 xx xx)+ ]+ ]
+ tests/test-misc.hs view
@@ -0,0 +1,91 @@+-- Test library+import Test++-- Functions under test+import Test.Speculate.Misc++-- Utils+import Test.Speculate.Expr+import Test.Speculate.Utils++main :: IO ()+main = mainTest tests 10000++-- NOTE: remember that in the expressions returned by functions<N> the+-- variables are actually values (bound by the arguments of the returned+-- function)++tests :: Int -> [Bool]+tests n =+ [ True+ , fillings (ord' c_) [cc,dd,xx] == [ord' cc, ord' dd]++ , map (show *** ($1)) (functions1 (i_ -+- i_) :: [(Expr,Int->Int)])+ == [("x + x :: Int", 2)]++ , map (show *** (($1).($2))) (functions2 (i_ -+- i_) :: [(Expr,Int->Int->Int)])+ == [ ("x + x :: Int", 4)+ , ("x + y :: Int", 3)+ , ("y + x :: Int", 3)+ , ("y + y :: Int", 2) ]++ , map (show *** (($1).($2).($3))) (functions3 (i_ -+- i_) :: [(Expr,Int->Int->Int->Int)])+ == [ ("x + x :: Int",6)+ , ("x + y :: Int",5)+ , ("y + x :: Int",5)+ , ("x + z :: Int",4)+ , ("y + y :: Int",4)+ , ("z + x :: Int",4)+ , ("y + z :: Int",3)+ , ("z + y :: Int",3)+ , ("z + z :: Int",2) ]++ , map (show *** (($1).($2).($3).($4))) (functions4 (i_ -+- i_) :: [(Expr,Int->Int->Int->Int->Int)])+ == [ ("x + x :: Int",8)+ , ("x + y :: Int",7)+ , ("y + x :: Int",7)+ , ("x + z :: Int",6)+ , ("y + y :: Int",6)+ , ("z + x :: Int",6)+ , ("x + w :: Int",5)+ , ("y + z :: Int",5)+ , ("z + y :: Int",5)+ , ("w + x :: Int",5)+ , ("y + w :: Int",4)+ , ("z + z :: Int",4)+ , ("w + y :: Int",4)+ , ("z + w :: Int",3)+ , ("w + z :: Int",3)+ , ("w + w :: Int",2) ]++ , take 3 (expressionsOf [ zero, xx, absE, plusE ])+ == [ [ zero, xx, absE, plusE ]+ , [ abs' zero, abs' xx, plusE :$ zero, plusE :$ xx ]+ , [ abs' (abs' zero)+ , abs' (abs' xx)+ , plusE :$ abs' zero+ , plusE :$ abs' xx+ , zero -+- zero+ , zero -+- xx+ , xx -+- zero+ , xx -+- xx ] ]++ , take 3 (valuedExpressionsOf [ zero, one, absE, plusE ])+ == [ [ (zero, 0 :: Int)+ , (one, 1) ]+ , [ (abs' zero, 0)+ , (abs' one, 1) ]+ , [ (abs' (abs' zero), 0)+ , (abs' (abs' one), 1)+ , (zero -+- zero, 0)+ , (zero -+- one, 1)+ , (one -+- zero, 1)+ , (one -+- one, 2) ] ]++ , take 3 (mapT (id *** ($ (10::Int))) $ valuedExpressionsOf [ zero, one, absE, plusE ])+ == [ [ (absE, 10 :: Int) ]+ , [ (plusE :$ zero, 10)+ , (plusE :$ one, 11) ]+ , [ (plusE :$ abs' zero, 10)+ , (plusE :$ abs' one, 11) ] ]+ ]
+ tests/test-order.hs view
@@ -0,0 +1,91 @@+import Test+import Test.Speculate.Utils++import Test.Speculate.Expr+import Test.Speculate.Reason.Order++main :: IO ()+main = do+ n <- getMaxTestsFromArgs 10000++ reportTests (tests n)+++tests :: Int -> [Bool]+tests n =+ [ True -- see test-expr.hs for general Expr orders++ , holds n $ simplificationOrder (|>|)+ , holds n $ simplificationOrder ( >|)+ , holds n $ simplificationOrder (|> )+ , holds n $ simplificationOrder (dwoBy (<))++ , fails n $ \e1 e2 -> (e1 |>| e2) == (e1 |> e2)+ , fails n $ \e1 e2 -> (e1 |>| e2) == (e1 >| e2)+ , fails n $ \e1 e2 -> (e1 |> e2) == (e1 >| e2)++ , not $ zero |> xx+ , not $ xx |> zero+ , negate' xx |> zero+ , negate' xx -+- xx |> zero+ , zero > xx+ , negateE > zero++ , weight xx == 1+ , weight zero == 1+ , weight (xx -+- zero) == 2+ , weight (one -+- yy) == 2+ , weight (xx -*- (yy -+- zz)) == 3+ , weight ((xx -*- yy) -+- (xx -*- zz)) == 4+ , holds n $ \e1 e2 -> weight (e1 -+- e2) == weight e1 + weight e2+ , holds n $ \e -> weight (e -+- zero) == 1 + weight e+ , holds n $ \e -> weight (abs' e) == 1 + weight e+ , holds n $ \e -> weightExcept absE (abs' e) <= weight e+ , holds n $ \e -> weightExcept absE (negate' e) <= weight e + 1+ , holds n $ \e -> weightExcept absE (abs' e) == weightExcept absE e+ , holds n $ \e -> weightExcept absE (negate' e) == weightExcept absE e + 1++ -- lexicompare is compatible (almost as if by coincidence)+ , fails n $ simplificationOrder lgt+ , holds n $ compatible lgt+ , fails n $ closedUnderSub lgt+ , fails n $ subtermProperty lgt++ -- compareComplexity has the subtermProperty+ , fails n $ simplificationOrder cgt+ , fails n $ compatible cgt+ , fails n $ closedUnderSub cgt+ , holds n $ subtermProperty cgt+ ]+ where+ e1 `lgt` e2 = e1 `lexicompare` e2 == GT+ e1 `cgt` e2 = e1 `compareComplexity` e2 == GT++simplificationOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+simplificationOrder (>) = \e1 e2 e3 -> reductionOrder (>) e1 e2 e3+ && subtermProperty (>) e1++subtermProperty :: (Expr -> Expr -> Bool) -> Expr -> Bool+subtermProperty (>) = \e -> all (e >)+ . filter (\e' -> e' /= e && typ e' == typ e)+ $ subexprs e -- isn't this subexprsV? I don't think so++reductionOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+reductionOrder (>) = \e1 e2 e3 -> strictPartialOrder (>) e1 e2 e3+ && compatible (>) e1 e2 e3+ && closedUnderSub (>) e1 e2 e3++compatible :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+compatible (>) = \e e1 e2 -> e1 > e2 && typ e1 == typ e2+ ==> and [ assign n e1 e > assign n e2 e+ | (t,n) <- vars e+ , t == typ e1+ , t == typ e2 ]++-- The formal definition contains multiple assignments,+-- here, just a single variable is assigned.+closedUnderSub :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+closedUnderSub (>) = \e1 e2 e -> e1 > e2+ ==> and [ assign n e e1 > assign n e e2+ | (t,n) <- vars e1 `nubMerge` vars e2+ , t == typ e ]
+ tests/test-reason.hs view
@@ -0,0 +1,230 @@+{-# LANGUAGE CPP #-}+-- Test library+import Test+import Test.Speculate.Utils++-- Functions under test+import Test.Speculate+import Test.Speculate.Expr+import Test.Speculate.Reason+import Test.Speculate.Reason.Order+import Data.Tuple (swap)+import Data.Function (on)+import Data.List (sortBy,permutations)++theorize' :: [(Expr,Expr)] -> Thy+theorize' eqs = finalize $ foldl (flip insert) emptyThy {closureLimit = 3, keepE = keepMaxOf eqs} eqs++theorize'' :: [(Expr,Expr)] -> Thy+theorize'' eqs = finalize $ foldr insert emptyThy {closureLimit = 3, keepE = keepMaxOf eqs} eqs++main :: IO ()+main = do+ n <- getMaxTestsFromArgs 10000++ reportTests (tests n)++ putStrLn "\nlength (rules $ theorize eqs)"+ reportCountsBy (\(SameTypedPairsE eqs) -> show . length . rules $ theorize eqs)+ (take n list)++ putStrLn "length (equations $ theorize eqs)"+ reportCountsBy (\(SameTypedPairsE eqs) -> show . length . equations $ theorize eqs)+ (take n list)++ putStrLn "\\e1 e2 e3 -> e1 > e2 && typ e1 == typ e2, length (vars e3)"+ reportCountsBy (\(e1,e2,e3) -> if e1 > e2 && typ e1 == typ e2+ then "OK, length " ++ show (length $ vars e3)+ else "Not OK")+ (take n list)++ putStrLn "\\e e1 e2 -> length $ reductions 1 e (e1,e2)"+ reportCountsBy (\(e,e1,e2) -> if e1 > e2 && typ e1 == typ e2+ then "OK, length " ++ show (length $ reductions1 e (e1,e2))+ else "Not OK")+ (take n list)++(~~) :: Expr -> Expr -> (Expr,Expr)+(~~) = (,)+infix 4 ~~++mkThy :: [(Expr,Expr)] -> [(Expr,Expr)] -> Thy+mkThy rs eqs = emptyThy+ { rules = rs+ , equations = eqs }++tests :: Int -> [Bool]+tests n =+ [ True++ -- Listable Thy sound and complete:+ , holds n $ okThy+ , all (`elem` take n list) (take (n`div`10) listThyInefficient)++ , holds n $ \(SameTypedPairsE eqs) -> theorize eqs == theorize (map swap eqs)+ , holds n $ \(SameTypedPairsE eqs) -> theorize eqs == theorize (reverse eqs)++ , holds n $ \(SameTypedPairsE eqs) -> theorize' eqs == theorize eqs+ , holds n $ \(SameTypedPairsE eqs) -> theorize'' eqs == theorize eqs++ , holds n $ okThy . deduce+ , holds n $ idempotent deduce+ , holds n $ \thy -> ((>=) `on` length . equations) (deduce thy) thy+ , holds n $ \thy -> ((==) `on` rules) (deduce thy) thy++ , holds n $ okThy . simplify+ , holds n $ idempotent simplify+ , holds n $ \thy -> ((<=) `on` length . equations) (simplify thy) thy+ , holds n $ \thy -> ((==) `on` rules) (simplify thy) thy++ , holds n $ okThy . delete+ , holds n $ idempotent delete+ , holds n $ \thy -> ((<=) `on` length . equations) (delete thy) thy+ , holds n $ \thy -> ((==) `on` rules) (delete thy) thy++ , holds n $ okThy . orient+ , holds n $ idempotent orient+ , holds n $ \thy -> ((<=) `on` length . equations) (orient thy) thy+ , holds n $ \thy -> ((>=) `on` length . rules) (orient thy) thy+ , holds n $ \thy -> length (equations thy) - length (equations $ orient thy)+ >= length (rules $ orient thy) - length (rules thy)++ , holds n $ okThy . compose+ , holds n $ idempotent compose+ , holds n $ \thy -> ((<=) `on` length . rules) (compose thy) thy+ , holds n $ \thy -> ((==) `on` equations) (compose thy) thy++ , holds n $ okThy . collapse+ , holds n $ idempotent collapse+ , holds n $ \thy -> ((<=) `on` length . rules) (collapse thy) thy+ , holds n $ \thy -> ((>=) `on` length . equations) (collapse thy) thy++ , holds n $ okThy . complete . unThyght++ , holds n $ \(Thyght thy') (SameTypedPairsE eqs) ->+ let thy = complete thy'+ in foldr insert thy eqs == complete (append thy eqs)++ -- TODO: make the following pass with n `div` 10+ -- Inference order should not matter:+ , holds 100+ $ \(Thyght thy) -> all (\steps -> iterateUntil (==) (chain steps) thy == complete thy)+ $ permutations [collapse, compose, orient, delete . simplify, deduce]+ -- I now think the above property is not true in all cases, investigate.++ -- NOTE: the following does not hold in general, only for most of the cases+ , holds 4000+ $ \(Thyght thy') (SameTypeE e1 e2) -> closureLimit thy' > 0 ==>+ let thy = insert (e1,e2)+ $ thy' { keepE = keepUpToLength (max (lengthE e1) (lengthE e2)) }+ in equivalent thy e1 e2++ , holds n $ idempotent finalize++ , criticalPairs emptyThy { rules = [ ((xx -+- yy) -+- zz,xx -+- (yy -+- zz))+ , (negate' xx -+- xx, zero) ] }+ == [ (negate' xx -+- (xx -+- yy),zero -+- yy)+ , ((xx -+- (yy -+- zz)) -+- xx', (xx -+- yy) -+- (zz -+- xx')) ]++ , criticalPairs emptyThy { rules = [ (negate' (negate' xx), id' xx) ] }+ == [ (negate' (id' xx), id' (negate' xx)) ]++ , criticalPairs emptyThy { canReduceTo = dwoBy (\e1 e2 -> e1 `lexicompare` e2 == GT)+ , rules = [ (ff (gg (ff xx)), xx)+ , (ff (gg xx), gg (ff xx)) ] }+ == (let sortuple (x,y) | x < y = (y,x)+ | otherwise = (x,y)+ in nubSort . map sortuple+ $ [ (gg xx, ff (gg (gg (ff xx))))+ , (gg (ff xx), ff (gg xx))+ , (gg (ff (ff xx)), xx)+ , (gg (ff (ff (gg xx))), gg xx) ])++ , criticalPairs emptyThy { rules = [ (ff (gg (ff xx)), xx)+ , (ff (gg xx), gg (ff xx)) ] }+ == [ (gg (ff xx), ff (gg xx))+ , (gg (ff (ff xx)), xx)+ , (ff (gg (gg (ff xx))), gg xx)+ , (gg (ff (ff (gg xx))), gg xx) ]++ , theorize [ (xx -*- yy) -*- (yy -*- zz) ~~ yy ]+ |==|+ [ (xx -*- yy) -*- (yy -*- zz) ~~ yy+ , xx -*- ((xx -*- yy) -*- zz) ~~ xx -*- yy+ , (xx -*- (yy -*- zz)) -*- zz ~~ yy -*- zz+ ] `mkThy` []++ , theorize [ xx -*- (yy -+- zz) ~~ (xx -*- yy) -+- (xx -*- zz)+ , (xx -+- yy) -*- zz ~~ (xx -*- zz) -+- (yy -*- zz) ]+ |==|+ [ (xx -*- yy) -+- (xx -*- zz) ~~ xx -*- (yy -+- zz)+ , (xx -*- yy) -+- (zz -*- yy) ~~ (xx -+- zz) -*- yy+ ] `mkThy` [ (xx -+- xx) -*- yy ~~ xx -*- (yy -+- yy) ]++ , theorizeBy (|>|) [ xx -+- zero ~~ xx+ , xx -+- succ' yy ~~ succ' (xx -+- yy) ]+ |==|+ [ xx -+- zero ~~ xx+ ] `mkThy` [ xx -+- succ' yy ~~ succ' (xx -+- yy) ]++ , theorizeBy (kboBy weight (<))+ [ xx -+- zero ~~ xx+ , xx -+- succ' yy ~~ succ' (xx -+- yy) ]+ |==|+ [ xx -+- zero ~~ xx+ , succ' (xx -+- yy) ~~ xx -+- succ' yy+ , xx -+- succ' zero ~~ succ' xx+ , xx -+- (succ' (succ' zero)) ~~ succ' (succ' xx)+ ] `mkThy` []++ , theorizeBy (|>) [ xx -+- zero ~~ xx+ , xx -+- succ' yy ~~ succ' (xx -+- yy) ]+ |==|+ [ xx -+- zero ~~ xx+ , xx -+- succ' yy ~~ succ' (xx -+- yy)+ ] `mkThy` []++ -- TODO: fix order under GHC <= 7.8+#if __GLASGOW_HASKELL >= 800+ , theorizeBy (dwoBy $ \e1 e2 -> if typ e1 == typ e2+ then e1 > e2+ else typ e1 < typ e2)+ [ ( xx -+- zero, xx )+ , ( xx -+- succ' yy, succ' (xx -+- yy) ) ]+ |==|+ [ ( xx -+- zero, xx )+ , ( succ' (xx -+- yy), xx -+- (succ' yy) )+ ] `mkThy` [ xx -+- (succ' zero) ~~ succ' xx]+#endif++ , theorizeBy (|>) [ ( zero -+- xx, xx )+ , ( negate' xx -+- xx, zero )+ , ( (xx -+- yy) -+- zz, xx -+- (yy -+- zz) ) ]+ |==| [ ( zero -+- xx , xx )+ , ( negate' xx -+- xx , zero )+ , ( (xx -+- yy) -+- zz , xx -+- (yy -+- zz) )+ , ( negate' xx -+- (xx -+- yy) , yy )+ , ( xx -+- zero , xx )+ , ( xx -+- (negate' xx -+- yy) , yy )+ , ( negate' (negate' xx) , xx )+ , ( negate' zero , zero )+ , ( xx -+- negate' xx , zero )+ ] `mkThy` []++ , theorizeBy (kboBy (weightExcept negateE) (gtExcept (>) negateE))+ [ ( zero -+- xx, xx )+ , ( negate' xx -+- xx, zero )+ , ( (xx -+- yy) -+- zz, xx -+- (yy -+- zz) ) ]+ |==| [ ( zero -+- xx , xx )+ , ( negate' xx -+- xx , zero )+ , ( (xx -+- yy) -+- zz , xx -+- (yy -+- zz) )+ , ( negate' xx -+- (xx -+- yy) , yy )+ , ( negate' zero -+- xx , xx )+ , ( xx -+- zero , xx )+ , ( xx -+- (negate' xx -+- yy) , yy )+ , ( negate' (negate' xx) , xx )+ , ( xx -+- negate' xx , zero )+ ] `mkThy` [( negate' zero, zero )]++ -- TODO: restore tests losts after removing test-kbc+ ]
+ tests/test-stats.hs view
@@ -0,0 +1,46 @@+-- Test library+import Test++-- Helper+import Data.Function (on)++-- Functions under test+import Test.Speculate+import Test.Speculate.Expr+import Test.Speculate.Reason+import Test.Speculate.Utils++main :: IO ()+main = do+ n <- getMaxTestsFromArgs 10000++ putStrLn "typ (e :: Expr)"+ reportCountsBy typ (take n list :: [Expr])++ putStrLn "lengthE (e :: Expr)"+ reportCountsBy lengthInterval (take n list :: [Expr])++ putStrLn "typ (e1 :: Expr) == typ (e2 :: Expr)"+ reportCountsBy equalTypes (take n list)++ putStrLn "typ (e1 :: Expr) == typ (e2 :: Expr)"+ reportCountsBy equalTypes . map unSameTypeE . take n $ list++ putStrLn "okThy thy"+ reportCountsBy (show . okThy) (take n list)++ putStrLn "length (equations thy)"+ reportCountsBy (show . length . equations) (take n list)++ putStrLn "length (rules thy)"+ reportCountsBy (show . length . rules) (take n list)++ putStrLn "length (equations thy + rules thy)"+ reportCountsBy (show . length . (\thy -> rules thy ++ equations thy)) (take n list)++lengthInterval :: Expr -> (Int,Int)+lengthInterval e = (l, l+2) where l = (lengthE e `div` 3) * 3++equalTypes :: (Expr,Expr) -> String+equalTypes (e1,e2) | typ e1 == typ e2 = show (typ e1)+ | otherwise = "invalid"
+ tests/test-utils.hs view
@@ -0,0 +1,129 @@+-- Test library+import Test++-- Functions under test+import Test.Speculate.Utils++-- Helper functions+import Data.List+import Data.Function++import Test.LeanCheck.Utils (comparison)++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+ [ True+ + -- iss is sound+ , and [ length xs == n | m <- [0..5], n <- [0..5], xs <- iss m n ]+ , and [ head (iss 0 n) == [0..(n-1)] | n <- [0..10] ]+ , and [ last (iss 0 n) == replicate n 0 | n <- [0..10] ]+ , and [ firsts xs `isPrefixOf` [0..] | n <- [0..10], xs <- iss 0 n ]+ , holds 100 $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys+ ==> strictlyOrdered (nubMerge xs (ys::[Int]))+ , and [ nubMerge xs xs == xs | n <- [0..10], let xs = [0..n] ]++ , holds 100 $ \xss -> ordered . concat $ discardLaterT (<=) (xss::[[Int]])+ , (length . concat $ discardLaterT (<=) [[1..100]]) == 100++ , collectOn snd [(1,2),(2,2),(2,3),(3,3)] == [[(1,2),(2,2)],[(2,3),(3,3)]]+ , collectOn fst [(1,2),(2,2),(2,3),(3,3)] == [[(1,2)],[(2,2),(2,3)],[(3,3)]]+ , collectOn (uncurry (+)) [(1,2),(2,2),(2,3),(3,3)] == [[(1,2)],[(2,2)],[(2,3)],[(3,3)]]+ , collectBy (compare `on` snd) [(1,2),(2,2),(2,3),(3,3)] == [[(1,2),(2,2)],[(2,3),(3,3)]]++ , holds n $ \x -> medianate (,) [x::Int] == [(x,x)]+ , holds n $ \x y -> medianate (,) [x::Int,y] == [(x,y)]+ , holds n $ \x y z -> medianate (,) [x::Int,y,z] == [(x,z),(y,y)]+ , holds n $ \x y z w -> medianate (,) [x::Int,y,z,w] == [(x,w),(y,z)]+ , holds n $ \x y z w v -> medianate (,) [x::Int,y,z,w,v] == [(x,v),(y,w),(z,z)]+ , holds n $ \x y z w v u -> medianate (,) [x::Int,y,z,w,v,u] == [(x,u),(y,v),(z,w)]++ , all (\f -> discardOthers f [] == ([]::[Int])) [(<=),(>=),(<),(>),(==),(/=),\x y -> True]+ , holds n $ \x -> all (\f -> discardOthers f [x] == [x::Int])+ [(<=),(>=),(<),(>),(==),(/=),\x y -> True]+ , holds n $ \xs -> not (null xs) ==> discardOthers (<=) xs == [maximum xs::Int]+ , holds n $ \xs -> not (null xs) ==> discardOthers (>=) xs == [minimum xs::Int]+ , holds n $ \xs -> not (null xs) ==>+ discardOthers (<) xs == replicate (count (maximum xs) xs) (maximum xs::Int)+ , holds n $ \xs -> not (null xs) ==>+ discardOthers (>) xs == replicate (count (minimum xs) xs) (minimum xs::Int)++ , ["x","y","z","x'","y'"] `isPrefixOf` namesFromTemplate "x"+ , ["xs","ys","zs","xs'"] `isPrefixOf` namesFromTemplate "xs"+ , ["xss","yss","zss","xss'"] `isPrefixOf` namesFromTemplate "xss"+ , ["c","d","e","c'","d'"] `isPrefixOf` namesFromTemplate "c"+ , ["s","t","u","s'","t'"] `isPrefixOf` namesFromTemplate "s"+ , ["0","1","2","3","4"] `isPrefixOf` namesFromTemplate "0"+ , ["1","2","3","4","5"] `isPrefixOf` namesFromTemplate "1"+--, ["z","a","b","z'","a'"] `isPrefixOf` namesFromTemplate "z" -- TODO: make this pass+ , ["x1","x2","x3","x4"] `isPrefixOf` namesFromTemplate "x1"+ , ["a0","a1","a2","a3"] `isPrefixOf` namesFromTemplate "a0"+ , ["e1","e2","e3","e4"] `isPrefixOf` namesFromTemplate "e1"+ , ["xs1","xs2","xs3"] `isPrefixOf` namesFromTemplate "xs1"+ , ["xy","zw","xy'","zw'"] `isPrefixOf` namesFromTemplate "xy"+ , ["ab","cd","ab'","cd'"] `isPrefixOf` namesFromTemplate "ab"+ , ["xys","zws","xys'"] `isPrefixOf` namesFromTemplate "xys"+ , ["xyz","xyz'","xyz''"] `isPrefixOf` namesFromTemplate "xyz"++ , table "l l l" [ ["asdf", "qwer", "zxvc\nzxvc"]+ , ["0", "1", "2"]+ , ["123", "456\n789", "3"] ] ==+ "asdf qwer zxvc\n\+ \ zxvc\n\+ \0 1 2\n\+ \123 456 3\n\+ \ 789\n"++ , table "r l l" [ ["asdf", "qwer", "zxvc\nzxvc"]+ , ["0", "1", "2"]+ , ["123", "456\n789", "3"] ] ==+ "asdf qwer zxvc\n\+ \ zxvc\n\+ \ 0 1 2\n\+ \ 123 456 3\n\+ \ 789\n"++ , table "r r l" [ ["asdf", "qwer", "zxvc\nzxvc"]+ , ["0", "1", "2"]+ , ["123", "456\n789", "3"] ] ==+ "asdf qwer zxvc\n\+ \ zxvc\n\+ \ 0 1 2\n\+ \ 123 456 3\n\+ \ 789\n"++ -- different versions of GHC/typeable impose different orders on TypeReps,+ -- hence: map show . sort+ , (sort . map show . typesIn $ typeOf (undefined :: (Int -> Int) -> Int -> Bool))+ == ["Bool","Int"]+ , (sort . map show . typesIn $ typeOf (undefined :: (Int -> Char) -> Integer -> Bool))+ == ["Bool","Char","Int","Integer"]++ , splitAtCommas "1,2,3" == ["1","2","3"]+ , splitAtCommas "123,456,789," == ["123","456","789"]+ , splitAtCommas "123 456,789" == ["123","456","789"] -- weird behaviour, but fine for speculate++ , compareIndex [3,2,1] 3 1 == LT+ , compareIndex [3,2,1] 1 3 == GT+ , compareIndex [3,2,1] 4 1 == GT+ , compareIndex [3,2,1] 1 0 == LT+ , holds n $ \xs -> comparison (compareIndex (xs::[Int]))++ , partitionByMarkers '#' '*' "" == ("","")+ , partitionByMarkers '#' '*' "abc*def" == ("abc","def")+ , partitionByMarkers '#' '*' "abcdef" == ("abcdef","")+ , partitionByMarkers '#' '*' "#abcdef" == ("abcdef","")+ , partitionByMarkers '#' '*' "abc#def" == ("abcdef","")+ , partitionByMarkers '#' '*' "*ab#cd" == ("cd","ab")+ , partitionByMarkers '#' '*' "abc#def*ghi*jkl#mno*pqr#stu" == ("abcdefmnostu","ghijklpqr")+ , partitionByMarkers '#' '*' "#foreground*background#foreground" == ("foregroundforeground","background")++ , holds n $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys+ ==> strictlyOrdered (xs +++ ys :: [Int])+ , holds n $ \xs ys -> xs +++ ys == ys +++ (xs :: [Int])+ , holds n $ \xs ys -> strictlyOrdered xs && strictlyOrdered ys+ ==> xs +++ ys == nubSort (xs ++ ys :: [Int])+ ]