The main program for Lambdascope

> {-# LANGUAGE NoMonomorphismRestriction,DoRec,CPP #-}

> module Main where

> import INet
> import Diagram hiding (S)
> import Lambda
> import Grid

> import Graphics.Rendering.OpenGL (($=), GLfloat)
> import qualified Graphics.Rendering.OpenGL as GL
> import qualified Graphics.UI.GLFW as GLFW
> import qualified Data.Map as Map
> import Control.Monad.Fix
> import Control.Monad.Task
> import Graphics.UI.GLFW.Task
> import Control.Monad.IO.Class
> import Control.Monad.Trans
> import Control.Monad.Trans.State
> import Control.Monad.Identity
> import Control.Monad 
> import Data.IORef
> import qualified Data.Set as Set
> import qualified Data.IntMap as IntMap
> import Data.IntMap hiding (null, lookup, mapMaybe, map)
> import Data.Maybe (mapMaybe, fromMaybe)
> import Control.Arrow (first, second)
> import Data.List (intercalate, sort)

An interactive net is a mapping from node IDs to their connected (node ID,
port No) pairs.

> type Clicks = Map.Map String Int 

> data MainState 
>   = MS { showHelp :: Bool                         -- whether to display help message 
>        , inet     :: INet                         -- current INet being displayed 
>        , frame    :: Frame                        -- single frame of display (for animation)
>        , hlset    :: Maybe ([(Int, Int)], HLSet)  -- wires to highlight
>        , backup   :: [(INet, GridMap Direction, Clicks)]  -- backups for undo/rollback
>        , clicks   :: Clicks                       -- collection of statistics
>        , preset   :: Int                          -- next preset to load
>        , title    :: String                       -- title of current inet
>        }
> initState net = MS False net emptyFrame Nothing [] Map.empty 0 ""

> lift3 = lift . lift . lift
> toggleShowHelp = lift3 $ modify $ \s -> s { showHelp = not (showHelp s) }
> getShowHelp = lift3 $ get >>= return . showHelp

> modifyTitle f = lift3 $ modify $ \s -> s { title = f (title s) }
> getTitle = lift3 $ get >>= return . title
> setTitle = modifyTitle . const

> modifyINet f  = lift3 $ modify $ \s -> s { inet = f (inet s) }
> setINet = modifyINet . const
> getINet = lift3 $ get >>= return . inet

> modifyFrame f = lift3 $ modify $ \s -> s { frame = f (frame s) }
> setFrame = modifyFrame . const
> getFrame = lift3 $ get >>= return . frame

> snapshot = do
>   grid <- lift $ getGrid
>   lift3 $ modify $ \s -> s { backup = take 10 $ (inet s, grid, clicks s) : backup s }
> rollback = do
>    grid <- lift3 $ do
>      b <- fmap backup get
>      case b of
>        [] -> return Nothing
>        (i, g, c) : bs -> modify (\s -> s { inet = i, clicks = c, backup = bs }) >> return (Just g)
>    maybe (return False) (\g -> lift (setGrid g) >> return True) grid

> click name f = lift3 $ modify $ \s -> s { clicks = click' (clicks s) }
>   where click' m = maybe (inc 0) inc $ Map.lookup name m 
>           where inc x = Map.insert name (f x) m
> resetClicks = lift3 $ modify $ \s -> s { clicks = Map.empty }
> getClicks = do
>   m <- lift3 $ get >>= return . clicks
>   return $ intercalate ", " $ map (\(x, y) -> x ++ " " ++ show y) $ Map.toList m

> renderINet = getINet >>= setDiagram . netToDiagram

> loadPreset f = do
>    i <- lift3 $ get >>= return . preset
>    lift3 $ modify $ \s -> s { preset = f i, backup = [], clicks = Map.empty }
>    let (title, inet) = presetINet (f i)
>    setTitle title
>    setINet inet
>    lift clearGrid 
>    setDirty Dirty
>    renderINet 
>    autoAdjust

Main Program

#ifdef _EnableGUI_
> import EnableGUI
> main = enableGUI >> do
#else
> main = do
#endif
>   GLFW.initialize
>   dState <- initWindow w h
>   evalStateT (evalStateT (evalGridT_ (runTask start) margin) dState) (initState emptyINet)
>   GLFW.closeWindow
>   GLFW.terminate
>   where
>     -- prepare an initial diagram to load
>     -- net = nodeToNet $ mkNode . termToNode $ App cube (VInt 3) -- (termToNode t4)) -- (App cube (VInt 3))))
>     w = 800
>     h = 600
>     start = do
>       loadPreset id
>       renderINet
>       waitForEvents <- liftIO registerTaskCallbacks
>       setupEvents $ (snapshot >>) . reduce
>       fork $ forever $ watch (onKey >=> isPress >=> isKey 'H') >> toggleShowHelp >> setDirty Lightly
>       fork $ forever $ watch (onKey >=> isPress >=> isKey 'L') >> snapshot >> lift clearGrid >> setDirty Dirty
>       fork $ forever $ watch (onKey >=> isPress >=> isKey '[') >> loadPreset (\x -> x - 1) 
>       fork $ forever $ watch (onKey >=> isPress >=> isKey ']') >> loadPreset (+1)
>       fork $ forever $ watch (onKey >=> isPress >=> isKey GLFW.BACKSPACE) >>
>                        rollback >> renderINet >> setDirty Dirty
>       mapM_ (\(c, f) -> fork $ forever $ watch (onKey >=> isPress >=> isKey c) >> snapshot >> getINet >>= f >>= setINet >>
>                         renderINet >> setDirty Dirty)
>          [('R', reduceAll),
>           ('Y', resetAll),
>           ('X', crossAll),
>           ('B', betaAll),
>           ('E', eraseAll),
>           ('U', unwindAll),
>           ('S', scopeAll),
>           ('C', loopcutAll),
>           ('T', toTerm),
>           ('M', metaAll),
>           -- ('P', pruneAll),
>           ('O', outer), 
>           ('Q', outerRed), 
>           ('A', outerRedAll), 
>           ('D', demoteDup) ]
>       forever $ do
>         waitForEvents
>         whenDirty renderAll
>         setDirty None
>       where
>         renderAll = do
>           title <- getTitle
>           font <- getFont
>           stats <- getClicks
>           renderS <- fmap (renderScene font) getFactor 
>           renderH <- fmap (renderHelp font ("INet for (" ++ title ++ ") " ++ stats)) getShowHelp 
>           oldFrame <- getFrame
>           newFrame <- getDiagram >>= renderDiagram 
>           setFrame newFrame
>           d <- getDirty 
>           if d < Dirty
>             then liftIO (clearAll >> renderS newFrame >> renderH)
>             else do
>               let f = betweenFrame oldFrame newFrame
>               t0 <- liftIO $ GL.get GLFW.time 
>               let dur = 0.5
>                   animate t | t >= t0 + dur = return ()
>                             | otherwise = do
>                     t <- liftIO $ GL.get GLFW.time 
>                     let p = realToFrac (t - t0) / dur
>                         g = f (if p > 1 then 1 else p)
>                     liftIO (clearAll >> renderS g >> renderH)
>                     animate t 
>               fork $ animate t0 
>         clearAll = GL.clear [GL.ColorBuffer] 
>         renderScene font (cx, cy, s) f = GL.preservingMatrix (do
>           GL.translate (vector3 (realToFrac (cx / unit)) (realToFrac (cy / unit)) 0) 
>           GL.scale (realToFrac s) (realToFrac s) (1 :: GL.GLfloat)
>           renderFrame font Set.empty f)
>         renderHelp font tagline help = do
>           GL.Size w h <- GL.get GLFW.windowSize 
>           GL.preservingMatrix (do
>               GL.color $ color3 0.2 0.3 0.8
>               GL.translate (vector3 (- fromIntegral w / unit' / 2) (fromIntegral h / unit' / 2 - 1.25) 0)
>               GL.scale 0.8 0.8 (1::GLfloat)
>               renderString font ("H toggles help, ESC quits. " ++ tagline)
>               GL.translate $ vector3 0 (-1.25) 0
>               when help $ renderText font helpText)
>           GLFW.swapBuffers

