-- | The main QuickSpec module, with internal stuff exported.
-- For QuickSpec hackers only.
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
module QuickSpec.Internal where

import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..), HasFriendly, FriendlyPredicateTestCase)
import qualified QuickSpec.Internal.Haskell as Haskell
import qualified QuickSpec.Internal.Haskell.Resolve as Haskell
import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck
import qualified QuickSpec.Internal.Pruning.UntypedTwee as Twee
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Term(Term)
import QuickSpec.Internal.Explore.Schemas(VariableUse(..))
import Test.QuickCheck
import Test.QuickCheck.Random
import Data.Constraint
import Data.Lens.Light
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Type hiding (defaultTo)
import Data.Proxy
import System.Environment
#if !MIN_VERSION_base(4,9,0)
import Data.Semigroup(Semigroup(..))
#endif

-- | Run QuickSpec. See the documentation at the top of this file.
quickSpec :: Signature sig => sig -> IO ()
quickSpec :: forall sig. Signature sig => sig -> IO ()
quickSpec sig
sig = do
  forall sig. Signature sig => sig -> IO [Prop (Term Constant)]
quickSpecResult sig
sig
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Run QuickSpec, returning the list of discovered properties.
quickSpecResult :: Signature sig => sig -> IO [Prop (Term Haskell.Constant)]
quickSpecResult :: forall sig. Signature sig => sig -> IO [Prop (Term Constant)]
quickSpecResult sig
sig = do
  -- Undocumented feature for testing :)
  Maybe String
seed <- String -> IO (Maybe String)
lookupEnv String
"QUICKCHECK_SEED"
  let
    sig' :: Sig
sig' = case Maybe String
seed of
      Maybe String
Nothing -> forall sig. Signature sig => sig -> Sig
signature sig
sig
      Just String
xs -> forall sig. Signature sig => sig -> Sig
signature [forall sig. Signature sig => sig -> Sig
signature sig
sig, Int -> Sig
withFixedSeed (forall a. Read a => String -> a
read String
xs)]

  Config -> IO [Prop (Term Constant)]
Haskell.quickSpec (forall sig. Signature sig => sig -> Context -> Config -> Config
runSig Sig
sig' (Int -> [String] -> Context
Context Int
1 []) Config
Haskell.defaultConfig)

-- | Add some properties to the background theory.
addBackground :: [Prop (Term Haskell.Constant)] -> Sig
addBackground :: [Prop (Term Constant)] -> Sig
addBackground [Prop (Term Constant)]
props =
  (Context -> Config -> Config) -> Sig
Sig forall a b. (a -> b) -> a -> b
$ \Context
_ Config
cfg -> Config
cfg { cfg_background :: [Prop (Term Constant)]
Haskell.cfg_background = Config -> [Prop (Term Constant)]
Haskell.cfg_background Config
cfg forall a. [a] -> [a] -> [a]
++ [Prop (Term Constant)]
props }

-- | A signature.
newtype Sig = Sig { Sig -> Context -> Config -> Config
unSig :: Context -> Haskell.Config -> Haskell.Config }

-- Settings for building the signature.
-- Int: number of nested calls to 'background'.
-- [String]: list of names to exclude.
data Context = Context Int [String]

instance Semigroup Sig where
  Sig Context -> Config -> Config
sig1 <> :: Sig -> Sig -> Sig
<> Sig Context -> Config -> Config
sig2 = (Context -> Config -> Config) -> Sig
Sig (\Context
ctx -> Context -> Config -> Config
sig2 Context
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config -> Config
sig1 Context
ctx)
instance Monoid Sig where
  mempty :: Sig
mempty = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a. a -> a
id)
  mappend :: Sig -> Sig -> Sig
mappend = forall a. Semigroup a => a -> a -> a
(<>)

-- | A class of things that can be used as a QuickSpec signature.
class Signature sig where
  -- | Convert the thing to a signature.
  signature :: sig -> Sig

instance Signature Sig where
  signature :: Sig -> Sig
signature = forall a. a -> a
id

instance Signature sig => Signature [sig] where
  signature :: [sig] -> Sig
