diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -55,6 +55,8 @@
 eg/subset
 eg/spec
 eg/colin/*Funs
+eg/tri
+eg/bits
 bench/carry-on
 bench/strategies
 bench/self
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -45,6 +45,8 @@
   eg/tapps \
   eg/tree \
   eg/bst \
+  eg/tri \
+  eg/bits \
   bench/candidates \
   bench/redundants \
   bench/erroneous \
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,9 +3,99 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
+* forbid recursion into negatives
+
 * consider the size of patterns to thin-out each size partition
 
 * consider non top-level cases
+
+
+## Forbid recursion into negatives
+
+Instead of reporting:
+
+	tri 1  =  1
+	tri x  =  x + tri (x - 1)
+
+Report:
+
+	tri 1          =  1
+	tri x | x > 1  =  x + tri (x - 1)
+
+This is not trivial to implement.
+Tentative steps:
+
+1. create a `descents` function, similar to `descends`,
+   that is able to list the groups of variable that have recursive descents.
+   This will somehow need a dummy `isDecOf` function.
+   This may require changing the format definitions themselves...
+2. use this on `showDefn` somehow
+3. use this on `toDynamicWithDefn` somehow
+
+
+## Thin-out size partitions
+
+Consider the following two candidates:
+
+	fib01 x y z  =  dec x
+
+	fib01 x y 0  =  x
+	fib01 x y z  =  y
+
+They both currently have size 2.
+Perhaps the second should be bigger than the first?
+"Simple" solution:
+consider the number of (extra) patterns as part of the size.
+
+See the following two candidates of size 3:
+
+	fib01 x y z  =  x + x
+
+	fib01 x y 0  =  x
+	fib01 x y z  =  dec x
+
+The same thing can be said.
+
+Now a little bit more complex...
+The following two candidates appear at size 3 for fib01:
+
+	fib01 x 0 y  =  x
+	fib01 x y 0  =  y
+	fib01 x y z  =  0
+
+	fib01 x 0 0  =  x
+	fib01 x 0 y  =  y
+	fib01 x y z  =  0
+
+Shouldn't these two have different size?
+The second feels bigger than the first.
+Maybe the size of non-variable patterns should be taken into account.
+
+This relates to the eg/fib01 example.
+
+Also:
+see the allowed patterns on the Int functions of two arguments
+in bench/candidates.txt.  Search for "allowed patterns".
+
+There are two levels here:
+
+1. considering the number of patterns as part of the size
+2. considering the number of non-variable LHS arguments as part of the size
+
+Level 2. is not addressed at all.  But it turns out that level 1. is already
+handled at the conjurePatterns function.  The patterns reported with showPatterns
+and on bench/candidates already seem to be divided considering the number of
+lines...
+
+Something to keep in mind: tiers enumerations have size "0".
+If one wants to increase size, one needs to push things to size "1".
+So the size is actually being considered.  One would need a delayedProducts to
+complete "1.".  Maybe it is better to start investigating from "2."
+
+The enumeration currently works like so:
+the size of patterns is defined by the number of patterns that are allowed to
+have _another_ option other than a simple variable.
+Perhaps these should be thinned-out in post processing to achieve "2."?
 
 
 ## Non top-level cases
diff --git a/bench/candidates.hs b/bench/candidates.hs
--- a/bench/candidates.hs
+++ b/bench/candidates.hs
@@ -19,6 +19,12 @@
   putStrLn $ unlines $ map showDefn $ concat $ take n $ css1
   putStrLn $ "pattern candidates:\n"
   putStrLn $ unlines $ map showDefn $ concat $ take n $ cssC
+  putStrLn ""
+  putStrLn $ "allowed patterns:\n"
+  putStrLn $ unlines $ map unlines $ map (map showDefn) $ pss
+  putStrLn ""
+  putStrLn $ "allowed deconstructions:\n"
+  putStrLn $ unlines $ map show ds
   where
   nd1  =  length cs1 - length (nubSort cs1)
   ndC  =  length csC - length (nubSort csC)
@@ -26,8 +32,8 @@
   csC  =  concat cssC
   css1  =  take m css1'
   cssC  =  take m cssC'
-  (css1', thy, _)  =  candidateDefns1 args nm f ps
-  (cssC', _, _)    =  candidateDefnsC args nm f ps
+  (css1', thy, _, _)  =  candidateDefns1 args nm f ps
+  (cssC', _, pss, ds)  =  candidateDefnsC args nm f ps
   nRules  =  length (rules thy)
   nREs  =  length (equations thy) + nRules
 
diff --git a/bench/candidates.txt b/bench/candidates.txt
--- a/bench/candidates.txt
+++ b/bench/candidates.txt
@@ -1,7 +1,7 @@
 Candidates for: foo :: Int -> Int
   pruning with 27/65 rules
   [3,0,8,0,30,0,177,0,1203] direct candidates, 0 duplicates
-  [3,3,9,10,32,39,185,217,1169] pattern candidates, 0 duplicates
+  [3,3,9,10,32,39,185,233,1169] pattern candidates, 0 duplicates
 
 rules:
 x - x == 0
@@ -428,6 +428,31 @@
 foo x  =  0 - x
 
 
+
+allowed patterns:
+
+foo x  =  _
+
+
+foo 0  =  _
+foo x  =  _
+
+
+foo 1  =  _
+foo x  =  _
+
+
+foo 0  =  _
+foo 1  =  _
+foo x  =  _
+
+
+
+
+allowed deconstructions:
+
+_ - 1 :: Int
+
 Candidates for: ? :: Int -> Int -> Int
   pruning with 13/34 rules
   [3,3,9,18,60,162,489,1475,4619] direct candidates, 0 duplicates
@@ -1586,6 +1611,42 @@
 x ? y  =  dec x
 
 
+
+allowed patterns:
+
+x ? y  =  _
+
+
+x ? 0  =  _
+x ? y  =  _
+
+0 ? x  =  _
+x ? y  =  _
+
+
+0 ? x  =  _
+x ? 0  =  _
+x ? y  =  _
+
+0 ? 0  =  _
+0 ? x  =  _
+x ? y  =  _
+
+
+0 ? 0  =  _
+0 ? x  =  _
+x ? 0  =  _
+x ? y  =  _
+
+
+
+
+allowed deconstructions:
+
+dec _ :: Int
+dec (dec _) :: Int
+dec (dec (dec _)) :: Int
+
 Candidates for: goo :: [Int] -> [Int]
   pruning with 4/4 rules
   [2,0,1,0,1,0,1,0,1] direct candidates, 0 duplicates
@@ -1661,6 +1722,21 @@
 goo (x:xs)  =  xs ++ (xs ++ xs)
 
 
+
+allowed patterns:
+
+goo xs  =  _
+
+
+goo []  =  _
+goo (x:xs)  =  _
+
+
+
+
+allowed deconstructions:
+
+
 Candidates for: ?? :: [Int] -> [Int] -> [Int]
   pruning with 4/4 rules
   [3,0,4,0,8,0,16,0,32] direct candidates, 0 duplicates
@@ -3307,6 +3383,39 @@
 (x:xs) ?? (y:ys)  =  []
 
 
+
+allowed patterns:
+
+xs ?? ys  =  _
+
+
+xs ?? []  =  _
+xs ?? (x:ys)  =  _
+
+[] ?? xs  =  _
+(x:xs) ?? ys  =  _
+
+
+[] ?? xs  =  _
+(x:xs) ?? []  =  _
+(x:xs) ?? (y:ys)  =  _
+
+[] ?? []  =  _
+[] ?? (x:xs)  =  _
+(x:xs) ?? ys  =  _
+
+
+[] ?? []  =  _
+[] ?? (x:xs)  =  _
+(x:xs) ?? []  =  _
+(x:xs) ?? (y:ys)  =  _
+
+
+
+
+allowed deconstructions:
+
+
 Candidates for: ton :: Bool -> Bool
   pruning with 39/49 rules
   [3,1,0,0,0,0,0,0,0] direct candidates, 0 duplicates
@@ -3392,6 +3501,21 @@
 ton True  =  False
 
 
+
+allowed patterns:
+
+ton p  =  _
+
+
+ton False  =  _
+ton True  =  _
+
+
+
+
+allowed deconstructions:
+
+
 Candidates for: &| :: Bool -> Bool -> Bool
   pruning with 39/49 rules
   [4,2,2,4,2,16,17,56,110] direct candidates, 0 duplicates
@@ -3721,6 +3845,39 @@
 p &| q  =  not q || (p || q)
 
 
+
+allowed patterns:
+
+p &| q  =  _
+
+
+p &| False  =  _
+p &| True  =  _
+
+False &| p  =  _
+True &| p  =  _
+
+
+False &| p  =  _
+True &| False  =  _
+True &| True  =  _
+
+False &| False  =  _
+False &| True  =  _
+True &| p  =  _
+
+
+False &| False  =  _
+False &| True  =  _
+True &| False  =  _
+True &| True  =  _
+
+
+
+
+allowed deconstructions:
+
+
 Candidates for: gcd :: Int -> Int -> Int
   pruning with 0/0 rules
   [3,0,9,0,54,0,405,0,3402] direct candidates, 0 duplicates
@@ -5353,4 +5510,38 @@
 gcd 0 x  =  0 `mod` (0 `mod` x)
 gcd x y  =  0
 
+
+
+allowed patterns:
+
+gcd x y  =  _
+
+
+gcd x 0  =  _
+gcd x y  =  _
+
+gcd 0 x  =  _
+gcd x y  =  _
+
+
+gcd 0 x  =  _
+gcd x 0  =  _
+gcd x y  =  _
+
+gcd 0 0  =  _
+gcd 0 x  =  _
+gcd x y  =  _
+
+
+gcd 0 0  =  _
+gcd 0 x  =  _
+gcd x 0  =  _
+gcd x y  =  _
+
+
+
+
+allowed deconstructions:
+
+x `mod` _ :: Int
 
diff --git a/bench/carry-on.txt b/bench/carry-on.txt
--- a/bench/carry-on.txt
+++ b/bench/carry-on.txt
@@ -12,32 +12,36 @@
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
--- looking through 195 candidates of size 8
+-- 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 539 candidates
+-- tested 547 candidates
 factorial 0  =  0
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- tested 547 candidates
+-- tested 555 candidates
 factorial 0  =  1
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- looking through 1256 candidates of size 10
--- looking through 7198 candidates of size 11
--- tested 3160 candidates
+-- 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 3340 candidates
+-- tested 3396 candidates
 factorial 0  =  1
 factorial x  =  x - x * (1 - factorial (x - 1))
 
--- tested 3463 candidates
+-- tested 3519 candidates
 factorial 0  =  1
 factorial x  =  (0 - x) * (0 - factorial (x - 1))
 
--- tested 9948 candidates
+-- tested 10004 candidates
 cannot conjure
 
diff --git a/bench/erroneous.hs b/bench/erroneous.hs
--- a/bench/erroneous.hs
+++ b/bench/erroneous.hs
@@ -40,7 +40,7 @@
   css            =  take n
                  .  discardT isRedundantByIntroduction -- additional pruning rule
                  $  css'
-  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  (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
diff --git a/bench/gps.txt b/bench/gps.txt
--- a/bench/gps.txt
+++ b/bench/gps.txt
@@ -305,9 +305,9 @@
 -- looking through 28 candidates of size 5
 -- looking through 35 candidates of size 6
 -- looking through 167 candidates of size 7
--- looking through 195 candidates of size 8
+-- looking through 203 candidates of size 8
 -- looking through 1048 candidates of size 9
--- tested 458 candidates
+-- tested 466 candidates
 gps17 0  =  0
 gps17 x  =  gps17 (x - 1) + x * x
 
diff --git a/bench/gps2.txt b/bench/gps2.txt
--- a/bench/gps2.txt
+++ b/bench/gps2.txt
@@ -320,13 +320,13 @@
 -- looking through 3 candidates of size 4
 -- looking through 11 candidates of size 5
 -- looking through 13 candidates of size 6
--- looking through 85 candidates of size 7
+-- looking through 91 candidates of size 7
 -- looking through 104 candidates of size 8
--- looking through 811 candidates of size 9
+-- looking through 850 candidates of size 9
 -- looking through 923 candidates of size 10
--- looking through 8602 candidates of size 11
+-- looking through 8902 candidates of size 11
 -- looking through 9662 candidates of size 12
--- tested 20217 candidates
+-- tested 20562 candidates
 cannot conjure
 
 gps22 :: Int -> [Char]
diff --git a/bench/p12.txt b/bench/p12.txt
--- a/bench/p12.txt
+++ b/bench/p12.txt
@@ -7,7 +7,7 @@
 -- looking through 6 candidates of size 3
 -- looking through 13 candidates of size 4
 -- looking through 40 candidates of size 5
--- looking through 137 candidates of size 6
+-- looking through 138 candidates of size 6
 -- tested 69 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (dec x)
diff --git a/bench/redundants.hs b/bench/redundants.hs
--- a/bench/redundants.hs
+++ b/bench/redundants.hs
@@ -40,7 +40,7 @@
   css            =  take n
                  .  discardT isRedundantByIntroduction -- additional pruning rule
                  $  css'
-  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  (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
diff --git a/bench/runtime/lapmatrud/bench/candidates.runtime b/bench/runtime/lapmatrud/bench/candidates.runtime
--- a/bench/runtime/lapmatrud/bench/candidates.runtime
+++ b/bench/runtime/lapmatrud/bench/candidates.runtime
@@ -1,1 +1,1 @@
-9.5
+9.2
diff --git a/bench/runtime/lapmatrud/bench/carry-on.runtime b/bench/runtime/lapmatrud/bench/carry-on.runtime
--- a/bench/runtime/lapmatrud/bench/carry-on.runtime
+++ b/bench/runtime/lapmatrud/bench/carry-on.runtime
@@ -1,1 +1,1 @@
-1.8
+2.4
diff --git a/bench/runtime/lapmatrud/bench/gps.runtime b/bench/runtime/lapmatrud/bench/gps.runtime
--- a/bench/runtime/lapmatrud/bench/gps.runtime
+++ b/bench/runtime/lapmatrud/bench/gps.runtime
@@ -1,1 +1,1 @@
-13.7
+14.3
diff --git a/bench/runtime/lapmatrud/bench/gps2.runtime b/bench/runtime/lapmatrud/bench/gps2.runtime
--- a/bench/runtime/lapmatrud/bench/gps2.runtime
+++ b/bench/runtime/lapmatrud/bench/gps2.runtime
@@ -1,1 +1,1 @@
-11.6
+11.9
diff --git a/bench/runtime/lapmatrud/bench/unique.runtime b/bench/runtime/lapmatrud/bench/unique.runtime
--- a/bench/runtime/lapmatrud/bench/unique.runtime
+++ b/bench/runtime/lapmatrud/bench/unique.runtime
@@ -1,1 +1,1 @@
-2.1
+2.2
diff --git a/bench/runtime/lapmatrud/eg/arith.runtime b/bench/runtime/lapmatrud/eg/arith.runtime
--- a/bench/runtime/lapmatrud/eg/arith.runtime
+++ b/bench/runtime/lapmatrud/eg/arith.runtime
@@ -1,1 +1,1 @@
-0.9
+1.0
diff --git a/bench/runtime/lapmatrud/eg/bits.runtime b/bench/runtime/lapmatrud/eg/bits.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/eg/bits.runtime
@@ -0,0 +1,1 @@
+2.8
diff --git a/bench/runtime/lapmatrud/eg/bools.runtime b/bench/runtime/lapmatrud/eg/bools.runtime
--- a/bench/runtime/lapmatrud/eg/bools.runtime
+++ b/bench/runtime/lapmatrud/eg/bools.runtime
@@ -1,1 +1,1 @@
-1.3
+1.4
diff --git a/bench/runtime/lapmatrud/eg/bst.runtime b/bench/runtime/lapmatrud/eg/bst.runtime
--- a/bench/runtime/lapmatrud/eg/bst.runtime
+++ b/bench/runtime/lapmatrud/eg/bst.runtime
@@ -1,1 +1,1 @@
-7.6
+7.5
diff --git a/bench/runtime/lapmatrud/eg/dupos.runtime b/bench/runtime/lapmatrud/eg/dupos.runtime
--- a/bench/runtime/lapmatrud/eg/dupos.runtime
+++ b/bench/runtime/lapmatrud/eg/dupos.runtime
@@ -1,1 +1,1 @@
-3.2
+3.4
diff --git a/bench/runtime/lapmatrud/eg/fib01.runtime b/bench/runtime/lapmatrud/eg/fib01.runtime
--- a/bench/runtime/lapmatrud/eg/fib01.runtime
+++ b/bench/runtime/lapmatrud/eg/fib01.runtime
@@ -1,1 +1,1 @@
-1.4
+0.8
diff --git a/bench/runtime/lapmatrud/eg/fibonacci.runtime b/bench/runtime/lapmatrud/eg/fibonacci.runtime
--- a/bench/runtime/lapmatrud/eg/fibonacci.runtime
+++ b/bench/runtime/lapmatrud/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-2.8
+3.3
diff --git a/bench/runtime/lapmatrud/eg/ints.runtime b/bench/runtime/lapmatrud/eg/ints.runtime
--- a/bench/runtime/lapmatrud/eg/ints.runtime
+++ b/bench/runtime/lapmatrud/eg/ints.runtime
@@ -1,1 +1,1 @@
-0.7
+0.5
diff --git a/bench/runtime/lapmatrud/eg/pow.runtime b/bench/runtime/lapmatrud/eg/pow.runtime
--- a/bench/runtime/lapmatrud/eg/pow.runtime
+++ b/bench/runtime/lapmatrud/eg/pow.runtime
@@ -1,1 +1,1 @@
-3.5
+4.1
diff --git a/bench/runtime/lapmatrud/eg/tri.runtime b/bench/runtime/lapmatrud/eg/tri.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/eg/tri.runtime
@@ -0,0 +1,1 @@
+0.2
diff --git a/bench/runtime/zero/bench/candidates.runtime b/bench/runtime/zero/bench/candidates.runtime
--- a/bench/runtime/zero/bench/candidates.runtime
+++ b/bench/runtime/zero/bench/candidates.runtime
@@ -1,1 +1,1 @@
-16.7
+16.1
diff --git a/bench/runtime/zero/bench/carry-on.runtime b/bench/runtime/zero/bench/carry-on.runtime
--- a/bench/runtime/zero/bench/carry-on.runtime
+++ b/bench/runtime/zero/bench/carry-on.runtime
@@ -1,1 +1,1 @@
-3.5
+4.3
diff --git a/bench/runtime/zero/bench/erroneous.runtime b/bench/runtime/zero/bench/erroneous.runtime
--- a/bench/runtime/zero/bench/erroneous.runtime
+++ b/bench/runtime/zero/bench/erroneous.runtime
@@ -1,1 +1,1 @@
-5.1
+4.8
diff --git a/bench/runtime/zero/bench/gps.runtime b/bench/runtime/zero/bench/gps.runtime
--- a/bench/runtime/zero/bench/gps.runtime
+++ b/bench/runtime/zero/bench/gps.runtime
@@ -1,1 +1,1 @@
-25.3
+25.6
diff --git a/bench/runtime/zero/bench/gps2.runtime b/bench/runtime/zero/bench/gps2.runtime
--- a/bench/runtime/zero/bench/gps2.runtime
+++ b/bench/runtime/zero/bench/gps2.runtime
@@ -1,1 +1,1 @@
-21.1
+22.9
diff --git a/bench/runtime/zero/bench/p12.runtime b/bench/runtime/zero/bench/p12.runtime
--- a/bench/runtime/zero/bench/p12.runtime
+++ b/bench/runtime/zero/bench/p12.runtime
@@ -1,1 +1,1 @@
-3.0
+2.9
diff --git a/bench/runtime/zero/bench/redundants.runtime b/bench/runtime/zero/bench/redundants.runtime
--- a/bench/runtime/zero/bench/redundants.runtime
+++ b/bench/runtime/zero/bench/redundants.runtime
@@ -1,1 +1,1 @@
-5.7
+5.6
diff --git a/bench/runtime/zero/bench/strategies.runtime b/bench/runtime/zero/bench/strategies.runtime
--- a/bench/runtime/zero/bench/strategies.runtime
+++ b/bench/runtime/zero/bench/strategies.runtime
@@ -1,1 +1,1 @@
-8.2
+8.0
diff --git a/bench/runtime/zero/bench/terpret.runtime b/bench/runtime/zero/bench/terpret.runtime
--- a/bench/runtime/zero/bench/terpret.runtime
+++ b/bench/runtime/zero/bench/terpret.runtime
@@ -1,1 +1,1 @@
-14.1
+13.6
diff --git a/bench/runtime/zero/bench/unique.runtime b/bench/runtime/zero/bench/unique.runtime
--- a/bench/runtime/zero/bench/unique.runtime
+++ b/bench/runtime/zero/bench/unique.runtime
@@ -1,1 +1,1 @@
-4.3
+4.0
diff --git a/bench/runtime/zero/bench/weird.runtime b/bench/runtime/zero/bench/weird.runtime
--- a/bench/runtime/zero/bench/weird.runtime
+++ b/bench/runtime/zero/bench/weird.runtime
@@ -1,1 +1,1 @@
-4.9
+4.6
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
--- a/bench/runtime/zero/eg/arith.runtime
+++ b/bench/runtime/zero/eg/arith.runtime
@@ -1,1 +1,1 @@
-1.9
+1.7
diff --git a/bench/runtime/zero/eg/bits.runtime b/bench/runtime/zero/eg/bits.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/bits.runtime
@@ -0,0 +1,1 @@
+5.6
diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime
--- a/bench/runtime/zero/eg/bools.runtime
+++ b/bench/runtime/zero/eg/bools.runtime
@@ -1,1 +1,1 @@
-3.4
+2.6
diff --git a/bench/runtime/zero/eg/bst.runtime b/bench/runtime/zero/eg/bst.runtime
--- a/bench/runtime/zero/eg/bst.runtime
+++ b/bench/runtime/zero/eg/bst.runtime
@@ -1,1 +1,1 @@
-14.4
+13.8
diff --git a/bench/runtime/zero/eg/count.runtime b/bench/runtime/zero/eg/count.runtime
--- a/bench/runtime/zero/eg/count.runtime
+++ b/bench/runtime/zero/eg/count.runtime
@@ -1,1 +1,1 @@
-0.7
+0.5
diff --git a/bench/runtime/zero/eg/dupos.runtime b/bench/runtime/zero/eg/dupos.runtime
--- a/bench/runtime/zero/eg/dupos.runtime
+++ b/bench/runtime/zero/eg/dupos.runtime
@@ -1,1 +1,1 @@
-6.6
+6.2
diff --git a/bench/runtime/zero/eg/either.runtime b/bench/runtime/zero/eg/either.runtime
--- a/bench/runtime/zero/eg/either.runtime
+++ b/bench/runtime/zero/eg/either.runtime
@@ -1,1 +1,1 @@
-0.3
+0.2
diff --git a/bench/runtime/zero/eg/factorial.runtime b/bench/runtime/zero/eg/factorial.runtime
--- a/bench/runtime/zero/eg/factorial.runtime
+++ b/bench/runtime/zero/eg/factorial.runtime
@@ -1,1 +1,1 @@
-2.4
+2.2
diff --git a/bench/runtime/zero/eg/fib01.runtime b/bench/runtime/zero/eg/fib01.runtime
--- a/bench/runtime/zero/eg/fib01.runtime
+++ b/bench/runtime/zero/eg/fib01.runtime
@@ -1,1 +1,1 @@
-2.8
+1.4
diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime
--- a/bench/runtime/zero/eg/fibonacci.runtime
+++ b/bench/runtime/zero/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-5.4
+5.9
diff --git a/bench/runtime/zero/eg/higher.runtime b/bench/runtime/zero/eg/higher.runtime
--- a/bench/runtime/zero/eg/higher.runtime
+++ b/bench/runtime/zero/eg/higher.runtime
@@ -1,1 +1,1 @@
-1.2
+1.1
diff --git a/bench/runtime/zero/eg/id.runtime b/bench/runtime/zero/eg/id.runtime
--- a/bench/runtime/zero/eg/id.runtime
+++ b/bench/runtime/zero/eg/id.runtime
@@ -1,1 +1,1 @@
-0.0
+0.1
diff --git a/bench/runtime/zero/eg/ints.runtime b/bench/runtime/zero/eg/ints.runtime
--- a/bench/runtime/zero/eg/ints.runtime
+++ b/bench/runtime/zero/eg/ints.runtime
@@ -1,1 +1,1 @@
-1.0
+0.9
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
--- a/bench/runtime/zero/eg/list.runtime
+++ b/bench/runtime/zero/eg/list.runtime
@@ -1,1 +1,1 @@
-3.8
+1.0
diff --git a/bench/runtime/zero/eg/maybe.runtime b/bench/runtime/zero/eg/maybe.runtime
--- a/bench/runtime/zero/eg/maybe.runtime
+++ b/bench/runtime/zero/eg/maybe.runtime
@@ -1,1 +1,1 @@
-0.6
+0.5
diff --git a/bench/runtime/zero/eg/oddeven.runtime b/bench/runtime/zero/eg/oddeven.runtime
--- a/bench/runtime/zero/eg/oddeven.runtime
+++ b/bench/runtime/zero/eg/oddeven.runtime
@@ -1,1 +1,1 @@
-3.0
+2.7
diff --git a/bench/runtime/zero/eg/pow.runtime b/bench/runtime/zero/eg/pow.runtime
--- a/bench/runtime/zero/eg/pow.runtime
+++ b/bench/runtime/zero/eg/pow.runtime
@@ -1,1 +1,1 @@
-6.8
+7.3
diff --git a/bench/runtime/zero/eg/replicate.runtime b/bench/runtime/zero/eg/replicate.runtime
--- a/bench/runtime/zero/eg/replicate.runtime
+++ b/bench/runtime/zero/eg/replicate.runtime
@@ -1,1 +1,1 @@
-0.6
+0.3
diff --git a/bench/runtime/zero/eg/setelem.runtime b/bench/runtime/zero/eg/setelem.runtime
--- a/bench/runtime/zero/eg/setelem.runtime
+++ b/bench/runtime/zero/eg/setelem.runtime
@@ -1,1 +1,1 @@
-2.1
+1.4
diff --git a/bench/runtime/zero/eg/take-drop.runtime b/bench/runtime/zero/eg/take-drop.runtime
--- a/bench/runtime/zero/eg/take-drop.runtime
+++ b/bench/runtime/zero/eg/take-drop.runtime
@@ -1,1 +1,1 @@
-0.6
+0.5
diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime
--- a/bench/runtime/zero/eg/tree.runtime
+++ b/bench/runtime/zero/eg/tree.runtime
@@ -1,1 +1,1 @@
-2.6
+2.5
diff --git a/bench/runtime/zero/eg/tri.runtime b/bench/runtime/zero/eg/tri.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/tri.runtime
@@ -0,0 +1,1 @@
+0.4
diff --git a/bench/strategies.txt b/bench/strategies.txt
--- a/bench/strategies.txt
+++ b/bench/strategies.txt
@@ -67,9 +67,9 @@
 -- looking through 12 candidates of size 3
 -- looking through 24 candidates of size 4
 -- looking through 37 candidates of size 5
--- looking through 70 candidates of size 6
+-- looking through 72 candidates of size 6
 -- looking through 196 candidates of size 7
--- tested 163 candidates
+-- tested 165 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -82,9 +82,9 @@
 -- looking through 12 candidates of size 3
 -- looking through 24 candidates of size 4
 -- looking through 47 candidates of size 5
--- looking through 70 candidates of size 6
+-- looking through 82 candidates of size 6
 -- looking through 342 candidates of size 7
--- tested 272 candidates
+-- tested 284 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -97,9 +97,9 @@
 -- looking through 21 candidates of size 3
 -- looking through 42 candidates of size 4
 -- looking through 302 candidates of size 5
--- looking through 600 candidates of size 6
+-- looking through 602 candidates of size 6
 -- looking through 6115 candidates of size 7
--- tested 999 candidates
+-- tested 1001 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -127,9 +127,9 @@
 -- looking through 21 candidates of size 3
 -- looking through 42 candidates of size 4
 -- looking through 330 candidates of size 5
--- looking through 600 candidates of size 6
+-- looking through 630 candidates of size 6
 -- looking through 7215 candidates of size 7
--- tested 1915 candidates
+-- tested 1945 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
diff --git a/bench/unique.hs b/bench/unique.hs
--- a/bench/unique.hs
+++ b/bench/unique.hs
@@ -46,7 +46,7 @@
   css            =  take n
                  $  discardT isRedundantByIntroduction -- additional pruning rule
                  $  css'
-  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  (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
diff --git a/bench/weird.hs b/bench/weird.hs
--- a/bench/weird.hs
+++ b/bench/weird.hs
@@ -24,7 +24,7 @@
   conjure "^^^" (^^^) primitives
   conjureWith args{usePatterns = False} "^^^" (^^^) primitives
 
-  -- This example is quite degenerate,
+  -- This example is quite the degenerate case,
   -- it takes a while to conjure even with just 2 primitives.
   -- I am leaving it commented-out for now...
   -- conjure "thirty" thirty [pr (0::Int), prim "+" ((+) :: Int -> Int -> Int)]
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,18 @@
 ============================
 
 
+v0.6.2 (February 2025)
+----------------------
+
+* don't require 0 as a base case by default
+  (defalt to `requireZero=False`)
+* add switch to limit the size of constant sub-expressions
+  (`Args.maxConstantSize`)
+* add switch to enable showing of allowed patterns
+  (`Args.showPatterns`)
+* update examples
+
+
 v0.6.0 (February 2025)
 ----------------------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -3,7 +3,7 @@
 -- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.6.0
+version:             0.6.2
 synopsis:            synthesize Haskell functions out of partial definitions
 description:
   Conjure is a tool that synthesizes Haskell functions out of partial definitions.
@@ -68,7 +68,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.6.0
+  tag:             v0.6.2
 
 library
   exposed-modules: Conjure
diff --git a/eg/bits.hs b/eg/bits.hs
new file mode 100644
--- /dev/null
+++ b/eg/bits.hs
@@ -0,0 +1,40 @@
+-- bits.hs: functions over bits
+--
+-- Copyright (C) 2025 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
+import Conjure
+
+-- binary digit sum
+-- binaryDigitSum
+bitsum :: Int -> Int
+bitsum 0  =  0  --   0
+bitsum 1  =  1  --   1
+bitsum 2  =  1  --  10
+bitsum 3  =  2  --  11
+bitsum 4  =  1  -- 100
+bitsum 5  =  2  -- 101
+bitsum 6  =  2  -- 110
+bitsum 7  =  3  -- 111
+
+main :: IO ()
+main  =  do
+  conjure "bitsum" bitsum
+    [ pr (0 :: Int)
+    , pr (1 :: Int)
+    , prim "halve" ((`div` 2) :: Int -> Int)
+    , prim "parity" ((`mod` 2) :: Int -> Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    ]
+  -- bitsum 0  =  0
+  -- bitsum n  =  parity n + bitsum (halve n)
+
+  conjure "bitsum" bitsum
+    [ pr (0 :: Int)
+    , pr (1 :: Int)
+    , pr (2 :: Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "`div`" (div :: Int -> Int -> Int)
+    , prim "`mod`" (mod :: Int -> Int -> Int)
+    ]
+  -- bitsum 0  =  0
+  -- bitsum n  =  n `mod` 2 + bitsum (n `div` 2)
diff --git a/eg/bits.txt b/eg/bits.txt
new file mode 100644
--- /dev/null
+++ b/eg/bits.txt
@@ -0,0 +1,30 @@
+bitsum :: Int -> Int
+-- testing 8 combinations of argument values
+-- pruning with 21/25 rules
+-- looking through 3 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 5 candidates of size 3
+-- looking through 10 candidates of size 4
+-- looking through 26 candidates of size 5
+-- looking through 68 candidates of size 6
+-- looking through 182 candidates of size 7
+-- tested 145 candidates
+bitsum 0  =  0
+bitsum x  =  bitsum (halve x) + parity x
+
+bitsum :: Int -> Int
+-- testing 8 combinations of argument values
+-- pruning with 27/32 rules
+-- looking through 4 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 17 candidates of size 3
+-- looking through 16 candidates of size 4
+-- looking through 246 candidates of size 5
+-- looking through 239 candidates of size 6
+-- looking through 4504 candidates of size 7
+-- looking through 4542 candidates of size 8
+-- looking through 89215 candidates of size 9
+-- tested 10191 candidates
+bitsum 0  =  0
+bitsum x  =  bitsum (x `div` 2) + x `mod` 2
+
diff --git a/eg/count.hs b/eg/count.hs
--- a/eg/count.hs
+++ b/eg/count.hs
@@ -1,19 +1,13 @@
 -- count.hs: elem and set functions
 import Conjure
 
+-- an idiomatic count without using filter
 count :: Eq a => a -> [a] -> Int
 count x  =  c
   where
   c []  =  0
   c (y:ys)  =  (if x == y then 1 else 0) + c ys
 
--- this is the expected function
-countIf :: A -> [A] -> Int
-countIf x xs  =  if null xs                                                 -- 3
-                 then 0                                                     -- 4
-                 else (if x == head xs then 1 else 0) + countIf x (tail xs) -- 16
-                 --    5  6 7   8   9      10     11 12   13   14   15  16
-
 count' :: A -> [A] -> Int
 count' 0 [0]  =  1
 count' 0 [1]  =  0
@@ -39,6 +33,8 @@
     , prim "==" ((==) :: A -> A -> Bool)
     ]
 
+  -- count x []  =  0
+  -- count x (y:xs)  =  count x xs + (if x == y then 1 else 0)
   conjure "count" count'
     [ pr (0 :: Int)
     , pr (1 :: Int)
diff --git a/eg/fib01.hs b/eg/fib01.hs
--- a/eg/fib01.hs
+++ b/eg/fib01.hs
@@ -23,27 +23,29 @@
 
 main :: IO ()
 main  =  do
-  conjureWithMaxSize 5 "fib01" fib01
+  -- These two examples show that currently
+  -- functions with "many" argument (>=3)
+  -- are particularly hard for conjure to synthesize.
+  -- I've added an item in TODO.md to address this in 2025-02.
+
+  -- It takes about 33 seconds to run with maxSize=8
+  -- running with maxSize = 5 for faster runtime
+  conjureWith args{maxSize=5, maxConstantSize=1} "fib01" fib01
     [ pr (0::Int)
     , prim "dec" (subtract 1 :: Int -> Int)
     , prim "+" ((+) :: Int -> Int -> Int)
     ]
 
-  -- takes about 22 seconds to run with maxSize=12
-  conjureWith args{usePatterns = False, maxSize = 10} "fib01" fib01
+  -- It takes about 27 seconds to run with maxSize=12
+  -- running with maxSize = 9 for faster runtime
+  conjureWith args{usePatterns = False, maxSize = 1, maxConstantSize=1} "fib01" fib01
     [ pr (0::Int)
     , prim "+" ((+) :: Int -> Int -> Int)
     , prim "dec" (subtract 1 :: Int -> Int)
     , prim "<=" ((<=) :: Int -> Int -> Bool)
+    , prif (undefined :: Int)
     ]
--- expected function:
--- fib01 x y z  =  if z <= 0 then y else fib01 y (x + y) (dec z)
---                 1  2 3  4      5      6     7  8 9 10  11 12
-
-  -- out of reach as well:
-  -- conjure "fib01" fib01
-  --   [ pr (0::Int)
-  --   , pr (1::Int)
-  --   , prim "+" ((+) :: Int -> Int -> Int)
-  --   , prim "-" ((-) :: Int -> Int -> Int)
-  --   ]
+  -- expected function:
+  -- fib01 x y z  =  if z <= 0                     -- 4
+  --                 then y                        -- 5
+  --                 else fib01 y (x + y) (dec z)  -- 12
diff --git a/eg/fib01.txt b/eg/fib01.txt
--- a/eg/fib01.txt
+++ b/eg/fib01.txt
@@ -11,17 +11,8 @@
 
 fib01 :: Int -> Int -> Int -> Int
 -- testing 8 combinations of argument values
--- pruning with 18/38 rules
+-- pruning with 21/41 rules
 -- looking through 4 candidates of size 1
--- looking through 4 candidates of size 2
--- looking through 10 candidates of size 3
--- looking through 16 candidates of size 4
--- looking through 44 candidates of size 5
--- looking through 92 candidates of size 6
--- 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
+-- tested 4 candidates
 cannot conjure
 
diff --git a/eg/fibonacci.txt b/eg/fibonacci.txt
--- a/eg/fibonacci.txt
+++ b/eg/fibonacci.txt
@@ -8,12 +8,12 @@
 -- looking through 26 candidates of size 5
 -- looking through 27 candidates of size 6
 -- looking through 116 candidates of size 7
--- looking through 102 candidates of size 8
--- looking through 532 candidates of size 9
--- looking through 474 candidates of size 10
--- looking through 2571 candidates of size 11
--- looking through 2287 candidates of size 12
--- tested 3951 candidates
+-- 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)
diff --git a/eg/pow.txt b/eg/pow.txt
--- a/eg/pow.txt
+++ b/eg/pow.txt
@@ -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 4118 candidates of size 7
+-- looking through 4136 candidates of size 7
 -- looking through 13292 candidates of size 8
--- tested 6365 candidates
+-- tested 6383 candidates
 pow x 0  =  1
 pow x y  =  x * pow x (y - 1)
 
@@ -21,7 +21,7 @@
 -- looking through 58 candidates of size 3
 -- looking through 174 candidates of size 4
 -- looking through 485 candidates of size 5
--- looking through 1369 candidates of size 6
--- tested 2108 candidates
+-- looking through 1387 candidates of size 6
+-- tested 2126 candidates
 cannot conjure
 
diff --git a/eg/take-drop.txt b/eg/take-drop.txt
--- a/eg/take-drop.txt
+++ b/eg/take-drop.txt
@@ -7,7 +7,7 @@
 -- looking through 6 candidates of size 4
 -- looking through 8 candidates of size 5
 -- looking through 13 candidates of size 6
--- looking through 22 candidates of size 7
+-- looking through 24 candidates of size 7
 -- tested 39 candidates
 drop 0 xs  =  xs
 drop x []  =  []
@@ -22,10 +22,10 @@
 -- looking through 6 candidates of size 4
 -- looking through 8 candidates of size 5
 -- looking through 13 candidates of size 6
--- looking through 22 candidates of size 7
--- looking through 26 candidates of size 8
--- looking through 58 candidates of size 9
--- tested 104 candidates
+-- looking through 24 candidates of size 7
+-- looking through 31 candidates of size 8
+-- looking through 59 candidates of size 9
+-- tested 111 candidates
 take 0 xs  =  []
 take x []  =  []
 take x (y:xs)  =  y:take (x - 1) xs
diff --git a/eg/tri.hs b/eg/tri.hs
new file mode 100644
--- /dev/null
+++ b/eg/tri.hs
@@ -0,0 +1,18 @@
+-- tri.hs: conjuring a tri function
+--
+-- 2025 Colin Runciman and Rudy Matela
+import Conjure
+
+tri :: Int -> Int
+tri 1  =  1
+tri 2  =  3
+tri 3  =  6
+tri 5  =  15
+
+main :: IO ()
+main  =  do
+  conjure "tri" tri
+    [ pr (1::Int)
+    , prim "+" ((+) :: Int -> Int -> Int)
+    , prim "-" ((-) :: Int -> Int -> Int)
+    ]
diff --git a/eg/tri.txt b/eg/tri.txt
new file mode 100644
--- /dev/null
+++ b/eg/tri.txt
@@ -0,0 +1,14 @@
+tri :: Int -> Int
+-- testing 4 combinations of argument values
+-- pruning with 11/33 rules
+-- looking through 2 candidates of size 1
+-- looking through 0 candidates of size 2
+-- looking through 5 candidates of size 3
+-- looking through 5 candidates of size 4
+-- looking through 10 candidates of size 5
+-- looking through 8 candidates of size 6
+-- looking through 41 candidates of size 7
+-- tested 31 candidates
+tri 1  =  1
+tri x  =  x + tri (x - 1)
+
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -292,6 +292,23 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   eg/arith.hs
+eg/bits: \
+  eg/bits.hs \
+  mk/toplibs
+eg/bits.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 \
+  eg/bits.hs
 eg/bools: \
   eg/bools.hs \
   mk/toplibs
@@ -734,6 +751,23 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   eg/tree.hs
+eg/tri: \
+  eg/tri.hs \
+  mk/toplibs
+eg/tri.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 \
+  eg/tri.hs
 mk/All.o: \
   src/Conjure/Utils.hs \
   src/Conjure/Red.hs \
diff --git a/src/Conjure/Defn.hs b/src/Conjure/Defn.hs
--- a/src/Conjure/Defn.hs
+++ b/src/Conjure/Defn.hs
@@ -169,8 +169,10 @@
   -- ef' :$ exprExpr ex :$ exprExpr ey :$ ...
   red :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
   red n m e  |  size e > n  =  err "argument-size limit reached"
-  -- prevent recursion into negatives:
-  -- red n m e  |  any isNegative (unfoldApp e)  =  err "recursion into negatives"
+  -- prevent recursion into negatives, we fail earlier in these cases
+  -- we match a non-empty memo table to know that we already have a call stack
+  -- red n (_:_) e | any isNegative (unfoldApp e)  =  err "recursion into negatives"
+  -- the above is not correct, we need to detect which arguments are descending somehow...
   red n m e  =  case lookup e m of
     Just Nothing -> err $ "loop detected " ++ show e
     Just (Just d) -> Just (n,m,d)
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -191,6 +191,7 @@
   , 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@)
+  , maxConstantSize       :: Int  -- ^ maximum size of constants (0 for no limit)
 
   -- advanced & debug options --
   , carryOn               :: Bool -- ^ whether to carry on after finding a suitable candidate
@@ -198,7 +199,8 @@
   , usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates
   , showCandidates        :: Bool -- ^ (debug) show candidates -- warning: wall of text
   , showTests             :: Bool -- ^ (debug) show tests
-  , showDeconstructions   :: Bool -- ^ (debug) show conjecture-and-allowed deconstructions
+  , showPatterns          :: Bool -- ^ (debug) show possible LHS patterns
+  , showDeconstructions   :: Bool -- ^ (debug) show conjectured-and-allowed deconstructions
 
   -- pruning options --
   , rewriting             :: Bool -- ^ unique-modulo-rewriting candidates
@@ -231,6 +233,7 @@
   , maxEquationSize        =   5
   , maxSearchTests         =  100000
   , maxDeconstructionSize  =   4
+  , maxConstantSize        =   0 -- unlimited
 
   -- advanced & debug options --
   , carryOn                =  False
@@ -239,6 +242,7 @@
   , showCandidates         =  False
   , showTests              =  False
   , showDeconstructions    =  False
+  , showPatterns           =  False
 
   -- pruning options --
   , rewriting              =  True
@@ -246,11 +250,13 @@
   , adHocRedundancy        =  True
   , copyBindings           =  True
   , atomicNumbers          =  True
-  , requireZero            =  True
+  , requireZero            =  False
   , uniqueCandidates       =  False
   }
 
+-- TODO: remove the requireZero option from args?
 
+
 -- | Like 'conjure' but allows setting options through 'Args'/'args'.
 --
 -- > conjureWith args{maxSize = 18} "function" function [...]
@@ -287,6 +293,8 @@
       putStrLn $ "invalid:"
       putStr   $ unlines $ map showEq $ invalid thy
       putStrLn $ "-}"
+  when (showPatterns args) $ do
+    putStr   $ unlines $ zipWith (\i -> (("-- allowed patterns of size " ++ show i ++ "\n{-\n") ++) . (++ "-}") . unlines) [1..] $ mapT showDefn $ patternss results
   when (showDeconstructions args) $ do
     putStrLn $ "{- List of allowed deconstructions:"
     putStr   $ unlines $ map show $ deconstructions results
@@ -331,6 +339,7 @@
   , candidatess :: [[Defn]]      -- ^ tiers of candidates
   , bindings :: [Expr]           -- ^ test bindings used to verify candidates
   , theory :: Thy                -- ^ the underlying theory
+  , patternss :: [[Defn]]        -- ^ tiers of allowed patterns
   , deconstructions :: [Expr]    -- ^ the list of allowed deconstructions
   }
 
@@ -370,6 +379,7 @@
   , candidatess  =  candidatesT
   , bindings  =  tests
   , theory  =  thy
+  , patternss  =  patternss
   , deconstructions  =  deconstructions
   }
   where
@@ -380,7 +390,7 @@
                  && errorToFalse (p (cevl maxEvalRecursions fx))
   candidatesT  =  (if uniqueCandidates then nubCandidates args nm f else id)
                $  take maxSize candidatesTT
-  (candidatesTT, thy, deconstructions)  =  candidateDefns args nm f es
+  (candidatesTT, thy, patternss, deconstructions)  =  candidateDefns args nm f es
   ffxx   =  conjureApplication nm f
   vffxx  =  conjureVarApplication nm f
 
@@ -420,7 +430,7 @@
 -- 1. tiers of candidate definitions
 -- 2. an equational theory
 -- 3. a list of allowed deconstructions
-candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])
+candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [[Defn]], [Expr])
 candidateDefns args  =  candidateDefns' args
   where
   candidateDefns'  =  if usePatterns args
@@ -430,17 +440,22 @@
 
 -- | Return apparently unique candidate definitions
 --   where there is a single body.
-candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])
-candidateDefns1 args nm f ps  =  first3 (mapT toDefn) $ candidateExprs args nm f ps
+candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [[Defn]], [Expr])
+candidateDefns1 args nm f ps  =  first4 (mapT toDefn) $ candidateExprs args nm f ps
   where
   efxs  =  conjureVarApplication nm f
   toDefn e  =  [(efxs, e)]
-  first3 f (x,y,z)  =  (f x, y, z)
+  first4 f (x,y,z,w)  =  (f x, y, z, w)
 
 
 -- | Return apparently unique candidate bodies.
-candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy, [Expr])
-candidateExprs Args{..} nm f ps  =  (as \/ concatMapT (`enumerateFillings` recs) ts, thy, deconstructions)
+candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy, [[Defn]], [Expr])
+candidateExprs Args{..} nm f ps  =
+  ( as \/ concatMapT (`enumerateFillings` recs) ts
+  , thy
+  , [[ [(efxs, eh)] ]]
+  , deconstructions
+  )
   where
   es  =  map fst ps
   ts | typ efxs == boolTy  =  foldAppProducts andE [cs, rs]
@@ -488,8 +503,13 @@
 
 -- | Return apparently unique candidate definitions
 --   using pattern matching.
-candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])
-candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundant $ concatMapT fillingsFor fss,thy,deconstructions)
+candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [[Defn]], [Expr])
+candidateDefnsC Args{..} nm f ps  =
+  ( discardT hasRedundant $ concatMapT fillingsFor fss
+  , thy
+  , mapT (map (,eh)) pats
+  , deconstructions
+  )
   where
   pats  =  conjurePats es nm f
   fss  =  concatMapT ps2fss pats
@@ -506,9 +526,12 @@
   appsWith eh vs  =  enumerateAppsFor eh k $ vs ++ es
     where
     k | atomicNumbers && isNumeric eh  =  \e -> keepNumeric e && keep e
+      | maxConstantSize > 0            =  \e -> keepConstant e && keep e
       | otherwise                      =  keep
     -- discards non-atomic numeric ground expressions such as 1 + 1
     keepNumeric e  =  isFun e || isConst e || not (isGround e)
+    -- discards big non-atomic ground expressions such as 1 + 1 or reverse [1,2]
+    keepConstant e  =  isFun e || isConst e || not (isGround e) || size e <= maxConstantSize
 
   isRedundant | adHocRedundancy  =  \e -> isRedundantDefn e || isRedundantModuloRewriting (normalize thy) e
               | otherwise        =  const False
@@ -530,7 +553,7 @@
     p2eess pat | copyBindings && isGroundPat f pat  =  [[(pat, toValPat f pat)]]
     p2eess pat  =  mapT (pat,)
                 .  appsWith pat
-                .  tail
+                .  drop 1 -- this excludes the function name itself
                 $  vars pat ++ [eh | any (uncurry should) (zip aess aes)]
       where
       -- computes whether we should include a recurse for this given argument