>
> module Control.CCA.CCNF
> (norm, normOpt,
> pprNorm, pprNormOpt, printCCA, ASyn) where
#if __GLASGOW_HASKELL__ >= 610
> import Control.Category
> import Prelude hiding ((.), init)
#else
> import Prelude hiding (init)
#endif
> import Control.Arrow
> import Control.CCA.Types
> import Data.Char (isAlpha)
> import Language.Haskell.TH
> import Language.Haskell.TH.Syntax
> import Language.Haskell.TH.Instances
> import qualified Data.Generics as G (everywhere, mkT)
Internal Representation
=======================
We use AExp to syntactically represent an arrow for normalization purposes.
> data AExp
> = Arr ExpQ
> | First AExp
> | AExp :>>> AExp
> | Loop AExp
> | LoopD ExpQ AExp
> | LoopB ExpQ AExp
> | Init ExpQ
> | Lft AExp
> infixl 1 :>>>
We use phantom types to make ASyn an Arrow.
> newtype ASyn b c = AExp AExp
#if __GLASGOW_HASKELL__ >= 610
> instance Category ASyn where
> id = AExp (Arr [|\x -> x|])
> AExp g . AExp f = AExp (f :>>> g)
> instance Arrow ASyn where
> arr f = error "use arr' instead"
> first (AExp f) = AExp (First f)
#else
> instance Arrow ASyn where
> arr f = error "use arr' instead"
> AExp f >>> AExp g = AExp (f :>>> g)
> first (AExp f) = AExp (First f)
#endif
> instance ArrowLoop ASyn where
> loop (AExp f) = AExp (Loop f)
> instance ArrowInit ASyn where
> init i = error "use init' instead"
> arr' f _ = AExp (Arr f)
> init' i _ = AExp (Init i)
ArrowChoice only requires definition for 'left', but the default implementation
for 'right' and '|||' uses arr so we need to redefine them using arr' here.
'+++' is also redefined here for completeness.
> instance ArrowChoice ASyn where
> left (AExp f) = AExp (Lft f)
> right f = arr' [| mirror |] mirror >>> left f
> >>> arr' [| mirror |] mirror
> f +++ g = left f >>> right g
> f ||| g = f +++ g >>> arr' [| untag |] untag
These helpers have to be at the toplevel because TH cannot splice in a
polymorphic local function.
> mirror (Left x) = Right x
> mirror (Right y) = Left y
> untag (Left x) = x
> untag (Right y) = y
Pretty printing AExp.
> printCCA (AExp x) = printAExp x
> printAExp x = runQ (fromAExp x) >>= putStrLn . simplify . pprint
> simplify = unwords . map (unwords . (map aux) . words) . lines
> where aux (c:x) | not (isAlpha c) = c : aux x
> aux x = let (u, v) = break (=='.') x
> in if length v > 1 then aux (tail v)
> else x
Traversal over AExp is defined in terms of imap (intermediate map)
and everywhere.
> type Traversal = AExp -> AExp
> imap :: Traversal -> Traversal
> imap h (First f) = First (h f)
> imap h (f :>>> g) = h f :>>> h g
> imap h (Loop f) = Loop (h f)
> imap h (LoopD i f) = LoopD i (h f)
> imap h (LoopB i f) = LoopB i (h f)
> imap h (Lft f) = Lft (h f)
> imap h x = x
> everywhere :: Traversal -> Traversal
> everywhere h e = h (imap (everywhere h) e)
Normalization
=============
norm is a TH function that normalizes a given CCA, e.g., $(norm e) will
give the CCNF of e.
> norm :: ASyn t t1 -> ExpQ
> norm (AExp e) = fromAExp (normE e)
> normE = everywhere (normalize normE)
normOpt returns the pair of state and pure function as (i, f) from optimized
CCNF in the form loopD i (arr f).
> normOpt :: ASyn t t1 -> ExpQ
> normOpt (AExp e) =
> case toLoopD $ normE e of
> LoopD i (Arr f) -> tupE [i, f]
> _ -> error "The given arrow can't be normalized to optimized CCNF."
pprNorm and pprNormOpt return the pretty printed normal forms as a
string.
> pprNorm = ppr' . norm
> pprNormOpt = ppr' . normOpt
> ppr' e = runQ (fmap toLet e) >>= litE . StringL . simplify . pprint
fromAExp converts AExp back to TH Exp structure.
> fromAExp (Arr f) = appE [|arr|] f
> fromAExp (First f) = appE [|first|] (fromAExp f)
> fromAExp (f :>>> g) = infixE (Just (fromAExp f)) [|(>>>)|] (Just (fromAExp g))
> fromAExp (Loop f) = appE [|loop|] (fromAExp f)
> fromAExp (LoopD i f) = appE (appE [|loopD|] i) (fromAExp f)
> fromAExp (LoopB i f) = appE (appE [|loopB|] i) (fromAExp f)
> fromAExp (Init i) = appE [|init|] i
> fromAExp (Lft f) = appE [|left|] (fromAExp f)
CCNF
====
Arrow laws:
> normalize norm (Arr f :>>> Arr g) = Arr (g `o` f)
> normalize norm (First (Arr f)) = Arr (f `crossE` idE)
> normalize norm (First f :>>> First g) = First ((f :>>> g))
Choice:
> normalize norm (Lft (Arr f)) = Arr [| \x -> case x of
> Left a -> Left ($f a)
> Right b -> Right b |]
> normalize norm (Lft (LoopB i f)) =
> norm (LoopB i (Arr tagE :>>> Lft f :>>> Arr untagE))
> where
> tagE = [| \(inp,s) -> case inp of
> Left a -> Left (a, s)
> Right c -> Right (c, s) |]
> untagE = [| \out -> case out of
> Left (b,s) -> (Left b, s)
> Right (c,s) -> (Right c, s) |]
LoopB laws:
> normalize norm (h :>>> (LoopB i f)) = norm (LoopB i (First h :>>> f))
> normalize norm ((LoopB i f) :>>> h) = norm (LoopB i (f :>>> First h))
> normalize norm (LoopB i (LoopB j f)) =
> norm (LoopB (tupE [i, j]) (Arr shuffleE :>>> f :>>> Arr shuffleE'))
> where
> shuffleE = assocE' `o` (idE `crossE` transposeE)
> shuffleE' = (idE `crossE` transposeE) `o` assocE
> normalize norm (First (LoopB i f)) =
> norm (LoopB i (Arr juggleE :>>> First f :>>> Arr juggleE))
LoopD, Loop, and Init are translated to LoopB:
>-- normalize norm (LoopD i f) = norm (Loop (f :>>> secondA (Init i)))
>-- normalize norm (Loop f) = LoopB (Term "()") (norm (Arr assocE' :>>> First f :>>> Arr assocE))
>-- normalize norm (Init i) = LoopB i (Arr (swapE `o` juggleE `o` swapE))
LoopD laws
> normalize norm (h :>>> LoopD i f) = norm (LoopD i (First h :>>> f))
> normalize norm (LoopD i f :>>> h) = norm (LoopD i (f :>>> First h))
> normalize norm (LoopD i (LoopD j f)) =
> norm (LoopD (tupE [i, j]) (Arr assocE' :>>> f :>>> Arr assocE))
> normalize norm (First (LoopD i f)) =
> norm (LoopD i (Arr juggleE :>>> First f :>>> Arr juggleE))
Loop laws
> normalize norm (h :>>> Loop f) = norm (Loop (First h :>>> f))
> normalize norm (Loop f :>>> h) = norm (Loop (f :>>> First h))
> normalize norm (Loop (Loop f)) =
> norm (Loop (Arr assocE' :>>> f :>>> Arr assocE))
> normalize norm (First (Loop f)) =
> norm (Loop (Arr juggleE :>>> First f :>>> Arr juggleE))
Loop and LoopB
> normalize norm (Loop (LoopB i f)) =
> norm (LoopB i (Arr shuffleE :>>> f :>>> Arr shuffleE'))
> where
> shuffleE = assocE' `o` (idE `crossE` assocE)
> shuffleE' = (idE `crossE` assocE') `o` assocE
> normalize norm (LoopB i (Loop f)) =
> norm (LoopB i (Arr shuffleE :>>> f :>>> Arr shuffleE'))
> where
> shuffleE = assocE' `o` (idE `crossE` juggleE)
> shuffleE' = (idE `crossE` juggleE) `o` assocE
Loop and LoopD
> normalize norm (Loop (LoopD i f)) =
> norm (LoopB i (Arr assocE' :>>> f :>>> Arr assocE))
> normalize norm (LoopD i (Loop f)) =
> norm (LoopB i (Arr (juggleE `o` assocE') :>>> f :>>>
> Arr (assocE' `o` juggleE)))
LoopB AND LoopD
> normalize norm (LoopB i (LoopD j f)) =
> norm (LoopB (tupE [i, j]) (Arr shuffleE :>>> f :>>> Arr shuffleE'))
> where
> shuffleE = assocE' `o` (idE `crossE` assocE')
> shuffleE' = (idE `crossE` assocE) `o` assocE
> normalize norm (LoopD i (LoopB j f)) =
> norm (LoopB (tupE [i, j]) (Arr shuffleE :>>> f :>>> Arr shuffleE'))
> where
> shuffleE = transposeE `o` assocE'
> shuffleE' = assocE `o` transposeE
Init
> normalize norm (Init i) = norm (LoopD i (Arr swapE))
All the other cases remain unchanged
> normalize norm e = e
Optimized CCNF
==============
to transform loopB to loopD:
loopB i (arr f) ---> loopD i (arr g)
we must generate the function g from f:
g (x, z) = let (x', (y, z')) = f (x, (y, z))
in (x', z')
> toLoopD (LoopB i (Arr f)) = LoopD i (Arr g)
> where
> g = do
> f' <- f
> [x, y, z, x', z'] <- mapM newName ["x", "y", "z", "x'", "z'"]
> return $ LamE [TupP [VarP x, VarP z]] $ LetE
> [ValD (TupP [VarP x', TupP [VarP y, VarP z']]) (NormalB $
> AppE f' (TupE [VarE x, TupE [VarE y, VarE z]])) []]
> (TupE [VarE x', VarE z'])
> toLoopD x = x
Notice the recursively defined variable y, and it'll prevent GHC from inlining
g and f. So we must further transform f into a set of letexpressions, and
move the definition of y inside. Here is a set of transformations we do to
function g:
1. Transform function applications to letexpressions.
(\x -> e1) e2 === let x = e2 in e1
> toLet :: Exp -> Exp
> toLet = G.everywhere (G.mkT aux)
> where
> aux (AppE (LamE [pat] body) arg) = LetE [ValD pat (NormalB arg) []] body
> aux (AppE (LamE (pat:ps) body) arg) = LamE ps (LetE [ValD pat (NormalB arg) []] body)
> aux x = x
2. TODO: For every pattern match agains tuples, unfold righthandsize until it is a
tuple too, and then break up into a list of letexpressions.
Auxiliary Functions
===================
> f `o` g = appE (appE [|\f g x -> f (g x)|] f) g
> f `crossE` g = appE (appE [|\f g x -> (f $ fst x, g $ snd x)|] f) g
> idE = [|\x -> x|]
> dupE = [|\x -> (x, x)|]
> swapE = [|\x -> (snd x, fst x)|]
> curryE = [|\f x y -> f (x, y)|]
> uncurryE = [|\f x -> f (fst x) (snd x)|]
> assocE = [|\x -> (fst $ fst x, (snd $ fst x, snd x))|]
> assocE' = [|\x -> ((fst x, fst $ snd x), snd $ snd x)|]
> juggleE = assocE' `o` (idE `crossE` swapE) `o` assocE
> transposeE = [|\x -> ((fst $ fst x, fst $ snd x),
> (snd $ fst x, snd $ snd x))|]