{- HLINT ignore "Avoid lambda" -}
{- HLINT ignore "Redundant bracket" -}
{- HLINT ignore "Use camelCase" -}
{- HLINT ignore "Use const" -}
{- HLINT ignore "Use null" -}

-- |
-- Copyright: © 2022–2024 Jonathan Knowles
-- License: Apache-2.0
--
-- This module provides 'Laws' definitions for classes exported by
-- "Data.Semigroup.Factorial".
--
module Test.QuickCheck.Classes.Semigroup.Factorial
    ( factorialLaws
    , stableFactorialLaws
    )
    where

import Data.Bool
    ( Bool (True) )
import Data.Eq
    ( Eq ((==)) )
import Data.Foldable
    ( all )
import Data.Function
    ( ($), (&) )
import Data.Functor
    ( Functor (fmap), (<$>) )
import Data.List.NonEmpty
    ( nonEmpty )
import Data.Maybe
    ( maybe )
import Data.Ord
    ( Ord ((>=)) )
import Data.Proxy
    ( Proxy )
import Data.Semigroup
    ( Semigroup (sconcat, (<>)) )
import Data.Semigroup.Factorial
    ( Factorial
    , StableFactorial
    , factors
    , foldl
    , foldl'
    , foldr
    , length
    , primePrefix
    , primeSuffix
    , reverse
    )
import Data.String
    ( String )
import Internal
    ( cover, makeLaw1, makeLaw2, makeProperty, report )
import Test.QuickCheck
    ( Arbitrary, Gen, Property, elements, forAllBlind )
import Test.QuickCheck.Classes
    ( Laws (Laws) )
import Text.Show
    ( Show )

import qualified Data.List as L

--------------------------------------------------------------------------------
-- Factorial
--------------------------------------------------------------------------------

-- | 'Laws' for instances of 'Factorial'.
--
-- Includes the following laws:
--
-- @
-- 'length' a '==' "Data.List".'Data.List.length' ('factors' a)
-- @
--
-- @
-- 'maybe' a 'sconcat' ('nonEmpty'   \ \ \     \ $ 'factors' a) '==' \       \ a
-- 'maybe' a 'sconcat' ('nonEmpty' $ 'L.reverse' $ 'factors' a) '==' 'reverse' a
-- @
--
-- @
-- 'all' (\\f -> 'factors' f '==' [f]) ('factors' a)
-- @
--
-- @
-- 'primePrefix' a '==' 'foldr' (\\x _ -> x) a a
-- 'primeSuffix' a '==' 'foldl' (\\_ x -> x) a a
-- @
--
-- @
-- 'foldl'  f x a '==' "Data.List".'Data.List.foldl'  f x ('factors' a)
-- 'foldl'' f x a '==' "Data.List".'Data.List.foldl'' f x ('factors' a)
-- 'foldr'  f x a '==' "Data.List".'Data.List.foldr'  f x ('factors' a)
-- @
--
-- Note that the following superclass laws are __not__ included:
--
-- * 'Test.QuickCheck.Classes.semigroupLaws'
--
factorialLaws
    :: forall a. (Arbitrary a, Show a, Eq a, Factorial a)
    => Proxy a
    -> Laws