> helpText = unlines 
>   [ -- "CTRL+ mouse  pan"
>     -- , "ALT + mouse  zoom"
>     "Left click   apply any rule to node"
>   , "Drag mouse   move node"
>   , "[  or  ]     load presets"
>   , "Space        auto zoom"
>   , "BackSpace    rollback one step (max 10)"
>   , "L  auto layout all nodes"
>   , "R  reduce to head normal form"
>   , "X  repeat cross rule everywhere"
>   , "B  repeat beta rule everywhere"
>   , "E  repeat erase rule everywhere"
>   , "U  apply unwind rule everywhere"
>   , "S  apply scope rule everywhere"
>   , "C  apply loopcut rule everywhere"
>   , "T  print term from net (after loopcut)"
>   , "M  repeat meta rule everywhere"
>   -- , "P  prune all none root tree" -- temporarily disable prune since it is not implemented correctly
>   , "O  outermost reduction once"
>   , "Q  outermost reduction once (also goes under lambda)"
>   , "A  repeat outermost reduction (also goes under lambda)"
>   , "D  zap duplicator's value (become call-by-need)"]
> 
> presetINet i = (title, node)
>   where
>     (title, node) = inets !! (i `mod` n)
>     n = length inets
>     inets 
>       = [ ("test0", (testL0, 4))
>         , ("trace0", cleanup $ nodeToNet $ mkNode $ termToNode (trace juggle))
>         -- , ("ccaE", cleanup $ nodeToNet $ mkNode $ termToNode ccaE)
>         , ("map2", nodeToNet $ mkNode $ termToNode map2)
>         , ("exp",  cleanup $ nodeToNet $ mkNode $ termToNode e)
>         , ("test1", (testL1, 4))
>         , ("test2", (testL2, 4))
>         , ("test3", (testL3, 4))
>         , ("test4", (testL4, 4))
>         ] ++ map (second (nodeToNet . mkNode))
>         [ ("2", termToNode t2)
>         , ("2 2", termToNode t4)
>         , ("opt 1", termToNode (opt 1))
>         , ("opt 2", termToNode (opt 2))
>         , ("opt 3", termToNode (opt 3))
>         , ("one", termToNode one)
>         -- , ("(\\x.x) x", termToNode (App (Abs Z) (VStr "x")))
>         -- , ("cube 3", termToNode $ App cube (VInt 3))
>         ]

