{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
module QuickSpec.Internal where
import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))
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 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
import Data.Semigroup(Semigroup(..))
quickSpec :: Signature sig => sig -> IO ()
quickSpec sig = do
quickSpecResult sig
return ()
quickSpecResult :: Signature sig => sig -> IO [Prop (Term Haskell.Constant)]
quickSpecResult sig = do
seed <- lookupEnv "QUICKCHECK_SEED"
let
sig' = case seed of
Nothing -> signature sig
Just xs -> signature [signature sig, withFixedSeed (read xs)]
Haskell.quickSpec (runSig sig' (Context 1 []) Haskell.defaultConfig)
addBackground :: [Prop (Term Haskell.Constant)] -> Sig
addBackground props =
Sig $ \_ cfg -> cfg { Haskell.cfg_background = Haskell.cfg_background cfg ++ props }
newtype Sig = Sig { unSig :: Context -> Haskell.Config -> Haskell.Config }
data Context = Context Int [String]
instance Semigroup Sig where
Sig sig1 <> Sig sig2 = Sig (\ctx -> sig2 ctx . sig1 ctx)
instance Monoid Sig where
mempty = Sig (\_ -> id)
mappend = (<>)
class Signature sig where
signature :: sig -> Sig
instance Signature Sig where
signature = id
instance Signature sig => Signature [sig] where
signature = mconcat . map signature
runSig :: Signature sig => sig -> Context -> Haskell.Config -> Haskell.Config
runSig = unSig . signature
con :: Typeable a => String -> a -> Sig
con name x =
Sig $ \ctx@(Context _ names) ->
if name `elem` names then id else
unSig (customConstant (Haskell.con name x)) ctx
customConstant :: Haskell.Constant -> Sig
customConstant con =
Sig $ \(Context n _) ->
modL Haskell.lens_constants (appendAt n [con])
type c ==> t = Dict c -> t
liftC :: (c => a) -> c ==> a
liftC a Dict = a
instanceOf :: forall c. (Typeable c, c) => Sig
instanceOf = inst (Sub Dict :: () :- c)
predicate :: ( Predicateable a
, Typeable a
, Typeable (PredicateTestCase a))
=> String -> a -> Sig
predicate name x =
Sig $ \ctx@(Context _ names) ->
if name `elem` names then id else
let (insts, con) = Haskell.predicate name x in
runSig [addInstances insts `mappend` customConstant con] ctx
predicateGen :: ( Predicateable a
, Typeable a
, Typeable b
, Typeable (PredicateTestCase a))
=> String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig
predicateGen name x gen =
Sig $ \ctx@(Context _ names) ->
if name `elem` names then id else
let (insts, con) = Haskell.predicateGen name x gen in
runSig [addInstances insts `mappend` customConstant con] ctx
monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig
monoType _ =
mconcat [
inst (Sub Dict :: () :- Ord a),
inst (Sub Dict :: () :- Arbitrary a)]
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 _ =
mconcat [
inst (Sub Dict :: () :- Observe test outcome a),
inst (Sub Dict :: () :- Arbitrary a)]
monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig
monoTypeWithVars xs proxy =
monoType proxy `mappend` vars xs proxy
vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig
vars xs _ = instFun (Names xs :: Names a)
inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig
inst = instFun
instFun :: Typeable a => a -> Sig
instFun x = addInstances (Haskell.inst x)
addInstances :: Haskell.Instances -> Sig
addInstances insts =
Sig (\_ -> modL Haskell.lens_instances (`mappend` insts))
withPrintFilter :: (Prop (Term Haskell.Constant) -> Bool) -> Sig
withPrintFilter p =
Sig (\_ -> setL Haskell.lens_print_filter p)
background :: Signature sig => sig -> Sig
background sig =
Sig (\(Context _ xs) -> runSig sig (Context 0 xs))
without :: Signature sig => sig -> [String] -> Sig
without sig xs =
Sig (\(Context n ys) -> runSig sig (Context n (ys ++ xs)))
series :: Signature sig => [sig] -> Sig
series = foldr op mempty . map signature
where
op sig sigs = sig `mappend` later (signature sigs)
later sig =
Sig (\(Context n xs) cfg -> unSig sig (Context (n+1) xs) cfg)
withMaxTermSize :: Int -> Sig
withMaxTermSize n = Sig (\_ -> setL Haskell.lens_max_size n)
withMaxCommutativeSize :: Int -> Sig
withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n)
withMaxTests :: Int -> Sig
withMaxTests n =
Sig (\_ -> setL (QuickCheck.lens_num_tests # Haskell.lens_quickCheck) n)
withMaxTestSize :: Int -> Sig
withMaxTestSize n =
Sig (\_ -> setL (QuickCheck.lens_max_test_size # Haskell.lens_quickCheck) n)
defaultTo :: Typeable a => proxy a -> Sig
defaultTo proxy = Sig (\_ -> setL Haskell.lens_default_to (typeRep proxy))
withPruningDepth :: Int -> Sig
withPruningDepth n =
Sig (\_ -> setL (Twee.lens_max_cp_depth # Haskell.lens_twee) n)
withPruningTermSize :: Int -> Sig
withPruningTermSize n =
Sig (\_ -> setL (Twee.lens_max_term_size # Haskell.lens_twee) n)
withFixedSeed :: Int -> Sig
withFixedSeed s = Sig (\_ -> setL (QuickCheck.lens_fixed_seed # Haskell.lens_quickCheck) (Just . mkQCGen $ s))
withInferInstanceTypes :: Sig
withInferInstanceTypes = Sig (\_ -> setL (Haskell.lens_infer_instance_types) True)
bools :: Sig
bools = background [
"||" `con` (||),
"&&" `con` (&&),
"not" `con` not,
"True" `con` True,
"False" `con` False]
arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig
arith proxy = background [
monoType proxy,
"0" `con` (0 :: a),
"1" `con` (1 :: a),
"+" `con` ((+) :: a -> a -> a)]
lists :: Sig
lists = background [
"[]" `con` ([] :: [A]),
":" `con` ((:) :: A -> [A] -> [A]),
"++" `con` ((++) :: [A] -> [A] -> [A])]
funs :: Sig
funs = background [
"." `con` ((.) :: (A -> A) -> (A -> A) -> (A -> A)),
"id" `con` (id :: A -> A) ]
prelude :: Sig
prelude = signature [bools, arith (Proxy :: Proxy Int), lists]