consider & uni: partly revert to v0.4.16 behaviour

In consider we only use the normalization if it reduces the number of variables, otherwise the equivalencesBetween are from the standard term. (Part reversal: sometimes till _will_ use the normalization) In criticalPairs / overlaps, we use the regular syntactic unification and not syntactic unification modulo commutativity. (Full reversal)
rudymatela · Feb 13, 2024 · 0d9664c · 0d9664c
1 parent 8857f5f
commit 0d9664c
Show file tree

Hide file tree

Showing 36 changed files with 37 additions and 36 deletions.
diff --git a/bench/list-t.txt b/bench/list-t.txt
@@ -22,6 +22,7 @@ tail (x:xs) == xs
 equations:
 head (xs ++ (x:zs)) == head (xs ++ (x:ys))
 head (xs ++ [x]) == head (xs ++ (x:ys))
+head (xs ++ (x:tail [])) == head (xs ++ (x:ys))
 
         head (x:xs) == x
 head (xs ++ (x:ys)) == head (xs ++ (x:zs))

diff --git a/bench/runtime/zero/bench/addition.runtime b/bench/runtime/zero/bench/addition.runtime
@@ -0,0 +1 @@
+0.45
diff --git a/bench/runtime/zero/bench/arith-c.runtime b/bench/runtime/zero/bench/arith-c.runtime
@@ -1 +1 @@
-0.75
+0.60
diff --git a/bench/runtime/zero/bench/arith-t.runtime b/bench/runtime/zero/bench/arith-t.runtime
@@ -1 +1 @@
-11.26
+10.02
diff --git a/bench/runtime/zero/bench/arithficial.runtime b/bench/runtime/zero/bench/arithficial.runtime
@@ -1 +1 @@
-0.44
+0.60
diff --git a/bench/runtime/zero/bench/bool-c.runtime b/bench/runtime/zero/bench/bool-c.runtime
@@ -1 +1 @@
-2.14
+1.81
diff --git a/bench/runtime/zero/bench/list-c.runtime b/bench/runtime/zero/bench/list-c.runtime
@@ -1 +1 @@
-1.59
+1.60
diff --git a/bench/runtime/zero/bench/list-t.runtime b/bench/runtime/zero/bench/list-t.runtime
@@ -1 +1 @@
-0.43
+0.48
diff --git a/bench/runtime/zero/bench/lowtests.runtime b/bench/runtime/zero/bench/lowtests.runtime
@@ -1 +1 @@
-0.48
+0.46
diff --git a/bench/runtime/zero/bench/minus-c.runtime b/bench/runtime/zero/bench/minus-c.runtime
@@ -1 +1 @@
-0.90
+0.91
diff --git a/bench/runtime/zero/bench/stats.runtime b/bench/runtime/zero/bench/stats.runtime
@@ -1 +1 @@
-0.28
+0.30
diff --git a/bench/runtime/zero/bench/trilean.runtime b/bench/runtime/zero/bench/trilean.runtime
@@ -1 +1 @@
-0.04
+0.05
diff --git a/bench/runtime/zero/eg/arith-negate-abs.runtime b/bench/runtime/zero/eg/arith-negate-abs.runtime
@@ -1 +1 @@
-1.78
+1.58
diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime
@@ -1 +1 @@
-0.28
+0.26
diff --git a/bench/runtime/zero/eg/binarytree.runtime b/bench/runtime/zero/eg/binarytree.runtime
@@ -1 +1 @@
-1.90
+1.89
diff --git a/bench/runtime/zero/eg/binarytree0.runtime b/bench/runtime/zero/eg/binarytree0.runtime
@@ -1 +1 @@
-0.53
+0.60
diff --git a/bench/runtime/zero/eg/bool.runtime b/bench/runtime/zero/eg/bool.runtime
@@ -1 +1 @@
-2.49
+2.42
diff --git a/bench/runtime/zero/eg/digraphs.runtime b/bench/runtime/zero/eg/digraphs.runtime
@@ -1 +1 @@
-1.54
+1.49
diff --git a/bench/runtime/zero/eg/fun.runtime b/bench/runtime/zero/eg/fun.runtime
@@ -1 +1 @@
-1.07
+1.08
diff --git a/bench/runtime/zero/eg/insertsort.runtime b/bench/runtime/zero/eg/insertsort.runtime
@@ -1 +1 @@
-7.74
+7.38
diff --git a/bench/runtime/zero/eg/length.runtime b/bench/runtime/zero/eg/length.runtime
@@ -1 +1 @@
-0.25
+0.24
diff --git a/bench/runtime/zero/eg/minus.runtime b/bench/runtime/zero/eg/minus.runtime
@@ -1 +1 @@
-0.52
+0.65
diff --git a/bench/runtime/zero/eg/monad.runtime b/bench/runtime/zero/eg/monad.runtime
@@ -1 +1 @@
-0.59
+0.61
diff --git a/bench/runtime/zero/eg/oddeven.runtime b/bench/runtime/zero/eg/oddeven.runtime
@@ -1 +1 @@
-6.87
+6.85
diff --git a/bench/runtime/zero/eg/plus-abs.runtime b/bench/runtime/zero/eg/plus-abs.runtime
@@ -1 +1 @@
-3.77
+3.50
diff --git a/bench/runtime/zero/eg/ratio.runtime b/bench/runtime/zero/eg/ratio.runtime
@@ -1 +1 @@
-8.34
+7.64
diff --git a/bench/runtime/zero/eg/sets.runtime b/bench/runtime/zero/eg/sets.runtime
@@ -1 +1 @@
-7.94
+7.34
diff --git a/bench/runtime/zero/eg/speculate-reason.runtime b/bench/runtime/zero/eg/speculate-reason.runtime
@@ -1 +1 @@
-2.98
+2.95
diff --git a/bench/runtime/zero/eg/string.runtime b/bench/runtime/zero/eg/string.runtime
@@ -1 +1 @@
-0.92
+0.87
diff --git a/bench/runtime/zero/eg/tauts.runtime b/bench/runtime/zero/eg/tauts.runtime
@@ -1 +1 @@
-4.12
+4.13
diff --git a/bench/runtime/zero/eg/tuples.runtime b/bench/runtime/zero/eg/tuples.runtime
@@ -1 +1 @@
-1.28
+1.27
diff --git a/bench/runtime/zero/eg/zip.runtime b/bench/runtime/zero/eg/zip.runtime
@@ -1 +1 @@
-2.38
+2.41
diff --git a/eg/insertsort.txt b/eg/insertsort.txt
@@ -30,7 +30,7 @@ sort :: [Int] -> [Int]
     ([] == insert x xs) == False
         (xs == sort xs) == ordered xs
        elem x (sort xs) == elem x xs
