-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.DLenses
-- Copyright   :  (c) 2011 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Lenses:
-- bidirectional lenses with point-free programming
-- 
-- This module defines the structure of delta lenses and provides Quickcheck procedures to test delta-lens well-behavedness.
--
-----------------------------------------------------------------------------

module Generics.Pointless.DLenses where

import Data.Relation
import Data.Shape
import Data.Diff
import Generics.Pointless.Lenses (Lens)
import qualified Generics.Pointless.Lenses as Lns

import qualified Data.Set as Set
import Test.QuickCheck.Gen
import Test.QuickCheck.Arbitrary
import Test.QuickCheck

-- | The data type of Diskin's et al delta lenses (http://dx.doi.org/10.5381/jot.2011.10.1.a6)
data DeltaLens s a v b = DeltaLens { get0 :: s a -> v b
                                   , getdelta :: s a -> s a -> Delta (s a) (s a) -> Delta (v b) (v b)
                                   , put0 :: (v b,s a) -> Delta (v b) (v b) -> s a
                                   , putdelta :: v b -> s a -> Delta (v b) (v b) -> Delta (s a) (s a) }

delta_lns :: (Shapely s,Shapely v) => DLens s a v b -> DeltaLens s a v b
delta_lns l = DeltaLens get0' getdelta' put0' putdelta'
    where get0' s = get l s
          getdelta' s' s dS = inv (getd l s) .~ dS .~ getd l s'
          put0' (v,s) dV = put l (v,s) dV
          putdelta' v s dV = eitherPosR (v,s) (getd l s .~ dV) (locsR s) .~ putd l v s dV

-- | The data type of (horizontal) delta lenses
data DLens s a v b = DLens { get     :: s a -> v b
                           , getd    :: s a -> Delta (v b) (s a)                                 -- delta (get s) s
                           , put     :: (v b,s a) -> Delta (v b) (v b) -> s a                    -- (v,s) -> delta v (get s) -> S
                           , putd    :: v b -> s a -> Delta (v b) (v b) -> Delta (s a) (v b,s a) -- v -> s -> d:delta v (get s) -> delta (put (v,s) d) (v,s)
                           , create  :: v b -> s a
                           , created :: v b -> Delta (s a) (v b)                                 -- v -> delta (create v) v
                           }

-- | The type of natural delta lenses.
type NatDLens s v = forall a. DLens s a v a

-- | Converts a delta lens, for a specific differencing operation, to a normal lens
embed_lns :: Shapely v => Diff (v b) -> DLens s a v b -> Lens (s a) (v b)
embed_lns diff l = Lns.Lens get' put' create'
    where get' = get l
          put' (v,s) = put l (v,s) (diff v (get l s) .~ getd l s)
          create' = create l

-- ** QuickCheck testing for well-behaved delta lenses

data TestArgs s a v b = TestArgs (v b) (s a) (Delta (v b) (v b)) deriving Show

-- | Generates a view, source and delta update triple
testGen :: (Arbitrary (s a),Arbitrary (v b),Shapely s,Shapely v) => DLens s a v b -> Gen (TestArgs s a v b)
testGen l = do
	v <- arbitrary
	s <- arbitrary
	dV <- deltaGen v (get l s)
	return $ TestArgs v s dV

-- | Generates a delta update (a partial function from positions to positions) between two values
deltaGen :: Shapely v => v b -> v b -> Gen (Delta (v b) (v b))
deltaGen v' v = locsGen (Set.toList $ locs v') (Set.toList $ locs v)
locsGen :: [Int] -> [Int] -> Gen (Int :->: Int)
locsGen [] l = return Set.empty
locsGen (i:is) l = do { x <- locGen i l; y <- locsGen is l; return (Set.union x y) }
locGen :: Int -> [Int] -> Gen (Int :->: Int)
locGen iv [] = return Set.empty
locGen iv l = oneof [do { is <- elements l; return (Set.singleton (iv,is)) },return Set.empty]

testDLens l = quickCheck $ forAll (testGen l) (wbDelta l)
    where wbDelta l (TestArgs v s dV) = wb l v s dV

-- | QuickCheck procedure to test if a lens is well-behaved.
wb :: (Eq (s a),Eq (v b),Shapely s,Shapely v) => DLens s a v b -> v b -> s a -> Delta (v b) (v b) -> Bool
wb l v s dV = putget l v s dV && getput l s && createget l v && putgetd l v s dV && getputd l s && creategetd l v

-- | QuickCheck procedure to test if a lens satisfies the PutGet law.
putget :: (Eq (s a),Eq (v b),Shapely s,Shapely v) => DLens s a v b -> v b -> s a -> Delta (v b) (v b) -> Bool
putget l v s dV = get l (put l (v,s) dV) == v

-- | QuickCheck procedure to test if a lens satisfies the GetPut law.
getput :: (Eq (s a),Shapely s,Shapely v) => DLens s a v b -> s a -> Bool
getput l s = let v = get l s in put l (get l s,s) (locsR v) == s

-- | QuickCheck procedure to test if a lens satisfies the CreateGet law.
createget :: (Eq (v b),Shapely s,Shapely v) => DLens s a v b -> v b -> Bool
createget l v = get l (create l v) == v

-- | QuickCheck procedure to test if a lens satisfies the PutGetDelta law.
putgetd :: (Shapely s,Shapely v) => DLens s a v b -> v b -> s a -> Delta (v b) (v b) -> Bool
putgetd l v s dV = let s' = put l (v,s) dV in putd l v s dV .~ getd l s' == inlPosR (v,s)

-- | QuickCheck procedure to test if a lens satisfies the GetPutDelta law.
getputd :: (Shapely s,Shapely v) => DLens s a v b -> s a -> Bool
getputd l s = let v = get l s in (eitherPosR (v,s) (getd l s) (locsR s)) .~ putd l (get l s) s (locsR v) == locsR s

-- | QuickCheck procedure to test if a lens satisfies the CreateGetDelta law.
creategetd :: (Shapely s,Shapely v) => DLens s a v b -> v b -> Bool
creategetd l v = let s = create l v in created l v .~ getd l s == locsR v