diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/TODO.md b/TODO.md new file mode 100644 --- /dev/null +++ b/TODO.md @@ -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` diff --git a/eg/plus-abs.hs b/eg/plus-abs.hs new file mode 100644 --- /dev/null +++ b/eg/plus-abs.hs @@ -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) + ] + } diff --git a/speculate.cabal b/speculate.cabal new file mode 100644 --- /dev/null +++ b/speculate.cabal @@ -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 +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 diff --git a/src/Test/Speculate.hs b/src/Test/Speculate.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate.hs @@ -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 diff --git a/src/Test/Speculate/Args.hs b/src/Test/Speculate/Args.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Args.hs @@ -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 + diff --git a/src/Test/Speculate/CondReason.hs b/src/Test/Speculate/CondReason.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/CondReason.hs @@ -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 diff --git a/src/Test/Speculate/Engine.hs b/src/Test/Speculate/Engine.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Engine.hs @@ -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 diff --git a/src/Test/Speculate/Expr.hs b/src/Test/Speculate/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr.hs @@ -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 diff --git a/src/Test/Speculate/Expr/Canon.hs b/src/Test/Speculate/Expr/Canon.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr/Canon.hs @@ -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 diff --git a/src/Test/Speculate/Expr/Core.hs b/src/Test/Speculate/Expr/Core.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr/Core.hs @@ -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] diff --git a/src/Test/Speculate/Expr/Equate.hs b/src/Test/Speculate/Expr/Equate.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr/Equate.hs @@ -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 diff --git a/src/Test/Speculate/Expr/Ground.hs b/src/Test/Speculate/Expr/Ground.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr/Ground.hs @@ -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 diff --git a/src/Test/Speculate/Expr/Match.hs b/src/Test/Speculate/Expr/Match.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr/Match.hs @@ -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 diff --git a/src/Test/Speculate/Expr/TypeInfo.hs b/src/Test/Speculate/Expr/TypeInfo.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Expr/TypeInfo.hs @@ -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" diff --git a/src/Test/Speculate/Misc.hs b/src/Test/Speculate/Misc.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Misc.hs @@ -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 + diff --git a/src/Test/Speculate/Reason.hs b/src/Test/Speculate/Reason.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Reason.hs @@ -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 diff --git a/src/Test/Speculate/Reason/Order.hs b/src/Test/Speculate/Reason/Order.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Reason/Order.hs @@ -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) diff --git a/src/Test/Speculate/Report.hs b/src/Test/Speculate/Report.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Report.hs @@ -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 diff --git a/src/Test/Speculate/Sanity.hs b/src/Test/Speculate/Sanity.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Sanity.hs @@ -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 diff --git a/src/Test/Speculate/SemiReason.hs b/src/Test/Speculate/SemiReason.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/SemiReason.hs @@ -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!" diff --git a/src/Test/Speculate/Utils.hs b/src/Test/Speculate/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils.hs @@ -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 diff --git a/src/Test/Speculate/Utils/Class.hs b/src/Test/Speculate/Utils/Class.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Class.hs @@ -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) diff --git a/src/Test/Speculate/Utils/Colour.hs b/src/Test/Speculate/Utils/Colour.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Colour.hs @@ -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 diff --git a/src/Test/Speculate/Utils/Digraph.hs b/src/Test/Speculate/Utils/Digraph.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Digraph.hs @@ -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) diff --git a/src/Test/Speculate/Utils/List.hs b/src/Test/Speculate/Utils/List.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/List.hs @@ -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." diff --git a/src/Test/Speculate/Utils/Memoize.hs b/src/Test/Speculate/Utils/Memoize.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Memoize.hs @@ -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) diff --git a/src/Test/Speculate/Utils/Misc.hs b/src/Test/Speculate/Utils/Misc.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Misc.hs @@ -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 +(..:) = (.) . (.:) diff --git a/src/Test/Speculate/Utils/Ord.hs b/src/Test/Speculate/Utils/Ord.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Ord.hs @@ -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 diff --git a/src/Test/Speculate/Utils/PrettyPrint.hs b/src/Test/Speculate/Utils/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/PrettyPrint.hs @@ -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 diff --git a/src/Test/Speculate/Utils/String.hs b/src/Test/Speculate/Utils/String.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/String.hs @@ -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) diff --git a/src/Test/Speculate/Utils/Tiers.hs b/src/Test/Speculate/Utils/Tiers.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Tiers.hs @@ -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)) diff --git a/src/Test/Speculate/Utils/Timeout.hs b/src/Test/Speculate/Utils/Timeout.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Timeout.hs @@ -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") diff --git a/src/Test/Speculate/Utils/Tuple.hs b/src/Test/Speculate/Utils/Tuple.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Tuple.hs @@ -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 diff --git a/src/Test/Speculate/Utils/Typeable.hs b/src/Test/Speculate/Utils/Typeable.hs new file mode 100644 --- /dev/null +++ b/src/Test/Speculate/Utils/Typeable.hs @@ -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) diff --git a/tests/Test.hs b/tests/Test.hs new file mode 100644 --- /dev/null +++ b/tests/Test.hs @@ -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. diff --git a/tests/test-expr.hs b/tests/test-expr.hs new file mode 100644 --- /dev/null +++ b/tests/test-expr.hs @@ -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) + ]