LambdaINet (empty) → 0.1.0
raw patch · 9 files changed
+2088/−0 lines, 9 filesdep +GLFWdep +OpenGLdep +basesetup-changedbinary-added
Dependencies added: GLFW, OpenGL, base, containers, mtl
Files
- LICENSE +20/−0
- LambdaINet.cabal +26/−0
- README +57/−0
- Setup.hs +6/−0
- data/font.tga binary
- src/Diagram.lhs +734/−0
- src/INet.lhs +479/−0
- src/Lambda.lhs +214/−0
- src/Main.lhs +552/−0
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2009 Paul H. Liu <paul@thev.net>++This software is provided 'as-is', without any express or implied+warranty. In no event will the authors be held liable for any damages+arising from the use of this software.++Permission is granted to anyone to use this software for any purpose,+including commercial applications, and to alter it and redistribute it+freely, subject to the following restrictions:++1. The origin of this software must not be misrepresented; you must not+ claim that you wrote the original software. If you use this software+ in a product, an acknowledgment in the product documentation would+ be appreciated but is not required.++2. Altered source versions must be plainly marked as such, and must not+ be misrepresented as being the original software.++3. This notice may not be removed or altered from any source+ distribution.
+ LambdaINet.cabal view
@@ -0,0 +1,26 @@+name: LambdaINet+version: 0.1.0+homepage: not available+maintainer: Paul H. Liu <paul@thev.net>+cabal-version: >= 1.6+build-type: Simple+category: Application+synopsis: Graphical Interaction Net Evaluator for Optimal Evaluation+description: An experimental evaluator for Interaction Nets that encodes+ optimal and call-by-need stragtegies based on Lambdascope, with+ an interactive graphical interface based on OpenGL and GLFW.+ See the README in source for more information.+license: BSD3+license-file: LICENSE+extra-source-files:+ README++data-dir: data+data-files: font.tga++executable LambdaINet+ Main-is: Main.lhs+ Other-Modules: Diagram INet Lambda+ Build-Depends: base >= 3 && < 5, OpenGL, GLFW, containers, mtl+ Hs-Source-Dirs: src+
+ README view
@@ -0,0 +1,57 @@+LambdaINet+==========++LambdaINet implements an interaction net based optimal evaluator following+Lambdascope [1], with an interactive graphical interface allowing user to view+and directly manipulate interaction net.++[1] Vincent van Oostrom, Kees-Jan van de Looij, Marijn Zwitserlood,+Lambdascope, Workshop on Algebra and Logic on Programming Systems (ALPS),+Kyoto, April 10th 2004+++USAGE+=====++After "cabal install", just type "LambdaINet" to start the application. Once+it starts, press H for help, and ESC to quit. To understand all the operations+in detail, you'll have to read the above mentioned paper by Oostrom et. al.++Currently there is no way to load input programs except modifying the source,+Try src/Main.lhs if you want to change the start-up program, or any of the +1..9 preset programs.++At this moment, the object language supports lambda expression with recursion,+tuples, and primitives such as numbers, strings and functions. ++SIDE NOTE+=========++The bulk of code was put together in two weeks when I was working on the leak+problem for FRP in 2007. So it was really a rushed job with no guarantee of+correctness, although I tried to stay faithful to the original paper as much as+I could. ++I only did some moderate clean-ups before releasing this application to public,+and the code itself was sparingly documented when it was originally written.+Some parts are probably still buggy, like the translation from net to term;+other parts could use more improvements, like the node positioning and line+layout algorithm. But I decide to release it anyway -- maybe some people some+where will find it useful.+++DEVELOPMENT+===========++Please forward bug reports or feedbacks to me (Paul Liu at paul@thev.net), but+don't hold your hope high on timely bug fixes. ++Help is also needed to develop LambdaINet further, for example, it really needs+a way to read lambda expressions from a separate file or standard input, which+should be a simple feature to add, but alas! I don't have the time in the+nearest future to do this kind of things myself.+++----+Last Modified: Mon Sep 14 EDT 2009 by Paul Liu+
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main (main) where++import Distribution.Simple (defaultMain)++main :: IO ()+main = defaultMain
+ data/font.tga view
binary file changed (absent → 56190 bytes)
+ src/Diagram.lhs view
@@ -0,0 +1,734 @@+A graphical interface for showing the Diagram.++A Diagram consists of Atoms, which are connected to each other via ports. Each+port has an orientation (N.E.W.S. directions), which decides the direction+of the line that connects it.++Everything is aligned on a grid with a unit scale.++> module Diagram where++> import qualified Graphics.UI.GLFW as GLFW+> import qualified Graphics.Rendering.OpenGL as GL+> import Graphics.Rendering.OpenGL (($=), GLclampf, GLfloat)++> import Data.IntMap as IntMap hiding (filter, map)+> import qualified Data.Set as Set +> import Data.IORef+> import Data.Maybe (fromMaybe, fromJust)++> import System.IO.Unsafe++> import Data.Bits ( (.&.) )+> import Foreign ( withArray )+> import Paths_LambdaINet (getDataFileName)++debugger ++> debug = seq . unsafePerformIO . (putStrLn $!!)+> debug1 s v = seq (unsafePerformIO $ putStrLn $!! (s ++ show v)) v+> ($!!) f s = seq (length s) (f s)++> data Atom = Atom { +> atomID :: Int,+> atomLabel :: String,+> atomPorts :: [Port],+> atomSize :: Size,+> atomDraw :: IO () -- drawing procedure+> }++> instance Eq Atom where+> a == b = atomID a == atomID b++> instance Show Atom where+> show a = "(id=" ++ show (atomID a) ++ ", label=" ++ atomLabel a +++> ", ports=" ++ show (atomPorts a) ++ ", size=" ++ +> show (atomSize a) ++ ")"++> data Port = Port {+> owner :: Atom,+> portEnd :: Port,+> portDir :: Direction,+> portPos :: Position -- relative to the atom's center+> }++> instance Eq Port where+> p == q = (owner p == owner q) && (portPos p == portPos q)++> instance Show Port where+> show p = "(" ++ show (atomID (owner p)) ++ "-" ++ +> show (atomID (owner (portEnd p))) +++> ", dir=" ++ show (portDir p) ++ ")"++> portdir' d p = +> let a = owner p+> in toEnum ((fromEnum (portDir p) + fromEnum d) `mod` 4)+>+> portdir posMap p = +> let a = owner p+> d = maybe N snd (IntMap.lookup (atomID a) posMap)+> in portdir' d p+>+> portpos' dir (x, y) = +> let r = sqrt $ fromIntegral (x * x + y * y)+> t = asin (fromIntegral y / r)+> t1 = if x < 0 then pi - t else t+> in case dir of+> N -> (x, y)+> W -> vec r (t1 + pi / 2)+> S -> vec r (t1 + pi)+> E -> vec r (t1 - pi / 2)+> where +> vec r t = (round (r * cos t), round (r * sin t))++> portpos posMap p = +> let a = owner p+> d = maybe N snd (IntMap.lookup (atomID a) posMap)+> in portpos' d (portPos p)++> type Position = (Int, Int)+> type Positions = IntMap (Position, Direction)+> type Size = (Int, Int) -- radius in X and Y direction++> data Direction = N | W | S | E deriving (Show, Eq, Enum, Ord)++A graph consists of isolated components, which has a starting Atom.++> data Diagram = Diagram { +> startAtoms :: [Atom],+> allAtoms :: IntMap Atom+> } deriving (Eq, Show)++A grid is a set containing all occupied positions.++> type Grid = Set.Set Position++> occupied :: Grid -> Position -> Size -> Bool+> occupied grid (x, y) (w, h) = +> any (flip Set.member grid) [(x + i, y + j) | i <- [-(w + margin) .. (w + margin)], j <- [-(h + margin) .. (h + margin)]]++> occupy :: Grid -> Position -> Size -> Grid+> occupy grid (x, y) (w, h) = +> foldr Set.insert grid +> [(x + i, y + j) | i <- [-w .. w], j <- [-h .. h]]++> position :: Grid -> Position -> Position -> Size -> Position+> position grid (x, y) (dx, dy) (w, h) = +> if occupied grid (x, y) (w, h) +> then position grid (x + dx * margin, y + dy * margin) (dx, dy) (w, h)+> else (x, y)++The layout process maintains a list of ports to be checked, and+for each port:++ 1. check its direction;++ 2. if its connecting Atom is not layed out, put it along+ the port direction such that it doesn't overlap with anything.++ 3. put those unchecked ports of the connected Atom in the list;++ 4 repeat until nothing's left.++> layout :: [Int] -> (Positions, Grid) -> [Port] -> +> (Positions, Grid)+> layout visited sol [] = sol+> layout visited (posMap, grid) (p:ps) = +> let a = owner p+> i = atomID a+> ((x, y), _) = posMap ! i+> q = portEnd p+> b = owner q+> j = atomID b+> d = maybe (autorotate (portdir posMap p) (portdir' N q)) snd +> (IntMap.lookup j posMap)+> (xd, yd, dx, dy) = placement (portdir posMap p) (portdir' d q)+> (portpos posMap p) (portpos' d (portPos q))+> (aw, ah) = atomSize a+> (bw, bh) = atomSize b+> pos = position grid (x + xd * (aw + bw + margin) + dx, +> y + yd * (ah + bh + margin) + dy) (xd, yd) (bw, bh)+> rs = filter (/= q) (atomPorts b)+> posMap' = insert j (pos, d) posMap +> in if elem j visited+> then layout visited (posMap, grid) ps+> else case IntMap.lookup j posMap of+> Just (pos, _) -> layout (atomID a : visited) (posMap, occupy grid pos (bw, bh)) (rs ++ ps)+> Nothing -> layout (atomID a : visited) (posMap', occupy grid pos (bw, bh)) (rs ++ ps)++The placement returns the relative position and adjustment according to the+line directions.++> placement N N (x1, y1) (x2, y2) = (signum x1, -1, x1 - x2, y1 - y2)+> placement N S (x1, y1) (x2, y2) = (signum x1, 1, x1 - x2, 0)+> placement S S (x1, y1) (x2, y2) = (signum x1, 1, x1 - x2, y1 - y2)+> placement S N (x1, y1) (x2, y2) = (signum x1, -1, x1 - x2, 0)+> placement E E (x1, y1) (x2, y2) = (-1, signum y1, x1 - x2, y1 - y2)+> placement E W (x1, y1) (x2, y2) = ( 1, signum y1, 0, y1 - y2)+> placement W W (x1, y1) (x2, y2) = ( 1, signum y1, x1 - x2, y1 - y2)+> placement W E (x1, y1) (x2, y2) = (-1, signum y1, 0, y1 - y2)+> placement _ _ _ _ = error "impossible placement: direction not match!"++The autorotate function returns a rotation (with respect to N) such that the+second direction would meet the first one head to head.++> autorotate N N = S+> autorotate N E = E+> autorotate N W = W+> autorotate N S = N+> autorotate E N = W+> autorotate E E = S+> autorotate E W = N+> autorotate E S = E+> autorotate W N = E+> autorotate W E = N+> autorotate W W = S+> autorotate W S = W+> autorotate S N = N+> autorotate S E = W+> autorotate S W = E+> autorotate S S = S++> margin = 2+> unit = 12 :: GLfloat -- grid unit is 10 pixel++> showDiagram = undefined++> initWindow w h = do+> let row = realToFrac h / unit / 2+> col = realToFrac w / unit / 2+> writeIORef rowcolRef (row, col)+> GLFW.openWindow (GL.Size w h) [GLFW.DisplayAlphaBits 8] GLFW.Window+> GLFW.windowTitle $= "Diagram"+> GL.clearColor $= clearcolor+> GL.shadeModel $= GL.Smooth+> -- enable antialiasing+> GL.lineSmooth $= GL.Enabled+> GL.blend $= GL.Enabled+> GL.blendFunc $= (GL.SrcAlpha, GL.OneMinusSrcAlpha)+> GL.lineWidth $= 1.5+> -- load font+> font <- loadFont+> writeIORef fontRef (Just font) +> GLFW.windowSizeCallback $= reshape++too troublesome to carry this around, so make it IORef!++> fontRef = unsafePerformIO (newIORef Nothing)+> rowcolRef = unsafePerformIO (newIORef (0, 0))++> reshape (GL.Size w h) = do+> GL.viewport $= (GL.Position 0 0, GL.Size (fromIntegral w) (fromIntegral h))+> GL.matrixMode $= GL.Projection+> GL.loadIdentity+> let row = realToFrac h / unit / 2+> col = realToFrac w / unit / 2+> (r, c) = (realToFrac row, realToFrac col)+> GL.ortho2D (-c) c (-r) r+> writeIORef rowcolRef (row, col)++> renderDiagram posMap d = +> let starts = startAtoms d+> pos = map (\a -> (maybe Nothing (Just . fst) (IntMap.lookup (atomID a) posMap), a)) starts+> pg@(posMap', grid) = foldr (\ (p, a) (pm, gr) -> +> let i = atomID a+> (wa, ha) = atomSize a+> mx = maximum (0 : map fst (Set.elems gr))+> p' = fromMaybe (mx + 4, 0) p+> dir = maybe N snd (IntMap.lookup i pm)+> in layout [] (insert i (p', dir) pm, occupy gr p' (wa, ha)) (atomPorts a)) (posMap, Set.empty) pos+> (io, grid') = render pg+> in ((posMap', grid'), io)+> where +> render (posMap, grid) = foldWithKey (\i a (io, grid) -> +> let ((x, y), d) = posMap ! i+> (lines, grid') = foldr (\ (p, q) (ls, grid) -> +> let (l, grid') = runLine grid p q+> in (l:ls, grid')) ([], grid)+> [ ((x + px, y + py, portdir posMap p),+> (x' + qx, y' + qy, portdir posMap q))+> | p <- atomPorts a,+> let q = portEnd p, +> let j = atomID (owner q),+> i < j || (i == j && portPos p <= portPos q),+> let ((x', y'), _) = posMap ! j,+> let (px, py) = portpos posMap p,+> let (qx, qy) = portpos posMap q ]+> action = do +> GL.preservingMatrix (do+> GL.translate (vector3 (fromIntegral x) (fromIntegral y) 0) +> let o = maybe N snd (IntMap.lookup i posMap)+> GL.rotate (realToFrac (90 * fromEnum o)) (vector3 0 0 1)+> atomDraw a) +> GL.preservingMatrix $ mapM_ (\l -> do+> GL.color linecolor+> GL.renderPrimitive GL.LineStrip $ mapM_ (\ (x0, y0) ->+> GL.vertex (vertex3 (fromIntegral x0) (fromIntegral y0) 0)) l) lines+> io+> in (action, grid')) (return (), grid) (allAtoms d)++The following is a very naive but fast line layout algorithm.++> runLine grid (x0, y0, d0) (x1, y1, d1) = +> let (var, f) = flexLine (x0, y0, d0) (x1, y1, d1)+> lines = map f (iterateList var)+> g l = let l' = mark l --(take (length l - 2) (tail l))+> in Set.fromList l' --Set.\\ Set.fromList (take 3 l' ++ drop (length l' - 3) l')+> LineSeg (l, s) _ = minimum $ take 10 $+> map (\x -> let s = g x in LineSeg (x, s) (Set.size (Set.intersection grid s))) lines+> in (l, Set.union grid s)+> where+> mark [] = []+> mark [(x0,y0)] = []+> mark l@((x0,y0):(x1,y1):rs) = Set.toList $ Set.fromList $+> [(x, y) | x <- segment x0 x1, y <- segment y0 y1] ++ mark (tail l)+> segment x0 x1 | x0 == x1 = [x0]+> segment x0 x1 = x0 : segment (x0 + signum (x1 - x0)) x1++> data LineSeg a b = LineSeg a b deriving (Eq, Show)+> instance (Eq a, Eq b, Ord b) => Ord (LineSeg a b) where+> compare (LineSeg _ x) (LineSeg _ y) = compare x y++> running grid l = running' l+> where+> running' l@(p@(x0, y0):q@(x1, y1):r@(x2, y2):xs) = +> (Set.member p grid && Set.member q grid && Set.member r grid && +> (((x0 == x1) && (x1 == x2) && (y1 + y1 == y0 + y2)) || +> ((y0 == y1) && (y1 == y2) && (x1 + x1 == x0 + x2)))) || running' (tail l)+> running' _ = False++> iterateList :: [[a]] -> [[a]]+> iterateList l = [ zipWith (!!) l idx | idx <- dia (length l) 0 ]++> dia d n = dia' d n ++ dia d (n + 1)+> where+> dia' 1 n = [[n]]+> dia' d n = [ u : v | u <- [0 .. n], v <- dia' (d - 1) (n - u)]++> flexLine :: (Int, Int, Direction) -> (Int, Int, Direction) -> +> ([[Int]], [Int] -> [(Int, Int)])+> flexLine (x0, y0, N) (x1, y1, N) = +> ([inc (max y0 y1)], \[y] -> [(x0, y0), (x0, y), (x1, y), (x1, y1)])+> flexLine (x0, y0, S) (x1, y1, S) = +> ([dec (min y0 y1)], \[y] -> [(x0, y0), (x0, y), (x1, y), (x1, y1)])+> flexLine (x0, y0, E) (x1, y1, E) = +> ([inc (max x0 x1)], \[x] -> [(x0, y0), (x, y0), (x, y1), (x1, y1)])+> flexLine (x0, y0, W) (x1, y1, W) = +> ([dec (min x0 x1)], \[x] -> [(x0, y0), (x, y0), (x, y1), (x1, y1)])+> flexLine (x0, y0, N) (x1, y1, E) = +> ([inc y0, inc x1], \[y, x] -> [(x0, y0), (x0, y), (x, y), (x, y1), (x1, y1)])+> flexLine (x0, y0, N) (x1, y1, W) = +> ([inc y0, dec x1], \[y, x] -> [(x0, y0), (x0, y), (x, y), (x, y1), (x1, y1)])+> flexLine (x0, y0, S) (x1, y1, E) = +> ([dec y0, inc x1], \[y, x] -> [(x0, y0), (x0, y), (x, y), (x, y1), (x1, y1)])+> flexLine (x0, y0, S) (x1, y1, W) = +> ([dec y0, dec x1], \[y, x] -> [(x0, y0), (x0, y), (x, y), (x, y1), (x1, y1)])+> flexLine (x0, y0, N) (x1, y1, S) | y0 > y1 = +> ([inc y0, alt ((x0 + x1) `div` 2), dec y1], +> \[y, x, y'] -> [(x0, y0), (x0, y), (x, y), (x, y'), (x1, y'), (x1, y1)])+> flexLine (x0, y0, N) (x1, y1, S) = +> ([alt ((y0 + y1) `div` 2)], +> \[y] -> [(x0, y0), (x0, y), (x1, y), (x1, y1)])+> flexLine (x0, y0, E) (x1, y1, W) | x0 > x1 = +> ([inc x0, alt ((y0 + y1) `div` 2), dec x1], +> \[x, y, x'] -> [(x0, y0), (x, y0), (x, y), (x', y), (x', y1), (x1, y1)])+> flexLine (x0, y0, E) (x1, y1, W) = +> ([alt ((x0 + x1) `div` 2)], +> \[x] -> [(x0, y0), (x, y0), (x, y1), (x1, y1)])+> flexLine p q = flexLine q p++> inc x = [x..]+> dec x = [x, x-1 ..]+> alt x = alt' (x : inc x) (tail (dec x))+> where alt' (i:is) (j:js) = i : j : alt' is js+++> data UserAction = UserAction (IO (UserAction, IO ()))++> lastKeyTime = unsafePerformIO (newIORef 0)+> readKeyPress l = do+> t <- GL.get GLFW.time+> t0 <- readIORef lastKeyTime+> k <- readKeyPress' l+> case k of+> Nothing -> return Nothing+> _ -> if t - t0 < 0.4+> then return Nothing+> else do+> writeIORef lastKeyTime t+> return k+> where +> readKeyPress' :: Enum a => [a] -> IO (Maybe a)+> readKeyPress' [] = return Nothing+> readKeyPress' (k:ks) = do+> p <- GLFW.getKey k+> if p == GLFW.Press then return (Just k) else readKeyPress' ks++> handleUserAction factor (keySet, keyHandle) reduce d = do+> let r@((_, grid), _) = renderDiagram empty d+> autoAdjust grid factor+> buttonReleased d r+> where+> buttonReleased d r@((posMap, grid), render) = do+> left <- GLFW.getMouseButton GLFW.ButtonLeft+> right <- GLFW.getMouseButton GLFW.ButtonRight+> zoom <- GLFW.getKey GLFW.LALT+> shift <- GLFW.getKey GLFW.LCTRL+> case (left == GLFW.Press, right == GLFW.Press, +> zoom == GLFW.Press, shift == GLFW.Press) of+> (True, _, False, False) -> processButton GLFW.ButtonLeft+> (_, _, True, False) -> processZoom GLFW.LALT+> (_, _, False, True) -> processShift GLFW.LCTRL+> (_, True, _, _) -> processButton GLFW.ButtonRight+> _ -> do+> k <- readKeyPress (' ' : keySet)+> case k of +> Just k' ->+> if k' == ' '+> then do+> --writeIORef factor (0,0,1)+> autoAdjust grid factor+> return (UserAction $ buttonReleased d r, render)+> else do+> (d', r'@(_, render')) <- keyHandle k' d r+> return (UserAction $ buttonReleased d' r', render')+> Nothing -> return (UserAction $ buttonReleased d r, render)+> where+> processButton but = do+> GL.Position mx my <- GL.get GLFW.mousePos+> (cx, cy, scale) <- readIORef factor+> (row, col) <- readIORef rowcolRef+> let (w, h) = (col * unit, row * unit) +> atom = locateAtom (allAtoms d) posMap +> ((fromIntegral mx - w - cx) / scale / unit) +> ((h - fromIntegral my - cy) / scale / unit)+> t0 <- GL.get GLFW.time+> return (UserAction $ buttonPressed but+> d r atom (mx, my) t0, render)+>+> processZoom key = do+> GL.Position mx my <- GL.get GLFW.mousePos+> t0 <- GL.get GLFW.time+> return (UserAction $ mouseZoom key (mx, my, mx, my, t0) d r, render)++> processShift key = do+> GL.Position mx my <- GL.get GLFW.mousePos+> t0 <- GL.get GLFW.time+> return (UserAction $ mouseShift key (mx, my, mx, my, t0) d r, render)++> buttonPressed but d r@((posMap, _), render) atom mp t0 = do+> status <- GLFW.getMouseButton but+> if status == GLFW.Release+> then case atom of+> Just a -> +> if but == GLFW.ButtonRight+> then do+> (ids, d') <- reduce (atomID a)+> let posMap' = filterWithKey (\i _ -> elem i ids) posMap+> r'@(_, render') = renderDiagram posMap' d'+> return (UserAction $ buttonReleased d' r', render')+> else do+> let (pos, o) = posMap ! atomID a+> o' = toEnum ((fromEnum o + 1) `mod` 4)+> posMap' = adjust (const (pos, o')) (atomID a) posMap+> r'@(_, render') = renderDiagram posMap' d+> return (UserAction $ buttonReleased d r', render')+> _ -> return (UserAction $ buttonReleased d r, render)+> else do+> t1 <- GL.get GLFW.time+> case (t1 - t0 > 0.4, atom) of+> (True, Just a) -> do+> let ((x, y), _) = posMap ! atomID a+> return (UserAction $ buttonHolding but d r a ((x, y), mp), render)+> _ -> return (UserAction $ buttonPressed but d r atom mp t0, render)+> buttonHolding but d r@((posMap, _), _) atom s@((ax, ay), (mx, my)) = do+> status <- GLFW.getMouseButton but+> GL.Position mx' my' <- GL.get GLFW.mousePos+> (_, _, scale) <- readIORef factor+> let ax' = ax + truncate (realToFrac (mx' - mx) / scale / unit)+> ay' = ay + truncate (realToFrac (my - my') / scale / unit)+> i = atomID atom+> moved = abs (ax' - ax) >= 1 || abs (ay' - ay) >= 1+> posMap' = if moved+> then adjust (\ ((x, y), d) -> ((ax', ay'), d)) i posMap +> else posMap+> r'@(_, render) = if moved then renderDiagram posMap' d else r+> if status == GLFW.Release+> then return (UserAction $ buttonReleased d r', render)+> else return (UserAction $ buttonHolding but d r' atom s, render)+>+> mouseZoom key state d r = do+> status <- GLFW.getKey key+> if status == GLFW.Release +> then return (UserAction $ buttonReleased d r, snd r)+> else do+> (dx, dy, state') <- relativeSpeed state+> (cx, cy, scale) <- readIORef factor+> let scale' = scale * (dx - dy) / 100+> writeIORef factor (cx, cy, scale + scale')+> return (UserAction $ mouseZoom key state' d r, snd r)++> mouseShift key state d r = do+> status <- GLFW.getKey key+> if status == GLFW.Release+> then return (UserAction $ buttonReleased d r, snd r)+> else do+> (dx, dy, state') <- relativeSpeed state+> (cx, cy, scale) <- readIORef factor+> writeIORef factor (cx - dx, cy - dy, scale)+> return (UserAction $ mouseShift key state' d r, snd r)++> relativeSpeed (mx, my, x0, y0, t0) = do+> GL.Position x y <- GL.get GLFW.mousePos+> t1 <- GL.get GLFW.time+> let (mx', my') = if signum (x0 - mx) * signum (x - x0) < 0 ||+> signum (y0 - my) * signum (y - y0) < 0+> then (x0, y0) else (mx, my)+> dx = fromIntegral (x - mx') / realToFrac (t1 - t0) / 1000+> dy = fromIntegral (my' - y) / realToFrac (t1 - t0) / 1000+> return (dx, dy, (mx', my', x, y, t1))++> autoAdjust grid factor = do+> GL.Size w h <- GL.get GLFW.windowSize +> let (x0, y0, x1, y1) = gridBounds grid+> cx = unit * fromIntegral (x0 + x1) / 2+> cy = unit * fromIntegral (y0 + y1) / 2 +> sx = fromIntegral (x1 - x0 + margin) * unit / fromIntegral w+> sy = fromIntegral (y1 - y0 + margin) * unit / fromIntegral h+> ms = max sx sy +> s = if ms < 1 then 1 else ms+> writeIORef factor (-cx / s, -cy / s, 1/s)++> gridBounds grid = +> let (xs, ys) = unzip (Set.elems grid)+> in (minimum xs, minimum ys, maximum xs, maximum ys)+> +> renderGrid grid = do +> let (c0, r0, c1, r1) = gridBounds grid +> l1 = [(x, r0, x, r1) | x <- [c0 .. c1]] +> l2 = [(c0, y, c1, y) | y <- [r0 .. r1]]+> GL.color gridcolor +> GL.renderPrimitive GL.Lines (mapM_ line (l1 ++ l2))+> mapM_ (\ (x, y) -> GL.preservingMatrix (do+> GL.translate (vector3 (fromIntegral x) (fromIntegral y) 0)+> GL.renderPrimitive GL.LineStrip (circle 0.1 0.1 4))) (Set.elems grid)+> where+> line (x1, y1, x2, y2) = do+> GL.vertex (vertex3 (fromIntegral x1) (fromIntegral y1) 0)+> GL.vertex (vertex3 (fromIntegral x2) (fromIntegral y2) 0)++> circle :: GLfloat -> GLfloat -> GLfloat -> IO ()+> circle r1 r2 step =+> let is = take (truncate step + 1) [0, i' .. ]+> i' = 2 * pi / step+> vs = [ (r1 * cos i, r2 * sin i) | i <- is ]+> in mapM_ (\(x, y) -> GL.vertex (GL.Vertex3 x y 0)) vs++> locateAtom atoms posMap mx my = locate (toList posMap)+> where+> locate [] = Nothing+> locate ((i, ((x, y), _)):rs) = +> let a = atoms ! i+> in if inside (x, y) (atomSize a) then Just a else locate rs+> inside (x, y) (w, h) =+> (realToFrac (x - w) <= mx) &&+> (realToFrac (x + w) > mx) &&+> (realToFrac (y - w) <= my) &&+> (realToFrac (y + w) > my)++Some primilinary font support++> loadFont = do+> fontpath <- getDataFileName "font.tga"+> [font] <- GL.genObjectNames 1+> GL.textureBinding GL.Texture2D $= Just font+> -- this next line is important, otherwise it won't render the texture!+> GL.textureFilter GL.Texture2D $= ((GL.Linear', Nothing), GL.Linear')+> GLFW.loadTexture2D fontpath [GLFW.OriginUL, GLFW.NoRescale]+> return font++> renderChar font c = do+> let y = fromIntegral (fromEnum c `rem` 16 * 16) / 256+> x = fromIntegral (fromEnum c `quot` 16 * 8) / 128+> dx = 8 / 128+> dy = 16 / 256+> h = 16 / unit +> w = 8 / unit+> GL.preservingMatrix $ GL.renderPrimitive GL.Quads (do+> GL.texCoord (texCoord2 x y)+> GL.vertex (vertex3 0 h 0)+> GL.texCoord (texCoord2 (x + dx) y)+> GL.vertex (vertex3 w h 0)+> GL.texCoord (texCoord2 (x + dx) (y + dy))+> GL.vertex (vertex3 w 0 0)+> GL.texCoord (texCoord2 x (y + dy))+> GL.vertex (vertex3 0 0 0))+> GL.translate (vector3 w 0 0)++> renderString s = do+> Just font <- readIORef fontRef+> GL.texture GL.Texture2D $= GL.Enabled+> GL.textureBinding GL.Texture2D $= Just font+> GL.preservingMatrix $ mapM_ (renderChar font) s+> GL.texture GL.Texture2D $= GL.Disabled++> renderText = mapM_ out . lines+> where out s = renderString s >> GL.translate (vector3 0 (-1.25) 0)++> color3 = GL.Color3 :: GLfloat -> GLfloat -> GLfloat -> GL.Color3 GLfloat+> vector3 = GL.Vector3 :: GLfloat -> GLfloat -> GLfloat -> GL.Vector3 GLfloat+> vertex3 = GL.Vertex3 :: GLfloat -> GLfloat -> GLfloat -> GL.Vertex3 GLfloat+> texCoord2 = GL.TexCoord2 :: GLfloat -> GLfloat -> GL.TexCoord2 GLfloat++> clearcolor = GL.Color4 1 1 1 1+> linecolor = color3 0 0 0+> gridcolor = color3 0.9 0.9 0.9+> unitcolor = color3 0 0 0+> textcolor = color3 0 0 1+> portcolor = color3 1 0 0++The drawing routings for Nodes++> drawApplicator label = do+> GL.color unitcolor+> GL.renderPrimitive GL.LineStrip (circle 1.5 1.5 20)+> GL.translate (vector3 0 1.5 0)+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 0.5 0))+> GL.translate (vector3 0 (-3) 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 (-0.5) 0))+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color unitcolor+> GL.translate (vector3 1.5 1.5 0)+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0.5 0 0))+> GL.translate (vector3 (-1.5 - 4 / unit) (-8 / unit) 0)+> renderString label++> drawAbstractor label = do+> GL.color unitcolor+> GL.renderPrimitive GL.LineStrip (circle 1.5 1.5 20)+> GL.translate (vector3 0 1.5 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 0.5 0))+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color unitcolor+> GL.translate (vector3 0 (-3) 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 (-0.5) 0))+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.translate (vector3 1.5 1.5 0)+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0.5 0 0))+> GL.translate (vector3 (-1.5 - 4 / unit) (- 8 / unit) 0)+> renderString label++> drawDelimiter label = do+> GL.color unitcolor+> GL.renderPrimitive GL.LineStrip (do+> GL.vertex (vertex3 (-1) 0.2 0)+> GL.vertex (vertex3 (-1) (-0.2) 0)+> GL.vertex (vertex3 1 (-0.2) 0)+> GL.vertex (vertex3 1 0.2 0))+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 2 0)+> GL.vertex (vertex3 0 1 0)+> GL.vertex (vertex3 0 (-1) 0)+> GL.vertex (vertex3 0 (-2) 0))+> GL.translate (vector3 0 1 0)+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.translate (vector3 0 (-2) 0)+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color unitcolor+> GL.translate (vector3 1.2 (1 - 8 / unit) 0)+> renderString label++> drawDuplicator label = do+> GL.color unitcolor+> GL.renderPrimitive GL.LineStrip (do+> GL.vertex (vertex3 (-1.5) 1 0)+> GL.vertex (vertex3 0 (-1) 0)+> GL.vertex (vertex3 1.5 1 0)+> GL.vertex (vertex3 (-1.5) 1 0))+> GL.translate (vector3 (-1) 1 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 1 0))+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.translate (vector3 2 0 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 1 0))+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.translate (vector3 (-1) (-2) 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 (-1) 0))+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color unitcolor+> GL.translate (vector3 (-4 / unit) (1 - 8 / unit) 0)+> renderString label++> drawEraser label = do+> GL.color unitcolor+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 (-1.2) 0)+> GL.vertex (vertex3 0 (-2) 0))+> GL.renderPrimitive GL.LineStrip (circle 1.2 1.2 20)+> GL.renderPrimitive GL.LineStrip (circle 0.8 0.8 20)+> GL.translate (vector3 0 (-1.2) 0)+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color unitcolor+> GL.translate (vector3 (- fromIntegral (length label * 4) / unit) (1.2 - 8 / unit) 0)+> renderString label++> drawTwoPin label = do+> GL.color unitcolor+> GL.renderPrimitive GL.LineStrip (circle 1.5 1.5 20)+> GL.translate (vector3 0 1.5 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 0.5 0))+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color unitcolor+> GL.translate (vector3 0 (-3) 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 (-0.5) 0))+> GL.renderPrimitive GL.LineStrip (circle 0.2 0.2 10)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0.5 0 0))+> GL.color textcolor+> GL.translate (vector3 (- fromIntegral (length label * 4) / unit) (1.5 - 8 / unit) 0)+> renderString label++> drawSingle label = do+> GL.color unitcolor+> GL.renderPrimitive GL.LineStrip (circle 1.5 1.5 20)+> GL.translate (vector3 0 1.5 0)+> GL.renderPrimitive GL.Lines (do+> GL.vertex (vertex3 0 0 0)+> GL.vertex (vertex3 0 0.5 0))+> GL.color portcolor+> GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)+> GL.color textcolor+> GL.translate (vector3 (- fromIntegral (length label * 4) / unit) (- 1.5 - 8 / unit) 0)+> renderString label+
+ src/INet.lhs view
@@ -0,0 +1,479 @@+Interactive Net for Lambdascope implmenetation++> module INet where++> import Diagram++> import Data.IntMap as IntMap hiding (filter, map)+> import Data.Maybe (fromJust)+> import Control.Monad.State++Interactive Net is defined to be a table, that maps node IDs to+a triple that contains the node type, a list of ports (indexed+by the list index), and value.++> type INetV = (NodeType, [(NodeID, Int)], Maybe Int)+> type INet = IntMap INetV++A port is a pair of the other end's NodeID and port index.++> type NetPort = (NodeID, Int)+> type NodeID = Int++> data NodeType = Applicator+> | Applicator' -- flip of Applicator+> | Abstractor +> | Delimiter +> | Delimiter' -- flip of Delimiter+> | Duplicator+> | SuperDup -- dup everything+> | Eraser+> | Dummy -- dummy for self-loop+> | Initiator -- never destroyed+> | Constructor String -- data constructor+> | TwoPin Int String | TwoPin' Int String -- for meta function+> | Single String | Single' String -- for meta value++> deriving (Eq, Show)++> findInitiator [] = Nothing+> findInitiator (a@(i, (Initiator, [(b, u)], Nothing)):as) = Just a+> findInitiator (a:as) = findInitiator as++ netToDiagram :: Net -> Diagram++> netToDiagram net = +> let list = toList net+> Just (init, _) = findInitiator list+> atoms = map toAtom list+> d = fromList (map (\a -> (atomID a, a)) atoms)+> heads = map (d!) $ foldl (\h i -> +> if any (\j -> reachable net [] [j] i) h then h else i : h) [] $+> ((init:) . filter (/=init)) $ map fst list+> in Diagram heads d+> where+> toAtom (i, (t, p, v)) = +> let a = Atom i l (map (toPort a t) (zip [0..] p)) (2, 2) (draw l)+> in a+> where+> (l, draw) = +> case t of+> Applicator -> ("@", drawApplicator)+> Applicator' -> ("@", drawAbstractor)+> Abstractor -> ("\x80", drawAbstractor)+> Delimiter -> (maybe "" show (v::Maybe Int), drawDelimiter)+> Duplicator -> (maybe "" show (v::Maybe Int), drawDuplicator)+> SuperDup -> ("*", drawDuplicator)+> Eraser -> ("", drawEraser)+> Initiator -> ("I", drawEraser)+> Delimiter' -> ("S", drawTwoPin)+> Constructor l -> (l, drawAbstractor)+> TwoPin _ l -> (l, drawTwoPin)+> TwoPin' _ l -> (l, drawTwoPin)+> Single l -> (l, drawSingle)+> Single' l -> (l, drawSingle)++> toPort a t (m, (j, n)) = +> let (d, p) = pos t m+> b = toAtom (j, (net ! j))+> in Port a (atomPorts b !! n) d p++> reachable :: INet -> [Int] -> [Int] -> Int -> Bool+> reachable d visited [] i = False+> reachable d visited (x:xs) i = +> let (_, ps, _) = (d ! x)+> js = map fst ps+> ks = filter (flip notElem visited) js+> in (x == i) || reachable d (x : visited) (xs ++ ks) i++> pos Applicator 0 = (S, (0, -2))+> pos Applicator 1 = (E, (2, 0))+> pos Applicator 2 = (N, (0, 2))+> pos Applicator' i = pos Abstractor i+> pos Abstractor 0 = (N, (0, 2))+> pos Abstractor 1 = (S, (0, -2))+> pos Abstractor 2 = (E, (2, 0))+> pos Delimiter 0 = (S, (0, -2))+> pos Delimiter 1 = (N, (0, 2))+> pos Duplicator 0 = (S, (0, -2))+> pos Duplicator 1 = (N, (1, 2))+> pos Duplicator 2 = (N, (-1, 2))+> pos SuperDup i = pos Duplicator i+> pos Eraser 0 = (S, (0, -2))+> pos Initiator 0 = (S, (0, -2))+> pos Delimiter' 0 = (N, (0, 2))+> pos Delimiter' 1 = (S, (0, -2))+> pos (Constructor _) i = pos Abstractor i+> pos (TwoPin arity l) i = pos Delimiter' i+> pos (TwoPin' arity l) i = pos Delimiter i+> pos (Single _) 0 = (N, (0, 2))+> pos (Single' _) 0 = (N, (0, 2))++> type LocalRule = INet -> (Int, INetV) -> (Int, INetV) -> Maybe INet+> type Rule = INet -> (INet, Int)++Make a local rule global by applying it once everywhere.++> applyRule :: LocalRule -> Rule+> applyRule rule net = applyRule' 0 rule (keys net) net++> applyRule' :: Int -> LocalRule -> [Int] -> Rule+> applyRule' num rule [] net = (net, num)+> applyRule' num rule (i:rs) net = +> let a@(at, ap, av) = net ! i+> (j, n) = head ap+> b@(bt, bp, bv) = net ! j+> r = rule net (i, a) (j, b)+> in if member i net +> then maybe (applyRule' num rule rs net) (applyRule' (num + 1) rule (filter (j/=) rs)) r+> else applyRule' num rule rs net++repeatedly apply a rule until it is no longer applicable.++> repeatRule = repeatRule' 0 ++> repeatRule' :: Int -> Rule -> Rule+> repeatRule' sum rule net = +> let (net', num) = rule net+> in if num == 0 +> then (net, sum)+> else repeatRule' (sum + num) rule net'++Apply a local rule at the outermost position.+actually beta and meta can be performed simultaneously)++> outermost :: LocalRule -> Rule+> outermost rule net =+> case findInitiator $ toList net of+> Just (i, _) -> outermost' [] [i]+> Nothing -> (net, 0)+> where +> outermost' _ [] = (net, 0)+> outermost' visited (i:is) =+> let a@(at, ((j, _):ps), _) = net ! i +> b = net ! j+> in if elem i visited+> then (net, 0)+> else maybe (outermost' (i:visited) (j:is)) (\net -> (net, 1)) $ rule net (i, a) (j, b)++Compose two local rules together, try the first one, if it succeeds, just+return; otherwise, try the second one.++> infixr 5 ->-+> (->-) :: LocalRule -> LocalRule -> LocalRule+> (->-) r1 r2 net a b = maybe (r2 net a b) Just $ r1 net a b++> infixr 5 +>++> (+>+) :: Rule -> Rule -> Rule+> (+>+) r1 r2 net = +> let r@(net', n) = r2 net+> in if n == 0 then r1 net else r++The cross rules: annihilate and commute. ++> cross net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> if head bp == (i, 0) -- princple ports meet?+> then if at == bt && av == bv -- same type and value?+> then Just $ annihilate net (i, a) (j, b)+> else case (at, bt) of -- different type+> (Applicator, Abstractor) -> Nothing -- leave the beta rule out+> (Abstractor, Applicator) -> Nothing+> (Constructor _, TwoPin _ _) -> Nothing -- leave the meta rule out+> (TwoPin _ _, Constructor _) -> Nothing+> (Single _, TwoPin _ _) -> Nothing -- FIXME: never cross single, but cross single'+> (TwoPin _ _, Single _) -> Nothing+> (Initiator, Delimiter) -> Just $ commute net (i, a) (j, b)+> (Delimiter, Initiator) -> Just $ commute net (i, a) (j, b)+> (Initiator, _) -> Nothing+> (_, Initiator) -> Nothing+> _ -> Just $ commute net (i, a) (j, b)+> else case (at, bt, snd (head ap)) of+> (SuperDup, Applicator, 2) -> Just $ superDup net (i, a) (j, b)+> (SuperDup, TwoPin _ _, 1) -> Just $ superDup net (i, a) (j, b)+> (SuperDup, Delimiter, 1) -> Just $ superDup net (i, a) (j, b)+> _ -> Nothing++cross from rear++> superDup net (i, a) (j, b) = +> let Just net' = upsideDown net (j, b)+> net'' = commute net' (i, a) (j, net'!j)+> ks = map fst $ filter (\ (i, (ct, _, _)) -> case ct of+> Applicator' -> True+> TwoPin' _ _ -> True+> Delimiter' -> True+> _ -> False) (toList net'')+> in foldr (\k net -> fromJust $ upsideDown net (k, net!k)) net'' ks+++The modified cross rule, only moves delimiter or annihilates.++> cross' net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> if head bp == (i, 0) -- princple ports meet?+> then if at == bt && av == bv -- same type and value?+> then Just $ annihilate net (i, a) (j, b)+> else case (at, bt) of -- different type+> (Delimiter, _) -> Just $ commute net (i, a) (j, b)+> (_, Delimiter) -> Just $ commute net (i, a) (j, b)+> _ -> Nothing+> else Nothing++> annihilate net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> let pairup = zip (tail ap) (tail bp)+> pair' = fixLoop pairup pairup+> in foldr (\ ((c, u), (d, v)) ->+> adjust (\ (ct, cp, cv) -> (ct, replace u (d, v) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace v (c, u) dp, dv)) d)+> ((delete i . delete j) net) pair'+> where+> fixLoop _ [] = []+> fixLoop pairs (x@(p@(c, u), q@(d, v)) : xs) = +> let p' = if c == i then snd (pairs!!(u-1)) else p+> q' = if d == j then fst (pairs!!(v-1)) else q+> in (p',q') : fixLoop pairs xs++The commute rule should also work for the Eraser so that the other thing+annihilates.++> commute net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> let maxID = maximum (keys net)+> bs = take (length ap - 1) [(maxID + 1) .. ] +> as = take (length bp - 1) [(maxID + 1 + length bs) .. ]+> bs_ = map (\ (k, (c, u)) -> (bt', +> (if c == i then (bs!!(u-1), 0) +> else if c == j then (as!!(u-1), 0) else (c, u))+> : zip as (repeat k), bv')) (tail (zip [0..] ap))+> as_ = map (\ (k, (c, u)) -> (at', +> (if c == j then (as!!(u-1), 0) +> else if c == i then (bs!!(u-1), 0) else (c, u)) +> : zip bs (repeat k), av'))+> (tail (zip [0..] bp))+> av' = maybe Nothing (\v -> Just $+> if bt == Abstractor || +> (bt == Delimiter && v >= fromJust bv) then v + 1 else v) av+> bv' = maybe Nothing (\v -> Just $+> if at == Abstractor || +> (at == Delimiter && v >= fromJust av) then v + 1 else v) bv+> at' = if at == Duplicator && av' == Nothing && bt == Abstractor then SuperDup else at+> bt' = if bt == Duplicator && bv' == Nothing && at == Abstractor then SuperDup else bt+> in (flip (foldr (\ (k, (c, u)) -> adjust (\ (ct, cp, cv) ->+> (ct, replace u (bs !! k, 0) cp, cv)) c)) (zip [0..] (tail ap)) .+> flip (foldr (\ (k, (c, u)) -> adjust (\ (ct, cp, cv) ->+> (ct, replace u (as !! k, 0) cp, cv)) c)) (zip [0..] (tail bp)) .+> flip (foldr (uncurry insert)) (zip bs bs_) .+> flip (foldr (uncurry insert)) (zip as as_) .+> delete i . delete j) net++The erase rule erase anything it sees.++> erase net (i, a@(at, ap@((_, n):_), av)) (j, b@(bt, bp, bv)) =+> case (at, bt, head bp == (i, 0)) of++Erase sharing is actually not strictly needed as they are not active pairs,+though it helps to speed up garbage collection and the reduction of degerated +(self-looping) components.++> (Eraser, Duplicator, False) -> eraseSharing +> (Eraser, SuperDup, False) -> eraseSharing+> (Eraser, _, True) -> cross net (i, a) (j, b) -- otherwise cross+> (_, Eraser, _) -> erase net (j, b) (i, a)+> _ -> Nothing+> where+> eraseSharing =+> let (c, u) = bp !! (3 - n)+> (d, v) = bp !! 0+> in Just $ (delete i . delete j . +> adjust (\ (ct, cp, cv) -> (ct, replace u (d, v) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace v (c, u) dp, dv)) d) net++The prune rule removes all trees without the initiator. This is necessary for+garbage collecting self-looping components.+ +> prune :: Rule+> prune net =+> let Just (i, a) = findInitiator (toList net)+> visited = visit [] [i]+> net' = filterWithKey (\k _ -> elem k visited) net+> in (net', 0)+> where +> visit visited [] = visited+> visit visited (i:is) = +> let a@(_, p, _) = net ! i+> bs = filter (flip notElem visited) (map fst p)+> in visit (i:visited) (is ++ bs)+ +The disintegrate rule is never really used here, because we won't be able+to recover the Abstractor afterwards. (FIXME: to handle self-loop)++> disintegrate net (i, a@(at, ap@[(b,l), (c,u), (d,v)], av)) = +> let maxID = maximum (keys net)+> (d1, d2) = (maxID + 1, maxID + 2)+> d1_ = (Delimiter, [(i,2), (c, u)], Just 0)+> d2_ = (Delimiter, [(i,1), (d, v)], Just 0)+> in (adjust (const (Applicator, [(b, l), (d2, 0), (d1, 0)], Nothing)) i .+> adjust (\ (ct, cp, cv) -> (ct, replace u (d1, 1) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace v (d2, 1) dp, dv)) d .+> insert d1 d1_ . insert d2 d2_) net++The beta rule aplies when Applicator meets Abstractor.++> beta net (i, a@(at, ap, _)) (j, b@(bt, bp, _)) =+> case (head bp == (i, 0), at, bt) of+> (True, Applicator, Abstractor) -> Just $ beta' net (i, a) (j, b)+> (True, Abstractor, Applicator) -> Just $ beta' net (j, b) (i, a)+> _ -> Nothing++> beta' net (i, a@(at, [_, (c,u), (d,v)], av))+> (j, b@(bt, [_, (e,x), (f,y)], bv)) = +> let maxID = maximum (keys net)+> (d1, d2) = (maxID + 1, maxID + 2)+> d1_ = (Delimiter, [(d, v), if e == j then (d2, 1) else (e, x)], Just 0)+> d2_ = (Delimiter, [(c, u), if f == j then (d1, 1) else (f, y)], Just 0)+> in (adjust (\ (ct, cp, cv) -> (ct, replace u (d2, 0) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace v (d1, 0) dp, dv)) d .+> adjust (\ (et, ep, ev) -> (et, replace x (d1, 1) ep, ev)) e .+> adjust (\ (ft, fp, fv) -> (ft, replace y (d2, 1) fp, fv)) f .+> insert d1 d1_ . insert d2 d2_ . delete i . delete j) net++> replace :: Int -> a -> [a] -> [a]+> replace _ _ [] = []+> replace 0 v (x:xs) = v : xs+> replace i v (x:xs) = x : replace (i - 1) v xs++The following rules are for reading back++> unwind net a@(_, (Delimiter, _, _)) _ = Nothing+> unwind net a@(_, (Delimiter', _, _)) _ = Nothing+> unwind net a@(_, (TwoPin _ _, _, _)) _ = Nothing+> unwind net a@(_, (TwoPin' _ _, _, _)) _ = Nothing+> unwind net a@(_, (Applicator', _, _)) _ = Nothing+> unwind net (i, a@(Single l, p, Nothing)) _ = Just $+> adjust (\_ -> (Single' l, p, Nothing)) i net+> unwind net a b = upsideDown net a++> upsideDown net (i, a@(at, _, _)) = +> case at of+> Applicator -> +> let (_, [(b,u), (c,v), (d, w)], _) = a +> in Just $+> (adjust (const (Applicator', [(d, w), (b, u), (c, v)], Nothing)) i .+> adjust (\ (bt, bp, bv) -> (bt, replace u (i, 1) bp, bv)) b .+> adjust (\ (ct, cp, cv) -> (ct, replace v (i, 2) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace w (i, 0) dp, dv)) d) net+> Applicator' -> +> let (_, [(b,u), (c,v), (d, w)], _) = a +> in Just $+> (adjust (const (Applicator, [(c, v), (d, w), (b, u)], Nothing)) i .+> adjust (\ (bt, bp, bv) -> (bt, replace u (i, 2) bp, bv)) b .+> adjust (\ (ct, cp, cv) -> (ct, replace v (i, 0) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace w (i, 1) dp, dv)) d) net+> TwoPin arity l -> Just $ upsideDown' (TwoPin' arity l) a+> TwoPin' arity l -> Just $ upsideDown' (TwoPin arity l) a+> Delimiter -> Just $ upsideDown' Delimiter' a+> Delimiter' -> Just $ upsideDown' Delimiter a+> _ -> Nothing+> where+> upsideDown' at' a@(_, [(b,u),(c,v)], av) = +> (adjust (const (at', [(c, v), (b, u)], av)) i .+> adjust (\ (bt, bp, bv) -> (bt, replace u (i, 1) bp, bv)) b .+> adjust (\ (ct, cp, cv) -> (ct, replace v (i, 0) cp, cv)) c) net++> scope net (i, a@(Delimiter, [(b, u), (c, v)], Just av)) _ = upsideDown net (i, a)+> scope _ _ _ = Nothing++> loopcut net (i, a@(Abstractor, [(b, u), (c, v), (d, w)], Nothing)) _ = +> let maxID = maximum (keys net)+> (e, f) = (maxID + 1, maxID + 2)+> e_ = (Eraser, [(i, 2)], Nothing)+> f_ = (Eraser, [(d, w)], Nothing)+> (dt, _, _) = net ! d+> in if dt /= Eraser +> then Just $+> (adjust (\ (at, ap, av) -> (at, replace 2 (e, 0) ap, Nothing)) i .+> adjust (\ (dt, dp, dv) -> (dt, replace w (f, 0) dp, dv)) d .+> insert e e_ . insert f f_) net+> else Nothing+> loopcut _ _ _ = Nothing++> readback = applyRule cross . fst . applyRule loopcut . fst . +> applyRule cross . fst . applyRule scope . fst . +> applyRule cross . fst . applyRule unwind++The Node representation helps to compose INet directly from let expressions.++> data Node = Node {+> nodeType :: NodeType,+> nodeID :: Int,+> nodePorts :: [Node],+> nodeValue :: Maybe Int+> }++> instance Eq Node where+> a == b = nodeID a == nodeID b++> instance Show Node where+> show a = "(" ++ show (nodeID a) ++ ")"++to generate new Node, it requires a unique ID, which can be accomplished by+MonadState.++> applicator fun arg app = incS >>= \i -> +> return $ Node Applicator i [fun, arg, app] Nothing+> abstractor abs body bind = incS >>= \i -> +> return $ Node Abstractor i [abs, body, bind] Nothing+> delimiter to from v = incS >>= \i -> +> return $ Node Delimiter i [to, from] (Just v)+> duplicator out right left v = incS >>= \i -> +> return $ Node Duplicator i [out, right, left] (Just v)+> eraser out = incS >>= \i -> +> return $ Node Eraser i [out] Nothing+> initiator out = incS >>= \i -> +> return $ Node Initiator i [out] Nothing+> tuple top left right = incS >>= \i -> +> return $ Node (Constructor "T") i [top, left, right] Nothing+> twopin arity l top bot = incS >>= \i -> +> return $ Node (TwoPin arity l) i [top, bot] Nothing+> single l top = incS >>= \i -> +> return $ Node (Single l) i [top] Nothing+> dummy top bot = incS >>= \i ->+> return $ Node Dummy i [top, bot] Nothing++> incS :: State Int Int+> incS = do +> i <- get+> put (i + 1)+> return i++> mkNode x = evalState x 0 ++Converting from Node representation to INet (a tree in this case).++> nodeToNet node = removeDummy $ visit [] empty [node]+> where+> visit :: [Node] -> INet -> [Node] -> INet+> visit visited net [] = net+> visit visited net (x:xs) = +> if elem x visited+> then visit visited net xs+> else +> let ps = zip (nodePorts x) [0..]+> net' = setNet net x (map (\ (i, n) ->+> let i' = nodeID i+> k = nth i n ps+> p = nodePorts i+> qs = zip p [0..]+> j = snd (filter ((x==) . fst) qs !! k)+> in (i', j)) ps)+> in visit (x:visited) net' (xs ++ nodePorts x)+> setNet :: INet -> Node -> [(Int, Int)] -> INet+> setNet net (Node t id _ v) p = insert id (t, p, v) net+> nth i n = length . takeWhile (\ (_, m) -> m < n) . filter (\ (j, _) -> j == i)+> removeDummy net = +> foldr (\ (i, (t, p, v)) net -> case t of+> Dummy -> +> let [(b, j), (c, k)] = p+> in (adjust (\ (bt, bp, bv) -> (bt, replace j (c, k) bp, bv)) b .+> adjust (\ (ct, cp, cv) -> (ct, replace k (b, j) cp, cv)) c .+> delete i) net+> _ -> net) net (toList net)+
+ src/Lambda.lhs view
@@ -0,0 +1,214 @@+Generalized Lambda for Lambdascope++> {-# LANGUAGE RecursiveDo #-}++> module Lambda (+> Term(..),+> termToNet,+> termToNode,+> netToTerm,+> meta,+> pretty+> ) where++> import Diagram hiding (S)+> import INet++> import Control.Monad.Fix+> import Data.IntMap hiding (map)+> import Prelude hiding (take, drop, head, tail)++> data Term = Z | S Term | Abs Term | App Term Term +> | Y Term -- fix point+> | Tup Term Term | Fst Term | Snd Term -- tuple+> | VInt Int | VStr String -- value+> | VFunc Int String Term -- function+> deriving (Eq, Show)++We need less strict list operators in order for the recursive do to work.++> head ~(x:xs) = x+> tail ~(x:xs) = xs++> take 0 x = []+> take i x = head x : take (i - 1) (tail x)+> drop 0 x = x+> drop i x = drop (i - 1) (tail x)++> erasers [] = return []+> erasers (x:xs) = mdo+> e <- eraser x+> es <- erasers xs+> return $ e : es++> termToNet i Z ps = debug ("termToNet: Z " ++ show i) $ mdo+> let inp = head ps+> out = head (drop i ps)+> mid = take (i - 1) (tail ps)+> a <- dummy inp out -- dummy used here for proper self-loop+> es <- erasers mid+> return $ (a : es) ++ [a]++> termToNet i x@(S t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo+> let inp = head ps+> out = head (drop i ps)+> mid = take (i - 1) (tail ps)+> d <- delimiter (head n) inp 0+> n <- termToNet (i - 1) t (d : mid)+> e <- eraser out+> return $ (d : tail n) ++ [e]++> termToNet i x@(Abs t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo+> let inp = head ps+> a <- abstractor inp (head n) (head (drop (i + 1) n))+> n <- termToNet (i + 1) t ((a : tail ps) ++ [a])+> let mid = take i (tail n)+> return $ a : mid++> termToNet i x@(App t1 t2) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo+> let inp = head ps+> a <- applicator (head m) (head n) inp+> m <- termToNet i t1 (a : qs)+> n <- termToNet i t2 (a : qs)+> qs <- dup i (tail m) (tail n) (tail ps)+> return $ a : qs+> where +> dup 0 _ _ _ = return []+> dup i ~(a:as) ~(b:bs) ~(c:cs) = mdo+> d <- duplicator c b a 0+> ds <- dup (i - 1) as bs cs+> return $ d : ds++> termToNet i x@(Y t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo+> let inp = head ps+> d <- duplicator a b inp 0+> b <- dummy a d+> a <- applicator (head m) b d+> m <- termToNet i t (a : tail ps)+> return $ d : tail m++> termToNet i x@(Tup t1 t2) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo+> let inp = head ps+> a <- tuple inp (head m) (head n) +> m <- termToNet i t1 (a : qs)+> n <- termToNet i t2 (a : qs)+> qs <- dup i (tail m) (tail n) (tail ps)+> return $ a : qs+> where +> dup 0 _ _ _ = return []+> dup i ~(a:as) ~(b:bs) ~(c:cs) = mdo+> d <- duplicator c b a 0+> ds <- dup (i - 1) as bs cs+> return $ d : ds++> termToNet i x (inp:out) = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo+> case x of +> Fst t -> mdo+> a <- twopin 1 "fst" (head n) inp+> n <- termToNet i t (a:out)+> return $ a : tail n+> Snd t -> mdo+> a <- twopin 1 "snd" (head n) inp+> n <- termToNet i t (a:out)+> return $ a : tail n+> VInt i -> mdo+> a <- single (show i) inp+> n <- erasers out+> return $ a : n+> VStr s -> mdo+> a <- single s inp+> n <- erasers out+> return $ a : n+> VFunc arity l t -> mdo+> a <- twopin arity l (head n) inp+> n <- termToNet i t (a:out)+> return $ a : tail n++> termToNode t = mdo+> e <- initiator a +> [a] <- termToNet 0 t [e]+> return e++> netToTerm :: INet -> Term+> netToTerm net = +> let Just (i, (_, [(b, u)], _)) = findInitiator (toList (debug1 "netToTerm net=" net))+> in toTerm (net ! b)+> where+> toTerm (Abstractor, [_, (b, _), _], _) = Abs (toTerm (net ! b))+> toTerm (Applicator', [_, (b, _), (c, _)], _) = App (toTerm (net ! b)) (toTerm (net ! c))+> toTerm (Delimiter', [_, (b, _)], _) = S (toTerm (net ! b))+> toTerm (Eraser, _, _) = Z+> toTerm (Constructor l, xs, _) = +> case l of +> "T" -> Tup (toTerm (net ! fst (xs !! 1))) (toTerm (net ! fst (xs !! 2)))+> toTerm (TwoPin' arity l, p, _) = +> case l of+> "fst" -> Fst (toTerm (net ! fst (p !! 1))) +> "snd" -> Snd (toTerm (net ! fst (p !! 1))) +> l -> VFunc arity l (toTerm (net ! fst (p !! 1)))+> toTerm (Single' l, p, _) =+> case l of+> (a:as) -> if a >= '0' && a <= '9' +> then VInt (read l)+> else VStr l +> toTerm n = error $ "illegal toTerm input: " ++ show n++meta rules for tuple handling, etc.++> meta net (i, (TwoPin arity l, [_, (c, u)], _))+> (j, (bt, bp, _)) = +> case (l, bt) of+> ("fst", Constructor "T") -> Just $ project 1+> ("snd", Constructor "T") -> Just $ project 2+> (_, Single m) -> Just $ applyFunc m+> _ -> Nothing+> where+> project n =+> let (d, v) = bp !! n+> (e, w) = bp !! (3 - n)+> maxID = maximum (keys net)+> f = maxID + 1+> f_ = (Eraser, [(e, w)], Nothing)+> in (adjust (\ (ct, cp, cv) -> (ct, replace u (d, v) cp, cv)) c .+> adjust (\ (dt, dp, dv) -> (dt, replace v (c, u) dp, dv)) d .+> adjust (\ (et, ep, ev) -> (et, replace w (f, 0) ep, ev)) e .+> insert f f_ . delete i . delete j) net+> applyFunc m =+> let maxID = maximum (keys net)+> l' = "(" ++ l ++ " " ++ m ++ ")"+> f = maxID + 1+> f_ = (Abstractor, [(c, u), (i, 1), (i, 0)], Nothing)+> in if arity == 1 +> then (adjust (\ (at, ap, av) -> (Single l', [(c, u)], av)) i .+> adjust (\ (ct, cp, cv) -> (ct, replace u (i, 0) cp, cv)) c .+> delete j) net+> else (adjust (\ (at, ap, av) -> (TwoPin (arity - 1) l', [(f, 2), (f, 1)], av)) i .+> adjust (\ (ct, cp, cv) -> (ct, replace u (f, 0) cp, cv)) c .+> insert f f_ . delete j) net++> meta net a b@(_, (TwoPin _ _, _, _)) = meta net b a+> meta _ _ _ = Nothing++a pretty printer for generalized lambda terms.++> show' (x:xs) vars Z = x+> show' (x:xs) vars (S t) = show' xs vars t+> show' env (v:vs) (Abs t) = "(\\" ++ v ++ "." ++ show' (v:env) vs t ++ ")"+> show' env vars (App t t') = "(" ++ show' env vars t ++ " " ++ show' env vars t' ++ ")"+> show' env vars (Y t) = "Y(\\" ++ show' env vars t ++ ")"+> show' env vars (Tup t t') = "(" ++ show' env vars t ++ ", " ++ show' env vars t' ++ ")"+> show' env vars (Fst t) = "(fst " ++ show' env vars t ++ ")"+> show' env vars (Snd t) = "(snd " ++ show' env vars t ++ ")"+> show' env vars (VInt i) = show i+> show' env vars (VStr s) = show s+> show' env vars (VFunc i s t) = s ++ "(" ++ show' env vars t ++ ")"++> pretty = show' [] freshVars++Fresh variables++> freshVars = atoz ++ map (\[x,y]->y++x) (sequence [nats, atoz])+> where+> atoz = map (\x -> ['_', x]) ['a' .. 'z']+> nats = map show [0..]+
+ src/Main.lhs view
@@ -0,0 +1,552 @@+The main program for Lambdascope++> {-# LANGUAGE RecursiveDo #-}++> 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++> main = do+> GLFW.initialize+> initWindow w h+> showHelp <- newIORef False+> GLFW.charCallback $= \c b -> when ((c == 'H' || c == 'h') && b == GLFW.Release) +> (modifyIORef showHelp not)+> factor <- newIORef (0, 0, 1.0)+> netRef <- newIORef net+> loop showHelp factor (handleUserAction factor (keyHandle 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+> loop showHelp factor 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 showHelp factor handle'++> 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 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)]+> handle k d r = do+> net <- readIORef netRef+> 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 = mdo+> 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 = mdo+> 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 t2 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 n f x = App (Abs (app' n f x)) f +> app' 0 f x = x+> app' n f x = App Z (app (n - 1) Z 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)))+