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

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 Optics.AffineFold (preview)
import Optics.AffineTraversal (matching)
import Optics.Getter (view)
import Optics.Iso (Iso')
import Optics.Lens (Lens')
import Optics.Prism (Prism')
import Optics.Review (review)
import Optics.Setter (set)
import Text.Show (Show)

-- | Checks whether a prism respects the well-formedness
--    laws given in "Optics.Prism"
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 :: forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen large -> Gen small -> Prism' large small -> PropertyT m ()
wellFormedPrism Gen large
genLarge Gen small
genSmall Prism' large small
o = do
  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
  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

getSetPrismLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Prism' large small ->
  PropertyT m ()
getSetPrismLaw :: 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 = do
  large
large <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
  case forall k (is :: IxList) s t a b.
Is k An_AffineTraversal =>
Optic k is s t a b -> s -> Either t a
matching Prism' large small
o large
large of
    Right small
small -> do
      forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The get-set law must hold for a Prism"
      forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Prism' large small
o small
small forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== large
large
    Left large
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

setGetPrismLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen small ->
  Prism' large small ->
  PropertyT m ()
setGetPrismLaw :: 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 = do
  small
small <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
  forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-get law must hold for a Prism"
  forall k (is :: IxList) s t a b.
Is k An_AffineTraversal =>
Optic k is s t a b -> s -> Either t a
matching Prism' large small
o (forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Prism' large small
o small
small) forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall a b. b -> Either a b
Right small
small

-- | Checks whether a lens respects the well-formedness
--    laws given in "Optics.Lens"
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 :: forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Gen large -> Gen small -> Lens' large small -> PropertyT m ()
wellFormedLens Gen large
genLarge Gen small
genSmall Lens' large small
o = do
  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
  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
  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

getPutLensLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Gen small ->
  Lens' large small ->
  PropertyT m ()
getPutLensLaw :: 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 = do
  large
large <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
  small
small <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
  forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-get law must hold for a Lens"
  forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Lens' large small
o (forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Lens' large small
o small
small large
large) forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== small
small

putGetLensLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Lens' large small ->
  PropertyT m ()
putGetLensLaw :: 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 = do
  large
large <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
  forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The get-set law must hold for a Lens"
  forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Lens' large small
o (forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Lens' large small
o large
large) large
large forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== large
large

putPutLensLaw ::
  Monad m =>
  (Show large, Eq large) =>
  (Show small, Eq small) =>
  Gen large ->
  Gen small ->
  Lens' large small ->
  PropertyT m ()
putPutLensLaw :: 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 = do
  large
large <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen large
genLarge
  small
small1 <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
  small
small2 <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen small
genSmall
  forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-set law must hold for a Lens"
  forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Lens' large small
o small
small2 (forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Lens' large small
o small
small1 large
large) forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Lens' large small
o small
small2 large
large

-- | Checks whether an isomorphism respects the
--    well-formedness laws given in "Optics.Iso"
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 :: forall (m :: * -> *) a b.
(Monad m, Show a, Eq a, Show b, Eq b) =>
Gen a -> Gen b -> Iso' a b -> PropertyT m ()
wellFormedIso Gen a
genA Gen b
genB Iso' a b
o = do
  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
  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

setGetIsoLaw ::
  Monad m =>
  (Show a, Eq a) =>
  (Show b, Eq b) =>
  Gen b ->
  Iso' a b ->
  PropertyT m ()
setGetIsoLaw :: 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 = do
  b
b <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen b
genB
  forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The set-get law must hold for an Iso"
  (forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Iso' a b
o forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Iso' a b
o) b
b forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== b
b

getSetIsoLaw ::
  Monad m =>
  (Show a, Eq a) =>
  (Show b, Eq b) =>
  Gen a ->
  Iso' a b ->
  PropertyT m ()
getSetIsoLaw :: 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 = do
  a
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
genA
  forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate String
"The get-set law must hold for an Iso"
  (forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Iso' a b
o forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Iso' a b
o) a
a 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 :: forall (m :: * -> *) large small.
(Monad m, Show large, Eq large, Show small, Eq small) =>
Prism' large small -> large -> small -> PropertyT m ()
prismExample Prism' large small
o large
large small
small = do
  forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Prism' large small
o small
small forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== large
large
  forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Prism' large small
o large
large forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall a. a -> Maybe a
Just small
small