-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Pf
-- Copyright   :  (c) 2010 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Rewrite:
-- automatic transformation system for point-free programs
-- 
-- Type-safe representation of point-free expressions at the value level.
--
-----------------------------------------------------------------------------

module Data.Pf where

-- * Representation of point-free expressions

import Data.Type

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

import Prelude hiding (Functor(..))
import Data.Monoid

data Pf a where
    
    -- Variables and pointwise expressions
    VAR           :: String -> Pf a
    FUN           :: String -> (a -> b) -> Pf (a -> b)
    
    -- Internal combinators
    BOT           :: Pf a
    TOP           :: Pf a
    CONV          :: Either One One -> Pf (a -> b) -> Pf (b -> a)
    CONV_LNS      :: Either One One -> Pf (Lens c a) -> Pf (Lens a c)
    LNS           :: String -> Lens c a -> Pf (Lens c a)
    COMPF         :: Functor f => Fctr f -> Type a -> Pf (Rep f a -> b) -> Pf (c -> Rep f a) -> Pf (c -> b)
    COMPF_LNS     :: Functor f => Fctr f -> Type a -> Pf (Lens (Rep f a) b) -> Pf (Lens c (Rep f a)) -> Pf (Lens c b)
    -- Internal encapsulators
    PROTECT       :: Pf (a -> b) -> Pf (a -> b)
    PROTECT_LNS   :: Pf (Lens a b) -> Pf (Lens a b)
    
    -- Non-recursive point-free combinators
    PNT           :: a -> Pf (One -> a)
    BANG          :: Pf (a -> One)
    COMP          :: Type b -> Pf (b -> c) -> Pf (a -> b) -> Pf (a -> c)
    FST           :: Pf ((a,b) -> a)
    SND           :: Pf ((a,b) -> b)
    SPLIT         :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))
    PROD          :: Pf (a -> c) -> Pf (b -> d) -> Pf ((a,b) -> (c,d))
    INL           :: Pf (a -> Either a b)
    INR           :: Pf (b -> Either a b)
    EITHER        :: Pf (a -> c) -> Pf (b -> c) -> Pf (Either a b -> c)
    SUM           :: Pf (a -> c) -> Pf (b -> d) -> Pf (Either a b -> Either c d)
    
    MKDYN         :: Type a -> Pf (a -> Dynamic)
    UNDYN         :: Type a -> Pf (Dynamic -> a)
    CAST          :: Type a -> Pf (b -> a)
   
    -- Monoids
    ZERO          :: Monoid b => Pf (a -> b)
    PLUS          :: Monoid a => Pf ((a,a) -> a)
    FOLD          :: Monoid a => Pf ([a] -> a)
   
    -- Isomorphic point-free combinators
    ID            :: Pf (c -> c)
    SWAP          :: Pf ((a,b) -> (b,a))
    COSWAP        :: Pf ((Either a b) -> (Either b a))
    DISTL         :: Pf ((Either a b,c) -> (Either (a,c) (b,c)))
    UNDISTL       :: Pf ((Either (a,c) (b,c)) -> (Either a b, c))
    DISTR         :: Pf ((c, Either a b) -> (Either (c,a) (c,b)))
    UNDISTR       :: Pf ((Either (c,a) (c,b)) -> (c,Either a b))
    ASSOCL        :: Pf ((a,(b,c)) -> ((a,b),c))
    ASSOCR        :: Pf (((a,b),c) -> (a,(b,c)))
    COASSOCL      :: Pf ((Either a (Either b c)) -> (Either (Either a b) c))
    COASSOCR      :: Pf ((Either (Either a b) c) -> (Either a (Either b c)))

    -- Recursive point-free combinators
    INN           :: (Mu a,Functor (PF a)) => Pf (F a a -> a)
    OUT           :: (Mu a,Functor (PF a)) => Pf (a -> F a a)
    FMAP          :: Functor f => Fctr f -> Type (c -> a) -> Pf (c -> a) -> Pf (Rep f c -> Rep f a)
    FZIP          :: Functor f => Fctr f -> Type (a -> c) -> Pf (a -> c) -> Pf ((Rep f a,Rep f c) -> Rep f (a,c))
    ANA           :: (Mu b,Functor (PF b)) => Pf (a -> (F b a)) -> Pf (a -> b)
    CATA          :: (Mu a,Functor (PF a)) => Pf (F a b -> b) -> Pf (a -> b)
    PARA          :: (Mu a,Functor (PF a)) => Pf (F a (b,a) -> b) -> Pf (a -> b)
    
    -- User-defined functions
    WRAP              :: Pf (a -> [a])
    MAP               :: Pf (a -> b) -> Pf ([a] -> [b])
    LHEAD              :: Pf ([a] -> [a]) -- safe head
    LTAIL              :: Pf ([a] -> [a]) -- safe tail
    NONEMPTY          :: Pf ([a] -> Bool)
    LENGTH            :: Pf ([a] -> Nat)
    ONE               :: Pf (a -> Nat)
    
    -- Lens Point-free functions
    GET           :: Pf (Lens c a) -> Pf (c -> a)
    PUT           :: Pf (Lens c a) -> Pf ((a,c) -> c)
    CREATE        :: Pf (Lens c a) -> Pf (a -> c)
    
    -- Non-recursive lenses
    COMP_LNS      :: Type b -> Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)
    FST_LNS       :: Pf (a -> b) -> Pf (Lens (a,b) a)
    SND_LNS       :: Pf (b -> a) -> Pf (Lens (a,b) b)
    PROD_LNS      :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))
    EITHER_LNS    :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
    SUM_LNS       :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
    SUMW_LNS      :: Pf ((a,d) -> c) -> Pf ((b,c) -> d) -> Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
    BANG_LNS      :: Pf (One -> c) -> Pf (Lens c One)
    BANGL_LNS     :: Pf (Lens c (One,c))
    BANGR_LNS     :: Pf (Lens c (c,One))
    
    -- Non-recursive isomorphisms
    ID_LNS        :: Pf (Lens c c)
    SWAP_LNS      :: Pf (Lens (a,b) (b,a))
    COSWAP_LNS    :: Pf (Lens (Either a b) (Either b a))
    DISTL_LNS     :: Pf (Lens (Either a b,c) (Either (a,c) (b,c)))
    UNDISTL_LNS   :: Pf (Lens (Either (a,c) (b,c)) (Either a b,c))
    DISTR_LNS     :: Pf (Lens (c, Either a b) (Either (c,a) (c,b)))
    UNDISTR_LNS   :: Pf (Lens (Either (c,a) (c,b)) (c,Either a b))
    ASSOCL_LNS    :: Pf (Lens (a,(b,c)) ((a,b),c))
    ASSOCR_LNS    :: Pf (Lens ((a,b),c) (a,(b,c)))
    COASSOCL_LNS  :: Pf (Lens (Either a (Either b c)) (Either (Either a b) c))
    COASSOCR_LNS  :: Pf (Lens (Either (Either a b) c) (Either a (Either b c)))
    
    -- Recursive lenses
    INN_LNS       :: (Mu a,Functor (PF a)) => Pf (Lens (F a a) a)
    OUT_LNS       :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a))
    FMAP_LNS      :: Functor f => Fctr f -> Type (c -> a) -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))
    ANA_LNS       :: (Mu b,Functor (PF b)) => Pf (Lens a (F b a)) -> Pf (Lens a b)
    CATA_LNS      :: (Mu a,Functor (PF a)) => Pf ((Lens (F a b) b)) -> Pf (Lens a b)
    
    -- User-defined lenses
    MAP_LNS           :: Pf (Lens a b) -> Pf (Lens [a] [b])
    LENGTH_LNS        :: a -> Pf (Lens [a] Nat)
    FILTER_LEFT_LNS   :: Pf (Lens [Either a b] [a])
    FILTER_RIGHT_LNS  :: Pf (Lens [Either a b] [b])
    CAT_LNS           :: Pf (Lens ([a],[a]) [a])
    CONCAT_LNS        :: Pf (Lens [[a]] [a])
    SUMN_LNS          :: Pf (Lens [Nat] Nat)
    PLUSN_LNS          :: Pf (Lens (Nat,Nat) Nat)

    -- Type-preserving strategy combinators
    APPLY             :: Type a -> Pf T -> Pf (a -> a)
    MKT               :: Type a -> Pf (a -> a) -> Pf T
    NOP               :: Pf T
    SEQ               :: Pf T -> Pf T -> Pf T
    EXTT              :: Pf T -> Type b -> Pf (b -> b) -> Pf T
    ALL               :: Pf T -> Pf T
    EVERYWHERE        :: Pf T -> Pf T		-- bottom-up (catamorphism)
    EVERYWHERE'       :: Pf T -> Pf T		-- top-down (anamorphism)
    -- Type-unifying strategy combinators
    APPLYQ            :: Type a -> Pf (Q r) -> Pf (a -> r)
    MKQ               :: Monoid r => Type a -> Pf (a -> r) -> Pf (Q r)
    EMPTYQ            :: Monoid r => Pf (Q r)
    UNION             :: Monoid r => Pf (Q r) -> Pf (Q r) -> Pf (Q r)
    EXTQ              :: Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (Q r)
    GMAPQ             :: Monoid r => Pf (Q r) -> Pf (Q r)
    EVERYTHING        :: Monoid r => Pf (Q r) -> Pf (Q r) -- bottom-up, right-to-left (paramorphism)
    -- XPath-like strategic combinators
    SELF              :: Pf (Q [Dynamic])
    ATT               :: Pf (Q [Dynamic]) --auxiliary self attribute, only used for eval of attribute
    CHILD             :: Pf (Q [Dynamic])
    ATTRIBUTE         :: Pf (Q [Dynamic])
    DESCENDANT        :: Pf (Q [Dynamic])
    DESCSELF          :: Pf (Q [Dynamic])
    NAME              :: String -> Pf (Q [Dynamic])
    (:/:)             :: Monoid r => Pf (Q [Dynamic]) -> Pf (Q r) -> Pf (Q r)
    SEQQ              :: Typeable r => Pf (Q r) -> Pf (r -> s) -> Pf (Q s)
    (:?:)             :: Pf (Q [Dynamic]) -> Pf (Q Bool) -> Pf (Q [Dynamic])
    (:/\:)            :: Pf (Q a) -> Pf (Q b) -> Pf (Q (a,b))

