Combinators.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.DLenses.Combinators
-- 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 lifts a standard set of point-free combinators into bidirectional delta-lenses.
--
-----------------------------------------------------------------------------

module Generics.Pointless.DLenses.Combinators where

import Data.Relation
import Data.Shape
import Generics.Pointless.DLenses
import Generics.Pointless.DLenses.ShapeCombinators
import Generics.Pointless.Lenses (Lens)
import qualified Generics.Pointless.Lenses as Lns
import Generics.Pointless.Lenses.Combinators

import Generics.Pointless.Functors
import Generics.Pointless.Combinators

-- | Delta lens composition
infixr 9 .<~
(.<~) :: (Shapely s,Shapely v,Shapely u) => DLens v b u c -> DLens s a v b -> DLens s a u c
f .<~ g = DLens get' getd' put' putd' create' created'
    where get' s = get f (get g s)
          getd' s = getd g s .~ getd f (get g s)
          put' (u,s) dU = put g (put f (u,get g s) dU,s) dV
            where dV = eitherPosR (u,s) (getd f v .~ dU) (locsR v) .~ putd f u v dU
                  v = get g s
          putd' u s dU =  eitherPosR (v',s)
            			    (sumPosR (u,v) (u,s) (locsR u) (getd g s) .~ putd f u v dU)
            			    (inrPosR (u,s))
            		   .~ putd g v' s dV
            where dV = eitherPosR (u,s) (getd f v .~ dU) (locsR v) .~ putd f u v dU
                  (v,v') = (get g s,put f (u,v) dV)
          create' u = create g (create f u)
          created' u = created f u .~ created g (create f u)

-- | Delta lens identity
id_dlns :: Shapely s => DLens s a s a
id_dlns = DLens get' getd' put' putd' create' created'
    where get' s = s
          getd' s = locsR s
          put' (s',s) dS = s'
          putd' s' s dS = inlPosR (s',s)
          create' s' = s'
          created' s' = locsR s'

-- | Delta lens bang
bang_dlns :: Shapely s => (Const One b -> s a) -> DLens s a (Const One) b
bang_dlns f = DLens get' getd' put' putd' create' created'
    where get' s = ConsF _L
          getd' s = emptyR
          put' (v,s) dV = s
          putd' v s dV = inlPosR (v,s)
          create' v = f v
          created' v = emptyR

-- | Delta lens left projection
fst_dlns :: (Shapely f,Shapely g) => (f a -> g a) -> DLens (f :*: g) a f a
fst_dlns h = DLens get' getd' put' putd' create' created'
    where get' (ProdF x y) = x
          getd' (ProdF x y) = inlPosR (x,y)
          put' (x',ProdF x y) dF = ProdF x' y
          putd' x' p@(ProdF x y) dF = sumPosR (x',y) (x',p) (locsR x') (inrPosR (x,y))
          create' x' = ProdF x' (h x')
          created' x' = inv (inlPosR (x',h x'))