signature = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall sig. Signature sig => sig -> Sig
signature

runSig :: Signature sig => sig -> Context -> Haskell.Config -> Haskell.Config
runSig :: forall sig. Signature sig => sig -> Context -> Config -> Config
runSig = Sig -> Context -> Config -> Config
unSig forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sig. Signature sig => sig -> Sig
signature

-- | Declare a constant with a given name and value.
-- If the constant you want to use is polymorphic, you can use the types
-- `A`, `B`, `C`, `D`, `E` to monomorphise it, for example:
--
-- > constant "reverse" (reverse :: [A] -> [A])
--
-- QuickSpec will then understand that the constant is really polymorphic.
con :: Typeable a => String -> a -> Sig
con :: forall a. Typeable a => String -> a -> Sig
con String
name a
x =
  (Context -> Config -> Config) -> Sig
Sig forall a b. (a -> b) -> a -> b
$ \ctx :: Context
ctx@(Context Int
_ [String]
names) ->
    if String
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
names then forall a. a -> a
id else
      Sig -> Context -> Config -> Config
unSig (Constant -> Sig
customConstant (forall a. Typeable a => String -> a -> Constant
Haskell.con String
name a
x)) Context
ctx

-- | Add a custom constant.
customConstant :: Haskell.Constant -> Sig
customConstant :: Constant -> Sig
customConstant Constant
con =
  (Context -> Config -> Config) -> Sig
Sig forall a b. (a -> b) -> a -> b
$ \(Context Int
n [String]
_) ->
    forall a b. Lens a b -> (b -> b) -> a -> a
modL Lens Config [[Constant]]
Haskell.lens_constants (forall a. Int -> [a] -> [[a]] -> [[a]]
appendAt Int
n [Constant
con])

-- | Type class constraints as first class citizens
type c ==> t = Dict c -> t

-- | Lift a constrained type to a `==>` type which QuickSpec
-- can work with
liftC :: (c => a) -> c ==> a
liftC :: forall (c :: Constraint) a. (c => a) -> c ==> a
liftC c => a
a Dict c
Dict = c => a
a

-- | Add an instance of a type class to the signature
instanceOf :: forall c. (Typeable c, c) => Sig
instanceOf :: forall (c :: Constraint). (Typeable c, c) => Sig
instanceOf = forall (c1 :: Constraint) (c2 :: Constraint).
(Typeable c1, Typeable c2) =>
(c1 :- c2) -> Sig
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- c)

-- | Declare a predicate with a given name and value.
-- The predicate should be a function which returns `Bool`.
-- It will appear in equations just like any other constant,
-- but will also be allowed to appear as a condition.
--
-- Warning: if the predicate is unlikely to be true for a
-- randomly-generated value, you will get bad-quality test data.
-- In that case, use `predicateGen` instead.
--
-- For example:
--
-- @
-- sig = [
--   `con` "delete" (`Data.List.delete` :: Int -> [Int] -> [Int]),
--   `con` "insert" (`Data.List.insert` :: Int -> [Int] -> [Int]),
--   predicate "member" (member :: Int -> [Int] -> Bool) ]
-- @
predicate :: ( Predicateable a
             , Haskell.PredicateResult a ~ Bool
             , Typeable a
             , Typeable (PredicateTestCase a))
             => String -> a -> Sig
predicate :: forall a.
(Predicateable a, PredicateResult a ~ Bool, Typeable a,
 Typeable (PredicateTestCase a)) =>
String -> a -> Sig
predicate String
name a
x =
  (Context -> Config -> Config) -> Sig
Sig forall a b. (a -> b) -> a -> b
$ \ctx :: Context
ctx@(Context Int
_ [String]
names) ->
    if String
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
names then forall a. a -> a
id else
    let (Instances
insts, Constant
con) = forall a.
(Predicateable a, PredicateResult a ~ Bool, Typeable a,
 Typeable (PredicateTestCase a)) =>
String -> a -> (Instances, Constant)
Haskell.predicate String
name a
x in
      forall sig. Signature sig => sig -> Context -> Config -> Config
