    {-# LANGUAGE ScopedTypeVariables #-}

    module Hedgehog.Classes.Ord (ordLaws) where

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'Ord' laws:
    --
    -- [__Antisymmetry__]: @x '<=' y '&&' y '<=' x@ ≡ @x '==' y@
    -- [__Transitivity__]: @x '<=' y '&&' y '<=' z@ ≡ @x '<=' z@
    -- [__Reflexivity__]: @x '<=' x@ ≡ @'True'@
    -- [__Totality__]: @x '<=' y '||' y '<=' x@ ≡ @'True'@
    ordLaws :: forall a. (Ord a, Show a) => Gen a -> Laws
    ordLaws :: forall a. (Ord a, Show a) => Gen a -> Laws
    ordLaws Gen a
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Ord"
      [ (String
    "Antisymmetry", Gen a -> Property
    forall a. (Ord a, Show a) => Gen a -> Property
    ordAntisymmetric Gen a
    gen)
      , (String
    "Transitivity", Gen a -> Property
    forall a. (Ord a, Show a) => Gen a -> Property
    ordTransitive Gen a
    gen)
      , (String
    "Reflexivity", Gen a -> Property
    forall a. (Ord a, Show a) => Gen a -> Property
    ordReflexive Gen a
    gen)
      , (String
    "Totality", Gen a -> Property
    forall a. (Ord a, Show a) => Gen a -> Property
    ordTotal Gen a
    gen)
      ]

    ordAntisymmetric :: forall a. (Ord a, Show a) => Gen a -> Property
    ordAntisymmetric :: forall a. (Ord a, Show a) => Gen a -> Property
    ordAntisymmetric 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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      let lhs = (a
    a a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    b) Bool -> Bool -> Bool
    && (a
    b a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    a)
      let rhs = a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    b
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Antisymmetry", lawContextTcName :: String
    lawContextTcName = String
    "Ord"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "x <= y && y <= x" String -> String -> String
    `congruency` String
    "x == y"
            , lawContextReduced :: String
    lawContextReduced = Bool -> Bool -> String
    forall a. Show a => a -> a -> String
    reduced Bool
    lhs Bool
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showA :: String
    showA = a -> String
    forall a. Show a => a -> String
    show a
    a; showB :: String
    showB = a -> String
    forall a. Show a => a -> String
    show a
    b;
                in [String] -> String
    lawWhere
                  [ String
    "x <= y && y <= x" String -> String -> String
    `congruency` String
    "x == y, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  , String
    "y = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showB
                  ]
            }
      heqCtx lhs rhs ctx

    ordTransitive :: forall a. (Ord a, Show a) => Gen a -> Property
    ordTransitive :: forall a. (Ord a, Show a) => Gen a -> Property
    ordTransitive 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
      x <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      y <- forAll gen
      z <- forAll gen
      let lhs = a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    y Bool -> Bool -> Bool
    && a
    y a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    z
      let rhs = a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    z
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Transitivity", lawContextTcName :: String
    lawContextTcName = String
    "Ord"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "x <= y && y <= z" String -> String -> String
    `implies` String
    "x <= z"
            , lawContextReduced :: String
    lawContextReduced = Bool -> Bool -> String
    forall a. Show a => a -> a -> String
    reduced Bool
    lhs Bool
    rhs
            , 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; showZ :: String
    showZ = a -> String
    forall a. Show a => a -> String
    show a
    z;
                in [String] -> String
    lawWhere
                  [ String
    "x <= y && y <= z" String -> String -> String
    `implies` String
    "x <= z, 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
                  , String
    "z = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showZ
                  ]
            }
      case (compare x y, compare y z) of
        (Ordering
    LT,Ordering
    LT) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, Ord a, Show a, HasCallStack) =>
    a -> a -> Context -> m ()
    hLessThanCtx a
    x a
    z Context
    ctx
        (Ordering
    LT,Ordering
    EQ) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, Ord a, Show a, HasCallStack) =>
    a -> a -> Context -> m ()
    hLessThanCtx a
    x a
    z Context
    ctx
        (Ordering
    LT,Ordering
    GT) -> PropertyT IO ()
    forall (m :: * -> *). MonadTest m => m ()
    success
        (Ordering
    EQ,Ordering
    LT) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, Ord a, Show a, HasCallStack) =>
    a -> a -> Context -> m ()
    hLessThanCtx a
    x a
    z Context
    ctx
        (Ordering
    EQ,Ordering
    EQ) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx a
    x a
    z Context
    ctx
        (Ordering
    EQ,Ordering
    GT) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, Ord a, Show a, HasCallStack) =>
    a -> a -> Context -> m ()
    hGreaterThanCtx a
    x a
    z Context
    ctx
        (Ordering
    GT,Ordering
    LT) -> PropertyT IO ()
    forall (m :: * -> *). MonadTest m => m ()
    success
        (Ordering
    GT,Ordering
    EQ) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, Ord a, Show a, HasCallStack) =>
    a -> a -> Context -> m ()
    hGreaterThanCtx a
    x a
    z Context
    ctx
        (Ordering
    GT,Ordering
    GT) -> a -> a -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, Ord a, Show a, HasCallStack) =>
    a -> a -> Context -> m ()
    hGreaterThanCtx a
    x a
    z Context
    ctx

    ordTotal :: forall a. (Ord a, Show a) => Gen a -> Property
    ordTotal :: forall a. (Ord a, Show a) => Gen a -> Property
    ordTotal 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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      let lhs = (a
    a a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    b) Bool -> Bool -> Bool
    || (a
    b a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    a)
      let rhs = Bool
    True
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Totality", lawContextTcName :: String
    lawContextTcName = String
    "Ord"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "x <= y || y <= x" String -> String -> String
    `congruency` String
    "True"
            , lawContextReduced :: String
    lawContextReduced = Bool -> Bool -> String
    forall a. Show a => a -> a -> String
    reduced Bool
    lhs Bool
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showA :: String
    showA = a -> String
    forall a. Show a => a -> String
    show a
    a; showB :: String
    showB = a -> String
    forall a. Show a => a -> String
    show a
    b;
                in [String] -> String
    lawWhere
                  [ String
    "(x <= y) || (y <= x)" String -> String -> String
    `congruency` String
    "True, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  , String
    "y = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showB
                  ]
            }
      heqCtx lhs rhs ctx

    ordReflexive :: forall a. (Ord a, Show a) => Gen a -> Property
    ordReflexive :: forall a. (Ord a, Show a) => Gen a -> Property
    ordReflexive 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
      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
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    x
      let rhs = Bool
    True
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Reflexivity", lawContextTcName :: String
    lawContextTcName = String
    "Ord"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "x <= x" String -> String -> String
    `congruency` String
    "True"
            , lawContextReduced :: String
    lawContextReduced = Bool -> Bool -> String
    forall a. Show a => a -> a -> String
    reduced Bool
    lhs Bool
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showX :: String
    showX = a -> String
    forall a. Show a => a -> String
    show a
    x;
                in [String] -> String
    lawWhere
                  [ String
    "x <= x" String -> String -> String
    `congruency` String
    "True, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  ]
            }
      heqCtx lhs rhs ctx