-- | Delta lens right projection
snd_dlns :: (Shapely f,Shapely g) => (g a -> f a) -> DLens (f :*: g) a g a
snd_dlns h = DLens get' getd' put' putd' create' created'
    where get' (ProdF x y) = y
          getd' (ProdF x y) = inrPosR (x,y)
          put' (y',ProdF x y) dF = ProdF x y'
          putd' y' p@(ProdF x y) dF = eitherPosR (x,y') (inrPosR (y',p) .~ inlPosR (x,y)) (inlPosR (y',p))
          create' y' = ProdF (h y') y'
          created' y' = inv (inrPosR (h y',y'))

-- | Delta lens product
infix 7 ><<~
(><<~) :: (Shapely f,Shapely g,Shapely h,Shapely i) => DLens f a h b -> DLens g a i b -> DLens (f :*: g) a (h :*: i) b
f ><<~ g = DLens get' getd' put' putd' create' created'
    where get' (ProdF x y) = ProdF (get f x) (get g y)
          getd' (ProdF x y) = sumPosR (get f x,get g y) (x,y) (getd f x) (getd g y)
          put' (ProdF z w,ProdF x y) dV = ProdF (put f (z,x) d1) (put g (w,y) d2)
            where d1 = inv (inlPosR (get f x,get g y)) .~ dV .~ inlPosR (z,w)
                  d2 = inv (inrPosR (get f x,get g y)) .~ dV .~ inrPosR (z,w)
          putd' p1@(ProdF z w) p2@(ProdF x y) dV = eitherPosR (put f (z,x) d1,put g (w,y) d2)
                                               (sumPosR (z,x) (p1,p2) (inlPosR (z,w)) (inlPosR (x,y)) .~ putd f z x d1)
                                               (sumPosR (w,y) (p1,p2) (inrPosR (z,w)) (inrPosR (x,y)) .~ putd g w y d2)
            where d1 = inv (inlPosR (get f x,get g y)) .~ dV .~ inlPosR (z,w)
                  d2 = inv (inrPosR (get f x,get g y)) .~ dV .~ inrPosR (z,w)
          create' (ProdF z w) = ProdF (create f z) (create g w)
          created' (ProdF z w) = sumPosR (create f z,create g w) (z,w) (created f z) (created g w)
	
-- | Delta lens either
infix 4 \/<~
(\/<~) :: (Shapely f,Shapely g,Shapely h) => (h b -> Either One One) -> DLens f a h b -> DLens g a h b -> DLens (f :+: g) a h b
(\/<~) p f g = DLens get' getd' put' putd' create' created'
    where get' (InlF x) = get f x
          get' (InrF y) = get g y
          getd' (InlF x) = getd f x
          getd' (InrF y) = getd g y
          put' (z,InlF x) dV = InlF (put f (z,x) dV)
          put' (z,InrF y) dV = InrF (put g (z,y) dV)
          putd' z (InlF x) dV = putd f z x dV
          putd' z (InrF y) dV = putd g z y dV
          create' z = case (p z) of { Left _  -> InlF (create f z) ; Right _ -> InrF (create g z) }
          created' z = case (p z) of { Left _  -> created f z ; Right _ -> created g z }

-- | Delta lens sum
infix 5 -|-<~
(-|-<~) :: (Shapely f,Shapely g,Shapely h,Shapely i) => DLens f a h b -> DLens g a i b -> DLens (f :+: g) a (h :+: i) b
f -|-<~ g = DLens get' getd' put' putd' create' created'
    where get' (InlF x) = InlF (get f x)
          get' (InrF y) = InrF (get g y)
          getd' (InlF x) = getd f x
          getd' (InrF y) = getd g y
          put' (InlF z,InlF x) dV = InlF (put f (z,x) dV)
          put' (InlF z,InrF y) dV = InlF (create f z)
          put' (InrF w,InlF x) dV = InrF (create g w)
          put' (InrF w,InrF y) dV = InrF (put g (w,y) dV)
          putd' (InlF z) (InlF x) dV = putd f z x dV
          putd' (InlF z) (InrF y) dV = inlPosR (z,y) .~ created f z
          putd' (InrF w) (InlF x) dV = inlPosR (w,x) .~ created g w
          putd' (InrF w) (InrF y) dV = putd g w y dV
          create' (InlF z) = InlF (create f z)
          create' (InrF w) = InrF (create g w)
          created' (InlF z) = created f z
          created' (InrF w) = created g w

swap_dlns :: (Shapely f,Shapely g,ToRep f,ToRep g) => DLens (f :*: g) a (g :*: f) a
swap_dlns = nat_dlns (\a -> swap_lns)

coswap_dlns :: (Shapely f,Shapely g,ToRep f,ToRep g) => DLens (f :+: g) a (g :+: f) a
coswap_dlns = nat_dlns (\a -> coswap_lns)

distl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :+: g) :*: h) a ((f :*: h) :+: (g :*: h)) a
distl_dlns = nat_dlns (\a -> distl_lns)

undistl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :*: h) :+: (g :*: h)) a ((f :+: g) :*: h) a
undistl_dlns = nat_dlns (\a -> undistl_lns)

distr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens (f :*: (g :+: h)) a ((f :*: g) :+: (f :*: h)) a
distr_dlns = nat_dlns (\a -> distr_lns)

undistr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :*: g) :+: (f :*: h)) a (f :*: (g :+: h)) a
undistr_dlns = nat_dlns (\a -> undistr_lns)

assocl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens (f :*: (g :*: h)) a ((f :*: g) :*: h) a
assocl_dlns = nat_dlns (\a -> assocl_lns)

assocr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :*: g) :*: h) a (f :*: (g :*: h)) a
assocr_dlns = nat_dlns (\a -> assocr_lns)

coassocl_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens (f :+: (g :+: h)) a ((f :+: g) :+: h) a
coassocl_dlns = nat_dlns (\a -> coassocl_lns)

coassocr_dlns :: (Shapely f,Shapely g,Shapely h,ToRep f,ToRep g,ToRep h) => DLens ((f :+: g) :+: h) a (f :+: (g :+: h)) a
coassocr_dlns = nat_dlns (\a -> coassocr_lns)