runSig [Instances -> Sig
addInstances Instances
insts forall a. Monoid a => a -> a -> a
`mappend` Constant -> Sig
customConstant Constant
con] Context
ctx

-- | Declare a predicate with a given name and value.
-- The predicate should be a function which returns `Bool`.
-- It will appear in equations just like any other constant,
-- but will also be allowed to appear as a condition.
-- The third argument is a generator for values satisfying the predicate.
--
-- For example, this declares a predicate that checks if a list is
-- sorted:
--
-- > predicateGen "sorted" sorted genSortedList
--
-- where
--
-- > sorted :: [a] -> Bool
-- > sorted xs = sort xs == xs
-- > genSortedList :: Gen [a]
-- > genSortedList = sort <$> arbitrary
predicateGen :: ( Predicateable a
                , Typeable a
                , Typeable (PredicateTestCase a)
                , HasFriendly (PredicateTestCase a))
                => String -> a -> Gen (FriendlyPredicateTestCase a) -> Sig
predicateGen :: forall a.
(Predicateable a, Typeable a, Typeable (PredicateTestCase a),
 HasFriendly (PredicateTestCase a)) =>
String -> a -> Gen (FriendlyPredicateTestCase a) -> Sig
predicateGen String
name a
x Gen (FriendlyPredicateTestCase a)
gen =
  (Context -> Config -> Config) -> Sig
Sig forall a b. (a -> b) -> a -> b
$ \ctx :: Context
ctx@(Context Int
_ [String]
names) ->
    if String
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
names then forall a. a -> a
id else
    let (Instances
insts, Constant
con) = forall a.
(Predicateable a, Typeable a, Typeable (PredicateTestCase a),
 HasFriendly (PredicateTestCase a)) =>
String
-> a -> Gen (FriendlyPredicateTestCase a) -> (Instances, Constant)
Haskell.predicateGen String
name a
x Gen (FriendlyPredicateTestCase a)
gen in
      forall sig. Signature sig => sig -> Context -> Config -> Config
runSig [Instances -> Sig
addInstances Instances
insts forall a. Monoid a => a -> a -> a
`mappend` Constant -> Sig
customConstant Constant
con] Context
ctx

-- | Declare a new monomorphic type.
-- The type must implement `Ord` and `Arbitrary`.
--
-- If the type does not implement `Ord`, you can use `monoTypeObserve`
-- to declare an observational equivalence function. If the type does
-- not implement `Arbitrary`, you can use `generator` to declare a
-- custom QuickCheck generator.
--
-- You do not necessarily need `Ord` and `Arbitrary` instances for
-- every type. If there is no `Ord` (or `Observe` instance) for a
-- type, you will not get equations between terms of that type. If
-- there is no `Arbitrary` instance (or generator), you will not get
-- variables of that type.
monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig
monoType :: forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Sig
monoType proxy a
_ =
  forall a. Monoid a => [a] -> a
mconcat [
    forall (c1 :: Constraint) (c2 :: Constraint).
(Typeable c1, Typeable c2) =>
(c1 :- c2) -> Sig
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- Ord a),
    forall (c1 :: Constraint) (c2 :: Constraint).
(Typeable c1, Typeable c2) =>
(c1 :- c2) -> Sig
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- Arbitrary a)]

-- | Like 'monoType', but designed to be used with TypeApplications directly.
--
-- For example, you can add 'Foo' to your signature via:
--
-- @
-- `mono` @Foo
-- @
mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig
mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig
mono = forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Sig
monoType (forall {k} (t :: k). Proxy t
Proxy @a)

-- | Declare a new monomorphic type using observational equivalence.
-- The type must implement `Observe` and `Arbitrary`.
monoTypeObserve :: forall proxy test outcome a.
  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
  proxy a -> Sig
monoTypeObserve :: forall (proxy :: * -> *) test outcome a.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
proxy a -> Sig
monoTypeObserve proxy a
_ =
  forall a. Monoid a => [a] -> a
mconcat [
    forall (c1 :: Constraint) (c2 :: Constraint).
(Typeable c1, Typeable c2) =>
(c1 :- c2) -> Sig
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- Observe test outcome a),
    forall (c1 :: Constraint) (c2 :: Constraint).
