module Data.Profunctor.Optic.Property where

import Control.Applicative
import Data.Profunctor.Optic.Prelude
import Data.Profunctor.Optic.Type
import Data.Profunctor.Optic.Iso
import Data.Profunctor.Optic.View
import Data.Profunctor.Optic.Setter
import Data.Profunctor.Optic.Lens
import Data.Profunctor.Optic.Prism
import Data.Profunctor.Optic.Grate
import Data.Profunctor.Optic.Fold
import Data.Profunctor.Optic.Fold0
import Data.Profunctor.Optic.Cofold
import Data.Profunctor.Optic.Traversal
import Data.Profunctor.Optic.Traversal0
import Data.Profunctor.Optic.Cotraversal

---------------------------------------------------------------------
-- 'Iso'
---------------------------------------------------------------------

iso_fromto' :: Eq s => Iso' s a -> s -> Bool
iso_fromto' o = withIso o iso_fromto

iso_tofrom' :: Eq a => Iso' s a -> a -> Bool
iso_tofrom' o = withIso o iso_tofrom

iso_fromto :: Eq s => (s -> a) -> (a -> s) -> s -> Bool
iso_fromto sa as s = as (sa s) == s

iso_tofrom :: Eq a => (s -> a) -> (a -> s) -> a -> Bool
iso_tofrom sa as a = sa (as a) == a

---------------------------------------------------------------------
-- 'Prism'
---------------------------------------------------------------------

-- If we are able to view an existing focus, then building it will return the original structure.
prism_tofrom :: Eq s => (s -> s + a) -> (a -> s) -> s -> Bool
prism_tofrom seta bt s = either id bt (seta s) == s

-- If we build a whole from any focus, that whole must contain a focus.
prism_fromto :: Eq s => Eq a => (s -> s + a) -> (a -> s) -> a -> Bool
prism_fromto seta bt a = seta (bt a) == Right a

prism_tofrom' :: Eq s => Prism' s a -> s -> Bool
prism_tofrom' o = withPrism o prism_tofrom

-- Reviewing a value with a 'Prism' and then previewing returns the value.
prism_fromto' :: Eq s => Eq a => Prism' s a -> a -> Bool
prism_fromto' o = withPrism o prism_fromto

---------------------------------------------------------------------
-- 'Lens'
---------------------------------------------------------------------


-- | A 'Lens' is a valid 'Traversal' with the following additional laws:
--
-- * @view o (set o b a)  ≡ b@
--
-- * @set o (view o a) a  ≡ a@
--
-- * @set o c (set o b a) ≡ set o c a@
--

lens_tofrom :: Eq s => (s -> a) -> (s -> a -> s) -> s -> Bool
lens_tofrom sa sas s = sas s (sa s) == s

lens_fromto :: Eq a => (s -> a) -> (s -> a -> s) -> s -> a -> Bool
lens_fromto sa sas s a = sa (sas s a) == a

lens_idempotent :: Eq s => (s -> a -> s) -> s -> a -> a -> Bool
lens_idempotent sas s a1 a2 = sas (sas s a1) a2 == sas s a2

-- | Putting back what you got doesn't change anything.
lens_tofrom' :: Eq s => Lens' s a -> s -> Bool
lens_tofrom' o = withLens o lens_tofrom

-- | You get back what you put in.
lens_fromto' :: Eq a => Lens' s a -> s -> a -> Bool
lens_fromto' o = withLens o lens_fromto

-- | Setting twice is the same as setting once.
lens_idempotent' :: Eq s => Lens' s a -> s -> a -> a -> Bool
lens_idempotent' o = withLens o $ const lens_idempotent

---------------------------------------------------------------------
-- 'Grate'
---------------------------------------------------------------------

-- | The 'Grate' laws are that of an algebra for a parameterised continuation monad.
--
-- * @grate ($ s) ≡ s@
--
-- * @grate (\k -> h (k . sabt)) ≡ sabt (\k -> h ($ k))@
--
grate_pure :: Eq s => (((s -> a) -> a) -> s) -> s -> Bool
grate_pure sabt s = sabt ($ s) == s

grate_pure' :: Eq s => (((s -> a) -> a) -> s) -> s -> a -> Bool
grate_pure' sabt s a = sabt (const a) == s

---------------------------------------------------------------------
-- 'Traversal0'
---------------------------------------------------------------------

atraversal_tofrom :: Eq a => Eq s => (s -> s + a) -> (s -> a -> s) -> s -> a -> Bool
atraversal_tofrom seta sbt s a = seta (sbt s a) == either (Left . flip const a) Right (seta s)

atraversal_fromto :: Eq s => (s -> s + a) -> (s -> a -> s) -> s -> Bool
atraversal_fromto seta sbt s = either id (sbt s) (seta s) == s

atraversal_idempotent :: Eq s => (s -> a -> s) -> s -> a -> a -> Bool
atraversal_idempotent sbt s a1 a2 = sbt (sbt s a1) a2 == sbt s a2

atraversal_tofrom' :: Eq a => Eq s => Traversal0' s a -> s -> a -> Bool
atraversal_tofrom' o = withTraversal0 o atraversal_tofrom

atraversal_fromto' :: Eq s => Traversal0' s a -> s -> Bool
atraversal_fromto' o = withTraversal0 o atraversal_fromto

atraversal_idempotent' :: Eq s => Traversal0' s a -> s -> a -> a -> Bool
atraversal_idempotent' o = withTraversal0 o $ const atraversal_idempotent

---------------------------------------------------------------------
-- 'Traversal'
---------------------------------------------------------------------


-- | 'Traversal' is a valid 'Setter' with the following additional laws:
--
-- * @t pure ≡ pure@
--
-- * @fmap (t f) . t g ≡ getCompose . t (Compose . fmap f . g)@
--
-- These can be restated in terms of 'traverseOf':
--
-- * @traverseOf t (Identity . f) ≡  Identity (fmap f)@
--
-- * @Compose . fmap (traverseOf t f) . traverseOf t g == traverseOf t (Compose . fmap f . g)@
--
-- See also < https://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf >
--

traverse_pure :: forall f s a. (Applicative f, Eq (f s)) => ((a -> f a) -> s -> f s) -> s -> Bool
traverse_pure o s = o pure s == (pure s :: f s)

--traverse_compose :: (Applicative f, Applicative g, Eq (f (g s))) => Traversal' s a -> (a -> g a) -> (a -> f a) -> s -> Bool
--traverse_compose t f g s = (fmap (t f) . t g) s == (getCompose . t (Compose . fmap f . g)) s

---------------------------------------------------------------------
-- 'Setter'
---------------------------------------------------------------------

-- | A 'Setter' is only legal if the following 3 laws hold:
--
-- 1. @set o y (set o x a) ≡ set o y a@
--
-- 2. @over o id ≡ id@
--
-- 3. @over o f . over o g ≡ over o (f . g)@

setter_id :: Eq s => Setter' s a -> s -> Bool
setter_id o s = over o id s == s

setter_compose :: Eq s => Setter' s a -> (a -> a) -> (a -> a) -> s -> Bool
setter_compose o f g s = (over o f . over o g) s == over o (f . g) s

setter_idempotent :: Eq s => Setter' s a -> s -> a -> a -> Bool
setter_idempotent o s a b = set o b (set o a s) == set o b s