-             (xs == []) == ([] == sort xs)
+        (sort xs == []) == (xs == [])
    all (x ==) (sort xs) == all (x ==) xs
     all (x <) (sort xs) == all (x <) xs
           all (x <=) xs == ordered (x:sort xs)

diff --git a/eg/insertsort0.txt b/eg/insertsort0.txt
@@ -22,7 +22,7 @@ False :: Bool
 
    (xs == insert x xs) == False
    ([] == insert x xs) == False
-            (xs == []) == ([] == sort xs)
+       (sort xs == []) == (xs == [])
                sort [] == []
         sort (sort xs) == sort xs
            insert x [] == [x]

diff --git a/src/Test/Speculate/Engine.hs b/src/Test/Speculate/Engine.hs
@@ -180,8 +180,8 @@ consider (===) sz s (thy,sss)
   where
   ns = rehole $ normalizeE thy (fastMostGeneralVariation s)
   -- between s and ns, choose the one with less holes to call equivalencesBetween
-  ms | length (holes s) < length (holes ns) = s
-     | otherwise = ns
+  ms | length (holes s) <= length (holes ns) = s
+     | otherwise = ns -- favour ns only if it reduces the number of variables
   e1 -===- e2  =  normalize thy e1 == normalize thy e2 || e1 === e2
   ss = uptoT sz sss
   sssWs = sss \/ wcons0 sz s

diff --git a/src/Test/Speculate/Reason.hs b/src/Test/Speculate/Reason.hs
@@ -239,12 +239,11 @@ criticalPairs thy@Thy{rules = rs}  =
   overlaps :: Expr -> Expr -> [Expr]
   overlaps e1 e2 = nubSortBy compareQuickly
                  . map (canonicalize . (e2' //-))
-                 $ (e1' `unifn`) `mapMaybe` nonVarSubexprs e2'
+                 $ (e1' `unification`) `mapMaybe` nonVarSubexprs e2'
     where
     nonVarSubexprs = discard isVar . nubSubexprs
     e1' = renameVarsBy (++ "1") e1
     e2' = renameVarsBy (++ "2") e2
-    unifn = unificationC (commutativeOperators thy)
 
 equivalent :: Thy -> Expr -> Expr -> Bool
 equivalent thy e1 e2 = e1' == e2'