{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}

#ifndef HAVE_COMONAD

module Hedgehog.Classes.Comonad () where

#else

module Hedgehog.Classes.Comonad (comonadLaws) where

import Control.Comonad

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'Comonad' laws:
--
-- [__Extend/Extract Identity__]: @'extend' 'extract' ≡ 'id'@
-- [__Extract/Extend__]: @'extract' '.' 'extend' f ≡ f@
-- [__Extend/Extend__]: @'extend' f '.' 'extend' g ≡ 'extend' (f '.' 'extend' g)@
-- [__Extract Right Identity__]: @f '=>=' 'extract' ≡ f@
-- [__Extract Left Identity__]: @'extract' '=>=' f ≡ f@
-- [__Cokleisli Associativity__]: @(f '=>=' g) '=>=' h ≡ f '=>=' (g '=>=' h)@
-- [__Extract/Duplicate Identity__]: @'extract' '.' 'duplicate' ≡ 'id'@
-- [__Fmap Extract/Duplicate Identity__]: @'fmap' 'extract' '.' 'duplicate' ≡ 'id'@
-- [__Double Duplication__]: @'duplicate' '.' 'duplicate' ≡ 'fmap' 'duplicate' '.' 'duplicate'@
-- [__Extend/Fmap . Duplicate Identity__]: @'extend' f ≡ 'fmap' f '.' 'duplicate'@
-- [__Duplicate/Extend id Identity__]: @'duplicate' ≡ 'extend' 'id'@
-- [__Fmap/Extend Extract__]: @'fmap' f ≡ 'extend' (f '.' 'extract')@
-- [__Fmap/LiftW Isomorphism__]: @'fmap' ≡ 'liftW'@
comonadLaws ::
  ( Comonad f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Laws
comonadLaws gen = Laws "Comonad"
  [ ("Extend/Extract Identity", extendExtractIdentity gen)
  , ("Extract/Extend", extractExtend gen)
  , ("Extend/Extend", extendExtend gen)
  , ("Extract Right Identity", extractRightIdentity gen)
  , ("Extract Left Identity", extractLeftIdentity gen)
  , ("Cokleisli Associativity", cokleisliAssociativity gen)
  , ("Extract/Duplicate Identity", extractDuplicateIdentity gen)
  , ("Fmap Extract/Duplicate Identity", fmapExtractDuplicateIdentity gen)
  , ("Double Duplication", doubleDup gen)
  , ("Extend/Fmap . Duplicate Identity", extendDuplicate gen)
  , ("Duplicate/Extend id Identity", duplicateExtendId gen)
  , ("Fmap/Extend Extract", fmapExtendExtract gen)
  , ("Fmap/LiftW Isomorphism", fmapLiftW gen)
  ]

type ComonadProp f =
  ( Comonad f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Property

extendExtractIdentity :: forall f. ComonadProp f
extendExtractIdentity fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  let lhs = extend extract x
  let rhs = x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extend/Extract Identity", lawContextTcName = "Comonad"
        , lawContextLawBody = "extend extract" `congruency` "id"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "extend extract x" `congruency` "x, where"
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

extractExtend :: forall f. ComonadProp f
extractExtend fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  k <- forAll $ genLinearEquationW fgen
  let k' = runLinearEquationW k
  let lhs = extract . extend k' $ x
  let rhs = k' x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extract/Extend", lawContextTcName = "Comonad"
        , lawContextLawBody = "extract . extend f" `congruency` "f"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "extract . extend f $ x" `congruency` "f x, where"
            , "f = " ++ show k
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

extendExtend :: forall f. ComonadProp f
extendExtend fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  f' <- forAll $ genLinearEquationW fgen
  g' <- forAll $ genLinearEquationW fgen
  let f = runLinearEquationW f'
  let g = runLinearEquationW g'
  let lhs = extend f . extend g $ x
  let rhs = extend (f . extend g) x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extend/Extend", lawContextTcName = "Comonad"
        , lawContextLawBody = "extend f . extend g" `congruency` "extend (f . extend g)"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "extend f . extend g $ x" `congruency` "extend (f . extend g) $ x, where"
            , "f = " ++ show f'
            , "g = " ++ show g'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

extractRightIdentity :: forall f. ComonadProp f
extractRightIdentity fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  f' <- forAll $ genLinearEquationW fgen
  let f = runLinearEquationW f'
  let lhs = f =>= extract $ x
  let rhs = f x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extract Cokleisli Right Identity", lawContextTcName = "Comonad"
        , lawContextLawBody = "f =>= extract" `congruency` "f"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "f =>= extract $ x" `congruency` "f x, where"
            , "f = " ++ show f'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

extractLeftIdentity :: forall f. ComonadProp f
extractLeftIdentity fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  f' <- forAll $ genLinearEquationW fgen
  let f = runLinearEquationW f'
  let lhs = extract =>= f $ x
  let rhs = f x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extract Cokleisli Left Identity", lawContextTcName = "Comonad"
        , lawContextLawBody = "extract =>= f" `congruency` "f"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "extract =>= f $ x" `congruency` "f x, where"
            , "f = " ++ show f'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

cokleisliAssociativity :: forall f. ComonadProp f
cokleisliAssociativity fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  f' <- forAll $ genLinearEquationW fgen
  g' <- forAll $ genLinearEquationW fgen
  h' <- forAll $ genLinearEquationW fgen
  let f = runLinearEquationW f'
  let g = runLinearEquationW g'
  let h = runLinearEquationW h'
  let lhs = (f =>= g) =>= h $ x
  let rhs = f =>= (g =>= h) $ x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Cokleisli Associativity", lawContextTcName = "Comonad"
        , lawContextLawBody = "(f =>= g) =>= h" `congruency` "f =>= (g =>= h)"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "(f =>= g) =>= h $ x" `congruency` "f =>= (g =>= h) $ x, where"
            , "f = " ++ show f'
            , "g = " ++ show g'
            , "h = " ++ show h'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx


extractDuplicateIdentity :: forall f. ComonadProp f
extractDuplicateIdentity fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  let lhs = extract . duplicate $ x
  let rhs = x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extract/Duplicate Identity", lawContextTcName = "Comonad"
        , lawContextLawBody = "extract . duplicate" `congruency` "id"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "extract . duplicate $ x" `congruency` "x, where"
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

fmapExtractDuplicateIdentity :: forall f. ComonadProp f
fmapExtractDuplicateIdentity fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  let lhs = fmap extract . duplicate $ x
  let rhs = x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Fmap Extract/Duplicate Identity", lawContextTcName = "Comonad"
        , lawContextLawBody = "fmap extract . duplicate" `congruency` "id"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "fmap extract . duplicate $ x" `congruency` "x, where"
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

doubleDup :: forall f. ComonadProp f
doubleDup fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  let lhs = duplicate . duplicate $ x
  let rhs = fmap duplicate . duplicate $ x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Double Duplicate", lawContextTcName = "Comonad"
        , lawContextLawBody = "duplicate . duplicate" `congruency` "fmap duplicate . duplicate"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "duplicate . duplicate $ x" `congruency` "fmap duplicate . duplicate $ x, where"
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

extendDuplicate :: forall f. ComonadProp f
extendDuplicate fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  f' <- forAll $ genLinearEquationW fgen
  let f = runLinearEquationW f'
  let lhs = extend f $ x
  let rhs = fmap f . duplicate $ x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Extend/Fmap Duplicate", lawContextTcName = "Comonad"
        , lawContextLawBody = "extend f" `congruency` "fmap f . duplicate"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "extend f x" `congruency` "fmap f . duplicate $ x, where"
            , "f = " ++ show f'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

duplicateExtendId :: forall f. ComonadProp f
duplicateExtendId fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  let lhs = duplicate x
  let rhs = extend id x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Duplicate/Extend Id", lawContextTcName = "Comonad"
        , lawContextLawBody = "duplicate" `congruency` "extend id"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "duplicate x" `congruency` "extend id x, where"
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

fmapExtendExtract :: forall f. ComonadProp f
fmapExtendExtract fgen = property $ do
  x :: f Integer <- forAll $ fgen genSmallInteger
  f' <- forAll genLinearEquation
  let f = runLinearEquation f'
  let lhs = fmap f x
  let rhs = extend (f . extract) x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Fmap/Extend Extract", lawContextTcName = "Comonad"
        , lawContextLawBody = "fmap f" `congruency` "extend (f . extract)"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "fmap f x" `congruency` "extend (f . extract) x, where"
            , "f = " ++ show f'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

fmapLiftW :: forall f. ComonadProp f
fmapLiftW fgen = property $ do
  x <- forAll $ fgen genSmallInteger
  f' <- forAll genLinearEquation
  let f = runLinearEquation f'
  let lhs = fmap f x
  let rhs = liftW f x
  let ctx = contextualise $ LawContext
        { lawContextLawName = "Fmap/LiftW", lawContextTcName = "Comonad"
        , lawContextLawBody = "fmap" `congruency` "liftW"
        , lawContextReduced = reduced lhs rhs
        , lawContextTcProp = lawWhere
            [ "fmap f x" `congruency` "liftW f x, where"
            , "f = " ++ show f'
            , "x = " ++ show x
            ]
        }
  heqCtx lhs rhs ctx

#endif