simplify pruning of commutative operators

Before we had:

	isRootNormalC thy (ef :$ ex :$ ey)
	  | ex <= ey  =  True
	  | not (isCommutative thy ef)  =  True
	  | isRootNormal thy (ef :$ ey :$ ex)  =  False

We were only pruning non-ordered commutative expressions
when the ordered version was root-normal.

I thought we could not prune something like the following expression:

	(x - 1) * (x + x)

as its reversal is not normal:

	(x + x) * (x - 1)
	rewrites to
	x * ((x - 1) + (x + 1))
	by
	(x + x) * y  =  x * (y + y)

So then we would have to stick with (x - 1) * (x + x) in the enumeration.
However, x * ((x - 1) + (x + 1)) is equivalent to it
and is bound to appear in the enumeration of expressions of size 9!

So we can definitely prune it,
with the side effect of delaying
some candidates to appear with a bigger size.
This aleady happens anyway, so no harm done.

I now have simply:

	isRootNormalC thy (ef :$ ex :$ ey) | isCommutative thy ef  =  ex <= ey

This can probably be extended to permutative laws in the future.

Runtime has decreased overall as expected:

* fibonacci:  -30%
* carry-on:   -13%
* arith:      -10%
* factorial    -7%
* gps(2):      -7%

Good thing Colin brought this to notice!

bench/candidates.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 @@ foo x  =  0 - x
 
 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 @@ ton True  =  False
 
 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

bench/carry-on.txt

@@ -7,41 +7,41 @@ factorial :: Int -> Int
 -- 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)
 
--- looking through 217 candidates of size 8
--- tested 266 candidates
+-- looking through 203 candidates of size 8
+-- tested 254 candidates
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- looking through 1196 candidates of size 9
--- tested 573 candidates
+-- looking through 1048 candidates of size 9
+-- tested 547 candidates
 factorial 0  =  0
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- tested 581 candidates
+-- tested 555 candidates
 factorial 0  =  1
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- looking through 1475 candidates of size 10
--- looking through 8678 candidates of size 11
--- tested 3586 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 3766 candidates
+-- tested 3396 candidates
 factorial 0  =  1
 factorial x  =  x - x * (1 - factorial (x - 1))
 
--- tested 3906 candidates
+-- tested 3519 candidates
 factorial 0  =  1
 factorial x  =  (0 - x) * (0 - factorial (x - 1))
 
--- tested 11829 candidates
+-- tested 10004 candidates
 cannot conjure
 

bench/erroneous.txt

@@ -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)

bench/gps.txt

@@ -151,8 +151,8 @@ wallisNext :: Ratio Integer -> Ratio Integer
 -- 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 @@ gps13 :: [Ratio Integer] -> Ratio Integer
 -- 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 @@ odd :: Int -> Bool
 -- 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 @@ gps14 :: [Int] -> Int
 -- 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 @@ gps17 :: Int -> Int
 -- 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 @@ gps24 :: [Char] -> Char
 -- 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]

bench/gps2.txt

@@ -155,11 +155,11 @@ gps10 :: [Int] -> Int
 -- 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)
 

bench/runtime/lapmatrud/bench/candidates.runtime

@@ -1 +1 @@
-10.0
+9.1

bench/runtime/lapmatrud/bench/carry-on.runtime

@@ -1 +1 @@
-2.9
+2.5

bench/runtime/lapmatrud/bench/erroneous.runtime

@@ -1 +1 @@
-2.9
+2.7

bench/runtime/lapmatrud/bench/gps.runtime

@@ -1 +1 @@
-15.2
+14.1

bench/runtime/lapmatrud/bench/gps2.runtime

@@ -1 +1 @@
-13.1
+12.1

bench/runtime/lapmatrud/bench/p12.runtime

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

bench/runtime/lapmatrud/bench/redundants.runtime

@@ -1 +1 @@
-3.1
+2.9

bench/runtime/lapmatrud/bench/strategies.runtime

@@ -1 +1 @@
-4.8
+4.4

bench/runtime/lapmatrud/bench/terpret.runtime

@@ -1 +1 @@
-8.4
+7.9

