{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}

module Hedgehog.Classes.Generic (genericLaws) where

import Hedgehog
import Hedgehog.Classes.Common

import GHC.Generics (Generic(..))

-- | Tests the following 'Generic' laws:
--
-- [__From-To Inverse__]: @'from' '.' 'to'@ ≡ @'id'@
-- [__To-From Inverse__]: @'to' '.' 'from'@ ≡ @'id'@
genericLaws ::
  ( Generic a, Eq a, Show a
  , Eq (Rep a x), Show (Rep a x)
  )
  => Gen a
  -> Gen (Rep a x) 
  -> Laws
genericLaws :: forall a x.
(Generic a, Eq a, Show a, Eq (Rep a x), Show (Rep a x)) =>
Gen a -> Gen (Rep a x) -> Laws
genericLaws Gen a
gena Gen (Rep a x)
genr = String -> [(String, Property)] -> Laws
Laws String
"Generic"
  [ (String
"From-To inverse", forall a x.
(Generic a, Eq (Rep a x), Show (Rep a x)) =>
Gen a -> Gen (Rep a x) -> Property
fromToInverse Gen a
gena Gen (Rep a x)
genr)
  , (String
"To-From inverse", forall a x.
(Generic a, Eq a, Show a) =>
Gen a -> Gen (Rep a x) -> Property
toFromInverse Gen a
gena Gen (Rep a x)
genr) 
  ]

fromToInverse :: forall a x.
  ( Generic a
  , Eq (Rep a x)
  , Show (Rep a x)
  ) => Gen a -> Gen (Rep a x) -> Property
fromToInverse :: forall a x.
(Generic a, Eq (Rep a x), Show (Rep a x)) =>
Gen a -> Gen (Rep a x) -> Property
fromToInverse Gen a
_gena Gen (Rep a x)
genr = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  Rep a x
r <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (Rep a x)
genr
  let lhs :: Rep a x
lhs = Rep a x
r
  let rhs :: Rep a x
rhs = forall a x. Generic a => a -> Rep a x
from (forall a x. Generic a => Rep a x -> a
to Rep a x
r :: a)
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"From-To inverse", lawContextTcName :: String
lawContextTcName = String
"Generic"
        , lawContextLawBody :: String
lawContextLawBody = String
"from . to" String -> String -> String
`congruency` String
"id"
        , lawContextTcProp :: String
lawContextTcProp =
            let showR :: String
showR = forall a. Show a => a -> String
show Rep a x
r
            in [String] -> String
lawWhere
              [ String
"from . to $ r" String -> String -> String
`congruency` String
"id r, where"
              , String
"r = " forall a. [a] -> [a] -> [a]
++ String
showR
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Rep a x
lhs forall {x}. Rep a x
rhs
        } 
  forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Rep a x
lhs forall {x}. Rep a x
rhs Context
ctx

toFromInverse :: forall a x.
  ( Generic a
  , Eq a
  , Show a
  ) => Gen a -> Gen (Rep a x) -> Property
toFromInverse :: forall a x.
(Generic a, Eq a, Show a) =>
Gen a -> Gen (Rep a x) -> Property
toFromInverse Gen a
gena Gen (Rep a x)
_genr = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
v <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gena
  let lhs :: a
lhs = forall a x. Generic a => Rep a x -> a
to (forall a x. Generic a => a -> Rep a x
from a
v)
  let rhs :: a
rhs = a
v
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"To-From inverse", lawContextTcName :: String
lawContextTcName = String
"Generic"
        , lawContextLawBody :: String
lawContextLawBody = String
"to . from" String -> String -> String
`congruency` String
"id"
        , lawContextTcProp :: String
lawContextTcProp =
            let showV :: String
showV = forall a. Show a => a -> String
show a
v
            in [String] -> String
lawWhere
              [ String
"to . from $ v" String -> String -> String
`congruency` String
"id v, where"
              , String
"v = " forall a. [a] -> [a] -> [a]
++ String
showV
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        } 
  forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
       
{-
type Generic1Prop f =
  ( Generic1 f
  , forall x. Eq x => Eq (f x)
  , forall x. Show x => Show (f x)
  , forall x. Eq x => Eq (Rep1 f x)
  , forall x. Show x => Show (Rep1 f x)
  ) => (forall x. Gen x -> Gen (f x))
    -> (forall x. Gen x -> Gen (Rep1 f x))
    -> Property

fromToInverse1 :: forall f. Generic1Prop f
fromToInverse1 _genf genr = property $ do
  r <- forAll $ genr genSmallInteger
  r === (from1 (to1 r :: f Integer))

toFromInverse1 :: forall f. Generic1Prop f
toFromInverse1 genf _genr = property $ do
  v <- forAll $ genf genSmallInteger
  v === (to1 . from1 $ v)
-}

{-
generic1Laws ::
  ( Generic1 f
  , forall x. Eq x => Eq (f x)
  , forall x. Show x => Show (f x)
  , forall x. Eq x => Eq (Rep1 f x)
  , forall x. Show x => Show (Rep1 f x)
  ) => (forall x. Gen x -> Gen (f x))
    -> (forall x. Gen x -> Gen (Rep1 f x))
    -> Laws
generic1Laws genf genr = Laws "Generic1"
  [ ("From1-To1 inverse", fromToInverse1 genf genr)
  , ("To1-From1 inverse", toFromInverse1 genf genr)
  ]
-}