The main program for Lambdascope

> {-# LANGUAGE DoRec,CPP #-}

> module Main where

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

> import Graphics.Rendering.OpenGL (($=), GLfloat)
> import qualified Graphics.Rendering.OpenGL as GL
> import qualified Graphics.UI.GLFW as GLFW
> import Control.Monad.Fix
> import Control.Monad (when, unless)
> import Data.IORef
> import Data.IntMap hiding (lookup, mapMaybe)
> import Data.Maybe (mapMaybe, fromMaybe)
> import Prelude hiding (map)
> import System.IO.Unsafe

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

Main Program

#ifdef _EnableGUI_
> import EnableGUI
> main = enableGUI >> do
#else
> main = do
#endif
>   GLFW.initialize
>   initWindow w h
>   showHelp <- newIORef False
>   factor <- newIORef (0, 0, 1.0)
>   netRef <- newIORef net
>   let loop handle = do 
>         (UserAction handle', render) <- handle
>         GL.clear [GL.ColorBuffer] 
>         (cx, cy, s) <- readIORef factor
>         GL.preservingMatrix (do
>           GL.translate (vector3 (cx / unit) (cy / unit) 0) 
>           GL.scale s s 1
>           render)
>         help <- readIORef showHelp 
>         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 "H toggles help, ESC quits"
>           GL.translate $ vector3 0 (-1.25) 0
>           when help $ renderText helpText)
>         GLFW.swapBuffers
>         GLFW.sleep 0.01
>         exit <- GLFW.getKey GLFW.ESC 
>         unless (exit == GLFW.Press) $ loop handle'
>   loop (handleUserAction factor (keyHandle showHelp netRef) (reduce netRef) d)
>   GLFW.closeWindow
>   GLFW.terminate
>   where
>     -- prepare an initial diagram to load
>     net = nodeToNet (mkNode (termToNode t2')) --(App cube (VInt 3))))
>     d = netToDiagram net
>     w = 800
>     h = 600

> helpText = unlines 
>   [ "CTRL+ mouse  pan"
>   , "ALT + mouse  zoom"
>   , "Left click   rotate node"
>   , "Right click  apply any rule to node"
>   , "Drag mouse   move node"
>   , "1 .. 9       load presets"
>   , "Space        auto zoom"
>   , "L  auto layout all nodes"
>   , "R  reduce to head normal form"
>   , "X  repeat outermost cross rule"
>   , "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  unwind, cross, scope, cross, loopcut, cross"
>   , "M  repeat meta rule everywhere"
>   , "P  prune all none root tree"
>   , "O  apply outermost reduction rules once"
>   , "V  print beta, meta, size couter on console"
>   , "D  zap duplicator's value (become call-by-need)"]
> 
>             
> keyHandle showHelp netRef = (fst $ unzip ks, handle)
>   where
>     -- change the following line to load different programs for 1..9
>     -- It currently loads the (opt N) lambda expression.
>     ks = [(c, load $ opt $ fromEnum c - 48) | c <- ['1'..'9']] ++ 
>          [('R', reduceAll),
>           ('X', crossAll),
>           ('B', betaAll),
>           ('E', eraseAll),
>           ('U', unwindAll),
>           ('S', scopeAll),
>           ('C', loopcutAll),
>           ('T', toTerm),
>           ('M', metaAll),
>           ('P', pruneAll),
>           ('O', outer),
>           ('V', viewCounter),
>           ('L', reLayout),
>           ('D', demoteDup),
>           ('H', \n d r -> (n, d, r))]
>     handle k d r = do
>       net <- readIORef netRef
>       when (k == 'H') $ (modifyIORef showHelp not)
>       let (net', d', r') = maybe (net, d, r) (\f -> f net d r) (lookup k ks)
>       writeIORef netRef net'
>       return (d', r')

> demoteDup net d r@((posMap, _), _) =
>   let net' = map (\a -> case a of
>          (Duplicator, cp, cv) -> (Duplicator, cp, Nothing)
>          _ -> a) net
>       d' = netToDiagram net'
>       ids = keys net'
>       posMap' = filterWithKey (\i _ -> elem i ids) posMap
>       r' = renderDiagram posMap' d'
>   in (net', d', r')

> load x n _ _ = 
>   let net = nodeToNet (mkNode (termToNode x))
>       d = netToDiagram net
>   in resetCounters n `seq` (net, d, renderDiagram empty d)

> reLayout net d r@((posMap, _), _) = (net, d, renderDiagram empty d)

activates a local rule to a node, and apply it once.

> reduce :: IORef INet -> Int -> IO ([Int], Diagram)
> reduce netRef i = do
>   net <- readIORef netRef
>   let a@(at, ap, av) = net ! i
>       (j, n) = head ap
>       b@(bt, bp, bv) = net ! j
>       net' = debug1 ("reduced from\n   " ++ show net ++ "\nto ") $ if ap == [] 
>         then error "here!" -- delete i net
>         else fromMaybe net $ localAll net (i, a) (j, b)
>       ids = keys net'
>   writeIORef netRef net'
>   return (ids, netToDiagram net')

> localAll = meta_ ->- beta_ ->- cross_ ->- erase

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 (repeatRule (outermost localAll +>+ applyRule erase_))
> crossAll   = wrapRule (repeatRule (outermost cross))
> betaAll    = wrapRule (repeatRule (applyRule beta_))
> eraseAll   = wrapRule (repeatRule (applyRule erase))
> unwindAll  = wrapRule (applyRule unwind)
> scopeAll   = wrapRule (applyRule scope)
> loopcutAll = wrapRule (applyRule loopcut)
> metaAll    = wrapRule (repeatRule (applyRule meta_))
> outer      = wrapRule (outermost localAll)
> pruneAll   = wrapRule prune

> toTerm net = 
>   let r@(net', d') = readback net
>       t = netToTerm net'
>   in debug ("toTerm=" ++ show t) $ wrapRule (const r) net

> wrapRule f net d r@((posMap, _), _)  = 
>   let (net', _) = f net
>       d' = netToDiagram net'
>       ids = keys net'
>       posMap' = filterWithKey (\i _ -> elem i ids) posMap
>       r' = renderDiagram posMap' d'
>   in (net', d', r')

Counters are hacks. Though our rules are already return the counting, 
they are not used.

> crossCounter = unsafePerformIO (newIORef 0)
> betaCounter = unsafePerformIO (newIORef 0)
> metaCounter = unsafePerformIO (newIORef 0)
> sizeTracker = unsafePerformIO (newIORef (1000000,0))

> trackSize net = unsafePerformIO $ do
>   m <- readIORef sizeTracker
>   let s = size net
>       m' = (min (fst m) s, max (snd m) s)
>   s `seq` fst m' `seq` snd m' `seq` writeIORef sizeTracker m'
>   --putStrLn $ show m'  
>   return net

> resetCounters n = unsafePerformIO $ do
>   writeIORef crossCounter 0
>   writeIORef betaCounter 0
>   writeIORef metaCounter 0
>   writeIORef sizeTracker (1000000, 0)

> viewCounter n d r = 
>   let view n c = do
>         m <- readIORef c
>         putStrLn $ n ++ " = " ++ show m
>       viewAll n = do
>         view "cross" crossCounter
>         view "beta" betaCounter
>         view "meta" metaCounter
>         view "size" sizeTracker
>   in unsafePerformIO (viewAll n) `seq` (n, d, r)

> incCounter c x y z = do
>   m <- readIORef c
>   let m' = m + 1
>   m' `seq` writeIORef c m'

> mkCounter c f x y z = 
>   let r = f x y z
>   in if r == Nothing 
>     then r
>     else unsafePerformIO (incCounter c x y z) `seq` r

> mkCounter' c f x y@(_, (t,_,_)) z@(_, (t', _, _)) = 
>   let r = f x y z
>       tup = case (t, t') of
>         (Constructor _, _) -> True
>         (_, Constructor _) -> True
>         _ -> False
>   in if r == Nothing || tup 
>     then r 
>     else unsafePerformIO (incCounter c x y z) `seq` r

Customizd beta, meta and erase rules that track statistics.

> cross_ = mkCounter crossCounter cross
> beta_ = mkCounter betaCounter beta
> meta_ = mkCounter metaCounter meta         -- don't track tuple projection
> erase_ net a b =
>   let net' = trackSize net  
>   in (trackSize net `seq`) $
>     maybe Nothing (Just . (\net -> trackSize net `seq` net)) $ 
>     erase net' a b

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

> 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 (Abs (App Z Z)) 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 :: INet
> 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 :: INet
> testL0 = fromList [
>   (0, (Eraser, [(2, 1)], Nothing)),
>   (1, (Eraser, [(2, 2)], Nothing)),
>   (2, (Duplicator, [(3, 0), (0, 0), (1, 0)], Just 0)),
>   (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]

two duplicators wiring to each other on both sides

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

for commute:

similar to testL0

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

similar to testL1

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

when a single duplicator loops its two ports

> testL4 :: INet
> testL4 = fromList [
>   (0, (Eraser, [(1, 1)], Nothing)),
>   (1, (Delimiter, [(2, 0), (0,0)], Just 0)),
>   (2, (Duplicator, [(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    453
9   644  719    539

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