code-conjure 0.5.4 → 0.5.6
raw patch · 28 files changed
+2299/−21 lines, 28 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Conjure.Engine: equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool
+ Conjure.Utils: classify :: Eq a => [a] -> [[a]]
+ Conjure.Utils: classifyBy :: (a -> a -> Bool) -> [a] -> [[a]]
+ Conjure.Utils: classifyOn :: Eq b => (a -> b) -> [a] -> [[a]]
+ Conjure.Utils: indent :: String -> String
+ Conjure.Utils: indentBy :: Int -> String -> String
Files
- .gitignore +1/−0
- Makefile +1/−0
- bench/redundants.hs +115/−0
- bench/redundants.out +2117/−0
- bench/runtime/zero/bench/candidates.runtime +1/−1
- bench/runtime/zero/bench/gps.runtime +1/−1
- bench/runtime/zero/bench/gps2.runtime +1/−1
- bench/runtime/zero/bench/redundants.runtime +1/−0
- bench/runtime/zero/bench/take-drop.runtime +1/−1
- bench/runtime/zero/bench/terpret.runtime +1/−1
- bench/runtime/zero/eg/bools.runtime +1/−1
- bench/runtime/zero/eg/bst.runtime +1/−1
- bench/runtime/zero/eg/factorial.runtime +1/−1
- bench/runtime/zero/eg/fib01.runtime +1/−1
- bench/runtime/zero/eg/fibonacci.runtime +1/−1
- bench/runtime/zero/eg/list.runtime +1/−1
- bench/runtime/zero/eg/pow.runtime +1/−1
- bench/runtime/zero/eg/replicate.runtime +1/−1
- bench/runtime/zero/eg/setelem.runtime +1/−1
- bench/runtime/zero/eg/sort.runtime +1/−1
- bench/runtime/zero/eg/spec.runtime +1/−1
- bench/runtime/zero/eg/tree.runtime +1/−1
- bench/runtime/zero/versions +1/−1
- changelog.md +9/−0
- code-conjure.cabal +2/−2
- mk/depend.mk +13/−0
- src/Conjure/Engine.hs +7/−1
- src/Conjure/Utils.hs +15/−0
.gitignore view
@@ -56,6 +56,7 @@ bench/p12 bench/p30 bench/candidates+bench/redundants bench/gps bench/gps2 bench/lowtests
Makefile view
@@ -31,6 +31,7 @@ eg/tree \ eg/bst \ bench/candidates \+ bench/redundants \ bench/ill-hit \ bench/longshot \ bench/lowtests \
+ bench/redundants.hs view
@@ -0,0 +1,115 @@+-- Print redundant candidates+--+-- Copyright (C) 2023 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++-- This script needs some internal utilities of Conjure:+import Conjure.Engine+import Conjure.Defn+import Conjure.Utils+++-- | This function prints redundant candidates.+--+-- The arguments are, in their respective order:+--+-- * maximum candidate size (5 = few seconds, 7 = few minutes);+-- * function name (for pretty-printing purposes);+-- * proxy value to indicate the type of functions to generate;+-- * list of primitives, in Conjure-compatible form.+printRedundantCandidates :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()+printRedundantCandidates n nm f ps = do+ putStrLn $ "Redundant candidates for: " ++ nm ++ " :: " ++ show (typeOf f)+ putStrLn $ " pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"+ putStrLn $ " " ++ show (map length css) ++ " candidates"+ putStrLn $ " " ++ show numUnique ++ "/" ++ show numCandidates ++ " unique candidates"+ putStrLn $ " " ++ show numRedundant ++ "/" ++ show numCandidates ++ " redundant candidates"+ putStrLn ""+ printThy thy+ putStrLn $ unlines . map showClass $ filter (\xs -> length xs > 1) $ classes+ where+ numCandidates = length candidates+ numUnique = length classes+ numRedundant = numCandidates - numUnique+ classes = classifyBy (equalModuloTesting maxTests maxEvalRecursions nm f) candidates+ candidates = concat css+ css = take n css'+ (css', thy) = candidateDefnsC args nm f ps -- Conjure uses this for listing candidates+ nRules = length (rules thy)+ nREs = length (equations thy) + nRules+ maxTests = 360 -- a hardcoded value probably will not hurt in this simple benchmark+ maxEvalRecursions = 60++ -- shows a class of candidates+ showClass :: [Defn] -> String+ showClass cs = unlines $ heading : map (indent . showDefn) cs+ where+ heading = "class of " ++ show (length cs) ++ " equivalent candidates:\n"+++main :: IO ()+main = do++ -- This N value limits the maximum size of candidates,+ -- increase it to print redundant candidates of bigger size.+ let n = 5+ -- With n = 5, this should run in a few seconds.+ -- With n = 7 and -O2 optimization,+ -- this should take a few minutes to run and generate a ~300K text file.+ -- We can also customize the n per-function below:++ printRedundantCandidates n "foo" (undefined :: Int -> Int)+ [ pr (0 :: Int)+ , pr (1 :: Int)+ , prim "+" ((+) :: Int -> Int -> Int)+ , prim "*" ((+) :: Int -> Int -> Int)+ , prim "-" ((-) :: Int -> Int -> Int)+ ]++ printRedundantCandidates n "?" (undefined :: Int -> Int -> Int)+ [ pr (0 :: Int)+ , prim "+" ((+) :: Int -> Int -> Int)+ , prim "*" ((+) :: Int -> Int -> Int)+ , prim "dec" (subtract 1 :: Int -> Int)+ ]++ printRedundantCandidates n "goo" (undefined :: [Int] -> [Int])+ [ pr ([] :: [Int])+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "++" ((++) :: [Int] -> [Int] -> [Int])+ ]++ printRedundantCandidates n "??" (undefined :: [Int] -> [Int] -> [Int])+ [ pr ([] :: [Int])+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "++" ((++) :: [Int] -> [Int] -> [Int])+ ]++ printRedundantCandidates n "ton" (undefined :: Bool -> Bool)+ [ pr False+ , pr True+ , prim "&&" (&&)+ , prim "||" (||)+ , prim "not" not+ ]++ printRedundantCandidates n "&|" (undefined :: Bool -> Bool -> Bool)+ [ pr False+ , pr True+ , prim "&&" (&&)+ , prim "||" (||)+ , prim "not" not+ ]++ -- Degenerate case:+ -- lots of redundancy, since 0 `mod` 0 = undefined+ -- Speculate is not able to discover that x `mod` x = 0+ -- nevertheless useful for observing candidate filtering+ -- through other means+ {-+ printRedundantCandidates n "gcd" (undefined :: Int -> Int -> Int)+ [ pr (0::Int)+ , prim "`mod`" (mod :: Int -> Int -> Int)+ ]+ -}
+ bench/redundants.out view
@@ -0,0 +1,2117 @@+Redundant candidates for: foo :: Int -> Int+ pruning with 15/35 rules+ [3,4,12,32,54] candidates+ 68/105 unique candidates+ 37/105 redundant candidates++rules:+x * y == x + y+x * y == y + x+x - x == 0+x + 0 == x+0 + x == x+x - 0 == x+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+x - (y - z) == z + (x - y)+(x - y) - z == x - (y + z)+(x - y) - z == x - (z + y)+(x + y) - z == x + (y - z)+(x + y) - z == y + (x - z)+x + (y - x) == y+(x - y) + y == x+equations:+y + x == x + y+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+y + (x - z) == x + (y - z)+(x - z) + y == x + (y - z)+(z - y) + x == (x - y) + z+y - (x + y) == 0 - x+y - (y + x) == 0 - x+z - (y + z) == x - (x + y)+z - (y + z) == x - (y + x)+z - (z + y) == x - (x + y)+z - (z + y) == x - (y + x)+x + (0 - y) == x - y+(0 - y) + x == x - y+x - (x + 1) == 0 - 1+x - (1 + x) == 0 - 1+y - (y + 1) == x - (x + 1)+y - (y + 1) == x - (1 + x)+y - (1 + y) == x - (1 + x)++class of 4 equivalent candidates:++ foo x = x++ foo 0 = 0+ foo x = x++ foo 1 = 1+ foo x = x++ foo 0 = 0+ foo 1 = 1+ foo x = x+++class of 2 equivalent candidates:++ foo 0 = 0+ foo x = 1++ foo 0 = 0+ foo 1 = 1+ foo x = 1+++class of 2 equivalent candidates:++ foo 0 = 1+ foo x = x++ foo 0 = 1+ foo 1 = 1+ foo x = x+++class of 2 equivalent candidates:++ foo 0 = 1+ foo x = 0++ foo 0 = 1+ foo 1 = 0+ foo x = 0+++class of 2 equivalent candidates:++ foo x = x + x++ foo 0 = 0+ foo x = x + x+++class of 4 equivalent candidates:++ foo x = x + 1++ foo x = 1 + x++ foo 0 = 1+ foo x = x + 1++ foo 0 = 1+ foo x = 1 + x+++class of 4 equivalent candidates:++ foo x = x - 1++ foo x = (0 - 1) + x++ foo x = x + (0 - 1)++ foo 1 = 0+ foo x = x - 1+++class of 5 equivalent candidates:++ foo x = 0 - x++ foo 0 = 0+ foo x = 0 - x++ foo x = x - (x + x)++ foo x = 1 - (x + 1)++ foo x = 1 - (1 + x)+++class of 4 equivalent candidates:++ foo x = 0 - 1++ foo x = x - (x + 1)++ foo x = x - (1 + x)++ foo x = 1 - (1 + 1)+++class of 5 equivalent candidates:++ foo x = 1 - x++ foo 0 = 1+ foo x = 1 - x++ foo x = (0 - x) + 1++ foo x = 1 + (0 - x)++ foo 1 = 0+ foo x = 1 - x+++class of 2 equivalent candidates:++ foo 1 = 0+ foo x = x++ foo 0 = 0+ foo 1 = 0+ foo x = x+++class of 2 equivalent candidates:++ foo 1 = 0+ foo x = 1++ foo 0 = 1+ foo 1 = 0+ foo x = 1+++class of 2 equivalent candidates:++ foo 1 = 1+ foo x = 0++ foo 0 = 0+ foo 1 = 1+ foo x = 0+++class of 2 equivalent candidates:++ foo 0 = 0+ foo x = x + 1++ foo 0 = 0+ foo x = 1 + x+++class of 2 equivalent candidates:++ foo x = (x - 1) + x++ foo x = x + (x - 1)+++class of 2 equivalent candidates:++ foo x = (1 - x) + 1++ foo x = 1 + (1 - x)+++class of 3 equivalent candidates:++ foo x = x + (x + 1)++ foo x = x + (1 + x)++ foo x = 1 + (x + x)+++class of 3 equivalent candidates:++ foo x = x + (1 + 1)++ foo x = 1 + (x + 1)++ foo x = 1 + (1 + x)+++class of 2 equivalent candidates:++ foo x = 0 - (x + 1)++ foo x = 0 - (1 + x)+++class of 2 equivalent candidates:++ foo 1 = 0+ foo x = x + 1++ foo 1 = 0+ foo x = 1 + x+++class of 2 equivalent candidates:++ foo 1 = 1+ foo x = x + 1++ foo 1 = 1+ foo x = 1 + x++++Redundant candidates for: ? :: Int -> Int -> Int+ pruning with 10/23 rules+ [3,10,40,116,338] candidates+ 363/507 unique candidates+ 144/507 redundant candidates++rules:+x * y == x + y+x * y == y + x+x + 0 == x+0 + x == x+dec (x + y) == x + dec y+dec (x + y) == y + dec x+dec (x + y) == dec x + y+dec (x + y) == dec y + x+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+equations:+y + x == x + y+y + dec x == x + dec y+dec x + y == x + dec y+dec y + x == dec x + y+x + dec 0 == dec x+dec 0 + x == dec x+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+y + dec (dec x) == x + dec (dec y)+dec (dec x) + y == x + dec (dec y)+x + dec (dec 0) == dec (dec x)+dec (dec 0) + x == dec (dec x)++class of 2 equivalent candidates:++ x ? y = x++ 0 ? x = 0+ x ? y = x+++class of 2 equivalent candidates:++ x ? y = y++ x ? 0 = 0+ x ? y = y+++class of 3 equivalent candidates:++ x ? y = 0++ x ? 0 = 0+ x ? y = dec x ? 0++ 0 ? x = 0+ x ? y = 0 ? dec y+++class of 4 equivalent candidates:++ x ? y = dec x++ x ? y = dec 0 + x++ x ? y = x + dec 0++ 0 ? x = dec 0+ x ? y = dec x+++class of 4 equivalent candidates:++ x ? y = dec y++ x ? y = dec 0 + y++ x ? y = y + dec 0++ x ? 0 = dec 0+ x ? y = dec y+++class of 2 equivalent candidates:++ x ? 0 = x+ x ? y = y++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = x+ x ? y = y+++class of 2 equivalent candidates:++ x ? 0 = x+ x ? y = 0++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = x+ x ? y = 0+++class of 2 equivalent candidates:++ x ? 0 = 0+ x ? y = x++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = 0+ x ? y = x+++class of 2 equivalent candidates:++ 0 ? x = x+ x ? y = 0++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = 0+ x ? y = 0+++class of 2 equivalent candidates:++ 0 ? x = 0+ x ? y = y++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = 0+ x ? y = y+++class of 2 equivalent candidates:++ x ? y = x + x++ 0 ? x = 0+ x ? y = x + x+++class of 8 equivalent candidates:++ x ? y = x + y++ x ? y = y + x++ x ? 0 = x+ x ? y = x + y++ x ? 0 = x+ x ? y = y + x++ 0 ? x = x+ x ? y = x + y++ 0 ? x = x+ x ? y = y + x++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = x+ x ? y = x + y++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = x+ x ? y = y + x+++class of 2 equivalent candidates:++ x ? y = y + y++ x ? 0 = 0+ x ? y = y + y+++class of 5 equivalent candidates:++ x ? y = dec (dec x)++ x ? y = dec (dec 0) + x++ x ? y = x + dec (dec 0)++ x ? y = dec x + dec 0++ x ? y = dec 0 + dec x+++class of 5 equivalent candidates:++ x ? y = dec (dec y)++ x ? y = dec (dec 0) + y++ x ? y = y + dec (dec 0)++ x ? y = dec y + dec 0++ x ? y = dec 0 + dec y+++class of 2 equivalent candidates:++ x ? y = dec (dec 0)++ x ? y = dec 0 + dec 0+++class of 5 equivalent candidates:++ x ? 0 = x+ x ? y = dec x++ x ? 0 = x+ x ? y = dec x ? 0++ x ? 0 = x+ x ? y = dec 0 + x++ x ? 0 = x+ x ? y = x + dec 0++ 0 ? 0 = 0+ 0 ? x = dec 0+ x ? 0 = x+ x ? y = dec x+++class of 4 equivalent candidates:++ x ? 0 = x+ x ? y = dec y++ x ? 0 = x+ x ? y = dec 0 + y++ x ? 0 = x+ x ? y = y + dec 0++ 0 ? 0 = 0+ 0 ? x = dec x+ x ? 0 = x+ x ? y = dec y+++class of 2 equivalent candidates:++ x ? 0 = x+ x ? y = dec 0++ 0 ? 0 = 0+ 0 ? x = dec 0+ x ? 0 = x+ x ? y = dec 0+++class of 4 equivalent candidates:++ x ? 0 = 0+ x ? y = dec x++ x ? 0 = 0+ x ? y = dec 0 + x++ x ? 0 = 0+ x ? y = x + dec 0++ 0 ? 0 = 0+ 0 ? x = dec 0+ x ? 0 = 0+ x ? y = dec x+++class of 3 equivalent candidates:++ x ? 0 = 0+ x ? y = dec y++ x ? 0 = 0+ x ? y = dec 0 + y++ x ? 0 = 0+ x ? y = y + dec 0+++class of 4 equivalent candidates:++ x ? 0 = dec x+ x ? y = x++ x ? 0 = dec 0 + x+ x ? y = x++ x ? 0 = x + dec 0+ x ? y = x++ 0 ? 0 = dec 0+ 0 ? x = 0+ x ? 0 = dec x+ x ? y = x+++class of 4 equivalent candidates:++ x ? 0 = dec x+ x ? y = y++ x ? 0 = dec 0 + x+ x ? y = y++ x ? 0 = x + dec 0+ x ? y = y++ 0 ? 0 = dec 0+ 0 ? x = x+ x ? 0 = dec x+ x ? y = y+++class of 4 equivalent candidates:++ x ? 0 = dec x+ x ? y = 0++ x ? 0 = dec 0 + x+ x ? y = 0++ x ? 0 = x + dec 0+ x ? y = 0++ 0 ? 0 = dec 0+ 0 ? x = 0+ x ? 0 = dec x+ x ? y = 0+++class of 2 equivalent candidates:++ x ? 0 = dec 0+ x ? y = x++ 0 ? 0 = dec 0+ 0 ? x = 0+ x ? 0 = dec 0+ x ? y = x+++class of 4 equivalent candidates:++ 0 ? x = x+ x ? y = dec x++ 0 ? x = x+ x ? y = dec 0 + x++ 0 ? x = x+ x ? y = x + dec 0++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = dec x+ x ? y = dec x+++class of 5 equivalent candidates:++ 0 ? x = x+ x ? y = dec y++ 0 ? x = x+ x ? y = 0 ? dec y++ 0 ? x = x+ x ? y = dec 0 + y++ 0 ? x = x+ x ? y = y + dec 0++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = dec 0+ x ? y = dec y+++class of 2 equivalent candidates:++ 0 ? x = x+ x ? y = dec 0++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = dec 0+ x ? y = dec 0+++class of 3 equivalent candidates:++ 0 ? x = 0+ x ? y = dec x++ 0 ? x = 0+ x ? y = dec 0 + x++ 0 ? x = 0+ x ? y = x + dec 0+++class of 4 equivalent candidates:++ 0 ? x = 0+ x ? y = dec y++ 0 ? x = 0+ x ? y = dec 0 + y++ 0 ? x = 0+ x ? y = y + dec 0++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = dec 0+ x ? y = dec y+++class of 4 equivalent candidates:++ 0 ? x = dec x+ x ? y = x++ 0 ? x = dec 0 + x+ x ? y = x++ 0 ? x = x + dec 0+ x ? y = x++ 0 ? 0 = dec 0+ 0 ? x = dec x+ x ? 0 = x+ x ? y = x+++class of 4 equivalent candidates:++ 0 ? x = dec x+ x ? y = y++ 0 ? x = dec 0 + x+ x ? y = y++ 0 ? x = x + dec 0+ x ? y = y++ 0 ? 0 = dec 0+ 0 ? x = dec x+ x ? 0 = 0+ x ? y = y+++class of 4 equivalent candidates:++ 0 ? x = dec x+ x ? y = 0++ 0 ? x = dec 0 + x+ x ? y = 0++ 0 ? x = x + dec 0+ x ? y = 0++ 0 ? 0 = dec 0+ 0 ? x = dec x+ x ? 0 = 0+ x ? y = 0+++class of 2 equivalent candidates:++ 0 ? x = dec 0+ x ? y = y++ 0 ? 0 = dec 0+ 0 ? x = dec 0+ x ? 0 = 0+ x ? y = y+++class of 2 equivalent candidates:++ x ? y = dec x + x++ x ? y = x + dec x+++class of 4 equivalent candidates:++ x ? y = dec x + y++ x ? y = dec y + x++ x ? y = x + dec y++ x ? y = y + dec x+++class of 2 equivalent candidates:++ x ? y = dec y + y++ x ? y = y + dec y+++class of 2 equivalent candidates:++ x ? 0 = x+ x ? y = x + x++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = x+ x ? y = x + x+++class of 2 equivalent candidates:++ x ? 0 = 0+ x ? y = x + x++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = 0+ x ? y = x + x+++class of 4 equivalent candidates:++ x ? 0 = 0+ x ? y = x + y++ x ? 0 = 0+ x ? y = y + x++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = 0+ x ? y = x + y++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = 0+ x ? y = y + x+++class of 2 equivalent candidates:++ x ? 0 = x + x+ x ? y = x++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = x + x+ x ? y = x+++class of 2 equivalent candidates:++ x ? 0 = x + x+ x ? y = y++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = x + x+ x ? y = y+++class of 2 equivalent candidates:++ x ? 0 = x + x+ x ? y = 0++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = x + x+ x ? y = 0+++class of 2 equivalent candidates:++ 0 ? x = x+ x ? y = y + y++ 0 ? 0 = 0+ 0 ? x = x+ x ? 0 = 0+ x ? y = y + y+++class of 4 equivalent candidates:++ 0 ? x = 0+ x ? y = x + y++ 0 ? x = 0+ x ? y = y + x++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = x+ x ? y = x + y++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = x+ x ? y = y + x+++class of 2 equivalent candidates:++ 0 ? x = 0+ x ? y = y + y++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = 0+ x ? y = y + y+++class of 2 equivalent candidates:++ 0 ? x = x + x+ x ? y = x++ 0 ? 0 = 0+ 0 ? x = x + x+ x ? 0 = x+ x ? y = x+++class of 2 equivalent candidates:++ 0 ? x = x + x+ x ? y = y++ 0 ? 0 = 0+ 0 ? x = x + x+ x ? 0 = 0+ x ? y = y+++class of 2 equivalent candidates:++ 0 ? x = x + x+ x ? y = 0++ 0 ? 0 = 0+ 0 ? x = x + x+ x ? 0 = 0+ x ? y = 0+++class of 3 equivalent candidates:++ x ? y = dec (dec x) + x++ x ? y = x + dec (dec x)++ x ? y = dec x + dec x+++class of 6 equivalent candidates:++ x ? y = dec (dec x) + y++ x ? y = dec (dec y) + x++ x ? y = x + dec (dec y)++ x ? y = y + dec (dec x)++ x ? y = dec x + dec y++ x ? y = dec y + dec x+++class of 3 equivalent candidates:++ x ? y = dec (dec y) + y++ x ? y = y + dec (dec y)++ x ? y = dec y + dec y+++class of 3 equivalent candidates:++ x ? y = x + (x + y)++ x ? y = x + (y + x)++ x ? y = y + (x + x)+++class of 3 equivalent candidates:++ x ? y = x + (y + y)++ x ? y = y + (x + y)++ x ? y = y + (y + x)+++class of 2 equivalent candidates:++ x ? 0 = x+ x ? y = dec x + x++ x ? 0 = x+ x ? y = x + dec x+++class of 4 equivalent candidates:++ x ? 0 = x+ x ? y = dec x + y++ x ? 0 = x+ x ? y = dec y + x++ x ? 0 = x+ x ? y = x + dec y++ x ? 0 = x+ x ? y = y + dec x+++class of 2 equivalent candidates:++ x ? 0 = x+ x ? y = dec y + y++ x ? 0 = x+ x ? y = y + dec y+++class of 2 equivalent candidates:++ x ? 0 = 0+ x ? y = dec x + x++ x ? 0 = 0+ x ? y = x + dec x+++class of 4 equivalent candidates:++ x ? 0 = 0+ x ? y = dec x + y++ x ? 0 = 0+ x ? y = dec y + x++ x ? 0 = 0+ x ? y = x + dec y++ x ? 0 = 0+ x ? y = y + dec x+++class of 2 equivalent candidates:++ x ? 0 = 0+ x ? y = dec y + y++ x ? 0 = 0+ x ? y = y + dec y+++class of 2 equivalent candidates:++ x ? 0 = dec x+ x ? y = x + y++ x ? 0 = dec x+ x ? y = y + x+++class of 2 equivalent candidates:++ x ? 0 = dec 0+ x ? y = x + y++ x ? 0 = dec 0+ x ? y = y + x+++class of 2 equivalent candidates:++ x ? 0 = dec x + x+ x ? y = x++ x ? 0 = x + dec x+ x ? y = x+++class of 2 equivalent candidates:++ x ? 0 = dec x + x+ x ? y = y++ x ? 0 = x + dec x+ x ? y = y+++class of 2 equivalent candidates:++ x ? 0 = dec x + x+ x ? y = 0++ x ? 0 = x + dec x+ x ? y = 0+++class of 2 equivalent candidates:++ 0 ? x = x+ x ? y = dec x + x++ 0 ? x = x+ x ? y = x + dec x+++class of 4 equivalent candidates:++ 0 ? x = x+ x ? y = dec x + y++ 0 ? x = x+ x ? y = dec y + x++ 0 ? x = x+ x ? y = x + dec y++ 0 ? x = x+ x ? y = y + dec x+++class of 2 equivalent candidates:++ 0 ? x = x+ x ? y = dec y + y++ 0 ? x = x+ x ? y = y + dec y+++class of 2 equivalent candidates:++ 0 ? x = 0+ x ? y = dec x + x++ 0 ? x = 0+ x ? y = x + dec x+++class of 4 equivalent candidates:++ 0 ? x = 0+ x ? y = dec x + y++ 0 ? x = 0+ x ? y = dec y + x++ 0 ? x = 0+ x ? y = x + dec y++ 0 ? x = 0+ x ? y = y + dec x+++class of 2 equivalent candidates:++ 0 ? x = 0+ x ? y = dec y + y++ 0 ? x = 0+ x ? y = y + dec y+++class of 2 equivalent candidates:++ 0 ? x = dec x+ x ? y = x + y++ 0 ? x = dec x+ x ? y = y + x+++class of 2 equivalent candidates:++ 0 ? x = dec 0+ x ? y = x + y++ 0 ? x = dec 0+ x ? y = y + x+++class of 2 equivalent candidates:++ 0 ? x = dec x + x+ x ? y = x++ 0 ? x = x + dec x+ x ? y = x+++class of 2 equivalent candidates:++ 0 ? x = dec x + x+ x ? y = y++ 0 ? x = x + dec x+ x ? y = y+++class of 2 equivalent candidates:++ 0 ? x = dec x + x+ x ? y = 0++ 0 ? x = x + dec x+ x ? y = 0+++class of 2 equivalent candidates:++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = 0+ x ? y = x + y++ 0 ? 0 = 0+ 0 ? x = 0+ x ? 0 = 0+ x ? y = y + x++++Redundant candidates for: goo :: [Int] -> [Int]+ pruning with 4/4 rules+ [2,1,2,3,4] candidates+ 9/12 unique candidates+ 3/12 redundant candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++class of 3 equivalent candidates:++ goo xs = xs++ goo [] = []+ goo (x:xs) = x:xs++ goo [] = []+ goo (x:xs) = x:goo xs+++class of 2 equivalent candidates:++ goo xs = []++ goo [] = []+ goo (x:xs) = goo xs++++Redundant candidates for: ?? :: [Int] -> [Int] -> [Int]+ pruning with 4/4 rules+ [3,7,13,66,152] candidates+ 161/241 unique candidates+ 80/241 redundant candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++class of 4 equivalent candidates:++ xs ?? ys = xs++ xs ?? [] = xs+ xs ?? (x:ys) = xs ?? ys++ xs ?? [] = xs+ xs ?? (x:ys) = xs ?? []++ [] ?? xs = []+ (x:xs) ?? ys = x:xs+++class of 4 equivalent candidates:++ xs ?? ys = ys++ [] ?? xs = xs+ (x:xs) ?? ys = xs ?? ys++ [] ?? xs = xs+ (x:xs) ?? ys = [] ?? ys++ xs ?? [] = []+ xs ?? (x:ys) = x:ys+++class of 29 equivalent candidates:++ xs ?? ys = []++ xs ?? [] = []+ xs ?? (x:ys) = xs ?? ys++ xs ?? [] = []+ xs ?? (x:ys) = xs ?? []++ xs ?? [] = []+ xs ?? (x:ys) = ys ?? xs++ xs ?? [] = []+ xs ?? (x:ys) = ys ?? ys++ xs ?? [] = []+ xs ?? (x:ys) = ys ?? []++ xs ?? [] = []+ xs ?? (x:ys) = [] ?? xs++ xs ?? [] = []+ xs ?? (x:ys) = [] ?? ys++ [] ?? xs = []+ (x:xs) ?? ys = xs ?? xs++ [] ?? xs = []+ (x:xs) ?? ys = xs ?? ys++ [] ?? xs = []+ (x:xs) ?? ys = xs ?? []++ [] ?? xs = []+ (x:xs) ?? ys = ys ?? xs++ [] ?? xs = []+ (x:xs) ?? ys = ys ?? []++ [] ?? xs = []+ (x:xs) ?? ys = [] ?? xs++ [] ?? xs = []+ (x:xs) ?? ys = [] ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = [] ?? xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs ?? xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs ?? []+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = [] ?? xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs ?? []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys ?? []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = [] ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = [] ?? ys+++class of 3 equivalent candidates:++ xs ?? [] = xs+ xs ?? (x:ys) = ys++ xs ?? [] = xs+ xs ?? (x:ys) = ys ?? []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = x:xs+ (x:xs) ?? (y:ys) = ys+++class of 5 equivalent candidates:++ xs ?? [] = xs+ xs ?? (x:ys) = []++ xs ?? [] = xs+ xs ?? (x:ys) = ys ?? ys++ xs ?? [] = xs+ xs ?? (x:ys) = [] ?? xs++ xs ?? [] = xs+ xs ?? (x:ys) = [] ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = x:xs+ (x:xs) ?? (y:ys) = []+++class of 2 equivalent candidates:++ xs ?? [] = []+ xs ?? (x:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = x:xs+++class of 2 equivalent candidates:++ xs ?? [] = []+ xs ?? (x:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs ?? []+ (x:xs) ?? (y:ys) = ys+++class of 5 equivalent candidates:++ [] ?? xs = xs+ (x:xs) ?? ys = []++ [] ?? xs = xs+ (x:xs) ?? ys = xs ?? xs++ [] ?? xs = xs+ (x:xs) ?? ys = xs ?? []++ [] ?? xs = xs+ (x:xs) ?? ys = ys ?? []++ [] ?? [] = []+ [] ?? (x:xs) = x:xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = []+++class of 2 equivalent candidates:++ [] ?? xs = []+ (x:xs) ?? ys = xs++ [] ?? [] = []+ [] ?? (x:xs) = [] ?? xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs+++class of 2 equivalent candidates:++ [] ?? xs = []+ (x:xs) ?? ys = ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = y:ys+++class of 3 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys ?? ys+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs ?? []+ (x:xs) ?? (y:ys) = xs+++class of 7 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs ?? xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs ?? []+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs ?? []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys ?? []+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = [] ?? xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys+++class of 7 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = [] ?? xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = []++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = [] ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = [] ?? ys+++class of 5 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = [] ?? xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs ?? []+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = [] ?? xs+ (x:xs) ?? (y:ys) = xs+++class of 5 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? []+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = [] ?? xs+ (x:xs) ?? [] = []+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = xs ?? []+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = []+ (x:xs) ?? [] = [] ?? xs+ (x:xs) ?? (y:ys) = ys+++class of 2 equivalent candidates:++ [] ?? xs = xs+ (x:xs) ?? ys = [] ?? xs++ [] ?? [] = []+ [] ?? (x:xs) = x:xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs ?? ys++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys ?? xs+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs ?? []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = [] ?? xs+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys ?? []++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = [] ?? ys+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs ?? xs+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = [] ?? xs+ (x:xs) ?? (y:ys) = xs+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = xs ?? xs+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = xs+ (x:xs) ?? [] = [] ?? xs+ (x:xs) ?? (y:ys) = ys+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = xs+++class of 2 equivalent candidates:++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? xs+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys++ [] ?? [] = []+ [] ?? (x:xs) = xs ?? []+ (x:xs) ?? [] = xs+ (x:xs) ?? (y:ys) = ys++++Redundant candidates for: ton :: Bool -> Bool+ pruning with 39/49 rules+ [3,3,0,0,0] candidates+ 4/6 unique candidates+ 2/6 redundant candidates++rules:+not False == True+not True == False+p && p == p+p || p == p+not (not p) == p+p && False == False+p && True == p+False && p == False+True && p == p+p || False == p+p || True == True+False || p == p+True || p == True+not (p && q) == not p || not q+not (p && q) == not q || not p+not (p || q) == not p && not q+not (p || q) == not q && not p+p && not p == False+not p && p == False+p || not p == True+not p || p == True+(p && q) && r == p && (q && r)+(p && q) && r == q && (p && r)+(p || q) || r == p || (q || r)+(p || q) || r == q || (p || r)+p && (p && q) == p && q+p && (q && p) == p && q+p && (q && p) == q && p+p || (p || q) == p || q+p || (q || p) == p || q+p || (q || p) == q || p+p && (p || q) == p+p && (q || p) == p+(p || q) && p == p+(p || q) && q == q+p || p && q == p+p || q && p == p+p && q || p == p+p && q || q == q+equations:+q && p == p && q+q || p == p || q+q && (p && r) == p && (q && r)+r && (p && q) == p && (q && r)+r && (q && p) == p && (q && r)+q || (p || r) == p || (q || r)+r || (p || q) == p || (q || r)+r || (q || p) == p || (q || r)+(r || q) && p == p && (q || r)+r && q || p == p || q && r++class of 2 equivalent candidates:++ ton p = p++ ton False = False+ ton True = True+++class of 2 equivalent candidates:++ ton p = not p++ ton False = True+ ton True = False++++Redundant candidates for: &| :: Bool -> Bool -> Bool+ pruning with 39/49 rules+ [4,14,26,8,4] candidates+ 16/56 unique candidates+ 40/56 redundant candidates++rules:+not False == True+not True == False+p && p == p+p || p == p+not (not p) == p+p && False == False+p && True == p+False && p == False+True && p == p+p || False == p+p || True == True+False || p == p+True || p == True+not (p && q) == not p || not q+not (p && q) == not q || not p+not (p || q) == not p && not q+not (p || q) == not q && not p+p && not p == False+not p && p == False+p || not p == True+not p || p == True+(p && q) && r == p && (q && r)+(p && q) && r == q && (p && r)+(p || q) || r == p || (q || r)+(p || q) || r == q || (p || r)+p && (p && q) == p && q+p && (q && p) == p && q+p && (q && p) == q && p+p || (p || q) == p || q+p || (q || p) == p || q+p || (q || p) == q || p+p && (p || q) == p+p && (q || p) == p+(p || q) && p == p+(p || q) && q == q+p || p && q == p+p || q && p == p+p && q || p == p+p && q || q == q+equations:+q && p == p && q+q || p == p || q+q && (p && r) == p && (q && r)+r && (p && q) == p && (q && r)+r && (q && p) == p && (q && r)+q || (p || r) == p || (q || r)+r || (p || q) == p || (q || r)+r || (q || p) == p || (q || r)+(r || q) && p == p && (q || r)+r && q || p == p || q && r++class of 2 equivalent candidates:++ p &| q = p++ False &| p = False+ True &| p = True+++class of 2 equivalent candidates:++ p &| q = q++ p &| False = False+ p &| True = True+++class of 2 equivalent candidates:++ p &| q = not p++ False &| p = True+ True &| p = False+++class of 2 equivalent candidates:++ p &| q = not q++ p &| False = True+ p &| True = False+++class of 5 equivalent candidates:++ p &| False = p+ p &| True = False++ False &| p = False+ True &| p = not p++ False &| False = False+ False &| True = False+ True &| False = True+ True &| True = False++ p &| q = not q && p++ p &| q = p && not q+++class of 5 equivalent candidates:++ p &| False = p+ p &| True = True++ False &| p = p+ True &| p = True++ p &| q = p || q++ p &| q = q || p++ False &| False = False+ False &| True = True+ True &| False = True+ True &| True = True+++class of 5 equivalent candidates:++ p &| False = False+ p &| True = p++ False &| p = False+ True &| p = p++ p &| q = p && q++ p &| q = q && p++ False &| False = False+ False &| True = False+ True &| False = False+ True &| True = True+++class of 5 equivalent candidates:++ p &| False = True+ p &| True = p++ False &| p = not p+ True &| p = True++ False &| False = True+ False &| True = False+ True &| False = True+ True &| True = True++ p &| q = not q || p++ p &| q = p || not q+++class of 5 equivalent candidates:++ False &| p = p+ True &| p = False++ p &| False = False+ p &| True = not p++ False &| False = False+ False &| True = True+ True &| False = False+ True &| True = False++ p &| q = not p && q++ p &| q = q && not p+++class of 5 equivalent candidates:++ False &| p = True+ True &| p = p++ p &| False = not p+ p &| True = True++ False &| False = True+ False &| True = True+ True &| False = False+ True &| True = True++ p &| q = not p || q++ p &| q = q || not p+++class of 3 equivalent candidates:++ p &| False = p+ p &| True = not p++ False &| p = p+ True &| p = not p++ False &| False = False+ False &| True = True+ True &| False = True+ True &| True = False+++class of 5 equivalent candidates:++ p &| False = True+ p &| True = not p++ False &| p = True+ True &| p = not p++ False &| False = True+ False &| True = True+ True &| False = True+ True &| True = False++ p &| q = not p || not q++ p &| q = not q || not p+++class of 3 equivalent candidates:++ p &| False = not p+ p &| True = p++ False &| p = not p+ True &| p = p++ False &| False = True+ False &| True = False+ True &| False = False+ True &| True = True+++class of 5 equivalent candidates:++ p &| False = not p+ p &| True = False++ False &| p = not p+ True &| p = False++ False &| False = True+ False &| True = False+ True &| False = False+ True &| True = False++ p &| q = not p && not q++ p &| q = not q && not p+++
bench/runtime/zero/bench/candidates.runtime view
@@ -1,1 +1,1 @@-11.0+10.9
bench/runtime/zero/bench/gps.runtime view
@@ -1,1 +1,1 @@-23.2+26.2
bench/runtime/zero/bench/gps2.runtime view
@@ -1,1 +1,1 @@-9.0+9.3
+ bench/runtime/zero/bench/redundants.runtime view
@@ -0,0 +1,1 @@+3.7
bench/runtime/zero/bench/take-drop.runtime view
@@ -1,1 +1,1 @@-0.5+0.6
bench/runtime/zero/bench/terpret.runtime view
@@ -1,1 +1,1 @@-12.4+12.0
bench/runtime/zero/eg/bools.runtime view
@@ -1,1 +1,1 @@-3.2+3.1
bench/runtime/zero/eg/bst.runtime view
@@ -1,1 +1,1 @@-6.5+6.6
bench/runtime/zero/eg/factorial.runtime view
@@ -1,1 +1,1 @@-2.5+2.4
bench/runtime/zero/eg/fib01.runtime view
@@ -1,1 +1,1 @@-4.5+5.7
bench/runtime/zero/eg/fibonacci.runtime view
@@ -1,1 +1,1 @@-4.6+4.7
bench/runtime/zero/eg/list.runtime view
@@ -1,1 +1,1 @@-1.3+1.2
bench/runtime/zero/eg/pow.runtime view
@@ -1,1 +1,1 @@-3.9+3.7
bench/runtime/zero/eg/replicate.runtime view
@@ -1,1 +1,1 @@-0.5+0.4
bench/runtime/zero/eg/setelem.runtime view
@@ -1,1 +1,1 @@-2.0+1.9
bench/runtime/zero/eg/sort.runtime view
@@ -1,1 +1,1 @@-1.0+1.2
bench/runtime/zero/eg/spec.runtime view
@@ -1,1 +1,1 @@-1.1+1.0
bench/runtime/zero/eg/tree.runtime view
@@ -1,1 +1,1 @@-2.0+1.9
bench/runtime/zero/versions view
@@ -1,4 +1,4 @@ GHC 9.0.2 leancheck-1.0.0-express-1.0.10+express-1.0.12 speculate-0.4.14
changelog.md view
@@ -2,6 +2,15 @@ ============================ +v0.5.6+------++* `Conjure` module: no main API changes+* `Conjure.Engine`: add `equalModuloTesting`+* `Conjure.Utils`: add some misc functions+* add `bench/redundants` that reports groups of redundant candidates++ v0.5.4 ------
code-conjure.cabal view
@@ -3,7 +3,7 @@ -- Copyright (C) 2021 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name: code-conjure-version: 0.5.4+version: 0.5.6 synopsis: synthesize Haskell functions out of partial definitions description: Conjure is a tool that synthesizes Haskell functions out of partial definitions.@@ -60,7 +60,7 @@ source-repository this type: git location: https://github.com/rudymatela/conjure- tag: v0.5.4+ tag: v0.5.6 library exposed-modules: Conjure
mk/depend.mk view
@@ -107,6 +107,19 @@ src/Conjure/Conjurable.hs \ src/Conjure/Conjurable/Derive.hs \ bench/p30.hs+bench/redundants: \+ bench/redundants.hs \+ mk/toplibs+bench/redundants.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Prim.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Defn.hs \+ src/Conjure/Conjurable.hs \+ src/Conjure/Conjurable/Derive.hs \+ bench/redundants.hs bench/self: \ bench/self.hs \ mk/toplibs
src/Conjure/Engine.hs view
@@ -31,6 +31,7 @@ , candidateDefnsC , conjureTheory , conjureTheoryWith+ , equalModuloTesting , module Data.Express , module Data.Express.Fixtures , module Test.Speculate.Engine@@ -336,7 +337,12 @@ nubCandidates :: Conjurable f => Args -> String -> f -> [[Defn]] -> [[Defn]]-nubCandidates Args{..} nm f = discardLaterT (===)+nubCandidates Args{..} nm f =+ discardLaterT $ equalModuloTesting maxTests maxEvalRecursions nm f+++equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool+equalModuloTesting maxTests maxEvalRecursions nm f = (===) where err = error "nubCandidates: unexpected evaluation error." eq = conjureDynamicEq f
src/Conjure/Utils.hs view
@@ -32,6 +32,11 @@ , choices , choicesThat , foldr0+ , indent+ , indentBy+ , classify -- from LeanCheck.Stats+ , classifyBy -- from LeanCheck.Stats+ , classifyOn -- from LeanCheck.Stats ) where @@ -44,6 +49,8 @@ import System.IO.Unsafe +import Test.LeanCheck.Stats (classify, classifyBy, classifyOn)+ -- | Checks if all elements of a list are equal. -- -- Exceptionally this function returns false for an empty or unit list.@@ -134,3 +141,11 @@ foldr0 :: (a -> a -> a) -> a -> [a] -> a foldr0 f z xs | null xs = z | otherwise = foldr1 f xs++-- | Indents a block of text by 4 spaces+indent :: String -> String+indent = indentBy 4++-- | Indents a block of text with the provided amount of spaces+indentBy :: Int -> String -> String+indentBy n = unlines . map (replicate n ' ' ++) . lines