speculate 0.4.4 → 0.4.6

raw patch · 22 files changed

+354/−181 lines, 22 filesdep ~expressdep ~leancheckPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: express, leancheck

API changes (from Hackage documentation)

Files

• .gitignore +1/−0
• Makefile +1/−0
• TODO.md +2/−10
• bench/runtime-zero +30/−29
• bench/trilean.hs +113/−0
• mk/depend.mk +44/−0
• mk/haskell.mk +7/−1
• speculate.cabal +5/−5
• src/Test/Speculate.hs +2/−0
• src/Test/Speculate/Args.hs +0/−12
• src/Test/Speculate/Engine.hs +32/−24
• src/Test/Speculate/Expr/Core.hs +22/−21
• src/Test/Speculate/Function.hs +0/−44
• src/Test/Speculate/Function/A10.hs +21/−0
• src/Test/Speculate/Function/A100.hs +2/−1
• src/Test/Speculate/Function/A1000.hs +2/−1
• src/Test/Speculate/Reason.hs +24/−10
• src/Test/Speculate/Report.hs +2/−2
• stack.yaml +2/−2
• test/model/trilean-s4.out +18/−0
• test/model/trilean.out +18/−0
• test/order.hs +6/−19

@@ -88,6 +88,7 @@ bench/arithficial bench/nord bench/unit+bench/trilean bench/qs*/0arith bench/qs*/arith-negate-abs bench/qs*/arith

@@ -51,6 +51,7 @@   eg/speculate-reason \   bench/arithficial \   bench/nord \+  bench/trilean \   bench/unit EXTRAEG = \   eg/regexes \

@@ -3,12 +3,9 @@  A list of things to do for Speculate. -* simpilfy "bench" handing.  Do like in LeanCheck and Extrapolate.+* remove lexicompare as it is already exported by Express -* improve performance of the Reason module:-  when listing rewrites of a given expression,-  I can use a custom data structure that computes-  matches all at once while traversing an expression.+* simpilfy "bench" handing.  Do like in LeanCheck and Extrapolate.  * (code readability) review and document code @@ -21,8 +18,3 @@   the expensive thing.  But it does not pay off to test x + y = z + w before   testing x + y = y + x.  The second needs to hold for the first to hold.  And,   it will be far more common!--* (performance and interface): actually compute what happens with-  undefined values.  e.g.: head [] == undefined.  This will/may make things-  faster as we can prune foo (head []) or head [] ++ head [], which are also-  undefined.

@@ -1,34 +1,35 @@ GHC 8.10.4-express-0.1.4-leancheck-0.9.3+express-0.1.5+leancheck-0.9.4 arith               0.233-arith-c             0.570-arithficial         0.860-arith-negate-abs    1.713-binarytree          1.633-binarytree0         0.483-bool                1.963-bool-c              1.730-colour              1.946-digraphs            1.460-fun                 1.103-insertsort          7.613+arith-c             0.593+arithficial         0.636+arith-negate-abs    1.776+binarytree          1.666+binarytree0         0.506+bool                1.973+bool-c              1.776+colour              2.006+digraphs            1.513+fun                 1.086+insertsort          7.743 insertsort0         0.913-length              0.460-list                2.586-list-c              1.596-minus               0.506-minus-c             0.883-monad               0.583+length              0.480+list                2.593+list-c              1.660+minus               0.516+minus-c             0.880+monad               0.570 nord                0.010-oddeven             6.673-plus-abs            3.543-pretty              8.953-ratio               8.093-sets                7.183-speculate-reason    3.016-string              0.856-tauts               4.073-tuples              1.200+oddeven             6.593+plus-abs            3.663+pretty              9.030+ratio               8.336+sets                7.230+speculate-reason    2.950+string              0.860+tauts               4.070+trilean             0.010+tuples              1.233 unit                0.010-zip                 2.303+zip                 2.323

