    -- | For documentation, see the paper "SmallCheck and Lazy SmallCheck:
    -- automatic exhaustive testing for small values" available at
    -- <http://www.cs.york.ac.uk/fp/smallcheck/>.  Several examples are
    -- also included in the package.

    module Test.LazySmallCheck
      ( Serial(series) -- :: class
      , Series         -- :: type Series a = Int -> Cons a
      , Cons           -- :: *
      , cons           -- :: a -> Series a
      , (><)           -- :: Series (a -> b) -> Series a -> Series b
      , empty          -- :: Series a
      , (\/)           -- :: Series a -> Series a -> Series a
      , drawnFrom      -- :: [a] -> Cons a
      , cons0          -- :: a -> Series a
      , cons1          -- :: Serial a => (a -> b) -> Series b
      , cons2          -- :: (Serial a, Serial b) => (a -> b -> c) -> Series c
      , cons3          -- :: ...
      , cons4          -- :: ...
      , cons5          -- :: ...
      , Testable       -- :: class
      , depthCheck     -- :: Testable a => Int -> a -> IO ()
      , smallCheck     -- :: Testable a => Int -> a -> IO ()
      , test           -- :: Testable a => a -> IO ()
      , (==>)          -- :: Bool -> Bool -> Bool
      , Property       -- :: *
      , lift           -- :: Bool -> Property
      , neg            -- :: Property -> Property
      , (*&*)          -- :: Property -> Property -> Property
      , (*|*)          -- :: Property -> Property -> Property
      , (*=>*)         -- :: Property -> Property -> Property
      , (*=*)          -- :: Property -> Property -> Property
      )
      where

    import Control.Monad
    import Control.Exception
    import System.Exit

    infixr 0 ==>, *=>*
    infixr 3 \/, *|*
    infixl 4 ><, *&*

    type Pos = [Int]

    data Term = Var Pos Type | Ctr Int [Term]

    data Type = SumOfProd [[Type]]

    type Series a = Int -> Cons a

    data Cons a = C Type ([[Term] -> a])

    class Serial a where
      series :: Series a

    -- Series constructors

    cons :: a -> Series a
    cons :: forall a. a -> Series a
    cons a
    a Int
    d = Type -> [[Term] -> a] -> Cons a
    forall a. Type -> [[Term] -> a] -> Cons a
    C ([[Type]] -> Type
    SumOfProd [[]]) [a -> [Term] -> a
    forall a b. a -> b -> a
    const a
    a]

    empty :: Series a
    empty :: forall a. Series a
    empty Int
    d = Type -> [[Term] -> a] -> Cons a
    forall a. Type -> [[Term] -> a] -> Cons a
    C ([[Type]] -> Type
    SumOfProd []) []

    (><) :: Series (a -> b) -> Series a -> Series b
    (Series (a -> b)
    f >< :: forall a b. Series (a -> b) -> Series a -> Series b
    >< Series a
    a) Int
    d = Type -> [[Term] -> b] -> Cons b
    forall a. Type -> [[Term] -> a] -> Cons a
    C ([[Type]] -> Type
    SumOfProd [Type
    taType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    p | Bool
    shallow, [Type]
    p <- [[Type]]
    ps]) [[Term] -> b]
    cs
      where
        C (SumOfProd [[Type]]
    ps) [[Term] -> a -> b]
    cfs = Series (a -> b)
    f Int
    d
        C Type
    ta [[Term] -> a]
    cas = Series a
    a (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)
        cs :: [[Term] -> b]
    cs = [\(Term
    x:[Term]
    xs) -> [Term] -> a -> b
    cf [Term]
    xs ([[Term] -> a] -> Term -> a
    forall a. [[Term] -> a] -> Term -> a
    conv [[Term] -> a]
    cas Term
    x) | Bool
    shallow, [Term] -> a -> b
    cf <- [[Term] -> a -> b]
    cfs]
        shallow :: Bool
    shallow = Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 Bool -> Bool -> Bool
    && Type -> Bool
    nonEmpty Type
    ta

    nonEmpty :: Type -> Bool
    nonEmpty :: Type -> Bool
    nonEmpty (SumOfProd [[Type]]
    ps) = Bool -> Bool
    not ([[Type]] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Type]]
    ps)

    (\/) :: Series a -> Series a -> Series a
    (Series a
    a \/ :: forall a. Series a -> Series a -> Series a
    \/ Series a
    b) Int
    d = Type -> [[Term] -> a] -> Cons a
    forall a. Type -> [[Term] -> a] -> Cons a
    C ([[Type]] -> Type
    SumOfProd ([[Type]]
    ssa [[Type]] -> [[Type]] -> [[Type]]
    forall a. [a] -> [a] -> [a]
    ++ [[Type]]
    ssb)) ([[Term] -> a]
    ca [[Term] -> a] -> [[Term] -> a] -> [[Term] -> a]
    forall a. [a] -> [a] -> [a]
    ++ [[Term] -> a]
    cb)
      where
        C (SumOfProd [[Type]]
    ssa) [[Term] -> a]
    ca = Series a
    a Int
    d
        C (SumOfProd [[Type]]
    ssb) [[Term] -> a]
    cb = Series a
    b Int
    d

    conv :: [[Term] -> a] -> Term -> a
    conv :: forall a. [[Term] -> a] -> Term -> a
    conv [[Term] -> a]
    cs (Var Pos
    p Type
    _) = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error (Char
    '\0'Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :(Int -> Char) -> Pos -> [Char]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Char
    forall a. Enum a => Int -> a
    toEnum Pos
    p)
    conv [[Term] -> a]
    cs (Ctr Int
    i [Term]
    xs) = ([[Term] -> a]
    cs [[Term] -> a] -> Int -> [Term] -> a
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    i) [Term]
    xs

    drawnFrom :: [a] -> Cons a
    drawnFrom :: forall a. [a] -> Cons a
    drawnFrom [a]
    xs = Type -> [[Term] -> a] -> Cons a
    forall a. Type -> [[Term] -> a] -> Cons a
    C ([[Type]] -> Type
    SumOfProd ((a -> [Type]) -> [a] -> [[Type]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Type] -> a -> [Type]
    forall a b. a -> b -> a
    const []) [a]
    xs)) ((a -> [Term] -> a) -> [a] -> [[Term] -> a]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> [Term] -> a
    forall a b. a -> b -> a
    const [a]
    xs)

    -- Helpers, a la SmallCheck

    cons0 :: a -> Series a
    cons0 :: forall a. a -> Series a
    cons0 a
    f = a -> Series a
    forall a. a -> Series a
    cons a
    f

    cons1 :: Serial a => (a -> b) -> Series b
    cons1 :: forall a b. Serial a => (a -> b) -> Series b
    cons1 a -> b
    f = (a -> b) -> Series (a -> b)
    forall a. a -> Series a
    cons a -> b
    f Series (a -> b) -> Series a -> Series b
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series a
    forall a. Serial a => Series a
    series

    cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
    cons2 :: forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
    cons2 a -> b -> c
    f = (a -> b -> c) -> Series (a -> b -> c)
    forall a. a -> Series a
    cons a -> b -> c
    f Series (a -> b -> c) -> Series a -> Series (b -> c)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series a
    forall a. Serial a => Series a
    series Series (b -> c) -> Series b -> Series c
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series b
    forall a. Serial a => Series a
    series

    cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
    cons3 :: forall a b c d.
    (Serial a, Serial b, Serial c) =>
    (a -> b -> c -> d) -> Series d
    cons3 a -> b -> c -> d
    f = (a -> b -> c -> d) -> Series (a -> b -> c -> d)
    forall a. a -> Series a
    cons a -> b -> c -> d
    f Series (a -> b -> c -> d) -> Series a -> Series (b -> c -> d)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series a
    forall a. Serial a => Series a
    series Series (b -> c -> d) -> Series b -> Series (c -> d)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series b
    forall a. Serial a => Series a
    series Series (c -> d) -> Series c -> Series d
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series c
    forall a. Serial a => Series a
    series

    cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
      (a -> b -> c -> d -> e) -> Series e
    cons4 :: forall a b c d e.
    (Serial a, Serial b, Serial c, Serial d) =>
    (a -> b -> c -> d -> e) -> Series e
    cons4 a -> b -> c -> d -> e
    f = (a -> b -> c -> d -> e) -> Series (a -> b -> c -> d -> e)
    forall a. a -> Series a
    cons a -> b -> c -> d -> e
    f Series (a -> b -> c -> d -> e)
    -> Series a -> Series (b -> c -> d -> e)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series a
    forall a. Serial a => Series a
    series Series (b -> c -> d -> e) -> Series b -> Series (c -> d -> e)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series b
    forall a. Serial a => Series a
    series Series (c -> d -> e) -> Series c -> Series (d -> e)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series c
    forall a. Serial a => Series a
    series Series (d -> e) -> Series d -> Series e
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series d
    forall a. Serial a => Series a
    series

    cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
      (a -> b -> c -> d -> e -> f) -> Series f
    cons5 :: forall a b c d e f.
    (Serial a, Serial b, Serial c, Serial d, Serial e) =>
    (a -> b -> c -> d -> e -> f) -> Series f
    cons5 a -> b -> c -> d -> e -> f
    f = (a -> b -> c -> d -> e -> f) -> Series (a -> b -> c -> d -> e -> f)
    forall a. a -> Series a
    cons a -> b -> c -> d -> e -> f
    f Series (a -> b -> c -> d -> e -> f)
    -> Series a -> Series (b -> c -> d -> e -> f)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series a
    forall a. Serial a => Series a
    series Series (b -> c -> d -> e -> f)
    -> Series b -> Series (c -> d -> e -> f)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series b
    forall a. Serial a => Series a
    series Series (c -> d -> e -> f) -> Series c -> Series (d -> e -> f)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series c
    forall a. Serial a => Series a
    series Series (d -> e -> f) -> Series d -> Series (e -> f)
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series d
    forall a. Serial a => Series a
    series Series (e -> f) -> Series e -> Series f
    forall a b. Series (a -> b) -> Series a -> Series b
    >< Series e
    forall a. Serial a => Series a
    series

    -- Standard instances

    instance Serial () where
      series :: Series ()
    series = () -> Series ()
    forall a. a -> Series a
    cons0 ()

    instance Serial Bool where
      series :: Series Bool
    series = Bool -> Series Bool
    forall a. a -> Series a
    cons0 Bool
    False Series Bool -> Series Bool -> Series Bool
    forall a. Series a -> Series a -> Series a
    \/ Bool -> Series Bool
    forall a. a -> Series a
    cons0 Bool
    True

    instance Serial a => Serial (Maybe a) where
      series :: Series (Maybe a)
    series = Maybe a -> Series (Maybe a)
    forall a. a -> Series a
    cons0 Maybe a
    forall a. Maybe a
    Nothing Series (Maybe a) -> Series (Maybe a) -> Series (Maybe a)
    forall a. Series a -> Series a -> Series a
    \/ (a -> Maybe a) -> Series (Maybe a)
    forall a b. Serial a => (a -> b) -> Series b
    cons1 a -> Maybe a
    forall a. a -> Maybe a
    Just

    instance (Serial a, Serial b) => Serial (Either a b) where
      series :: Series (Either a b)
    series = (a -> Either a b) -> Series (Either a b)
    forall a b. Serial a => (a -> b) -> Series b
    cons1 a -> Either a b
    forall a b. a -> Either a b
    Left Series (Either a b) -> Series (Either a b) -> Series (Either a b)
    forall a. Series a -> Series a -> Series a
    \/ (b -> Either a b) -> Series (Either a b)
    forall a b. Serial a => (a -> b) -> Series b
    cons1 b -> Either a b
    forall a b. b -> Either a b
    Right

    instance Serial a => Serial [a] where
      series :: Series [a]
    series = [a] -> Series [a]
    forall a. a -> Series a
    cons0 [] Series [a] -> Series [a] -> Series [a]
    forall a. Series a -> Series a -> Series a
    \/ (a -> [a] -> [a]) -> Series [a]
    forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
    cons2 (:)

    instance (Serial a, Serial b) => Serial (a, b) where
      series :: Series (a, b)
    series = (a -> b -> (a, b)) -> Series (a, b)
    forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
    cons2 (,) Series (a, b) -> (Int -> Int) -> Series (a, b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
      series :: Series (a, b, c)
    series = (a -> b -> c -> (a, b, c)) -> Series (a, b, c)
    forall a b c d.
    (Serial a, Serial b, Serial c) =>
    (a -> b -> c -> d) -> Series d
    cons3 (,,) Series (a, b, c) -> (Int -> Int) -> Series (a, b, c)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    instance (Serial a, Serial b, Serial c, Serial d) =>
        Serial (a, b, c, d) where
      series :: Series (a, b, c, d)
    series = (a -> b -> c -> d -> (a, b, c, d)) -> Series (a, b, c, d)
    forall a b c d e.
    (Serial a, Serial b, Serial c, Serial d) =>
    (a -> b -> c -> d -> e) -> Series e
    cons4 (,,,) Series (a, b, c, d) -> (Int -> Int) -> Series (a, b, c, d)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
        Serial (a, b, c, d, e) where
      series :: Series (a, b, c, d, e)
    series = (a -> b -> c -> d -> e -> (a, b, c, d, e))
    -> Series (a, b, c, d, e)
    forall a b c d e f.
    (Serial a, Serial b, Serial c, Serial d, Serial e) =>
    (a -> b -> c -> d -> e -> f) -> Series f
    cons5 (,,,,) Series (a, b, c, d, e) -> (Int -> Int) -> Series (a, b, c, d, e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)

    instance Serial Int where
      series :: Series Int
    series Int
    d = Pos -> Cons Int
    forall a. [a] -> Cons a
    drawnFrom [-Int
    d..Int
    d]

    instance Serial Integer where
      series :: Series Integer
    series Int
    d = [Integer] -> Cons Integer
    forall a. [a] -> Cons a
    drawnFrom ((Int -> Integer) -> Pos -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger [-Int
    d..Int
    d])

    instance Serial Char where
      series :: Series Char
    series Int
    d = [Char] -> Cons Char
    forall a. [a] -> Cons a
    drawnFrom (Int -> [Char] -> [Char]
    forall a. Int -> [a] -> [a]
    take (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) [Char
    'a'..])

    instance Serial Float where
      series :: Series Float
    series Int
    d = [Float] -> Cons Float
    forall a. [a] -> Cons a
    drawnFrom (Int -> [Float]
    forall a. RealFloat a => Int -> [a]
    floats Int
    d)

    instance Serial Double where
      series :: Series Double
    series Int
    d = [Double] -> Cons Double
    forall a. [a] -> Cons a
    drawnFrom (Int -> [Double]
    forall a. RealFloat a => Int -> [a]
    floats Int
    d)

    floats :: RealFloat a => Int -> [a]
    floats :: forall a. RealFloat a => Int -> [a]
    floats Int
    d = [ Integer -> Int -> a
    forall a. RealFloat a => Integer -> Int -> a
    encodeFloat Integer
    sig Int
    exp
               | Integer
    sig <- (Int -> Integer) -> Pos -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger [-Int
    d..Int
    d]
               , Int
    exp <- [-Int
    d..Int
    d]
               , Integer -> Bool
    forall a. Integral a => a -> Bool
    odd Integer
    sig Bool -> Bool -> Bool
    || Integer
    sig Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 Bool -> Bool -> Bool
    && Int
    exp Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0
               ]

    -- Term refinement

    refine :: Term -> Pos -> [Term]
    refine :: Term -> Pos -> [Term]
    refine (Var Pos
    p (SumOfProd [[Type]]
    ss)) [] = Pos -> [[Type]] -> [Term]
    new Pos
    p [[Type]]
    ss
    refine (Ctr Int
    c [Term]
    xs) Pos
    p = ([Term] -> Term) -> [[Term]] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> [Term] -> Term
    Ctr Int
    c) ([Term] -> Pos -> [[Term]]
    refineList [Term]
    xs Pos
    p)

    refineList :: [Term] -> Pos -> [[Term]]
    refineList :: [Term] -> Pos -> [[Term]]
    refineList [Term]
    xs (Int
    i:Pos
    is) = [[Term]
    ls [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ Term
    yTerm -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[Term]
    rs | Term
    y <- Term -> Pos -> [Term]
    refine Term
    x Pos
    is]
      where ([Term]
    ls, Term
    x:[Term]
    rs) = Int -> [Term] -> ([Term], [Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i [Term]
    xs

    new :: Pos -> [[Type]] -> [Term]
    new :: Pos -> [[Type]] -> [Term]
    new Pos
    p [[Type]]
    ps = [ Int -> [Term] -> Term
    Ctr Int
    c ((Int -> Type -> Term) -> Pos -> [Type] -> [Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\Int
    i Type
    t -> Pos -> Type -> Term
    Var (Pos
    pPos -> Pos -> Pos
    forall a. [a] -> [a] -> [a]
    ++[Int
    i]) Type
    t) [Int
    0..] [Type]
    ts)
               | (Int
    c, [Type]
    ts) <- Pos -> [[Type]] -> [(Int, [Type])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] [[Type]]
    ps ]

    -- Find total instantiations of a partial value

    total :: Term -> [Term]
    total :: Term -> [Term]
    total Term
    val = Term -> [Term]
    tot Term
    val
      where
        tot :: Term -> [Term]
    tot (Ctr Int
    c [Term]
    xs) = [Int -> [Term] -> Term
    Ctr Int
    c [Term]
    ys | [Term]
    ys <- (Term -> [Term]) -> [Term] -> [[Term]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Term -> [Term]
    tot [Term]
    xs]
        tot (Var Pos
    p (SumOfProd [[Type]]
    ss)) = [Term
    y | Term
    x <- Pos -> [[Type]] -> [Term]
    new Pos
    p [[Type]]
    ss, Term
    y <- Term -> [Term]
    tot Term
    x]

    -- Answers

    answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
    answer :: forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
    answer a
    a a -> IO b
    known Pos -> IO b
    unknown =
      do res <- IO a -> IO (Either ErrorCall a)
    forall e a. Exception e => IO a -> IO (Either e a)
    try (a -> IO a
    forall a. a -> IO a
    evaluate a
    a)
         case res of
           Right a
    b -> a -> IO b
    known a
    b
           Left (ErrorCall (Char
    '\0':[Char]
    p)) -> Pos -> IO b
    unknown ((Char -> Int) -> [Char] -> Pos
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Int
    forall a. Enum a => a -> Int
    fromEnum [Char]
    p)
           Left ErrorCall
    e -> ErrorCall -> IO b
    forall a e. (HasCallStack, Exception e) => e -> a
    throw ErrorCall
    e

    -- Refute

    refute :: Result -> IO Int
    refute :: Result -> IO Int
    refute Result
    r = [Term] -> IO Int
    ref (Result -> [Term]
    args Result
    r)
      where
        ref :: [Term] -> IO Int
    ref [Term]
    xs = Property -> (Bool -> IO Int) -> (Pos -> IO Int) -> IO Int
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval (Result -> [Term] -> Property
    apply Result
    r [Term]
    xs) Bool -> IO Int
    forall {a}. Num a => Bool -> IO a
    known Pos -> IO Int
    unknown
          where
            known :: Bool -> IO a
    known Bool
    True = a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    1
            known Bool
    False = IO a
    forall {b}. IO b
    report
            unknown :: Pos -> IO Int
    unknown Pos
    p = ([Term] -> IO Int) -> Int -> [[Term]] -> IO Int
    forall a. (a -> IO Int) -> Int -> [a] -> IO Int
    sumMapM [Term] -> IO Int
    ref Int
    1 ([Term] -> Pos -> [[Term]]
    refineList [Term]
    xs Pos
    p)

            report :: IO b
    report =
              do [Char] -> IO ()
    putStrLn [Char]
    "Counter example found:"
                 ([Char] -> IO ()) -> [[Char]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [Char] -> IO ()
    putStrLn ([[Char]] -> IO ()) -> [[Char]] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ((Term -> [Char]) -> Term -> [Char])
    -> [Term -> [Char]] -> [Term] -> [[Char]]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Term -> [Char]) -> Term -> [Char]
    forall a b. (a -> b) -> a -> b
    ($) (Result -> [Term -> [Char]]
    showArgs Result
    r)
                                ([Term] -> [[Char]]) -> [Term] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [[Term]] -> [Term]
    forall a. HasCallStack => [a] -> a
    head [[Term]
    ys | [Term]
    ys <- (Term -> [Term]) -> [Term] -> [[Term]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Term -> [Term]
    total [Term]
    xs]
                 ExitCode -> IO b
    forall a. ExitCode -> IO a
    exitWith ExitCode
    ExitSuccess

    sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
    sumMapM :: forall a. (a -> IO Int) -> Int -> [a] -> IO Int
    sumMapM a -> IO Int
    f Int
    n [] = Int -> IO Int
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    n
    sumMapM a -> IO Int
    f Int
    n (a
    a:[a]
    as) = Int -> IO Int -> IO Int
    forall a b. a -> b -> b
    seq Int
    n (do m <- a -> IO Int
    f a
    a ; sumMapM f (n+m) as)

    -- Properties with parallel conjunction (Lindblad TFP'07)

    data Property =
        Bool Bool
      | Neg Property
      | And Property Property
      | ParAnd Property Property
      | Eq Property Property

    eval :: Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval :: forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p Bool -> IO a
    k Pos -> IO a
    u = Property -> (Property -> IO a) -> (Pos -> IO a) -> IO a
    forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
    answer Property
    p (\Property
    p -> Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval' Property
    p Bool -> IO a
    k Pos -> IO a
    u) Pos -> IO a
    u

    eval' :: Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    eval' (Bool Bool
    b) Bool -> IO b
    k Pos -> IO b
    u = Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
    answer Bool
    b Bool -> IO b
    k Pos -> IO b
    u
    eval' (Neg Property
    p) Bool -> IO b
    k Pos -> IO b
    u = Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (Bool -> IO b
    k (Bool -> IO b) -> (Bool -> Bool) -> Bool -> IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not) Pos -> IO b
    u
    eval' (And Property
    p Property
    q) Bool -> IO b
    k Pos -> IO b
    u = Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (\Bool
    b-> if Bool
    b then Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q Bool -> IO b
    k Pos -> IO b
    u else Bool -> IO b
    k Bool
    b) Pos -> IO b
    u
    eval' (Eq Property
    p Property
    q) Bool -> IO b
    k Pos -> IO b
    u = Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (\Bool
    b-> if Bool
    b then Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q Bool -> IO b
    k Pos -> IO b
    u else Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval (Property -> Property
    Neg Property
    q) Bool -> IO b
    k Pos -> IO b
    u) Pos -> IO b
    u
    eval' (ParAnd Property
    p Property
    q) Bool -> IO b
    k Pos -> IO b
    u = Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (\Bool
    b-> if Bool
    b then Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q Bool -> IO b
    k Pos -> IO b
    u else Bool -> IO b
    k Bool
    b) Pos -> IO b
    unknown
      where
        unknown :: Pos -> IO b
    unknown Pos
    pos = Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q (\Bool
    b-> if Bool
    b then Pos -> IO b
    u Pos
    pos else Bool -> IO b
    k Bool
    b) (\Pos
    _-> Pos -> IO b
    u Pos
    pos)

    lift :: Bool -> Property
    lift :: Bool -> Property
    lift Bool
    b = Bool -> Property
    Bool Bool
    b

    neg :: Property -> Property
    neg :: Property -> Property
    neg Property
    p = Property -> Property
    Neg Property
    p

    (*&*), (*|*), (*=>*), (*=*) :: Property -> Property -> Property
    Property
    p *&* :: Property -> Property -> Property
    *&* Property
    q = Property -> Property -> Property
    ParAnd Property
    p Property
    q
    Property
    p *|* :: Property -> Property -> Property
    *|* Property
    q = Property -> Property
    neg (Property -> Property
    neg Property
    p Property -> Property -> Property
    *&* Property -> Property
    neg Property
    q)
    Property
    p *=>* :: Property -> Property -> Property
    *=>* Property
    q = Property -> Property
    neg (Property
    p Property -> Property -> Property
    *&* Property -> Property
    neg Property
    q)
    Property
    p *=* :: Property -> Property -> Property
    *=* Property
    q = Property -> Property -> Property
    Eq Property
    p Property
    q

    -- Boolean implication

    (==>) :: Bool -> Bool -> Bool
    Bool
    False ==> :: Bool -> Bool -> Bool
    ==> Bool
    _ = Bool
    True
    Bool
    True ==> Bool
    x = Bool
    x

    -- Testable

    data Result =
      Result { Result -> [Term]
    args     :: [Term]
             , Result -> [Term -> [Char]]
    showArgs :: [Term -> String]
             , Result -> [Term] -> Property
    apply    :: [Term] -> Property
             }

    data P = P (Int -> Int -> Result)

    run :: Testable a => ([Term] -> a) -> Int -> Int -> Result
    run :: forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
    run [Term] -> a
    a = Int -> Int -> Result
    f where P Int -> Int -> Result
    f = ([Term] -> a) -> P
    forall a. Testable a => ([Term] -> a) -> P
    property [Term] -> a
    a

    class Testable a where
      property :: ([Term] -> a) -> P

    instance Testable Bool where
      property :: ([Term] -> Bool) -> P
    property [Term] -> Bool
    apply = (Int -> Int -> Result) -> P
    P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
    forall a b. (a -> b) -> a -> b
    $ \Int
    n Int
    d -> [Term] -> [Term -> [Char]] -> ([Term] -> Property) -> Result
    Result [] [] (Bool -> Property
    Bool (Bool -> Property) -> ([Term] -> Bool) -> [Term] -> Property
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> Bool
    apply ([Term] -> Bool) -> ([Term] -> [Term]) -> [Term] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> [Term]
    forall a. [a] -> [a]
    reverse)

    instance Testable Property where
      property :: ([Term] -> Property) -> P
    property [Term] -> Property
    apply = (Int -> Int -> Result) -> P
    P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
    forall a b. (a -> b) -> a -> b
    $ \Int
    n Int
    d -> [Term] -> [Term -> [Char]] -> ([Term] -> Property) -> Result
    Result [] [] ([Term] -> Property
    apply ([Term] -> Property) -> ([Term] -> [Term]) -> [Term] -> Property
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> [Term]
    forall a. [a] -> [a]
    reverse)

    instance (Show a, Serial a, Testable b) => Testable (a -> b) where
      property :: ([Term] -> a -> b) -> P
    property [Term] -> a -> b
    f = (Int -> Int -> Result) -> P
    P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
    forall a b. (a -> b) -> a -> b
    $ \Int
    n Int
    d ->
        let C Type
    t [[Term] -> a]
    c = Series a
    forall a. Serial a => Series a
    series Int
    d
            c' :: Term -> a
    c' = [[Term] -> a] -> Term -> a
    forall a. [[Term] -> a] -> Term -> a
    conv [[Term] -> a]
    c
            r :: Result
    r = ([Term] -> b) -> Int -> Int -> Result
    forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
    run (\(Term
    x:[Term]
    xs) -> [Term] -> a -> b
    f [Term]
    xs (Term -> a
    c' Term
    x)) (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Int
    d
        in  Result
    r { args = Var [n] t : args r, showArgs = (show . c') : showArgs r }

    -- Top-level interface

    depthCheck :: Testable a => Int -> a -> IO ()
    depthCheck :: forall a. Testable a => Int -> a -> IO ()
    depthCheck Int
    d a
    p =
      do n <- Result -> IO Int
    refute (Result -> IO Int) -> Result -> IO Int
    forall a b. (a -> b) -> a -> b
    $ ([Term] -> a) -> Int -> Int -> Result
    forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
    run (a -> [Term] -> a
    forall a b. a -> b -> a
    const a
    p) Int
    0 Int
    d
         putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d

    smallCheck :: Testable a => Int -> a -> IO ()
    smallCheck :: forall a. Testable a => Int -> a -> IO ()
    smallCheck Int
    d a
    p = (Int -> IO ()) -> Pos -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Int -> a -> IO ()
    forall a. Testable a => Int -> a -> IO ()
    `depthCheck` a
    p) [Int
    0..Int
    d]

    test :: Testable a => a -> IO ()
    test :: forall a. Testable a => a -> IO ()
    test a
    p = (Int -> IO ()) -> Pos -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Int -> a -> IO ()
    forall a. Testable a => Int -> a -> IO ()
    `depthCheck` a
    p) [Int
    0..]