> cleanup = fst . runIdentity . repeatRule (applyRule (ruleM erase)) 


> demoteDup = return . first (IntMap.map demote)
>   where 
>      demote a = case a of
>                   (Duplicator _, cp, cv) -> (Duplicator (Sup False), cp, cv)
>                   _ -> a

> reLayout net d = (net, d)

activates a local rule to a node, and apply it once.
This will also revive dormant Cycle. 

> -- reduce :: Int -> IO ([Int], Diagram)
> reduce i = do
>   -- traceShow ("NID", i)
>   net@(netMap, _) <- getINet
>   let a@(at, ap, av) = revive (netMap ! i)
>       (j, n) = head ap
>       b@(bt, bp, bv) = revive (netMap ! j)
>   when (ap == []) $ error "here!" -- delete i net
>   net' <- localAll (i, a) (j, b) net >>= return . fromMaybe net 
>   -- traceShow ("reduced", net, net') 
>   setINet net'
>   renderINet
>   where
>     revive (Duplicator (Cycle _), ap, v) = (Duplicator (Cycle True), ap, v)
>     revive x = x


> localAll = meta_ ->- beta_ ->- cross_ ->- erase_ -- ->- share_

Note that in optimal reduction, the erase is a global rule rather than an 
outermost one because it'll otherwise results in redudant beta or meta 
reduction.

> reduceAll  = wrapRule (applyRule (ruleM resetCycle) +&+ 
>                        repeatRule (applyRule meta_) +&+ 
>                        repeatRule (applyRule beta_) +&+ 
>                        repeatRule (applyRule cross_) +&+ 
>                        repeatRule (applyRule erase_))
> resetAll   = wrapRule (applyRule (ruleM resetCycle))
> crossAll   = wrapRule (applyRule cross_)
> betaAll    = wrapRule (applyRule beta_)
> eraseAll   = wrapRule (applyRule erase_)
> metaAll    = wrapRule (applyRule meta_)
> unwindAll  = wrapRule (applyRule unwind_)
> scopeAll   = wrapRule (applyRule scope_)
> loopcutAll = wrapRule (applyRule loopcut_)
> outer      = wrapRule (outermost localAll)
> outerRed   = wrapRule (outerReducible localAll)
> outerRedAll = wrapRule (repeatRule (outerReducible localAll))
> pruneAll   = wrapRule (return . prune)

> readbackM = 
>   applyRule unwind_  >=> return . fst >=> 
>   applyRule scope_   >=> return . fst >=>
>   wrapRule (repeatRule (applyRule cross_)) >=>
>   applyRule loopcut_ >=> return . fst >=>
>   wrapRule (repeatRule (applyRule cross_)) 

> toTerm net = do
>   net' <- readbackM net
>   let t = netToTerm net'
>   liftIO $ putStrLn ("toTerm = " ++ show t) 
>   return net'

> wrapRule f net = fmap fst (f net) 

Rules with click counters.

> cross_   = wrapClick "cross"   cross
> beta_    = wrapClick "beta"    beta
> meta_    = wrapClick "meta"    meta
> erase_   = wrapClick "erase"   erase
> unwind_  = wrapClick "unwind"  unwind
> scope_   = wrapClick "scope"   scope
> loopcut_ = wrapClick "loopcut" loopcut
> -- share_   = wrapClick "share"   share
> wrapClick counter r a b c = do
>   n <- ruleM r a b c
>   click counter (maybe id (\_ -> (+1)) n)
>   return n

Testing
=======

We can compose INet nodes by wiring them

> two s = do
>   rec a <- abstractor s b e
>       b <- abstractor a c m
>       c <- applicator d f b
>       d <- delimiter  e c 0
>       e <- duplicator a k d 0
>       f <- applicator g l c
>       g <- delimiter  k f 0
>       h <- eraser     m
>       i <- eraser     l
>       j <- eraser     k
>       k <- duplicator e g j 0
>       l <- duplicator m i f 0
>       m <- duplicator b l h 0
>   return a

> four = do
>   rec s <- initiator a
>       a <- applicator b b s
>       b <- duplicator t a a 0
>       t <- two b
>   return s

or we can write a Generalized Lambda term, and convert it to INet.

> x = VStr "x"
> f = Abs (VFunc 1 "f" Z)
> g = Abs (VFunc 1 "g" Z)

> t2 = church 2
> t2' = App (App (church 2) f) x --App (App (Abs (Abs (App (S Z) (App (S Z) Z))))  f) x

> t4 = App t2 t2
> t4' = App (App t4 f) x

> church n = Abs (Abs (app n (S Z) Z))

> app 0 f x = x
> app n f x = App f (app (n - 1) f x)

> double = Abs (App (VFunc 2 "+" (App id Z)) Z)
>   where id = Abs Z

> testDouble n = app n double (VInt 1)

Test substitution

> testSub = App f (VInt 7)
>   where
>     s = Abs (App (VFunc 2 "*" Z) Z)
>     f = Abs (App (Abs (App (VFunc 2 ":" Z) (App (VFunc 2 "*" Z) (S Z)))) 
>                  (App (VFunc 2 "*" Z) Z))

Test for meta level fuction with arity

> d1 = App (Abs (App (VFunc 2 "g" Z) Z)) t2'

Test for handling disconnected graph, rather than tree

> test = fromList [
>   (0, (Eraser, [(1, 0)], Nothing)),
>   (1, (Eraser, [(0, 0)], Nothing)),
>   (2, (Eraser, [(3, 0)], Nothing)),
>   (3, (Eraser, [(2, 0)], Nothing)) ]

Test for tuples

> p0 = App (Abs (Fst Z)) (Tup t0 t1)
> t0 = Abs (Abs Z)
> t1 = Abs (Abs (App (S Z) Z))

> ones = Y (Abs (Tup (VInt 1) Z))
> one = Fst ones

Tests for cross rule with self-loop

for annihilate:

two duplicators wiring to each other on one side

> testL0 = fromList [
>   (0, (Eraser, [(2, 1)], Nothing)),
>   (1, (Eraser, [(3, 2)], Nothing)),
>   (2, (Delimiter, [(3, 1), (0, 0)], Just 0)),
>   (3, (Duplicator Dup, [(4, 0), (2, 0), (1, 0)], Just 0)),
>   (4, (Duplicator Dup, [(3, 0), (4, 2), (4, 1)], Just 0))]

two duplicators wiring to each other on both sides

> testL1 = fromList [
>   (2, (Duplicator Dup, [(3, 0), (2, 2), (2, 1)], Just 0)),
>   (3, (Duplicator Dup, [(2, 0), (3, 2), (3, 1)], Just 0))]

for commute:

similar to testL0

> testL2 = fromList [
>   (0, (Eraser, [(2, 1)], Nothing)),
>   (1, (Eraser, [(2, 2)], Nothing)),
>   (2, (Duplicator Dup, [(3, 0), (0, 0), (1, 0)], Just 1)),
>   (3, (Duplicator Dup, [(2, 0), (3, 2), (3, 1)], Just 0))]

similar to testL1

> testL3 = fromList [
>   (2, (Duplicator Dup, [(3, 0), (2, 2), (2, 1)], Just 1)),
>   (3, (Duplicator Dup, [(2, 0), (3, 2), (3, 1)], Just 0))]

when a single duplicator loops its two ports

> testL4 = fromList [
>   (0, (Eraser, [(1, 1)], Nothing)),
>   (1, (Delimiter, [(2, 0), (0,0)], Just 0)),
>   (2, (Duplicator Dup, [(1, 0), (2, 2), (2, 1)], Just 0))]

These are tests for optimality. With church numbers, (n 2 i x)
takes exponential time in call-by-need, but only linear to n
in optimal reduction.

> i = Abs Z

> opt n = App (App (App (church n) (church 2)) i) i

Chart for opt 1 .. 7

Optimal 
cross, beta, size(min, max)

47 6 (2, 27)
84 9 (2, 40)
128 12 (2, 54)
179 15 (2, 69)
237 18 (2, 85)
302 21 (2, 102)
374 24 (2, 120)

Lazy
beta, size(min, max)

6 (2, 14)
11 (2, 18)
20 (2, 32)
37 (2, 52)
70 (2, 84)
135 (2, 152)
264 (2, 284)
392

Compare Lazy, Completely Lazy (M. J. Thyer's thesis: http://thyer.name/phd-thesis/)
and Optimal using number of beta reduction, steps, interactions (excluding garbage
collection) as metrics respectively.

n   Lazy C.Lazy Optimal
--------------------------
1   6    8      53
2   11   15     93
3   20   25     140
4   37   40     194
5   70   66     255
6   135  114    323
7   264  204    398
8   392  377    480
9   644  719    569

It's easy to tell that they are of O(n * 2^n), O(n^7) and O(n^2)
respectively. It's also worth mentioning that if we only count the number of
betas, optimal is O(n), and completely lazy is O(n^3), lazy is O(n^4).


Test for integral function
==========================

integral i x = (i, \dt -> integral (next dt i (fst x)) (snd x dt))

also make tuple construction involve beta reduction.

> tup x y = App (App (Abs (Abs (Tup (S Z) Z))) x) y

> next = VFunc 3 "next"
> integral = 
>   Y (Abs                                        -- \integral ->
>       (Abs                                      -- \i ->
>         (Abs                                    -- \s ->
>           (tup (S Z)                            -- i, 
>                 (Abs                            -- \dt ->
>                    (App (App (S (S (S Z)))      -- integral 
>                      (App (App (next Z)         -- next dt 
>                        (S (S Z)))               -- i
>                        (Fst (S Z))))            -- fst x
>                      (App (Snd (S Z)) Z)))))))  -- snd x dt

> e = Y (App integral (VInt 1)) -- (1, \dt -> (next dt 1 1, snd e))
> unfold = Abs (App (Snd Z) (VStr "dt"))
> expN n = Fst (app n unfold e)

Chart of computing expN 1 to expN 7

Optimal

cross, beta, meta (total, include projection), meta (arith), size (min, max)

199  11 6   3 (41, 104)
472  16 12  6 (44, 155)
820  21 18  9 (47, 211)
1254 26 24 12 (50, 272)
1818 31 30 15 (53, 338)
2570 36 36 18 (56, 409)
3580 41 42 21 (59, 485)

Call-by-need

 13  3 (41, 134)
 28  9 (44, 277)
 50 18 (47, 516)
 79 30 (50, 843)
115 45 (53, 1267)
158 63 (56, 2800)
208 84 (59, 2454)

It indeed shows that call-by-need incurs recomputation at the meta
arithmetic level:

  cbn(n) = optimal(n) + cbn(n - 1)

Tests for traversing circular structure using cursor.

A cursor is a tuple

 Data Cursor a = (a, List a -> List a)

List is nested tuple, a circular structure

 Data List a = (a, List a)

> c1 = tup (VInt 1) (Abs Z)                               -- c1 = (1, \x -> (2, (3, x)))
> c2 = tup (VInt 1) (Abs (tup (VInt 2) Z))                -- c2 = (1, \x -> (2, (3, x)))
> c3 = tup (VInt 1) (Abs (tup (VInt 2) (tup (VInt 3) Z))) -- c3 = (1, \x -> (2, (3, x)))

 adv (Cursor u@(Elem i v) f) =
   let f' x = next (f (Cons u x))
       u' = this (fix (f . Cons u))
   in Cursor u' f'

(u', f'

> nextc = 
>   Abs
>    (tup 
>      (Fst (Y (Abs (App (Snd (S Z)) (tup (Fst (S Z)) Z)))))
>      (Abs (Snd (App (Snd (S Z)) (tup (Fst (S Z)) Z))))
>      )

> c n = Fst (app n nextc c2)

3 0 (31, 50)
5 0 (53, 93)
7 0 (77,130)
11 0 (..)
13 
15
19

9 3
15 5
21 8
29 12
35 14
41 17
49 21

9 3
15 6
23 10
29 13
37 17
43 20
51 24

9 3
15 6
25 10
34 15
47 21
59 28
75 36

Power Cube Example
==================

> cons x xs = App (VFunc 2 ":" x) xs
> cond c t f = App (App (VFunc 3 "cond" c) t) f
> eq x y = App (VFunc 2 "==" x) y
> times x y = App (VFunc 2 "*" x) y
> minus x y = App (VFunc 2 "-" x) y
> power = Y (Abs (Abs (Abs (
>           cond (eq (S Z) (VInt 1)) 
>                (VInt 1)
>                (times Z (App (S (S Z)) (minus (S Z) (VInt 1))))))))
> cube = App power (VInt 3)
> powerCube = cons power (cons cube (App cube (VInt 5)))

CCA Integral of Exp Example
===========================

GHC cannot give the most optimized result for the following expression:

    trace (juggle .  ((dup .  snd) `cross`  id) .  (swap `cross` id) . juggle . 
           ((((+1) `cross`  id) .  trace (juggle .  (dup `cross`  id) .  swap .  
           (acc `cross`  id) .  juggle)) `cross`  id) .  juggle .  
           (swap `cross`  id) .  juggle)

    trace f x = let (y, z) = f (x, z) in y
    juggle ((x, y), z) = ((x, z), y)
    cross f g (x, y) = (f x, g y)
    acc (x, i) = i + dt * x
    assoc ((x,y),z) = (x,(y,z))
    unassoc (x,(y,z)) = ((x,y),z)

    trace f x = let g z = snd (f (x, z))
                in fst (f (x, (fix g)))

> trace = App $ Abs $ Abs $ Fst $ App (S Z) (Tup Z (Y (Abs $ Snd $ App (S (S Z)) (Tup (S Z) Z))))
> plus x y = App (VFunc 2 "+" x) y
> juggle = Abs $ Tup (Tup (Fst (Fst Z)) (Snd Z)) (Snd (Fst Z))
> across f g = Abs $ Tup (App f (Fst Z)) (App g (Snd Z))
> acc = Abs $ plus (Snd Z) (times (VStr "dt") (Fst Z))
> assoc = Abs $ Tup (Fst (Fst Z)) (Tup (Snd (Fst Z)) (Snd Z))
> unassoc = Abs $ Tup (Tup (Fst Z) (Fst (Snd Z))) (Snd (Snd Z))
> dup = Abs $ Tup Z Z
> f `dot` g = App (App (Abs $ Abs $ Abs $ App (S (S Z)) (App (S Z) Z)) f) g

> cca0 = assoc `dot` unassoc
> ccaE = trace (juggle `dot` 
>        ((dup `dot` snd) `across` id) `dot`
>        (swap `across` id) `dot` juggle `dot`
>        ((((Abs $ plus Z (VInt 1)) `across` id) `dot`  
>        trace (juggle `dot` (dup `across` id) `dot` swap `dot`
>              (acc `across` id) `dot` juggle)) `across` id) `dot` 
>        juggle `dot` (swap `across` id) `dot` juggle)
> {-
> ccaE = trace
>        (juggle `dot` (dup `across` id) `dot` swap `dot`
>              (acc `across` id) `dot` juggle)
> -}
>   where
>     snd = Abs $ Snd Z
>     id = Abs Z
>     swap = Abs (Tup (Snd Z) (Fst Z))

toTerm = Abs (Tup (App (VFunc 2 "+" (Snd Z)) (VInt 1)) (App (VFunc 2 "+" (Snd Z)) (App (VFunc 1 "(* dt)" (VFunc 2 "+" (Snd Z))) (VInt 1))))

f (a, b) = (1 + b, dt * b + 1)
f (a, b) = (1 + b, b + dt * (1 + b))

Map Fusion
==========

   map f (x,y) = (f x, map f y)

> map' = Y $ Abs $ Abs $ Abs $ Tup (App (S Z) (Fst Z)) (App (App (S (S Z)) (S Z)) (Snd Z))
> map2 = App (Abs (App Z f `dot` App Z g)) map'
> map2' = App map' (f `dot` g)

(map f . map g) (x, y) = ((f . g) x, (map f ((map g) y)))

(map f . map g) = Y F 
  where F h (x, y) = ((f.g) x, h y)