module LawfulConversions.Properties
  ( isSomeProperties,
    isManyProperties,
    isProperties,
  )
where

import LawfulConversions.Algebra
import LawfulConversions.Prelude
import Test.QuickCheck

-- |
-- Properties testing whether an instance satisfies the laws of 'IsSome'.
--
-- The instance is identified via the proxy types that you provide.
--
-- E.g., here's how you can integrate it into an Hspec test-suite:
--
-- > spec = do
-- >   describe "IsSome laws" do
-- >     traverse_
-- >       (uncurry prop)
-- >       (isSomeProperties @Int32 @Int16 Proxy Proxy)
isSomeProperties ::
  forall a b.
  (IsSome a b, Eq a, Eq b, Show a, Show b, Arbitrary a, Arbitrary b) =>
  Proxy a ->
  Proxy b ->
  [(String, Property)]
isSomeProperties :: forall a b.
(IsSome a b, Eq a, Eq b, Show a, Show b, Arbitrary a,
 Arbitrary b) =>
Proxy a -> Proxy b -> [(String, Property)]
isSomeProperties Proxy a
aProxy Proxy b
bProxy =
  [ ( String
"'to' is injective",
      (b -> b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \b
b1 b
b2 ->
        if b
b1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b2
          then Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
          else b -> a
to' b
b1 a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= b -> a
to' b
b2
    ),
    ( String
"'maybeFrom' is a partial inverse of 'to'",
      (b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \b
b ->
        a -> Maybe b
maybeFrom' (b -> a
to' b
b) Maybe b -> Maybe b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> Maybe b
forall a. a -> Maybe a
Just b
b
    ),
    ( String
"'maybeFrom' characterizes the image of 'to'",
      (a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \a
a ->
        case a -> Maybe b
maybeFrom' a
a of
          Just b
b -> b -> a
to' b
b a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== a
a
          Maybe b
Nothing -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    )
  ]
  where
    to' :: b -> a
to' = Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy (a -> a) -> (b -> a) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> a
forall a b. IsSome a b => b -> a
to (b -> a) -> (b -> b) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy
    maybeFrom' :: a -> Maybe b
maybeFrom' = (b -> b) -> Maybe b -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy) (Maybe b -> Maybe b) -> (a -> Maybe b) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Maybe b
forall a b. IsSome a b => a -> Maybe b
maybeFrom (a -> Maybe b) -> (a -> a) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy

-- |
-- Properties testing whether an instance satisfies the laws of 'IsMany'.
--
-- The instance is identified via the proxy types that you provide.
--
-- E.g., here's how you can integrate it into an Hspec test-suite:
--
-- > spec = do
-- >   describe "IsMany laws" do
-- >     traverse_
-- >       (uncurry prop)
-- >       (isManyProperties @String @Text Proxy Proxy)
isManyProperties ::
  forall a b.
  (IsMany a b, Eq a, Eq b, Show a, Show b, Arbitrary a, Arbitrary b) =>
  Proxy a ->
  Proxy b ->
  [(String, Property)]
isManyProperties :: forall a b.
(IsMany a b, Eq a, Eq b, Show a, Show b, Arbitrary a,
 Arbitrary b) =>
Proxy a -> Proxy b -> [(String, Property)]
isManyProperties Proxy a
aProxy Proxy b
bProxy =
  [ ( String
"'onfrom' is an inverse of 'to'",
      (b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \b
b -> b
b b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== a -> b
onfrom' (b -> a
to' b
b)
    ),
    ( String
"'onfrom' is consistent with 'maybeFrom'",
      (b -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \(b
b :: b) ->
        let a :: a
a = forall a b. IsSome a b => b -> a
to @a b
b
         in a -> Maybe b
forall a b. IsSome a b => a -> Maybe b
maybeFrom (forall a b. IsSome a b => b -> a
to @a b
b) Maybe b -> Maybe b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> Maybe b
forall a. a -> Maybe a
Just (forall a b. IsMany a b => a -> b
onfrom @a @b a
a)
    ),
    ( String
"'to' after 'onfrom' always succeeds with 'maybeFrom'",
      (a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \a
a ->
        let b :: b
b = a -> b
onfrom' a
a
         in a -> Maybe b
forall a b. IsSome a b => a -> Maybe b
maybeFrom (b -> a
to' b
b) Maybe b -> Maybe b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> Maybe b
forall a. a -> Maybe a
Just b
b
    )
  ]
    [(String, Property)]
-> [(String, Property)] -> [(String, Property)]
forall a. Semigroup a => a -> a -> a
<> Proxy a -> Proxy b -> [(String, Property)]
forall a b.
(IsSome a b, Eq a, Eq b, Show a, Show b, Arbitrary a,
 Arbitrary b) =>
Proxy a -> Proxy b -> [(String, Property)]
isSomeProperties Proxy a
aProxy Proxy b
bProxy
  where
    to' :: b -> a
to' = Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy (a -> a) -> (b -> a) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> a
forall a b. IsSome a b => b -> a
to (b -> a) -> (b -> b) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy
    onfrom' :: a -> b
onfrom' = Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
forall a b. IsMany a b => a -> b
onfrom (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy

-- |
-- Properties testing whether an instance satisfies the laws of 'Is'.
--
-- The instance is identified via the proxy types that you provide.
--
-- E.g., here's how you can integrate it into an Hspec test-suite:
--
-- > spec = do
-- >   describe "Is laws" do
-- >     traverse_
-- >       (uncurry prop)
-- >       (isProperties @Int32 @Word32 Proxy Proxy)
isProperties ::
  (Is a b, Eq a, Eq b, Show a, Show b, Arbitrary a, Arbitrary b) =>
  Proxy a ->
  Proxy b ->
  [(String, Property)]
isProperties :: forall a b.
(Is a b, Eq a, Eq b, Show a, Show b, Arbitrary a, Arbitrary b) =>
Proxy a -> Proxy b -> [(String, Property)]
isProperties Proxy a
aProxy Proxy b
bProxy =
  [ ( String
"'to' is an inverse of 'from'",
      (a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \a
b -> a
b a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> a
to' (a -> b
from' a
b)
    ),
    ( String
"'from' equals 'onfrom'",
      (a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property \a
a -> a -> b
from' a
a b -> b -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== a -> b
onfrom' a
a
    )
  ]
    [(String, Property)]
-> [(String, Property)] -> [(String, Property)]
forall a. Semigroup a => a -> a -> a
<> Proxy a -> Proxy b -> [(String, Property)]
forall a b.
(IsMany a b, Eq a, Eq b, Show a, Show b, Arbitrary a,
 Arbitrary b) =>
Proxy a -> Proxy b -> [(String, Property)]
isManyProperties Proxy a
aProxy Proxy b
bProxy
  where
    to' :: b -> a
to' = Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy (a -> a) -> (b -> a) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. b -> a
forall a b. IsSome a b => b -> a
to (b -> a) -> (b -> b) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy
    from' :: a -> b
from' = Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
forall b a. IsSome a b => b -> a
from (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy
    onfrom' :: a -> b
onfrom' = Proxy b -> b -> b
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy b
bProxy (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
forall a b. IsMany a b => a -> b
onfrom (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Proxy a -> a -> a
forall (proxy :: * -> *) c. proxy c -> c -> c
as Proxy a
aProxy