diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2009 Paul H. Liu + +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. diff --git a/LambdaINet.cabal b/LambdaINet.cabal new file mode 100644 --- /dev/null +++ b/LambdaINet.cabal @@ -0,0 +1,26 @@ +name: LambdaINet +version: 0.1.0 +homepage: not available +maintainer: Paul H. Liu +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 + diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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 + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,6 @@ +module Main (main) where + +import Distribution.Simple (defaultMain) + +main :: IO () +main = defaultMain diff --git a/data/font.tga b/data/font.tga new file mode 100644 Binary files /dev/null and b/data/font.tga differ diff --git a/src/Diagram.lhs b/src/Diagram.lhs new file mode 100644 --- /dev/null +++ b/src/Diagram.lhs @@ -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 + diff --git a/src/INet.lhs b/src/INet.lhs new file mode 100644 --- /dev/null +++ b/src/INet.lhs @@ -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) + diff --git a/src/Lambda.lhs b/src/Lambda.lhs new file mode 100644 --- /dev/null +++ b/src/Lambda.lhs @@ -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..] + diff --git a/src/Main.lhs b/src/Main.lhs new file mode 100644 --- /dev/null +++ b/src/Main.lhs @@ -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))) +