    {-# LANGUAGE ScopedTypeVariables #-}

    module Hedgehog.Classes.Integral (integralLaws) where

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'Integral' laws:
    --
    -- [__Quotient Remainder__]: @'quot' x y '*' y '+' ('rem' x y)@ ≡ @x@
    -- [__Division Modulus__]: @('div' x y) '*' y '+' ('mod' x y)@ ≡ @x@
    -- [__Integer Roundtrip__]: @'fromInteger' '.' 'toInteger'@ ≡ @'id'@
    integralLaws :: (Integral a, Show a) => Gen a -> Laws
    integralLaws :: forall a. (Integral a, Show a) => Gen a -> Laws
    integralLaws Gen a
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Integral"
      [ (String
    "Quotient Remainder", Gen a -> Property
    forall a. (Integral a, Show a) => Gen a -> Property
    integralQuotientRemainder Gen a
    gen)
      , (String
    "Division Modulus", Gen a -> Property
    forall a. (Integral a, Show a) => Gen a -> Property
    integralDivisionModulus Gen a
    gen)
      , (String
    "Integer Roundtrip", Gen a -> Property
    forall a. (Integral a, Show a) => Gen a -> Property
    integralIntegerRoundtrip Gen a
    gen)
      ]

    integralQuotientRemainder :: forall a. (Integral a, Show a) => Gen a -> Property
    integralQuotientRemainder :: forall a. (Integral a, Show a) => Gen a -> Property
    integralQuotientRemainder Gen a
    gen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a
    x <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      a
    y <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      let lhs :: a
    lhs = (a -> a -> a
    forall a. Integral a => a -> a -> a
    quot a
    x a
    y) a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    y a -> a -> a
    forall a. Num a => a -> a -> a
    + (a -> a -> a
    forall a. Integral a => a -> a -> a
    rem a
    x a
    y)
      let rhs :: a
    rhs = a
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Quotient Remainder", lawContextTcName :: String
    lawContextTcName = String
    "Integral"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "quot x y * y + (rem x y)" String -> String -> String
    `congruency` String
    "x"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showX :: String
    showX = a -> String
    forall a. Show a => a -> String
    show a
    x; showY :: String
    showY = a -> String
    forall a. Show a => a -> String
    show a
    y;
                in [String] -> String
    lawWhere
                  [ String
    "quot x y * y + (rem x y)" String -> String -> String
    `congruency` String
    "x, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  , String
    "y = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showY
                  ]
            , lawContextReduced :: String
    lawContextReduced = a -> a -> String
    forall a. Show a => a -> a -> String
    reduced a
    lhs a
    rhs
            }
      a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx a
    lhs a
    rhs Context
    ctx

    integralDivisionModulus :: forall a. (Integral a, Show a) => Gen a -> Property
    integralDivisionModulus :: forall a. (Integral a, Show a) => Gen a -> Property
    integralDivisionModulus Gen a
    gen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a
    x <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      a
    y <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      let lhs :: a
    lhs = (a -> a -> a
    forall a. Integral a => a -> a -> a
    div a
    x a
    y) a -> a -> a
    forall a. Num a => a -> a -> a
    * a
    y a -> a -> a
    forall a. Num a => a -> a -> a
    + (a -> a -> a
    forall a. Integral a => a -> a -> a
    mod a
    x a
    y)
      let rhs :: a
    rhs = a
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Division Modulus", lawContextTcName :: String
    lawContextTcName = String
    "Integral"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "(div x y) * y + (mod x y)" String -> String -> String
    `congruency` String
    "x"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showX :: String
    showX = a -> String
    forall a. Show a => a -> String
    show a
    x; showY :: String
    showY = a -> String
    forall a. Show a => a -> String
    show a
    y;
                in [String] -> String
    lawWhere
                  [ String
    "(div x y) * y + (mod x y)" String -> String -> String
    `congruency` String
    "x, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  , String
    "y = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showY
                  ]
            , lawContextReduced :: String
    lawContextReduced = a -> a -> String
    forall a. Show a => a -> a -> String
    reduced a
    lhs a
    rhs
            }
      a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx a
    lhs a
    rhs Context
    ctx

    integralIntegerRoundtrip :: forall a. (Integral a, Show a) => Gen a -> Property
    integralIntegerRoundtrip :: forall a. (Integral a, Show a) => Gen a -> Property
    integralIntegerRoundtrip Gen a
    gen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a
    x <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      let lhs :: a
    lhs = Integer -> a
    forall a. Num a => Integer -> a
    fromInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    x)
      let rhs :: a
    rhs = a
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Integer Roundtrip", lawContextTcName :: String
    lawContextTcName = String
    "Integral"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "fromInteger . toInteger" String -> String -> String
    `congruency` String
    "id"
            , lawContextTcProp :: String
    lawContextTcProp =
                let showX :: String
    showX = a -> String
    forall a. Show a => a -> String
    show a
    x;
                in [String] -> String
    lawWhere
                  [ String
    "fromInteger . toInteger $ x" String -> String -> String
    `congruency` String
    "id x, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  ]
            , lawContextReduced :: String
    lawContextReduced = a -> a -> String
    forall a. Show a => a -> a -> String
    reduced a
    lhs a
    rhs
            }
      a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx a
    lhs a
    rhs Context
    ctx