constPf :: a -> Pf (b -> a)
constPf v = COMP One (PNT v) BANG  

infix 5  ?=
(?=) :: Type a -> Pf (a -> Either One One) -> Pf (a -> Either a a)
(?=) a p = COMP (Either (Prod One a) (Prod One a)) (SND -|-= SND) $ COMP (Prod (Either One One) a) DISTL $ p /\= ID

infixr 9 .=
(.=) :: Typeable b => Pf (b -> a) -> Pf (c -> b) -> Pf (c -> a)
(.=) f g = COMP typeof f g

infix 6  /\=
(/\=) :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))
(/\=) f g = SPLIT f g

infix 7 ><=
(><=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((c,d) -> (a,b))
(><=) f g = PROD f g

infix 4 \/=
(\/=) :: Pf (b -> a) -> Pf (c -> a) -> Pf (Either b c -> a)
(\/=) f g = EITHER f g

infix 5 -|-=
(-|-=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((Either c d) -> (Either a b))
(-|-=) f g = SUM f g

distp_pf :: Pf (((c,d),(a,b)) -> ((c,a),(d,b)))
distp_pf = FST ><= FST /\= SND ><= SND

dists_pf :: Type (Either a b,Either c d) -> Pf ((Either a b,Either c d) -> (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))
dists_pf (Prod (Either a b) (Either c d)) = COMP t (DISTR -|-= DISTR) DISTL
    where t = Either (Prod a (Either c d)) (Prod b (Either c d))

infixr 9 .<<
(.<<) :: Typeable b => Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)
(.<<) f g = COMP_LNS typeof f g

infix 7 ><<<
(><<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))
(><<<) f g = PROD_LNS f g