bench/runtime/lapmatrud/bench/unique.runtime

@@ -1 +1 @@
-2.3
+2.2

bench/runtime/lapmatrud/bench/weird.runtime

@@ -1 +1 @@
-3.0
+2.7

bench/runtime/lapmatrud/eg/arith.runtime

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

bench/runtime/lapmatrud/eg/bools.runtime

@@ -1 +1 @@
-1.9
+1.8

bench/runtime/lapmatrud/eg/bst.runtime

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

bench/runtime/lapmatrud/eg/count.runtime

@@ -1 +1 @@
-0.4
+0.3

bench/runtime/lapmatrud/eg/dupos.runtime

@@ -1 +1 @@
-3.6
+3.5

bench/runtime/lapmatrud/eg/factorial.runtime

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

bench/runtime/lapmatrud/eg/fib01.runtime

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

bench/runtime/lapmatrud/eg/fibonacci.runtime

@@ -1 +1 @@
-4.8
+3.3

bench/runtime/lapmatrud/eg/higher.runtime

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

bench/runtime/lapmatrud/eg/ints.runtime

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

bench/runtime/lapmatrud/eg/list.runtime

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

bench/runtime/lapmatrud/eg/oddeven.runtime

@@ -1 +1 @@
-1.7
+1.5

bench/runtime/lapmatrud/eg/pow.runtime

@@ -1 +1 @@
-4.5
+4.1

bench/runtime/lapmatrud/eg/setelem.runtime

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

bench/runtime/lapmatrud/eg/tree.runtime

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

bench/strategies.txt

@@ -8,7 +8,7 @@ factorial :: Int -> Int
 -- looking through 8 candidates of size 4
 -- looking through 23 candidates of size 5
 -- looking through 30 candidates of size 6
--- looking through 84 candidates of size 7
+-- looking through 82 candidates of size 7
 -- tested 84 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
@@ -23,7 +23,7 @@ factorial :: Int -> Int
 -- 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)
@@ -53,7 +53,7 @@ factorial :: Int -> Int
 -- looking through 8 candidates of size 4
 -- looking through 28 candidates of size 5
 -- looking through 35 candidates of size 6
--- looking through 264 candidates of size 7
+-- looking through 252 candidates of size 7
 -- tested 148 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
@@ -68,7 +68,7 @@ factorial :: Int -> Int
 -- looking through 24 candidates of size 4
 -- looking through 37 candidates of size 5
 -- looking through 72 candidates of size 6
--- looking through 208 candidates of size 7
+-- looking through 196 candidates of size 7
 -- tested 165 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
@@ -83,7 +83,7 @@ factorial :: Int -> Int
 -- looking through 24 candidates of size 4
 -- looking through 47 candidates of size 5
 -- looking through 82 candidates of size 6
--- looking through 354 candidates of size 7
+-- looking through 342 candidates of size 7
 -- tested 284 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)

bench/terpret.txt

@@ -58,8 +58,8 @@ cshift :: (Bool,Bool,Bool) -> (Bool,Bool,Bool)
 -- 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)

bench/unique.txt

@@ -1,9 +1,9 @@
 Unique candidates for: foo :: Int -> Int
   pruning with 27/65 rules
-  [3,3,9,10,32,39,197] candidates
-  [3,3,9,10,27,34,97] unique candidates
-  183/293 unique candidates
-  110/293 redundant candidates
+  [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
@@ -458,14 +458,10 @@ foo x  =  1 - x * (x + x)
 
 foo x  =  1 - x * (x * x)
 
-foo x  =  (x - 1) * (x + x)
-
 foo x  =  (x - 1) * (x - 1)
 
 foo x  =  (x - 1) * (1 - x)
 
-foo x  =  (1 - x) * (x + x)
-
 foo x  =  x * x - (x + x)
 
 foo 1  =  0

bench/weird.txt

@@ -18,11 +18,11 @@ x ^^^ y  =  0
 -- 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

eg/bst.txt

@@ -12,7 +12,7 @@ mem :: Int -> Tree -> Bool
 -- 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)

eg/factorial.txt

@@ -7,7 +7,7 @@ factorial :: Int -> Int
 -- 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)