{-# LANGUAGE RankNTypes #-}

module Hedgehog.Lens
  ( wellFormedPrism,
    wellFormedLens,
    wellFormedIso,
    prismExample,
  )
where

import Control.Lens
  ( Iso',
    Lens',
    Prism',
    matching,
    preview,
    review,
    set,
    view,
  )
import Control.Monad (Monad (return))
import Data.Either (Either (Left, Right))
import Data.Eq (Eq)
import Data.Function ((.))
import Data.Maybe (Maybe (Just))
import Hedgehog (Gen, PropertyT, annotate, forAll, (===))
import Text.Show (Show)

-- | Checks whether a prism respects the well-formedness laws:
--
-- 1) Get-Set Prism Law
-- 2) Set-Get Prism Law
wellFormedPrism ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Gen small ->
  -- | Prism signifying that the
  --          @small@ type is a subset of the @large@ type
  Prism' large small ->
  PropertyT m ()
wellFormedPrism :: Gen large -> Gen small -> Prism' large small -> PropertyT m ()
wellFormedPrism Gen large
genLarge Gen small
genSmall Prism' large small
o =
  do
    Gen large -> Prism' large small -> PropertyT m ()
forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen large -> Prism' large small -> PropertyT m ()
getSetPrismLaw Gen large
genLarge Prism' large small
o
    Gen small -> Prism' large small -> PropertyT m ()
forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen small -> Prism' large small -> PropertyT m ()
setGetPrismLaw Gen small
genSmall Prism' large small
o

-- | Get-Set Prism Law
--
-- @
-- 'matching' o s ≡ 'Right' a => 'review' o a ≡ s
-- @
getSetPrismLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Prism' large small ->
  PropertyT m ()
getSetPrismLaw :: Gen large -> Prism' large small -> PropertyT m ()
getSetPrismLaw Gen large
genLarge Prism' large small
o =
  do
    large
large <- Gen large -> PropertyT m large
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
    case APrism large large small small -> large -> Either large small
forall s t a b. APrism s t a b -> s -> Either t a
matching APrism large large small small
Prism' large small
o large
large of
      Right small
small ->
        do
          String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The get-set law must hold for a Prism"
          AReview large small -> small -> large
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview large small
Prism' large small
o small
small large -> large -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== large
large
      Left large
_ -> () -> PropertyT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Set-Get Prism Law
--
-- @
-- 'matching' o ('review' o b) ≡ 'Right' b
-- @
setGetPrismLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen small ->
  Prism' large small ->
  PropertyT m ()
setGetPrismLaw :: Gen small -> Prism' large small -> PropertyT m ()
setGetPrismLaw Gen small
genSmall Prism' large small
o =
  do
    small
small <- Gen small -> PropertyT m small
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
    String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-get law must hold for a Prism"
    APrism large large small small -> large -> Either large small
forall s t a b. APrism s t a b -> s -> Either t a
matching APrism large large small small
Prism' large small
o (AReview large small -> small -> large
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview large small
Prism' large small
o small
small) Either large small -> Either large small -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== small -> Either large small
forall a b. b -> Either a b
Right small
small

-- | Checks whether a lens respects the well-formedness laws:
--
-- 1) Get-Put Lens Law
-- 2) Put-Get Lens Law
-- 3) Put-Put Lens Law
wellFormedLens ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Gen small ->
  -- | Lens signifying that the @small@
  --          type is a constituent part of the @large@ type
  Lens' large small ->
  PropertyT m ()
wellFormedLens :: Gen large -> Gen small -> Lens' large small -> PropertyT m ()
wellFormedLens Gen large
genLarge Gen small
genSmall Lens' large small
o =
  do
    Gen large -> Gen small -> Lens' large small -> PropertyT m ()
forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen large -> Gen small -> Lens' large small -> PropertyT m ()
getPutLensLaw Gen large
genLarge Gen small
genSmall Lens' large small
o
    Gen large -> Lens' large small -> PropertyT m ()
forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen large -> Lens' large small -> PropertyT m ()
putGetLensLaw Gen large
genLarge Lens' large small
o
    Gen large -> Gen small -> Lens' large small -> PropertyT m ()
forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen large -> Gen small -> Lens' large small -> PropertyT m ()
putPutLensLaw Gen large
genLarge Gen small
genSmall Lens' large small
o

-- | Get-Put Lens Law
-- You get back what you put in:
--
-- @
-- 'view' l ('set' l v s) ≡ v
-- @
getPutLensLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Gen small ->
  Lens' large small ->
  PropertyT m ()
getPutLensLaw :: Gen large -> Gen small -> Lens' large small -> PropertyT m ()
getPutLensLaw Gen large
genLarge Gen small
genSmall Lens' large small
o =
  do
    large
large <- Gen large -> PropertyT m large
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
    small
small <- Gen small -> PropertyT m small
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
    String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-get law must hold for a Lens"
    Getting small large small -> large -> small
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting small large small
Lens' large small
o (ASetter large large small small -> small -> large -> large
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter large large small small
Lens' large small
o small
small large
large) small -> small -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== small
small

-- | Put-Get Lens Law
-- Putting back what you got doesn't change anything:
--
-- @
-- 'set' l ('view' l s) s ≡ s
-- @
putGetLensLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Lens' large small ->
  PropertyT m ()