(Typeable c1, Typeable c2) =>
(c1 :- c2) -> Sig
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- Arbitrary a)]

-- | Like 'monoTypeObserve', but designed to be used with TypeApplications directly.
--
-- For example, you can add 'Foo' to your signature via:
--
-- @
-- `monoObserve` @Foo
-- @
monoObserve :: forall a test outcome.
  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
  Sig
monoObserve :: forall a test outcome.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
Sig
monoObserve = forall (proxy :: * -> *) test outcome a.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
proxy a -> Sig
monoTypeObserve (forall {k} (t :: k). Proxy t
Proxy @a)

-- | Declare a new monomorphic type using observational equivalence, saying how you want variables of that type to be named.
monoTypeObserveWithVars :: forall proxy test outcome a.
  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
  [String] -> proxy a -> Sig
monoTypeObserveWithVars :: forall (proxy :: * -> *) test outcome a.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
[String] -> proxy a -> Sig
monoTypeObserveWithVars [String]
xs proxy a
proxy =
  forall (proxy :: * -> *) test outcome a.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
proxy a -> Sig
monoTypeObserve proxy a
proxy forall a. Monoid a => a -> a -> a
`mappend` forall (proxy :: * -> *) a.
Typeable a =>
[String] -> proxy a -> Sig
vars [String]
xs proxy a
proxy

-- | Like 'monoTypeObserveWithVars', but designed to be used with TypeApplications directly.
--
-- For example, you can add 'Foo' to your signature via:
--
-- @
-- `monoObserveVars` @Foo ["foo"]
-- @
monoObserveVars :: forall a test outcome.
  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>
  [String] -> Sig
monoObserveVars :: forall a test outcome.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
[String] -> Sig
monoObserveVars [String]
xs = forall (proxy :: * -> *) test outcome a.
(Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a,
 Typeable test, Typeable outcome, Typeable a) =>
[String] -> proxy a -> Sig
monoTypeObserveWithVars [String]
xs (forall {k} (t :: k). Proxy t
Proxy @a)

-- | Declare a new monomorphic type, saying how you want variables of that type to be named.
monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig
monoTypeWithVars :: forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
[String] -> proxy a -> Sig
monoTypeWithVars [String]
xs proxy a
proxy =
  forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Sig
monoType proxy a
proxy forall a. Monoid a => a -> a -> a
`mappend` forall (proxy :: * -> *) a.
Typeable a =>
[String] -> proxy a -> Sig
vars [String]
xs proxy a
proxy

-- | Like 'monoTypeWithVars' designed to be used with TypeApplications directly.
--
-- For example, you can add 'Foo' to your signature via:
--
-- @
-- `monoVars` @Foo ["foo"]
-- @
monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig
monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig
monoVars [String]
xs = forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
[String] -> proxy a -> Sig
monoTypeWithVars [String]
xs (forall {k} (t :: k). Proxy t
Proxy @a)

-- | Customize how variables of a particular type are named.
vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig
vars :: forall (proxy :: * -> *) a.
Typeable a =>
[String] -> proxy a -> Sig
vars [String]
xs proxy a
_ = forall a. Typeable a => a -> Sig
instFun (forall a. [String] -> Names a
Names [String]
xs :: Names a)

-- | Constrain how variables of a particular type may occur in a term.
-- The default value is @'UpTo' 4@.
variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig
variableUse :: forall (proxy :: * -> *) a.
Typeable a =>
VariableUse -> proxy a -> Sig
variableUse VariableUse
x proxy a
_ = forall a. Typeable a => a -> Sig
instFun (forall a. VariableUse -> Use a
Use VariableUse
x :: Use a)

-- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and
-- `Arbitrary` instance for each type you want it to test.
--
-- For example, if you are testing @`Data.Map.Map` k v@, you will need to add
-- the following two declarations to your signature:
--
-- @
-- `inst` (`Sub` `Dict` :: (Ord A, Ord B) `:-` Ord (Map A B))
-- `inst` (`Sub` `Dict` :: (Arbitrary A, Arbitrary B) `:-` Arbitrary (Map A B))
-- @
--
-- For a monomorphic type @T@, you can use `monoType` instead, but if you
-- want to use `inst`, you can do it like this:
--
-- @
-- `inst` (`Sub` `Dict` :: () `:-` Ord T)
-- `inst` (`Sub` `Dict` :: () `:-` Arbitrary T)
-- @
inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig
inst :: forall (c1 :: Constraint) (c2 :: Constraint).
(Typeable c1, Typeable c2) =>
(c1 :- c2) -> Sig
inst = forall a. Typeable a => a -> Sig
instFun

-- | Declare a generator to be used to produce random values of a
-- given type. This will take precedence over any `Arbitrary` instance.
generator :: Typeable a => Gen a -> Sig
generator :: forall a. Typeable a => Gen a -> Sig
generator = forall a. Typeable a => a -> Sig
instFun

-- | Declare an arbitrary value to be used by instance resolution.
instFun :: Typeable a => a -> Sig
instFun :: forall a. Typeable a => a -> Sig
instFun a
x = Instances -> Sig
addInstances (forall a. Typeable a => a -> Instances
Haskell.inst a
x)

addInstances :: Haskell.Instances -> Sig
addInstances :: Instances -> Sig
addInstances Instances
insts =
  (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> (b -> b) -> a -> a
modL Lens Config Instances
Haskell.lens_instances (forall a. Monoid a => a -> a -> a
`mappend` Instances
insts))

withPrintFilter :: (Prop (Term Haskell.Constant) -> Bool) -> Sig
withPrintFilter :: (Prop (Term Constant) -> Bool) -> Sig
withPrintFilter Prop (Term Constant) -> Bool
p =
  (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL Lens Config (Prop (Term Constant) -> Bool)
Haskell.lens_print_filter Prop (Term Constant) -> Bool
p)

-- | Declare some functions as being background functions.
-- These are functions which are not interesting on their own,
-- but which may appear in interesting laws with non-background functions.
-- Declaring background functions may improve the laws you get out.
--
-- Here is an example, which tests @++@ and @length@, giving @0@ and @+@ as
-- background functions:
--
-- > main = quickSpec [
-- >   con "++" ((++) :: [A] -> [A] -> [A]),
-- >   con "length" (length :: [A] -> Int),
-- >
-- >   background [
-- >     con "0" (0 :: Int),
-- >     con "+" ((+) :: Int -> Int -> Int) ] ]
background :: Signature sig => sig -> Sig
background :: forall sig. Signature sig => sig -> Sig
background sig
sig =
  (Context -> Config -> Config) -> Sig
Sig (\(Context Int
_ [String]
xs) -> forall sig. Signature sig => sig -> Context -> Config -> Config
runSig sig
sig (Int -> [String] -> Context
Context Int
0 [String]
xs))

-- | Remove a function or predicate from the signature.
-- Useful in combination with 'prelude' and friends.
without :: Signature sig => sig -> [String] -> Sig
without :: forall sig. Signature sig => sig -> [String] -> Sig
without sig
sig [String]
xs =
  (Context -> Config -> Config) -> Sig
Sig (\(Context Int
n [String]
ys) -> forall sig. Signature sig => sig -> Context -> Config -> Config
runSig sig
sig (Int -> [String] -> Context
Context Int
n ([String]
ys forall a. [a] -> [a] -> [a]
++ [String]
xs)))

-- | Run QuickCheck on a series of signatures. Tests the functions in the first
-- signature, then adds the functions in the second signature, then adds the
-- functions in the third signature, and so on.
--
-- This can be useful when you have a core API you want to test first, and a
-- larger API you want to test later. The laws for the core API will be printed
-- separately from the laws for the larger API.
--
-- Here is an example which first tests @0@ and @+@ and then adds @++@ and @length@:
--
-- > main = quickSpec (series [sig1, sig2])
-- >   where
-- >     sig1 = [
-- >       con "0" (0 :: Int),
-- >       con "+" ((+) :: Int -> Int -> Int) ]
-- >     sig2 = [
-- >       con "++" ((++) :: [A] -> [A] -> [A]),
-- >       con "length" (length :: [A] -> Int) ]
series :: Signature sig => [sig] -> Sig
series :: forall sig. Signature sig => [sig] -> Sig
series = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {sig}. Signature sig => Sig -> sig -> Sig
op forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall sig. Signature sig => sig -> Sig
signature
  where
    op :: Sig -> sig -> Sig
