code-conjure 0.5.12 → 0.5.14

raw patch · 57 files changed

+2880/−115 lines, 57 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• .gitignore +3/−0
• Makefile +7/−1
• bench/candidates.txt +6/−6
• bench/carry-on.hs +33/−0
• bench/carry-on.txt +47/−0
• bench/erroneous.txt +2/−2
• bench/gps.txt +17/−17
• bench/gps2.txt +5/−5
• bench/runtime/lapmatrud/bench/candidates.runtime +1/−1
• bench/runtime/lapmatrud/bench/carry-on.runtime +1/−0
• bench/runtime/lapmatrud/bench/erroneous.runtime +1/−1
• bench/runtime/lapmatrud/bench/gps.runtime +1/−1
• bench/runtime/lapmatrud/bench/gps2.runtime +1/−1
• bench/runtime/lapmatrud/bench/p12.runtime +1/−1
• bench/runtime/lapmatrud/bench/redundants.runtime +1/−1
• bench/runtime/lapmatrud/bench/strategies.runtime +1/−0
• bench/runtime/lapmatrud/bench/terpret.runtime +1/−1
• bench/runtime/lapmatrud/bench/unique.runtime +1/−0
• bench/runtime/lapmatrud/bench/weird.runtime +1/−1
• bench/runtime/lapmatrud/eg/arith.runtime +1/−1
• bench/runtime/lapmatrud/eg/bools.runtime +1/−1
• bench/runtime/lapmatrud/eg/bst.runtime +1/−1
• bench/runtime/lapmatrud/eg/fib01.runtime +1/−1
• bench/runtime/lapmatrud/eg/fibonacci.runtime +1/−1
• bench/runtime/lapmatrud/eg/higher.runtime +1/−1
• bench/runtime/lapmatrud/eg/ints.runtime +1/−1
• bench/runtime/lapmatrud/eg/list.runtime +1/−1
• bench/runtime/lapmatrud/eg/oddeven.runtime +1/−1
• bench/runtime/lapmatrud/eg/pow.runtime +1/−1
• bench/runtime/lapmatrud/eg/setelem.runtime +1/−1
• bench/runtime/lapmatrud/eg/sort.runtime +1/−1
• bench/runtime/lapmatrud/eg/tree.runtime +1/−1
• bench/runtime/lapmatrud/versions +1/−1
• bench/runtime/zero/bench/carry-on.runtime +1/−0
• bench/runtime/zero/bench/strategies.runtime +1/−0
• bench/runtime/zero/bench/unique.runtime +1/−0
• bench/strategies.hs +72/−0
• bench/strategies.txt +135/−0
• bench/terpret.txt +2/−2
• bench/unique.hs +107/−0
• bench/unique.txt +2276/−0
• bench/weird.txt +5/−5
• changelog.md +9/−0
• code-conjure.cabal +2/−2
• eg/bst.txt +1/−1
• eg/factorial.txt +1/−1
• eg/fib01.txt +5/−5
• eg/fibonacci.txt +9/−9
• eg/list.txt +3/−3
• eg/oddeven.txt +4/−4
• eg/pow.txt +3/−3
• eg/sort.hs +1/−0
• eg/tree.txt +5/−5
• mk/depend.mk +51/−0
• src/Conjure/Defn/Redundancy.hs +1/−6
• src/Conjure/Engine.hs +39/−12
• src/Conjure/Reason.hs +1/−4

@@ -53,6 +53,8 @@ eg/sort eg/subset eg/spec+bench/carry-on+bench/strategies bench/self bench/longshot bench/ill-hit@@ -67,6 +69,7 @@ bench/lowtests bench/terpret bench/weird+bench/unique proto/u-conjure test/expr test/conjurable

@@ -44,13 +44,16 @@   bench/ill-hit \   bench/longshot \   bench/lowtests \+  bench/strategies \   bench/self \+  bench/carry-on \   bench/take-drop \   bench/p12 \   bench/p30 \   bench/gps \   bench/gps2 \   bench/terpret \+  bench/unique \   bench/weird \   proto/u-conjure @@ -128,7 +131,10 @@ 	./$<  %.txt: %-	./$< >$<.txt+	./$< >$@++%.tee: %+	$(LONG) unbuffer ./$< | tee $<.txt  %.diff: % 	./$< | diff -rud $<.txt -

@@ -1,7 +1,7 @@ Candidates for: foo :: Int -> Int   pruning with 27/65 rules-  [3,0,8,0,30,0,194,0,1406] direct candidates, 0 duplicates-  [3,3,9,10,32,39,197,247,1325] pattern candidates, 0 duplicates+  [3,0,8,0,30,0,177,0,1203] direct candidates, 0 duplicates+  [3,3,9,10,32,39,185,233,1169] pattern candidates, 0 duplicates  rules: x - x == 0@@ -430,8 +430,8 @@  Candidates for: ? :: Int -> Int -> Int   pruning with 13/34 rules-  [3,3,9,18,60,162,516,1587,5148] direct candidates, 0 duplicates-  [3,8,25,71,205,632,1976,6067,19140] pattern candidates, 0 duplicates+  [3,3,9,18,60,162,489,1475,4619] direct candidates, 0 duplicates+  [3,8,25,71,205,632,1957,5906,18303] pattern candidates, 0 duplicates  rules: x * 0 == 0@@ -3394,8 +3394,8 @@  Candidates for: &| :: Bool -> Bool -> Bool   pruning with 39/49 rules-  [4,2,2,4,2,16,18,60,120] direct candidates, 0 duplicates-  [4,14,26,10,2,16,18,60,120] pattern candidates, 0 duplicates+  [4,2,2,4,2,16,17,56,110] direct candidates, 0 duplicates+  [4,14,26,10,2,16,17,56,110] pattern candidates, 0 duplicates  rules: not False == True

@@ -0,0 +1,33 @@+-- carryon.hs: conjuring implementations of a factorial function+--+-- Copyright (C) 2021-2024 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++factorial :: Int -> Int+factorial 1  =  1+factorial 2  =  2+factorial 3  =  6+factorial 4  =  24+++main :: IO ()+main  =  do+  -- carry on Conjuring larger implementations+  conjureWith args{carryOn = True, maxSize = 11} "factorial n" factorial+    [ pr (0::Int)+    , pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "-" ((-) :: Int -> Int -> Int)+    ]+  -- should produce:+  -- factorial 0  =  1+  -- factorial x  =  x * factorial (x - 1)+  --+  -- and+  -- factorial 0  =  1+  -- factorial 1  =  1+  -- factorial x  =  x * factorial (x - 1)+  --+  -- among other implementations

@@ -0,0 +1,47 @@+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 7 candidates of size 3+-- looking through 8 candidates of size 4+-- looking through 28 candidates of size 5+-- looking through 35 candidates of size 6+-- looking through 167 candidates of size 7+-- tested 95 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- looking through 203 candidates of size 8+-- tested 254 candidates+factorial 1  =  1+factorial x  =  x * factorial (x - 1)++-- looking through 1048 candidates of size 9+-- tested 547 candidates+factorial 0  =  0+factorial 1  =  1+factorial x  =  x * factorial (x - 1)++-- tested 555 candidates+factorial 0  =  1+factorial 1  =  1+factorial x  =  x * factorial (x - 1)++-- looking through 1301 candidates of size 10+-- looking through 7201 candidates of size 11+-- tested 3216 candidates+factorial 0  =  1+factorial x  =  x + x * (factorial (x - 1) - 1)++-- tested 3396 candidates+factorial 0  =  1+factorial x  =  x - x * (1 - factorial (x - 1))++-- tested 3519 candidates+factorial 0  =  1+factorial x  =  (0 - x) * (0 - factorial (x - 1))++-- tested 10004 candidates+cannot conjure+

@@ -1,7 +1,7 @@ Erroneous candidates for: foo :: Int -> Int   pruning with 41/82 rules-  [4,8,16,42,70,162,493] candidates-  30/795 erroneous candidates+  [4,8,16,42,65,150,417] candidates+  30/702 erroneous candidates  foo 0  =  0 foo x  =  x + foo (x - 2)