infix 5 -|-<<
(-|-<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
(-|-<<) f g = SUM_LNS f g

infix 4 \/<<
(\/<<) :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
(\/<<) x f g = EITHER_LNS x f g

infix 4 .\/<<
(.\/<<) :: Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
(.\/<<) f g = EITHER_LNS (COMP One INL BANG) f g

infix 4 \/.<<
(\/.<<) :: Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
(\/.<<) f g = EITHER_LNS (COMP One INR BANG) f g


dists_lns :: Type (Either a b,Either c d) -> Pf (Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))
dists_lns (Prod (Either a b) (Either c d)) = COMP_LNS t (DISTR_LNS -|-<< DISTR_LNS) DISTL_LNS
    where t = Either (Prod a (Either c d)) (Prod b (Either c d))

fmap_Lns :: (Functor f,Typeable (c -> a)) => Fctr f -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))
fmap_Lns fctr f = FMAP_LNS fctr typeof f

listzip :: Type a -> Type b -> Pf (([a],[b]) -> [(a,b)])
listzip a b = ANA $ COMP t3 (BANG `SUM` distp) $ COMP t2 COASSOCL $ COMP t1 dists $ OUT `PROD` OUT
    where distp = distp_pf
          dists = dists_pf t1
          (la,lb) = (List a,List b)
          t1 = Prod (Either One $ Prod a la) (Either One $ Prod b lb)
          t2 = Either (Either (Prod One One) (Prod One $ Prod b lb)) (Either (Prod (Prod a la) One) (Prod (Prod a la) (Prod b lb)))
          t3 = Either (Either (Either (Prod One One) (Prod One $ Prod b lb)) (Prod (Prod a la) One)) (Prod (Prod a la) (Prod b lb))