op Sig
sig sig
sigs = Sig
sig forall a. Monoid a => a -> a -> a
`mappend` Sig -> Sig
later (forall sig. Signature sig => sig -> Sig
signature sig
sigs)
    later :: Sig -> Sig
later Sig
sig =
      (Context -> Config -> Config) -> Sig
Sig (\(Context Int
n [String]
xs) Config
cfg -> Sig -> Context -> Config -> Config
unSig Sig
sig (Int -> [String] -> Context
Context (Int
nforall a. Num a => a -> a -> a
+Int
1) [String]
xs) Config
cfg)

-- | Set the maximum size of terms to explore (default: 7).
withMaxTermSize :: Int -> Sig
withMaxTermSize :: Int -> Sig
withMaxTermSize Int
n = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL Lens Config Int
Haskell.lens_max_size Int
n)

withMaxCommutativeSize :: Int -> Sig
withMaxCommutativeSize :: Int -> Sig
withMaxCommutativeSize Int
n = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL Lens Config Int
Haskell.lens_max_commutative_size Int
n)

-- | Limit how many different function symbols can occur in a term.
withMaxFunctions :: Int -> Sig
withMaxFunctions :: Int -> Sig
withMaxFunctions Int
n = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL Lens Config Int
Haskell.lens_max_functions Int
n)

-- | Set how many times to test each discovered law (default: 1000).
withMaxTests :: Int -> Sig
withMaxTests :: Int -> Sig
withMaxTests Int
n =
  (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config Int
QuickCheck.lens_num_tests forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# Lens Config Config
Haskell.lens_quickCheck) Int
n)

-- | Set the maximum value for QuickCheck's size parameter when generating test
-- data (default: 20).
withMaxTestSize :: Int -> Sig
withMaxTestSize :: Int -> Sig
withMaxTestSize Int
n =
  (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config Int
QuickCheck.lens_max_test_size forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# Lens Config Config
Haskell.lens_quickCheck) Int
n)

-- | Set which type polymorphic terms are tested at.
defaultTo :: Typeable a => proxy a -> Sig
defaultTo :: forall a (proxy :: * -> *). Typeable a => proxy a -> Sig
defaultTo proxy a
proxy = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL Lens Config Type
Haskell.lens_default_to (forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep proxy a
proxy))

-- | Set how QuickSpec should display its discovered equations (default: 'ForHumans').
--
-- If you'd instead like to turn QuickSpec's output into QuickCheck tests, set
-- this to 'ForQuickCheck'.
withPrintStyle :: Haskell.PrintStyle -> Sig
withPrintStyle :: PrintStyle -> Sig
withPrintStyle PrintStyle
style = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL Lens Config PrintStyle
Haskell.lens_print_style PrintStyle
style)

-- | Set how hard QuickSpec tries to filter out redundant equations (default: no limit).
--
-- If you experience long pauses when running QuickSpec, try setting this number
-- to 2 or 3.
withPruningDepth :: Int -> Sig
withPruningDepth :: Int -> Sig
withPruningDepth Int
n =
  (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config Int
Twee.lens_max_cp_depth forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# Lens Config Config
Haskell.lens_twee) Int
n)

-- | Set the maximum term size QuickSpec will reason about when it filters out
-- redundant equations (default: same as maximum term size).
--
-- If you get laws you believe are redundant, try increasing this number to 1 or
-- 2 more than the maximum term size.
withPruningTermSize :: Int -> Sig
withPruningTermSize :: Int -> Sig
withPruningTermSize Int
n =
  (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config Int
Twee.lens_max_term_size forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# Lens Config Config
Haskell.lens_twee) Int
n)