@@ -151,8 +151,8 @@ -- looking through 4 candidates of size 5 -- looking through 86 candidates of size 6 -- looking through 5 candidates of size 7--- looking through 537 candidates of size 8--- tested 588 candidates+-- looking through 513 candidates of size 8+-- tested 564 candidates wallisNext (x % y)  =  (y + 1) % (x + 1)  wallisNext :: Ratio Integer -> Ratio Integer@@ -235,7 +235,7 @@ -- looking through 13 candidates of size 5 -- looking through 51 candidates of size 6 -- looking through 103 candidates of size 7--- looking through 365 candidates of size 8+-- looking through 360 candidates of size 8 -- tested 267 candidates gps13 qs  =  foldr (+) 0 qs / fromIntegral (length qs) @@ -244,10 +244,10 @@ -- pruning with 12/13 rules -- looking through 0 candidates of size 1 -- looking through 0 candidates of size 2--- looking through 4 candidates of size 3--- looking through 3 candidates of size 4--- looking through 39 candidates of size 5--- tested 20 candidates+-- looking through 3 candidates of size 3+-- looking through 2 candidates of size 4+-- looking through 37 candidates of size 5+-- tested 17 candidates odd x  =  0 /= x `mod` 2  gps14 :: [Int] -> Int@@ -268,9 +268,9 @@ -- looking through 0 candidates of size 3 -- looking through 27 candidates of size 4 -- looking through 30 candidates of size 5--- looking through 258 candidates of size 6--- looking through 474 candidates of size 7--- tested 378 candidates+-- looking through 240 candidates of size 6+-- looking through 453 candidates of size 7+-- tested 353 candidates gps14 []  =  0 gps14 (x:xs)  =  x + gps14 xs `mod` 2 @@ -304,10 +304,10 @@ -- looking through 8 candidates of size 4 -- looking through 28 candidates of size 5 -- looking through 35 candidates of size 6--- looking through 179 candidates of size 7--- looking through 217 candidates of size 8--- looking through 1196 candidates of size 9--- tested 492 candidates+-- looking through 167 candidates of size 7+-- looking through 203 candidates of size 8+-- looking through 1048 candidates of size 9+-- tested 466 candidates gps17 0  =  0 gps17 x  =  gps17 (x - 1) + x * x @@ -459,9 +459,9 @@ -- looking through 13 candidates of size 6 -- looking through 30 candidates of size 7 -- looking through 75 candidates of size 8--- looking through 195 candidates of size 9--- looking through 474 candidates of size 10--- tested 457 candidates+-- looking through 194 candidates of size 9+-- looking through 470 candidates of size 10+-- tested 456 candidates gps24 cs  =  chr (ord ' ' + sum (map ord cs) `mod` 64)  gps25 :: Int -> [Int]

@@ -155,11 +155,11 @@ -- looking through 0 candidates of size 3 -- looking through 68 candidates of size 4 -- looking through 80 candidates of size 5--- looking through 1084 candidates of size 6--- looking through 1556 candidates of size 7--- looking through 20600 candidates of size 8--- looking through 35632 candidates of size 9--- tested 29538 candidates+-- looking through 980 candidates of size 6+-- looking through 1428 candidates of size 7+-- looking through 17324 candidates of size 8+-- looking through 30724 candidates of size 9+-- tested 25024 candidates gps10 []  =  0 gps10 (x:xs)  =  gps10 xs + (x `div` 3 - 2) 

@@ -1,1 +1,1 @@-10.8+9.1

@@ -0,0 +1,1 @@+2.5

@@ -1,1 +1,1 @@-3.2+2.7

@@ -1,1 +1,1 @@-15.8+14.1

@@ -1,1 +1,1 @@-14.3+12.1

@@ -1,1 +1,1 @@-1.8+1.6

@@ -1,1 +1,1 @@-3.2+2.9

@@ -0,0 +1,1 @@+4.4

@@ -1,1 +1,1 @@-9.2+7.9

@@ -0,0 +1,1 @@+2.2

@@ -1,1 +1,1 @@-3.3+2.7

@@ -1,1 +1,1 @@-1.0+0.9

@@ -1,1 +1,1 @@-2.1+1.8

@@ -1,1 +1,1 @@-7.9+7.5

@@ -1,1 +1,1 @@-1.5+1.4

@@ -1,1 +1,1 @@-15.5+3.3

@@ -1,1 +1,1 @@-0.7+0.6

@@ -1,1 +1,1 @@-0.6+0.5

@@ -1,1 +1,1 @@-1.2+1.1

@@ -1,1 +1,1 @@-2.1+1.5

@@ -1,1 +1,1 @@-4.4+4.1

@@ -1,1 +1,1 @@-1.3+1.1

@@ -1,1 +1,1 @@-1.4+1.3

@@ -1,1 +1,1 @@-1.4+1.2

@@ -1,4 +1,4 @@ GHC 9.0.2 leancheck-1.0.2 express-1.0.16-speculate-0.4.18+speculate-0.4.20

@@ -0,0 +1,1 @@+4.9

@@ -0,0 +1,1 @@+8.1

@@ -0,0 +1,1 @@+4.5

@@ -0,0 +1,72 @@+-- strategies.hs: conjuring factorial with different strategies+--+-- Copyright (C) 2021-2024 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++factorial :: Int -> Int+factorial 1  =  1+factorial 2  =  2+factorial 3  =  6+factorial 4  =  24+++mkStrategy :: String -> Args+mkStrategy s  =  args+  { rewriting         =  r+  , requireDescent    =  d+  , adHocRedundancy   =  a+  , copyBindings      =  a -- previously c+  , uniqueCandidates  =  u+--, carryOn  =  True+--, maxSize  =  10+  }+  where+  itob 0  =  False+  itob _  =  True+  [r,d,a,u]  =  map itob $+    case s of+    "unique candidates" -> [1,1,1,1]+    "default"           -> [1,1,1,0]+    "without reasoning" -> [0,1,1,0]+    "without descent"   -> [1,0,1,0]+    "without ad-hoc"    -> [1,1,0,0]+    "only reasoning"    -> [1,0,0,0]+    "only descent"      -> [0,1,0,0]+    "only ad-hoc"       -> [0,0,1,0]+    "only typed"        -> [0,0,0,0]+    _                   -> error "unknown strategy"++conjureStrategy :: Conjurable f => String -> String -> f -> [Prim] -> IO ()+conjureStrategy name nm f prims  =  do+  putStrLn $ "-- strategy: " ++ name+  conjureWith (mkStrategy name) nm f prims++strategies :: [String]+strategies  =  +  [ "unique candidates"+  , "default"+  , "without reasoning"+  , "without descent"+  , "without ad-hoc"+  , "only reasoning"+  , "only descent"+  , "only ad-hoc"+  , "only typed"+  ]++main :: IO ()+main  =  do+  sequence_+    [ conjureStrategy s "factorial n" factorial primitives+    | s <- strategies+    ]++primitives :: [Prim]+primitives = +    [ pr (0::Int)+    , pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "-" ((-) :: Int -> Int -> Int)+    ]

@@ -0,0 +1,135 @@+-- strategy: unique candidates+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 7 candidates of size 3+-- looking through 8 candidates of size 4+-- looking through 23 candidates of size 5+-- looking through 30 candidates of size 6+-- looking through 82 candidates of size 7+-- tested 84 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: default+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 7 candidates of size 3+-- looking through 8 candidates of size 4+-- looking through 28 candidates of size 5+-- looking through 35 candidates of size 6+-- looking through 167 candidates of size 7+-- tested 95 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: without reasoning+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 16 candidates of size 3+-- looking through 17 candidates of size 4+-- looking through 279 candidates of size 5+-- looking through 313 candidates of size 6+-- looking through 5763 candidates of size 7+-- tested 656 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: without descent+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 7 candidates of size 3+-- looking through 8 candidates of size 4+-- looking through 28 candidates of size 5+-- looking through 35 candidates of size 6+-- looking through 252 candidates of size 7+-- tested 148 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: without ad-hoc+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 6 candidates of size 2+-- looking through 12 candidates of size 3+-- looking through 24 candidates of size 4+-- looking through 37 candidates of size 5+-- looking through 72 candidates of size 6+-- looking through 196 candidates of size 7+-- tested 165 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: only reasoning+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 6 candidates of size 2+-- looking through 12 candidates of size 3+-- looking through 24 candidates of size 4+-- looking through 47 candidates of size 5+-- looking through 82 candidates of size 6+-- looking through 342 candidates of size 7+-- tested 284 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: only descent+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 6 candidates of size 2+-- looking through 21 candidates of size 3+-- looking through 42 candidates of size 4+-- looking through 302 candidates of size 5+-- looking through 602 candidates of size 6+-- looking through 6115 candidates of size 7+-- tested 1001 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: only ad-hoc+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 16 candidates of size 3+-- looking through 17 candidates of size 4+-- looking through 279 candidates of size 5+-- looking through 313 candidates of size 6+-- looking through 6281 candidates of size 7+-- tested 1004 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)++-- strategy: only typed+factorial :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 27/65 rules+-- looking through 3 candidates of size 1+-- looking through 6 candidates of size 2+-- looking through 21 candidates of size 3+-- looking through 42 candidates of size 4+-- looking through 330 candidates of size 5+-- looking through 630 candidates of size 6+-- looking through 7215 candidates of size 7+-- tested 1945 candidates+factorial 0  =  1+factorial x  =  x * factorial (x - 1)+

@@ -58,8 +58,8 @@ -- looking through 1242 candidates of size 8 -- looking through 3087 candidates of size 9 -- looking through 8937 candidates of size 10--- looking through 102875 candidates of size 11--- tested 40385 candidates+-- looking through 102200 candidates of size 11+-- tested 39710 candidates cshift (p,q,r)  =  if p                    then (p,r,q)                    else (p,q,r)

