-----------------------------------------------------------------------------
-- |
-- 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))