packages feed

speculate 0.4.18 → 0.4.20

raw patch · 76 files changed

+187/−74 lines, 76 files

Files

.gitignore view
@@ -82,6 +82,7 @@ eg/tauts eg/tuples eg/oddeven+bench/addition bench/expressions bench/representatives bench/representatives2
Makefile view
@@ -15,6 +15,9 @@   $(shell grep -q "Arch Linux" /etc/lsb-release && echo --optghc=-dynamic --optghc=-package=cmdargs --optghc=-package=regex-tdfa --optghc=-package=algebraic-graphs) MAXTESTS = 4000 MAXSIZE = -s4+# Sets the number of jobs to the the number of processors minus one.+NJOBS := $(shell grep ^processor /proc/cpuinfo | head -n -1 | wc -l | sed 's/^0$$/1/')+LONG := $(shell which long >/dev/null 2>/dev/null && echo long) TESTS = \   test/creason \   test/engine \@@ -47,6 +50,7 @@   eg/monad \   eg/tuples \   eg/speculate-reason \+  bench/addition \   bench/arithficial \   bench/lowtests \   bench/nord \@@ -108,6 +112,15 @@  test-via-stack: 	stack test speculate:test:engine --ghc-options="$(GHCFLAGS) -O0" --system-ghc --no-install-ghc --no-terminal++fastest:+	$(LONG) make test -j$(NJOBS)++fastestbench:+	$(LONG) make test -j$(NJOBS) && $(LONG) make bench++fastxtestbench:+	$(LONG) make txt -j$(NJOBS) && $(LONG) make test -j$(NJOBS) && $(LONG) make bench  legacy-test: 	make clean  &&  make -j8 GHC=ghc-8.2   &&  make quick-test -j8 GHC=ghc-8.2
+ bench/addition.hs view
@@ -0,0 +1,13 @@+import Test.Speculate++main :: IO ()+main = speculate args+  { maxSize = 7+  , showTheory = True+  , showSemiequations = False+  , showConditions = False+  , constants =+      [ showConstant (0::Int)+      , constant "+"  ((+) :: Int -> Int -> Int)+      ]+  }
+ bench/addition.txt view
@@ -0,0 +1,31 @@+max expr size  =    7+  |- on ineqs  =    6+  |- on conds  =    6+max  #-tests   =  500+max  #-vars    =    2  (for inequational and conditional laws)++_ :: Int+0 :: Int+(+) :: Int -> Int -> Int++rules:+x + 0 == x+0 + x == x+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+equations:+y + x == x + y+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)+y + (x + (x' + z)) == x + (y + (z + x'))+z + (x + (y + x')) == x + (y + (z + x'))+z + (y + (x + x')) == x + (y + (z + x'))+z + (x' + (x + y)) == x + (y + (z + x'))+x' + (y + (z + x)) == x + (y + (z + x'))+x' + (z + (y + x)) == x + (y + (z + x'))++      x + 0 == x+      x + y == y + x+(x + y) + z == x + (y + z)+
bench/list-t.txt view
@@ -22,6 +22,7 @@ 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))
+ bench/runtime/lapmatrud/bench/addition.runtime view
@@ -0,0 +1,1 @@+0.22
+ bench/runtime/lapmatrud/bench/arith-c.runtime view
@@ -0,0 +1,1 @@+0.35
+ bench/runtime/lapmatrud/bench/arith-t.runtime view
@@ -0,0 +1,1 @@+6.58
bench/runtime/lapmatrud/bench/arithficial.runtime view
@@ -1,1 +1,1 @@-0.37+0.24
+ bench/runtime/lapmatrud/bench/bool-c.runtime view
@@ -0,0 +1,1 @@+1.26
+ bench/runtime/lapmatrud/bench/list-c.runtime view
@@ -0,0 +1,1 @@+0.94
+ bench/runtime/lapmatrud/bench/list-t.runtime view
@@ -0,0 +1,1 @@+0.24
+ bench/runtime/lapmatrud/bench/minus-c.runtime view
@@ -0,0 +1,1 @@+0.51
+ bench/runtime/lapmatrud/bench/stats.runtime view
@@ -0,0 +1,1 @@+0.16
bench/runtime/lapmatrud/eg/arith-negate-abs.runtime view
@@ -1,1 +1,1 @@-0.92+1.02
bench/runtime/lapmatrud/eg/arith.runtime view
@@ -1,1 +1,1 @@-0.14+0.16
bench/runtime/lapmatrud/eg/binarytree.runtime view
@@ -1,1 +1,1 @@-0.90+1.00
bench/runtime/lapmatrud/eg/binarytree0.runtime view
@@ -1,1 +1,1 @@-0.28+0.31
bench/runtime/lapmatrud/eg/bool.runtime view
@@ -1,1 +1,1 @@-1.05+1.43
bench/runtime/lapmatrud/eg/colour.runtime view
@@ -1,1 +1,1 @@-1.07+1.16
bench/runtime/lapmatrud/eg/digraphs.runtime view
@@ -1,1 +1,1 @@-0.80+0.90
bench/runtime/lapmatrud/eg/fun.runtime view
@@ -1,1 +1,1 @@-0.58+0.64
bench/runtime/lapmatrud/eg/insertsort.runtime view
@@ -1,1 +1,1 @@-4.08+4.47
bench/runtime/lapmatrud/eg/insertsort0.runtime view
@@ -1,1 +1,1 @@-0.52+0.55
bench/runtime/lapmatrud/eg/length.runtime view
@@ -1,1 +1,1 @@-0.25+0.14
bench/runtime/lapmatrud/eg/list.runtime view
@@ -1,1 +1,1 @@-1.38+1.51
bench/runtime/lapmatrud/eg/minus.runtime view
@@ -1,1 +1,1 @@-0.34+0.30
bench/runtime/lapmatrud/eg/monad.runtime view
@@ -1,1 +1,1 @@-0.36+0.37
bench/runtime/lapmatrud/eg/oddeven.runtime view
@@ -1,1 +1,1 @@-3.56+3.90
bench/runtime/lapmatrud/eg/plus-abs.runtime view
@@ -1,1 +1,1 @@-1.94+2.17
bench/runtime/lapmatrud/eg/ratio.runtime view
@@ -1,1 +1,1 @@-4.39+4.87
bench/runtime/lapmatrud/eg/sets.runtime view
@@ -1,1 +1,1 @@-4.09+4.93
bench/runtime/lapmatrud/eg/speculate-reason.runtime view
@@ -1,1 +1,1 @@-1.59+1.62
bench/runtime/lapmatrud/eg/string.runtime view
@@ -1,1 +1,1 @@-0.52+0.53
bench/runtime/lapmatrud/eg/tauts.runtime view
@@ -1,1 +1,1 @@-2.34+2.32
bench/runtime/lapmatrud/eg/tuples.runtime view
@@ -1,1 +1,1 @@-0.74+0.72
bench/runtime/lapmatrud/eg/zip.runtime view
@@ -1,1 +1,1 @@-1.24+1.39
+ bench/runtime/zero/bench/addition.runtime view
@@ -0,0 +1,1 @@+0.45
bench/runtime/zero/bench/arith-c.runtime view
@@ -1,1 +1,1 @@-0.75+0.60
bench/runtime/zero/bench/arith-t.runtime view
@@ -1,1 +1,1 @@-11.26+10.02
bench/runtime/zero/bench/arithficial.runtime view
@@ -1,1 +1,1 @@-0.44+0.60
bench/runtime/zero/bench/bool-c.runtime view
@@ -1,1 +1,1 @@-2.14+1.81
bench/runtime/zero/bench/list-c.runtime view
@@ -1,1 +1,1 @@-1.59+1.60
bench/runtime/zero/bench/list-t.runtime view
@@ -1,1 +1,1 @@-0.43+0.48
bench/runtime/zero/bench/lowtests.runtime view
@@ -1,1 +1,1 @@-0.48+0.46
bench/runtime/zero/bench/minus-c.runtime view
@@ -1,1 +1,1 @@-0.90+0.91
bench/runtime/zero/bench/stats.runtime view
@@ -1,1 +1,1 @@-0.28+0.30
bench/runtime/zero/bench/trilean.runtime view
@@ -1,1 +1,1 @@-0.04+0.05
bench/runtime/zero/eg/arith-negate-abs.runtime view
@@ -1,1 +1,1 @@-1.78+1.58
bench/runtime/zero/eg/arith.runtime view
@@ -1,1 +1,1 @@-0.28+0.26
bench/runtime/zero/eg/binarytree.runtime view
@@ -1,1 +1,1 @@-1.90+1.89
bench/runtime/zero/eg/binarytree0.runtime view
@@ -1,1 +1,1 @@-0.53+0.60
bench/runtime/zero/eg/bool.runtime view
@@ -1,1 +1,1 @@-2.49+2.42
bench/runtime/zero/eg/digraphs.runtime view
@@ -1,1 +1,1 @@-1.54+1.49
bench/runtime/zero/eg/fun.runtime view
@@ -1,1 +1,1 @@-1.07+1.08
bench/runtime/zero/eg/insertsort.runtime view
@@ -1,1 +1,1 @@-7.74+7.38
bench/runtime/zero/eg/length.runtime view
@@ -1,1 +1,1 @@-0.25+0.24
bench/runtime/zero/eg/minus.runtime view
@@ -1,1 +1,1 @@-0.52+0.65
bench/runtime/zero/eg/monad.runtime view
@@ -1,1 +1,1 @@-0.59+0.61
bench/runtime/zero/eg/oddeven.runtime view
@@ -1,1 +1,1 @@-6.87+6.85
bench/runtime/zero/eg/plus-abs.runtime view
@@ -1,1 +1,1 @@-3.77+3.50
bench/runtime/zero/eg/ratio.runtime view
@@ -1,1 +1,1 @@-8.34+7.64
bench/runtime/zero/eg/sets.runtime view
@@ -1,1 +1,1 @@-7.94+7.34
bench/runtime/zero/eg/speculate-reason.runtime view
@@ -1,1 +1,1 @@-2.98+2.95
bench/runtime/zero/eg/string.runtime view
@@ -1,1 +1,1 @@-0.92+0.87
bench/runtime/zero/eg/tauts.runtime view
@@ -1,1 +1,1 @@-4.12+4.13
bench/runtime/zero/eg/tuples.runtime view
@@ -1,1 +1,1 @@-1.28+1.27
bench/runtime/zero/eg/zip.runtime view
@@ -1,1 +1,1 @@-2.38+2.41
changelog.md view
@@ -2,6 +2,17 @@ =======================  +v0.4.20 (February 2024)+-----------------------++* minor changes only+* improve `consider` by favouring the normalization+  _only_ if it reduces the number of variables+* revert back (v0.4.16) to using vanilla syntactic unification+  instead of syntactic unification modulo commutativity+* some internal refactoring++ v0.4.18 (February 2024) -----------------------
eg/insertsort.txt view
@@ -30,7 +30,7 @@     ([] == 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)
eg/insertsort0.txt view
@@ -22,7 +22,7 @@     (xs == insert x xs) == False    ([] == insert x xs) == False-            (xs == []) == ([] == sort xs)+       (sort xs == []) == (xs == [])                sort [] == []         sort (sort xs) == sort xs            insert x [] == [x]
mk/depend.mk view
@@ -1,3 +1,36 @@+bench/addition: \+  bench/addition.hs \+  mk/toplibs+bench/addition.o: \+  src/Test/Speculate/Utils/Tuple.hs \+  src/Test/Speculate/Utils/Timeout.hs \+  src/Test/Speculate/Utils/Tiers.hs \+  src/Test/Speculate/Utils/String.hs \+  src/Test/Speculate/Utils/PrettyPrint.hs \+  src/Test/Speculate/Utils.hs \+  src/Test/Speculate/Utils/Ord.hs \+  src/Test/Speculate/Utils/Misc.hs \+  src/Test/Speculate/Utils/Memoize.hs \+  src/Test/Speculate/Utils/List.hs \+  src/Test/Speculate/Utils/Digraph.hs \+  src/Test/Speculate/Utils/Colour.hs \+  src/Test/Speculate/Utils/Class.hs \+  src/Test/Speculate/SemiReason.hs \+  src/Test/Speculate/Sanity.hs \+  src/Test/Speculate/Report.hs \+  src/Test/Speculate/Reason.hs \+  src/Test/Speculate/Reason/Order.hs \+  src/Test/Speculate/Pretty.hs \+  src/Test/Speculate.hs \+  src/Test/Speculate/Expr.hs \+  src/Test/Speculate/Expr/Instance.hs \+  src/Test/Speculate/Expr/Ground.hs \+  src/Test/Speculate/Expr/Equate.hs \+  src/Test/Speculate/Expr/Core.hs \+  src/Test/Speculate/Engine.hs \+  src/Test/Speculate/CondReason.hs \+  src/Test/Speculate/Args.hs \+  bench/addition.hs bench/arithficial: \   bench/arithficial.hs \   mk/toplibs
speculate.cabal view
@@ -1,5 +1,5 @@ name:                speculate-version:             0.4.18+version:             0.4.20 synopsis:            discovery of properties about Haskell functions description:   Speculate automatically discovers laws about Haskell functions.@@ -70,7 +70,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/speculate-  tag:             v0.4.18+  tag:             v0.4.20   library
src/Test/Speculate/Engine.hs view
@@ -180,8 +180,8 @@   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
src/Test/Speculate/Reason.hs view
@@ -158,7 +158,7 @@ normalize :: Thy -> Expr -> Expr normalize Thy {rules = rs} = n   where-  n e = case concatMap (e `reductions1`) rs of+  n e = case concatMap (`reductions1` e) rs of           []     -> e -- already normalized           (e':_) -> n e' @@ -167,7 +167,7 @@ normalizeE thy@(Thy {equations = eqs, canReduceTo = (->-)})  =  n1   where   n1  =  n2 . normalize thy-  n2 e = case filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of+  n2 e = case filter (e ->-) (concatMap (`reductions1` e) $ eqs ++ map swap eqs) of          []     -> e -- already normalized          (e':_) -> n1 e' @@ -188,12 +188,14 @@ reduceRoot e (e1,e2) = (e2 //-) <$> (e `match` e1)  -- Lists all reductions by one rule, note that reductions may be repeated.-reductions1 :: Expr -> Rule -> [Expr]-reductions1 e (l,_) | size l > size e = [] -- optional optimization-reductions1 e@(e1 :$ e2) r = maybeToList (e `reduceRoot` r)-                          ++ map (:$ e2) (reductions1 e1 r)-                          ++ map (e1 :$) (reductions1 e2 r)-reductions1 e r = maybeToList (e `reduceRoot` r)+reductions1 :: Rule -> Expr -> [Expr]+reductions1 r@(l,_)  =  r1+  where+  r1 e  |  size l > size e  =  [] -- optional optimization+  r1 e@(e1 :$ e2)  =  maybeToList (e `reduceRoot` r)+                   ++ map (:$ e2) (r1 e1)+                   ++ map (e1 :$) (r1 e2)+  r1 e  =  maybeToList (e `reduceRoot` r)  -- as defined by Martin & Nipkow in "Ordered Rewriting and Confluence" on 1990 -- this definition is sound, but incomplete (some groundJoinable pairs won't be@@ -225,7 +227,7 @@       nubSortBy compareEqnQuickly     . map sortuple     . filter (uncurry (/=))-    . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))+    . concatMap (\e -> (r1 `reductions1` e) ** (r2 `reductions1` e))     $ overlaps e1 e2   xs ** ys = [(x,y) | x <- xs, y <- ys]   sortuple (x,y) | x < y     = (y,x)@@ -237,12 +239,11 @@   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'@@ -269,7 +270,7 @@   where   eqs = equations thy   step = nubMergeMap reductionsEqs1-  reductionsEqs1 e = e `L.insert` nubMergeMap (reductions1 e) (eqs ++ map swap eqs)+  reductionsEqs1 e = e `L.insert` nubMergeMap (`reductions1` e) (eqs ++ map swap eqs)  insert :: Equation -> Thy -> Thy insert (e1,e2) thy@@ -358,7 +359,7 @@   collapsable = not . null . collapse   collapse :: Rule -> [Equation]   collapse (e1,e2) = foldr (+++) []-    [ nubSort [ canonicalizeEqn thy (e,e2) | e <- reductions1 e1 (e1',e2') ]+    [ nubSort [ canonicalizeEqn thy (e,e2) | e <- reductions1 (e1',e2') e1 ]     | (e1',e2') <- rs     , (e1',e2') /= (e1,e2)     , e1 =| e1' ]
test/reason.hs view
@@ -42,7 +42,7 @@    putStrLn "\\e e1 e2 -> length $ reductions 1 e (e1,e2)"   reportCountsBy (\(e,e1,e2) -> if e1 > e2 && typ e1 == typ e2-                                  then "OK, length " ++ show (length $ reductions1 e (e1,e2))+                                  then "OK, length " ++ show (length $ reductions1 (e1,e2) e)                                   else "Not OK")                  (take n list)