@@ -0,0 +1,107 @@+-- Print unique candidates+--+-- Copyright (C) 2023-2024 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+--+-- This can be used to track+-- if we loose any solutions from implementing pruning techniques.+import Conjure++-- This script needs some internal utilities of Conjure:+import Conjure.Engine+import Conjure.Defn+import Conjure.Defn.Redundancy+import Conjure.Defn.Test+import Conjure.Utils+import Test.LeanCheck.Tiers (discardT, discardLaterT)+++-- | This function prints unique 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.+printUniqueCandidates :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()+printUniqueCandidates n nm f ps  =  do+  putStrLn $ "Unique candidates for: " ++ nm ++ " :: " ++ show (typeOf f)+  putStrLn $ "  pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"+  putStrLn $ "  " ++ show (map length css) ++ " candidates"+  putStrLn $ "  " ++ show (map length uss) ++ " unique candidates"+  putStrLn $ "  " ++ show numUnique ++ "/" ++ show numCandidates ++ " unique candidates"+  putStrLn $ "  " ++ show numRedundant ++ "/" ++ show numCandidates ++ " redundant candidates"+  putStrLn ""+  printThy thy+  putStrLn $ unlines . map showDefn $ unique+  where+  numCandidates  =  length candidates+  numUnique      =  length unique+  numRedundant   =  numCandidates - numUnique+  unique         =  concat uss+  candidates     =  concat css+  uss            =  discardLaterT (equalModuloTesting maxTests maxEvalRecursions nm f)+                 $  css+  css            =  take n+                 $  discardT isRedundantByIntroduction -- additional pruning rule+                 $  css'+  (css', thy)    =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates+  nRules         =  length (rules thy)+  nREs           =  length (equations thy) + nRules+  maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark+  maxEvalRecursions  =  30++  -- 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+  let n = 5++  printUniqueCandidates (n+2) "foo" (undefined :: Int -> Int)+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "-" ((-) :: Int -> Int -> Int)+    ]++  printUniqueCandidates n "?" (undefined :: Int -> Int -> Int)+    [ pr (0 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "dec" (subtract 1 :: Int -> Int)+    ]++  printUniqueCandidates (n+2) "goo" (undefined :: [Int] -> [Int])+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    ]++  printUniqueCandidates n "??" (undefined :: [Int] -> [Int] -> [Int])+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    ]++  printUniqueCandidates (n+2) "ton" (undefined :: Bool -> Bool)+    [ pr False+    , pr True+    , prim "&&" (&&)+    , prim "||" (||)+    , prim "not" not+    ]++  printUniqueCandidates n "&|" (undefined :: Bool -> Bool -> Bool)+    [ pr False+    , pr True+    , prim "&&" (&&)+    , prim "||" (||)+    , prim "not" not+    ]