factorialLaws :: forall a.
(Arbitrary a, Show a, Eq a, Factorial a) =>
Proxy a -> Laws
factorialLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"Factorial"
    [ forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_coverage"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_coverage)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_length_factors"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_length_factors)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_maybe_sconcat_nonEmpty_factors"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_maybe_sconcat_nonEmpty_factors)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_maybe_sconcat_nonEmpty_factors_reverse"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_maybe_sconcat_nonEmpty_factors_reverse)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_all_factors_prime"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_all_factors_prime)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_primePrefix_foldr"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_primePrefix_foldr)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"factorialLaw_primeSuffix_foldl"
        (a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_primeSuffix_foldl)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"factorialLaw_factors_foldl"
        (a -> a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldl)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"factorialLaw_factors_foldl'"
        (a -> a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldl')
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"factorialLaw_factors_foldr"
        (a -> a -> Property
forall a. (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldr)
    ]

factorialLaw_coverage
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_coverage :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_coverage a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"True"
        (Bool
True)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"length a == 0"
        (a -> Int
forall m. Factorial m => m -> Int
length a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"length a == 1"
        (a -> Int
forall m. Factorial m => m -> Int
length a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Bool -> Property -> Property
forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"length a >= 2"
        (a -> Int
forall m. Factorial m => m -> Int
length a
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2)

factorialLaw_length_factors
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_length_factors :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_length_factors a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"length a == L.length (factors a)"
        (a -> Int
forall m. Factorial m => m -> Int
length a
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Int -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"length a"
        (a -> Int
forall m. Factorial m => m -> Int
length a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Int -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"L.length (factors a)"
        ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))

factorialLaw_maybe_sconcat_nonEmpty_factors
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_maybe_sconcat_nonEmpty_factors :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_maybe_sconcat_nonEmpty_factors a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"maybe a sconcat (nonEmpty (factors a)) == a"
        (a -> (NonEmpty a -> a) -> Maybe (NonEmpty a) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
a NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
sconcat ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe (NonEmpty a) -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"nonEmpty (factors a)"
        ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"fmap sconcat (nonEmpty (factors a))"
        ((NonEmpty a -> a) -> Maybe (NonEmpty a) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
sconcat ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)))

factorialLaw_maybe_sconcat_nonEmpty_factors_reverse
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_maybe_sconcat_nonEmpty_factors_reverse :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_maybe_sconcat_nonEmpty_factors_reverse a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"maybe a sconcat (nonEmpty (L.reverse (factors a))) == reverse a"
        (a -> (NonEmpty a -> a) -> Maybe (NonEmpty a) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
a NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
sconcat ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([a] -> [a]
forall a. [a] -> [a]
L.reverse (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall m. Factorial m => m -> m
reverse a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"L.reverse (factors a)"
        ([a] -> [a]
forall a. [a] -> [a]
L.reverse (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> Maybe (NonEmpty a) -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"nonEmpty (L.reverse (factors a))"
        ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([a] -> [a]
forall a. [a] -> [a]
L.reverse (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"maybe a sconcat (nonEmpty (L.reverse (factors a)))"
        (a -> (NonEmpty a -> a) -> Maybe (NonEmpty a) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
a NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
sconcat ([a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([a] -> [a]
forall a. [a] -> [a]
L.reverse (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"reverse a"
        (a -> a
forall m. Factorial m => m -> m
reverse a
a)

factorialLaw_all_factors_prime
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_all_factors_prime :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_all_factors_prime a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"all (λf -> factors f == [f]) (factors a)"
        ((a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\a
f -> a -> [a]
forall m. Factorial m => m -> [m]
factors a
f [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a
f]) (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [[a]] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors <$> factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors (a -> [a]) -> [a] -> [[a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)

factorialLaw_primePrefix_foldr
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_primePrefix_foldr :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_primePrefix_foldr a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"primePrefix a == foldr (λx _ -> x) a a"
        (a -> a
forall m. Factorial m => m -> m
primePrefix a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (m -> a -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldr (\a
x a
_ -> a
x) a
a a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"primePrefix a"
        (a -> a
forall m. Factorial m => m -> m
primePrefix a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"foldr (λx _ -> x) a a"
        ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (m -> a -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldr (\a
x a
_ -> a
x) a
a a
a)

factorialLaw_primeSuffix_foldl
    :: (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_primeSuffix_foldl :: forall a. (Eq a, Show a, Factorial a) => a -> Property
factorialLaw_primeSuffix_foldl a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"primeSuffix a == foldl (λ_ x -> x) a a"
        (a -> a
forall m. Factorial m => m -> m
primeSuffix a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (a -> m -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldl (\a
_ a
x -> a
x) a
a a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"primeSuffix a"
        (a -> a
forall m. Factorial m => m -> m
primeSuffix a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"foldl (λ_ x -> x) a a"
        ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (a -> m -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldl (\a
_ a
x -> a
x) a
a a
a)

factorialLaw_factors_foldl
    :: (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldl :: forall a. (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldl a
x a
a =
    Gen (String, a -> a -> a)
-> ((String, a -> a -> a) -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen (String, a -> a -> a)
forall a. Semigroup a => Gen (String, a -> a -> a)
genAccumulatorFn (((String, a -> a -> a) -> Property) -> Property)
-> ((String, a -> a -> a) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(String
fDefinition, a -> a -> a
f) ->
        String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
            String
"foldl f x a == L.foldl f x (factors a)"
            ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (a -> m -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldl a -> a -> a
f a
x a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a -> a) -> a -> [a] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl a -> a -> a
f a
x (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> String -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"f"
            (String
fDefinition)
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"foldl f x a"
            ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (a -> m -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldl a -> a -> a
f a
x a
a)
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"L.foldl f x (factors a)"
            ((a -> a -> a) -> a -> [a] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl a -> a -> a
f a
x (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))

factorialLaw_factors_foldl'
    :: (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldl' :: forall a. (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldl' a
x a
a =
    Gen (String, a -> a -> a)
-> ((String, a -> a -> a) -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen (String, a -> a -> a)
forall a. Semigroup a => Gen (String, a -> a -> a)
genAccumulatorFn (((String, a -> a -> a) -> Property) -> Property)
-> ((String, a -> a -> a) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(String
fDefinition, a -> a -> a
f) ->
        String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
            String
"foldl' f x a == L.foldl' f x (factors a)"
            ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (a -> m -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldl' a -> a -> a
f a
x a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a -> a) -> a -> [a] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> a -> a
f a
x (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> String -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"f"
            (String
fDefinition)
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"foldl' f x a"
            ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (a -> m -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldl' a -> a -> a
f a
x a
a)
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"L.foldl' f x (factors a)"
            ((a -> a -> a) -> a -> [a] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> a -> a
f a
x (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))

factorialLaw_factors_foldr
    :: (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldr :: forall a. (Eq a, Show a, Factorial a) => a -> a -> Property
factorialLaw_factors_foldr a
x a
a =
    Gen (String, a -> a -> a)
-> ((String, a -> a -> a) -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen (String, a -> a -> a)
forall a. Semigroup a => Gen (String, a -> a -> a)
genAccumulatorFn (((String, a -> a -> a) -> Property) -> Property)
-> ((String, a -> a -> a) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(String
fDefinition, a -> a -> a
f) ->
        String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
            String
"foldr f x a == L.foldr f x (factors a)"
            ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (m -> a -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldr a -> a -> a
f a
x a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr a -> a -> a
f a
x (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> String -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"f"
            (String
fDefinition)
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"foldr f x a"
            ((a -> a -> a) -> a -> a -> a
forall m a. Factorial m => (m -> a -> a) -> a -> m -> a
forall a. (a -> a -> a) -> a -> a -> a
foldr a -> a -> a
f a
x a
a)
        Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
            String
"L.foldr f x (factors a)"
            ((a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr a -> a -> a
f a
x (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))

--------------------------------------------------------------------------------
-- StableFactorial
--------------------------------------------------------------------------------

-- | 'Laws' for instances of 'StableFactorial'.
--
-- Includes the following laws:
--
-- @
-- 'factors' (a '<>' b) '==' 'factors' a '<>' 'factors' b
-- @
--
-- @
-- 'factors' ('reverse' a) '==' "Data.List".'L.reverse' ('factors' a)
-- @
--
-- @
-- 'primePrefix' a '==' 'primeSuffix' ('reverse' a)
-- 'primeSuffix' a '==' 'primePrefix' ('reverse' a)
-- @
--
-- Note that the following superclass laws are __not__ included:
--
-- * 'factorialLaws'
--
stableFactorialLaws
    :: forall a. (Arbitrary a, Show a, Eq a, StableFactorial a)
    => Proxy a
    -> Laws
stableFactorialLaws :: forall a.
(Arbitrary a, Show a, Eq a, StableFactorial a) =>
Proxy a -> Laws
stableFactorialLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"StableFactorial"
    [ forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"stableFactorialLaw_factors_mappend"
        (a -> a -> Property
forall a. (Eq a, Show a, StableFactorial a) => a -> a -> Property
stableFactorialLaw_factors_mappend)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"stableFactorialLaw_factors_reverse"
        (a -> Property
forall a. (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_factors_reverse)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"stableFactorialLaw_primePrefix_primeSuffix_reverse"
        (a -> Property
forall a. (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_primePrefix_primeSuffix_reverse)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"stableFactorialLaw_primeSuffix_primePrefix_reverse"
        (a -> Property
forall a. (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_primeSuffix_primePrefix_reverse)
    ]

stableFactorialLaw_factors_mappend
    :: (Eq a, Show a, StableFactorial a) => a -> a -> Property
stableFactorialLaw_factors_mappend :: forall a. (Eq a, Show a, StableFactorial a) => a -> a -> Property
stableFactorialLaw_factors_mappend a
a a
b =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"factors (a <> b) == factors a <> factors b"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b) [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== a -> [a]
forall m. Factorial m => m -> [m]
factors a
a [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> a -> [a]
forall m. Factorial m => m -> [m]
factors a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> b"
        (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors b"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
b)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors (a <> b)"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a <> factors b"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> a -> [a]
forall m. Factorial m => m -> [m]
factors a
b)

stableFactorialLaw_factors_reverse
    :: (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_factors_reverse :: forall a. (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_factors_reverse a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"factors (reverse a) == L.reverse (factors a)"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors (a -> a
forall m. Factorial m => m -> m
reverse a
a) [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> [a]
forall a. [a] -> [a]
L.reverse (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"reverse a"
        (a -> a
forall m. Factorial m => m -> m
reverse a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors (reverse a)"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors (a -> a
forall m. Factorial m => m -> m
reverse a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"factors a"
        (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> [a] -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"L.reverse (factors a)"
        ([a] -> [a]
forall a. [a] -> [a]
L.reverse (a -> [a]
forall m. Factorial m => m -> [m]
factors a
a))

stableFactorialLaw_primePrefix_primeSuffix_reverse
    :: (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_primePrefix_primeSuffix_reverse :: forall a. (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_primePrefix_primeSuffix_reverse a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"primePrefix a == primeSuffix (reverse a)"
        (a -> a
forall m. Factorial m => m -> m
primePrefix a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall m. Factorial m => m -> m
primeSuffix (a -> a
forall m. Factorial m => m -> m
reverse a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"primePrefix a"
        (a -> a
forall m. Factorial m => m -> m
primePrefix a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"reverse a"
        (a -> a
forall m. Factorial m => m -> m
reverse a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"primeSuffix (reverse a)"
        (a -> a
forall m. Factorial m => m -> m
primeSuffix (a -> a
forall m. Factorial m => m -> m
reverse a
a))

stableFactorialLaw_primeSuffix_primePrefix_reverse
    :: (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_primeSuffix_primePrefix_reverse :: forall a. (Eq a, Show a, StableFactorial a) => a -> Property
stableFactorialLaw_primeSuffix_primePrefix_reverse a
a =
    String -> Bool -> Property
forall t. Testable t => String -> t -> Property
makeProperty
        String
"primeSuffix a == primePrefix (reverse a)"
        (a -> a
forall m. Factorial m => m -> m
primeSuffix a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall m. Factorial m => m -> m
primePrefix (a -> a
forall m. Factorial m => m -> m
reverse a
a))
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"primeSuffix a"
        (a -> a
forall m. Factorial m => m -> m
primeSuffix a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"reverse a"
        (a -> a
forall m. Factorial m => m -> m
reverse a
a)
    Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& String -> a -> Property -> Property
forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"primePrefix (reverse a)"
        (a -> a
forall m. Factorial m => m -> m
primePrefix (a -> a
forall m. Factorial m => m -> m
reverse a
a))

--------------------------------------------------------------------------------
-- Utilities
--------------------------------------------------------------------------------

genAccumulatorFn :: Semigroup a => Gen (String, a -> a -> a)
genAccumulatorFn :: forall a. Semigroup a => Gen (String, a -> a -> a)
genAccumulatorFn = [(String, a -> a -> a)] -> Gen (String, a -> a -> a)
forall a. HasCallStack => [a] -> Gen a
elements
    [ ( String
"λa _ -> a"
      , (\a
a a
_ -> a
a)
      )
    , ( String
"λ_ b -> b"
      , (\a
_ a
b -> a
b)
      )
    , ( String
"λa b -> a <> b"
      , (\a
a a
b -> a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)
      )
    , ( String
"λa b -> b <> a"
      , (\a
a a
b -> a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a)
      )
    ]