@@ -0,0 +1,113 @@+-- bench/trilean.hs -- Speculate example on trileans+--+-- Copyright (C) 2021  Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+--+--+-- If used correctly,+-- Speculate deals with Trileans just fine producing correct equations.+--+--+-- The point of this example is to make Speculate produce incorrect equations+-- by failing to include all possible values on the 'Listable' enumeration.+--+-- Of the three possible trilean values (@M@, @F@ and @T@),+-- here we fail to enumerate @M@.  This ultimately causes Speculate print:+--+-- > p == M+--+-- How does that happen?+--+-- We first test to discover that:+--+-- > p &&& F == F+--+-- This is only true when x is F and T (the tested values)+-- but not true in general.+-- Speculate does not know this, then by consequence,+-- it infers:+--+-- > M &&& F == F+--+-- Which, using the correct equation @ M &&& p  ==  M @, rewrites to:+--+-- > M == F+--+-- Similarly we also get that:+--+-- > T == M+--+-- Ultimately arriving at:+--+-- > p == M+--+--+-- This illustrates why Speculate cannot consider equality between error values+-- using 'Test.LeanCheck.Error.errorToEither'+-- or    'Test.LeanCheck.Error.errorToNothing'.+--+-- You could also think now, to include error values in the generation,+-- however you will lose interesting equations if you do that+-- so it does not pay off.++{-# Language DeriveDataTypeable, StandaloneDeriving #-}  -- for GHC <= 7.8++import Test.Speculate hiding ((|||), (&&&))+import Test.Speculate.Function.A10+import Test.LeanCheck.Function.ShowFunction++data Tril = M | F | T deriving (Show, Eq, Ord)++deriving instance Typeable Tril  -- for GHC <= 7.8++instance Listable Tril where+  tiers  =  cons0 F+         \/ cons0 T+--       \/ cons0 M `ofWeight` 1+-- Here we intentionally fail to enumerate M.++instance ShowFunction Tril where bindtiers = bindtiersShow++instance Name Tril where+  name _  =  "p"++neg :: Tril -> Tril+neg T = F+neg F = T+neg M = M++unc :: Tril -> Tril+unc M = T+unc _ = F++(&&&) :: Tril -> Tril -> Tril+M &&& _  =  M+_ &&& M  =  M+T &&& T  =  T+_ &&& _  =  F++(|||) :: Tril -> Tril -> Tril+M ||| _  =  M+_ ||| M  =  M+F ||| F  =  F+_ ||| _  =  T++(===>) :: Tril -> Tril -> Tril+M ===> _  =  M+F ===> _  =  T+T ===> p  =  p++main :: IO ()+main = speculate args+  { constants =+      [ showConstant M+      , showConstant F+      , showConstant T+      , constant "neg" neg+      , constant "&&&" (&&&)+--    , constant "|||" (|||)+      ]+  , instances = [ reifyInstances (undefined :: Tril)+--              , reifyInstances (undefined :: Tril -> Tril -> Tril)+                ]+  }

@@ -64,6 +64,41 @@   src/Test/Speculate/CondReason.hs \   src/Test/Speculate/Args.hs \   bench/nord.hs+bench/trilean: \+  bench/trilean.hs \+  mk/toplibs+bench/trilean.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/Function.hs \+  src/Test/Speculate/Function/A100.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/trilean.hs bench/unit: \   bench/unit.hs \   mk/toplibs@@ -1078,6 +1113,15 @@   src/Test/Speculate/Engine.hs \   src/Test/Speculate/CondReason.hs src/Test/Speculate/Expr/Core.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/Expr/Core.hs src/Test/Speculate/Expr/Equate.o: \

@@ -80,7 +80,8 @@   # Cleaning rule (add as a clean dependency)-.PHONY: clean-hi-o+clean-hs: clean-hi-o clean-haddock clean-cabal clean-stack+ clean-hi-o: 	find $(ALL_HSS) | sed -e 's/hs$$/o/'      | xargs rm -f 	find $(ALL_HSS) | sed -e 's/hs$$/hi/'     | xargs rm -f@@ -113,6 +114,11 @@ 	  $(HADDOCK_HLNK_SRC) \ 	  $(HADDOCKFLAGS) +clean-cabal:+	rm -rf dist/ dist-newstyle/ cabal.project.local cabal.project.local~++clean-stack:+	rm -rf .stack-work/ stack.yaml.lock  # lists all Haskell source files list-all-hss:

@@ -1,5 +1,5 @@ name:                speculate-version:             0.4.4+version:             0.4.6 synopsis:            discovery of properties about Haskell functions description:   Speculate automatically discovers laws about Haskell functions.@@ -84,13 +84,13 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/speculate-  tag:             v0.4.4+  tag:             v0.4.6   library   exposed-modules: Test.Speculate                  , Test.Speculate.Args-                 , Test.Speculate.Function+                 , Test.Speculate.Function.A10                  , Test.Speculate.Function.A100                  , Test.Speculate.Function.A1000                  , Test.Speculate.Report@@ -120,8 +120,8 @@                  , Test.Speculate.Utils.Timeout                  , Test.Speculate.Utils.Tuple   build-depends: base >= 4 && < 5-               , leancheck >= 0.9.3-               , express >= 0.1.4+               , leancheck >= 0.9.4+               , express >= 0.1.6                , cmdargs                , containers   hs-source-dirs:    src

@@ -52,6 +52,7 @@   , reifyOrd   , reifyEqOrd   , reifyListable+  , reifyName   , mkEq   , mkOrd   , mkOrdLessEqual@@ -87,6 +88,7 @@   , reifyOrd   , reifyEqOrd   , reifyListable+  , reifyName   , mkEq   , mkOrd   , mkOrdLessEqual

@@ -23,7 +23,6 @@   , computeInstances   , types   , atoms-  , compareExpr   , keepExpr   , timeout   , shouldShowEquation@@ -228,17 +227,6 @@ timeout :: Args -> Bool -> Bool timeout Args{evalTimeout = Nothing} = id timeout Args{evalTimeout = Just t}  = timeoutToFalse t--compareExpr :: Args -> Expr -> Expr -> Ordering-compareExpr args = compareComplexity <> lexicompareBy cmp-  where-  e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT-  e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT-  e1 `cmp` e2 = compareIndex (exprPair:concat (atoms args)) e1 e2 <> e1 `compare` e2-  exprPair = head . unfoldApp $ foldPair (val (), val ())--- NOTE: "concat $ atoms args" may be an infinite list.  This function assumes--- that the symbols will appear on the list eventually for termination.  If I--- am correct this ivariant is assured by the rest of the code.  constant :: Typeable a => String -> a -> Expr constant = value

@@ -15,6 +15,9 @@   , theoryAndRepresentativesFromAtoms   , representativesFromAtoms   , theoryFromAtoms+  , theoryAndRepresentativesFromAtomsKeeping+  , representativesFromAtomsKeeping+  , theoryFromAtomsKeeping   , equivalencesBetween    , consider@@ -110,7 +113,7 @@  -- | Computes a theory from atomic expressions.  Example: ----- > > theoryFromAtoms 5 compare (const True) (equal preludeInstances 100)+-- > > theoryFromAtoms 5 (const True) (equal preludeInstances 100) -- > >   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)] -- > Thy { rules = [ (x + y) + z == x + (y + z) ] -- >     , equations = [ y + x == x + y@@ -121,15 +124,21 @@ -- >     , closureLimit = 2 -- >     , keepE = keepUpToLength 5 -- >     }-theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> Thy-theoryFromAtoms sz cmp keep (===) = fst . theoryAndRepresentativesFromAtoms sz cmp keep (===)--- TODO: eliminate two arguments:--- * cmp can default to use order of appearance--- * keep can default to "const True"+theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy+theoryFromAtoms  =  theoryFromAtomsKeeping (const True) -representativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]]-representativesFromAtoms sz cmp keep (===) = snd . theoryAndRepresentativesFromAtoms sz cmp keep (===)+representativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]+representativesFromAtoms  =  representativesFromAtomsKeeping (const True) +theoryAndRepresentativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy,[[Expr]])+theoryAndRepresentativesFromAtoms  =  theoryAndRepresentativesFromAtomsKeeping (const True)++theoryFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy+theoryFromAtomsKeeping keep (===) sz  =  fst . theoryAndRepresentativesFromAtomsKeeping keep (===) sz++representativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]+representativesFromAtomsKeeping keep (===) sz  =  snd . theoryAndRepresentativesFromAtomsKeeping keep (===) sz+ expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [Expr] -> (Thy,[[Expr]]) -> (Thy,[[Expr]]) expand keep (===) sz ss (thy,sss) = (complete *** id)                                   . foldl (flip $ consider (===) sz) (thy,sss)@@ -141,12 +150,10 @@   fes *$* xes = filter keep $ catMaybes [fe $$ xe | fe <- fes, xe <- xes]  -- | Given atomic expressions, compute theory and representative schema---   expressions.-theoryAndRepresentativesFromAtoms :: Int-                                  -> (Expr -> Expr -> Ordering)-                                  -> (Expr -> Bool) -> (Expr -> Expr -> Bool)-                                  -> [[Expr]] -> (Thy,[[Expr]])-theoryAndRepresentativesFromAtoms sz cmp keep (===) dss =+--   expressions.  (cf. 'theoryFromAtoms')+theoryAndRepresentativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool)+                                         -> Int -> [[Expr]] -> (Thy,[[Expr]])+theoryAndRepresentativesFromAtomsKeeping keep (===) sz dss  =   chain [expand keep (===) sz' (dss ! (sz'-1)) | sz' <- reverse [1..sz]] (iniThy,[])   where   iniThy = emptyThy { keepE = keepUpToLength sz@@ -154,6 +161,10 @@                     , canReduceTo = dwoBy (\e1 e2 -> e1 `cmp` e2 == GT)                     , compareE = cmp                     }+  cmp  =  compareComplexityThenIndex (concat dss)+  -- NOTE: "concat dss" may be an infinite list.  This function assumes that+  -- the symbols will appear on the list eventually for termination.  If I am+  -- correct, this invariant is assured by the rest of the code.  -- considers a schema consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy,[[Expr]]) -> (Thy,[[Expr]])@@ -163,8 +174,8 @@   | otherwise =     ( append thy $ equivalencesBetween (-===-) ns ns ++ eqs     , if any (\(e1,e2) -> unrepeatedVars e1 && unrepeatedVars e2) eqs-        then sss-        else sssWs )+      then sss+      else sssWs )   where   ns = rehole $ normalizeE thy (fastMostGeneralVariation s)   e1 -===- e2  =  normalize thy e1 == normalize thy e2 || e1 === e2@@ -240,13 +251,11 @@   . filter (isOrd ti)  conditionalTheoryFromThyAndReps :: Instances-                                -> (Expr -> Expr -> Ordering)                                 -> Int -> Int -> Int                                 -> Thy -> [Expr] -> Chy-conditionalTheoryFromThyAndReps ti cmp nt nv csz thy es' =+conditionalTheoryFromThyAndReps ti nt nv csz thy es' =   conditionalEquivalences-    cmp-    (canonicalCEqnBy cmp ti)+    (canonicalCEqnBy (compareE thy) ti)     (condEqual ti nt)     (lessOrEqual ti nt)     csz thy clpres cles@@ -256,15 +265,14 @@                 . filter (isEq ti . fst)                 $ classesFromSchemas ti nt nv thy es' -conditionalEquivalences :: (Expr -> Expr -> Ordering)-                        -> ((Expr,Expr,Expr) -> Bool)+conditionalEquivalences :: ((Expr,Expr,Expr) -> Bool)                         -> (Expr -> Expr -> Expr -> Bool)                         -> (Expr -> Expr -> Bool)                         -> Int -> Thy -> [Class Expr] -> [Class Expr] -> Chy-conditionalEquivalences cmp canon cequal (==>) csz thy clpres cles =+conditionalEquivalences canon cequal (==>) csz thy clpres cles =     cdiscard (\(ce,e1,e2) -> subConsequence thy clpres ce e1 e2)   . foldl (flip cinsert) (Chy [] cdg clpres thy)-  . sortBy (cmp `on` foldTrio)+  . sortBy (compareE thy `on` foldTrio)   . discard (\(pre,e1,e2) -> pre == val False                           || length (nubVars pre \\ (nubVars e1 +++ nubVars e2)) > 0                           || subConsequence thy [] pre e1 e2)