@@ -0,0 +1,2276 @@+Unique candidates for: foo :: Int -> Int+  pruning with 27/65 rules+  [3,3,9,10,32,39,185] candidates+  [3,3,9,10,27,34,95] unique candidates+  181/281 unique candidates+  100/281 redundant candidates++rules:+x - x == 0+x * 0 == 0+x * 1 == x+0 * x == 0+1 * x == x+x + 0 == x+0 + x == x+x - 0 == x+(x * y) * z == x * (y * z)+(x * y) * z == y * (x * z)+(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 + x) * y == x * (y + y)+x + (y - x) == y+(x - y) + y == x+x * y - x == x * (y - 1)+x * y - y == y * (x - 1)+x * (y + 1) == x + x * y+x * (y + 1) == x * y + x+(x + 1) * y == y + x * y+0 - x * y == x * (0 - y)+0 - x * y == y * (0 - x)+equations:+y * x == x * y+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)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+(z + y) * x == x * (y + z)+y + (x - z) == x + (y - z)+z * y + x == x + y * z+(x - z) + y == x + (y - z)+(z - y) + x == (x - y) + z+y * (x + x) == x * (y + y)+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 * (1 - y) == x - x * y+x * (1 - y) == x - y * x+y * (0 - x) == x * (0 - y)+(0 - x) * y == x * (0 - y)+(0 - y) * x == (0 - x) * y+(1 - y) * x == x - x * y+(1 - y) * x == 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)+x * (0 - 1) == 0 - x+(0 - 1) * x == 0 - x+(0 - 1) * y == x - (x + y)+(0 - 1) * y == x - (y + x)++foo x  =  x++foo x  =  0++foo x  =  1++foo 0  =  0+foo x  =  1++foo 0  =  1+foo x  =  x++foo 0  =  1+foo x  =  0++foo x  =  x + x++foo x  =  x + 1++foo x  =  x * x++foo x  =  x - 1++foo x  =  0 - x++foo x  =  1 - x++foo 1  =  0+foo x  =  x++foo 1  =  0+foo x  =  1++foo 1  =  1+foo x  =  0++foo 0  =  0+foo x  =  x + 1++foo 0  =  0+foo x  =  x - 1++foo 0  =  0+foo x  =  1 - x++foo 0  =  1+foo x  =  x + x++foo 0  =  1+foo x  =  x * x++foo 0  =  1+foo x  =  x - 1++foo 0  =  1+foo x  =  0 - x++foo 0  =  0+foo 1  =  0+foo x  =  1++foo 0  =  1+foo 1  =  0+foo x  =  x++foo 0  =  1+foo 1  =  1+foo x  =  0++foo x  =  x * x - 1++foo x  =  x + (x + x)++foo x  =  x + (x + 1)++foo x  =  x + x * x++foo x  =  x + (x - 1)++foo x  =  1 + (x + 1)++foo x  =  1 + x * x++foo x  =  1 + (1 - x)++foo x  =  x * (x + x)++foo x  =  x * (x * x)++foo x  =  x * (x - 1)++foo x  =  x * (0 - x)++foo x  =  x * (1 - x)++foo x  =  x - (x + 1)++foo x  =  0 - (x + x)++foo x  =  0 - (x + 1)++foo x  =  1 - (x + x)++foo x  =  1 - x * x++foo 1  =  0+foo x  =  x + x++foo 1  =  0+foo x  =  x + 1++foo 1  =  0+foo x  =  x * x++foo 1  =  0+foo x  =  0 - x++foo 1  =  1+foo x  =  x + x++foo 1  =  1+foo x  =  x + 1++foo 1  =  1+foo x  =  x - 1++foo 1  =  1+foo x  =  0 - x++foo 1  =  1+foo x  =  1 - x++foo 0  =  0+foo x  =  x * x - 1++foo 0  =  0+foo x  =  x + (x + 1)++foo 0  =  0+foo x  =  x + (x - 1)++foo 0  =  0+foo x  =  1 + (x + 1)++foo 0  =  0+foo x  =  1 + x * x++foo 0  =  0+foo x  =  1 + (1 - x)++foo 0  =  0+foo x  =  x - (x + 1)++foo 0  =  0+foo x  =  0 - (x + 1)++foo 0  =  0+foo x  =  1 - (x + x)++foo 0  =  0+foo x  =  1 - x * x++foo 0  =  1+foo x  =  x * x - 1++foo 0  =  1+foo x  =  x + (x + x)++foo 0  =  1+foo x  =  x + x * x++foo 0  =  1+foo x  =  x + (x - 1)++foo 0  =  1+foo x  =  1 + (x + 1)++foo 0  =  1+foo x  =  1 + (1 - x)++foo 0  =  1+foo x  =  x * (x + x)++foo 0  =  1+foo x  =  x * (x * x)++foo 0  =  1+foo x  =  x * (x - 1)++foo 0  =  1+foo x  =  x * (0 - x)++foo 0  =  1+foo x  =  x * (1 - x)++foo 0  =  1+foo x  =  x - (x + 1)++foo 0  =  1+foo x  =  0 - (x + x)++foo 0  =  1+foo x  =  0 - (x + 1)++foo 0  =  0+foo 1  =  0+foo x  =  x + 1++foo 0  =  0+foo 1  =  1+foo x  =  x + 1++foo 0  =  0+foo 1  =  1+foo x  =  x - 1++foo 0  =  0+foo 1  =  1+foo x  =  1 - x++foo 0  =  1+foo 1  =  0+foo x  =  x + x++foo 0  =  1+foo 1  =  0+foo x  =  x * x++foo 0  =  1+foo 1  =  0+foo x  =  0 - x++foo 0  =  1+foo 1  =  1+foo x  =  x + x++foo 0  =  1+foo 1  =  1+foo x  =  x - 1++foo 0  =  1+foo 1  =  1+foo x  =  0 - x++foo 0  =  0+foo x  =  x + foo (x - 1)++foo 0  =  0+foo x  =  foo (x - 1) + 1++foo 0  =  0+foo x  =  x * foo (x - 1)++foo 0  =  0+foo x  =  x - foo (x - 1)++foo 0  =  0+foo x  =  foo (x - 1) - x++foo 0  =  0+foo x  =  foo (x - 1) - 1++foo 0  =  0+foo x  =  1 - foo (x - 1)++foo 0  =  1+foo x  =  x + foo (x - 1)++foo 0  =  1+foo x  =  foo (x - 1) + 1++foo 0  =  1+foo x  =  x * foo (x - 1)++foo 0  =  1+foo x  =  x - foo (x - 1)++foo 0  =  1+foo x  =  foo (x - 1) - x++foo 0  =  1+foo x  =  foo (x - 1) - 1++foo 0  =  1+foo x  =  0 - foo (x - 1)++foo 0  =  1+foo x  =  1 - foo (x - 1)++foo x  =  x * (x + x) - 1++foo x  =  x * (x * x) - 1++foo x  =  x * (x - 1) - 1++foo x  =  x * (0 - x) - 1++foo x  =  x * (1 - x) - 1++foo x  =  x + (x * x - 1)++foo x  =  x + (x + (x + x))++foo x  =  x + (x + (x + 1))++foo x  =  x + (x + x * x)++foo x  =  x + (x + (x - 1))++foo x  =  x + (1 + (x + 1))++foo x  =  x + (1 + x * x)++foo x  =  x + (1 + (1 - x))++foo x  =  x + x * (x + x)++foo x  =  x + x * (x * x)++foo x  =  x + x * (1 - x)++foo x  =  x + (1 - x * x)++foo x  =  1 + (1 + (x + 1))++foo x  =  1 + (1 + x * x)++foo x  =  1 + (1 + (1 - x))++foo x  =  1 + x * (x + x)++foo x  =  1 + x * (x * x)++foo x  =  1 + x * (x - 1)++foo x  =  1 + (1 - (x + x))++foo x  =  1 + (1 - x * x)++foo x  =  x * (x * x - 1)++foo x  =  x * (x + (x + x))++foo x  =  x * (x + x * x)++foo x  =  x * (x + (x - 1))++foo x  =  x * (x * (x + x))++foo x  =  x * (x * (x * x))++foo x  =  x * (x * (x - 1))++foo x  =  x * (x * (0 - x))++foo x  =  x * (x * (1 - x))++foo x  =  x * (0 - (x + x))++foo x  =  x * (0 - (x + 1))++foo x  =  x * (1 - (x + x))++foo x  =  x * (1 - x * x)++foo x  =  x - (1 + (x + 1))++foo x  =  x - (1 + (1 - x))++foo x  =  0 - (x + (x + x))++foo x  =  0 - (x + (x + 1))++foo x  =  0 - (1 + (x + 1))++foo x  =  0 - (1 + (1 - x))++foo x  =  1 - (x + (x + x))++foo x  =  1 - (x + x * x)++foo x  =  1 - x * (x + x)++foo x  =  1 - x * (x * x)++foo x  =  (x - 1) * (x - 1)++foo x  =  (x - 1) * (1 - x)++foo x  =  x * x - (x + x)++foo 1  =  0+foo x  =  x + (x + x)++foo 1  =  0+foo x  =  x + (x + 1)++foo 1  =  0+foo x  =  x + x * x++foo 1  =  0+foo x  =  x + (x - 1)++foo 1  =  0+foo x  =  1 + (x + 1)++foo 1  =  0+foo x  =  1 + x * x++foo 1  =  0+foo x  =  1 + (1 - x)++foo 1  =  0+foo x  =  x * (x + x)++foo 1  =  0+foo x  =  x * (x * x)++foo 1  =  0+foo x  =  x * (0 - x)++foo 1  =  0+foo x  =  x - (x + 1)++foo 1  =  0+foo x  =  0 - (x + x)++foo 1  =  0+foo x  =  0 - (x + 1)++foo 1  =  0+foo x  =  1 - (x + x)++foo 1  =  1+foo x  =  x * x - 1++foo 1  =  1+foo x  =  x + (x + x)++foo 1  =  1+foo x  =  x + (x + 1)++foo 1  =  1+foo x  =  x + x * x++foo 1  =  1+foo x  =  1 + (x + 1)++foo 1  =  1+foo x  =  1 + x * x++foo 1  =  1+foo x  =  x * (x + x)++foo 1  =  1+foo x  =  x * (x - 1)++foo 1  =  1+foo x  =  x * (0 - x)++foo 1  =  1+foo x  =  x * (1 - x)++foo 1  =  1+foo x  =  x - (x + 1)++foo 1  =  1+foo x  =  0 - (x + x)++foo 1  =  1+foo x  =  0 - (x + 1)++foo 1  =  1+foo x  =  1 - (x + x)++foo 1  =  1+foo x  =  1 - x * x+++Unique candidates for: ? :: Int -> Int -> Int+  pruning with 13/34 rules+  [3,8,25,71,205] candidates+  [3,8,25,70,188] unique candidates+  294/312 unique candidates+  18/312 redundant candidates++rules:+x * 0 == 0+0 * x == 0+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)+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+(x + x) * y == x * (y + y)+equations:+y * x == x * y+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 + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+(z + y) * x == x * (y + z)+z * y + x == x + y * z+y * (x + x) == x * (y + y)+y + dec (dec x) == x + dec (dec y)+dec (dec x) + y == x + dec (dec y)+dec (dec y) + x == dec (dec x) + y+x + dec (dec 0) == dec (dec x)+dec (dec 0) + x == dec (dec x)++x ? y  =  x++x ? y  =  y++x ? y  =  0++x ? y  =  dec x++x ? y  =  dec y++x ? 0  =  x+x ? y  =  y++x ? 0  =  x+x ? y  =  0++x ? 0  =  0+x ? y  =  x++0 ? x  =  x+x ? y  =  x++0 ? x  =  x+x ? y  =  0++0 ? x  =  0+x ? y  =  y++x ? y  =  x + x++x ? y  =  x + y++x ? y  =  y + y++x ? y  =  x * x++x ? y  =  x * y++x ? y  =  y * y++x ? y  =  dec (dec x)++x ? y  =  dec (dec y)++x ? 0  =  x+x ? y  =  dec x++x ? 0  =  x+x ? y  =  dec y++x ? 0  =  0+x ? y  =  dec x++x ? 0  =  0+x ? y  =  dec y++x ? 0  =  dec x+x ? y  =  x++x ? 0  =  dec x+x ? y  =  y++x ? 0  =  dec x+x ? y  =  0++0 ? x  =  x+x ? y  =  dec x++0 ? x  =  x+x ? y  =  dec y++0 ? x  =  0+x ? y  =  dec x++0 ? x  =  0+x ? y  =  dec y++0 ? x  =  dec x+x ? y  =  x++0 ? x  =  dec x+x ? y  =  y++0 ? x  =  dec x+x ? y  =  0++0 ? x  =  x+x ? 0  =  x+x ? y  =  0++0 ? x  =  x+x ? 0  =  0+x ? y  =  x++0 ? x  =  0+x ? 0  =  x+x ? y  =  y++x ? y  =  dec (x * x)++x ? y  =  dec (x * y)++x ? y  =  dec (y * y)++x ? y  =  dec (dec (dec x))++x ? y  =  dec (dec (dec y))++x ? y  =  x + dec x++x ? y  =  x + dec y++x ? y  =  y + dec y++x ? y  =  x * dec x++x ? y  =  x * dec y++x ? y  =  y * dec x++x ? y  =  y * dec y++x ? 0  =  x+x ? y  =  x + x++x ? 0  =  x+x ? y  =  y + y++x ? 0  =  x+x ? y  =  x * x++x ? 0  =  x+x ? y  =  x * y++x ? 0  =  x+x ? y  =  y * y++x ? 0  =  x+x ? y  =  dec (dec x)++x ? 0  =  x+x ? y  =  dec (dec y)++x ? 0  =  0+x ? y  =  x + x++x ? 0  =  0+x ? y  =  x + y++x ? 0  =  0+x ? y  =  x * x++x ? 0  =  0+x ? y  =  dec (dec x)++x ? 0  =  0+x ? y  =  dec (dec y)++x ? 0  =  dec x+x ? y  =  dec y++x ? 0  =  x + x+x ? y  =  x++x ? 0  =  x + x+x ? y  =  y++x ? 0  =  x + x+x ? y  =  0++x ? 0  =  x * x+x ? y  =  x++x ? 0  =  x * x+x ? y  =  y++x ? 0  =  x * x+x ? y  =  0++x ? 0  =  dec (dec x)+x ? y  =  x++x ? 0  =  dec (dec x)+x ? y  =  y++x ? 0  =  dec (dec x)+x ? y  =  0++0 ? x  =  x+x ? y  =  x + x++0 ? x  =  x+x ? y  =  y + y++0 ? x  =  x+x ? y  =  x * x++0 ? x  =  x+x ? y  =  x * y++0 ? x  =  x+x ? y  =  y * y++0 ? x  =  x+x ? y  =  dec (dec x)++0 ? x  =  x+x ? y  =  dec (dec y)++0 ? x  =  0+x ? y  =  x + y++0 ? x  =  0+x ? y  =  y + y++0 ? x  =  0+x ? y  =  y * y++0 ? x  =  0+x ? y  =  dec (dec x)++0 ? x  =  0+x ? y  =  dec (dec y)++0 ? x  =  dec x+x ? y  =  dec x++0 ? x  =  x + x+x ? y  =  x++0 ? x  =  x + x+x ? y  =  y++0 ? x  =  x + x+x ? y  =  0++0 ? x  =  x * x+x ? y  =  x++0 ? x  =  x * x+x ? y  =  y++0 ? x  =  x * x+x ? y  =  0++0 ? x  =  dec (dec x)+x ? y  =  x++0 ? x  =  dec (dec x)+x ? y  =  y++0 ? x  =  dec (dec x)+x ? y  =  0++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec x++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec y++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec x++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec y++0 ? x  =  x+x ? 0  =  dec x+x ? y  =  x++0 ? x  =  x+x ? 0  =  dec x+x ? y  =  0++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec x++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec y++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec x++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec y++0 ? x  =  0+x ? 0  =  dec x+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  x+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  x+x ? y  =  0++0 ? x  =  dec x+x ? 0  =  0+x ? y  =  x++x ? 0  =  x+x ? y  =  y ? dec x++x ? 0  =  x+x ? y  =  y ? dec y++x ? 0  =  x+x ? y  =  dec x ? x++x ? 0  =  x+x ? y  =  dec x ? y++x ? 0  =  x+x ? y  =  dec y ? x++0 ? x  =  x+x ? y  =  x ? dec y++0 ? x  =  x+x ? y  =  y ? dec x++0 ? x  =  x+x ? y  =  y ? dec y++0 ? x  =  x+x ? y  =  dec x ? x++0 ? x  =  x+x ? y  =  dec y ? x++x ? y  =  dec (dec (x * x))++x ? y  =  dec (dec (x * y))++x ? y  =  dec (dec (y * y))++x ? y  =  dec (dec (dec (dec x)))++x ? y  =  dec (dec (dec (dec y)))++x ? y  =  dec (x * dec x)++x ? y  =  dec (x * dec y)++x ? y  =  dec (y * dec x)++x ? y  =  dec (y * dec y)++x ? y  =  x + (x + x)++x ? y  =  x + (x + y)++x ? y  =  x + (y + y)++x ? y  =  x + x * x++x ? y  =  x + x * y++x ? y  =  x + y * y++x ? y  =  x + dec (dec x)++x ? y  =  x + dec (dec y)++x ? y  =  y + (y + y)++x ? y  =  y + x * x++x ? y  =  y + x * y++x ? y  =  y + y * y++x ? y  =  y + dec (dec y)++x ? y  =  x * (x + x)++x ? y  =  x * (x + y)++x ? y  =  x * (y + y)++x ? y  =  x * (x * x)++x ? y  =  x * (x * y)++x ? y  =  x * (y * y)++x ? y  =  x * dec (dec x)++x ? y  =  x * dec (dec y)++x ? y  =  y * (x + y)++x ? y  =  y * (y + y)++x ? y  =  y * (y * y)++x ? y  =  y * dec (dec x)++x ? y  =  y * dec (dec y)++x ? y  =  dec x * dec x++x ? y  =  dec x * dec y++x ? y  =  dec y * dec y++x ? 0  =  x+x ? y  =  dec (x * x)++x ? 0  =  x+x ? y  =  dec (x * y)++x ? 0  =  x+x ? y  =  dec (y * y)++x ? 0  =  x+x ? y  =  dec (dec (dec x))++x ? 0  =  x+x ? y  =  dec (dec (dec y))++x ? 0  =  x+x ? y  =  x + dec x++x ? 0  =  x+x ? y  =  x + dec y++x ? 0  =  x+x ? y  =  y + dec y++x ? 0  =  x+x ? y  =  x * dec x++x ? 0  =  x+x ? y  =  x * dec y++x ? 0  =  x+x ? y  =  y * dec x++x ? 0  =  x+x ? y  =  y * dec y++x ? 0  =  0+x ? y  =  dec (x * x)++x ? 0  =  0+x ? y  =  dec (x * y)++x ? 0  =  0+x ? y  =  dec (y * y)++x ? 0  =  0+x ? y  =  dec (dec (dec x))++x ? 0  =  0+x ? y  =  dec (dec (dec y))++x ? 0  =  0+x ? y  =  x + dec x++x ? 0  =  0+x ? y  =  x + dec y++x ? 0  =  0+x ? y  =  y + dec y++x ? 0  =  0+x ? y  =  x * dec x++x ? 0  =  0+x ? y  =  x * dec y++x ? 0  =  dec x+x ? y  =  x + x++x ? 0  =  dec x+x ? y  =  x + y++x ? 0  =  dec x+x ? y  =  y + y++x ? 0  =  dec x+x ? y  =  x * x++x ? 0  =  dec x+x ? y  =  x * y++x ? 0  =  dec x+x ? y  =  y * y++x ? 0  =  dec x+x ? y  =  dec (dec x)++x ? 0  =  dec x+x ? y  =  dec (dec y)++x ? 0  =  x + x+x ? y  =  dec x++x ? 0  =  x + x+x ? y  =  dec y++x ? 0  =  x * x+x ? y  =  dec x++x ? 0  =  x * x+x ? y  =  dec y++x ? 0  =  dec (dec x)+x ? y  =  dec x++x ? 0  =  dec (dec x)+x ? y  =  dec y++x ? 0  =  dec (x * x)+x ? y  =  x++x ? 0  =  dec (x * x)+x ? y  =  y++x ? 0  =  dec (x * x)+x ? y  =  0++x ? 0  =  dec (dec (dec x))+x ? y  =  x++x ? 0  =  dec (dec (dec x))+x ? y  =  y++x ? 0  =  dec (dec (dec x))+x ? y  =  0++x ? 0  =  x + dec x+x ? y  =  x++x ? 0  =  x + dec x+x ? y  =  y++x ? 0  =  x + dec x+x ? y  =  0++x ? 0  =  x * dec x+x ? y  =  x++x ? 0  =  x * dec x+x ? y  =  y++x ? 0  =  x * dec x+x ? y  =  0++0 ? x  =  x+x ? y  =  dec (x * x)++0 ? x  =  x+x ? y  =  dec (x * y)++0 ? x  =  x+x ? y  =  dec (y * y)++0 ? x  =  x+x ? y  =  dec (dec (dec x))++0 ? x  =  x+x ? y  =  dec (dec (dec y))++0 ? x  =  x+x ? y  =  x + dec x++0 ? x  =  x+x ? y  =  x + dec y++0 ? x  =  x+x ? y  =  y + dec y++0 ? x  =  x+x ? y  =  x * dec x++0 ? x  =  x+x ? y  =  x * dec y++0 ? x  =  x+x ? y  =  y * dec x++0 ? x  =  x+x ? y  =  y * dec y++0 ? x  =  0+x ? y  =  dec (x * x)++0 ? x  =  0+x ? y  =  dec (x * y)++0 ? x  =  0+x ? y  =  dec (y * y)++0 ? x  =  0+x ? y  =  dec (dec (dec x))++0 ? x  =  0+x ? y  =  dec (dec (dec y))++0 ? x  =  0+x ? y  =  x + dec x++0 ? x  =  0+x ? y  =  x + dec y++0 ? x  =  0+x ? y  =  y + dec y++0 ? x  =  0+x ? y  =  y * dec x++0 ? x  =  0+x ? y  =  y * dec y++0 ? x  =  dec x+x ? y  =  x + x++0 ? x  =  dec x+x ? y  =  x + y++0 ? x  =  dec x+x ? y  =  y + y++0 ? x  =  dec x+x ? y  =  x * x++0 ? x  =  dec x+x ? y  =  x * y++0 ? x  =  dec x+x ? y  =  y * y++0 ? x  =  dec x+x ? y  =  dec (dec x)++0 ? x  =  dec x+x ? y  =  dec (dec y)++0 ? x  =  x + x+x ? y  =  dec x++0 ? x  =  x + x+x ? y  =  dec y++0 ? x  =  x * x+x ? y  =  dec x++0 ? x  =  x * x+x ? y  =  dec y++0 ? x  =  dec (dec x)+x ? y  =  dec x++0 ? x  =  dec (dec x)+x ? y  =  dec y++0 ? x  =  dec (x * x)+x ? y  =  x++0 ? x  =  dec (x * x)+x ? y  =  y++0 ? x  =  dec (x * x)+x ? y  =  0++0 ? x  =  dec (dec (dec x))+x ? y  =  x++0 ? x  =  dec (dec (dec x))+x ? y  =  y++0 ? x  =  dec (dec (dec x))+x ? y  =  0++0 ? x  =  x + dec x+x ? y  =  x++0 ? x  =  x + dec x+x ? y  =  y++0 ? x  =  x + dec x+x ? y  =  0++0 ? x  =  x * dec x+x ? y  =  x++0 ? x  =  x * dec x+x ? y  =  y++0 ? x  =  x * dec x+x ? y  =  0++0 ? x  =  x+x ? 0  =  x+x ? y  =  x + x++0 ? x  =  x+x ? 0  =  x+x ? y  =  y + y++0 ? x  =  x+x ? 0  =  x+x ? y  =  x * x++0 ? x  =  x+x ? 0  =  x+x ? y  =  x * y++0 ? x  =  x+x ? 0  =  x+x ? y  =  y * y++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec (dec x)++0 ? x  =  x+x ? 0  =  x+x ? y  =  dec (dec y)++0 ? x  =  x+x ? 0  =  0+x ? y  =  x + x++0 ? x  =  x+x ? 0  =  0+x ? y  =  x * x++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec (dec x)++0 ? x  =  x+x ? 0  =  0+x ? y  =  dec (dec y)++0 ? x  =  x+x ? 0  =  dec x+x ? y  =  dec y++0 ? x  =  x+x ? 0  =  x + x+x ? y  =  x++0 ? x  =  x+x ? 0  =  x + x+x ? y  =  0++0 ? x  =  x+x ? 0  =  x * x+x ? y  =  x++0 ? x  =  x+x ? 0  =  x * x+x ? y  =  0++0 ? x  =  x+x ? 0  =  dec (dec x)+x ? y  =  x++0 ? x  =  x+x ? 0  =  dec (dec x)+x ? y  =  0++0 ? x  =  0+x ? 0  =  x+x ? y  =  y + y++0 ? x  =  0+x ? 0  =  x+x ? y  =  y * y++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec (dec x)++0 ? x  =  0+x ? 0  =  x+x ? y  =  dec (dec y)++0 ? x  =  0+x ? 0  =  0+x ? y  =  x + y++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec (dec x)++0 ? x  =  0+x ? 0  =  0+x ? y  =  dec (dec y)++0 ? x  =  0+x ? 0  =  dec x+x ? y  =  dec y++0 ? x  =  0+x ? 0  =  x + x+x ? y  =  y++0 ? x  =  0+x ? 0  =  x * x+x ? y  =  y++0 ? x  =  0+x ? 0  =  dec (dec x)+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  x+x ? y  =  dec x++0 ? x  =  dec x+x ? 0  =  0+x ? y  =  dec x++0 ? x  =  dec x+x ? 0  =  dec x+x ? y  =  x++0 ? x  =  dec x+x ? 0  =  dec x+x ? y  =  y++0 ? x  =  dec x+x ? 0  =  dec x+x ? y  =  0++0 ? x  =  x + x+x ? 0  =  x+x ? y  =  y++0 ? x  =  x + x+x ? 0  =  x+x ? y  =  0++0 ? x  =  x + x+x ? 0  =  0+x ? y  =  x++0 ? x  =  x * x+x ? 0  =  x+x ? y  =  y++0 ? x  =  x * x+x ? 0  =  x+x ? y  =  0++0 ? x  =  x * x+x ? 0  =  0+x ? y  =  x++0 ? x  =  dec (dec x)+x ? 0  =  x+x ? y  =  y++0 ? x  =  dec (dec x)+x ? 0  =  x+x ? y  =  0++0 ? x  =  dec (dec x)+x ? 0  =  0+x ? y  =  x++0 ? 0  =  0+0 ? x  =  dec x+x ? y  =  dec x+++Unique candidates for: goo :: [Int] -> [Int]+  pruning with 4/4 rules+  [2,1,1,2,4,7,10] candidates+  [2,1,1,2,3,6,10] unique candidates+  25/27 unique candidates+  2/27 redundant candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++goo xs  =  xs++goo xs  =  []++goo []  =  []+goo (x:xs)  =  xs++goo xs  =  xs ++ xs++goo []  =  []+goo (x:xs)  =  [x]++goo []  =  []+goo (x:xs)  =  xs ++ xs++goo []  =  []+goo (x:xs)  =  xs ++ goo xs++goo []  =  []+goo (x:xs)  =  goo xs ++ xs++goo xs  =  xs ++ (xs ++ xs)++goo []  =  []+goo (x:xs)  =  x:x:xs++goo []  =  []+goo (x:xs)  =  [x,x]++goo []  =  []+goo (x:xs)  =  x:(xs ++ xs)++goo []  =  []+goo (x:xs)  =  xs ++ (x:xs)++goo []  =  []+goo (x:xs)  =  xs ++ [x]++goo []  =  []+goo (x:xs)  =  xs ++ (xs ++ xs)++goo []  =  []+goo (x:xs)  =  x:x:goo xs++goo []  =  []+goo (x:xs)  =  x:(xs ++ goo xs)++goo []  =  []+goo (x:xs)  =  x:(goo xs ++ xs)++goo []  =  []+goo (x:xs)  =  xs ++ (x:goo xs)++goo []  =  []+goo (x:xs)  =  xs ++ (xs ++ goo xs)++goo []  =  []+goo (x:xs)  =  xs ++ (goo xs ++ xs)++goo []  =  []+goo (x:xs)  =  goo xs ++ (x:xs)++goo []  =  []+goo (x:xs)  =  goo xs ++ [x]++goo []  =  []+goo (x:xs)  =  goo xs ++ (xs ++ xs)++goo xs  =  xs ++ (xs ++ (xs ++ xs))+++Unique candidates for: ?? :: [Int] -> [Int] -> [Int]+  pruning with 4/4 rules+  [3,8,15,43,122] candidates+  [3,8,15,35,89] unique candidates+  150/191 unique candidates+  41/191 redundant candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++xs ?? ys  =  xs++xs ?? ys  =  ys++xs ?? ys  =  []++xs ?? []  =  xs+xs ?? (x:ys)  =  ys++xs ?? []  =  xs+xs ?? (x:ys)  =  []++xs ?? []  =  []+xs ?? (x:ys)  =  xs++xs ?? []  =  []+xs ?? (x:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  []++[] ?? xs  =  []+(x:xs) ?? ys  =  xs++[] ?? xs  =  []+(x:xs) ?? ys  =  ys++xs ?? ys  =  xs ++ xs++xs ?? ys  =  xs ++ ys++xs ?? ys  =  ys ++ xs++xs ?? ys  =  ys ++ ys++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  []++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ?? xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ?? xs++xs ?? []  =  xs+xs ?? (x:ys)  =  x:xs++xs ?? []  =  xs+xs ?? (x:ys)  =  x:ys++xs ?? []  =  xs+xs ?? (x:ys)  =  [x]++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ++ xs++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ++ ys++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ++ xs++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ++ ys++xs ?? []  =  []+xs ?? (x:ys)  =  x:xs++xs ?? []  =  []+xs ?? (x:ys)  =  [x]++xs ?? []  =  []+xs ?? (x:ys)  =  xs ++ xs++xs ?? []  =  []+xs ?? (x:ys)  =  xs ++ ys++xs ?? []  =  []+xs ?? (x:ys)  =  ys ++ xs++xs ?? []  =  []+xs ?? (x:ys)  =  ys ++ ys++xs ?? []  =  xs ++ xs+xs ?? (x:ys)  =  xs++xs ?? []  =  xs ++ xs+xs ?? (x:ys)  =  ys++xs ?? []  =  xs ++ xs+xs ?? (x:ys)  =  []++[] ?? xs  =  xs+(x:xs) ?? ys  =  x:xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  x:ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  [x]++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ++ xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ++ ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ++ xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ++ ys++[] ?? xs  =  []+(x:xs) ?? ys  =  x:ys++[] ?? xs  =  []+(x:xs) ?? ys  =  [x]++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ++ xs++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ++ ys++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ++ xs++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ++ ys++[] ?? xs  =  xs ++ xs+(x:xs) ?? ys  =  xs++[] ?? xs  =  xs ++ xs+(x:xs) ?? ys  =  ys++[] ?? xs  =  xs ++ xs+(x:xs) ?? ys  =  []++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs ?? []++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys ?? xs++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys ?? []++[] ?? xs  =  xs+(x:xs) ?? []  =  xs ?? xs+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  xs+(x:xs) ?? []  =  xs ?? xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs ?? ys++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys ?? xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs ?? ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys ?? xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs ?? xs+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs ?? xs+(x:xs) ?? (y:ys)  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  ys ?? xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  [] ?? xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs ?? xs+(x:xs) ?? ys  =  xs++xs ?? ys  =  xs ++ (xs ++ xs)++xs ?? ys  =  xs ++ (xs ++ ys)++xs ?? ys  =  xs ++ (ys ++ xs)++xs ?? ys  =  xs ++ (ys ++ ys)++xs ?? ys  =  ys ++ (xs ++ xs)++xs ?? ys  =  ys ++ (xs ++ ys)++xs ?? ys  =  ys ++ (ys ++ xs)++xs ?? ys  =  ys ++ (ys ++ ys)++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  x:xs++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  x:ys++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  [x]++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  y:xs++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  y:ys++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  [y]++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs ++ xs++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs ++ ys++[] ?? xs  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys ++ ys++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  x:xs++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  x:ys++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  [x]++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  y:xs++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  [y]++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs ++ xs++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs ++ ys++[] ?? xs  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys ++ ys++[] ?? xs  =  xs+(x:xs) ?? []  =  x:xs+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  xs+(x:xs) ?? []  =  x:xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? []  =  x:xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  xs+(x:xs) ?? []  =  [x]+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  xs+(x:xs) ?? []  =  [x]+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? []  =  [x]+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  xs+(x:xs) ?? []  =  xs ++ xs+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  xs+(x:xs) ?? []  =  xs ++ xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? []  =  xs ++ xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  x:xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  x:ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  [x]++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  y:xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  y:ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  [y]++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs ++ xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs ++ ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys ++ ys++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  x:ys++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  [x]++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  y:xs++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  [y]++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs ++ xs++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs ++ ys++[] ?? xs  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys ++ ys++[] ?? xs  =  []+(x:xs) ?? []  =  x:xs+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  []+(x:xs) ?? []  =  x:xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  []+(x:xs) ?? []  =  [x]+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  []+(x:xs) ?? []  =  [x]+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  []+(x:xs) ?? []  =  [x]+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  []+(x:xs) ?? []  =  xs ++ xs+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  []+(x:xs) ?? []  =  xs ++ xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  []+(x:xs) ?? []  =  xs ++ xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  xs ++ xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys++[] ?? xs  =  xs ++ xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  []++[] ?? xs  =  xs ++ xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs++[] ?? xs  =  xs ++ xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  x:xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  x:ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  [x]++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  xs ++ xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  xs ++ ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  ys ++ xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? ys  =  ys ++ ys++[] ?? []  =  []+[] ?? (x:xs)  =  [x]+(x:xs) ?? ys  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  [x]+(x:xs) ?? ys  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  [x]+(x:xs) ?? ys  =  []++[] ?? []  =  []+[] ?? (x:xs)  =  xs ++ xs+(x:xs) ?? ys  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs ++ xs+(x:xs) ?? ys  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs ++ xs+(x:xs) ?? ys  =  []+++Unique candidates for: ton :: Bool -> Bool+  pruning with 39/49 rules+  [3,2,0,0,0,0,0] candidates+  [3,1,0,0,0,0,0] unique candidates+  4/5 unique candidates+  1/5 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++ton p  =  p++ton p  =  False++ton p  =  True++ton p  =  not p+++Unique candidates for: &| :: Bool -> Bool -> Bool+  pruning with 39/49 rules+  [4,12,20,6,2] candidates+  [4,8,4,0,0] unique candidates+  16/44 unique candidates+  28/44 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++p &| q  =  p++p &| q  =  q++p &| q  =  False++p &| q  =  True++p &| q  =  not p++p &| q  =  not q++p &| False  =  p+p &| True  =  False++p &| False  =  p+p &| True  =  True++p &| False  =  False+p &| True  =  p++p &| False  =  True+p &| True  =  p++False &| p  =  p+True &| p  =  False++False &| p  =  True+True &| p  =  p++p &| False  =  p+p &| True  =  not p++p &| False  =  True+p &| True  =  not p++p &| False  =  not p+p &| True  =  p++p &| False  =  not p+p &| True  =  False++

@@ -18,11 +18,11 @@ -- looking through 0 candidates of size 4 -- looking through 39 candidates of size 5 -- looking through 60 candidates of size 6--- looking through 225 candidates of size 7--- looking through 1056 candidates of size 8--- looking through 1488 candidates of size 9--- looking through 13020 candidates of size 10--- tested 7148 candidates+-- looking through 222 candidates of size 7+-- looking through 996 candidates of size 8+-- looking through 1266 candidates of size 9+-- looking through 11700 candidates of size 10+-- tested 6683 candidates x ^^^ y  =  if 0 == x * y             then x + y             else 0

@@ -2,6 +2,15 @@ ============================  +v0.5.14 (February 2024)+-----------------------++* improve commutative pruning, slightly faster Conjure+* add `carryOn`, `rewriting`, `requireDescent`, `adHocRedundancy` switches+  to the `Args` record+* add more benchmarks and tests++ v0.5.12 (February 2024) ----------------------- 

@@ -3,7 +3,7 @@ -- Copyright (C) 2021-2024 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name:                code-conjure-version:             0.5.12+version:             0.5.14 synopsis:            synthesize Haskell functions out of partial definitions description:   Conjure is a tool that synthesizes Haskell functions out of partial definitions.@@ -67,7 +67,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/conjure-  tag:             v0.5.12+  tag:             v0.5.14  library   exposed-modules: Conjure

@@ -12,7 +12,7 @@ -- looking through 92 candidates of size 9 -- looking through 0 candidates of size 10 -- looking through 304 candidates of size 11--- looking through 199 candidates of size 12+-- looking through 151 candidates of size 12 -- tested 497 candidates mem x Leaf  =  False mem x (Node t1 y t2)  =  mem x t1 || (mem x t2 || x == y)

@@ -7,7 +7,7 @@ -- looking through 8 candidates of size 4 -- looking through 28 candidates of size 5 -- looking through 35 candidates of size 6--- looking through 179 candidates of size 7+-- looking through 167 candidates of size 7 -- tested 95 candidates factorial 0  =  1 factorial x  =  x * factorial (x - 1)

@@ -18,10 +18,10 @@ -- looking through 16 candidates of size 4 -- looking through 44 candidates of size 5 -- looking through 92 candidates of size 6--- looking through 234 candidates of size 7--- looking through 544 candidates of size 8--- looking through 1332 candidates of size 9--- looking through 10676 candidates of size 10--- tested 12956 candidates+-- looking through 210 candidates of size 7+-- looking through 520 candidates of size 8+-- looking through 1197 candidates of size 9+-- looking through 10436 candidates of size 10+-- tested 12533 candidates cannot conjure 

@@ -5,15 +5,15 @@ -- looking through 3 candidates of size 2 -- looking through 9 candidates of size 3 -- looking through 9 candidates of size 4--- looking through 30 candidates of size 5--- looking through 30 candidates of size 6--- looking through 156 candidates of size 7--- looking through 157 candidates of size 8--- looking through 813 candidates of size 9--- looking through 797 candidates of size 10--- looking through 4449 candidates of size 11--- looking through 4438 candidates of size 12--- tested 6539 candidates+-- looking through 26 candidates of size 5+-- looking through 27 candidates of size 6+-- looking through 116 candidates of size 7+-- looking through 120 candidates of size 8+-- looking through 552 candidates of size 9+-- looking through 540 candidates of size 10+-- looking through 2663 candidates of size 11+-- looking through 2675 candidates of size 12+-- tested 4147 candidates fibonacci 0  =  1 fibonacci 1  =  1 fibonacci x  =  fibonacci (x - 1) + fibonacci (x - 2)

@@ -105,9 +105,9 @@ -- looking through 20 candidates of size 7 -- looking through 30 candidates of size 8 -- looking through 56 candidates of size 9--- looking through 114 candidates of size 10--- looking through 216 candidates of size 11--- tested 331 candidates+-- looking through 112 candidates of size 10+-- looking through 200 candidates of size 11+-- tested 319 candidates ordered []  =  True ordered (x:xs)  =  ordered xs && (null xs || x <= head xs) 

@@ -35,8 +35,8 @@ -- looking through 0 candidates of size 2 -- looking through 3 candidates of size 3 -- looking through 1 candidates of size 4--- looking through 50 candidates of size 5--- tested 35 candidates+-- looking through 46 candidates of size 5+-- tested 31 candidates odd x  =  1 == x `mod` 2  even :: Int -> Bool@@ -46,7 +46,7 @@ -- looking through 0 candidates of size 2 -- looking through 3 candidates of size 3 -- looking through 2 candidates of size 4--- looking through 49 candidates of size 5--- tested 26 candidates+-- looking through 45 candidates of size 5+-- tested 22 candidates even x  =  0 == x `mod` 2 

@@ -7,9 +7,9 @@ -- looking through 159 candidates of size 4 -- looking through 433 candidates of size 5 -- looking through 1382 candidates of size 6--- looking through 4156 candidates of size 7--- looking through 13406 candidates of size 8--- tested 6403 candidates+-- looking through 4136 candidates of size 7+-- looking through 13292 candidates of size 8+-- tested 6383 candidates pow x 0  =  1 pow x y  =  x * pow x (y - 1) 

@@ -74,6 +74,7 @@   -- merge (x:xs) (y:ys)  =  if x <= y then x:merge xs (y:ys) else y:merge (x:xs) ys   --                         2  3 4  5      678     9 10 11 12  13 14 15  16 17 18 19   -- OOM after size 17, out of reach performance wise+  -- update: cannot reach at size 19 on lapmatrud OOM   conjureWith args{maxSize=12} "merge" merge'     [ pr ([] :: [Int])     , prim ":" ((:) :: Int -> [Int] -> [Int])

@@ -55,7 +55,7 @@ -- looking through 14 candidates of size 5 -- looking through 34 candidates of size 6 -- looking through 98 candidates of size 7--- looking through 283 candidates of size 8+-- looking through 274 candidates of size 8 -- tested 200 candidates height Leaf  =  -1 height (Node t1 x t2)  =  1 + max (height t1) (height t2)@@ -74,7 +74,7 @@ -- looking through 0 candidates of size 9 -- looking through 0 candidates of size 10 -- looking through 0 candidates of size 11--- looking through 96 candidates of size 12+-- looking through 80 candidates of size 12 -- tested 88 candidates mem x Leaf  =  False mem x (Node t1 y t2)  =  mem x t1 || (mem x t2 || x == y)@@ -92,9 +92,9 @@ -- looking through 32 candidates of size 8 -- looking through 80 candidates of size 9 -- looking through 56 candidates of size 10--- looking through 450 candidates of size 11--- looking through 708 candidates of size 12--- tested 1359 candidates+-- looking through 386 candidates of size 11+-- looking through 596 candidates of size 12+-- tested 1183 candidates cannot conjure  ordered :: Tree -> Bool

@@ -20,6 +20,23 @@   src/Conjure/Conjurable.hs \   src/Conjure/Conjurable/Derive.hs \   bench/candidates.hs+bench/carry-on: \+  bench/carry-on.hs \+  mk/toplibs+bench/carry-on.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Red.hs \+  src/Conjure/Reason.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn/Test.hs \+  src/Conjure/Defn/Redundancy.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  src/Conjure/Conjurable/Derive.hs \+  bench/carry-on.hs bench/erroneous: \   bench/erroneous.hs \   mk/toplibs@@ -190,6 +207,23 @@   src/Conjure/Conjurable.hs \   src/Conjure/Conjurable/Derive.hs \   bench/self.hs+bench/strategies: \+  bench/strategies.hs \+  mk/toplibs+bench/strategies.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Red.hs \+  src/Conjure/Reason.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn/Test.hs \+  src/Conjure/Defn/Redundancy.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  src/Conjure/Conjurable/Derive.hs \+  bench/strategies.hs bench/take-drop: \   bench/take-drop.hs \   mk/toplibs@@ -224,6 +258,23 @@   src/Conjure/Conjurable.hs \   src/Conjure/Conjurable/Derive.hs \   bench/terpret.hs+bench/unique: \+  bench/unique.hs \+  mk/toplibs+bench/unique.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Red.hs \+  src/Conjure/Reason.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn/Test.hs \+  src/Conjure/Defn/Redundancy.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  src/Conjure/Conjurable/Derive.hs \+  bench/unique.hs bench/weird: \   bench/weird.hs \   mk/toplibs

@@ -141,7 +141,7 @@ -- | Returns whether a given 'Defn' is redundant --   with regards to root recursions. ----- When there is a single base case and all recursive calls+-- When there is a single constant base case and all recursive calls -- are at the root: we have a redundant function. -- (Modulo error functions, which are undesired anyway.) --@@ -150,11 +150,6 @@ -- -- Above it does not really pays off to follow the recursive calls, -- at the end we always reach an empty list.------ The same goes for the following:------ > xs ? []  =  xs--- > xs ? (x:ys)  =  xs ? ys isRedundantByRootRecursions :: Defn -> Bool isRedundantByRootRecursions d  =  case partition isGround $ map snd d of   ([b], rs@(_:_))  ->  all isHole rs

@@ -159,11 +159,18 @@   , maxEquationSize       :: Int  -- ^ maximum size of equation operands   , maxSearchTests        :: Int  -- ^ maximum number of tests to search for defined values   , maxDeconstructionSize :: Int  -- ^ maximum size of deconstructions (e.g.: @_ - 1@)-  , requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments++  -- advanced options --+  , carryOn               :: Bool -- ^ whether to carry on after finding a suitable candidate+  , showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning   , usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates++  -- pruning options --+  , rewriting             :: Bool -- ^ unique-modulo-rewriting candidates+  , requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments+  , adHocRedundancy       :: Bool -- ^ ad-hoc redundancy checks   , copyBindings          :: Bool -- ^ copy partial definition bindings in candidates   , atomicNumbers         :: Bool -- ^ restrict constant/ground numeric expressions to atoms-  , showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning   , uniqueCandidates      :: Bool -- ^ unique-modulo-testing candidates   } @@ -187,11 +194,18 @@   , maxEquationSize        =   5   , maxSearchTests         =  100000   , maxDeconstructionSize  =   4-  , requireDescent         =  True++  -- advanced options --+  , carryOn                =  False+  , showTheory             =  False   , usePatterns            =  True++  -- pruning options --+  , rewriting              =  True+  , requireDescent         =  True+  , adHocRedundancy        =  True   , copyBindings           =  True   , atomicNumbers          =  True-  , showTheory             =  False   , uniqueCandidates       =  False   } @@ -239,9 +253,15 @@     -- when (n<=12) $ putStrLn $ unlines $ map showDefn cs     case is of       []     ->  pr (n+1) (t+nc) rs-      (i:_)  ->  do let nc' = fromMaybe nc (findIndex (i==) cs)-                    putStrLn $ "-- tested " ++ show (t+nc'+1) ++ " candidates"-                    putStrLn $ showDefn i+      (_:_)  ->  do pr1 t is cs+                    when (carryOn args) $ pr (n+1) (t+nc) rs+  pr1 t [] cs  =  return ()+  pr1 t (i:is) cs  =  do+    let (cs',cs'') = break (i==) cs+    let t' = t + length cs' + 1+    putStrLn $ "-- tested " ++ show t' ++ " candidates"+    putStrLn $ showDefn i+    when (carryOn args) $ pr1 t' is (drop 1 cs'')   rs  =  zip iss css   (iss, css, ts, thy)  =  conjpure0With args nm f p es   nRules  =  length (rules thy)@@ -363,7 +383,8 @@   eh  =  holeAsTypeOf efxs   efxs  =  conjureVarApplication nm f   (ef:exs)  =  unfoldApp efxs-  keep  =  isRootNormalC thy . fastMostGeneralVariation+  keep | rewriting  =  isRootNormalC thy . fastMostGeneralVariation+       | otherwise  =  const True   keepR | requireDescent  =  descends isDecOf efxs         | otherwise       =  const True     where@@ -391,7 +412,7 @@ -- | Return apparently unique candidate definitions --   using pattern matching. candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)-candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundantRecursion $ concatMapT fillingsFor fss,thy)+candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundant $ concatMapT fillingsFor fss,thy)   where   pats  =  conjurePats es nm f   fss  =  concatMapT ps2fss pats@@ -401,7 +422,8 @@   efxs  =  conjureVarApplication nm f   (ef:exs)  =  unfoldApp efxs -  keep  =  isRootNormalC thy . fastMostGeneralVariation+  keep | rewriting  =  isRootNormalC thy . fastMostGeneralVariation+       | otherwise  =  const True    appsWith :: Expr -> [Expr] -> [[Expr]]   appsWith eh vs  =  enumerateAppsFor eh k $ vs ++ es@@ -411,9 +433,14 @@     -- discards non-atomic numeric ground expressions such as 1 + 1     keepNumeric e  =  isFun e || isConst e || not (isGround e) +  isRedundant | adHocRedundancy  =  \e -> isRedundantDefn e || isRedundantModuloRewriting (normalize thy) e+              | otherwise        =  const False++  hasRedundant | adHocRedundancy  =  hasRedundantRecursion+               | otherwise        =  const False+   ps2fss :: [Expr] -> [[Defn]]-  ps2fss pats  =  discardT (isRedundantModuloRewriting $ normalize thy)-               .  discardT isRedundantDefn+  ps2fss pats  =  discardT isRedundant                .  products                $  map p2eess pats     where

@@ -55,10 +55,7 @@ -- but nevertheless correct isRootNormalC :: Thy -> Expr -> Bool isRootNormalC thy e | not (isRootNormal thy e)  =  False-isRootNormalC thy (ef :$ ex :$ ey)-  | ex <= ey  =  True-  | not (isCommutative thy ef)  =  True-  | isRootNormal thy (ef :$ ey :$ ex)  =  False+isRootNormalC thy (ef :$ ex :$ ey) | isCommutative thy ef  =  ex <= ey isRootNormalC _ _  =  True  isRootNormalE :: Thy -> Expr -> Bool