-- | Set the random number seed used for test case generation.
-- Useful if you want repeatable results.
withFixedSeed :: Int -> Sig
withFixedSeed :: Int -> Sig
withFixedSeed Int
s = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config (Maybe QCGen)
QuickCheck.lens_fixed_seed forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# Lens Config Config
Haskell.lens_quickCheck) (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> QCGen
mkQCGen forall a b. (a -> b) -> a -> b
$ Int
s))

-- | Automatically infer types to add to the universe from
-- available type class instances
withInferInstanceTypes :: Sig
withInferInstanceTypes :: Sig
withInferInstanceTypes = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config Bool
Haskell.lens_infer_instance_types) Bool
True)

-- | (Experimental) Check that the discovered laws do not imply any
-- false laws
withConsistencyCheck :: Sig
withConsistencyCheck :: Sig
withConsistencyCheck = (Context -> Config -> Config) -> Sig
Sig (\Context
_ -> forall a b. Lens a b -> b -> a -> a
setL (Lens Config Bool
Haskell.lens_check_consistency) Bool
True)

-- | A signature containing boolean functions:
-- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
bools :: Sig
bools :: Sig
bools = forall sig. Signature sig => sig -> Sig
background [
  String
"||"    forall a. Typeable a => String -> a -> Sig
`con` Bool -> Bool -> Bool
(||),
  String
"&&"    forall a. Typeable a => String -> a -> Sig
`con` Bool -> Bool -> Bool
(&&),
  String
"not"   forall a. Typeable a => String -> a -> Sig
`con` Bool -> Bool
not,
  String
"True"  forall a. Typeable a => String -> a -> Sig
`con` Bool
True,
  String
"False" forall a. Typeable a => String -> a -> Sig
`con` Bool
False]

-- | A signature containing arithmetic operations:
-- @0@, @1@, @(`+`)@.
-- Instantiate it with e.g. @arith (`Proxy` :: `Proxy` `Int`)@.
arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig
arith :: forall (proxy :: * -> *) a.
(Typeable a, Ord a, Num a, Arbitrary a) =>
proxy a -> Sig
arith proxy a
proxy = forall sig. Signature sig => sig -> Sig
background [
  forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Sig
monoType proxy a
proxy,
  String
"0" forall a. Typeable a => String -> a -> Sig
`con` (a
0   :: a),
  String
"1" forall a. Typeable a => String -> a -> Sig
`con` (a
1   :: a),
  String
"+" forall a. Typeable a => String -> a -> Sig
`con` (forall a. Num a => a -> a -> a
(+) :: a -> a -> a)]

-- | A signature containing list operations:
-- @[]@, @(:)@, @(`++`)@.
lists :: Sig
lists :: Sig
lists = forall sig. Signature sig => sig -> Sig
background [
  String
"[]"      forall a. Typeable a => String -> a -> Sig
`con` ([]      :: [A]),
  String
":"       forall a. Typeable a => String -> a -> Sig
`con` ((:)     :: A -> [A] -> [A]),
  String
"++"      forall a. Typeable a => String -> a -> Sig
`con` (forall a. [a] -> [a] -> [a]
(++)    :: [A] -> [A] -> [A])]

-- | A signature containing higher-order functions:
-- @(`.`)@ and `id`.
-- Useful for testing `map` and similar.
funs :: Sig
funs :: Sig
funs = forall sig. Signature sig => sig -> Sig
background [
  String
"."  forall a. Typeable a => String -> a -> Sig
`con` (forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) :: (A -> A) -> (A -> A) -> (A -> A)),
  String
"id" forall a. Typeable a => String -> a -> Sig
`con` (forall a. a -> a
id  :: A -> A) ]

-- | The QuickSpec prelude.
-- Contains boolean, arithmetic and list functions, and function composition.
-- For more precise control over what gets included,
-- see 'bools', 'arith', 'lists', 'funs' and 'without'.
prelude :: Sig
prelude :: Sig
prelude = forall sig. Signature sig => sig -> Sig
signature [Sig
bools, forall (proxy :: * -> *) a.
(Typeable a, Ord a, Num a, Arbitrary a) =>
proxy a -> Sig
arith (forall {k} (t :: k). Proxy t
Proxy :: Proxy Int), Sig
lists]