@@ -12,9 +12,8 @@   , module Data.Express.Utils.Typeable    -- * Order-  , lexicompare-  , lexicompareBy-  , fastCompare+  , compareLexicographicallyBy+  , compareComplexityThenIndex    -- * Properties   , isConstantNamed@@ -34,25 +33,15 @@  import Data.Express import Data.Express.Utils.Typeable-import Test.Speculate.Utils.List+import Test.Speculate.Utils import Data.Monoid ((<>)) import Data.Functor ((<$>)) -- for GHC <= 7.8 --- faster comparison, to be used when nubSorting Expr values-fastCompare :: Expr -> Expr -> Ordering-fastCompare  =  cmp-  where-  (f :$ x)       `cmp` (g :$ y)        =  f  `cmp` g <> x `cmp` y-  (_ :$ _)       `cmp` _               =  GT-  _              `cmp` (_ :$ _)        =  LT-  x@(Value n1 _) `cmp` y@(Value n2 _)  =  typ x `compareTy` typ y-                                       <> n1 `compare` n2--lexicompare :: Expr -> Expr -> Ordering-lexicompare = lexicompareBy compare--lexicompareBy :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering-lexicompareBy compareConstants  =  cmp+-- | Lexicographical comparison of 'Expr's+--   where variables < constants < applications and+--   constants are disambiguated by the given function.+compareLexicographicallyBy :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering+compareLexicographicallyBy compareConstants  =  cmp   where   (f :$ x) `cmp` (g :$ y)  =  f  `cmp` g <> x `cmp` y   (_ :$ _) `cmp` _         =  GT@@ -60,11 +49,23 @@   e1 `cmp` e2  =  case (isVar e1, isVar e2) of     (True,  True)  -> let Value n1 _ = e1                           Value n2 _ = e2-                      in typ e1 `compareTy` typ e2 <> n1 `compare` n2+                      in typ e1 `compareTy` typ e2+                      <> length n1 `compare` length n2+                      <> n1 `compare` n2     (False, True)  -> GT     (True,  False) -> LT     (False, False) -> e1 `compareConstants` e2-  -- Var < Constants < Apps++-- | Comparison of 'Expr's:+--+-- 1. 'compareComplexity' from 'Data.Express'+-- 2. 'lexicompareBy' index of the given list+compareComplexityThenIndex :: [Expr] -> Expr -> Expr -> Ordering+compareComplexityThenIndex as  =  compareComplexity <> compareLexicographicallyBy cmp+  where+  e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT+  e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT+  e1 `cmp` e2 = compareIndex as e1 e2 <> e1 `compare` e2  countVars :: Expr -> [(Expr,Int)] countVars e = map (\e' -> (e',length . filter (== e') $ vars e)) $ nubVars e

@@ -1,44 +0,0 @@--- |--- Module      : Test.Speculate.Function--- Copyright   : (c) 2016-2019 Rudy Matela--- License     : 3-Clause BSD  (see the file LICENSE)--- Maintainer  : Rudy Matela <rudy@matela.com.br>------ This module is part of Speculate.------ If should import this if you want Speculate to treat functions as data--- values.  This exports a Listable instance for functions an a facility to--- define Eq and Ord instances for functions.------ Please see the @fun@ and @monad@ examples from Speculate's source--- repository for more details.-module Test.Speculate.Function-  ( funToList-  , areEqualFor-  , compareFor-  )-where--import Test.Speculate-import Test.LeanCheck.Function()-import Test.LeanCheck.Error (errorToNothing)-import Data.Function (on)--funToList :: Listable a => (a -> b) -> [Maybe b]-funToList f = map (errorToNothing . f) list---- | This function can be used to define an Eq instance for functions based on---   testing and equality of returned values, like so:------ > instance (Listable a, Eq b) => Eq (a -> b) where--- >   (==) = areEqualFor 100-areEqualFor :: (Listable a, Eq b) => Int -> (a -> b) -> (a -> b) -> Bool-areEqualFor n = (==) `on` (take n . funToList)---- | This function can be used to define an Ord instance for functions based on---   testing and ordering of returned values, like so:------ > instance (Listable a, Ord b) => Ord (a -> b) where--- >   compare = compareFor 100-compareFor :: (Listable a, Ord b) => Int -> (a -> b) -> (a -> b) -> Ordering-compareFor n = compare `on` (take n . funToList)

@@ -0,0 +1,21 @@+-- |+-- Module      : Test.Speculate.Function.A10+-- Copyright   : (c) 2019 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Speculate.+--+-- This module exports a Listable instance for functions along with two toy Eq+-- and Ord instances for functions based on 10 sample return values.+module Test.Speculate.Function.A10 () where++import Test.Speculate+import Test.LeanCheck.Function ()+import Test.LeanCheck.Function.List (areEqualFor, compareFor)++instance (Listable a, Eq b) => Eq (a -> b) where+  (==) = areEqualFor 10++instance (Listable a, Ord b) => Ord (a -> b) where+  compare = compareFor 10

@@ -11,7 +11,8 @@ module Test.Speculate.Function.A100 () where  import Test.Speculate-import Test.Speculate.Function+import Test.LeanCheck.Function ()+import Test.LeanCheck.Function.List (areEqualFor, compareFor)  instance (Listable a, Eq b) => Eq (a -> b) where   (==) = areEqualFor 100

@@ -11,7 +11,8 @@ module Test.Speculate.Function.A1000 () where  import Test.Speculate-import Test.Speculate.Function+import Test.LeanCheck.Function ()+import Test.LeanCheck.Function.List (areEqualFor, compareFor)  instance (Listable a, Eq b) => Eq (a -> b) where   (==) = areEqualFor 1000

@@ -13,6 +13,8 @@   , normalize   , normalizeE   , isNormal+  , isRootNormal+  , isRootNormalE   , complete   , equivalent   , equivalentInstance@@ -157,16 +159,28 @@  -- normalize by rules and equations normalizeE :: Thy -> Expr -> Expr-normalizeE Thy {rules = rs, equations = eqs, canReduceTo = (->-) } = n+normalizeE thy@(Thy {equations = eqs, canReduceTo = (->-)})  =  n1   where-  n e = case concatMap (e `reductions1`) rs-          ++ filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of-          []     -> e -- already normalized-          (e':_) -> n e'+  n1  =  n2 . normalize thy+  n2 e = case filter (e ->-) (concatMap (e `reductions1`) $ eqs ++ map swap eqs) of+         []     -> e -- already normalized+         (e':_) -> n1 e'  isNormal :: Thy -> Expr -> Bool isNormal thy e = normalizeE thy e == e +isRootNormal :: Thy -> Expr -> Bool+isRootNormal thy e  =  none (e `isInstanceOf`) $ map fst (rules thy)+  where+  none p  =  not . any p++isRootNormalE :: Thy -> Expr -> Bool+isRootNormalE thy e  =  isRootNormal thy e+                    &&  null (filter (e ->-) . mapMaybe (reduceRoot e) $ equations thy ++ map swap (equations thy))+  where+  (->-)  =  canReduceTo thy+  reduceRoot e (e1,e2) = (e2 //-) <$> (e `match` e1)+ reduceRoot :: Expr -> Rule -> Maybe Expr reduceRoot e (e1,e2) = (e2 //-) <$> (e `match` e1) @@ -209,22 +223,22 @@  criticalPairs :: Thy -> [(Expr,Expr)] criticalPairs thy@Thy{rules = rs}  =-  nubMergesBy fastCompareEqn [r `criticalPairsWith` s | r <- rs, s <- rs]+  nubMergesBy compareEqnQuickly [r `criticalPairsWith` s | r <- rs, s <- rs]   where   criticalPairsWith :: Rule -> Rule -> [(Expr,Expr)]   r1@(e1,_) `criticalPairsWith` r2@(e2,_) =-      nubSortBy fastCompareEqn+      nubSortBy compareEqnQuickly     . map sortuple     . filter (uncurry (/=))     . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))-    . nubSortBy fastCompare+    . nubSortBy compareQuickly     $ overlaps e1 e2   xs ** ys = [(x,y) | x <- xs, y <- ys]   sortuple (x,y) | x < y     = (y,x)                  | otherwise = (x,y)-  fastCompareEqn = fastCompare `on` foldPair+  compareEqnQuickly = compareQuickly `on` foldPair   (<) :: Expr -> Expr -> Bool-  e1 < e2 = e1 `fastCompare` e2 == LT+  e1 < e2 = e1 `compareQuickly` e2 == LT  -- Warning: will have to also be applied in reverse to get all overlaps. --

@@ -32,7 +32,7 @@   let ti = computeInstances args   let ats = types args   let dss = atoms args-  let (thy,ess) = theoryAndRepresentativesFromAtoms sz (compareExpr args) (keepExpr args) (timeout args .: equal ti n) dss+  let (thy,ess) = theoryAndRepresentativesFromAtomsKeeping (keepExpr args) (timeout args .: equal ti n) sz dss   let es = uptoT sz ess   putArgs args   -- TODO: somehow show the tail of dss, maybe use "..."@@ -50,7 +50,7 @@   when (showTheory args)       . putStrLn $ showThy thy   let shy = semiTheoryFromThyAndReps ti n (maxVars args) thy           $ filter (\e -> size e <= computeMaxSemiSize args) es-  let chy = conditionalTheoryFromThyAndReps ti (compareExpr args) n (maxVars args) (computeMaxCondSize args) thy es+  let chy = conditionalTheoryFromThyAndReps ti n (maxVars args) (computeMaxCondSize args) thy es   let equations     = finalEquations     (shouldShowEquation args) ti                          thy   let semiEquations = finalSemiEquations (shouldShowEquation args) ti (equivalentInstance thy) shy   let condEquations = finalCondEquations (shouldShowConditionalEquation args)                  chy

@@ -4,5 +4,5 @@ - .  extra-deps:-- leancheck-0.9.3-- express-0.1.4+- leancheck-0.9.4+- express-0.1.6

@@ -0,0 +1,18 @@+max expr size  =    4+  |- on ineqs  =    3+  |- on conds  =    3+max  #-tests   =  500+min  #-tests   =   25  (to consider p ==> q true)+max  #-vars    =    2  (for inequational and conditional laws)++_ :: Tril+M :: Tril+F :: Tril+T :: Tril+neg :: Tril -> Tril+(&&&) :: Tril -> Tril -> Tril++p == M++M <= p+

@@ -0,0 +1,18 @@+max expr size  =    5+  |- on ineqs  =    4+  |- on conds  =    4+max  #-tests   =  500+min  #-tests   =   25  (to consider p ==> q true)+max  #-vars    =    2  (for inequational and conditional laws)++_ :: Tril+M :: Tril+F :: Tril+T :: Tril+neg :: Tril -> Tril+(&&&) :: Tril -> Tril -> Tril++p == M++M <= p+

@@ -19,23 +19,10 @@ tests n =   [ True -- see test-expr.hs for general Expr orders -  , holds n $ compare ==== (compareComplexity <> lexicompare)-  , holds n $ isComparison lexicompare-  , holds n $ isComparison compareComplexity--  , holds n $ \(IntToIntE e1) (IntToIntE e2) (IntE e3) -> let cmp = lexicompare in-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)-  , holds n $ \(IntToIntE e1) (IntToIntE e2) (IntE e3) -> let cmp = lexicompareBy (flip compare) in-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)-  , holds n $ \(BoolToBoolE e1) (BoolToBoolE e2) (BoolE e3) -> let cmp = lexicompare in-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)-  , holds n $ \(BoolToBoolE e1) (BoolToBoolE e2) (BoolE e3) -> let cmp = lexicompareBy (flip compare) in-                e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)--  -- some tests of order-  , value "xx" xx < zero-  , value "xxeqxx" (Equation xx xx) < value "xx" xx-  , value "xx" xx < value "emptyThyght" (Thyght emptyThy)+  , holds n $ compareLexicographicallyBy compareLexicographically ==== compareLexicographically+  , holds n $ compareLexicographicallyBy compare ==== compareLexicographically+  , holds n $ isComparison (compareLexicographicallyBy $ flip compareLexicographically)+  , holds n $ isComparison (compareLexicographicallyBy $ flip compare)    , holds n $ simplificationOrder (|>|)   , holds n $ seriousSimplificationOrder (|> )@@ -78,7 +65,7 @@   , holds n $ \e     -> weightExcept absE (abs' e)    == weightExcept absE e   , holds n $ \e     -> weightExcept absE (negate' e) == weightExcept absE e + 1 -  -- lexicompare is compatible (almost as if by coincidence)+  -- compareLexicographically is compatible (almost as if by coincidence)   , fails n $ simplificationOrder lgt   , holds n $ compatible          lgt   , fails n $ closedUnderSub      lgt@@ -91,7 +78,7 @@   , holds n $ subtermProperty     cgt   ]   where-  e1 `lgt` e2 = e1 `lexicompare` e2 == GT+  e1 `lgt` e2 = e1 `compareLexicographically` e2 == GT   e1 `cgt` e2 = e1 `compare` e2 == GT  -- weaker than simplificationOrder