speculate (empty) → 0.2.0
raw patch · 39 files changed
+5561/−0 lines, 39 filesdep +basedep +cmdargsdep +containerssetup-changed
Dependencies added: base, cmdargs, containers, leancheck
Files
- LICENSE +30/−0
- README.md +148/−0
- Setup.hs +2/−0
- TODO.md +204/−0
- eg/plus-abs.hs +15/−0
- speculate.cabal +86/−0
- src/Test/Speculate.hs +100/−0
- src/Test/Speculate/Args.hs +276/−0
- src/Test/Speculate/CondReason.hs +138/−0
- src/Test/Speculate/Engine.hs +234/−0
- src/Test/Speculate/Expr.hs +16/−0
- src/Test/Speculate/Expr/Canon.hs +35/−0
- src/Test/Speculate/Expr/Core.hs +416/−0
- src/Test/Speculate/Expr/Equate.hs +119/−0
- src/Test/Speculate/Expr/Ground.hs +111/−0
- src/Test/Speculate/Expr/Match.hs +191/−0
- src/Test/Speculate/Expr/TypeInfo.hs +243/−0
- src/Test/Speculate/Misc.hs +120/−0
- src/Test/Speculate/Reason.hs +480/−0
- src/Test/Speculate/Reason/Order.hs +145/−0
- src/Test/Speculate/Report.hs +144/−0
- src/Test/Speculate/Sanity.hs +69/−0
- src/Test/Speculate/SemiReason.hs +107/−0
- src/Test/Speculate/Utils.hs +24/−0
- src/Test/Speculate/Utils/Class.hs +41/−0
- src/Test/Speculate/Utils/Colour.hs +304/−0
- src/Test/Speculate/Utils/Digraph.hs +65/−0
- src/Test/Speculate/Utils/List.hs +205/−0
- src/Test/Speculate/Utils/Memoize.hs +43/−0
- src/Test/Speculate/Utils/Misc.hs +116/−0
- src/Test/Speculate/Utils/Ord.hs +16/−0
- src/Test/Speculate/Utils/PrettyPrint.hs +111/−0
- src/Test/Speculate/Utils/String.hs +144/−0
- src/Test/Speculate/Utils/Tiers.hs +45/−0
- src/Test/Speculate/Utils/Timeout.hs +35/−0
- src/Test/Speculate/Utils/Tuple.hs +81/−0
- src/Test/Speculate/Utils/Typeable.hs +64/−0
- tests/Test.hs +648/−0
- tests/test-expr.hs +190/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2016, Rudy Matela Braquehais++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * 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.++ * Neither the name of Rudy Matela Braquehais nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS 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 COPYRIGHT+OWNER 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.
+ README.md view
@@ -0,0 +1,148 @@+Speculate+=========++Speculate automatically discovers laws about Haskell functions.+Give Speculate a bunch of Haskell functions and it will discover laws like:++ * equations, such as `id x == x`;+ * inequalities, such as `0 <= x * x`;+ * conditional equations, such as `x <= 0 ==> x + abs x == 0`.++Speculate is similar to, and inspired by, [QuickSpec].+++Crash Course+------------++Install pre-requisites:++ $ cabal install cmdargs+ $ cabal install leancheck++Clone and enter the repository:++ $ git clone https://github.com/rudymatela/speculate+ $ cd speculate++There are some examples in the `eg` folter. For example `eg/plus-abs.hs`:++ $ cat eg/plus-abs.hs+ ...+ ...++Compile and run with:++ $ ghc -isrc eg/plus-abs.hs+ $ ./eg/plus-abs+ ...+++Installing Speculate+--------------------++Pre-requisites are [cmdargs] and [leancheck].+You can install them with:++ $ cabal install cmdargs+ $ cabal install leancheck++No `cabal` package has been made yet. For now, clone the repository with:++ $ git clone https://github.com/rudymatela/speculate++and compile programs that use it with:++ $ ghc -ipath/to/speculate/src program.hs+++Using Speculate+---------------++Speculate is used as a library: import it, then call the function `speculate`+with relevant arguments. The following program Speculates about the functions+`(+)` and `abs`:++ import Test.Speculate++ main :: IO ()+ main = speculate args+ { constants =+ [ showConstant (0::Int)+ , showConstant (1::Int)+ , constant "+" ((+) :: Int -> Int -> Int)+ , constant "abs" (abs :: Int -> Int)+ ]+ }++when run, it prints the following:++ _ :: Int (holes: Int)+ 0 :: Int+ 1 :: Int+ (+) :: Int -> Int -> Int+ abs :: Int -> Int++ abs (abs x) == abs x+ x + 0 == x+ x + y == y + x+ (x + y) + z == x + (y + z)+ abs (x + abs x) == x + abs x+ abs x + abs x == abs (x + x)+ abs (1 + abs x) == 1 + abs x++ x <= abs x+ 0 <= abs x+ x <= x + 1+++Now, if we add `<=` and `<` as background constants on `args`++ , constants =+ [ showConstant (0::Int)+ , showConstant (1::Int)+ , constant "+" ((+) :: Int -> Int -> Int)+ , constant "abs" (abs :: Int -> Int)+ , background+ , constant "<=" ((<=) :: Int -> Int -> Bool)+ , constant "<" ((<) :: Int -> Int -> Bool)+ ]++then run again, we get the following as well:++ y <= x ==> abs (x + abs y) == x + abs y+ x <= 0 ==> x + abs x == 0+ abs x <= y ==> abs (x + y) == x + y+ abs y <= x ==> abs (x + y) == x + y++For more examples, see the [eg](eg) folder.+++Similarities and Differences to QuickSpec+-----------------------------------------++Speculate is inspired by [QuickSpec].+Like QuickSpec, Speculate uses testing to speculate equational laws about given+Haskell functions. There are some differences:++| | Speculate | QuickSpec |+| ----------------: | ------------------------- | --------------------------------- |+| testing | enumerative ([LeanCheck]) | random ([QuickCheck]) |+| equational laws | yes (after completion) | yes (as discovered) |+| inequational laws | yes | no |+| conditional laws | yes | restricted to a set of predicates |+| polymorphism | no | yes |+| performance | slower | faster |++For most examples, Speculate runs slower than QuickSpec 2 but faster than QuickSpec 1.+++More documentation+------------------++For more examples, see the [eg](eg) and [bench](bench) folders.++[leancheck]: https://hackage.haskell.org/package/leancheck+[LeanCheck]: https://hackage.haskell.org/package/leancheck+[QuickSpec]: https://github.com/nick8325/quickspec+[QuickCheck]: https://hackage.haskell.org/package/QuickCheck+[cmdargs]: https://hackage.haskell.org/package/cmdargs
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ TODO.md view
@@ -0,0 +1,204 @@+TODO+====++A non-exhaustive list of things TODO for Speculate++Warning: I tend to ramble...+++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.++* improve printing by separating variables, constants and background constants.++* derive `tiers` using speculate itself. Use provided constructors.+ Maybe a new field in args? Or even things begining with capital letters and+ ":".++++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+---------------++* after adding:++ constant "/=" $ (/=) -:> integer++ to `backgroundConstants`, these:++ (q == negate q) == False+ (q == q + r) == False++ along with a handful of other strange laws appear.+ Find out why and remove them.+++* see commit `f7b323a`, why does the following equation disappears after+ requiring a minimum number of tests to pass?++ x /= y ==> delete y (insert x Null) == insert x Null++ The precondition should hold most of the time, so, a minimum number of+ tests should not discard it.+++redundancy to remove+--------------------++* remove redundancy on taut example:++ taut q ==> subst n (taut q) p == subst n True p++ pruning principle:+ 1. `genericMatch LHS RHS = [(taut q, True)]`+ 2. `equivalent thy (taut q) (taut q == True)`++* remove the following redundant laws on insertsort:++ ordered (ys ++ xs) ==> ys ++ sort xs == sort (xs ++ ys)+ ordered (ys ++ xs) ==> sort ys ++ xs == sort (xs ++ ys)+ ordered (ys ++ xs) ==> sort ys ++ sort xs == sort (xs ++ ys)++ implied by `ordered (sort xs) == True` *and* `sort (xs++ys) == sort (ys++xs)`++* on `./eg/insertsort`, we get:++ xs == sort ys ==> ordered xs+ (sort xs == []) == (xs == [])++ those are consequences of substitution++* On `./eg/digraphs -s6`, I get+ `False == isNode x a ==> succs x a == preds x a`+ (and other related equations.) A more general version wouldn't be+ `False == isNode x a ==> succs x a == []`?++ I checked on ghci, it does hold for 30000 tests, so the library isn't buggy.++ Maybe the issue is that `== []` is redundant and discarded?++ There are lots of other redundant equations there. Maybe those are related+ to the planned genericMatch pruning principle? (see a bit above)++* On `./eg/binarytree`, when toList and fromList are moved into the foreground,+ the following redundant laws appear:++ (xs == []) == (Null == fromList xs)+ xs == toList t ==> ordered xs+ xs == toList t ==> strictlyOrdered xs+ xs == toList t ==> t == fromList xs+++Later Later+-----------++* improve performance of inequality generation by using the following+ algorithm:++ 1. compute a theory and equivalence classes of schemas as usual;+ 2. from classes of schemas, build class representatives of canonical+ expressions (first occurrences in lexicographic order);+ 3. rehole those representatives then compute <= relations+ 4. expand <= expressions, filtering those that are true and discarding+ redundancies "internally" (within possible variable namings)+ 5. filter redundant <= expressions. I believe this has to be adapted a+ tiny bit.++ I am not sure if it will work. But it might be worth a try.++* print errors on stderr, not on stdout++* add maximum commutative size limit?++* 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+ undefined.++* (for performance) note that variable assignments form a lattice. So I only+ need to test stuff from upper if the lower is true. Of course, testing is+ the expensive thing. But it does not pay off to test x + y = z + w before+ 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 the TypeInfo. This way, background will look nicer,+ with less functions and values. Computing the size of values and expressions+ may be a problem.++* (for interface) make dwoList, where the order between expressions is given by+ the order in which they appear in a list. Note this *cannot* be composed+ with a lexicographical order (as it could break transitivity, I think).+ Better raise an error in case a symbol is not in the list. On second thought,+ 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:+ - complete -- 88%+ - deduce -- 79%+ - normalizedCP -- 78%+ - normalize -- 68%+ I don't think normalizedCriticalPairs / normalize can be optimized any+ further. Maybe the problem comes with complete itself, that should deduce+ less often or even maybe interleave steps more often. Maybe adding+ normalizedCriticalPairs as soon as I add a rule? Running deduce twice less+ often does not help, as other steps take a bit over and deduce still accounts+ for a high percentage (let's say 60%). Possible fixes:+ - implement deduce2, simplify2, compose2 and collapse2 from unfailing+ completion+ - finish groundJoinable from "Ordered Rewriting and Confluence" by+ adding one last condition++* 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`
+ eg/plus-abs.hs view
@@ -0,0 +1,15 @@+import Test.Speculate++main :: IO ()+main = speculate args+ { constants =+ [ constant "+" ((+) :: Int -> Int -> Int)+ , constant "id" (id :: Int -> Int)+ , constant "abs" (abs :: Int -> Int)+ , background+ , showConstant (0::Int)+ , showConstant (1::Int)+ , constant "<=" ((<=) :: Int -> Int -> Bool)+ , constant "<" ((<) :: Int -> Int -> Bool)+ ]+ }
+ speculate.cabal view
@@ -0,0 +1,86 @@+name: speculate+version: 0.2.0+synopsis: discovery of properties about Haskell functions+description:+ Speculate automatically discovers laws about Haskell functions.+ Give Speculate a bunch of Haskell functions and it will discover laws like:+ .+ * equations, such as 'id x == x';+ .+ * inequalities, such as '0 <= x * x';+ .+ * conditional equations, such as 'x <= 0 ==> x + abs x == 0'.++homepage: https://github.com/rudymatela/speculate#readme+license: BSD3+license-file: LICENSE+author: Rudy Matela, Colin Runciman+maintainer: Rudy Matela <rudy@matela.com.br>+category: Testing+build-type: Simple+cabal-version: >=1.10++extra-doc-files: README.md+ , TODO.md+tested-with: GHC==8.0, GHC==7.10, GHC==7.8, GHC==7.6, GHC==7.4++source-repository head+ type: git+ location: https://github.com/rudymatela/speculate++source-repository this+ type: git+ location: https://github.com/rudymatela/speculate+ tag: v0.2.0+++library+ exposed-modules: Test.Speculate+ , Test.Speculate.Args+ , Test.Speculate.Report+ , Test.Speculate.Engine+ , Test.Speculate.Expr+ , Test.Speculate.Expr.Canon+ , Test.Speculate.Expr.Core+ , Test.Speculate.Expr.Equate+ , Test.Speculate.Expr.Ground+ , Test.Speculate.Expr.Match+ , Test.Speculate.Expr.TypeInfo+ , Test.Speculate.Reason+ , Test.Speculate.Reason.Order+ , Test.Speculate.SemiReason+ , Test.Speculate.CondReason+ , Test.Speculate.Sanity+ , Test.Speculate.Misc+ other-modules: Test.Speculate.Utils+ , Test.Speculate.Utils.Class+ , Test.Speculate.Utils.Colour+ , Test.Speculate.Utils.Digraph+ , Test.Speculate.Utils.List+ , Test.Speculate.Utils.Memoize+ , Test.Speculate.Utils.Misc+ , Test.Speculate.Utils.Ord+ , Test.Speculate.Utils.PrettyPrint+ , Test.Speculate.Utils.String+ , Test.Speculate.Utils.Tiers+ , Test.Speculate.Utils.Timeout+ , Test.Speculate.Utils.Tuple+ , Test.Speculate.Utils.Typeable+ build-depends: base >= 4 && < 5, leancheck >= 0.6.1, cmdargs, containers+ hs-source-dirs: src+ default-language: Haskell2010++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++benchmark plus-abs+ main-is: plus-abs.hs+ build-depends: base >= 4 && < 5, leancheck, cmdargs, containers+ hs-source-dirs: src, eg+ default-language: Haskell2010+ type: exitcode-stdio-1.0
+ src/Test/Speculate.hs view
@@ -0,0 +1,100 @@+-- | __ Speculate: discovery of properties by reasoning from test results __+--+-- Speculate automatically discovers laws about Haskell functions.+-- Those laws involve:+--+-- * equations, such as @ id x == x @;+-- * inequalities, such as @ 0 <= x * x @;+-- * conditional equations, such as @ x \<= 0 ==\> x + abs x == 0 @.+--+-- _Example:_ the following program prints laws about @0@, @1@, @+@ and @abs@.+--+-- > import Test.Speculate+-- >+-- > main :: IO ()+-- > main = speculate args+-- > { constants =+-- > [ showConstant (0::Int)+-- > , showConstant (1::Int)+-- > , constant "+" ((+) :: Int -> Int -> Int)+-- > , constant "abs" (abs :: Int -> Int)+-- > , background+-- > , constant "<=" ((<=) :: Int -> Int -> Bool)+-- > ]+-- > }+module Test.Speculate+ ( speculate+ , Args (..)+ , args++ -- * The constants list+ -- | The following combinators are used to build+ -- the 'constants' list from 'Args'.+ , Expr+ , constant+ , showConstant+ , hole+ , foreground+ , background++ -- * The instances list+ -- | The following combinators are used to build+ -- the 'instances' list from 'Args'.+ , Instances+ , ins, eq, ord, eqWith, ordWith, names++ -- * Misc.+ , report+ , getArgs++ -- useful for declaring Listable instances+ , module Test.LeanCheck++ -- test types & type binding operators:+ , module Test.LeanCheck.Utils++ -- useful export for GHC < 7.10:+ , module Data.Typeable+ )+where++import Data.Typeable+import Test.LeanCheck+import Test.LeanCheck.Utils hiding (comparison)++import Test.Speculate.Expr+ ( Expr+ , constant+ , var+ , hole+ , showConstant+ , Instances+ , ins+ , eq+ , eqWith+ , ord+ , ordWith+ , names+ )+import Test.Speculate.Args+ ( Args (..)+ , args+ , getArgs+ , foreground+ , background+ , processArgs+ , prepareArgs+ , HelpFormat (..)+ , helpText+ , showHelp+ )+import Test.Speculate.Report (report)++-- | Calls Speculate. See the example above (at the top of the file).+-- Its only argument is an 'Args' structure.+speculate :: Args -> IO ()+speculate args = do+ as <- processArgs (prepareArgs args)+ if showHelp as+ then print $ helpText [] HelpFormatDefault (prepareArgs args)+ else report as
+ src/Test/Speculate/Args.hs view
@@ -0,0 +1,276 @@+module Test.Speculate.Args+ ( Args (..)+ , args++ , foreground+ , background++ , getArgs+ , computeMaxSemiSize+ , computeMaxCondSize+ , computeInstances+ , types+ , atoms+ , compareExpr+ , keepExpr+ , timeout+ , shouldShowEquation+ , shouldShowConditionalEquation+ , reallyShowConditions++ -- TODO: remove the following exports eventually:+ , prepareArgs+ , module System.Console.CmdArgs.Explicit+ )+where++import Test.Speculate.Expr+import Test.Speculate.Utils+import System.Console.CmdArgs.Explicit++import qualified Data.List as L (insert)+import Data.List hiding (insert)+import Data.Maybe (catMaybes)+import Data.Monoid ((<>))+++-- | Arguments to Speculate+data Args = Args+ { maxSize :: Int -- ^ maximum size of considered expressions+ , maxTests :: Int -- ^ maximum number of test for each law+ , constants :: [Expr] -- ^ constants considered when generating expressions+ , instances :: [Instances] -- ^ typeclass instance information for @Eq@, @Ord@ and @Listable@+ , maxSemiSize :: Int -- ^ maximum size of inqualities RHS/LHS+ , maxCondSize :: Int -- ^ maximum size of considered condition+ , maxVars :: Int -- ^ maximum number of variables allowed in inequalities and conditional equations++ , showConstants :: Bool -- ^ repeat constants on output+ , showEquations :: Bool -- ^ whether to show equations+ , showSemiequations :: Bool -- ^ whether to show inequalties+ , showConditions :: Bool -- ^ whether to show conditional equations+ , showConstantLaws :: Bool -- ^ whether to show laws with no variables++ , minTests :: Int -> Int -- ^ __(intermediary)__ minimum number of tests+ -- for passing postconditions in function of+ -- 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+ , 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+ , evalTimeout :: Maybe Double -- ^ __(advanced)__ timeout when evaluating ground expressions+ , force :: Bool -- ^ __(advanced)__ ignore errors+ , extra :: [String] -- ^ __(advanced)__ unused, user-defined meaning+ , exclude :: [String] -- ^ __(advanced)__ exclude this symbols from signature before running+ , onlyTypes :: [String] -- ^ __(advanced)__ only allow those types at top-level equations / semi-equations+ , showClassesFor :: [Int] -- ^ __(advanced)__ show equivalence classes of expressions+ , showDot :: Bool -- ^ __(advanced)__ whether to show a Graphviz dotfile with an Ord lattice+ , quietDot :: Bool -- ^ __(advanced)__ whether to show a Graphviz dotfiel with an Ord lattice (less verbose)+ }+-- TODO: future options:+--, closureLimit :: Int+--, order :: OptOrder -- data OptOrder = Dershowitz | KnuthBendix+--, maxRuleSize :: Maybe Int+--, maxEquationSize :: Maybe Int+--, keepRewriteRules :: Bool+-- Maybe add an empty Thy here.++-- | Default arguments to Speculate+args :: Args+args = Args+ { maxSize = 5+ , maxTests = 500+ , minTests = \n -> n `div` 20 -- defaults to 5% of maxTests+ , maxSemiSize = -1+ , maxCondSize = -1+ , maxDepth = Nothing+ , instances = []+ , showConstants = True+ , showArgs = True+ , showTheory = False+ , showEquations = True+ , showSemiequations = True+ , showConditions = True+ , showConstantLaws = False+ , showDot = False+ , quietDot = False+ , showClassesFor = []+ , maxVars = 2+ , maxConstants = Nothing+ , evalTimeout = Nothing+--, closureLimit = 2+--, order = Dershowitz+--, maxRuleSize = Nothing+--, maxEquationSize = Nothing+--, keepRewriteRules = False+ , showHelp = False+ , force = False+ , extra = []+ , constants = []+ , exclude = []+ , onlyTypes = []+ }+++computeMaxSemiSize :: Args -> Int+computeMaxSemiSize args+ | maxSemiSize args > 0 = maxSemiSize args+ | otherwise = maxSize args + maxSemiSize args++computeMaxCondSize :: Args -> Int+computeMaxCondSize args+ | maxCondSize args > 0 = maxCondSize args+ | otherwise = maxSize args + maxCondSize args++computeInstances :: Args -> Instances+computeInstances args = concat (instances args) ++ preludeInstances++shouldShow2 :: Args -> (Expr,Expr) -> Bool+shouldShow2 args (e1,e2) = showConstantLaws args || hasVar e1 || hasVar e2+-- `allAbout` constants // (conditionAtoms `union` equationAtoms)++shouldShowEquation :: Args -> (Expr,Expr) -> Bool+shouldShowEquation args (e1,e2) =+ shouldShow2 args (e1,e2) && (e1 `about` fore || e2 `about` fore)+ where+ fore = foregroundConstants args++shouldShow3 :: Args -> (Expr,Expr,Expr) -> Bool+shouldShow3 args (e1,e2,e3) = showConstantLaws args+ || hasVar e1 || hasVar e2 || hasVar e3++shouldShowConditionalEquation :: Args -> (Expr,Expr,Expr) -> Bool+shouldShowConditionalEquation args (ce,e1,e2) = shouldShow3 args (ce,e1,e2)+ && cem ce e1 e2+ && (ce `about` fore+ || e1 `about` fore+ || e2 `about` fore)+ where+ cem = condEqualM (computeInstances args) (maxTests args) (minTests args (maxTests args))+ fore = foregroundConstants args++keepExpr :: Args -> Expr -> Bool+keepExpr Args{maxConstants = Just n} e | length (consts e) > n = False+keepExpr Args{maxDepth = Just n} e | depthE e > n = False+keepExpr _ _ = True++reallyShowConditions :: Args -> Bool+reallyShowConditions args = showConditions args+ && boolTy `elem` map (finalResultTy . typ) (allConstants args)++atoms :: Args -> [Expr]+atoms args = map holeOfTy ts+ `union` allConstants args+ `union` [showConstant True | showConds || showDot args]+ `union` [showConstant False | showConds || showDot args]+ `union` catMaybes [eqE (computeInstances args) t | t <- ts, showConds]+ where+ ts = types args+ showConds = reallyShowConditions args++types :: Args -> [TypeRep]+types = nubMergeMap (typesIn . typ) . allConstants++foregroundConstants, backgroundConstants :: Args -> [Expr]+foregroundConstants = fst . partitionByMarkers foreground background . constants+backgroundConstants = snd . partitionByMarkers foreground background . constants++allConstants :: Args -> [Expr]+allConstants args = discard (\c -> any (c `isConstantNamed`) (exclude args))+ $ discard (\e -> e == foreground || e == background)+ $ constants args++-- | Are all constants in an expression about a list of constants?+-- Examples in pseudo-Haskell:+--+-- > x + y `allAbout` [(+)] == True+-- > x + y == z `allAbout` [(+)] == False+-- > x + y == z `allAbout` [(+),(==)] == True+allAbout :: Expr -> [Expr] -> Bool+e `allAbout` es = atomicConstants e `areAll` (`elem` es)++about :: Expr -> [Expr] -> Bool+e `about` es = atomicConstants e `areAny` (`elem` es)++notAbout :: Expr -> [Expr] -> Bool+notAbout = not .: about++timeout :: Args -> Bool -> Bool+timeout Args{evalTimeout = Nothing} = id+timeout Args{evalTimeout = Just t} = timeoutToFalse t++-- needs lexicompareBy+compareExpr :: Args -> Expr -> Expr -> Ordering+compareExpr args = compareComplexityThen (lexicompareBy cmp)+ 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++-- | A special 'Expr' value.+-- When provided on the 'constants' list, +-- makes all the following constants 'foreground' constants.+foreground :: Expr+foreground = constant "foreground" (undefined :: Args)++-- | A special 'Expr' value.+-- When provided on the 'constants' list,+-- makes all the following constants 'background' constants.+-- Background constants can appear in laws about other constants, but not by+-- themselves.+background :: Expr+background = constant "background" (undefined :: Args)+-- NOTE: Hack! TODO: add reason why++-- for cmdArgs+prepareArgs :: Args -> Mode Args+prepareArgs args =+ mode "speculate" args "" (flagArg (\s a -> Right a {extra = s:extra a}) "")+ [ "ssize" --= \s a -> a {maxSize = read s}+ , "ttests" --= \s a -> a {maxTests = read s}+ , "mmin-tests" --= \s a -> a {minTests = parseMinTests s}+ , "zsemisize" --= \s a -> a {maxSemiSize = read s}+ , "xcondsize" --= \s a -> a {maxCondSize = read s}+ , "Aconstants" --. \a -> a {showConstants = False} -- TODO: fix name+ , "Ohide-args" --. \a -> a {showArgs = False}+ , "Ttheory" --. \a -> a {showTheory = True}+ , "Eno-equations" --. \a -> a {showEquations = False}+ , "Sno-semiequations" --. \a -> a {showSemiequations = False}+ , "Cno-sideconditions" --. \a -> a {showConditions = False}+ , "0no-constant-laws" --. \a -> a {showConstantLaws = True}+ , "rclass-reps-for" --= \s a -> a {showClassesFor = read s `L.insert` showClassesFor a}+ , "vvars" --= \s a -> a {maxVars = read s}+ , "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}+ , "gsemi-digraph" --. \a -> a {showDot = True+ ,quietDot = False+ ,showConstants = False+ ,showEquations = False+ ,showSemiequations = False+ ,showConditions = False+ ,showArgs = False}+ , "Dquiet-dot" --. \a -> a {showDot = True+ ,quietDot = True+ ,showConstants = False+ ,showEquations = False+ ,showSemiequations = False+ ,showConditions = False+ ,showArgs = False}+ , " only-types" --= \s a -> a {onlyTypes = onlyTypes a ++ splitAtCommas s}+ , "fforce" --. \a -> a {force = True}+ , "hhelp" --. \a -> a {showHelp = True}+ , " exclude" --= \s a -> a {exclude = exclude a ++ splitAtCommas s}+ , "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 ""+ 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
@@ -0,0 +1,138 @@+module Test.Speculate.CondReason where++import Test.Speculate.Expr+import Test.Speculate.Reason+import qualified Test.Speculate.Utils.Digraph as D+import Test.Speculate.Utils.Digraph (Digraph)+import Data.Maybe (mapMaybe,maybeToList,fromMaybe)+import Data.List (lookup)+import Data.Functor ((<$>)) -- for GHC < 7.10+import qualified Data.List as L+import Test.Speculate.Utils++-- Chy = Conditional Thy = Conditional Theory+data Chy = Chy+ { cequations :: [(Expr,Expr,Expr)]+ , cimplications :: Digraph Expr+ , cclasses :: [(Expr,[Expr])]+ , unThy :: Thy+ }++emptyChy = Chy+ { cequations = []+ , cimplications = D.empty+ , cclasses = []+ , unThy = emptyThy+ }++updateCEquationsBy :: ([(Expr,Expr,Expr)] -> [(Expr,Expr,Expr)]) -> Chy -> Chy+updateCEquationsBy f chy@Chy{cequations = ceqs} = chy{cequations = f ceqs}++listImplied :: Chy -> Expr -> [Expr]+listImplied Chy{cimplications = ccss} ce = D.succs ce ccss++listImplies :: Chy -> Expr -> [Expr]+listImplies Chy{cimplications = ccss} ce = D.preds ce ccss++listEquivalent :: Chy -> Expr -> [Expr]+listEquivalent Chy{cclasses = ccss} ce = fromMaybe [] $ lookup ce ccss++reduceRootWith :: Binds -> Expr -> (Expr,Expr) -> Maybe Expr+reduceRootWith bs e (e1,e2) = (e2 `assigning`) <$> matchWith bs e e1++reductions1With :: Binds -> Expr -> (Expr,Expr) -> [Expr]+reductions1With bs e (l,_) | lengthE l > lengthE e = [] -- optional optimization+reductions1With bs e@(e1 :$ e2) r = maybeToList (reduceRootWith bs e r)+ ++ map (:$ e2) (reductions1With bs e1 r)+ ++ map (e1 :$) (reductions1With bs e2 r)+reductions1With bs e r = maybeToList (reduceRootWith bs e r)++creductions1 :: Expr -> Expr -> (Expr,Expr,Expr) -> [Expr]+creductions1 ce e (ceq,el,er) =+ case ce `match` ceq of+ Nothing -> []+ Just bs -> reductions1With bs e (el,er)++-- normalize is maybe a misnomer. not necessarily convergent.+cnormalize :: Chy -> Expr -> Expr -> Expr+cnormalize chy@Chy{cequations = ceqs, unThy = thy} ce = n+ where+ n e = case filter (canReduceTo thy e)+ $ concatMap (creductions1 ce e) ceqs+ ++ concatMap (\ce' -> concatMap (creductions1 ce' e) ceqs) (listEquivalent chy ce)+ ++ concatMap (\ce' -> concatMap (creductions1 ce' e) ceqs) (listImplied chy ce)+ ++ concatMap (\ce' -> concatMap (creductions1 ce' e) ceqs) (concatMap (listEquivalent chy) (listImplied chy ce)) of+ [] -> e -- already normalized+ (e':_) -> n $ normalize thy e'+-- TODO: fix silly code structure in cnormalize!++cequivalent :: Chy -> Expr -> Expr -> Expr -> Bool+cequivalent chy ce e1 e2 =+ equivalent (unThy chy) (cnormalize chy ce e1) (cnormalize chy ce e2)++cIsInstanceOf :: Chy -> (Expr,Expr,Expr) -> (Expr,Expr,Expr) -> Bool+cIsInstanceOf chy (ce2,le2,re2) (ce1,le1,re1) =+ case match2 (le2,re2) (le1,re1) of+ Nothing -> False+ Just bs -> equivalent (unThy chy) (ce1 `assigning` bs) ce2++-- TODO: make cinsert result independent of insertion order+cinsert :: (Expr,Expr,Expr) -> Chy -> Chy+cinsert ceq@(ce,e1,e2) chy@Chy{cequations = eqs}+ | cequivalent chy ce e1 e2 = chy+ | otherwise = cdelete $ chy {cequations = eqs ++ [ceq]}++cfilter :: ((Expr,Expr,Expr) -> Bool) -> Chy -> Chy+cfilter p = updateCEquationsBy (filter p)++cdiscard :: ((Expr,Expr,Expr) -> Bool) -> Chy -> Chy+cdiscard p = cfilter (not . p)++cdelete :: Chy -> Chy+cdelete chy = updateCEquationsBy upd chy+ where+ upd = discardLater (cIsInstanceOf chy)+ . discardByOthers (\(ce,e1,e2) eqs -> cequivalent chy{cequations = eqs} ce e1 e2)++cfinalize :: Chy -> Chy+cfinalize chy@Chy{cequations = ceqs} =+ updateCEquationsBy (concatMap expandSmallerConditions) chy+ where+ expandSmallerConditions ceq@(ce,e1,e2) =+ (ce,e1,e2) : [ (ce',cnormalize chy' ce' e1,cnormalize chy' ce' e2)+ | ce' <- listImplies chy ce+ , lengthE ce' < lengthE ce+ , ce' /= falseE+ , let chy' = chy{cequations = L.delete ceq ceqs}+ , not $ cequivalent chy' ce' e1 e2+ ]++canonicalizeCEqn :: (Expr -> Expr -> Ordering) -> (Expr,Expr,Expr) -> (Expr,Expr,Expr)+canonicalizeCEqn cmp = canonicalizeCEqnWith cmp preludeInstances++canonicalizeCEqnWith :: (Expr -> Expr -> Ordering) -> Instances -> (Expr,Expr,Expr) -> (Expr,Expr,Expr)+canonicalizeCEqnWith cmp ti = c . o+ where+ c (ce,e1,e2) = case canonicalizeWith ti (e2 :$ (e1 :$ ce)) of+ (e2' :$ (e1' :$ ce')) -> (ce',e1',e2')+ _ -> error $ "canonicalizeCEqnWith: the impossible happened,"+ ++ "this is definitely a bug, see source!"+ o (ce,e1,e2) | e1 `cmp` e2 == LT = (ce,e2,e1)+ | otherwise = (ce,e1,e2)++canonicalCEqnBy :: (Expr -> Expr -> Ordering) -> Instances -> (Expr,Expr,Expr) -> Bool+canonicalCEqnBy cmp ti ceqn = canonicalizeCEqnWith cmp ti ceqn == ceqn++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))+ . filter shouldShow+ . cequations+ . cfinalize
+ src/Test/Speculate/Engine.hs view
@@ -0,0 +1,234 @@+module Test.Speculate.Engine+ ( vassignments+ , expansions+ , mostGeneral+ , mostSpecific++ , theoryAndRepresentativesFromAtoms+ , theoryFromAtoms+ , equivalencesBetween++ , consider+ , distinctFromSchemas+ , classesFromSchemas++ , semiTheoryFromThyAndReps++ , conditionalTheoryFromThyAndReps+ , conditionalEquivalences+ , subConsequence++ , psortBy++ , module Test.Speculate.Expr+ )+where++import Data.Dynamic+import Data.Maybe+import Data.List hiding (insert)+import Data.Function (on)+import Data.Monoid ((<>))++import Test.Speculate.Utils+import Test.Speculate.Expr+import Test.Speculate.Reason+import Test.Speculate.CondReason+import Test.Speculate.SemiReason+import Test.Speculate.Utils.Class (Class)+import qualified Test.Speculate.Utils.Class as C+import qualified Test.Speculate.Utils.Digraph as D++------------------------------+-- * Manipulating expressions++-- | List all relevant variable assignments in an expresssion.+-- In pseudo-Haskell:+--+-- > vassignments (0 + x) == [0 + x]+-- > vassignments (0 + 0) == [0 + 0]+-- > vassignments (0 + _) == [0 + x]+-- > vassignments (_ + _) == [x + x, x + y]+-- > vassignments (_ + (_ + ord _)) == [x + (x + ord c), x + (y + ord c)]+--+-- You should not use this on expression with already assinged variables+-- (undefined, but currently defined behavior):+--+-- > vassignments (ii -+- i_) == [ii -+- ii]+vassignments :: Expr -> [Expr]+vassignments e =+ [ foldl fill e [ [ Var (defNames !! i) t | i <- is ]+ | (t,is) <- fs ]+ | fs <- productsList [[(t,is) | is <- iss 0 c] | (t,c) <- counts (holes e)] ]+ -- > fss _ + _ = [ [(Int,[0,0])], [(Int,[0,1])] ]+ -- > fss _ + (_ + ord _) = [ [(Int,[0,0]),(Char,[1])]+ -- > , [(Int,[0,1]),(Char,[1])] ]+-- TODO: rename vassignments, silly name. what about canonicalExpansions?++vassignmentsEqn :: (Expr,Expr) -> [(Expr,Expr)]+vassignmentsEqn = filter (uncurry (/=)) . map unEquation . vassignments . uncurry phonyEquation++expansions :: Instances -> Int -> Expr -> [Expr]+expansions ti n e =+ [ foldl fill e [ [ Var (names ti t !! i) t | i <- is ]+ | (t,is) <- fs ]+ | fs <- productsList [[(t,is) | is <- foo c n] | (t,c) <- counts (holes e)] ]+ where+ foo :: Int -> Int -> [[Int]]+ foo 0 nVars = [[]]+ foo nPos nVars = [i:is | i <- [0..(nVars-1)], is <- foo (nPos-1) nVars]+-- TODO: test expansions, put foo together with iss++-- | List the most general assignment of holes in an expression+mostGeneral :: Expr -> Expr+mostGeneral = head . vassignments -- TODO: make this efficient++-- | List the most specific assignment of holes in an expression+mostSpecific :: Expr -> Expr+mostSpecific = last . vassignments -- TODO: make this efficient++rehole :: Expr -> Expr+rehole (e1 :$ e2) = rehole e1 :$ rehole e2+rehole (Var _ t) = Var "" t+rehole e = e++----------------------------+-- * Enumerating expressions++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 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+ where+ fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes]++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)+ where+ dsThy = (complete *** id) $ foldl (flip $ consider (===)) (iniThy,[]) ds+ iniThy = emptyThy { keepE = keepUpToLength sz+ , closureLimit = 2+ , canReduceTo = dwoBy (\e1 e2 -> e1 `cmp` e2 == GT)+ , compareE = cmp+ }++-- 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)+ | otherwise =+ ( append thy $ equivalencesBetween (===) s s ++ eqs+ , ss ++ [s | not $ any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs])+ where+ eqs = concatMap (equivalencesBetween (===) s) $ filter (s ===) ss++distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr]+distinctFromSchemas ti nt nv thy = map C.rep . classesFromSchemas ti nt nv thy++classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr]+classesFromSchemas ti nt nv thy = C.mergesThat (equal ti nt)+ . C.mergesOn (normalizeE thy)+ . concatMap (classesFromSchema ti thy nv)+-- the "mergesThat (equal ...)" above is necesary because "equivalent thy"+-- won't detect all equivalences. here we test the few remaining+-- there shouldn't be that much overhead++classesFromSchema :: Instances -> Thy -> Int -> Expr -> [Class Expr]+classesFromSchema ti thy n = C.mergesOn (normalizeE thy)+ . map C.fromRep+ . expansions ti n++-- Return relevant equivalences between holed expressions:+--+-- > equivalencesBetween basicInstances 500 (_ + _) (_ + _) =+-- > [i + j == j + i]+equivalencesBetween :: (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr,Expr)]+equivalencesBetween (===) e1 e2 = discardLater (isInstanceOf `on` uncurry phonyEquation)+ . filter (uncurry (===))+ $ vassignmentsEqn (e1,e2)++semiTheoryFromThyAndReps :: Instances -> Int -> Int+ -> Thy -> [Expr] -> Shy+semiTheoryFromThyAndReps ti nt nv thy =+ stheorize thy+ . pairsThat (\e1 e2 -> e1 /= e2+ && typ e1 == typ e2+ && lessOrEqual ti nt e1 e2)+ . distinctFromSchemas ti nt nv thy+ . filter (isOrdE ti)++conditionalTheoryFromThyAndReps :: Instances+ -> (Expr -> Expr -> Ordering)+ -> Int -> Int -> Int+ -> Thy -> [Expr] -> Chy+conditionalTheoryFromThyAndReps ti cmp nt nv csz thy es' =+ conditionalEquivalences+ cmp+ (canonicalCEqnBy cmp ti)+ (condEqual ti nt)+ (lessOrEqual ti nt)+ csz thy clpres cles+ where+ (cles,clpres) = (id *** filter (\(e,_) -> lengthE e <= csz))+ . partition (\(e,_) -> typ e /= boolTy)+ . filter (isEqE ti . fst)+ $ classesFromSchemas ti nt nv thy es'++conditionalEquivalences :: (Expr -> Expr -> Ordering)+ -> ((Expr,Expr,Expr) -> Bool)+ -> (Expr -> Expr -> Expr -> Bool)+ -> (Expr -> Expr -> Bool)+ -> Int -> Thy -> [Class Expr] -> [Class Expr] -> Chy+conditionalEquivalences cmp canon cequal (==>) csz thy clpres cles =+ cdiscard (\(ce,e1,e2) -> subConsequence thy clpres ce e1 e2)+ . foldl (flip cinsert) (Chy [] cdg clpres thy)+ . sortBy (\(c1,e11,e12) (c2,e21,e22) -> c1 `cmp` c2+ <> ((e11 `phonyEquation` e12) `cmp` (e21 `phonyEquation` e22)))+ . discard (\(pre,e1,e2) -> pre == falseE+ || length (vars pre \\ (vars e1 +++ vars e2)) > 0+ || subConsequence thy [] pre e1 e2)+ . filter canon+ $ [ (ce, e1, e2)+ | e1 <- es, e2 <- es, e1 /= e2, canon (falseE,e1,e2)+ , typ e1 == typ e2, typ e1 /= boolTy+ , ce <- explain e1 e2+ ]+ where+ (es,pres) = (map C.rep cles, map C.rep clpres)+ explain e1 e2 = D.narrow (\ep -> cequal ep e1 e2) cdg+ cdg = D.fromEdges+ . pairsThat (==>)+ $ filter (\e -> typ e == boolTy && not (isAssignment e)) pres++-- | Is the equation a consequence of substitution?+-- > subConsequence (x == y) (x + y) (x + x) == True+-- > subConsequence (x <= y) (x + y) (x + x) == False -- not sub+-- > subConsequence (abs x == abs y) (abs x) (abs y) == True+-- > subConsequence (abs x == 1) (x + abs x) (20) == False (artificial)+subConsequence :: Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool+subConsequence thy clpres ((Constant "==" _ :$ ea) :$ eb) e1 e2+ -- NOTE: the first 4 are uneeded, but make it a bit faster...+ | ea `isSub` e1 && equivalent thy{closureLimit=1} (sub ea eb e1) e2 = True+ | eb `isSub` e1 && equivalent thy{closureLimit=1} (sub eb ea e1) e2 = True+ | ea `isSub` e2 && equivalent thy{closureLimit=1} (sub ea eb e2) e1 = True+ | eb `isSub` e2 && equivalent thy{closureLimit=1} (sub eb ea e2) e1 = True+ | equivalent ((ea,eb) `insert` thy){closureLimit=1} e1 e2 = True+subConsequence thy clpres ce e1 e2 = or+ [ subConsequence thy clpres ce' e1 e2+ | (rce,ces) <- clpres, ce == rce, ce' <- ces ]++psortBy :: (a -> a -> Bool) -> [a] -> [(a,a)]+psortBy (<) xs = [(x,y) | x <- xs, y <- xs, x < y, none (\z -> x < z && z < y) xs]+ where+ none = (not .) . any
+ src/Test/Speculate/Expr.hs view
@@ -0,0 +1,16 @@+module Test.Speculate.Expr+ ( module Test.Speculate.Expr.Core+ , module Test.Speculate.Expr.Ground+ , module Test.Speculate.Expr.Match+ , module Test.Speculate.Expr.TypeInfo+ , module Test.Speculate.Expr.Equate+ , module Test.Speculate.Expr.Canon+ )+where++import Test.Speculate.Expr.Core+import Test.Speculate.Expr.Ground+import Test.Speculate.Expr.Match+import Test.Speculate.Expr.TypeInfo+import Test.Speculate.Expr.Equate+import Test.Speculate.Expr.Canon
+ src/Test/Speculate/Expr/Canon.hs view
@@ -0,0 +1,35 @@+module Test.Speculate.Expr.Canon+ ( canonicalize+ , canonicalizeWith+ , canonicalWith+ )+where++import Test.Speculate.Expr.Core+import Test.Speculate.Expr.Match+import Test.Speculate.Expr.TypeInfo+import Data.List ((\\))++-- | Canonicalize variable names in an expression.+--+-- > canonicalize (x + y) = (x + y)+-- > canonicalize (y + x) = (x + y)+-- > canonicalize (y + (z + x)) = (x + (y + z))+-- > canonicalize ((w + z) + (z + x)) = ((x + y) + (y + z))+-- > canonicalize (y + abs y) = (x + abs x)+-- > canonicalize ((y + x) == (x + y)) = ((x + y) == (y + x))+canonicalizeWith :: Instances -> Expr -> Expr+canonicalizeWith ti e = e `assigning` ((\(t,n,n') -> (n,Var n' t)) `map` cr [] e)+ where+ cr :: [(TypeRep,String,String)] -> Expr -> [(TypeRep,String,String)]+ cr bs (e1 :$ e2) = cr (cr bs e1) e2+ cr bs (Var n t)+ | any (\(t',n',_) -> t == t' && n == n') bs = bs+ | otherwise = (t,n,head $ names ti t \\ map (\(_,_,n) -> n) bs):bs+ cr bs _ = bs++canonicalize :: Expr -> Expr+canonicalize = canonicalizeWith preludeInstances++canonicalWith :: Instances -> Expr -> Bool+canonicalWith ti e = canonicalizeWith ti e == e
+ src/Test/Speculate/Expr/Core.hs view
@@ -0,0 +1,416 @@+module Test.Speculate.Expr.Core+ ( Expr (..)+ -- * Smart constructors+ , constant+ , showConstant+ , var+ , hole+ , holeOfTy+ , ($$)++ -- * Smart destructors+ , evaluate+ , eval+ , typ+ , etyp ++ -- * Queries+ , typeCorrect+ , arity+ , holes+ , vars+ , consts+ , atomicConstants+ , subexprs+ , subexprsV+ , isSub+ , hasVar+ , unfoldApp+ , isConstantNamed++ -- * Properties of expressions+ , lengthE+ , depthE+ , countVar+ , countVars+ , unrepeatedVars+ , isAssignment+ , lexicompare+ , lexicompareBy+ , compareComplexity+ , compareComplexityThen++ -- * Useful expressions+ , falseE++ -- * Showing+ , showExpr+ , showPrecExpr+ , showsPrecExpr+ , showOpExpr+ , showsOpExpr+ , eqExprCommuting+ )+where++import Data.List (intercalate, find)+import Data.Maybe (fromMaybe, isJust, catMaybes)+import Data.Function (on)+import Data.Monoid ((<>))++import Data.Dynamic+import Test.LeanCheck+import Test.Speculate.Utils+++-- | An encoded Haskell functional-application expression for use by Speculate.+data Expr = Constant String Dynamic+ | Var String TypeRep+ | Expr :$ Expr++-- | Encode a constant Haskell expression for use by Speculate.+-- It takes a string representation of a value and a value, returning an+-- 'Expr'. Examples:+--+-- > constant "0" 0+-- > constant "'a'" 'a'+-- > constant "True" True+-- > constant "id" (id :: Int -> Int)+-- > constant "(+)" ((+) :: Int -> Int -> Int)+-- > constant "sort" (sort :: [Bool] -> [Bool])+constant :: Typeable a => String -> a -> Expr+constant s x = Constant s (toDyn x)++-- | A shorthand for 'constant' to be used on values that are 'Show' instances.+-- Examples:+--+-- > showConstant 0 = constant "0" 0+-- > showConstant 'a' = constant "'a'" 'a' +-- > showConstant True = constant "True" True+showConstant :: (Typeable a, Show a) => a -> Expr+showConstant x = constant (show x) x++-- | @var "x" (undefined :: Ty)@ returns a variable of type 'Ty' named "x"+var :: (Listable a, Typeable a) => String -> a -> Expr+var s a = Var s (typeOf a)++-- | __(intended for advanced users)__+--+-- @hole (undefined :: Ty)@ returns a hole of type 'Ty'+--+-- By convention, a Hole is a variable named with the empty string.+hole :: (Listable a, Typeable a) => a -> Expr+hole = holeOfTy . typeOf++holeOfTy :: TypeRep -> Expr+holeOfTy = Var ""++-- | 'Just' an 'Expr' application if the types match,+-- 'Nothing' otherwise.+($$) :: Expr -> Expr -> Maybe Expr+e1 $$ e2 =+ case typ e1 `funResultTy` typ e2 of+ Nothing -> Nothing+ Just _ -> Just $ e1 :$ e2+++-- Deprecated smart constructors:++++-- quick and dirty show instance+instance Show Expr where+ showsPrec d e = showParen (d > 10)+ $ showsPrecExpr 0 e+ . showString " :: "+ . shows (typ e)+ . showString (showHoles e)+ where+ showHoles e = case holes e of+ [] -> ""+ hs -> " (holes: " ++ intercalate ", " (map show hs) ++ ")"++showsPrecExpr :: Int -> Expr -> String -> String+showsPrecExpr d (Constant s _) | atomic s && isInfixedPrefix s = showString $ toPrefix s+showsPrecExpr d (Constant s _) = showParen sp $ showString s+ where sp = if atomic s then isInfix s else maybe True (d >) $ outernmostPrec s+showsPrecExpr d (Var "" _) = showString "_" -- a hole+showsPrecExpr d (Var s _) = showParen (isInfix s) $ showString s+showsPrecExpr d ((Constant ":" _ :$ e1) :$ e2) =+ case showsPrecExpr 0 e2 "" of+ "[]" -> showString "[" . showsPrecExpr 0 e1 . showString "]"+ '[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs+ cs -> showParen (d > prec ":")+ $ showsOpExpr ":" e1 . showString ":" . showsOpExpr ":" e2+showsPrecExpr d ((Constant f _ :$ e1) :$ e2)+ | isInfix f = showParen (d > prec f)+ $ showsOpExpr f e1+ . showString " " . showString f . showString " "+ . showsOpExpr f e2+ | otherwise = showParen (d > prec " ")+ $ showString f+ . showString " " . showsOpExpr " " e1+ . showString " " . showsOpExpr " " e2+showsPrecExpr d (Constant f _ :$ e1)+ | isInfix f = showParen True+ $ showsOpExpr f e1 . showString " " . showString f+showsPrecExpr d (e1 :$ e2) = showParen (d > prec " ")+ $ showsPrecExpr (prec " ") e1+ . showString " "+ . showsPrecExpr (prec " " + 1) e2++showsOpExpr :: String -> Expr -> String -> String+showsOpExpr op = showsPrecExpr (prec op + 1)++showOpExpr :: String -> Expr -> String+showOpExpr op = showPrecExpr (prec op + 1)++showPrecExpr :: Int -> Expr -> String+showPrecExpr n e = showsPrecExpr n e ""++showExpr :: Expr -> String+showExpr = showPrecExpr 0++-- Does not evaluate values when comparing, but rather their representation as+-- strings and their types.+instance Eq Expr where (==) = eqExprCommuting []++eqExprCommuting :: [Expr] -> Expr -> Expr -> Bool+eqExprCommuting ces = e+ where+ e (Var s1 t1) (Var s2 t2) = t1 == t2 && s1 == s2+ e (Constant s1 d1) (Constant s2 d2) = dynTypeRep d1 == dynTypeRep d2 && s1 == s2+ e ((ef1 :$ ex1) :$ ey1) ((ef2 :$ ex2) :$ ey2)+ | ef1 == ef2 && ef1 `elem` ces = eqExprCommuting ces ex1 ex2 && eqExprCommuting ces ey1 ey2+ || eqExprCommuting ces ex1 ey2 && eqExprCommuting ces ey1 ex2+ e (ef1 :$ ex1) (ef2 :$ ex2) = ef1 == ef2 && ex1 == ex2+ e _ _ = False++instance Ord Expr where+ compare = compareComplexity+++lexicompareBy :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering+lexicompareBy compareConstants = cmp+ where+ c1@(Constant _ _) `cmp` c2@(Constant _ _) = c1 `compareConstants` c2+ e1 `cmp` e2 | typ e1 /= typ e2 = typ e1 `compareTy` typ e2+ Var s1 _ `cmp` Var s2 _ = s1 `compare` s2+ (f :$ x) `cmp` (g :$ y) = f `cmp` g `thn` x `cmp` y+ (_ :$ _) `cmp` _ = GT+ _ `cmp` (_ :$ _) = LT+ _ `cmp` Var _ _ = GT+ Var _ _ `cmp` _ = LT+ -- Var < Constants < Apps++compareTy :: TypeRep -> TypeRep -> Ordering+compareTy = (compare `on` tyArity) <> compare++lexicompareConstants :: Expr -> Expr -> Ordering+lexicompareConstants = cmp+ where+ e1 `cmp` e2 | typ e1 /= typ e2 = typ e1 `compareTy` typ e2+ Constant s1 _ `cmp` Constant s2 _ = s1 `compare` s2+ _ `cmp` _ = error "lexicompareConstants can only compare constants"++-- | Compare two expressiosn lexicographically+--+-- 1st their type arity;+-- 2nd their type;+-- 3rd var < constants < apps+-- 4th lexicographic order on names+lexicompare :: Expr -> Expr -> Ordering+lexicompare = lexicompareBy lexicompareConstants++-- | Compares two expressions first by their complexity:+-- 1st length;+-- 2nd number of variables (more variables is less complex);+-- 3nd sum of number of variable occurrences;+-- 4th their depth;+-- 5th normal `compare`.+compareComplexityThen :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering+compareComplexityThen cmp = (compare `on` lengthE)+ <> (flip compare `on` length . vars)+ <> (flip compare `on` length . repVars)+ <> (compare `on` length . consts)+ <> cmp++-- | Compares two expressions first by their complexity:+-- 1st length;+-- 2nd number of variables (more variables is less complex);+-- 3nd sum of number of variable occurrences;+-- 4th their depth;+-- 5th lexicompare.+compareComplexity :: Expr -> Expr -> Ordering+compareComplexity = compareComplexityThen lexicompare++falseE :: Expr+falseE = showConstant False++-- | 'Just' the value of an expression when possible (correct type, no holes),+-- 'Nothing' otherwise.+evaluate :: Typeable a => Expr -> Maybe a+evaluate e = v e >>= fromDynamic+ where+ v :: Expr -> Maybe Dynamic+ v (Var _ _) = Nothing+ v (Constant _ x) = Just x+ v (e1 :$ e2) = do v1 <- v e1+ v2 <- v e2+ dynApply v1 v2++-- | Evaluates an expression when possible (correct type, no holes).+-- Returns a default value otherwise.+eval :: Typeable a => a -> Expr -> a+eval x e = fromMaybe x (evaluate e)++-- | The type of an expression. This raises errors, but those should not+-- happen if expressions are smart-constructed.+typ :: Expr -> TypeRep+typ (Constant _ d) = dynTypeRep d+typ (Var _ t) = t+typ (e1 :$ e2) = resultTy (typ e1) -- this silently ignores type mismatches, was:+{-+ case typ e1 `funResultTy` typ e2 of+ Nothing -> error $ "type mismatch, cannot apply "+ ++ show (typ e1) ++ " to " ++ show (typ e2)+ Just t -> t+-}++-- | etyp returns either:+-- the Right type+-- a Left expression with holes with the structure of the I'll typed expression+etyp :: Expr -> Either Expr TypeRep+etyp (e1 :$ e2) =+ case (et1,et2) of+ (Right t1, Right t2) ->+ case t1 `funResultTy` t2 of+ Just t -> Right t+ Nothing -> Left e+ _ -> Left e+ where+ et1 = etyp e1+ et2 = etyp e2+ ettoe et = case et of Right t -> Var "" t+ Left e -> e+ e = ettoe et1 :$ ettoe et2+etyp e = Right (typ e)+-- on error, what's left is an ill typed expression made up entirely of holes+-- this could be a good workaround, but let's think more: cause it is really workaroundish++typeCorrect :: Expr -> Bool+typeCorrect (e1 :$ e2) = typeCorrect e1+ && typeCorrect e2+ && isJust (typ e1 `funResultTy` typ e2)+typeCorrect _ = True++-- | Type arity of an 'Expr'+arity :: Expr -> Int+arity = tyArity . typ++-- | List types holes (unamed variables) in an expression+holes :: Expr -> [TypeRep]+holes (e1 :$ e2) = holes e1 ++ holes e2+holes (Var "" t) = [t]+holes _ = []++-- | List all variables in an expression.+vars :: Expr -> [(TypeRep,String)]+vars (e1 :$ e2) = vars e1 +++ vars e2+vars (Var s t) = [(t,s)]+vars _ = []++atomicConstants :: Expr -> [Expr]+atomicConstants (e1 :$ e2) = atomicConstants e1 +++ atomicConstants e2+atomicConstants e@(Constant _ _) = [e]+atomicConstants _ = []++hasVar :: Expr -> Bool+hasVar (e1 :$ e2) = hasVar e1 || hasVar e2+hasVar (Var s t) = True+hasVar _ = False++-- | List all variables in an expression, in order, with repetitions+repVars :: Expr -> [(TypeRep,String)]+repVars (e1 :$ e2) = repVars e1 ++ repVars e2+repVars (Var s t) = [(t,s)]+repVars _ = []++-- | List terminal constants in an expression. This does not repeat values.+consts :: Expr -> [Expr]+consts (e1 :$ e2) = consts e1 +++ consts e2+consts e@(Constant _ _) = [e]+consts _ = []+++-- | Returns the length of an expression. In term rewriting terms: |s|+lengthE :: Expr -> Int+lengthE (e1 :$ e2) = lengthE e1 + lengthE e2+lengthE _ = 1++-- | Returns the maximum depth of an expression.+depthE :: Expr -> Int+depthE e@(_:$_) = 1 + maximum (map depthE $ unfoldApp e)+depthE _ = 1++-- | Number of occurrences of a given variable name.+-- In term rewriting terms: |s|_x+countVar :: TypeRep -> String -> Expr -> Int+countVar t n (e1 :$ e2) = countVar t n e1 + countVar t n e2+countVar t n (Var n' t') | t == t' && n == n' = 1+countVar _ _ _ = 0++countVars :: Expr -> [(TypeRep,String,Int)]+countVars e = map (\(t,n) -> (t,n,countVar t n e)) $ vars e++unrepeatedVars :: Expr -> Bool+unrepeatedVars = all (\(_,_,n) -> n == 1) . countVars++-- Is this espression an assignment of a variable to a value?+isAssignment :: Expr -> Bool+isAssignment ((Constant "==" _ :$ Var _ _) :$ e2) = True+isAssignment ((Constant "==" _ :$ e1) :$ Var _ _) = True+isAssignment _ = False++-- | Non-variable sub-expressions of an expression+--+-- This includes the expression itself+subexprs :: Expr -> [Expr]+subexprs e@(e1 :$ e2) = [e] +++ subexprs e1 +++ subexprs e2+subexprs e@(Constant _ _) = [e]+subexprs _ = []++-- | Sub-expressions of an expression+-- including variables and the expression itself.+subexprsV :: Expr -> [Expr]+subexprsV e@(e1 :$ e2) = [e] +++ subexprsV e1 +++ subexprsV e2+subexprsV e = [e]++isConstant :: Expr -> Bool+isConstant (Constant _ _) = True+isConstant _ = False++-- | Is a subexpression of.+isSub :: Expr -> Expr -> Bool+isSub e e0 | e == e0 = True+isSub e (e1 :$ e2) = isSub e e1 || isSub e e2+isSub e e0 = e == e0++-- | Make substitutions on subexpressions, variables have to match exactly!+sub :: Expr -> Expr -> Expr -> Expr+sub ef et = s+ where+ s e | e == ef = et+ s (e1 :$ e2) = s e1 :$ s e2+ s e = e++isConstantNamed :: Expr -> String -> Bool+Constant n' _ `isConstantNamed` n = n' == n+_ `isConstantNamed` _ = False++-- | Unfold function application:+--+-- > (((f :$ e1) :$ e2) :$ e3) = [f,e1,e2,e3]+unfoldApp :: Expr -> [Expr]+unfoldApp (ef :$ ex) = unfoldApp ef ++ [ex]+unfoldApp ef = [ef]
+ src/Test/Speculate/Expr/Equate.hs view
@@ -0,0 +1,119 @@+-- | This module exports+-- smart constructors,+-- smart destructors+-- and queries over+-- equations,+-- inequations+-- and conditional equations.+module Test.Speculate.Expr.Equate+ ( equation, unEquation, isEquation, uselessEquation, usefulEquation+ , phonyEquation++ , comparisonLT, comparisonLE, unComparison++ , implication, unImplication, usefulImplication++ , conditionalEquation, unConditionalEquation, usefulConditionalEquation+ , conditionalComparisonLT, conditionalComparisonLE, unConditionalComparison+ )+where++import Test.LeanCheck ((==>))+import Data.List ((\\))+import Test.Speculate.Utils+import Test.Speculate.Expr.Core+import Test.Speculate.Expr.TypeInfo++equation :: Instances -> Expr -> Expr -> Maybe Expr+equation ti e1 e2 = do+ e <- eqE ti (typ e1)+ e :$ e1 $$ e2++phonyEquation :: Expr -> Expr -> Expr+phonyEquation e1 e2 | typ e1 /= typ e2 = error $ "phonyEquation: type mismatch "+ ++ show (typ e1) ++ ", "+ ++ show (typ e2)+phonyEquation e1 e2 = Var "==" (mkEqnTy $ typ e1) :$ e1 :$ e2++unEquation :: Expr -> (Expr,Expr)+unEquation ((Constant "==" _ :$ e1) :$ e2) = (e1,e2)+unEquation ((Var "==" _ :$ e1) :$ e2) = (e1,e2)+unEquation _ = error "unEquation: not an equation!"++isEquation :: Expr -> Bool+isEquation ((Constant "==" _ :$ e1) :$ e2) = True+isEquation ((Var "==" _ :$ e1) :$ e2) = True+isEquation _ = False++-- | Given an equation encoded as an 'Expr'.+-- Checks if both sides of an equation are the same.+-- If the 'Expr' is not an equation, this raises an error.+uselessEquation :: Expr -> Bool+uselessEquation = uncurry (==) . unEquation++usefulEquation :: Expr -> Bool+usefulEquation = uncurry (/=) . unEquation++comparisonLT :: Instances -> Expr -> Expr -> Maybe Expr+comparisonLT ti e1 e2 = do+ e <- ltE ti (typ e1)+ e :$ e1 $$ e2++comparisonLE :: Instances -> Expr -> Expr -> Maybe Expr+comparisonLE ti e1 e2 = do+ e <- leE ti (typ e1)+ e :$ e1 $$ e2++unComparison :: Expr -> (Expr,Expr)+unComparison ((Constant "compare" _ :$ e1) :$ e2) = (e1,e2)+unComparison ((Constant "<" _ :$ e1) :$ e2) = (e1,e2)+unComparison ((Constant "<=" _ :$ e1) :$ e2) = (e1,e2)+unComparison ((Constant ">" _ :$ e1) :$ e2) = (e1,e2)+unComparison ((Constant ">=" _ :$ e1) :$ e2) = (e1,e2)+unComparison _ = error "unComparisonL: not a compare/(<)/(<=)/(>)/(>=) application"++implication :: Expr -> Expr -> Maybe Expr+implication e1 e2+ | typ e1 == boolTy = implicationE :$ e1 $$ e2+ | otherwise = Nothing+ where+ implicationE = constant "==>" (==>)++unImplication :: Expr -> (Expr,Expr)+unImplication ((Constant "==>" _ :$ e1) :$ e2) = (e1,e2)+unImplication _ = error "unImplication: not an implication"++usefulImplication :: Expr -> Bool+usefulImplication e = vp \\ ve /= vp+ where+ (pre,e') = unImplication e+ vp = vars pre+ ve = vars e'++conditionalEquation :: Instances -> Expr -> Expr -> Expr -> Maybe Expr+conditionalEquation ti pre e1 e2 = (pre `implication`) =<< equation ti e1 e2++unConditionalEquation :: Expr -> (Expr,Expr,Expr)+unConditionalEquation ((Constant "==>" _ :$ pre) :$ ((Constant "==" _ :$ e1) :$ e2)) = (pre,e1,e2)+unConditionalEquation _ = error "unConditionalEquation: not an equation with side condition"++-- an equation with a side condition is useful when sides of the equation are different+-- and at least one variable is shared between the side condition and the equation+usefulConditionalEquation :: Expr -> Bool+usefulConditionalEquation e = e1 /= e2 && vp \\ ve /= vp+ where+ (pre,e1,e2) = unConditionalEquation e+ vp = vars pre+ ve = vars e1 +++ vars e2++conditionalComparisonLE :: Instances -> Expr -> Expr -> Expr -> Maybe Expr+conditionalComparisonLE ti pre e1 e2 = (pre `implication`) =<< comparisonLE ti e1 e2++conditionalComparisonLT :: Instances -> Expr -> Expr -> Expr -> Maybe Expr+conditionalComparisonLT ti pre e1 e2 = (pre `implication`) =<< comparisonLT ti e1 e2++unConditionalComparison :: Expr -> (Expr,Expr,Expr)+unConditionalComparison e = (econd,e1,e2)+ where+ (e1,e2) = unComparison ecmp+ (econd,ecmp) = unImplication e
+ src/Test/Speculate/Expr/Ground.hs view
@@ -0,0 +1,111 @@+module Test.Speculate.Expr.Ground+ ( grounds+ , groundBinds+ , groundAndBinds+ , equal+ , lessOrEqual+ , less+ , inequal+ , true+ , false+ , condEqual+ , condEqualM+ , trueBinds+ , trueRatio+ )+where++import Test.Speculate.Expr.Core+import Test.Speculate.Expr.Match+import Test.Speculate.Expr.TypeInfo+import Test.Speculate.Expr.Equate+import Test.LeanCheck+import Data.Ratio+import Data.Functor ((<$>)) -- for GHC < 7.10+import Data.Maybe (fromMaybe)++-- TODO: move vassignments / etc here++-- | List all possible valuations of an expression (potentially infinite).+-- In pseudo-Haskell:+--+-- > take 3 $ grounds preludeInstances ((x + x) + y)+-- > == [(0 + 0) + 0, (0 + 0) + 1, (1 + 1) + 0]+grounds :: Instances -> Expr -> [Expr]+grounds ti e = (e `assigning`) <$> groundBinds ti e++-- | List all possible variable bindings to an expression+--+-- > take 3 $ groundBinds preludeInstances ((x + x) + y)+-- > == [ [("x",0),("y",0)]+-- > , [("x",0),("y",1)]+-- > , [("x",1),("y",0)] ]+groundBinds :: Instances -> Expr -> [Binds]+groundBinds ti e =+ concat $ products [mapT ((,) n) (tiersE ti t) | (t,n) <- vars e]++-- | List all possible variable bindings and valuations to an expression+--+-- > groundAndBinds ti e == zipWith (,) (grounds ti e) (groundBinds ti e)+groundAndBinds :: Instances -> Expr -> [(Binds,Expr)]+groundAndBinds ti e = (\bs -> (bs, e `assigning` bs)) <$> groundBinds ti e++-- | Are two expressions equal for a given number of tests?+equal :: Instances -> Int -> Expr -> Expr -> Bool+-- equal ti _ e1 e2 | e1 == e2 = isComparable ti e1 -- optional optimization+equal ti n e1 e2 = maybe False (true ti n) (equation ti e1 e2)+-- TODO: discover why the optimization above changes the output+-- 1. $ make eg/list && ./eg/list -ES -r0 -s4 > without+-- 2. uncomment above+-- 3. $ make eg/list && ./eg/list -ES -r0 -s4 > with+-- 4. diff -rud without with+-- 5. see that there are less equivalence classes now!++-- | Are two expressions equal+-- under a given condition+-- for a given number of tests?+condEqual :: Instances -> Int -> Expr -> Expr -> Expr -> Bool+condEqual ti n pre e1 e2 = maybe False (true ti n) (conditionalEquation ti pre e1 e2)++-- | Are two expressions equal+-- under a given condition+-- for a given number of tests+-- and a minimum amount of tests+condEqualM :: Instances -> Int -> Int -> Expr -> Expr -> Expr -> Bool+condEqualM ti n n0 pre e1 e2 = condEqual ti n pre e1 e2 && length cs >= n0+ where+ cs = fromMaybe []+ $ filter (eval False) . map condition . take n . grounds ti+ <$> conditionalEquation ti pre e1 e2+ condition ceq = let (ce,_,_) = unConditionalEquation ceq in ce++-- | Are two expressions less-than-or-equal for a given number of tests?+lessOrEqual :: Instances -> Int -> Expr -> Expr -> Bool+lessOrEqual ti n e1 e2 = maybe False (true ti n) (comparisonLE ti e1 e2)++-- | Are two expressions less-than for a given number of tests?+less :: Instances -> Int -> Expr -> Expr -> Bool+less ti n e1 e2 = maybe False (true ti n) (comparisonLT ti e1 e2)++-- | Are two expressions inequal for *all* variable assignments?+-- Note this is different than @not . equal@.+inequal :: Instances -> Int -> Expr -> Expr -> Bool+inequal ti n e1 e2 = maybe False (false ti n) (equation ti e1 e2)++-- | Is a boolean expression true for all variable assignments?+true :: Instances -> Int -> Expr -> Bool+true ti n e = all (eval False) . take n $ grounds ti e++-- | List variable bindings for which an expression holds true.+trueBinds :: Instances -> Int -> Expr -> [Binds]+trueBinds ti n e = [bs | (bs,e) <- take n $ groundAndBinds ti e, eval False e]++-- | Under a maximum number of tests,+-- returns the ratio for which an expression holds true.+trueRatio :: Instances -> Int -> Expr -> Ratio Int+trueRatio ti n e = length (trueBinds ti n e) % length (take n $ groundAndBinds ti e)++-- | Is an expression ALWAYS false?+-- This is *NOT* the same as not true+false :: Instances -> Int -> Expr -> Bool+false ti n e = all (not . eval False) . take n $ grounds ti e
+ src/Test/Speculate/Expr/Match.hs view
@@ -0,0 +1,191 @@+module Test.Speculate.Expr.Match+ ( Binds+ -- * Assigning+ , fill+ , assign+ , assigning+ , sub+ , renameBy++ -- * Matching+ , match+ , match2+ , matchWith+ , unify+ , unification+ , isInstanceOf+ , hasInstanceOf+ , isCanonInstanceOf+ , hasCanonInstanceOf+ )+where++import Test.Speculate.Expr.Core++import Data.Typeable+import Data.List (find)+import Data.Maybe (isJust,fromMaybe)+import Data.Functor ((<$>))+import Test.Speculate.Utils+import Control.Monad ((>=>))++type Binds = [(String,Expr)]++findB :: String -> TypeRep -> Binds -> Maybe Expr+findB n t bs = snd <$> find (\(n',e) -> n' == n && typ e == t) bs++updateAssignments :: String -> Expr -> Binds -> Maybe Binds+updateAssignments s e = \bs ->+ case findB s (typ e) bs of+ Nothing -> Just ((s,e):bs)+ Just e' -> if e' == e+ then Just bs+ else Nothing++-- | Fill holes in an expression.+-- Silently skips holes that are not of the right type.+-- Silently discard remaining expressions.+fill :: Expr -> [Expr] -> Expr+fill e = fst . fill' e+ where+ fill' :: Expr -> [Expr] -> (Expr,[Expr])+ fill' (e1 :$ e2) es = let (e1',es') = fill' e1 es+ (e2',es'') = fill' e2 es'+ in (e1' :$ e2', es'')+ fill' (Var "" t) (e:es) | t == typ e = (e,es)+ fill' e es = (e,es)++-- | Assign all occurences of a variable in an expression.+--+-- Examples in pseudo-Haskell:+--+-- > assign "x" (10) (x + y) = (10 + y)+-- > assign "y" (y + z) ((x + y) + (y + z)) = (x + (y + z)) + ((y + z) + z)+--+-- This respects the type (won't change occurrences of a similarly named+-- variable of a different type).+assign :: String -> Expr -> Expr -> Expr+assign n e (e1 :$ e2) = assign n e e1 :$ assign n e e2+assign n e (Var n' t) | t == typ e && n == n' = e+assign n e e1 = e1++-- | Assign all occurrences of several variables in an expression.+--+-- For single variables, this works as assign:+--+-- > x + y `assigning` [("x",10)] = (10 + y)+-- > ((x + y) + (y + z)) `assigning` [("y",y+z)] = (x + (y + z)) + ((y + z) + z)+--+-- Note this is /not/ equivalent to @foldr (uncurry assign)@. Variables inside+-- expressions being assigned will not be assigned.+assigning :: Expr -> Binds -> Expr+(e1 :$ e2) `assigning` as = (e1 `assigning` as) :$ (e2 `assigning` as)+(Var n t) `assigning` as = fromMaybe (Var n t) $ findB n t as+e `assigning` _ = e++-- | Substitute matching subexpressios.+--+-- sub (x + y) 0 ((x + y) + z) == (0 + z)+-- sub (x + y) 0 (x + (y + z)) == (x + (y + z))+sub :: Expr -> Expr -> Expr -> Expr+sub ef et = s+ where+ s e | e == ef = et+ s (e1 :$ e2) = s e1 :$ s e2+ s e = e++-- | Primeify variable names in an expression.+--+-- > renameBy (++ "'") (x + y) = (x' + y')+-- > renameBy (++ "'") (y + (z + x)) = (y' + (z' + x'))+-- > renameBy (++ "1") abs x = abs x1+-- > renameBy (++ "2") abs (x + y) = abs (x2 + y2)+--+-- Note this will affect holes!+renameBy :: (String -> String) -> Expr -> Expr+renameBy f (e1 :$ e2) = renameBy f e1 :$ renameBy f e2+renameBy f (Var n t) = Var (f n) t+renameBy f e = e++-- | List matches if possible+--+-- > 0 + 1 `match` x + y = Just [x=0, y=1]+-- > 0 + (1 + 2) `match` x + y = Just [x=0, y=1 + 2]+-- > 0 + (1 + 2) `match` x + (y + y) = Nothing+-- > (x + x) + (1 + 2) `match` x + (y + y) = Nothing+match :: Expr -> Expr -> Maybe Binds+match = matchWith []++-- | List matches of pairs of expressions if possible+--+-- > (0,1) `match2` (x,y) = Just [x=0, y=1]+-- > (0,1+2) `match2` (x,y+y) = Nothing+match2 :: (Expr,Expr) -> (Expr,Expr) -> Maybe Binds+match2 (e1,e2) (e3,e4) =+ case matchWith [] e1 e3 of+ Nothing -> Nothing+ Just bs -> matchWith bs e2 e4++-- | List matches with preexisting bindings:+--+-- > 0 + 1 `matchWith [(x,0)]` x + y = Just [x=0, y=1]+-- > 0 + 1 `matchWith [(x,1)]` x + y = Nothing+matchWith :: Binds -> Expr -> Expr -> Maybe Binds+matchWith bs e1' e2' = m e1' e2' bs+ where+ m :: Expr -> Expr -> Binds -> Maybe Binds+ m e1 e2 | typ e1 /= typ e2 = const Nothing+ m e1 (Var s t) = updateAssignments s e1+ m (f1 :$ x1) (f2 :$ x2) = m f1 f2 >=> m x1 x2+ m e1 e2 | e1 == e2 = Just+ | otherwise = const Nothing++unify :: Expr -> Expr -> Maybe Expr+unify e1 e2 = (e1' `assigning`) <$> unification e1' e2'+ where+ e1' = renameBy (++ "1") e1+ e2' = renameBy (++ "2") e2++-- NOTE: Take care of passing disjoing variable namespaces on both expressions!+-- see unify for an example of that.+unification :: Expr -> Expr -> Maybe Binds+unification e1' e2' = u e1' e2' []+ where+ u :: Expr -> Expr -> Binds -> Maybe Binds+ u e1 e2 | typ e1 /= typ e2 = const Nothing+ u e1@(Var s1 t1) e2@(Var s2 t2) = updateAssignments s1 e2 >=> updateAssignments s2 e1+ u e1 (Var s t) = updateAssignments s e1+ u (Var s t) e2 = updateAssignments s e2+ u (f1 :$ x1) (f2 :$ x2) = u f1 f2 >=> u x1 x2+ u e1 e2 | e1 == e2 = Just+ | otherwise = const Nothing++-- 0 `isInstanceOf` x = True+-- y `isInstanceOf` x = True+-- x `isInstanceOf` 0 = False+-- 1 `isInstanceOf` 0 = False+-- x + (y + x) `isInstanceOf` x + y = True+-- y + (y + x) `isInstanceOf` x + y = True+-- 0 + (y + x) `isInstanceOf` x + y = True+-- x `isInstanceOf` x = True+-- _ `isInstanceOf` x = True+isInstanceOf :: Expr -> Expr -> Bool+e1 `isInstanceOf` e2 = isJust $ e1 `match` e2++hasInstanceOf :: Expr -> Expr -> Bool+e1 `hasInstanceOf` e2 | e1 `isInstanceOf` e2 = True+(e1f :$ e1x) `hasInstanceOf` e2 | e1f `hasInstanceOf` e2 ||+ e1x `hasInstanceOf` e2 = True+_ `hasInstanceOf` _ = False++isCanonInstanceOf :: Expr -> Expr -> Bool+e1 `isCanonInstanceOf` e2 =+ case e1 `match` e2 of+ Nothing -> False+ Just xs -> strictlyOrderedOn snd (sortOn fst xs)++hasCanonInstanceOf :: Expr -> Expr -> Bool+e1 `hasCanonInstanceOf` e2 | e1 `isCanonInstanceOf` e2 = True+(e1f :$ e1x) `hasCanonInstanceOf` e2 | e1f `hasCanonInstanceOf` e2 ||+ e1x `hasCanonInstanceOf` e2 = True+_ `hasCanonInstanceOf` _ = False
+ src/Test/Speculate/Expr/TypeInfo.hs view
@@ -0,0 +1,243 @@+module Test.Speculate.Expr.TypeInfo+ ( Instances+ , Instance (..)+ , TypeRep++ -- * Smart constructors+ , ins+ , eq, eqWith+ , ord, ordWith+ , eqOrd+ , listable, listableWith++ -- * Queries on Instances+ , instanceType+ , findInfo+ , names+ , eqE, isEq, isEqE+ , leE, ltE, isOrd, isOrdE+ , isEqOrd, isEqOrdE+ , tiersE, isListable++ -- * Type info for standard Haskell types+ , preludeInstances++ -- * Does not belong here?+ , defNames++ , boolTy+ , mkEqnTy+ )+where++import Test.Speculate.Expr.Core+import Test.Speculate.Expr.Match+import Test.Speculate.Utils hiding (ord)+import Test.LeanCheck+import Test.LeanCheck.Utils hiding (comparison)+import Test.LeanCheck.Error (errorToFalse)+import Data.Dynamic++import Data.Maybe (isJust,fromMaybe,listToMaybe,catMaybes,mapMaybe)+import Data.List (find,(\\))+++-- | Type information needed to Speculate expressions (single type / single class).+data Instance = Eq TypeRep Expr+ | Ord TypeRep Expr Expr+ | Listable TypeRep [[Expr]]+ | Names TypeRep [String]++-- | Type information needed to Speculate expressions.+type Instances = [Instance]++instanceType :: Instance -> TypeRep+instanceType (Eq t _) = t+instanceType (Ord t _ _) = t+instanceType (Listable t _) = t+instanceType (Names t _) = t++-- | Usage: @ins1 "x" (undefined :: Type)@+ins1 :: (Typeable a, Listable a, Show a, Eq a, Ord a)+ => String -> a -> Instances+ins1 n x = eq x ++ ord x ++ listable x ++ name n x++ins :: (Typeable a, Listable a, Show a, Eq a, Ord a)+ => String -> a -> Instances+ins n x = concat+ [ x / n++ , [x] / n ++ "s"+ , [[x]] / n ++ "ss"+--, [[[x]]] / n ++ "ss"++ , (x,x) / n ++ m+ , (x,x,x) / n ++ m ++ o+--, (x,x,x,x) / n ++ m ++ o ++ p++ , [(x,x)] / n ++ m ++ "s"+--, [(x,x,x)] / n ++ m ++ o ++ "ss"++--, (x,[x]) / n ++ m ++ "s"+--, ([x],x) / n ++ "s" ++ m+--, ([x],[x]) / n ++ "s" ++ m ++ "s"+--, (x,(x,x)) / n ++ m ++ o+--, ((x,x),x) / n ++ m ++ o++ , mayb x / "m" ++ n ++ "1"+--, eith x x / "e" ++ n ++ o ++ "1"+ ]+ where+ (/) :: (Typeable a, Listable a, Show a, Eq a, Ord a)+ => a -> String -> Instances -- monomorphism restriction strikes again+ (/) = flip ins1+ infixr 0 /+ m = namesFromTemplate n !! 1+ o = namesFromTemplate m !! 1+ p = namesFromTemplate o !! 1+-- NOTE: the function typeInfoN is not perfect: it won't help produce types+-- combining different sub-types, like for example: (Bool,Int). But it is+-- way better than the original version in which I had to explictly define+-- everything. A definitive solution is still to be thought of.+-- NOTE: see related TODO on the definition of basicInstances++eq :: (Typeable a, Eq a) => a -> Instances+eq x = eqWith $ (==) -:> x++ord :: (Typeable a, Ord a) => a -> Instances+ord x = ordWith $ (<=) -:> x++eqOrd :: (Typeable a, Eq a, Ord a) => a -> Instances+eqOrd x = eq x ++ ord x++listable :: (Typeable a, Show a, Listable a) => a -> Instances+listable x = listableWith $ tiers `asTypeOf` [[x]]++name :: Typeable a => String -> a -> Instances+name n x = [Names (typeOf x) (namesFromTemplate n)]++eqWith :: (Typeable a, Eq a) => (a -> a -> Bool) -> Instances+eqWith (==) = [Eq (typeOf $ arg (==)) $ constant "==" $ errorToFalse .: (==)]+ where+ arg :: (a -> b) -> a+ arg _ = undefined++ordWith :: (Typeable a, Ord a) => (a -> a -> Bool) -> Instances+ordWith (<=) = [Ord (typeOf $ arg (<=))+ (constant "<=" (errorToFalse .: (<=)))+ (constant "<" ((errorToFalse . not) .: flip (<=)))]+ where+ arg :: (a -> b) -> a+ arg _ = undefined++listableWith :: (Typeable a, Show a) => [[a]] -> Instances+listableWith xss =+ [Listable (typeOf $ head $ head xss) (mapT showConstant xss)]++isEq :: Instances -> TypeRep -> Bool+isEq ti = isJust . eqE ti++isOrd :: Instances -> TypeRep -> Bool+isOrd ti = isJust . ltE ti++isEqOrd :: Instances -> TypeRep -> Bool+isEqOrd ti t = isOrd ti t && isEq ti t++isEqE :: Instances -> Expr -> Bool+isEqE ti = isEq ti . typ++isOrdE :: Instances -> Expr -> Bool+isOrdE ti = isOrd ti . typ++isEqOrdE :: Instances -> Expr -> Bool+isEqOrdE ti = isEqOrd ti . typ++isListable :: Instances -> TypeRep -> Bool+isListable ti t = isJust $ findInfo m ti+ where+ m (Listable t' ts) | t' == t = Just ts+ m _ = Nothing++-- TODO: implement above using something similar to the following+-- isComparable ti = isJust . (`findInfo` ti) . typ++findInfo :: (Instance -> Maybe a) -> Instances -> Maybe a+findInfo may = listToMaybe . mapMaybe may++findInfoOr :: a -> (Instance -> Maybe a) -> Instances -> a+findInfoOr def may = fromMaybe def . findInfo may++names :: Instances -> TypeRep -> [String]+names ti t = findInfoOr defNames m ti+ where+ m (Names t' ns) | t == t' = Just ns+ m _ = Nothing++tiersE :: Instances -> TypeRep -> [[Expr]]+tiersE ti t = findInfoOr (error $ "could not find Listable " ++ show t) m ti+ where+ m (Listable t' ts) | t == t' = Just ts+ m _ = Nothing++eqE :: Instances -> TypeRep -> Maybe Expr+eqE ti t = findInfo m ti+ where+ m (Eq t' eq) | t == t' = Just eq+ m _ = Nothing++ltE :: Instances -> TypeRep -> Maybe Expr+ltE ti t = findInfo m ti+ where+ m (Ord t' _ lt) | t == t' = Just lt+ m _ = Nothing++leE :: Instances -> TypeRep -> Maybe Expr+leE ti t = findInfo m ti+ where+ m (Ord t' le _) | t == t' = Just le+ m _ = Nothing++-- TODO: include *ALL* prelude types on basicInstances+preludeInstances :: Instances+preludeInstances = concat+ [ ins1 "x" (undefined :: ())+ , ins1 "xs" (undefined :: [()])++ , ins "p" (undefined :: Bool)++ , ins "x" (undefined :: Int)+--, ins "x" (undefined :: Word)+ , ins "x" (undefined :: Integer)++ , ins "o" (undefined :: Ordering)+ , ins "c" (undefined :: Char)++ , ins "q" (undefined :: Rational)+ , ins "f" (undefined :: Float)+ , ins "f" (undefined :: Double)++-- TODO: uncomment the following and investigate why compilation takes so long+--, ins "x" (undefined :: Int1)+--, ins "x" (undefined :: Int2)+--, ins "x" (undefined :: Int3)+--, ins "x" (undefined :: Int4)+--, ins "x" (undefined :: Word1)+ , ins "x" (undefined :: Word2)+--, ins "x" (undefined :: Word3)+--, ins "x" (undefined :: Word4)+--, ins "x" (undefined :: Nat1)+--, ins "x" (undefined :: Nat2)+--, ins "x" (undefined :: Nat3)+--, ins "x" (undefined :: Nat4)+--, ins "x" (undefined :: Nat5)+--, ins "x" (undefined :: Nat6)+--, ins "x" (undefined :: Nat7)+ ]+-- WHOA! Have I discovered a "bug" in GHC? adding to many type compositions+-- on ins and types on preludeInstances makes compilation of this module+-- *really* slow: it takes a whopping 2 minutes!+-- (the above report is using -O2, I have not tested without optimizations).+++defNames :: [String]+defNames = namesFromTemplate "x"
+ src/Test/Speculate/Misc.hs view
@@ -0,0 +1,120 @@+-- | Miscellaneous functions I still did not find a reasonable place to put+-- them in.+module Test.Speculate.Misc+ ( functions1+ , functions2+ , functions3+ , functions4+ , fillings++ , expressionsOf+ , valuedExpressionsOf+ )+where++import Test.Speculate+import Test.Speculate.Expr+import Test.Speculate.Utils+import Data.Dynamic+import Test.LeanCheck++functions1 :: (Typeable a, Typeable b) => Expr -> [(Expr,a->b)]+functions1 e =+ case l undefined of+ [] -> []+ _ -> fist l+ where+ l = \x -> [(e',v) | e' <- fillings e [constant "x" x], let Just v = evaluate e']++functions2 :: (Typeable a, Typeable b, Typeable c) => Expr -> [(Expr,a->b->c)]+functions2 e =+ case l undefined undefined of+ [] -> []+ _ -> fist2 l+ where+ l = \x y -> [(e',v) | e' <- fillings e [constant "x" x, constant "y" y]+ , let Just v = evaluate e']++functions3 :: (Typeable a, Typeable b, Typeable c, Typeable d)+ => Expr -> [(Expr,a->b->c->d)]+functions3 e =+ case l undefined undefined undefined of+ [] -> []+ _ -> fist3 l+ where+ l = \x y z -> [(e',v) | e' <- fillings e [constant "x" x, constant "y" y, constant "z" z]+ , let Just v = evaluate e']++functions4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e)+ => Expr -> [(Expr,a->b->c->d->e)]+functions4 e =+ case l undefined undefined undefined undefined of+ [] -> []+ _ -> fist4 l+ where+ l = \x y z w -> [(e',v) | e' <- fillings e [constant "x" x, constant "y" y, constant "z" z, constant "w" w]+ , let Just v = evaluate e']+++-- This function is dangerous:+--+-- @f@ should always return the same number of values+-- and should not evaluateuate it's argument when producing the list spine+--+-- fist (function-list), in lack of a better name+fist :: (a->[(z,b)]) -> [(z,a->b)]+fist f = [ (fst $ f' undefined, snd . f')+ | i <- [0..(length (f undefined)-1)]+ , let f' = (!! i) . f ]++fist2 :: (a->b->[(z,c)]) -> [(z,a->b->c)]+fist2 f = map (id *** curry) $ fist (uncurry f)++fist3 :: (a->b->c->[(z,d)]) -> [(z,a->b->c->d)]+fist3 f = map (id *** curry3) $ fist (uncurry3 f)++fist4 :: (a->b->c->d->[(z,e)]) -> [(z,a->b->c->d->e)]+fist4 f = map (id *** curry4) $ fist (uncurry4 f)++-- All possible fillings of holes in an expression:+-- +-- * For an expression without holes, this returns a singleton list with that+-- expression.+--+-- * If there is no type match between the given filler-expressions,+-- return an empty list.+fillings :: Expr -> [Expr] -> [Expr]+fillings e vs = [fill e f | f <- fs]+ where+ fs = productsList [[v | v <- vs, typ v == h] | h <- holes e]++-- | Given a list of atomic expressions, enumerate experssions by application+--+-- NOTE: for now, very inneficient+--+-- This function exists solely for documentation and will never actually be+-- useful, as:+--+-- > mapT fst $ classes+--+-- Will return as expressions that are semantially different (and is more+-- efficient)+--+-- Eventually this function will be removed from Speculate+expressionsOf :: [Expr] -> [[Expr]]+expressionsOf ds = [ds] \/ productMaybeWith ($$) es es `addWeight` 1+ where+ es = expressionsOf ds++-- | Given a list of atomic expressinos, enumerated expressions of a given type+-- by application.+--+-- Never will be actually useful, see 'expressionsOf'.+--+-- Eventually this functino will be removed from Speculate+valuedExpressionsOf :: Typeable a => [Expr] -> [[(Expr,a)]]+valuedExpressionsOf = mapTMaybe exprValue . expressionsOf+ where+ exprValue :: Typeable a => Expr -> Maybe (Expr,a)+ exprValue e = (,) e `fmap` evaluate e+
+ src/Test/Speculate/Reason.hs view
@@ -0,0 +1,480 @@+module Test.Speculate.Reason+ ( Thy (..)+ , emptyThy+ , normalize+ , normalizeE+ , isNormal+ , complete+ , equivalent+ , equivalentInstance+ , insert+ , showThy+ , printThy+ , keepUpToLength+ , keepMaxOf+ , (|==|)+ , theorize+ , theorizeBy+ , prettyThy+ , criticalPairs+ , normalizedCriticalPairs+ , append+ , difference++ , okThy+ , canonicalEqn+ , canonicalRule+ , canonicalizeEqn+ , deduce+ , simplify+ , delete+ , orient+ , compose+ , collapse+ , updateRulesBy+ , updateEquationsBy+ , discardRedundantEquations+ , finalize+ , initialize+ , defaultKeep++ , reductions1+ , reductionsO++ , dwoBy+ , (|>)+ )+where++import Test.Speculate.Expr+import Test.Speculate.Reason.Order+import Test.Speculate.Utils+import Data.Either+import Data.Tuple (swap)+import Data.List (partition, (\\), sortBy, sort)+import Data.Function (on)+import Data.Monoid ((<>))+import Data.Functor ((<$>)) -- for GHC < 7.10+import qualified Data.List as L (insert)+import Data.Maybe (fromJust,isJust,listToMaybe,maybeToList,mapMaybe)+import Control.Monad++type Rule = (Expr,Expr)+type Equation = (Expr,Expr)++data Thy = Thy+ { rules :: [Rule]+ , equations :: [Equation]+ , canReduceTo :: Expr -> Expr -> Bool -- ^ should be compatible with compareE+ , compareE :: Expr -> Expr -> Ordering -- ^ total order used to "sort" equations+ , closureLimit :: Int+ , keepE :: Expr -> Bool+ }++compareEqn :: Thy -> Equation -> Equation -> Ordering+compareEqn thy@Thy {compareE = cmp} (e1l,e1r) (e2l,e2r) =+ e1l `cmp` e2l <> e1r `cmp` e2r++-- data invariant+okThy :: Thy -> Bool+okThy thy@Thy {rules = rs, equations = eqs, canReduceTo = (->-), keepE = keep, compareE = cmp} =+ orderedBy (<) rs+ && orderedBy (<) eqs+ && all (uncurry (->-)) rs+ && all ((/= LT) . uncurry cmp) eqs+ && all (uncurry ((==) `on` typ)) (rs++eqs)+ && all (canonicalEqn thy) eqs+ && all canonicalRule rs+-- && canonicalizeThy thy == thy -- (uneeded, follows from above)+ && all keepEqn (rs++eqs)+ where+ e1 < e2 = compareEqn thy e1 e2 == LT+ keepEqn (e1,e2) = keep e1 && keep e2++updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy+updateRulesBy f thy@Thy {rules = rs} = thy {rules = f rs}++updateEquationsBy :: ([Equation] -> [Equation]) -> Thy -> Thy+updateEquationsBy f thy@Thy {equations = es} = thy {equations = f es}++mapRules :: (Rule -> Rule) -> Thy -> Thy+mapRules = updateRulesBy . map++mapEquations :: (Equation -> Equation) -> Thy -> Thy+mapEquations = updateEquationsBy . map++-- | This instance is as efficient as it gets, but, this function will not+-- detect equality when rules and equations are in a different order (or+-- repeated). See '|==|'.+instance Eq Thy where+ t == u = rules t == rules u+ && equations t == equations u+ && closureLimit t == closureLimit u -- useful when self-speculating++(|==|) :: Thy -> Thy -> Bool+(|==|) t u = rules t =|= rules u+ && map orient (equations t) =|= map orient (equations u)+ where+ xs =|= ys = nubSort xs == nubSort ys+ orient (e1,e2) | e1 < e2 = (e2,e1)+ | otherwise = (e1,e2)+infix 4 |==|++emptyThy :: Thy+emptyThy = Thy+ { rules = []+ , equations = []+ , canReduceTo = (|>)+ , compareE = compare+ , closureLimit = 0+ , keepE = const True+ }++ruleFilter :: Thy -> [Rule] -> [Rule]+ruleFilter Thy {keepE = keep} = filter keepR+ where+ keepR (e1,e2) = keep e1 && keep e2++keepUpToLength :: Int -> Expr -> Bool+keepUpToLength limit e = lengthE e <= limit++keepMaxOf :: [Equation] -> Expr -> Bool+keepMaxOf = keepUpToLength . (+1) . maximum . (0:) . map lengthE . catPairs++normalize :: Thy -> Expr -> Expr+normalize Thy {rules = rs} = n+ where+ n e = case concatMap (e `reductions1`) rs of+ [] -> e -- already normalized+ (e':_) -> n e'++-- normalize by rules and equations+normalizeE :: Thy -> Expr -> Expr+normalizeE Thy {rules = rs, equations = eqs, canReduceTo = (->-) } = n+ where+ n e = case concatMap (e `reductions1`) rs+ ++ filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of+ [] -> e -- already normalized+ (e':_) -> n e'++isNormal :: Thy -> Expr -> Bool+isNormal thy e = normalizeE thy e == e++reduceRoot :: Expr -> Rule -> Maybe Expr+reduceRoot e (e1,e2) = (e2 `assigning`) <$> (e `match` e1)++-- Lists all reductions by one rule, note that reductions may be repeated.+-- For unrepeated reductions see reductionsO+reductions1 :: Expr -> Rule -> [Expr]+reductions1 e (l,_) | lengthE l > lengthE e = [] -- optional optimization+reductions1 e@(e1 :$ e2) r = maybeToList (e `reduceRoot` r)+ ++ map (:$ e2) (reductions1 e1 r)+ ++ map (e1 :$) (reductions1 e2 r)+reductions1 e r = maybeToList (e `reduceRoot` r)++-- Lists all reductions by one rule without repetitions.+-- For a faster version that allows repetitions, see reductions1+reductionsO :: Expr -> Rule -> [Expr]+reductionsO e (l,_) | lengthE l > lengthE e = [] -- optional optimization+reductionsO e@(e1 :$ e2) r = maybeToList (e `reduceRoot` r)+ +++ map (:$ e2) (reductionsO e1 r)+ +++ map (e1 :$) (reductionsO e2 r)+reductionsO e r = maybeToList (e `reduceRoot` r)++-- as defined by Martin & Nipkow in "Ordered Rewriting and Confluence" on 1990+-- this definition is sound, but incomplete (some groundJoinable pairs won't be+-- detected).+groundJoinable :: Thy -> Expr -> Expr -> Bool+groundJoinable thy@Thy{equations = eqs} e1 e2 =+ e1 == e2+ || any (\(el,er) -> maybe2 False ((==) `on` sort) (e1 `match` el) (e2 `match` er)) (eqs ++ map swap eqs)+ || (f == g && and (zipWith (groundJoinable thy) xs ys))+ where+ (f:xs) = unfoldApp e1+ (g:ys) = unfoldApp e2+-- TODO: one case missing on groundJoinable+-- I need a function f, such that:+-- f (x) = [x]+-- f (xy) = [xx, xy, yx]+-- f (xyz) = [xxx, xxy, xyx, xyy, xyz, xzy, yxx, yxy, yyx, yzx, zxy, zyx]+-- f (xyzw) = [ xxxx, xxxy, xxyx, xxyy, xxyz, xxzy+-- , xyxx, xyxy, xyyx, xyyy, xyyz, xyzx, xyzy, xyzz, xyzw, xywz+-- , xzxy, xzyx, xzyy, xzyz, xzyw, xzzy, xzwx, xzwy,+-- , xwyz, ... ]++normalizedCriticalPairs :: Thy -> [(Expr,Expr)]+normalizedCriticalPairs thy = nubSortBy (compareEqn thy)+ . map (canonicalizeEqn thy)+ . discard (uncurry $ groundJoinable thy)+ . filter (uncurry (/=))+ . map (normalize thy *** normalize thy)+ $ criticalPairs thy++criticalPairs :: Thy -> [(Expr,Expr)]+criticalPairs thy@Thy {rules = rs, compareE = cmp} =+ nubMerges [r `criticalPairsWith` s | r <- rs, s <- rs]+ where+ criticalPairsWith :: Rule -> Rule -> [(Expr,Expr)]+ r1@(e1,_) `criticalPairsWith` r2@(e2,_) =+ nubSortBy (compareEqn thy)+ . map sortuple+ . filter (uncurry (/=))+ . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))+ . nubSortBy cmp+ $ overlaps e1 e2+ xs ** ys = [(x,y) | x <- xs, y <- ys]+ sortuple (x,y) | x < y = (y,x)+ | otherwise = (x,y)+ (<) :: Expr -> Expr -> Bool+ e1 < e2 = e1 `cmp` e2 == LT++-- Warning: will have to also be applied in reverse to get all overlaps.+--+-- canonicalization here is needed for the nub+overlaps :: Expr -> Expr -> [Expr]+overlaps e1 e2 = id -- nubSort+ . map (canonicalize . (e2' `assigning`))+ $ (e1' `unification`) `mapMaybe` subexprs e2'+ where+ e1' = renameBy (++ "1") e1+ e2' = renameBy (++ "2") e2++equivalent :: Thy -> Expr -> Expr -> Bool+equivalent thy e1 e2 = e1' == e2'+ || or [ normalizeE thy e1'' == normalizeE thy e2''+ | e1'' <- closure thy e1'+ , e2'' <- closure thy e2'+ ]+ where+ e1' = normalizeE thy e1+ e2' = normalizeE thy e2++equivalentInstance :: Thy -> Expr -> Expr -> Bool+equivalentInstance thy e1 e2 = e1' == e2'+ || or [ normalizeE thy e1'' `isInstanceOf` normalizeE thy e2''+ | e1'' <- closure thy e1'+ , e2'' <- closure thy e2'+ ]+ where+ e1' = normalizeE thy e1+ e2' = normalizeE thy e2++closure :: Thy -> Expr -> [Expr]+closure thy e = iterateUntilLimit (closureLimit thy) (==) step [normalizeE thy e]+ where+ eqs = equations thy+ step = nubMergeMap reductionsEqs1+ reductionsEqs1 e = e `L.insert` nubMergeMap (reductions1 e) (eqs ++ map swap eqs)++insert :: Equation -> Thy -> Thy+insert (e1,e2) thy+ | normalize thy e1 == normalize thy e2 = thy+ | otherwise = complete $ updateEquationsBy (canonicalizeEqn thy (e1,e2) `L.insert`) thy++append :: Thy -> [Equation] -> Thy+append thy eqs = updateEquationsBy (nubSort . (++ eqs')) thy+ where+ eqs' = map (canonicalizeEqn thy) $ filter (uncurry ((/=) `on` normalize thy)) eqs++difference :: Thy -> Thy -> Thy+difference thy1@Thy {equations = eqs1, rules = rs1}+ thy2@Thy {equations = eqs2, rules = rs2} =+ thy1 {equations = eqs1 \\ eqs2, rules = rs1 \\ rs2}++complete :: Thy -> Thy+complete = iterateUntil (==)+ $ deduce+ . collapse+ . compose+ . orient+ . deleteGroundJoinable+ . delete+ . simplify+-- TODO: (?) on complete, each step should also return a boolean indicating+-- whether the rule was applied succesfully. (low priority)++completeVerbose :: Thy -> IO Thy+completeVerbose thy0 = do+ let {thy1 = canonicalizeThy thy0}; unless (thy1 == thy0) $ pr "canonThy" thy1+ let {thy2 = deduce thy1}; unless (thy2 == thy1) $ pr "deduce" thy2+ let {thy3 = simplify thy2}; unless (thy3 == thy2) $ pr "simplify" thy3+ let {thy4 = delete thy3}; unless (thy4 == thy3) $ pr "delete" thy4+ let {thy5 = orient thy4}; unless (thy5 == thy4) $ pr "orient" thy5+ let {thy6 = compose thy5}; unless (thy6 == thy5) $ pr "compose" thy6+ let {thy7 = collapse thy6}; unless (thy7 == thy6) $ pr "collapse" thy7+ -- threadDelay $ 100 * 1000 -- 100 milisecond delay+ if thy7 /= thy0 then completeVerbose thy7+ else return thy7+ where+ pr n = (putStrLn (":: After " ++ n ++ ":") >>)+ . putStrLn . showThy+++deduce :: Thy -> Thy+deduce thy = updateEquationsBy (+++ ruleFilter thy (normalizedCriticalPairs thy)) thy++orient :: Thy -> Thy+orient thy@Thy {equations = eqs, rules = rs, canReduceTo = (>)} =+ thy {equations = eqs', rules = rs +++ nubSort (map canonicalizeRule rs')}+ where+ (eqs',rs') = partitionEithers . map o $ ruleFilter thy eqs+ o (e1,e2) | e1 > e2 = Right (e1,e2)+ | e2 > e1 = Right (e2,e1)+ | otherwise = Left (e1,e2)++delete :: Thy -> Thy+delete = updateEquationsBy $ discard (uncurry (==))++deleteEquivalent :: Thy -> Thy+deleteEquivalent thy =+ updateEquationsBy (discard (\(e1,e2) -> equivalent (updateEquationsBy (filter (/= (e1,e2))) thy{closureLimit=1}) e1 e2)) thy++deleteGroundJoinable :: Thy -> Thy+deleteGroundJoinable thy =+ updateEquationsBy (discard (\(e1,e2) -> groundJoinable (updateEquationsBy (filter (/= (e1,e2))) thy) e1 e2)) thy+-- TODO: make deleteGroundJoinable more efficient (it is *very* inneficient right now)++-- a.k.a. Simplify-identity+simplify :: Thy -> Thy+simplify thy = updateEquationsBy (nubSort . map (canonicalizeEqn thy))+ $ mapEquations (normalize thy *** normalize thy) thy++-- a.k.a. R-Simplify-rule+compose :: Thy -> Thy+compose thy = updateRulesBy (nubSort . map canonicalizeRule)+ $ mapRules (id *** normalize thy) thy++-- a.k.a. L-Simplify-rule+collapse :: Thy -> Thy+collapse thy@Thy {equations = eqs, rules = rs} =+ thy {equations = eqs +++ foldr (+++) [] (map collapse eqs'), rules = rs'}+ where+ (eqs',rs') = partition collapsable rs+ collapsable = not . null . collapse+ collapse :: Rule -> [Equation]+ collapse (e1,e2) = foldr (+++) []+ [ nubSort [ canonicalizeEqn thy (e,e2) | e <- reductions1 e1 (e1',e2') ]+ | (e1',e2') <- rs+ , (e1',e2') /= (e1,e2)+ , e1 =| e1' ]+ -- emcompasses or ">" or specialization ordering or duck beak+ (=|) :: Expr -> Expr -> Bool+ e1 =| e2 = e1 `hasInstanceOf` e2+ && not (e2 `hasInstanceOf` e1)++canonicalizeThy :: Thy -> Thy+canonicalizeThy = canonicalizeThyWith preludeInstances++canonicalizeThyWith :: Instances -> Thy -> Thy+canonicalizeThyWith ti thy = mapRules (canonicalizeRuleWith ti)+ . mapEquations (canonicalizeEqnWith thy ti)+ $ thy++canonicalizeEqn :: Thy -> Equation -> Equation+canonicalizeEqn thy = canonicalizeEqnWith thy preludeInstances++canonicalEqn :: Thy -> Equation -> Bool+canonicalEqn thy eq = canonicalizeEqn thy eq == eq++canonicalizeEqnWith :: Thy -> Instances -> Equation -> Equation+canonicalizeEqnWith thy ti = swap . canonicalizeRuleWith ti . swap . o+ where+ cmp = compareE thy+ o (e1,e2) | e1 `cmp` e2 == LT = (e2,e1)+ | otherwise = (e1,e2)+++canonicalizeRule :: Rule -> Rule+canonicalizeRule = canonicalizeRuleWith preludeInstances++canonicalRule :: Rule -> Bool+canonicalRule r = canonicalizeRule r == r++canonicalizeRuleWith :: Instances -> Rule -> Rule+canonicalizeRuleWith ti (e1,e2) =+ case canonicalizeWith ti (e1 :$ e2) of+ e1' :$ e2' -> (e1',e2')+ _ -> error $ "canonicalizeRuleWith: the impossible happened,"+ ++ "this is definitely a bug, see source!"++printThy :: Thy -> IO ()+printThy = putStrLn . showThy++showThy :: Thy -> String+showThy thy = (if null rs+ then "no rules.\n"+ else "rules:\n" ++ showEquations rs)+ ++ (if null eqs+ then ""+ else "equations:\n" ++ showEquations eqs)+ where+ thy' = canonicalizeThy thy+ rs = rules thy'+ eqs = equations thy'+ 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)+ . 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.+finalize :: Thy -> Thy+finalize = discardRedundantEquations++theorize :: [Equation] -> Thy+theorize = theorizeBy (canReduceTo emptyThy)++theorizeBy :: (Expr -> Expr -> Bool) -> [Equation] -> Thy+theorizeBy (>) = finalize+ . canonicalizeThy+ . complete+ . initialize 3 (>)++initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy+initialize n (>) eqs = thy+ where+ thy = emptyThy+ { equations = nubSort $ map (canonicalizeEqn thy) eqs+ , keepE = keepMaxOf eqs+ , canReduceTo = (>)+ , closureLimit = n+ }++defaultKeep :: Thy -> Thy+defaultKeep thy@Thy {equations = eqs, rules = rs} =+ thy { keepE = keepMaxOf (eqs++rs) }++discardRedundantEquations :: Thy -> Thy+discardRedundantEquations thy =+ updateEquationsBy discardRedundant thy+ where+ discardRedundant = d []+ . discardLater eqnInstanceOf+ . reverse+ . sortOn (uncurry (+) . (lengthE *** lengthE))+ (e1l,e1r) `eqnInstanceOf` (e0l,e0r) = e1l `hasCanonInstanceOf` e0l+ && e1r `hasCanonInstanceOf` e0r+ || e1l `hasCanonInstanceOf` e0r+ && e1r `hasCanonInstanceOf` e0l+ d ks [] = ks+ d ks ((e1,e2):eqs)+ | equivalent thy {equations = eqs} e1 e2 = d ks eqs+ | otherwise = d ((e1,e2):ks) eqs++discardRedundantRulesByEquations :: Thy -> Thy+discardRedundantRulesByEquations thy = updateRulesBy (d [] . reverse) thy+ where+ d ks [] = ks+ d ks ((e1,e2):rs)+ | equivalent thy {rules = ks++rs} e1 e2 = d ks rs+ | otherwise = d ((e1,e2):ks) rs
+ src/Test/Speculate/Reason/Order.hs view
@@ -0,0 +1,145 @@+module Test.Speculate.Reason.Order+ ( (|>|)+ , (>|)+ , (|>)+ , kboBy+ , dwoBy+ , weight+ , weightExcept+ , gtExcept+ )+where++import Test.Speculate.Expr+import Test.Speculate.Utils (nubMerge)++-- | Greater than or equal number of occurences of each variable+(>=\/) :: Expr -> Expr -> Bool+e1 >=\/ e2 = all (\(t,n) -> countVar t n e1 >= countVar t n e2)+ (vars e1 `nubMerge` vars e2)+++-- | Strict order between expressions as defined in TRAAT p103.+--+-- > s > t iff |s| > |t| and , for all x in V, |s|_x > |t|_x+--+-- This is perhaps the simplest order that can be used with KBC.+(|>|) :: Expr -> Expr -> Bool+e1 |>| e2 = lengthE e1 > lengthE e2+ && e1 >=\/ e2+infix 4 |>|+++-- | Strict order between expressions loosely as defined in TRAAT p124 (KBO)+--+-- Reversed K @>|@ for Knuth, sorry Bendix.+(>|) :: Expr -> Expr -> Bool+(>|) = kboBy weight (>)+infix 4 >|++kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool+kboBy w (->-) e1 e2 = e1 >=\/ e2+ && ( w e1 > w e2+ || w e1 == w e2 && ( e1 `fn` e2 -- f (f x) > x+ || e1 `fg` e2 -- f x > g y if f > g+ || e1 `ff` e2 -- f x y z > f x w v if y > w+ )+ )+ where+ ef :$ (eg :$ ex) `fn` ey@(Var _ _) | ef == eg = fn (eg :$ ex) ey+ ef@(Constant _ _) :$ ex@(Var _ _) `fn` ey@(Var _ _) | ex == ey = True+ _ `fn` _ = False+ e1 `fg` e2 =+ case (unfoldApp e1, unfoldApp e2) of+ -- do I really need the _:_ instead of just _?+ -- do I really need to restrict to functional values?+ (ef@(Constant _ _):(_:_),eg@(Constant _ _):(_:_)) -> ef ->- eg+ _ -> False+ e1 `ff` e2 =+ case (unfoldApp e1, unfoldApp e2) of+ -- Not restricting to functional values.+ -- Since we are making an equality comparison,+ -- this hopefully will be strict enough not bo break KBO.+ (f:xs,g:ys) -> f == g+ && length xs == length ys+ && case dropEq xs ys of+ (x:_,y:_) -> x >=\/ y+ _ -> False+ _ -> False++-- | Weight function for kboBy:+--+-- * Variables weigh 1+-- * Nullary functions weigh 1 (a.k.a. constants)+-- * N-ary functions weigh 0+-- * Unary functions weigh 1+--+-- This is the weight when using '>|'.+weight :: Expr -> Int+weight = w+ where+ w (e1 :$ e2) = weight e1 + weight e2+ w (Var _ _) = 1+ w e = case arity e of+ 0 -> 1+ 1 -> 1+ _ -> 0++-- | Weight function for kboBy:+--+-- * Variables weigh 1+-- * Nullary functions weigh 1 (a.k.a. constants)+-- * N-ary functions weigh 0+-- * Unary functions weigh 1 except for the one given as argument+weightExcept :: Expr -> Expr -> Int+weightExcept f0 = w+ where+ w (e1 :$ e2) = w e1 + w e2+ w (Var _ _) = 1+ w e = case arity e of+ 0 -> 1+ 1 -> if e == f0 then 0 else 1+ _ -> 0++-- | To be used alongside weightExcept+gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+gtExcept (>) f0 e1 e2 | e2 == f0 = False -- nothing can be greater than f0+ | e1 == f0 = True -- f0 is greater than everything+ | otherwise = e1 > e2 -- compare normally++-- Note this default Dershowitz order can sometimes be weird:+--+-- > x - y |> x + negate y -- as (-) > (+)+-- > negate x + y |> negate (x + negate y) -- as (+) > negate, as I->I->I > I->I+(|>) :: Expr -> Expr -> Bool+(|>) = dwoBy (>)+infix 4 |>++-- | Dershowitz reduction order as defined in TRAAT+--+-- @|>@ a "D" for Dershowitz+dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool+dwoBy (>) = (|>)+ where+ e1 |> e2@(Var n t) | (t,n) `elem` vars e1 && e1 /= e2 = True+ e1 |> e2 = any (|>= e2) xs+ || (notVar f && notVar g && f > g && all (e1 |>) ys)+ || (notVar f && notVar g && f == g && all (e1 |>) ys+ && case dropEq xs ys of+ (x:_,y:_) -> x |> y+ _ -> False)+ where+ (f:xs) = unfoldApp e1+ (g:ys) = unfoldApp e2+ notVar (Var _ _) = False+ notVar _ = True+ e1 |>= e2 = e1 == e2+ || e1 |> e2++++--- Misc Utilities ---++dropEq :: Eq a => [a] -> [a] -> ([a],[a])+dropEq (x:xs) (y:ys) | x == y = dropEq xs ys+dropEq xs ys = (xs,ys)
+ src/Test/Speculate/Report.hs view
@@ -0,0 +1,144 @@+module Test.Speculate.Report+ ( report+ )+where++import Test.Speculate.Expr+import Test.Speculate.Reason+import Test.Speculate.SemiReason+import Test.Speculate.CondReason+import Test.Speculate.Engine+import Test.Speculate.Sanity+import Test.Speculate.Args+import Test.Speculate.Utils+import Test.Speculate.Utils.Colour++import Data.Ratio ((%))+import Control.Monad (when,unless)+import Test.LeanCheck.Utils ((&&&&))+import Data.List (intercalate)++report :: Args -> IO ()+report args@Args {maxSize = sz, maxTests = n} = do+ 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'+ putArgs args+ when (showConstants args) . putStrLn . unlines $ map show ds'+ warnMissingInstances ti ats+ let ies = instanceErrors ti n ats+ unless (null ies) $ do+ let pref | force args = "Warning: "+ | otherwise = "Error: "+ putStrLn . unlines . map (pref ++) $ ies+ unless (force args) $ do+ putStrLn "There were instance errors, refusing to run."+ 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+ 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++putArgs :: Args -> IO ()+putArgs args = when (showArgs args) $ do+ let sz = maxSize args+ let isz = computeMaxSemiSize args+ let csz = computeMaxCondSize args+ putOpt "max expr size" sz+ when (isz /= sz) $ putOpt " |- on ineqs" isz+ when (csz /= sz) $ putOpt " |- on conds" csz+ case maxDepth args of+ Nothing -> return ()+ Just d -> putOpt "max expr depth" (show d)+ putOpt "max #-tests" (maxTests args)+ when (showConditions args) $+ putOptSuffix "min #-tests" (minTests args $ maxTests args) " (to consider p ==> q true)"+ putOptSuffix "max #-vars" (maxVars args) " (for inequational and conditional laws)"+ case evalTimeout args of+ Nothing -> return ()+ Just t -> putOptSuffix "eval timeout" t "s"+ putStrLn ""+ where+ putOpt :: Show a => String -> a -> IO ()+ putOpt s x = putOptSuffix s x ""+ putOptSuffix :: Show a => String -> a -> String -> IO ()+ putOptSuffix s x p = putStrLn $ alignLeft 14 s ++ " = " ++ alignRight 4 (show x) ++ p++warnMissingInstances :: Instances -> [TypeRep] -> IO ()+warnMissingInstances is ts = putLines+ $ ["Warning: no Listable instance for " ++ show t +++ ", variables of this type will not be considered"+ | t <- ts, not (isListable is t)]+ ++ ["Warning: no Eq instance for " ++ show t +++ ", equations of this type will not be considered"+ | t <- ts, not (isEq is t)]+ ++ ["Warning: no Ord instance for " ++ show t +++ ", inequations of this type will not be considered"+ | t <- ts, not (isOrd is t)]++reportClassesFor :: Instances -> Int -> [Int] -> Thy -> [Expr] -> IO ()+reportClassesFor ti nTests nVarss thy res = do+ mapM_ (putStrLn . unlines . map show . r) nVarss+ mapM_ pn nVarss+ where+ pn 0 = putStrLn $ "Number of Eq schema classes: " ++ show (length $ r 0)+ pn n = putStrLn $ "Number of Eq " ++ show n ++ "-var classes: " ++ show (length $ r n)+ r 0 = filter (isEqE ti) res+ r n = distinctFromSchemas ti nTests n thy (r 0)++reportDot :: Instances -> [String] -> Bool -> Int -> Int -> Thy -> [Expr] -> IO ()+reportDot ti onlyTypes quiet nVars n thy es = do+ let ces = distinctFromSchemas ti n nVars thy+ $ (if null onlyTypes+ then id+ else filter ((`elem` map (map toLower) onlyTypes) . map toLower . show . typ))+ $ filter (isEqOrdE ti) es+ let res = [(trueRatio ti n e, e) | e <- ces, typ e == boolTy]+ putStrLn "digraph G {"+ putStrLn " rankdir = BT"+ putStrLn . unlines+ . map showExprEdge+ . psortBy ((/=) &&&& lessOrEqual ti n)+ $ ces+ unless quiet . putStrLn . unlines+ . map (\(r,e) -> showExprNode e+ ++ " [style=filled, fillcolor = \""+ ++ showNodeColour (length (vars e) % (nVars*2)) r+ ++ "\"]")+ . filter (\(r,e) -> typ e == boolTy)+ $ res+ putStrLn . unlines+ . map (\e -> " " ++ showExprNode e ++ " [shape=box]")+ . filter isEquation+ . map snd+ $ res+--let rs = sort $ map fst ress+--putStrLn . unlines $ zipWith (\r1 r2 -> "\"" ++ show r1 ++ "\" -> \"" ++ show r2 ++ "\"") rs (tail rs)+--putStrLn . unlines $ map showRank $ collectSndByFst res+ putStrLn "}"+ where+ showRank (r,es) = " { rank = same; " ++ "\"" ++ show r ++ "\""+ ++ intercalate "; " (map showExprNode es)+ ++ " }"+ showExprEdge (e1,e2) = " " ++ showExprNode e1 ++ " -> " ++ showExprNode e2+ showExprNode e+ | typ e == boolTy && not quiet = let tre = trueRatio ti n e+ in "\"" ++ showExpr e+ ++ "\\n" ++ showRatio tre+ ++ "\\n" ++ show (percent tre) ++ "%\""+ | otherwise = "\"" ++ showExpr e ++ "\""+ showNodeColour varRatio trueRatio =+ showRGB $ fromHSV (hue0 blue) (frac $ coerceRatio varRatio) 1+ `mix` fromHSV (hue0 orange) (1 - frac (coerceRatio trueRatio)) 1+ `mix` white
+ src/Test/Speculate/Sanity.hs view
@@ -0,0 +1,69 @@+module Test.Speculate.Sanity+ ( instanceErrors+ , eqOrdErrors+ , eqErrors+ , ordErrors+ )+where++import Test.Speculate.Expr+import Test.LeanCheck ((==>))+import Data.Maybe (fromMaybe)+import Data.List (intercalate)+import Test.Speculate.Utils++(-==>-) :: Expr -> Expr -> Expr+e1 -==>- e2 = impliesE :$ e1 :$ e2 where impliesE = constant "==>" (==>)+infixr 1 -==>-++(-&&-) :: Expr -> Expr -> Expr+e1 -&&- e2 = andE :$ e1 :$ e2 where andE = constant "&&" (&&)+infixr 3 -&&-++-- returns a list of errors on the Eq instances (if any)+-- returns an empty list when ok+eqErrors :: Instances -> Int -> TypeRep -> [String]+eqErrors is n t =+ ["not reflexive" | f (x -==- x)]+ ++ ["not symmetric" | f ((x -==- y) -==- (y -==- x))]+ ++ ["not transitive" | f (((x -==- y) -&&- (y -==- z)) -==>- (x -==- z))]+ where+ f = not . true is n+ e1 -==- e2 = fromMaybe falseE $ equation is e1 e2+ x = Var "x" t+ y = Var "y" t+ z = Var "z" t++-- returns a list of errors on the Ord instance (if any)+ordErrors :: Instances -> Int -> TypeRep -> [String]+ordErrors is n t =+ ["not reflexive" | f (x -<=- x)]+ ++ ["not antisymmetric" | f (((x -<=- y) -&&- (y -<=- x)) -==>- (x -==- y))]+ ++ ["not transitive" | f (((x -<=- y) -&&- (y -<=- z)) -==>- (x -<=- z))]+ where+ f = not . true is n+ e1 -==- e2 = fromMaybe falseE $ equation is e1 e2+ e1 -<=- e2 = fromMaybe falseE $ comparisonLE is e1 e2+ x = Var "x" t+ y = Var "y" t+ z = Var "z" t++eqOrdErrors :: Instances -> Int -> TypeRep -> [String]+eqOrdErrors is n t =+ [ "(==) :: " ++ ty ++ " is not an equiavalence (" ++ intercalate ", " es ++ ")"+ | let es = eqErrors is n t, isEq is t, not (null es) ]+ ++ [ "(<=) :: " ++ 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)]+ where+ f = not . true is n+ x = Var "x" t+ y = Var "y" t+ z = Var "z" t+ e1 -==- e2 = fromMaybe falseE $ equation is e1 e2+ e1 -<=- e2 = fromMaybe falseE $ comparisonLE is e1 e2+ ty = show t ++ " -> " ++ show t ++ " -> Bool"++instanceErrors :: Instances -> Int -> [TypeRep] -> [String]+instanceErrors is n = concatMap $ eqOrdErrors is n
+ src/Test/Speculate/SemiReason.hs view
@@ -0,0 +1,107 @@+module Test.Speculate.SemiReason where++import Test.Speculate.Expr+import Test.Speculate.Reason+import Test.Speculate.Utils+import Data.List as L (sortBy, delete)+import Data.Function (on)++type Equation = (Expr, Expr)+-- Maybe (Bool, Expr, Expr)? where bool tells if it is strict++data Shy = Shy+ { sequations :: [Equation] -- <='s+--, ssequations :: [Equation] -- <'s -- LATER!+ , sthy :: Thy+ }++emptyShy = Shy+ { sequations = []+ , sthy = emptyThy+ }++updateSemiEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy+updateSemiEquationsBy f shy@Shy {sequations = es} = shy {sequations = f es}++mapSemiEquations :: (Equation -> Equation) -> Shy -> Shy+mapSemiEquations = updateSemiEquationsBy . map++scompareE :: Shy -> (Expr -> Expr -> Ordering)+scompareE = compareE . sthy++lesser :: Shy -> Expr -> [Expr]+lesser shy e = [ e1 | (e1,e2) <- sequations shy, e == e2 ]++greater :: Shy -> Expr -> [Expr]+greater shy e = [ e2 | (e1,e2) <- sequations shy, e == e1 ]++-- | given a semi-equation (inequality),+-- simplerThan restricts the Shy (SemiTheory)+-- into only equations simpler+-- than the given semi-equation+-- or that are instances of simpler equations.+--+-- half-baked example:+--+-- @x + 1@ is simpler than @x + y@ and it is returned.+-- @(1 + 1) + 1@ is more complex than @x + y@+-- but it is returned as well as it is an instance of @x + 1@.+simplerThan :: Equation -> Shy -> Shy+simplerThan seq = updateSEquationsBy upd+ where+ isSEInstanceOf = isInstanceOf `on` uncurry phonyEquation+ upd eqs = r ++ [seq' | seq' <- r'+ , any (seq' `isSEInstanceOf`) r ]+ where+ r = takeWhile (/= seq) eqs+ r' = drop 1 $ dropWhile (/= seq) eqs+-- simplerThan used to be just:+-- simplerThan seq = updateSEquationsBy (takeWhile (/= seq))++transConsequence :: Shy -> Equation -> Bool+transConsequence shy (e1,e2) = or [ e1' == e2'+ | e1' <- L.delete e2 $ greater shy' e1+ , e2' <- L.delete e1 $ lesser shy' e2+ ]+ where+ shy' = simplerThan (e1,e2) shy++updateSEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy+updateSEquationsBy f shy@Shy{sequations = seqs} = shy{sequations = f seqs}++stheorize :: Thy -> [Equation] -> Shy+stheorize thy seqs =+ Shy{ sequations = sortBy (compareE thy `on` uncurry phonyEquation) seqs+ , sthy = thy+ }++-- list all equation sides in a Shy+sides :: Shy -> [Expr]+sides shy = nubSortBy (scompareE shy)+ . 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)+ . 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++canonicalizeSemiEquationWith :: Instances -> Equation -> Equation+canonicalizeSemiEquationWith is (e1,e2) =+ case canonicalizeWith is (e1 :$ e2) of+ e1' :$ e2' -> (e1',e2')+ _ -> error $ "canonicalizeShyWith: the impossible happened,"+ ++ "this is definitely a bug, see source!"
+ src/Test/Speculate/Utils.hs view
@@ -0,0 +1,24 @@+module Test.Speculate.Utils+ ( module Test.Speculate.Utils.Misc+ , module Test.Speculate.Utils.PrettyPrint+ , module Test.Speculate.Utils.Tuple+ , module Test.Speculate.Utils.String+ , module Test.Speculate.Utils.List+ , module Test.Speculate.Utils.Tiers+ , module Test.Speculate.Utils.Typeable+ , module Test.Speculate.Utils.Timeout+ , module Test.Speculate.Utils.Ord+ , module Test.Speculate.Utils.Memoize+ )+where++import Test.Speculate.Utils.Misc+import Test.Speculate.Utils.PrettyPrint+import Test.Speculate.Utils.Tuple+import Test.Speculate.Utils.String+import Test.Speculate.Utils.List+import Test.Speculate.Utils.Tiers+import Test.Speculate.Utils.Typeable+import Test.Speculate.Utils.Timeout+import Test.Speculate.Utils.Ord+import Test.Speculate.Utils.Memoize
+ src/Test/Speculate/Utils/Class.hs view
@@ -0,0 +1,41 @@+module Test.Speculate.Utils.Class+ ( merge+ , mergesOn+ , mergesThat+ , rep+ , map+ , fromRep+ , Class+ )+where++import Test.Speculate.Utils.List (collectOn)+import Data.Function (on)+import Data.List (partition)+import Prelude hiding (map)+import qualified Prelude as P (map)++type Class a = (a,[a])++map :: (a -> b) -> Class a -> Class b+map f (x,xs) = (f x, P.map f xs)++rep :: Class a -> a+rep (x,_) = x++fromRep :: a -> Class a+fromRep x = (x,[])++mergesOn :: Eq b => (a -> b) -> [Class a] -> [Class a]+mergesOn f = P.map (map fst)+ . mergesThat ((==) `on` snd)+ . P.map (map $ \x -> (x, f x))++mergesThat :: (a -> a -> Bool) -> [Class a] -> [Class a]+mergesThat _ [] = []+mergesThat (===) (c:cs) = foldl merge c cs' : mergesThat (===) cs''+ where+ (cs',cs'') = partition (\c' -> rep c === rep c') cs++merge :: Class a -> Class a -> Class a+merge (x,xs) (y,ys) = (x,xs ++ y:ys)
+ src/Test/Speculate/Utils/Colour.hs view
@@ -0,0 +1,304 @@+-- | Simple colour module.+module Test.Speculate.Utils.Colour+ ( Colour (RGB)+ , Color+ , showRGB+ , (.+.), (.-.), (.*.)+ , black, white, grey+ , red, green, blue+ , cyan, magenta, yellow+ , violet, orange, lime, aquamarine, azure, indigo+ , makeGrey+ , grey1, grey2, grey3, grey4, grey5, grey6, grey7, grey8, grey9+ , rgb, cmy+ , chroma+ , hue0+ , hue+ , intensity, value, lightness+ , saturation, saturationHSV, saturationHSL, saturationHSI+ , fromRGB, fromCMY, fromHSV, fromHSL, fromHCL, fromHCM+ , mix, mixHSV++ -- * colour properties+ , primary, secondary, tertiary+ , primary'+ , isGrey+ , notGrey+ , isOppositeTo++ -- * Misc Utils+ , frac+ , coerceRatio+ , modulo+ )+where++import Data.Char+import Data.List+import Data.Maybe+import Data.Ratio+import Data.Tuple+import Data.Functor ((<$>)) -- for GHC < 7.10+import Control.Applicative ((<*>)) -- for GHC < 7.10++data Colour = RGB Rational Rational Rational+ deriving (Eq, Ord)++type Color = Colour++instance Show Colour where+ show c@(RGB r g b) = "RGB (" ++ show r ++ ") (" ++ show g ++ ") (" ++ show b ++ ")"+ ++ " {- " ++ showRGB c ++ " -}"++showRGB :: Colour -> String+showRGB (RGB r g b) = "#" ++ hexRatio r ++ hexRatio g ++ hexRatio b++hexRatio :: Integral a => Ratio a -> String+hexRatio r = hex $ numerator r * 0xFF `div` denominator r++hex :: Integral a => a -> String+hex = (\s -> case s of+ [] -> "00"+ [c] -> '0':[c]+ cs -> cs)+ . map (intToDigit . coerceNum)+ . reverse+ . unfoldr (\n -> listToMaybe [swap $ n `divMod` 16 | n /= 0])++coerceNum :: (Integral a, Num b) => a -> b+coerceNum = fromInteger . toInteger++coerceRatio :: (Integral a, Integral b) => Ratio a -> Ratio b+coerceRatio r = coerceNum (numerator r) % coerceNum (denominator r)++mod1 :: Integral a => Ratio a -> Ratio a+mod1 r = (numerator r `mod` denominator r) % denominator r++modulo :: Integral a => Ratio a -> Ratio a -> Ratio a+n `modulo` d = mod1 (n / d) * d++frac :: Integral a => Ratio a -> Ratio a+frac r | r < 0 = 0+ | r > 1 = 1+ | otherwise = r++instance Num Colour where+ RGB r1 g1 b1 + RGB r2 g2 b2 = RGB (frac $ r1 + r2) (frac $ g1 + g2) (frac $ b1 + b2)+ RGB r1 g1 b1 - RGB r2 g2 b2 = RGB (frac $ r1 - r2) (frac $ g1 - g2) (frac $ b1 - b2)+ RGB r1 g1 b1 * RGB r2 g2 b2 = RGB (r1 * r2) (g1 * g2) (b1 * b2)+ negate (RGB r g b) = RGB (1 - r) (1 - g) (1 - b)+ abs c = c+ signum c = 1+ fromInteger i = let j = i `div` 0x100+ k = j `div` 0x100+ in RGB (k `mod` 0x100 % 255) (j `mod` 0x100 % 255) (i `mod` 0x100 % 255)++(.+.) :: Colour -> Colour -> Colour+c1 .+. c2 = negate $ negate c1 + negate c2++(.-.) :: Colour -> Colour -> Colour+c1 .-. c2 = negate $ negate c1 - negate c2++(.*.) :: Colour -> Colour -> Colour+c1 .*. c2 = negate $ negate c1 * negate c2++black :: Colour+black = RGB 0 0 0++white :: Colour+white = RGB 1 1 1++red :: Colour+red = RGB 1 0 0++green :: Colour+green = RGB 0 1 0++blue :: Colour+blue = RGB 0 0 1++cyan :: Colour+cyan = RGB 0 1 1++magenta :: Colour+magenta = RGB 1 0 1++yellow :: Colour+yellow = RGB 1 1 0++violet :: Colour+violet = red `mix` magenta++orange :: Colour+orange = red `mix` yellow++lime :: Colour+lime = green `mix` yellow++aquamarine :: Colour+aquamarine = green `mix` cyan++azure :: Colour+azure = blue `mix` cyan++indigo :: Colour+indigo = blue `mix` magenta++grey :: Colour+grey = grey5++grey1, grey2, grey3, grey4, grey5, grey6, grey7, grey8, grey9 :: Colour+grey1 = makeGrey $ 1%10+grey2 = makeGrey $ 2%10+grey3 = makeGrey $ 3%10+grey4 = makeGrey $ 4%10+grey5 = makeGrey $ 5%10+grey6 = makeGrey $ 6%10+grey7 = makeGrey $ 7%10+grey8 = makeGrey $ 8%10+grey9 = makeGrey $ 9%10++makeGrey :: Rational -> Colour+makeGrey r = RGB r r r++rgb :: Colour -> (Rational, Rational, Rational)+rgb (RGB r g b) = (r,g,b)++cmy :: Colour -> (Rational, Rational, Rational)+cmy (RGB r g b) = (1 - r, 1 - g, 1 - b)++maxi :: Colour -> Rational+maxi (RGB r g b) = maximum [r,g,b]++mini :: Colour -> Rational+mini (RGB r g b) = minimum [r,g,b]++chroma :: Colour -> Rational+chroma c = maxi c - mini c++hue0 :: Colour -> Rational+hue0 = fromMaybe 0 . hue++hue :: Colour -> Maybe Rational+hue colour@(RGB r g b) = (\h' -> mod1 $ h' / 6) <$> h' -- h' * 60 / 360+ where+ c = chroma colour+ m = maxi colour+ h' | c == 0 = Nothing+ | m == r = Just $ (g - b) / c+ | m == g = Just $ (b - r) / c + 2+ | m == b = Just $ (r - g) / c + 4++intensity :: Colour -> Rational+intensity (RGB r g b) = (r + g + b) / 3++value :: Colour -> Rational+value = maxi++lightness :: Colour -> Rational+lightness c = (maxi c + mini c) / 2++saturation :: Colour -> Rational+saturation = saturationHSV++saturationHSV :: Colour -> Rational+saturationHSV c =+ if value c == 0+ then 0+ else chroma c / value c++saturationHSL :: Colour -> Rational+saturationHSL c =+ if lightness c == 1+ then 0+ else chroma c / (1 - abs (2 * lightness c - 1))++saturationHSI :: Colour -> Rational+saturationHSI c =+ case intensity c of+ 0 -> 0+ i -> 1 - mini c/i++fromRGB :: Rational -> Rational -> Rational -> Colour+fromRGB = RGB++-- TODO: double check this, I don't think this is quite right+fromCMY :: Rational -> Rational -> Rational -> Colour+fromCMY c m y = RGB (1 - c) (1 - m) (1 - y)++fromHSV :: Rational -> Rational -> Rational -> Colour+fromHSV h s v = fromHCM h c m+ where+ c = v * s+ m = v - c++fromHSL :: Rational -> Rational -> Rational -> Colour+fromHSL h s l = fromHCM h c m+ where+ c = (1 - abs (2*l - 1)) * s+ m = l - c / 2++fromHCL :: Rational -> Rational -> Rational -> Colour+fromHCL h c l = fromHCM h c m where m = (1 - c) * l++-- | From hue, chroma and min+fromHCM :: Rational -> Rational -> Rational -> Colour+fromHCM h' c m = RGB (r' + m) (g' + m) (b' + m)+ where+ h = h' `modulo` 1+ x = c * (1 - abs ((h*6) `modulo` 2 - 1))+ (r',g',b')+ | 0%6 <= h && h <= 1%6 = (c,x,0)+ | 1%6 <= h && h <= 2%6 = (x,c,0)+ | 2%6 <= h && h <= 3%6 = (0,c,x)+ | 3%6 <= h && h <= 4%6 = (0,x,c)+ | 4%6 <= h && h <= 5%6 = (x,0,c)+ | 5%6 <= h && h <= 6%6 = (c,0,x)++mix :: Colour -> Colour -> Colour+mix (RGB r1 g1 b1) (RGB r2 g2 b2) = RGB ((r1 + r2) / 2) ((g1 + g2) / 2) ((b1 + b2) / 2)++mixHSV :: Colour -> Colour -> Colour+mixHSV c1 c2 = fromHSV h+ ((saturationHSV c1 + saturationHSV c2) / 2)+ ((value c1 + value c2) / 2)+ where+ h = fromMaybe 0 $ do+ hc1 <- hue c1+ hc2 <- hue c2+ return $ (hc1 + hc2) / 2++primary' :: Colour -> Bool+primary' c = c == red+ || c == green+ || c == blue++primary :: Colour -> Bool+primary c = hue c == hue red+ || hue c == hue green+ || hue c == hue blue++secondary :: Colour -> Bool+secondary c = hue c == hue cyan+ || hue c == hue magenta+ || hue c == hue yellow++tertiary :: Colour -> Bool+tertiary c = hue c == hue violet+ || hue c == hue orange+ || hue c == hue lime+ || hue c == hue aquamarine+ || hue c == hue azure+ || hue c == hue indigo++isGrey :: Colour -> Bool+isGrey = isNothing . hue++notGrey :: Colour -> Bool+notGrey = isJust . hue++isOppositeTo :: Colour -> Colour -> Bool+c1 `isOppositeTo` c2 = notGrey c1 && notGrey c2+ && saturation c1 == saturation c2+ && lightness c1 == lightness c2+ && (hue0 c1 + 1/2) `modulo` 1 == hue0 c2
+ src/Test/Speculate/Utils/Digraph.hs view
@@ -0,0 +1,65 @@+module Test.Speculate.Utils.Digraph+ ( Digraph+ , empty+ , succs+ , preds+ , filter+ , discard+ , isNode+ , isEdge+ , fromEdges+ , narrow+ )+where++import Prelude hiding (filter)+import qualified Data.List as L+import Data.Maybe (fromMaybe,isJust)+import Test.Speculate.Utils (collectSndByFst)++type Digraph a = [(a,[a])]++empty :: Digraph a+empty = []++succs :: Eq a => a -> Digraph a -> [a]+succs x = fromMaybe [] . lookup x++preds :: Eq a => a -> Digraph a -> [a]+preds x yyss = [y | (y,ys) <- yyss, x `elem` ys]++isNode :: Eq a => a -> Digraph a -> Bool+isNode x = isJust . lookup x++isEdge :: Eq a => a -> a -> Digraph a -> Bool+isEdge x y d = y `elem` succs x d++filter :: Eq a => (a -> Bool) -> Digraph a -> Digraph a+filter p xxss = [(x,L.filter p xs) | (x,xs) <- xxss, p x]++discard :: Eq a => (a -> Bool) -> Digraph a -> Digraph a+discard p = filter (not . p)++subgraph :: Eq a => [a] -> Digraph a -> Digraph a+subgraph xs = filter (`elem` xs)++invsubgraph :: Eq a => [a] -> Digraph a -> Digraph a+invsubgraph xs = discard (`elem` xs)++fromEdges :: Ord a => [(a,a)] -> Digraph a+fromEdges = collectSndByFst++-- | pick a node in a Digraph+pick :: Eq a => Digraph a -> Maybe a+pick [] = Nothing+pick ((x,xs):xxss) = Just x++narrow :: Eq a => (a -> Bool) -> Digraph a -> [a]+narrow p d =+ case pick d of+ Nothing -> []+ Just n+ | p n -> case narrow p (subgraph (L.delete n $ succs n d) d) of+ [] -> n:narrow p (invsubgraph (n:succs n d ++ preds n d) d)+ xs -> xs+ | otherwise -> narrow p (invsubgraph (n:succs n d) d)
+ src/Test/Speculate/Utils/List.hs view
@@ -0,0 +1,205 @@+{-# LANGUAGE CPP #-}+module Test.Speculate.Utils.List+ ( pairsThat+ , count, counts, countsBy+ , firsts+ , nubSort, nubSortBy+ , (+++), nubMerge, nubMergeBy, nubMergeOn, nubMerges, nubMergeMap+ , ordIntersect, ordIntersectBy+ , ordered, orderedBy, orderedOn, strictlyOrdered, strictlyOrderedOn+ , areAll, areAny+ , allLater+ , (+-)+ , sortOn+ , groupOn+ , collectOn, collectBy, collectWith, collectSndByFst+ , discard, discardLater, discardEarlier, discardOthers, discardByOthers+ , allUnique+ , chain+ , zipWithReverse+ , medianate+ , takeGreaterHalf+ , accum+ , partitionByMarkers+ )+where++import Data.List+import Data.Function (on)++pairsThat :: (a -> a -> Bool) -> [a] -> [(a,a)]+pairsThat p xs = [(x,y) | x <- xs, y <- xs, p x y]++count :: Eq a => a -> [a] -> Int+count x = length . filter (==x)++counts :: Eq a => [a] -> [(a,Int)]+counts [] = []+counts (x:xs) = (x,1+count x xs) : counts (filter (/= x) xs)++countsBy :: Eq b => (a -> b) -> [a] -> [(b,Int)]+countsBy f = counts . map f++firsts :: Eq a => [a] -> [a]+firsts [] = []+firsts (x:xs) = x : firsts (filter (/= x) xs)++nubSort :: Ord a => [a] -> [a]+nubSort = nub . sort++nubSortBy :: (a -> a -> Ordering) -> [a] -> [a]+nubSortBy cmp = nubBy (\x y -> x `cmp` y == EQ) . sortBy cmp++nubMergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]+nubMergeBy cmp (x:xs) (y:ys) = case x `cmp` y of+ LT -> x:nubMergeBy cmp xs (y:ys)+ GT -> y:nubMergeBy cmp (x:xs) ys+ EQ -> x:nubMergeBy cmp xs ys+nubMergeBy _ xs ys = xs ++ ys++nubMergeOn :: Ord b => (a -> b) -> [a] -> [a] -> [a]+nubMergeOn f = nubMergeBy (compare `on` f)++nubMerge :: Ord a => [a] -> [a] -> [a]+nubMerge = nubMergeBy compare++(+++) :: Ord a => [a] -> [a] -> [a]+(+++) = nubMerge+infixr 5 +++++ordIntersectBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]+ordIntersectBy cmp (x:xs) (y:ys) = case x `cmp` y of+ LT -> ordIntersectBy cmp xs (y:ys)+ GT -> ordIntersectBy cmp (x:xs) ys+ EQ -> x:ordIntersectBy cmp xs ys+ordIntersectBy _ xs ys = []++ordIntersect :: Ord a => [a] -> [a] -> [a]+ordIntersect = ordIntersectBy compare++nubMerges :: Ord a => [[a]] -> [a]+nubMerges [] = []+nubMerges [xs] = xs+nubMerges xss = nubMerges yss `nubMerge` nubMerges zss+ where+ (yss,zss) = splitHalf xss+ splitHalf xs = splitAt (length xs `div` 2) xs++nubMergeMap :: Ord b => (a -> [b]) -> [a] -> [b]+nubMergeMap f = nubMerges . map f++orderedBy :: (a -> a -> Bool) -> [a] -> Bool+orderedBy (<) (x:y:xs) = x < y && orderedBy (<) (y:xs)+orderedBy _ _ = True++orderedOn :: Ord b => (a -> b) -> [a] -> Bool+orderedOn f = orderedBy (<=) . map f++ordered :: Ord a => [a] -> Bool+ordered = orderedBy (<=)++strictlyOrderedOn :: Ord b => (a -> b) -> [a] -> Bool+strictlyOrderedOn f = orderedBy (<) . map f++strictlyOrdered :: Ord a => [a] -> Bool+strictlyOrdered = orderedBy (<)++areAll :: [a] -> (a -> Bool) -> Bool+xs `areAll` p = all p xs++areAny :: [a] -> (a -> Bool) -> Bool+xs `areAny` p = any p xs++allLater :: (a -> a -> Bool) -> [a] -> Bool+allLater (<) (x:xs) = all (< x) xs && allLater (<) xs+allLater _ _ = True++-- | @xs +- ys@ superimposes @xs@ over @ys@.+--+-- [1,2,3] +- [0,0,0,0,0,0,0] == [1,2,3,0,0,0,0]+-- [x,y,z] +- [a,b,c,d,e,f,g] == [x,y,z,d,e,f,g]+-- "asdf" +- "this is a test" == "asdf is a test"+(+-) :: Eq a => [a] -> [a] -> [a]+xs +- ys = xs ++ drop (length xs) ys++groupOn :: Eq b => (a -> b) -> [a] -> [[a]]+groupOn f = groupBy ((==) `on` f)++#if __GLASGOW_HASKELL__ < 710+sortOn :: Ord b => (a -> b) -> [a] -> [a]+sortOn f = sortBy (compare `on` f)+#endif++-- TODO: rename this to classify!+collectOn :: Ord b => (a -> b) -> [a] -> [[a]]+collectOn f = groupOn f . sortOn f++collectBy :: (a -> a -> Ordering) -> [a] -> [[a]]+collectBy cmp = groupBy (===) . sortBy cmp+ where+ x === y = x `cmp` y == EQ++collectWith :: Ord b+ => (a -> b) -> (a -> c) -> (b -> [c] -> d)+ -> [a] -> [d]+collectWith f g h = map collapse+ . groupOn f+ where collapse (x:xs) = f x `h` map g (x:xs)++collectSndByFst :: Ord a => [(a,b)] -> [(a,[b])]+collectSndByFst = collectWith fst snd (,)++discard :: (a -> Bool) -> [a] -> [a]+discard p = filter (not . p)++discardLater :: (a -> a -> Bool) -> [a] -> [a]+discardLater d [] = []+discardLater d (x:xs) = x : discardLater d (discard (`d` x) xs)++discardEarlier :: (a -> a -> Bool) -> [a] -> [a]+discardEarlier d = reverse . discardLater d . reverse++discardOthers :: (a -> a -> Bool) -> [a] -> [a]+discardOthers d = dis []+ where+ dis xs [] = xs+ dis xs (y:ys) = dis (y:discard (`d` y) xs) (discard (`d` y) ys)++discardByOthers :: (a -> [a] -> Bool) -> [a] -> [a]+discardByOthers f = d []+ where+ d xs [] = xs+ d xs (y:ys) | f y (xs ++ ys) = d xs ys+ | otherwise = d (xs++[y]) ys++allUnique :: Ord a => [a] -> Bool+allUnique xs = nub (sort xs) == sort xs++chain :: [a -> a] -> a -> a+chain = foldr (.) id++zipWithReverse :: (a -> a -> b) -> [a] -> [b]+zipWithReverse f xs = zipWith f xs (reverse xs)++-- bad name, can't think of something better+medianate :: (a -> a -> b) -> [a] -> [b]+medianate f xs = zipWith f (takeGreaterHalf xs) (takeGreaterHalf $ reverse xs)++takeGreaterHalf :: [a] -> [a]+takeGreaterHalf xs = take (uncurry (+) $ length xs `divMod` 2) xs++accum :: Num a => [a] -> [a]+accum = a 0+ where+ a _ [] = []+ a s (x:xs) = s+x : a (s+x) xs++-- partitionByMarkers x y [x,a,b,c,y,d,e,f,x,g] == ([a,b,c,g],[d,e,f])+partitionByMarkers :: Eq a => a -> a -> [a] -> ([a],[a])+partitionByMarkers y z xs =+ case span (\x -> x /= y && x /= z) xs of+ (ys,[]) -> (ys,[])+ (ys,x:zs)+ | 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."
+ src/Test/Speculate/Utils/Memoize.hs view
@@ -0,0 +1,43 @@+module Test.Speculate.Utils.Memoize+ ( memory, memory2+ , memoryFor, memory2For+ , withMemory, withMemory2+ )+where++import qualified Data.Map as M+import Data.Map (Map)+import Test.LeanCheck (Listable(..))+import Data.Maybe (fromMaybe)++defaultMemory :: Int+defaultMemory = 2520 -- 2^3 * 3^2 * 5 * 7++{- those don't work, GHC wont cache them+memoize :: (Listable a, Ord a) => (a -> b) -> a -> b+memoize = memoizeFor defaultMemory++memoizeFor :: (Listable a, Ord a) => Int -> (a -> b) -> a -> b+memoizeFor n f x = fromMaybe (f x) (M.lookup x m)+ where+ m = memoryFor n f+-}++withMemory :: Ord a => (a -> b) -> Map a b -> a -> b+withMemory f m x = fromMaybe (f x) (M.lookup x m)++withMemory2 :: (Ord a, Ord b) => (a -> b -> c) -> Map (a,b) c -> a -> b -> c+withMemory2 f m = curry (uncurry f `withMemory` m)++memory :: (Listable a, Ord a) => (a -> b) -> Map a b+memory = memoryFor defaultMemory++memory2 :: (Listable a, Listable b, Ord a, Ord b) => (a -> b -> c) -> Map (a,b) c+memory2 = memory2For defaultMemory++memoryFor :: (Listable a, Ord a) => Int -> (a -> b) -> Map a b+memoryFor n f = foldr (uncurry M.insert) M.empty . take n $ map (\x -> (x, f x)) list++memory2For :: (Listable a, Listable b, Ord a, Ord b)+ => Int -> (a -> b -> c) -> Map (a,b) c+memory2For n f = memoryFor n (uncurry f)
+ src/Test/Speculate/Utils/Misc.hs view
@@ -0,0 +1,116 @@+module Test.Speculate.Utils.Misc where++import Test.LeanCheck+import Data.Maybe+import Data.List+import Data.Char+import Data.Function+import Data.Ratio+import Data.Tuple+import Test.Speculate.Utils.String+import Test.Speculate.Utils.List++-- easy debug:+undefined1 :: a+undefined1 = error "undefined1"++undefined2 :: a+undefined2 = error "undefined2"++-- TODO: Find a better name for iss:+--+-- > iss 0 0 = [ [] ]+-- > iss 0 1 = [ [0] ]+-- > iss 0 2 = [ [0,1], [0,0] ]+-- > iss 0 3 = [ [0,1,2], [0,1,0], [0,1,1], [0,0,1], [0,0,0] ]+iss :: Int -> Int -> [[Int]]+iss _ 0 = [[]]+iss i n = concat [map (j:) (iss (i + j-=-i) (n-1)) | j <- i:[0..(i-1)]]+ where x -=- y | x == y = 1+ | otherwise = 0++thn :: Ordering -> Ordering -> Ordering+thn EQ o = o+thn o _ = o+infixr 8 `thn`++-- TODO: Add a function like this on LeanCheck? Not working exactly like+-- this, but something like:+--+-- > > classifyBy somefoo+-- > Int: 9988 99%+-- > Bool: 10 0%+-- > Char: 2 0%+-- > total: 10000 100%+--+-- > > preconditionInfo [precond_1, precond_2, precond_3]+-- > precond_1: 3 0%+-- > precond_2: 100 1%+-- > precond_3: 2345 23%+--+-- > > preconditionInfoT [...]+-- > tier cond1 cond2 cond3+-- > 0 9 100 1% 303 2% 3821 4%+-- > 1 56 100 1% 303 2% 3821 4%+-- > 2 102 100 1% 303 2% 3821 4%+-- > 3 400 100 1% 303 2% 3821 4%+-- > 4 713 100 1% 303 2% 3821 4%+-- > all 1232 100 1% 303 2% 3821 4%+reportCountsBy :: (Eq b, Show b) => (a -> b) -> [a] -> IO ()+reportCountsBy f xs = putStrLn . unlines+ . map showCount $ countsBy f xs+ where+ len = length xs+ showCount (x,n) = unquote (show x) ++ ": "+ ++ show n ++ "/" ++ show len ++ " "+ ++ show (100 * n `div` len) ++ "%"++-- O(1) bell number implementation (I'm lazy)+-- TODO: actually implement bell+bell :: Int -> Int+bell 0 = 1+bell 1 = 1+bell 2 = 2+bell 3 = 5+bell 4 = 15+bell 5 = 52+bell 6 = 203+bell 7 = 877+bell 8 = 4140+bell _ = error "bell: argument > 8, implement me!"++maybesToMaybe :: [Maybe a] -> Maybe a+maybesToMaybe = listToMaybe . catMaybes++maybe2 :: c -> (a -> b -> c) -> Maybe a -> Maybe b -> c+maybe2 _ f (Just x) (Just y) = f x y+maybe2 z _ _ _ = z++iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a+iterateUntil p f x = let fx = f x+ in if x `p` fx+ then x+ else iterateUntil p f fx++iterateUntilLimit :: Int -> (a -> a -> Bool) -> (a -> a) -> a -> a+iterateUntilLimit 0 p f x = x+iterateUntilLimit n p f x = let fx = f x+ in if x `p` fx+ then x+ else iterateUntilLimit (n-1) p f fx++showRatio :: (Integral a, Show a) => Ratio a -> String+showRatio r = show (numerator r) ++ "/" ++ show (denominator r)++percent :: Integral a => Ratio a -> a+percent r = numerator r * 100 `div` denominator r++putLines :: [String] -> IO ()+putLines [] = return ()+putLines ls = putStrLn (unlines ls)++(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d+(.:) = (.) . (.)++(..:) :: (d -> e) -> (a -> b -> c -> d) -> a -> b -> c -> e+(..:) = (.) . (.:)
+ src/Test/Speculate/Utils/Ord.hs view
@@ -0,0 +1,16 @@+module Test.Speculate.Utils.Ord+ ( module Data.Ord+ , compareIndex+ )+where++import Data.Ord+import Data.List (elemIndex)++compareIndex :: Eq a => [a] -> a -> a -> Ordering+compareIndex xs x y =+ case (elemIndex x xs, elemIndex y xs) of+ (Just i, Just j) -> i `compare` j+ (Nothing, Just _) -> GT+ (Just _, Nothing) -> LT+ _ -> EQ
+ src/Test/Speculate/Utils/PrettyPrint.hs view
@@ -0,0 +1,111 @@+-- | A very simple pretty printing library+module Test.Speculate.Utils.PrettyPrint+ ( beside+ , above+ , table+ , spaces+ )+where+-- TODO: Fix somewhat inefficient implementations, i.e.: heavy use of '(++)'.++import Data.List (intercalate,transpose,isSuffixOf)+import Data.Char (toUpper,isSpace)+import Test.Speculate.Utils.List+import Test.LeanCheck ((+|))++-- | Appends two Strings side by side, line by line+--+-- > beside ["asdf\nqw\n","zxvc\nas"] ==+-- > "asdfzxvc\n\+-- > \qw as\n"+beside :: String -> String -> String+beside cs ds = unlines $ zipWith (++) (normalize ' ' css) dss+ where [css,dss] = normalize "" [lines cs,lines ds]++-- | Append two Strings on top of each other, adding line breaks *when needed*.+above :: String -> String -> String+above cs ds = if last cs == '\n' || head ds == '\n'+ then cs ++ ds+ else cs ++ '\n':ds++-- | Formats a table. Examples:+--+-- > 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"+table :: String -> [[String]] -> String+table s [] = ""+table s sss = unlines+ . map (removeTrailing ' ')+ . map (concat . (+| spaces s))+ . transpose+ . zipWith (`normalizeTo` ' ') (discard isSpace s)+ . foldr1 (zipWith (++))+ . map (normalize "" . map lines)+ . normalize ""+ $ sss++-- | Fits a list to a certain width by appending a certain value+--+-- > fit ' ' 6 "str" == "str "+--+-- > fit 0 6 [1,2,3] == [1,2,3,0,0,0]+fit :: a -> Int -> [a] -> [a]+fit x n xs = xs ++ replicate (n - length xs) x++fitR :: a -> Int -> [a] -> [a]+fitR x n xs = replicate (n - length xs) x ++ xs++-- | normalize makes all list the same length by adding a value+--+-- > normalize ["asdf","qw","er"] == normalize ["asdf","qw ","er "]+normalize :: a -> [[a]] -> [[a]]+normalize x xs = map (x `fit` maxLength xs) xs++normalizeR :: a -> [[a]] -> [[a]]+normalizeR x xs = map (x `fitR` maxLength xs) xs++normalizeTo :: Char -> a -> [[a]] -> [[a]]+normalizeTo 'l' = normalize+normalizeTo 'r' = normalizeR++-- | Given a list of lists returns the maximum length+maxLength :: [[a]] -> Int+maxLength = maximum . (0:) . map length++removeTrailing :: Eq a => a -> [a] -> [a]+removeTrailing x = reverse+ . dropWhile (==x)+ . reverse++spaces :: String -> [String]+spaces "" = []+spaces s = case takeWhile isSpace s of+ "" -> spaces (dropWhile isntSpace $ dropWhile isSpace s)+ s' -> s' : spaces (dropWhile isntSpace $ dropWhile isSpace s)++isntSpace :: Char -> Bool+isntSpace = not . isSpace
+ src/Test/Speculate/Utils/String.hs view
@@ -0,0 +1,144 @@+module Test.Speculate.Utils.String+ ( module Data.String+ , module Data.Char+ , unquote+ , atomic+ , outernmostPrec+ , isInfix, isPrefix, isInfixedPrefix+ , toPrefix+ , prec+ , prime, primeCycle+ , namesFromTemplate+ , indent, alignRight, alignLeft+ , splitAtCommas+ )+where++import Data.String+import Data.Char+import Data.Functor ((<$>)) -- for GHC < 7.10++unquote :: String -> String+unquote ('"':s) | last s == '"' = init s+unquote s = s++-- wrong but will work for a lot of cases+atomic :: String -> Bool+atomic s | all (not . isSpace) s = True+atomic ('\'':s) | last s == '\'' = True+atomic ('"':s) | last s == '"' = True+atomic ('[':s) | last s == ']' = True+atomic ('(':s) | last s == ')' = True+atomic _ = False++outernmostPrec :: String -> Maybe Int+outernmostPrec s =+ case words s of+ [l,o,r] | isInfix o -> Just (prec o)+ _ -> Nothing++-- | Check if a function / operator is infix+--+-- > isInfix "foo" == False+-- > isInfix "(+)" == False+-- > isInfix "`foo`" == True+-- > isInfix "+" == True+isInfix :: String -> Bool+isInfix (c:_) = c `notElem` "()'\"[" && not (isAlphaNum c)++-- | Returns the precedence of default Haskell operators+prec :: String -> Int+prec " " = 10+prec "!!" = 9+prec "." = 9+prec "^" = 8+prec "^^" = 8+prec "**" = 8+prec "*" = 7+prec "/" = 7+prec "%" = 7+prec "+" = 6+prec "-" = 6+prec ":" = 5+prec "++" = 5+prec "\\" = 5+prec ">" = 4+prec "<" = 4+prec ">=" = 4+prec "<=" = 4+prec "==" = 4+prec "/=" = 4+prec "`elem`" = 4+prec "&&" = 3+prec "||" = 2+prec ">>=" = 1+prec ">>" = 1+prec ">=>" = 1+prec "<=<" = 1+prec "$" = 0+prec "`seq`" = 0+prec "==>" = 0+prec "<==>" = 0+prec _ = 9++isPrefix :: String -> Bool+isPrefix = not . isInfix++-- | Is the string of the form @`string`@+isInfixedPrefix :: String -> Bool+isInfixedPrefix ('`':cs) = last cs == '`'+isInfixedPrefix _ = False++-- | Transform an infix operator into an infix function:+--+-- > toPrefix "`foo`" == "foo"+-- > toPrefix "+" == "(+)"+toPrefix :: String -> String+toPrefix ('`':cs) = init cs+toPrefix cs = '(':cs ++ ")"++-- Primeify the name of a function by appending prime @'@ to functions and+-- minus @-@ to operators.+--+-- > prime "(+)" == "(+-)"+-- > prime "foo" == "foo'"+-- > prime "`foo`" == "`foo'`"+-- > prime "*" == "*-+prime :: String -> String+prime ('`':cs) = '`':init cs ++ "'`" -- `foo` to `foo'`+prime ('(':cs) = '(':init cs ++ "-)" -- (+) to (+-)+prime cs | isInfix cs = cs ++ "-" -- + to +-+ | otherwise = cs ++ "'" -- foo to foo'++primeCycle :: [String] -> [String]+primeCycle [] = []+primeCycle ss = ss ++ map (++ "'") (primeCycle ss)++namesFromTemplate :: String -> [String]+namesFromTemplate = primeCycle . f+ where+ f "" = f "x"+ f cs | isDigit (last cs) = map (\n -> init cs ++ show n) [digitToInt (last cs)..]+ f [c] = map ((:[]) . chr) [x,x+1,x+2] where x = ord c+ f cs | last cs == 's' = (++ "s") <$> f (init cs)+ f "xy" = ["xy","zw"]+ f [c,d] | ord d - ord c == 1 = [[c,d], [chr $ ord c + 2, chr $ ord d + 2]]+ f cs = [cs]++alignRight :: Int -> String -> String+alignRight n cs = replicate (n - length cs) ' ' ++ cs++alignLeft :: Int -> String -> String+alignLeft n cs = cs ++ replicate (n - length cs) ' '++indent :: Int -> String -> String+indent n = unlines . map (replicate n ' ' ++) . lines++splitAtCommas :: String -> [String]+splitAtCommas = words . map commaToSpace+ where+ commaToSpace ',' = ' '+ commaToSpace c = c+-- FIXME (uncomma): quick-and-dirty implementation+-- weird behaviour: uncomma "123 456,789" == ["123","456","789"]+-- but that's fine for speculate (Haskell symbols cannot have spaces)
+ src/Test/Speculate/Utils/Tiers.hs view
@@ -0,0 +1,45 @@+module Test.Speculate.Utils.Tiers+ ( productsList+ , mapTMaybe+ , discardT+ , discardLaterT+ , partitionT+ , uptoT+ , filterTS+ , discardTS+ )+where++import Test.LeanCheck+import Data.Maybe (mapMaybe)++productsList :: [[a]] -> [[a]]+productsList = concat . products . map toTiers++mapTMaybe :: (a -> Maybe b) -> [[a]] -> [[b]]+mapTMaybe f = map (mapMaybe f)++discardT :: (a -> Bool) -> [[a]] -> [[a]]+discardT p = filterT (not . p)++partitionT :: (a -> Bool) -> [[a]] -> ([[a]],[[a]])+partitionT p xss = (filterT p xss, discardT p xss)++uptoT :: Int -> [[a]] -> [a]+uptoT sz = concat . take sz++-- this passes the size of the a to the selecting function+filterTS :: (Int -> a -> Bool) -> [[a]] -> [[a]]+filterTS p = fts 0+ where+ fts n [] = []+ fts n (xs:xss) = filter (p n) xs : fts (n+1) xss++discardTS :: (Int -> a -> Bool) -> [[a]] -> [[a]]+discardTS p = filterTS ((not .) . p)++discardLaterT :: (a -> a -> Bool) -> [[a]] -> [[a]]+discardLaterT d [] = []+discardLaterT d ([]:xss) = [] : discardLaterT d xss+discardLaterT d ((x:xs):xss) = [[x]]+ \/ discardLaterT d (discardT (`d` x) (xs:xss))
+ src/Test/Speculate/Utils/Timeout.hs view
@@ -0,0 +1,35 @@+module Test.Speculate.Utils.Timeout+ ( timeoutToNothing+ , fromTimeout+ , timeoutToFalse+ , timeoutToTrue+ , timeoutToError+ )+where++import System.IO.Unsafe (unsafePerformIO)+import Control.Exception (evaluate)+import System.Timeout+import Data.Maybe (fromMaybe)++-- TODO: Move this into LeanCheck?++-- | In microseconds+usTimeoutToNothing :: Int -> a -> Maybe a+usTimeoutToNothing n = unsafePerformIO . timeout n . evaluate++-- | Returns Nothing if value cannot be evaluated to WHNF in a given number of seconds+timeoutToNothing :: RealFrac s => s -> a -> Maybe a+timeoutToNothing n = usTimeoutToNothing $ round (n * 1000000)++fromTimeout :: RealFrac s => s -> a -> a -> a+fromTimeout n x = fromMaybe x . timeoutToNothing n++timeoutToFalse :: RealFrac s => s -> Bool -> Bool+timeoutToFalse n = fromTimeout n False++timeoutToTrue :: RealFrac s => s -> Bool -> Bool+timeoutToTrue n = fromTimeout n True++timeoutToError :: RealFrac s => s -> a -> a+timeoutToError n = fromTimeout n (error "timeoutToError: timed out")
+ src/Test/Speculate/Utils/Tuple.hs view
@@ -0,0 +1,81 @@+module Test.Speculate.Utils.Tuple+ ( module Data.Tuple+ , fst3, fst4+ , snd3, snd4+ , trd3, trd4+ , fth4+ , curry3, curry4+ , uncurry3, uncurry4, uncurry5, uncurry6, uncurry7+ , uncurry8, uncurry9, uncurry10, uncurry11, uncurry12+ , (***)+ , catPairs+ )+where++import Data.Tuple++fst3 :: (a,b,c) -> a+fst3 (x,y,z) = x++snd3 :: (a,b,c) -> b+snd3 (x,y,z) = y++trd3 :: (a,b,c) -> c+trd3 (x,y,z) = z++fst4 :: (a,b,c,d) -> a+fst4 (x,y,z,w) = x++snd4 :: (a,b,c,d) -> b+snd4 (x,y,z,w) = y++trd4 :: (a,b,c,d) -> c+trd4 (x,y,z,w) = z++fth4 :: (a,b,c,d) -> d+fth4 (x,y,z,w) = w++curry3 :: ((a,b,c)->d) -> a -> b -> c -> d+curry3 f x y z = f (x,y,z)++curry4 :: ((a,b,c,d)->e) -> a -> b -> c -> d -> e+curry4 f x y z w = f (x,y,z,w)++uncurry3 :: (a->b->c->d) -> (a,b,c) -> d+uncurry3 f t = f (fst3 t) (snd3 t) (trd3 t)++uncurry4 :: (a->b->c->d->e) -> (a,b,c,d) -> e+uncurry4 f q = f (fst4 q) (snd4 q) (trd4 q) (fth4 q)++uncurry5 :: (a->b->c->d->e->f) -> (a,b,c,d,e) -> f+uncurry5 f (x,y,z,w,v) = f x y z w v++uncurry6 :: (a->b->c->d->e->f->g) -> (a,b,c,d,e,f) -> g+uncurry6 f (x,y,z,w,v,u) = f x y z w v u++uncurry7 :: (a->b->c->d->e->f->g->h) -> (a,b,c,d,e,f,g) -> h+uncurry7 f (x,y,z,w,v,u,r) = f x y z w v u r++uncurry8 :: (a->b->c->d->e->f->g->h->i) -> (a,b,c,d,e,f,g,h) -> i+uncurry8 f (x,y,z,w,v,u,r,s) = f x y z w v u r s++uncurry9 :: (a->b->c->d->e->f->g->h->i->j) -> (a,b,c,d,e,f,g,h,i) -> j+uncurry9 f (x,y,z,w,v,u,r,s,t) = f x y z w v u r s t++uncurry10 :: (a->b->c->d->e->f->g->h->i->j->k) -> (a,b,c,d,e,f,g,h,i,j) -> k+uncurry10 f (x,y,z,w,v,u,r,s,t,o) = f x y z w v u r s t o++uncurry11 :: (a->b->c->d->e->f->g->h->i->j->k->l)+ -> (a,b,c,d,e,f,g,h,i,j,k) -> l+uncurry11 f (x,y,z,w,v,u,r,s,t,o,p) = f x y z w v u r s t o p++uncurry12 :: (a->b->c->d->e->f->g->h->i->j->k->l->m)+ -> (a,b,c,d,e,f,g,h,i,j,k,l) -> m+uncurry12 f (x,y,z,w,v,u,r,s,t,o,p,q) = f x y z w v u r s t o p q++(***) :: (a -> b) -> (c -> d) -> (a,c) -> (b,d)+f *** g = \(x,y) -> (f x, g y)++catPairs :: [(a,a)] -> [a]+catPairs [] = []+catPairs ((x,y):xys) = x:y:catPairs xys
+ src/Test/Speculate/Utils/Typeable.hs view
@@ -0,0 +1,64 @@+module Test.Speculate.Utils.Typeable+ ( tyArity+ , typesIn+ , unFunTy+ , isFunTy+ , argumentTy+ , resultTy+ , finalResultTy+ , boolTy+ , mkEqnTy+ , funTyCon+ , module Data.Typeable+ )+where++import Data.Typeable+import Test.Speculate.Utils.List ((+++))++tyArity :: TypeRep -> Int+tyArity t+ | isFunTy t = 1 + tyArity (resultTy t)+ | otherwise = 0++-- | For a given type, return all *-kinded types.+-- (all non-function types)+--+-- > typesIn (typeOf (undefined :: (Int -> Int) -> Int -> Bool))+-- > == [Bool,Int]+typesIn :: TypeRep -> [TypeRep]+typesIn t+ | isFunTy t = typesIn (argumentTy t)+ +++ typesIn (resultTy t)+ | otherwise = [t]++finalResultTy :: TypeRep -> TypeRep+finalResultTy t+ | isFunTy t = finalResultTy (resultTy t)+ | otherwise = t++unFunTy :: TypeRep -> (TypeRep,TypeRep)+unFunTy t+ | isFunTy t = let (f,[a,b]) = splitTyConApp t in (a,b)+ | otherwise = error "unFunTy: not a function type"++argumentTy :: TypeRep -> TypeRep+argumentTy = fst . unFunTy++resultTy :: TypeRep -> TypeRep+resultTy = snd . unFunTy++boolTy :: TypeRep+boolTy = typeOf (undefined :: Bool)++funTyCon :: TyCon+funTyCon = typeRepTyCon $ typeOf (undefined :: () -> ())++isFunTy :: TypeRep -> Bool+isFunTy t =+ case splitTyConApp t of+ (con,[_,_]) | con == funTyCon -> True+ _ -> False++mkEqnTy :: TypeRep -> TypeRep+mkEqnTy a = a `mkFunTy` (a `mkFunTy` boolTy)
+ tests/Test.hs view
@@ -0,0 +1,648 @@+-- | This module defines utilities to test 'Speculate' itself.+--+-- It should never be exported in a cabal package, and should not be included+-- in Haddock documentation. Hence the weird name, simply "Test".+--+-- This module exports a Listable Expr instance, that does not, by any means,+-- list all possible expressions. But instead, list expressions based on the+-- names exported by this module.+module Test+ (+ -- * Module exports+ module Test.LeanCheck+ , module Test.LeanCheck.Utils+ , module Test.Speculate++ -- * Test reporting+ , reportTests+ , getMaxTestsFromArgs+ , mainTest+ , printLines++ -- * Properties+ , tiersExprTypeCorrect++ , listThyInefficient++ , IntE (..)+ , BoolE (..)+ , CharE (..)+ , ListE (..)+ , FunE (..)+ , SameTypeE (..)+ , unSameTypeE+ , SameTypedPairsE (..)+ , Thyght (..)+ , Equation (..)++ -- * Functions and values encoded as 'Expr' or functions of Exprs+ -- | Terminal values are named;+ -- Variables are duplicated;+ -- Functions are primed;+ -- Operators are surrounded by dashes.++ -- ** Integers+ , zero, one+ , xx, yy, zz, xx'+ , id', abs'+ , (-+-), (-*-), (.-.)+ , ii, jj, kk, ii'+ , negate'+ , ff, gg+ , succ'++ , idE+ , absE+ , succE+ , negateE+ , plusE+ , timesE+ , minusE++ -- ** Booleans+ , true, false+ , pp, qq, rr+ , not', (-&&-), (-||-), (-==>-)+ , (-==-), (-<=-), (-<-)+ , odd', even'++ -- ** Characters+ , aa+ , cc, dd+ , ord'+ , ordE++ -- ** Lists (of Inteters)+ , ll+ , xxs, yys+ , (-:-), (-++-)+ , head', tail'+ , insert', elem', sort'++ , consE, appendE++ -- ** Typereps+ , intTy+ , charTy++ -- ** checks for types+ , intE+ , charE+ , boolE++ -- ** Unamed holes+ , i_+ , c_+ , b_++ -- ** Dummy+ , expr++ -- ** Enumerate expressions+ , expressionsT+ )+where++import Test.LeanCheck+import Test.LeanCheck.Tiers+import Test.LeanCheck.Utils hiding (comparison)++import System.Environment (getArgs)+import System.Exit (exitFailure)+import Data.List (elemIndices)++import Test.Speculate hiding (getArgs)+import Test.Speculate.Expr hiding (true, false, ord)+import qualified Test.Speculate.Expr as E+import Test.Speculate.Reason+import Test.Speculate.Reason.Order++import Data.Char (ord)+import Data.Dynamic+import Data.Function (on)+import Data.List as L (sort,insert)+import Data.Maybe (fromMaybe)++import Test.Speculate.Utils++isTrue :: Instances -> Int -> Expr -> Bool+isTrue = E.true++isFalse :: Instances -> Int -> Expr -> Bool+isFalse = E.false++reportTests :: [Bool] -> IO ()+reportTests tests =+ case elemIndices False tests of+ [] -> putStrLn "+++ Tests passed!"+ is -> do putStrLn ("*** Failed tests:" ++ show is)+ exitFailure++getMaxTestsFromArgs :: Int -> IO Int+getMaxTestsFromArgs n = do+ as <- getArgs+ return $ case as of+ (s:_) -> read s+ _ -> n++mainTest :: (Int -> [Bool]) -> Int -> IO ()+mainTest tests n' = do+ n <- getMaxTestsFromArgs n'+ reportTests (tests n)++printLines :: Show a => [a] -> IO ()+printLines = putStrLn . unlines . map show++-- | This will not enumerate all possible 'Expr's, as that is impossible.+-- But eventually, a rather a nice subset of it, with Integers, Booleans,+-- Chars and lists of Integers.+instance Listable Expr where+ tiers = cons1 unIntE+ \/ cons1 unBoolE+ \/ cons1 unCharE+ \/ cons1 unListE `addWeight` 1+ \/ cons1 unFunE `addWeight` 1++tiersExprTypeCorrect :: Int -> Bool+tiersExprTypeCorrect n = all typeCorrect $ take n (list :: [Expr])++-- Not a particularly efficient implementation. If performance ever becomes an+-- issue, declare something like:+--+-- > tiersIntE = ...+-- > \/ mapT ord tiersCharE+-- > \/ ...+-- > where+-- > cons1 c = mapT c tiersIntE+-- > cons2 c = mapT ...++newtype IntE = IntE { unIntE :: Expr } deriving Show+newtype BoolE = BoolE { unBoolE :: Expr } deriving Show+newtype CharE = CharE { unCharE :: Expr } deriving Show+newtype ListE = ListE { unListE :: Expr } deriving Show+newtype FunE = FunE { unFunE :: Expr } deriving Show++consI :: (Expr -> a) -> [[a]]; consI f = cons1 (f . unIntE)+consB :: (Expr -> a) -> [[a]]; consB f = cons1 (f . unBoolE)+consC :: (Expr -> a) -> [[a]]; consC f = cons1 (f . unCharE)+consL :: (Expr -> a) -> [[a]]; consL f = cons1 (f . unListE)+consF :: (Expr -> a) -> [[a]]; consF f = cons1 (f . unFunE)+consII :: (Expr -> Expr -> a) -> [[a]]; consII o = cons2 (o `on` unIntE)+consBB :: (Expr -> Expr -> a) -> [[a]]; consBB o = cons2 (o `on` unBoolE)+consLL :: (Expr -> Expr -> a) -> [[a]]; consLL o = cons2 (o `on` unListE)+consIL :: (Expr -> Expr -> a) -> [[a]]; consIL o = cons2 (\(IntE x) (ListE xs) -> x `o` xs)++instance Listable IntE where+ tiers = mapT IntE $ cons0 zero `addWeight` 1+ \/ cons0 one `addWeight` 2+ \/ cons0 i_+ \/ cons0 xx+ \/ cons0 yy `addWeight` 1+ \/ cons0 zz `addWeight` 2+ \/ consI id'+ \/ consI abs' `addWeight` 1+ \/ consII (-+-)+ \/ consII (-*-) `addWeight` 1+ \/ consC ord' `addWeight` 2++instance Listable BoolE where+ tiers = mapT BoolE $ cons0 true `addWeight` 1+ \/ cons0 false `addWeight` 1+ \/ cons0 b_+ \/ cons0 pp+ \/ cons0 qq `addWeight` 1+ \/ cons0 rr `addWeight` 2+ \/ consB not'+ \/ consBB (-&&-) `addWeight` 1+ \/ consBB (-||-) `addWeight` 2+ \/ consBB (-==>-) `addWeight` 3+ \/ maybeCons1 (uncurry (equation preludeInstances) . unSameTypeE) `addWeight` 3+ \/ maybeCons1 (uncurry (comparisonLT preludeInstances) . unSameTypeE) `addWeight` 4+ \/ maybeCons1 (uncurry (comparisonLE preludeInstances) . unSameTypeE) `addWeight` 4+ \/ consI odd' `addWeight` 1+ \/ consI even' `addWeight` 1+ \/ consIL elem' `addWeight` 4++instance Listable CharE where+ tiers = mapT CharE $ cons0 aa `addWeight` 1+ \/ cons0 c_+ \/ cons0 cc+ \/ cons0 dd `addWeight` 1++instance Listable ListE where+ tiers = mapT ListE $ cons0 ll+ \/ cons0 xxs+ \/ cons0 yys `addWeight` 1+ \/ consIL (-:-)+ \/ consLL (-++-) `addWeight` 1+ \/ consIL insert' `addWeight` 2+ \/ consL sort' `addWeight` 2++instance Listable FunE where+ list = map FunE+ [ idE+ , plusE+ , appendE+ , ordE+ , consE+ , absE+ , timesE+ , negateE+ , succE+ ]++data SameTypeE = SameTypeE Expr Expr deriving Show++unSameTypeE :: SameTypeE -> (Expr,Expr)+unSameTypeE (SameTypeE e1 e2) = (e1,e2)++instance Listable SameTypeE where+ tiers = cons1 (\(IntE e1, IntE e2) -> SameTypeE e1 e2) `ofWeight` 0+ \/ cons1 (\(BoolE e1, BoolE e2) -> SameTypeE e1 e2) `ofWeight` 0+ \/ cons1 (\(CharE e1, CharE e2) -> SameTypeE e1 e2) `ofWeight` 0+ \/ cons1 (\(ListE e1, ListE e2) -> SameTypeE e1 e2) `ofWeight` 0+ \/ cons1 (\(FunE e1, FunE e2) -> SameTypeE e1 e2) `ofWeight` 0+ `suchThat` (\(SameTypeE e1 e2) -> typ e1 == typ e2) -- for func, manual++newtype SameTypedPairsE = SameTypedPairsE [(Expr,Expr)] deriving Show++instance Listable SameTypedPairsE where+ tiers = cons1 (SameTypedPairsE . map unSameTypeE) `ofWeight` 0+++zero :: Expr+zero = showConstant (0 :: Int)++one :: Expr+one = showConstant (1 :: Int)++xx :: Expr -- ex+xx = var "x" int++yy :: Expr -- wye+yy = var "y" int++zz :: Expr -- zed+zz = var "z" int++xx' :: Expr -- ex prime+xx' = var "x'" int++id' :: Expr -> Expr+id' = (idE :$)++idE :: Expr+idE = constant "id" (id :: Int -> Int)++abs' :: Expr -> Expr+abs' = (absE :$)++absE :: Expr+absE = constant "abs" (abs :: Int -> Int)++negate' :: Expr -> Expr+negate' = (negateE :$)++negateE :: Expr+negateE = constant "negate" (negate :: Int -> Int)++succ' :: Expr -> Expr+succ' = (succE :$)++succE :: Expr+succE = constant "succ" ((1+) :: Int -> Int)++(-+-) :: Expr -> Expr -> Expr+e1 -+- e2 = plusE :$ e1 :$ e2+infixl 6 -+-++plusE :: Expr+plusE = constant "+" ((+) :: Int -> Int -> Int)++(-*-) :: Expr -> Expr -> Expr+e1 -*- e2 = timesE :$ e1 :$ e2++timesE :: Expr+timesE = constant "*" ((*) :: Int -> Int -> Int)++(.-.) :: Expr -> Expr -> Expr+e1 .-. e2 = minusE :$ e1 :$ e2++minusE :: Expr+minusE = constant "-" ((-) :: Int -> Int -> Int)++ii :: Expr+ii = var "i" int++jj :: Expr+jj = var "j" int++kk :: Expr+kk = var "k" int++ii' :: Expr+ii' = var "i'" int++ff :: Expr -> Expr+ff = (ffE :$) where ffE = constant "f" (undefined :: Int -> Int)++gg :: Expr -> Expr+gg = (ggE :$) where ggE = constant "g" (undefined :: Int -> Int)+++true :: Expr+true = showConstant (True :: Bool)++false :: Expr+false = showConstant (False :: Bool)++pp :: Expr -- pee+pp = var "p" bool++qq :: Expr -- cue+qq = var "q" bool++rr :: Expr -- ar, I'm a pirate+rr = var "r" bool++not' :: Expr -> Expr+not' = (notE :$) where notE = constant "not" not++(-&&-) :: Expr -> Expr -> Expr+e1 -&&- e2 = andE :$ e1 :$ e2 where andE = constant "&&" (&&)+infixr 3 -&&-++(-||-) :: Expr -> Expr -> Expr+e1 -||- e2 = orE :$ e1 :$ e2 where orE = constant "||" (||)+infixr 2 -||-++(-==>-) :: Expr -> Expr -> Expr+e1 -==>- e2 = impliesE :$ e1 :$ e2 where impliesE = constant "==>" (==>)+infixr 0 -==>-++(-==-) :: Expr -> Expr -> Expr+e1 -==- e2 =+ fromMaybe (error $ "(-==-): cannot equate " ++ show e1 ++ " and " ++ show e2)+ (equation preludeInstances e1 e2)+infix 4 -==-++(-<=-) :: Expr -> Expr -> Expr+e1 -<=- e2 =+ fromMaybe (error $ "(-<=-): cannot lessEq " ++ show e1 ++ " and " ++ show e2)+ (comparisonLE preludeInstances e1 e2)+infix 4 -<=-++(-<-) :: Expr -> Expr -> Expr+e1 -<- e2 =+ fromMaybe (error $ "(-<-): cannot less " ++ show e1 ++ " and " ++ show e2)+ (comparisonLT preludeInstances e1 e2)+infix 4 -<-++odd' :: Expr -> Expr+odd' = (oddE :$) where oddE = constant "odd" (odd :: Int -> Bool)++even' :: Expr -> Expr+even' = (evenE :$) where evenE = constant "even" (even :: Int -> Bool)+++aa :: Expr -- a, the character, not variable+aa = showConstant 'a'++cc :: Expr -- cee, a variable character+cc = var "c" char++dd :: Expr -- dee, a variable character+dd = var "d" char++ord' :: Expr -> Expr+ord' = (ordE :$)++ordE :: Expr+ordE = constant "ord" Data.Char.ord+++ll :: Expr+ll = showConstant ([] :: [Int])++xxs :: Expr -- exes+xxs = var "xs" [int]++yys :: Expr -- wyes+yys = var "ys" [int]++(-:-) :: Expr -> Expr -> Expr+e1 -:- e2 = consE :$ e1 :$ e2+infixr 5 -:-++consE :: Expr+consE = constant ":" ((:) :: Int -> [Int] -> [Int])++(-++-) :: Expr -> Expr -> Expr+e1 -++- e2 = appendE :$ e1 :$ e2+infixr 5 -++-++appendE :: Expr+appendE = constant "++" ((++) :: [Int] -> [Int] -> [Int])++head' :: Expr -> Expr+head' exs = headE :$ exs where headE = constant "head" (head :: [Int] -> Int)++tail' :: Expr -> Expr+tail' exs = tailE :$ exs where tailE = constant "tail" (tail :: [Int] -> [Int])++insert' :: Expr -> Expr -> Expr+insert' ex exs = insertE :$ ex :$ exs where insertE = constant "insert" (L.insert :: Int -> [Int] -> [Int])++elem' :: Expr -> Expr -> Expr+elem' ex exs = elemE :$ ex :$ exs where elemE = constant "elem" (elem :: Int -> [Int] -> Bool)++sort' :: Expr -> Expr+sort' exs = sortE :$ exs where sortE = constant "sort" (sort :: [Int] -> [Int])++-- boolTy already exported by Speculate.TypeInfo++intTy :: TypeRep+intTy = typeOf int++charTy :: TypeRep+charTy = typeOf char++listTy :: TypeRep+listTy = typeOf [int]++intE :: Expr -> Bool+intE e = typ e == intTy++boolE :: Expr -> Bool+boolE e = typ e == boolTy++charE :: Expr -> Bool+charE e = typ e == charTy++listE :: Expr -> Bool+listE e = typ e == listTy++i_ :: Expr+i_ = hole int++c_ :: Expr+c_ = hole char++b_ :: Expr+b_ = hole bool++xs_ :: Expr+xs_ = hole [int]++-- | Dummy expr value, for use in type binding+expr :: Expr+expr = undefined+++data Rule = Rule Expr Expr deriving (Show, Eq, Ord)+data Equation = Equation Expr Expr deriving (Show, Eq, Ord)++unEquation :: Equation -> (Expr,Expr)+unEquation (Equation e1 e2) = (e1,e2)++-- beware: enumerating beyond 600 values will make this very slow as it is+-- very hard to satisfy canonicalEqn and ->-. In practice, this should not be a+-- problem as we enumerate far less than that when enerating 'Thy's.+instance Listable Rule where+ tiers = (`ofWeight` 0)+ . filterT (\(Rule e1 e2) -> canonicalRule (e1,e2) && e1 ->- e2)+ . mapT (uncurry Rule . orientRule)+ . filterT (uncurry (<))+ . mapT unSameTypeE+ $ tiers+ where+ (->-) = canReduceTo emptyThy+ orientRule (e1,e2) | e1 ->- e2 = (e1,e2)+ | otherwise = (e2,e1)++instance Listable Equation where+ tiers = (`ofWeight` 0)+ . mapT (uncurry Equation)+ . filterT (canonicalEqn emptyThy)+ . mapT orientEqn+ . filterT (uncurry (<=))+ . mapT unSameTypeE+ $ tiers+ where+ orientEqn (e1,e2) | e1 `compareComplexity` e2 == LT = (e2,e1)+ | otherwise = (e1,e2)++newtype RuleSet = RuleSet [(Expr,Expr)] deriving Show+newtype EquationSet = EquationSet [(Expr,Expr)] deriving Show++instance Listable RuleSet where+ tiers = setCons (RuleSet . map unRule) `ofWeight` 0+ where+ unRule (Rule e1 e2) = (e1,e2)++instance Listable EquationSet where+ tiers = setCons (EquationSet . map unEquation) `ofWeight` 0+ where+ unEquation (Equation e1 e2) = (e1,e2)++instance Listable Thy where+ tiers = concatMapT expandCanReduceTo+ $ concatMapT expandClosureLimit+ $ concatMapT expandKeepE+ $ cons2 (\(RuleSet rs) (EquationSet eqs)+ -> emptyThy { rules = sort rs+ , equations = sort eqs })++newtype Thyght = Thyght { unThyght :: Thy } deriving Show++instance Listable Thyght where+ tiers = mapT Thyght+ $ concatMapT expandCanReduceTo+ $ concatMapT expandClosureLimit+ $ mapT defaultKeep+ $ cons2 (\(RuleSet rs) (EquationSet eqs)+ -> emptyThy { rules = sort rs+ , equations = sort eqs })++expandKeepE :: Thy -> [[Thy]]+expandKeepE thy = cons0 thy+ \/ cons0 thy {keepE = keepUpToLength (maxLen + 0)} `ofWeight` 1+ \/ cons0 thy {keepE = keepUpToLength (maxLen + 1)} `ofWeight` 2+ \/ cons0 thy {keepE = keepUpToLength (maxLen + 2)} `ofWeight` 4+ \/ cons0 thy {keepE = keepUpToLength (maxLen + 3)} `ofWeight` 6+ \/ cons0 thy {keepE = keepUpToLength (maxLen + 4)} `ofWeight` 8+ where+ maxLen = maximum . map lengthE . catPairs $ equations thy ++ rules thy++expandClosureLimit :: Thy -> [[Thy]]+expandClosureLimit thy = cons0 thy {closureLimit = 3}+ \/ cons0 thy {closureLimit = 0} `ofWeight` 1+ \/ cons0 thy {closureLimit = 2} `ofWeight` 2+ \/ cons0 thy {closureLimit = 1} `ofWeight` 3++-- TODO: make Listable Thy enumeration complete w.r.t: canReduceTo+-- for a complete version, Listable Rule will have to be transformed on a+-- higher order function that take canReduceTo. (harder to maintain)+expandCanReduceTo :: Thy -> [[Thy]]+expandCanReduceTo thy = cons0 thy+ \/ if all (uncurry (|>|)) (rules thy)+ then cons0 thy {canReduceTo = (|>|)} `ofWeight` 1+ else []+ \/ if all (uncurry ( >|)) (rules thy)+ then cons0 thy {canReduceTo = ( >|)} `ofWeight` 2+ else []++listThyInefficient :: [Thy]+listThyInefficient = concat+ . concatMapT expandCanReduceTo+ . concatMapT expandClosureLimit+ . concatMapT expandKeepE+ $ cons2 (\(SameTypedPairsE rs) (SameTypedPairsE eqs)+ -> emptyThy { rules = sort rs+ , equations = sort eqs+ }) `suchThat` okThy++-- Quick and Dirty!+instance Show Thy where+ show Thy { rules = rs+ , equations = eqs+ , canReduceTo = (->-)+ , closureLimit = cl+ , keepE = keep+ }+ = "Thy { rules = "+ ++ drop 14 (indent 14 . listLines $ map showEquation rs)+ ++ " , equations = "+ ++ drop 18 (indent 18 . listLines $ map showEquation eqs)+ ++ " , canReduceTo = " ++ showCanReduceTo (->-) ++ "\n"+ ++ " , closureLimit = " ++ show cl ++ "\n"+ ++ " , keepE = " ++ showKeepE keep ++ "\n"+ ++ " }"+ where+ showEquation (e1,e2) = showExpr e1 ++ " == " ++ showExpr e2+ listLines [] = "[]"+ listLines ss = '[':(tail . unlines $ map (", " ++) ss) ++ "]"+ showCanReduceTo (->-) | holds 1000 $ (->-) ==== (|>|) = "(|>|)"+ | holds 1000 $ (->-) ==== ( >|) = "(>|)"+ | holds 1000 $ (->-) ==== (|> ) = "(|>)"+ | otherwise = "(??)"+ showKeepE keep | holds 1000 $ keep === const True = "const True"+ | holds 1000 $ keep === keepUpToLength 0 = "keepUpToLength 0"+ | holds 1000 $ keep === keepUpToLength 1 = "keepUpToLength 1"+ | holds 1000 $ keep === keepUpToLength 2 = "keepUpToLength 2"+ | holds 1000 $ keep === keepUpToLength 3 = "keepUpToLength 3"+ | holds 1000 $ keep === keepUpToLength 4 = "keepUpToLength 4"+ | holds 1000 $ keep === keepUpToLength 5 = "keepUpToLength 5"+ | holds 1000 $ keep === keepUpToLength 6 = "keepUpToLength 6"+ | holds 1000 $ keep === keepUpToLength 7 = "keepUpToLength 7"+ | holds 1000 $ keep === keepUpToLength 8 = "keepUpToLength 8"+ | holds 1000 $ keep === keepUpToLength 9 = "keepUpToLength 9"+ | otherwise = "\\e -> ??"++expressionsT :: [Expr] -> [[Expr]]+expressionsT ds = [ds] \/ productMaybeWith ($$) es es `addWeight` 1+ where+ es = expressionsT ds+-- TODO: maybe use expressionsT as the main function to generate Exprs.+-- By using it, I speculate a 20% increase in runtime. But the code will+-- certainly be smaller and easier to maintain.
+ tests/test-expr.hs view
@@ -0,0 +1,190 @@+{-# LANGUAGE CPP #-}+-- Test library+import Test+import qualified Test.LeanCheck.Utils as LC (comparison)++-- Functions under test+import Test.Speculate.Expr+import Test.Speculate.Utils+import Data.List (sort)+import Data.Functor ((<$>)) -- for GHC < 7.10+import Data.Typeable (typeOf)+import Data.Maybe (isJust)++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+ [ True+ + , consts (xx -+- yy) == [plusE]+ , consts (xx -+- (yy -+- zz)) == [plusE]+ , consts (zero -+- one) =$ sort $= [zero, one, plusE]+ , consts ((zero -+- abs' zero) -+- (ord' aa -+- ord' cc))+ =$ sort $= [zero, aa, absE, plusE, ordE]+ , holds n $ \e1 e2 -> timesE `elem` consts (e1 -*- e2)+++ , arity zero == 0+ , arity xx == 0+ , arity absE == 1+ , arity plusE == 2+ , arity timesE == 2+++ , holds n $ okEqOrd -:> expr+ , holds n $ compare ==== compareComplexity+ , holds n $ LC.comparison lexicompare+ , holds n $ LC.comparison compareComplexity++ , holds n $ \(FunE e1) (FunE e2) e3 -> let cmp = lexicompare+ in typ e1 == typ e2 && isJust (e1 $$ e3) && isJust (e2 $$ e3)+ ==> e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)+ , holds n $ \(FunE e1) (FunE e2) e3 -> let cmp = lexicompareBy (flip compare)+ in typ e1 == typ e2 && isJust (e1 $$ e3) && isJust (e2 $$ e3)+ ==> e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)++ , holds n $ equivalence (eqExprCommuting [plusE])+ , holds n $ equivalence (eqExprCommuting [timesE])+ , holds n $ equivalence (eqExprCommuting [plusE,timesE])++ , xx -+- yy == xx -+- yy+ , xx -+- yy /= yy -+- xx+ , not $ eqExprCommuting [timesE] (xx -+- yy) (yy -+- xx)+ , eqExprCommuting [plusE] (xx -+- yy) (yy -+- xx)+ , eqExprCommuting [plusE] (zz -+- (xx -+- yy)) ((yy -+- xx) -+- zz)+ , eqExprCommuting [plusE,timesE] (zz -+- (xx -*- yy)) ((yy -*- xx) -+- zz)++ -- Holes < Values < Apps+ , xx < zero+ , zero < zero -+- one+ , xx < xx -+- yy+ , zero < xx -+- yy++ -- Less arity is less+ , zero < absE+ , absE < timesE+ , aa < ordE+ , ordE < timesE++ , unfoldApp (abs' xx) == [absE, xx]+ , unfoldApp (abs' (xx -+- yy)) == [absE, xx -+- yy]+ , unfoldApp (xx -+- abs' xx) == [plusE, xx, abs' xx]++ , holds n $ \e -> renameBy id e == e+ , holds n $ \e -> renameBy tail (renameBy ('x':) e) == e+ , renameBy (++ "1") (xx -+- yy) == (var "x1" int -+- var "y1" int)+ , renameBy (\(c:cs) -> succ c:cs) ((xx -+- yy) -+- ord' cc)+ == ((yy -+- zz) -+- ord' dd)++ , unification xx yy == Just [("y",xx),("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 xx)]+ , 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) (xx -+- zero))+ == Just (negate' (negate' xx) -+- zero)++ , canonicalize (xx -+- yy)+ == (xx -+- yy)+ , canonicalize (jj -+- (ii -+- ii))+ == (xx -+- (yy -+- yy))+ , canonicalize ((jj -+- ii) -+- (xx -+- xx))+ == ((xx -+- yy) -+- (zz -+- zz))++ , typ zero == typ one+ , typ zero == typ xx+ , typ zero == typ ii+ , typ xx /= typ cc+ , typ xx == typ (ord' cc)+ , holds n $ \(SameTypeE e1 e2) -> typ e1 == typ e2+ , holds n $ \(IntE e) -> typ e == typ i_+ , holds n $ \(BoolE e) -> typ e == typ b_+ , holds n $ \(CharE e) -> typ e == typ c_+ , holds n $ \(ListE e) -> typ e == typ xxs+ , etyp (xx :$ yy) == Left (i_ :$ i_)+ , etyp (xx :$ (cc :$ yy)) == Left (i_ :$ (c_ :$ i_))+ , etyp (ff xx :$ (ord' cc :$ gg yy)) == Left (i_ :$ (i_ :$ i_))+ , holds n $ \(SameTypeE ef eg) (SameTypeE ex ey) -> (etyp (ef :$ ex) == etyp (eg :$ ey))+ , holds n $ \ef eg ex ey -> (etyp ef == etyp eg && etyp ex == etyp ey)+ == (etyp (ef :$ ex) == etyp (eg :$ ey))+ , holds n $ \e -> case etyp e of+ Right t -> t == typ e+ Left _ -> error "Either Listable Expr is generating ill typed expressions or etyp is wrong!"++ , lengthE zero == 1+ , depthE zero == 1+ , lengthE one == 1+ , depthE one == 1+ , lengthE (zero -+- one) == 3+ , depthE (zero -+- one) == 2+ , lengthE (zero -+- (xx -+- yy)) == 5+ , depthE (zero -+- (xx -+- yy)) == 3+ , lengthE (((xx -+- yy) -*- zz) -==- ((xx -*- zz) -+- (yy -*- zz))) == 13+ , depthE (((xx -+- yy) -*- zz) -==- ((xx -*- zz) -+- (yy -*- zz))) == 4+ , depthE (xx -*- yy -+- xx -*- zz -==- xx -*- (yy -+- zz)) == 4+ , lengthE (xx -*- yy -+- xx -*- zz -==- xx -*- (yy -+- zz)) == 13+ , depthE (xx -*- yy -+- xx -*- zz) == 3+ , depthE (xx -*- (yy -+- zz)) == 3++ , allUnique (take (n`div`10) list :: [Expr])+ , allUnique (take (n`div`10) $ map unSameTypeE list)+ , allUnique (take (n`div`10) $ map unIntE list)++ , holds n $ \(IntE e) -> e `isInstanceOf` xx+ , holds n $ \(IntE e) -> abs' e `isInstanceOf` abs' xx+ , holds n $ \(IntE e) -> (e -+- e) `isInstanceOf` (xx -+- xx)+ , holds n $ \(IntE e1) (IntE e2) -> (e1 -+- e2) `isInstanceOf` (xx -+- yy)+ , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> not ((e1 -+- e2) `isInstanceOf` (xx -+- xx))+ , holds n $ \e -> e /= zero ==> not (e `isInstanceOf` zero)++ , (zero -+- one) `isInstanceOf` (xx -+- yy)+ , (zero -+- zero) `isInstanceOf` (xx -+- yy)+ , (yy -+- xx) `isInstanceOf` (xx -+- yy)+ , (zero -+- zero) `isInstanceOf` (xx -+- xx)+ , not $ (zero -+- one) `isInstanceOf` (xx -+- xx)+ , zero `isInstanceOf` xx+ , not $ xx `isInstanceOf` zero+ , (xx -+- (yy -+- xx)) `isInstanceOf` (xx -+- yy)+ , (xx -+- (xx -+- xx)) `isInstanceOf` (xx -+- yy)+ , not $ (xx -+- (xx -+- xx)) `isInstanceOf` (xx -+- xx)++ , vars (xx -+- yy) == [(intTy,"x"),(intTy,"y")]+ , vars (xx -+- xx) == [(intTy,"x")]+ , vars (xx -+- xx -+- yy) == [(intTy,"x"),(intTy,"y")]+ , vars (yy -+- xx -+- yy) == [(intTy,"x"),(intTy,"y")]++ , (xx -+- xx) < (xx -+- (xx -+- xx))+ , ((xx -+- xx) -+- xx) > (xx -+- (xx -+- xx))+ , xx < yy+ , zero < one+ , xx < zero++ -- If those two ever fail, it is because the instance for Ord TypeRep in+ -- Data.Typeable has changed. I do rely on this for a "nice" knuth-bendix+ -- order (by prefering less arity). If this ever changes, I will have to+ -- explicitly compare type arity on Ord Expr.+ -- (update: haha! It has changed from before, and twice!)+ -- TODO: fix order under GHC <= 7.8+#if __GLASGOW_HASKELL__ < 706+ , typeOf ((+) :: Int -> Int -> Int) > typeOf (abs :: Int -> Int)+ , typeOf (abs :: Int -> Int) < typeOf (0 :: Int)+#elif __GLASGOW_HASKELL__ < 800+ , typeOf ((+) :: Int -> Int -> Int) < typeOf (abs :: Int -> Int)+ , typeOf (abs :: Int -> Int) < typeOf (0 :: Int)+#else+ , typeOf ((+) :: Int -> Int -> Int) > typeOf (abs :: Int -> Int)+ , typeOf (abs :: Int -> Int) > typeOf (0 :: Int)+#endif++ , holds n $ \e1 e2 -> e1 `isSub` e2 == (e1 `elem` subexprsV e2)+ ]