    -- | 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 :: a -> Series a
    cons a :: a
    a d :: 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 :: Series a
    empty d :: 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
    (f :: Series (a -> b)
    f >< :: Series (a -> b) -> Series a -> Series b
    >< a :: Series a
    a) d :: 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 ps :: [[Type]]
    ps) cfs :: [[Term] -> a -> b]
    cfs = Series (a -> b)
    f Int
    d
        C ta :: Type
    ta cas :: [[Term] -> a]
    cas = Series a
    a (Int
    dInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1)
        cs :: [[Term] -> b]
    cs = [\(x :: Term
    x:xs :: [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
    > 0 Bool -> Bool -> Bool
    && Type -> Bool
    nonEmpty Type
    ta

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

    (\/) :: Series a -> Series a -> Series a
    (a :: Series a
    a \/ :: Series a -> Series a -> Series a
    \/ b :: Series a
    b) d :: 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 ssa :: [[Type]]
    ssa) ca :: [[Term] -> a]
    ca = Series a
    a Int
    d
        C (SumOfProd ssb :: [[Type]]
    ssb) cb :: [[Term] -> a]
    cb = Series a
    b Int
    d

    conv :: [[Term] -> a] -> Term -> a
    conv :: [[Term] -> a] -> Term -> a
    conv cs :: [[Term] -> a]
    cs (Var p :: Pos
    p _) = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ('\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 cs :: [[Term] -> a]
    cs (Ctr i :: Int
    i xs :: [Term]
    xs) = ([[Term] -> a]
    cs [[Term] -> a] -> Int -> [Term] -> a
    forall a. [a] -> Int -> a
    !! Int
    i) [Term]
    xs

    drawnFrom :: [a] -> Cons a
    drawnFrom :: [a] -> Cons a
    drawnFrom xs :: [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 :: a -> Series a
    cons0 f :: a
    f = a -> Series a
    forall a. a -> Series a
    cons a
    f

    cons1 :: Serial a => (a -> b) -> Series b
    cons1 :: (a -> b) -> Series b
    cons1 f :: 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 :: (a -> b -> c) -> Series c
    cons2 f :: 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 :: (a -> b -> c -> d) -> Series d
    cons3 f :: 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 :: (a -> b -> c -> d -> e) -> Series e
    cons4 f :: 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 :: (a -> b -> c -> d -> e -> f) -> Series f
    cons5 f :: 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
    +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
    +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
    +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
    +1)

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

    instance Serial Integer where
      series :: Series Integer
    series d :: 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 d :: 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
    +1) ['a'..])

    instance Serial Float where
      series :: Series Float
    series d :: 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 d :: 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 :: Int -> [a]
    floats d :: 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
    == 0 Bool -> Bool -> Bool
    && Int
    exp Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
               ]

    -- Term refinement

    refine :: Term -> Pos -> [Term]
    refine :: Term -> Pos -> [Term]
    refine (Var p :: Pos
    p (SumOfProd ss :: [[Type]]
    ss)) [] = Pos -> [[Type]] -> [Term]
    new Pos
    p [[Type]]
    ss
    refine (Ctr c :: Int
    c xs :: [Term]
    xs) p :: 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 xs :: [Term]
    xs (i :: Int
    i:is :: 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 (ls :: [Term]
    ls, x :: Term
    x:rs :: [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 p :: Pos
    p ps :: [[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 (\i :: Int
    i t :: Type
    t -> Pos -> Type -> Term
    Var (Pos
    pPos -> Pos -> Pos
    forall a. [a] -> [a] -> [a]
    ++[Int
    i]) Type
    t) [0..] [Type]
    ts)
               | (c :: Int
    c, ts :: [Type]
    ts) <- Pos -> [[Type]] -> [(Int, [Type])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [0..] [[Type]]
    ps ]

    -- Find total instantiations of a partial value

    total :: Term -> [Term]
    total :: Term -> [Term]
    total val :: Term
    val = Term -> [Term]
    tot Term
    val
      where
        tot :: Term -> [Term]
    tot (Ctr c :: Int
    c xs :: [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)
    mapM Term -> [Term]
    tot [Term]
    xs]
        tot (Var p :: Pos
    p (SumOfProd ss :: [[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 :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
    answer a :: a
    a known :: a -> IO b
    known unknown :: Pos -> IO b
    unknown =
      do Either ErrorCall a
    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 Either ErrorCall a
    res of
           Right b :: a
    b -> a -> IO b
    known a
    b
           Left (ErrorCall ('\0':p :: [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 e :: ErrorCall
    e -> ErrorCall -> IO b
    forall a e. Exception e => e -> a
    throw ErrorCall
    e

    -- Refute

    refute :: Result -> IO Int
    refute :: Result -> IO Int
    refute r :: Result
    r = [Term] -> IO Int
    ref (Result -> [Term]
    args Result
    r)
      where
        ref :: [Term] -> IO Int
    ref xs :: [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 True = a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return 1
            known False = IO a
    forall b. IO b
    report
            unknown :: Pos -> IO Int
    unknown p :: Pos
    p = ([Term] -> IO Int) -> Int -> [[Term]] -> IO Int
    forall a. (a -> IO Int) -> Int -> [a] -> IO Int
    sumMapM [Term] -> IO Int
    ref 1 ([Term] -> Pos -> [[Term]]
    refineList [Term]
    xs Pos
    p)

            report :: IO b
    report =
              do [Char] -> IO ()
    putStrLn "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. [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)
    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 :: (a -> IO Int) -> Int -> [a] -> IO Int
    sumMapM f :: a -> IO Int
    f n :: Int
    n [] = Int -> IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    n
    sumMapM f :: a -> IO Int
    f n :: Int
    n (a :: a
    a:as :: [a]
    as) = Int -> IO Int -> IO Int
    forall a b. a -> b -> b
    seq Int
    n (do Int
    m <- a -> IO Int
    f a
    a ; (a -> IO Int) -> Int -> [a] -> IO Int
    forall a. (a -> IO Int) -> Int -> [a] -> IO Int
    sumMapM a -> IO Int
    f (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    m) [a]
    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 :: Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval p :: Property
    p k :: Bool -> IO a
    k u :: 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 (\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 a) -> (Pos -> IO a) -> IO a
    eval' (Bool b :: Bool
    b) k :: Bool -> IO a
    k u :: Pos -> IO a
    u = Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
    answer Bool
    b Bool -> IO a
    k Pos -> IO a
    u
    eval' (Neg p :: Property
    p) k :: Bool -> IO a
    k u :: Pos -> IO a
    u = 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 (Bool -> IO a) -> (Bool -> Bool) -> Bool -> IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not) Pos -> IO a
    u
    eval' (And p :: Property
    p q :: Property
    q) k :: Bool -> IO a
    k u :: Pos -> IO a
    u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (\b :: Bool
    b-> if Bool
    b then Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q Bool -> IO a
    k Pos -> IO a
    u else Bool -> IO a
    k Bool
    b) Pos -> IO a
    u
    eval' (Eq p :: Property
    p q :: Property
    q) k :: Bool -> IO a
    k u :: Pos -> IO a
    u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (\b :: Bool
    b-> if Bool
    b then Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q Bool -> IO a
    k Pos -> IO a
    u else Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval (Property -> Property
    Neg Property
    q) Bool -> IO a
    k Pos -> IO a
    u) Pos -> IO a
    u
    eval' (ParAnd p :: Property
    p q :: Property
    q) k :: Bool -> IO a
    k u :: Pos -> IO a
    u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    p (\b :: Bool
    b-> if Bool
    b then Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q Bool -> IO a
    k Pos -> IO a
    u else Bool -> IO a
    k Bool
    b) Pos -> IO a
    unknown
      where
        unknown :: Pos -> IO a
    unknown pos :: Pos
    pos = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
    eval Property
    q (\b :: Bool
    b-> if Bool
    b then Pos -> IO a
    u Pos
    pos else Bool -> IO a
    k Bool
    b) (\_-> Pos -> IO a
    u Pos
    pos)

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

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

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

    -- Boolean implication

    (==>) :: Bool -> Bool -> Bool
    False ==> :: Bool -> Bool -> Bool
    ==> _ = Bool
    True
    True ==> x :: 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 :: ([Term] -> a) -> Int -> Int -> Result
    run a :: [Term] -> a
    a = Int -> Int -> Result
    f where P f :: 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 apply :: [Term] -> Bool
    apply = (Int -> Int -> Result) -> P
    P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
    forall a b. (a -> b) -> a -> b
    $ \n :: Int
    n d :: 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 apply :: [Term] -> Property
    apply = (Int -> Int -> Result) -> P
    P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
    forall a b. (a -> b) -> a -> b
    $ \n :: Int
    n d :: 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 f :: [Term] -> a -> b
    f = (Int -> Int -> Result) -> P
    P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
    forall a b. (a -> b) -> a -> b
    $ \n :: Int
    n d :: Int
    d ->
        let C t :: Type
    t c :: [[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 (\(x :: Term
    x:xs :: [Term]
    xs) -> [Term] -> a -> b
    f [Term]
    xs (Term -> a
    c' Term
    x)) (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) Int
    d
        in  Result
    r { args :: [Term]
    args = Pos -> Type -> Term
    Var [Int
    n] Type
    t Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : Result -> [Term]
    args Result
    r, showArgs :: [Term -> [Char]]
    showArgs = (a -> [Char]
    forall a. Show a => a -> [Char]
    show (a -> [Char]) -> (Term -> a) -> Term -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> a
    c') (Term -> [Char]) -> [Term -> [Char]] -> [Term -> [Char]]
    forall a. a -> [a] -> [a]
    : Result -> [Term -> [Char]]
    showArgs Result
    r }

    -- Top-level interface

    depthCheck :: Testable a => Int -> a -> IO ()
    depthCheck :: Int -> a -> IO ()
    depthCheck d :: Int
    d p :: a
    p =
      do Int
    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) 0 Int
    d
         [Char] -> IO ()
    putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "OK, required " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ " tests at depth " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    d

    smallCheck :: Testable a => Int -> a -> IO ()
    smallCheck :: Int -> a -> IO ()
    smallCheck d :: Int
    d p :: 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) [0..Int
    d]

    test :: Testable a => a -> IO ()
    test :: a -> IO ()
    test p :: 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) [0..]