{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Profunctor.Optic.Property (
Iso
, fromto_iso
, tofrom_iso
, Prism
, tofrom_prism
, fromto_prism
, idempotent_prism
, Lens
, tofrom_lens
, fromto_lens
, idempotent_lens
, Grate
, pure_grate
, compose_grate
, Traversal0
, tofrom_traversal0
, fromto_traversal0
, idempotent_traversal0
, Traversal
, pure_traversal
, compose_traversal
, compose_traversal1
, Cotraversal1
, compose_cotraversal1
, Setter
, pure_setter
, compose_setter
, idempotent_setter
) where
import Control.Applicative
import Data.Profunctor.Optic.Import
import Data.Profunctor.Optic.Type
import Data.Profunctor.Optic.Iso
import Data.Profunctor.Optic.Setter
import Data.Profunctor.Optic.Lens
import Data.Profunctor.Optic.Prism
import Data.Profunctor.Optic.Grate
import Data.Profunctor.Optic.Traversal
import Data.Profunctor.Optic.Traversal0
fromto_iso :: Eq s => Iso' s a -> s -> Bool
fromto_iso o s = withIso o $ \sa as -> as (sa s) == s
tofrom_iso :: Eq a => Iso' s a -> a -> Bool
tofrom_iso o a = withIso o $ \sa as -> sa (as a) == a
tofrom_prism :: Eq s => Prism' s a -> s -> Bool
tofrom_prism o s = withPrism o $ \sta bt -> either id bt (sta s) == s
fromto_prism :: Eq s => Eq a => Prism' s a -> a -> Bool
fromto_prism o a = withPrism o $ \sta bt -> sta (bt a) == Right a
idempotent_prism :: Eq s => Eq a => Prism' s a -> s -> Bool
idempotent_prism o s = withPrism o $ \sta _ -> left sta (sta s) == left Left (sta s)
tofrom_lens :: Eq s => Lens' s a -> s -> Bool
tofrom_lens o s = withLens o $ \sa sas -> sas s (sa s) == s
fromto_lens :: Eq a => Lens' s a -> s -> a -> Bool
fromto_lens o s a = withLens o $ \sa sas -> sa (sas s a) == a
idempotent_lens :: Eq s => Lens' s a -> s -> a -> a -> Bool
idempotent_lens o s a1 a2 = withLens o $ \_ sas -> sas (sas s a1) a2 == sas s a2
pure_grate :: Eq s => Grate' s a -> s -> Bool
pure_grate o s = withGrate o $ \sabt -> sabt ($ s) == s
compose_grate :: Eq s => Grate' s a -> ((((s -> a) -> a) -> a) -> a) -> Bool
compose_grate o f = withGrate o $ \sabt -> sabt (\k -> f (k . sabt)) == sabt (\k -> f ($ k))
tofrom_traversal0 :: Eq a => Eq s => Traversal0' s a -> s -> a -> Bool
tofrom_traversal0 o s a = withTraversal0 o $ \sta sbt -> sta (sbt s a) == either (Left . flip const a) Right (sta s)
fromto_traversal0 :: Eq s => Traversal0' s a -> s -> Bool
fromto_traversal0 o s = withTraversal0 o $ \sta sbt -> either id (sbt s) (sta s) == s
idempotent_traversal0 :: Eq s => Traversal0' s a -> s -> a -> a -> Bool
idempotent_traversal0 o s a1 a2 = withTraversal0 o $ \_ sbt -> sbt (sbt s a1) a2 == sbt s a2
pure_traversal
:: Eq (f s)
=> Applicative f
=> ((a -> f a) -> s -> f s)
-> s -> Bool
pure_traversal abst = liftA2 (==) (abst pure) pure
compose_traversal
:: Eq (f (g s))
=> Applicative f
=> Applicative g
=> (forall f. Applicative f => (a -> f a) -> s -> f s)
-> (a -> g a) -> (a -> f a) -> s -> Bool
compose_traversal abst f g = liftA2 (==) (fmap (abst f) . abst g)
(getCompose . abst (Compose . fmap f . g))
compose_traversal1
:: Eq (f (g s))
=> Apply f
=> Apply g
=> (forall f. Apply f => (a -> f a) -> s -> f s)
-> (a -> g a) -> (a -> f a) -> s -> Bool
compose_traversal1 abst f g = liftF2 (==) (fmap (abst f) . abst g)
(getCompose . abst (Compose . fmap f . g))
compose_cotraversal1
:: Eq s
=> Apply f
=> Apply g
=> (forall f. Apply f => (f a -> a) -> f s -> s)
-> (g a -> a) -> (f a -> a) -> g (f s) -> Bool
compose_cotraversal1 abst f g = liftF2 (==) (abst f . fmap (abst g))
(abst (f . fmap g . getCompose) . Compose)
pure_setter :: Eq s => Setter' s a -> s -> Bool
pure_setter o s = over o id s == s
compose_setter :: Eq s => Setter' s a -> (a -> a) -> (a -> a) -> s -> Bool
compose_setter o f g s = (over o f . over o g) s == over o (f . g) s
idempotent_setter :: Eq s => Setter' s a -> s -> a -> a -> Bool
idempotent_setter o s a b = set o b (set o a s) == set o b s