putGetLensLaw :: Gen large -> Lens' large small -> PropertyT m ()
putGetLensLaw Gen large
genLarge Lens' large small
o =
  do
    large
large <- Gen large -> PropertyT m large
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
    String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The get-set law must hold for a Lens"
    ASetter large large small small -> small -> large -> large
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter large large small small
Lens' large small
o (Getting small large small -> large -> small
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting small large small
Lens' large small
o large
large) large
large large -> large -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== large
large

-- | Put-Put Lens Law
-- Setting twice is the same as setting once:
--
-- @
-- 'set' l v' ('set' l v s) ≡ 'set' l v' s
-- @
putPutLensLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Gen small ->
  Lens' large small ->
  PropertyT m ()
putPutLensLaw :: Gen large -> Gen small -> Lens' large small -> PropertyT m ()
putPutLensLaw Gen large
genLarge Gen small
genSmall Lens' large small
o =
  do
    large
large <- Gen large -> PropertyT m large
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
    small
small1 <- Gen small -> PropertyT m small
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
    small
small2 <- Gen small -> PropertyT m small
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
    String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-set law must hold for a Lens"
    ASetter large large small small -> small -> large -> large
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter large large small small
Lens' large small
o small
small2 (ASetter large large small small -> small -> large -> large
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter large large small small
Lens' large small
o small
small1 large
large) large -> large -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== ASetter large large small small -> small -> large -> large
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter large large small small
Lens' large small
o small
small2 large
large

-- | Checks whether an isomorphism respects the well-formedness laws:
--
-- 1) Set-Get Iso Law
-- 2) Get-Set Iso Law
wellFormedIso ::
  Monad m =>
  (Show a, Eq a) =>
  (Show b, Eq b) =>
  Gen a ->
  Gen b ->
  -- | Isomorphism signifying that types
  --          @a@ and @b@ are basically the same thing
  Iso' a b ->
  PropertyT m ()
wellFormedIso :: Gen a -> Gen b -> Iso' a b -> PropertyT m ()
wellFormedIso Gen a
genA Gen b
genB Iso' a b
o =
  do
    Gen b -> Iso' a b -> PropertyT m ()
forall (m :: * -> *) a b.
(Monad m, Show a, Eq a, Show b, Eq b) =>
Gen b -> Iso' a b -> PropertyT m ()
setGetIsoLaw Gen b
genB Iso' a b
o
    Gen a -> Iso' a b -> PropertyT m ()
forall (m :: * -> *) a b.
(Monad m, Show a, Eq a, Show b, Eq b) =>
Gen a -> Iso' a b -> PropertyT m ()
getSetIsoLaw Gen a
genA Iso' a b
o

-- | Set-Get Iso Law
-- You get back what you put in:
--
-- @
-- 'view' i . 'review' i ≡ 'id'
-- @
setGetIsoLaw ::
  Monad m =>
  (Show a, Eq a) =>
  (Show b, Eq b) =>
  Gen b ->
  Iso' a b ->
  PropertyT m ()
setGetIsoLaw :: Gen b -> Iso' a b -> PropertyT m ()
setGetIsoLaw Gen b
genB Iso' a b
o =
  do
    b
b <- Gen b -> PropertyT m b
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen b
genB
    String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-get law must hold for an Iso"
    (Getting b a b -> a -> b
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting b a b
Iso' a b
o (a -> b) -> (b -> a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AReview a b -> b -> a
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview a b
Iso' a b
o) b
b b -> b -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== b
b

-- | Get-Set Iso Law
-- You get back what you put in:
--
-- @
-- 'review' i . 'view' i ≡ 'id'
-- @
getSetIsoLaw ::
  Monad m =>
  (Show a, Eq a) =>
  (Show b, Eq b) =>
  Gen a ->
  Iso' a b ->
  PropertyT m ()
getSetIsoLaw :: Gen a -> Iso' a b -> PropertyT m ()
getSetIsoLaw Gen a
genA Iso' a b
o =
  do
    a
a <- Gen a -> PropertyT m a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
genA
    String -> PropertyT m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The get-set law must hold for an Iso"
    (AReview a b -> b -> a
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview a b
Iso' a b
o (b -> a) -> (a -> b) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting b a b -> a -> b
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting b a b
Iso' a b
o) a
a a -> a -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== a
a

-- | Assert that a prism matches for a particular set of values:
-- A 'review' of the @small@ value should produce the @large@ value, and
-- a 'preview' of the @large@ value should produce the @small@ value.
prismExample ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  -- | Prism signifying that the
  --          @small@ type is a subset of the @large@ type
  Prism' large small ->
  large ->
  small ->
  PropertyT m ()
prismExample :: Prism' large small -> large -> small -> PropertyT m ()
prismExample Prism' large small
o large
large small
small =
  do
    AReview large small -> small -> large
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview large small
Prism' large small
o small
small large -> large -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== large
large
    Getting (First small) large small -> large -> Maybe small
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview Getting (First small) large small
Prism' large small
o large
large Maybe small -> Maybe small -> PropertyT m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== small -> Maybe small
forall a. a -> Maybe a
Just small
small