LambdaINet 0.1.2.1 → 0.2.0.0
raw patch · 7 files changed
+1439/−813 lines, 7 filesdep +GLFW-taskdep +monad-taskdep +transformersdep ~containers
Dependencies added: GLFW-task, monad-task, transformers, vector
Dependency ranges changed: containers
Files
- LambdaINet.cabal +4/−3
- README +3/−0
- src/Diagram.lhs +479/−404
- src/Grid.lhs +143/−0
- src/INet.lhs +437/−177
- src/Lambda.lhs +36/−31
- src/Main.lhs +337/−198
LambdaINet.cabal view
@@ -1,5 +1,5 @@ name: LambdaINet-version: 0.1.2.1+version: 0.2.0.0 homepage: not available maintainer: Paul H. Liu <paul@thev.net> cabal-version: >= 1.6@@ -20,7 +20,8 @@ executable LambdaINet Main-is: Main.lhs- Other-Modules: Diagram INet Lambda- Build-Depends: base >= 3 && < 5, OpenGL, GLFW >= 0.5.0.0, containers, mtl+ Other-Modules: Diagram INet Lambda Grid+ Build-Depends: base >= 3 && < 5, OpenGL, GLFW >= 0.5.0.0, containers >= 0.5.0.0, mtl, transformers, monad-task, GLFW-task, vector Hs-Source-Dirs: src+ ghc-options: -rtsopts
README view
@@ -12,6 +12,9 @@ CHANGES ======= +* Tue Sep 1 PDT 2014 - New GUI based on GLFW-task, new layout algorithm.+ bump version to 0.2.0.0.+ * Tue Sep 15 EDT 2009 - fix GUI on OS X; fix glitch when moving nodes. bump version to 0.1.2.
src/Diagram.lhs view
@@ -6,40 +6,92 @@ Everything is aligned on a grid with a unit scale. -> module Diagram where+> {-# LANGUAGE NoMonomorphismRestriction #-}+> module Diagram +> ( Atom(..)+> , Port(..)+> , Diagram(..)+> , Direction(..) +> , Dirty(..)+> , HLSet+> , Frame+> , M+> , unit, unit'+> , margin+> , initWindow+> , setupEvents+> , setDiagram+> , modifyDiagram+> , getDiagram+> , getFont+> , getFactor+> , getDirty+> , whenDirty+> , setDirty+> , renderString+> , renderText+> , renderFrame+> , renderDiagram+> , emptyFrame+> , betweenFrame +> , vector3+> , color3+> , drawApplicator+> , drawAbstractor+> , drawDelimiter+> , drawDuplicator+> , drawCycle+> , drawEraser+> , drawTwoPin+> , drawSingle+> , autoAdjust+> ) where > import qualified Graphics.UI.GLFW as GLFW > import qualified Graphics.Rendering.OpenGL as GL+> import qualified Graphics.Rendering.OpenGL.GL.Texturing.Objects as TO > import Graphics.Rendering.OpenGL (($=), GLclampf, GLfloat) -> import Data.IntMap as IntMap hiding (filter, map)-> import qualified Data.Set as Set +> import qualified Data.Vector.Unboxed as UV +> import qualified Data.Set as Set+> import qualified Data.Map as Map +> import qualified Data.IntMap as IntMap +> import Data.List (sortBy, elemIndex)+> import Data.Complex > import Data.IORef > import Data.Maybe (fromMaybe, fromJust)--> import System.IO.Unsafe+> import Control.Arrow (first, second)+> import Control.Monad+> import Control.Monad.Trans+> import Control.Monad.Trans.State+> import Control.Monad.IO.Class+> import Control.Monad.Task+> import Graphics.UI.GLFW.Task+> import Debug.Trace+> import Grid > import Data.Bits ( (.&.) ) > import Foreign ( withArray ) > import Paths_LambdaINet (getDataFileName) -debugger +> type Font = TO.TextureObject -> debug = seq . unsafePerformIO . (putStrLn $!!)-> debug1 s v = seq (unsafePerformIO $ putStrLn $!! (s ++ show v)) v-> ($!!) f s = seq (length s) (f s)+> type Color = (GLfloat -> GL.Color4 GLfloat) -> IO () > data Atom = Atom { > atomID :: Int, > atomLabel :: String, > atomPorts :: [Port], > atomSize :: Size,-> atomDraw :: IO () -- drawing procedure+> atomDraw :: Color -> Font -> IO () -- drawing procedure > } > instance Eq Atom where > a == b = atomID a == atomID b +> instance Ord Atom where+> compare a b = atomID a `compare` atomID b+ > instance Show Atom where > show a = "(id=" ++ show (atomID a) ++ ", label=" ++ atomLabel a ++ > ", ports=" ++ show (atomPorts a) ++ ", size=" ++ @@ -55,23 +107,35 @@ > instance Eq Port where > p == q = (owner p == owner q) && (portPos p == portPos q) +> instance Ord Port where+> compare p q = case owner p `compare ` owner q of+> EQ -> portPos p `compare` portPos q+> r -> r+ > instance Show Port where > show p = "(" ++ show (atomID (owner p)) ++ "-" ++ > show (atomID (owner (portEnd p))) ++ > ", dir=" ++ show (portDir p) ++ ")" +> data Direction = N | W | S | E deriving (Show, Eq, Enum, Ord)+> type Position = (Float, Float)+> type Size = (Float, Float) -- radius in X and Y direction++> portdir' :: Direction -> Port -> Direction > portdir' d p = > let a = owner p > in toEnum ((fromEnum (portDir p) + fromEnum d) `mod` 4) >-> portdir posMap p = +> portdir :: Monad m => Port -> GridT Direction m Direction+> portdir p = do > let a = owner p-> d = maybe N snd (IntMap.lookup (atomID a) posMap)-> in portdir' d p+> d <- lookupNode (atomID a) >>= return . maybe N snd +> return $ portdir' d p >+> portpos' :: Direction -> Position -> Position > portpos' dir (x, y) = -> let r = sqrt $ fromIntegral (x * x + y * y)-> t = asin (fromIntegral y / r)+> let r = sqrt (x * x + y * y)+> t = asin (y / r) > t1 = if x < 0 then pi - t else t > in case dir of > N -> (x, y)@@ -79,94 +143,78 @@ > S -> vec r (t1 + pi) > E -> vec r (t1 - pi / 2) > where -> vec r t = (round (r * cos t), round (r * sin t))+> vec r t = (r * cos t, r * sin t) -> portpos posMap p = +> portpos :: Monad m => Port -> GridT Direction m Position+> portpos p = do > 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)+> d <- lookupNode (atomID a) >>= return . maybe N snd +> return $ portpos' d (portPos p) A graph consists of isolated components, which has a starting Atom. > data Diagram = Diagram { > startAtoms :: [Atom],-> allAtoms :: IntMap Atom+> allAtoms :: IntMap.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)+> emptyDiagram = Diagram [] IntMap.empty 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.+ 2. if its connecting Atom is not layed out, put it along the port direction. 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) = +> -- layoutByPort :: Monad m => [Port] -> GridT Direction m ()+> layoutByPort visited [] = return ()+> layoutByPort visited (p:ps) = do > 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)+> case IntMap.lookup j visited of+> Just _ -> layoutByPort visited ps+> Nothing -> do+> node <- lookupNode j +> case node of+> Just _ -> return ()+> Nothing -> do +> (((x, y), r), _) <- lookupNode i >>= return . fromMaybe (notFound "layoutByPort:" i)+> pd <- portdir p+> pp <- portpos p+> let qd = autorotate pd (portdir' N q)+> (xd, yd, dx, dy) = placement pd (portdir' qd q) pp (portpos' qd (portPos q))+> (bw, bh) = atomSize b+> rb = sqrt (bw * bw + bh * bh) / 2+> -- traceShow ("newNode", j) $+> newNode j (x + xd * (r + rb + realToFrac margin) + dx, y + yd * (r + rb + realToFrac margin) + dy) rb qd+> let ht = filter (/= q) (atomPorts b) +> layoutByPort (IntMap.insert i () visited) $ ht ++ ps +> interleave (x:xs) (y:ys) = x : y : interleave xs ys+> interleave [] ys = ys+> interleave xs [] = xs++> notFound msg i = error (msg ++ " atom " ++ show i ++ " not found")+ 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 N N (x1, y1) (x2, y2) = (signum x1, 0, x1 - x2, y1 - y2)+> placement N S (x1, y1) (x2, y2) = (0, 1, x1 - x2, 0)+> placement S S (x1, y1) (x2, y2) = (signum x1, 0, x1 - x2, y1 - y2)+> placement S N (x1, y1) (x2, y2) = (0, -1, x1 - x2, 0)+> placement E E (x1, y1) (x2, y2) = (0, signum y1, x1 - x2, y1 - y2)+> placement E W (x1, y1) (x2, y2) = (1, 0, 0, y1 - y2)+> placement W W (x1, y1) (x2, y2) = (0, signum y1, x1 - x2, y1 - y2)+> placement W E (x1, y1) (x2, y2) = (-1, 0, 0, y1 - y2) > placement _ _ _ _ = error "impossible placement: direction not match!" The autorotate function returns a rotation (with respect to N) such that the@@ -189,15 +237,16 @@ > autorotate S W = E > autorotate S S = S -> margin = 2-> unit = 12 :: GLfloat -- grid unit is 10 pixel+> margin = 3 +> unit = 12 :: Float -- grid unit in pixels+> unit' = realToFrac unit+> speed = 0.95 -- how fast it zooms > 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@@ -209,299 +258,306 @@ > 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!+> return (S0 font (row, col) (0,0,1) emptyDiagram Lightly) -> fontRef = unsafePerformIO (newIORef Nothing)-> rowcolRef = unsafePerformIO (newIORef (0, 0))+> setupEvents reduce = do+> fork $ forever $ watch onRefresh >> setDirty Lightly+> fork $ forever $ watch onSize >>= reshape+> fork $ forever $ handleLeftButton reduce+> fork $ forever $ handleZoom+> fork $ forever $ handleKeys+> fork $ watch (onKey >=> isPress >=> isKey GLFW.ESC) >> exit+> fork $ watch onClose >> exit > reshape (GL.Size w h) = do-> GL.viewport $= (GL.Position 0 0, GL.Size (fromIntegral w) (fromIntegral h))-> GL.matrixMode $= GL.Projection-> GL.loadIdentity+> liftIO $ 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)+> liftIO $ GL.ortho2D (-c) c (-r) r+> modifyRowCol $ const (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)+> data Dirty = None | Lightly | Dirty deriving (Eq, Show, Enum, Ord) -The following is a very naive but fast line layout algorithm.+> data S = S0 { font :: Font+> , rowcol :: (Float, Float)+> , factor :: (Float, Float, Float)+> , diagram :: Diagram+> , dirty :: Dirty+> }+> +> type M m a = TaskT Event (GridT Direction (StateT S m)) a -> 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+> modifyRowCol f = lift $ lift $ modify $ \s -> s { rowcol = f (rowcol s), dirty = Lightly } +> modifyFactor f = lift $ lift $ modify $ \s -> s { factor = f (factor s), dirty = Lightly } +> modifyDiagram f = lift $ lift $ modify $ \s -> s { diagram = f (diagram s), dirty = Dirty } +> setDiagram = modifyDiagram . const+> getFont = lift $ lift $ fmap font get +> getRowCol = lift $ lift $ fmap rowcol get +> getFactor = lift $ lift $ fmap factor get +> getDiagram = lift $ lift $ fmap diagram get +> getDirty = lift $ lift $ fmap dirty get +> setDirty d = lift $ lift $ modify $ \s -> s { dirty = d }+> whenDirty f = do+> d <- lift $ lift $ fmap dirty get+> when (d /= None) f -> 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+To support animating the "morphism" between two diagrams, we render each diagram+into a Frame. -> running grid l = running' l+> data Frame = Frame +> { objs :: IntMap.IntMap (Atom, GLfloat, GLfloat, GLfloat, GLfloat) -- (atom, x, y, rotation, alpha)+> , wires :: Map.Map (Port, Port) (Wire, GLfloat) -- wire between ports+> } deriving (Eq, Show)++> emptyFrame = Frame IntMap.empty Map.empty++> type Wire = UV.Vector (Float, Float)++> wirePoints = 15 -- number of line connecting points in every wire++We can morph a frame into another by compute a frame in between based on+a ratio between 0 (same as f0) and 1 (same as f1).++> betweenFrame (Frame objs wires) (Frame objs' wires') t = Frame obs wis > 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+> obs = IntMap.mergeWithKey bothO leftO rightO objs objs'+> wis = Map.mergeWithKey bothW leftW rightW wires wires'+> bothO _ (i, x, y, r, a) (j, x', y', r', a') | atomPorts i == atomPorts j = Just (j, x %% x', y %% y', r %%% r', a %% a')+> | otherwise = Just (j { atomDraw = drawBoth }, x %% x', y %% y', r', t)+> where drawBoth _ f = do+> GL.preservingMatrix (GL.rotate (r - r') (vector3 0 0 1) >> +> atomDraw i (GL.color . ($ (1 - t))) f)+> GL.preservingMatrix (atomDraw j (GL.color . ($ t)) f) +> leftO = IntMap.map (\(i, x, y, r, _) -> (i, x, y, r, 1 - t)) +> rightO = IntMap.map (\(i, x, y, r, _) -> (i, x, y, r, t)) +> bothW _ (us, _) (vs, _) = Just (UV.zipWith (\(x, y) (x', y') -> (x %% x', y %% y')) us vs, 1)+> leftW = Map.map (\(w, _) -> (w, 1 - t))+> rightW =Map.map (\(w, _) -> (w, t))+> x %% y = x * (1 - t') + y * t'+> r %%% r' = if r' > r then if r' - r > 180 then r %% (r' - 360) else r %% r'+> else if r - r' > 180 then r %% (r' + 360) else r %% r'+> t' = realToFrac t -> iterateList :: [[a]] -> [[a]]-> iterateList l = [ zipWith (!!) l idx | idx <- dia (length l) 0 ]+Sometimes it is useful to highlight a set of wires when we render the frame. -> dia d n = dia' d n ++ dia d (n + 1)+> type HLSet = Set.Set ((Int, Int), (Int, Int)) -- A pair of (atomID, portIndex) +> elemHLSet (p, q) s = Set.member (getIdx p, getIdx q) s+> where getIdx p = (atomID a, u)+> where a = owner p+> u = maybe (-1) id $ elemIndex p (atomPorts a)++> renderFrame font hlset (Frame objs wires) = do+> IntMap.fold ((>>) . drawObj) (return ()) objs+> Map.foldWithKey ((.) (>>) . drawWire) (return ()) wires > where-> dia' 1 n = [[n]]-> dia' d n = [ u : v | u <- [0 .. n], v <- dia' (d - 1) (n - u)]+> drawObj (a, x, y, d, c) = GL.preservingMatrix $ do+> GL.translate (vector3 x y 0) +> GL.rotate d (vector3 0 0 1)+> atomDraw a (GL.color . ($ c)) font +> drawWire pq@(p, q) (lines, c) = do+> let i = atomID $ owner p+> j = atomID $ owner q+> (_, _, _, _, a) = objs IntMap.! i+> (_, _, _, _, b) = objs IntMap.! j+> GL.preservingMatrix $ GL.color (linecolor c) >> polyline lines +> when (elemHLSet pq hlset) $ GL.preservingMatrix $+> GL.translate (vector3 1 1 0) >> GL.color (linecolor c) >> polyline lines -> 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+> renderDiagram :: MonadIO m => Diagram -> M m Frame +> renderDiagram d = lift $ do+> let atoms = allAtoms d+> existing <- getGrid+> let removed = foldr IntMap.delete existing $ IntMap.keys (allAtoms d)+> mapM_ removeNode $ IntMap.keys removed+> mapM_ layoutAtoms (startAtoms d)+> nodes <- getGrid+> let newNodes = foldr IntMap.delete nodes $ IntMap.keys existing+> adjustNodes atoms nodes+> nodes <- getNodes+> let nodes' = map (fst . snd) nodes+> foldl ((. drawAtom nodes' atoms) . (>>=)) (return emptyFrame) nodes +> where+> layoutAtoms a = do+> let i = atomID a+> (wa, ha) = atomSize a+> r = sqrt (wa * wa + ha * ha) / 2+> mx <- getNodes >>= return . maximum . (0:) . map (fst . fst . fst . snd) +> lookupNode i >>= maybe (newNode i (mx, 0) r N) (\_ -> return ())+> layoutByPort IntMap.empty $ atomPorts a+> drawAtom nodes atoms (i, (((x, y), _), o)) (Frame objs wires) = do+> let a = fromMaybe (notFound "drawAtom:" i) $ IntMap.lookup i atoms+> let objs' = IntMap.insert i (a, realToFrac x, realToFrac y, realToFrac (90 * fromEnum o), 1) objs+> let cond i j p q = i < j || (i == j && portPos p <= portPos q)+> lines <- linesFromAtom cond lineSeg (i, a, o, x, y)+> let wires' = foldr (\(k, w) ws -> Map.insert k (polyBezier w, 1) ws) wires lines+> return $ Frame objs' wires'+> where+> lineSeg id x y x' y' pd qd = (id, +> (x, y) : navigate nodes (x + px', y + py') (x' + qx', y' + qy') ++ [(x', y')])+> where (px', py') = extend pd+> (qx', qy') = extend qd -> 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+> linesFromAtom cond f (i, a, o, x, y) = sequence +> [ do let pd = portdir' o p+> (px, py) = portpos' o (portPos p)+> qd <- portdir q+> (qx, qy) <- portpos q+> (x', y') <- lookupNode j >>= return . maybe (notFound "sequence line:" j) (fst . fst)+> return $ f (p, q) (x + px) (y + py) (x' + qx) (y' + qy) pd qd+> | p <- atomPorts a,+> let q = portEnd p,+> let j = atomID (owner q),+> cond i j p q ] +Adjust the rotation of each node to make lines "more straight". -> data UserAction = UserAction (IO (UserAction, IO ()))+> adjustNodes atoms = sequence_ . map adjustAtom . IntMap.keys+> where+> adjustAtom i = do+> let a = fromMaybe (notFound "adjustNodes:" i) $ IntMap.lookup i atoms+> ds = [ N, W, S, E ]+> cond _ _ _ _ = True+> (x, y) <- lookupNode i >>= return . fst . fst . fromMaybe (notFound "impossible1" i)+> weighted <- sequence [ linesFromAtom cond (const lineDis) (i, a, o, x, y) >>= return . sum | o <- ds ]+> let sorted = sortBy (\u v -> compare (snd u) (snd v)) $ zip ds weighted +> w = head $ sorted+> modifyNodeVal i $ \d -> if fromMaybe (notFound "impossible2" d) (lookup d sorted) - snd w > 0.1 then fst w else d+> lineDis x0 y0 x1 y1 pd qd = dis (x0, y0) (x1, y1)+> -- dis (x0, y0) (x0', y0') + dis (x0', y0') (x1', y1') + dis (x1', y1') (x1, y1)+> where (px', py') = extend pd+> (qx', qy') = extend qd+> x0' = x0 + px'+> y0' = y0 + py'+> x1' = x1 + qx'+> y1' = y1 + qy'+> dis (x0, y0) (x1, y1) = sqrt (dx * dx + dy * dy)+> where dx = x0 - x1+> dy = y0 - y1 -> 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+> extend N = ( 0, 1)+> extend S = ( 0, -1)+> extend W = (-1, 0)+> extend E = ( 1, 0)++> navigate nodes (x0,y0) (x1, y1) = +> case (backTo . sorted . collided . relative) nodes of+> [] -> [(x0,y0),(x1,y1)]+> node@((x2,y2),r):_ -> +> if abs (x0 - x1) < 1e-4 && abs (y0 - y1) < 1e-4 +> then [(x0, y0)]+> else +> case midPoint node (x0,y0) (x1,y1) of+> Just (x3, y3) -> navigate nodes (x0,y0) (x3,y3) ++ navigate nodes (x3,y3) (x1,y1)+> Nothing -> [(x0,y0), (x1,y1)] > 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+> (p, a) = polar $ toC (x1, y1)+> fromC (x :+ y) = (x + x0, y + y0)+> toC (x, y) = (x - x0) :+ (y - y0)+> backTo = map (\((p, t), d) -> (fromC $ mkPolar p (t + a), d))+> sorted = sortBy (\u v -> compare (snd $ fst u) (snd $ fst v)) . +> map (\(c, d) -> (polar c, d))+> collided = filter (\(x :+ y, d) -> x >= 0 && x <= p && y >= -(d+tolerance) && y <= (d+tolerance))+> relative = map ((\((r, b), d) -> (mkPolar r (b - a), d)) . first (polar . toC)) -> 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)+> tolerance = margin / 5 -> 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)+> midPoint ((x0,y0),d) (x1,y1) (x2,y2) = +> let (p, a) = polar $ toC (x1, y1)+> (q, b) = polar $ toC (x2, y2)+> d' = d + tolerance + tolerance+> a' = acos (d'/p) `or` acos (d/p)+> b' = acos (d'/q) `or` acos (d/q)+> t = ((a + b) - a' + b') / 2+> t' = ((a + b) - b' + a') / 2+> r = d' / cos (t - b' - b)+> r' = d' / cos (t' - a' - a)+> in if isNaN a' || isNaN b' then Nothing+> else case (isNaN r, isNaN r') of+> (True, True) -> Nothing+> (False, True) -> Just $ fromC $ mkPolar r t+> (True, False) -> Just $ fromC $ mkPolar r' t'+> _ -> Just $ fromC $ if abs r + 0.01 < abs r' then mkPolar r t else mkPolar r' t'+> where+> fromC (x :+ y) = (x + x0, y + y0)+> toC (x, y) = (x - x0) :+ (y - y0)+> or x y = if isNaN x then y else x -> 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-> posMap' = adjust (\ ((x, y), d) -> ((ax', ay'), d)) i posMap -> r'@(_, render) = renderDiagram posMap' d-> 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)+> onLocated f g = do+> (GL.Position mx my) <- liftIO $ GL.get GLFW.mousePos+> (cx, cy, scale) <- getFactor+> (row, col) <- getRowCol +> let (w, h) = (col * unit, row * unit) +> x = (fromIntegral mx - w - cx) / scale / unit +> y = (h - fromIntegral my - cy) / scale / unit+> lift (locateNode (x, y)) >>= \i -> case i of +> [] -> g +> uid:_ -> f uid -> 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)+> handleLeftButton reduce = do+> watch (onButton >=> isPress >=> isButton GLFW.ButtonLeft)+> GL.Position mx my <- liftIO $ GL.get GLFW.mousePos+> onLocated (moveOrReduce (mx, my)) (shift (mx, my))+> where+> shift (mx, my) = do+> watch (onPos `orElse` (onButton >=> isRelease)) >>=+> either track (\_ -> return ())+> where+> track (GL.Position x y) = do+> let dx = 10 * fromIntegral (x - mx) / unit+> dy = 10 * fromIntegral (my - y) / unit+> modifyFactor $ \(cx, cy, scale) -> (cx - dx / scale, cy - dy / scale, scale)+> shift (x, y)+> moveOrReduce (mx, my) uid = do+> src <- lift getGrid+> (ax, ay) <- lift $ lookupNode uid >>= return . maybe (notFound "moveOrReduce:" uid) (fst . fst)+> watch (onPos `orElse` (onButton >=> isRelease)) >>=+> either (move src ax ay) (\_ -> reduce uid >> setDirty Dirty)+> where+> move src ax ay (GL.Position x y) = do+> (_, _, scale) <- getFactor+> let ax' = ax + (realToFrac (x - mx) / scale / unit)+> ay' = ay + (realToFrac (my - y) / scale / unit)+> lift $ setGrid src+> lift $ modifyNodePos uid (\(_, r) -> ((ax', ay'), r))+> setDirty Lightly+> watch (onPos `orElse` (onButton >=> isRelease)) >>=+> either (move src ax ay) (\_ -> return ())+> +> handleKeys = do+> watch (onKey >=> isRelease >=> isKey ' ')+> autoAdjust +> +> handleZoom = do+> oz <- liftIO $ GL.get GLFW.mouseWheel+> z <- watch onWheel+> modifyFactor $ \(x, y, scale) -> (x, y, scale * (speed ** fromIntegral (oz - z))) -> 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))+> gridBounds :: Monad m => GridT Direction m (Float, Float, Float, Float)+> gridBounds = do+> pos <- getNodes >>= return . map (fst . snd)+> return $ foldr updateBounds (0,0,0,0) pos+> where+> updateBounds ((x, y), r) (x0, y0, x1, y1) = +> (min x0 (x - r), min y0 (y - r), max x1 (x + r), max y1 (y + r)) -> 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+> autoAdjust = do+> GL.Size w h <- liftIO $ GL.get GLFW.windowSize +> (x0, y0, x1, y1) <- lift $ gridBounds +> let cx = unit * (x0 + x1) / 2+> cy = unit * (y0 + y1) / 2 +> sx = (x1 - x0 + margin) * unit / realToFrac w+> sy = (y1 - y0 + margin) * unit / realToFrac h > ms = max sx sy > s = if ms < 1 then 1 else ms-> writeIORef factor (-cx / s, -cy / s, 1/s)+> modifyFactor $ const (-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 +> (c0, r0, c1, r1) <- gridBounds > l1 = [(x, r0, x, r1) | x <- [c0 .. c1]] > l2 = [(c0, y, c1, y) | y <- [r0 .. r1]] > GL.color gridcolor @@ -513,6 +569,7 @@ > 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 =@@ -521,17 +578,11 @@ > 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)+> locateAtom atoms mx my = do+> uids <- locateNode (mx, my) +> case uids of+> [] -> return Nothing+> i:_ -> return $ atoms IntMap.! i Some primilinary font support @@ -549,8 +600,8 @@ > x = fromIntegral (fromEnum c `quot` 16 * 8) / 128 > dx = 8 / 128 > dy = 16 / 256-> h = 16 / unit -> w = 8 / unit+> h = 16 / unit' +> w = 8 / unit' > GL.preservingMatrix $ GL.renderPrimitive GL.Quads (do > GL.texCoord (texCoord2 x y) > GL.vertex (vertex3 0 h 0)@@ -562,32 +613,32 @@ > GL.vertex (vertex3 w h 0)) > GL.translate (vector3 w 0 0) -> renderString s = do-> Just font <- readIORef fontRef+> renderString font s = do > 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)+> renderText font = mapM_ out . lines+> where out s = renderString font s >> GL.translate (vector3 0 (-1.25) 0) +> color4 = GL.Color4 :: GLfloat -> GLfloat -> GLfloat -> GLfloat -> GL.Color4 GLfloat > 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+> linecolor = color4 0 0 0 +> gridcolor = color4 0.9 0.9 0.9+> unitcolor = color4 0 0 0+> textcolor = color4 0 0 1+> portcolor = color4 1 0 0 The drawing routings for Nodes -> drawApplicator label = do-> GL.color unitcolor+> drawApplicator label color font = do+> 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)@@ -598,27 +649,27 @@ > GL.renderPrimitive GL.Lines (do > GL.vertex (vertex3 0 0 0) > GL.vertex (vertex3 0 (-0.5) 0))-> GL.color portcolor+> color portcolor > GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)-> GL.color unitcolor+> 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+> GL.translate (vector3 (-1.5 - 4 / unit') (-8 / unit') 0)+> renderString font label -> drawAbstractor label = do-> GL.color unitcolor+> drawAbstractor label color font = do+> 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+> color portcolor > GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)-> GL.color unitcolor+> color unitcolor > GL.translate (vector3 0 (-3) 0) > GL.renderPrimitive GL.Lines (do > GL.vertex (vertex3 0 0 0)@@ -629,11 +680,11 @@ > 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+> GL.translate (vector3 (-1.5 - 4 / unit') (- 8 / unit') 0)+> renderString font label -> drawDelimiter label = do-> GL.color unitcolor+> drawDelimiter label color font = do+> color unitcolor > GL.renderPrimitive GL.LineStrip (do > GL.vertex (vertex3 (-1) 0.2 0) > GL.vertex (vertex3 (-1) (-0.2) 0)@@ -647,14 +698,18 @@ > 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+> 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+> color unitcolor+> GL.translate (vector3 1.2 (1 - 8 / unit') 0)+> renderString font label -> drawDuplicator label = do-> GL.color unitcolor+> drawDuplicator = drawDuplicator' unitcolor+> drawCycle True = drawDuplicator' (color4 0 1 0)+> drawCycle False = drawDuplicator' (color4 0.5 1 0.5)++> drawDuplicator' labelColor label color font = do+> color unitcolor > GL.renderPrimitive GL.LineStrip (do > GL.vertex (vertex3 (-1.5) 1 0) > GL.vertex (vertex3 0 (-1) 0)@@ -674,36 +729,37 @@ > GL.renderPrimitive GL.Lines (do > GL.vertex (vertex3 0 0 0) > GL.vertex (vertex3 0 (-1) 0))-> GL.color portcolor+> 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+> color unitcolor+> GL.translate (vector3 (-4 / unit') (1 - 8 / unit') 0)+> color labelColor+> renderString font label -> drawEraser label = do-> GL.color unitcolor+> drawEraser label color font = do+> 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+> 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+> color unitcolor+> GL.translate (vector3 (- fromIntegral (length label * 4) / unit') (1.2 - 8 / unit') 0)+> renderString font label -> drawTwoPin label = do-> GL.color unitcolor+> drawTwoPin label color font = do+> 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+> color portcolor > GL.renderPrimitive GL.Polygon (circle 0.2 0.2 10)-> GL.color unitcolor+> color unitcolor > GL.translate (vector3 0 (-3) 0) > GL.renderPrimitive GL.Lines (do > GL.vertex (vertex3 0 0 0)@@ -712,20 +768,39 @@ > 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+> color textcolor+> GL.translate (vector3 (- fromIntegral (length label * 4) / unit') (1.5 - 8 / unit') 0)+> renderString font label -> drawSingle label = do-> GL.color unitcolor+> drawSingle label color font = do+> 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+> 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+> color textcolor+> GL.translate (vector3 (- fromIntegral (length label * 4) / unit') (- 1.5 - 8 / unit') 0)+> renderString font label +> polyline = GL.renderPrimitive GL.LineStrip . UV.mapM_ draw+> where+> draw (x, y) = GL.vertex (vertex3 (realToFrac x) (realToFrac y) 0)+> +> polyBezier [] = UV.empty+> polyBezier ps = UV.map (bezier ps) segs+> where+> size = wirePoints - 1 -- floor (lineLength ps / margin * 10)+> segs = UV.generate (size + 1) $ \i -> if i < size then fromIntegral i / fromIntegral size else 1+> lineLength ((x1,y1):(x2,y2):ps) = +> let dx = x2 - x1+> dy = y2 - y1+> in sqrt (dx * dx + dy * dy) + lineLength ((x2,y2):ps)+> lineLength _ = 0+>+> bezier [(x1,y1)] t = (x1, y1)+> bezier [(x1,y1),(x2,y2)] t = (x1 + ((x2 - x1) * t), +> y1 + ((y2 - y1) * t))+> bezier ps t = bezier (map (\ (p, q) -> bezier [p,q] t) (zip ps (tail ps))) t
+ src/Grid.lhs view
@@ -0,0 +1,143 @@+Grid Layout+====++We implement a simple and robust layout algorithm for drawing interaction nets.+We guarantee a minimum distance between any two nodes, and dynamic addition and+deletion of nodes should bring minimal changes to existing layout. All nodes+and lines are aligned to grids.++Layout computation is encapsulated in a monad transformer, and thus is easy+to compose with other parts of the program.++> {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances, +> StandaloneDeriving, GeneralizedNewtypeDeriving, TupleSections #-}+> module Grid +> ( GridT+> , GridMap+> , Pos+> , Radius+> , evalGridT+> , evalGridT_+> , getGrid+> , setGrid+> , modifyGrid+> , clearGrid+> , getNodes+> , lookupNode+> , locateNode+> , modifyNodeVal+> , modifyNodePos+> , newNode+> , removeNode+> ) where++> import qualified Data.IntMap as M+> import Data.Complex+> import Control.Arrow (first, second, (***))+> import Control.Monad.State +> import Data.List (sortBy)++> type Uid = M.Key+> type Radius = Float+> type Pos = (Float, Float)+> type GridMap v = M.IntMap ((Pos, Radius), v)++> data S a = S { spacing :: Float, grid :: a }+> +> newtype GridT v m a +> = GridT (StateT (S (GridMap v)) m a)+> deriving (Functor, Monad, MonadTrans) +>+> deriving instance Monad m => MonadState (S (GridMap v)) (GridT v m)+> deriving instance MonadIO m => MonadIO (GridT v m)++> clearGrid :: Monad m => GridT v m ()+> clearGrid = modify $ \s -> s { grid = M.empty }++> getGrid :: Monad m => GridT v m (GridMap v)+> getGrid = get >>= return . grid+> modifyGrid f = modify $ \s -> s { grid = f (grid s) }+> modifyGrid' f = modify $ \s -> s { grid = f (spacing s) (grid s) }+> setGrid :: Monad m => GridMap v -> GridT v m ()+> setGrid = modifyGrid . const++> evalGridT :: Monad m => GridT v m a -> Float -> GridMap v -> m a+> evalGridT (GridT m) space grid = evalStateT m $ S space grid++> evalGridT_ :: Monad m => GridT v m a -> Float -> m a+> evalGridT_ m space = evalGridT m space M.empty ++> getNodes :: Monad m => GridT v m [(Uid, ((Pos, Radius), v))]+> getNodes = getGrid >>= return . M.toList ++> lookupNode :: Monad m => Uid -> GridT v m (Maybe ((Pos, Radius), v))+> lookupNode uid = getGrid >>= return . M.lookup uid ++> locateNode :: Monad m => Pos -> GridT v m [Uid]+> locateNode (x0, y0) = getGrid >>= return . M.keys . M.filter (inside . fst)+> where +> inside ((x, y), r) = sqrt (dx * dx + dy * dy) < r+> where +> dx = x - x0 +> dy = y - y0++> modifyNodeVal :: Monad m => Uid -> (v -> v) -> GridT v m ()+> modifyNodeVal uid f = modifyGrid (M.alter (fmap (second f)) uid)++> modifyNodePos :: Monad m => Uid -> ((Pos, Radius) -> (Pos, Radius)) -> GridT v m Bool+> modifyNodePos uid f = do+> modifyGrid (M.alter (fmap (first f)) uid)+> m <- getGrid+> maybe (return False) (\n -> modifyGrid' (`adjust` (fst n)) >> return True)+> (M.lookup uid m)+> where+> adjust spacing ((x0, y0), r0) = +> M.fromList . map (fromPolar x0 y0) . +> balanceList spacing . sortByDistance . +> map (toPolar x0 y0) . M.toList ++> newNode :: Monad m => Uid -> Pos -> Radius -> v -> GridT v m ()+> newNode uid (x0, y0) rad v = modifyGrid' insert+> where+> newNode = (uid, (((0, 0), rad), v))+> insert spacing = M.fromList . map (fromPolar x0 y0) . +> foldl (balance spacing) [newNode] . sortByDistance . +> map (toPolar x0 y0) . M.toList ++> removeNode :: Monad m => Uid -> GridT v m Bool+> removeNode uid = getGrid >>=+> maybe (return False) (\_ -> modifyGrid (M.delete uid) >> return True) +> -- maybe (return False) (\n -> modifyGrid' (`delete` (fst n)) >> return True) +> . M.lookup uid +> where+> delete spacing ((x0, y0), r0) = M.fromList . map (fromPolar x0 y0) . +> balanceList spacing . tail . sortByDistance . +> map (shorten . toPolar x0 y0) . M.toList+> where +> shorten = modPos $ \d -> d - r0 - spacing / 2++> modPos = second . first . first . first++> balanceList spacing (x:xs) = foldl (balance spacing) [x] xs+> balanceList spacing [] = []++> balance spacing l p = foldl improve p l : l+> where +> improve u@(i, (((r, a), r0), _)) v@(_, (((r', a'), r1), _)) = +> if d > minD then u else modPos (const r'') u+> where +> d = r' * sin (a' - a)+> s = sqrt (minD * minD - d * d)+> t = r' * cos (a' - a)+> st = s + t +> r'' = if st > r then st else r+> minD = spacing + r0 + r1+>+> sortByDistance = sortBy $ \u v -> compare (p u) (p v)+> where p = fst . fst . fst . snd++> toPolar x0 y0 = second $ first $ first (polar . toC (x0, y0))+> toC (x0, y0) (x, y) = (x - x0) :+ (y - y0)++> fromPolar x0 y0 = second $ first $ first (fromC (x0, y0) . uncurry mkPolar)+> fromC (x0, y0) c = (x0 + realPart c, y0 + imagPart c)
src/INet.lhs view
@@ -1,19 +1,26 @@ Interactive Net for Lambdascope implmenetation +> {-# LANGUAGE TupleSections #-} > module INet where > import Diagram -> import Data.IntMap as IntMap hiding (filter, map)-> import Data.Maybe (fromJust)+> import Data.IntMap as IntMap hiding (filter, map, foldl, foldr)+> import Data.Monoid (Monoid, mappend, mconcat, mempty)+> import Data.Maybe (fromJust, fromMaybe)+> import Data.List (mapAccumR) > import Control.Monad.State+> import Control.Arrow (first)+> import Debug.Trace 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+> type INetMap = IntMap INetV+> type INet = (INetMap, Int) -- map of ID to INetV, and maxID+> emptyINet = (IntMap.empty, 0) :: INet A port is a pair of the other end's NodeID and port index. @@ -25,17 +32,17 @@ > | Abstractor > | Delimiter > | Delimiter' -- flip of Delimiter-> | Duplicator-> | SuperDup -- dup everything+> | Duplicator DupKind > | Eraser > | Dummy -- dummy for self-loop > | Initiator -- never destroyed-> | Constructor String -- data constructor+> | Constructor String -- tuple constructor > | TwoPin Int String | TwoPin' Int String -- for meta function > | Single String | Single' String -- for meta value- > deriving (Eq, Show) +> data DupKind = Dup | Cycle Bool | Sup Bool deriving (Eq, Show) -- Normal, Recursive, Super+ > findInitiator [] = Nothing > findInitiator (a@(i, (Initiator, [(b, u)], Nothing)):as) = Just a > findInitiator (a:as) = findInitiator as@@ -43,13 +50,13 @@ netToDiagram :: Net -> Diagram > netToDiagram net = -> let list = toList net-> Just (init, _) = findInitiator list+> let list = toList $ fst net+> adjust = maybe id (\(init, _) -> (init:).filter(/=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+> adjust $ map fst list > in Diagram heads d > where > toAtom (i, (t, p, v)) = @@ -62,8 +69,7 @@ > Applicator' -> ("@", drawAbstractor) > Abstractor -> ("\x80", drawAbstractor) > Delimiter -> (maybe "" show (v::Maybe Int), drawDelimiter)-> Duplicator -> (maybe "" show (v::Maybe Int), drawDuplicator)-> SuperDup -> ("*", drawDuplicator)+> Duplicator k -> drawDup (maybe "" show (v::Maybe Int)) k > Eraser -> ("", drawEraser) > Initiator -> ("I", drawEraser) > Delimiter' -> ("S", drawTwoPin)@@ -72,16 +78,20 @@ > TwoPin' _ l -> (l, drawTwoPin) > Single l -> (l, drawSingle) > Single' l -> (l, drawSingle)+> drawDup l Dup = (l, drawDuplicator)+> drawDup l (Cycle k) = (l, drawCycle k)+> drawDup l (Sup False) = (" ", drawDuplicator)+> drawDup l (Sup True) = ("*", drawDuplicator) > toPort a t (m, (j, n)) = > let (d, p) = pos t m-> b = toAtom (j, (net ! j))+> b = toAtom (j, (fst 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)+> let (_, ps, _) = (fst d ! x) > js = map fst ps > ks = filter (flip notElem visited) js > in (x == i) || reachable d (x : visited) (xs ++ ks) i@@ -95,10 +105,9 @@ > 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 (Duplicator _) 0 = (S, (0, -2))+> pos (Duplicator _) 1 = (N, (1, 2))+> pos (Duplicator _) 2 = (N, (-1, 2)) > pos Eraser 0 = (S, (0, -2)) > pos Initiator 0 = (S, (0, -2)) > pos Delimiter' 0 = (N, (0, 2))@@ -109,136 +118,244 @@ > pos (Single _) 0 = (N, (0, 2)) > pos (Single' _) 0 = (N, (0, 2)) -> type LocalRule = INet -> (Int, INetV) -> (Int, INetV) -> Maybe INet+> type LocalRule = (Int, INetV) -> (Int, INetV) -> INet -> Maybe INet+> type LocalRuleM m = (Int, INetV) -> (Int, INetV) -> INet -> m (Maybe INet) > type Rule = INet -> (INet, Int)+> type RuleM m = INet -> m (INet, Int) Make a local rule global by applying it once everywhere. -> applyRule :: LocalRule -> Rule-> applyRule rule net = applyRule' 0 rule (keys net) net+> ruleM :: Monad m => LocalRule -> LocalRuleM m+> ruleM = (((return .) .) .) -> applyRule' :: Int -> LocalRule -> [Int] -> Rule-> applyRule' num rule [] net = (net, num)-> applyRule' num rule (i:rs) net = -> let a@(at, ap, av) = net ! i+> applyRule :: Monad m => LocalRuleM m -> RuleM m+> applyRule rule net = applyRule' 0 rule (keys $ fst net) net++> applyRule' :: Monad m => Int -> LocalRuleM m -> [Int] -> RuleM m+> applyRule' num rule [] net = return (net, num)+> applyRule' num rule (i:rs) net = do+> let a@(at, ap, av) = fst 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+> b@(bt, bp, bv) = fst net ! j+> net' <- rule (i, a) (j, b) net+> let rs' = filter (`member` (fst $ fromJust net')) rs +> if member i (fst net)+> then maybe (applyRule' num rule rs net) (applyRule' (num + 1) rule (filter (j/=) rs')) net' > else applyRule' num rule rs net repeatedly apply a rule until it is no longer applicable. +> repeatRule :: Monad m => RuleM m -> RuleM m > repeatRule = repeatRule' 0 -> repeatRule' :: Int -> Rule -> Rule-> repeatRule' sum rule net = -> let (net', num) = rule net-> in if num == 0 -> then (net, sum)+> repeatRule' :: Monad m => Int -> RuleM m -> RuleM m+> repeatRule' sum rule net = do+> (net', num) <- rule net+> if num == 0 +> then return (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+> outermost :: Monad m => LocalRuleM m -> RuleM m+> outermost rule net@(netMap, _) =+> case findInitiator $ toList netMap of > Just (i, _) -> outermost' [] [i]-> Nothing -> (net, 0)+> Nothing -> return (net, 0) > where -> outermost' _ [] = (net, 0)+> outermost' _ [] = return (net, 0) > outermost' visited (i:is) =-> let a@(at, ((j, _):ps), _) = net ! i -> b = net ! j+> let a@(at, ((j, _):ps), _) = netMap ! i +> b = netMap ! 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)+> then return (net, 0)+> else rule (i, a) (j, b) net >>= +> maybe (outermost' (i:visited) (j:is)) (\net -> return (net, 1)) +Similar to outermost, but it looks under lambda.++> outerReducible :: Monad m => LocalRuleM m -> RuleM m+> outerReducible rule net@(netMap, _) = reduce $ zip all (tail all)+> where +> all = traverse (\(i, u) a@(t, _, _) -> +> case (t, u) of +> (Duplicator (Cycle _), 1) -> []+> _ -> [(i, u, a)]) netMap+> reduce [] = return (net, 0)+> reduce (((i, _, a), (j, u, b@(_, bp, _))) : xs) = +> if u == 0 && i == fst (bp!!u) +> then rule (i, a) (j, b) net >>= maybe (reduce xs) (return . (,1))+> else reduce xs+ 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+> (->-) :: Monad m => LocalRuleM m -> LocalRuleM m -> LocalRuleM m+> (->-) r1 r2 a b net = do+> r1 a b net >>= maybe (r2 a b net) (return . Just) > infixr 5 +>+-> (+>+) :: Rule -> Rule -> Rule-> (+>+) r1 r2 net = -> let r@(net', n) = r2 net-> in if n == 0 then r1 net else r+> (+>+) :: Monad m => RuleM m -> RuleM m -> RuleM m+> (+>+) r1 r2 net = do+> r@(net', n) <- r1 net+> if n == 0 then r2 net else return r +> infixr 5 +&++> (+&+) :: Monad m => RuleM m -> RuleM m -> RuleM m+> (+&+) r1 r2 net = do+> r@(net', _) <- r1 net+> r2 net' +++> at f j net = f (j, fst net!j) net+ The cross rules: annihilate and commute. -> cross net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> cross :: LocalRule+> cross x@(i, a@(at, ap, av)) y@(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)+> then if match at bt && av == bv -- same type and value?+> then Just . annihilate (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)+> (Applicator, Abstractor) -> const Nothing -- leave the beta rule out+> (Abstractor, Applicator) -> const Nothing+> (Constructor _, TwoPin _ _) -> const Nothing -- leave the meta rule out+> (TwoPin _ _, Constructor _) -> const Nothing+> (Single _, TwoPin _ _) -> const Nothing -- FIXME: never cross single, but cross single'+> (TwoPin _ _, Single _) -> const Nothing+>-- (Initiator, Delimiter) -> Just . commute (i, a) (j, b) +>-- (Delimiter, Initiator) -> Just . commute (j, b) (i, a)+> (Initiator, _) -> const Nothing+> (_, Initiator) -> const Nothing+> (Duplicator (Cycle False), _) -> const Nothing+> (_, Duplicator (Cycle False)) -> const Nothing+> (Constructor _, Duplicator k) -> cross y x+> (Duplicator k, Constructor _) -> fmap (commute x y) . isSelector (tail ap)+> {-+> (Duplicator (Cycle _), Duplicator Dup) -> Just . +> (if bv == Just 0 then either (crossCycle x y) (commute x y) . +> reachable (ap!!1) (j, 1)+> else commute x y)+> -}+> _ -> Just . commute x y > 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+> (Duplicator (Sup True), Applicator, 2) -> Just . superDup (i, a) (j, b) +> (Duplicator (Sup True), TwoPin _ _, 1) -> Just . superDup (i, a) (j, b) +> (Duplicator (Sup True), Delimiter, 1) -> Just . superDup (i, a) (j, b) +> _ -> const Nothing+> where+> match (Duplicator _) (Duplicator _) = True+> match t t' = t == t' +> reachable p q m@(netMap, _) = check p+> where check p | p == q = Left m+> | otherwise = case netMap ! (fst p) of+> (_, [p0, p1], _) -> check (if snd p == 0 then p1 else p0)+> _ -> Right m+> isSelector xs m@(netMap, _) = check xs+> where+> check [] = Nothing+> check ((k, u):xs) = +> let (t, p, _) = netMap ! k +> more = check (xs ++ tail p)+> next = check xs+> in if u /= 0 then next+> else case t of+> Delimiter -> more+> Duplicator _ -> more+> TwoPin _ s -> if s == "fst" || s == "snd" then Just m+> else next+> _ -> next cross from rear -> superDup net (i, a) (j, b) = -> let Just net' = upsideDown net (j, b)-> net'' = commute net' (i, a) (j, net'!j)+> superDup (i, a) (j, b) net = +> let Just net' = upsideDown (j, b) net+> net'' = at (commute (i, a)) j net' > 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+> _ -> False) (toList $ fst net'')+> in foldr (\k net -> fromJust $ upsideDown (k, fst net!k) net) net'' ks +A special case where a Cycle duplicator meets a normal duplicator of level 0. +> crossCycle (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> let (x, p) = ap !! 2 +> (y, q) = bp !! 2+> in first (adjust (replaceP p (j, 0)) x . +> adjust (replaceP q (i, 0)) y . +> adjust (\_ -> (at, [(y, q), ap!!1, (j, 2)], av)) i .+> adjust (\_ -> (bt, [(x, p), bp!!1, (i, 2)], bv)) j)+> + The modified cross rule, only moves delimiter or annihilates. -> cross' net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> cross' (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)+> then Just . annihilate (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+> (Delimiter, _) -> Just . commute (i, a) (j, b) +> (_, Delimiter) -> Just . commute (i, a) (j, b) +> _ -> const Nothing+> else const Nothing -> annihilate net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) = +> {-++Sharing recovery by moving identical nodes from the rear of a duplicator+to the front.++> share :: LocalRule+> share (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) (netMap, maxID) = +> let (_, p) = head ap+> q = 3 - p+> (k, kp) = bp !! q+> (ct, cp, cv) = netMap ! k+> (d, dp) = ap !! 1+> (e, ep) = cp !! 1+> (f, fp) = bp !! 0+> n = maxID + 1+> in if bt == Duplicator && length ap == 2 && p > 0 && kp == 0 && ct /= Delimiter && ct == at && cv == av+> then Just ((insert n (at, [bp!!0, (j, 0)], av) .+> adjust (replaceP fp (n, 0)) f .+> adjust (replaceP ep (j, q)) e .+> adjust (replaceP dp (j, p)) d .+> adjust (replaceP 0 (n,1) . replaceP p (ap!!1) . replaceP q (cp!!1)) j .+> delete i . delete k) netMap, n)+> else if bt == Duplicator && at != Delimiter && length ap == 2 && p > 0 && kp == 0 +> then Just ((insert n (at, [bp!!q, (j, q)], av) .+> insert (n+1) (at, [bp!!0, (j, 0)], av) .+> adjust (replaceP fp (n+1, 0)) f .+> adjust (replaceP kp (n, 0)) k .+> adjust (replaceP dp (j, p)) d .+> adjust (replaceP 0 (n+1,1) . replaceP p (ap!!1) . replaceP q (n,1)) j .+> delete i) netMap, n + 1)+> else Nothing+> -}++> annihilate (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'+> in first $ flip (foldr zipup) pair' . delete i . delete j > 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+> zipup ((c, u), (d, v)) =+> adjust (replaceP u (d, v)) c .+> adjust (replaceP v (c, u)) d 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) .. ]+> commute (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) net@(netMap, maxID) = +> let bs = take (length ap - 1) $ [(maxID + 1) .. ] +> as = if at == Initiator then [j] else 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))@@ -246,158 +363,299 @@ > 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))+> : 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)) .+> at' = case (at, bt) of+> (Duplicator (Sup False), Abstractor) -> Duplicator (Sup True)+> (Duplicator (Cycle _), _) -> Duplicator (Cycle False) -- disable Cycle duplicator after commuting+> _ -> at+> bt' = case (bt, at) of +> (Duplicator (Sup False), Abstractor) -> Duplicator (Sup True)+> (Duplicator (Cycle _), _) -> Duplicator (Cycle False) -- disable Cycle duplicator after commuting+> _ -> bt+> in ((flip (foldr (\ (k, (c, u)) -> adjust (replaceP u (bs !! k, 0)) c)) (zip [0..] (tail ap)) .+> flip (foldr (\ (k, (c, u)) -> adjust (replaceP u (as !! k, 0)) c)) (zip [0..] (tail bp)) . > flip (foldr (uncurry insert)) (zip bs bs_) . > flip (foldr (uncurry insert)) (zip as as_) .-> delete i . delete j) net+> delete i . delete j) netMap, maximum $ maxID : (bs ++ as)) +> resetCycle :: LocalRule+> resetCycle (i, a@(Duplicator (Cycle False), p, v)) _ = +> Just . first (adjust (\_ -> (Duplicator (Cycle True), p, v)) i)+> resetCycle _ (i, a@(Duplicator (Cycle False), p, v)) = +> Just . first (adjust (\_ -> (Duplicator (Cycle True), p, v)) i)+> resetCycle _ _ = const Nothing++> {-++Fixed point operator BigY needs special treatment because we don't want to+unroll it more than once. The way to do this is to check its value, if it+is Nothing, then we don't unroll, otherwise unroll and change the value+to Nothing.++> unrollBigY (i, (yt, [(_, u), (c, v)], yv)) (j, (bt, bp, bv)) =+> maybe (const Nothing) (const unroll) yv+> where+> unroll :: INet -> Maybe INet+> unroll net@(netMap, maxID) = +> let (a, d) = (maxID + 1, maxID + 2)+> a_ = (Applicator, [(d, 2), (i, 1), (c, v)], Nothing)+> d_ = (Duplicator, [(j, u), (i, 0), (a, 0)], Just 0)+> y = (yt, [(d, 1), (a, 1)], Nothing)+> b' = (bt, replace u (d, 0) bp, bv)+> in Just ((adjust (replaceP v (a, 2)) c . +> adjust (\_ -> b') j . adjust (\_ -> y) i .+> insert a a_ . insert d d_) netMap, maxID + 2)+> -}+ 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 (i, a@(at, ap@((_, n):_), av)) (j, b@(bt, bp, bv)) =+> case (at, bt, bv, 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+> (Eraser, Duplicator k, Just 0, False) -> eraseSharing +>-- (Eraser, BigY _, False) -> eraseSharing +>-- (Eraser, SuperDup, False) -> eraseSharing+> (Eraser, _, _, True) -> eraseNode+> -- (Eraser, _, False) -> auxAreErasers >=> eraseNode +> _ -> const Nothing > where+> auxAreErasers :: INet -> Maybe INet+> auxAreErasers net@(netMap, _) = if all auxIsEraser (tail bp) then Just net else Nothing+> where auxIsEraser (n, _) = case netMap ! n of+> (Eraser, _, _) -> True+> _ -> False+> eraseSharing :: INet -> Maybe INet > 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+> in Just . first (delete i . delete j . +> adjust (replaceP u (d, v)) c .+> adjust (replaceP v (c, u)) d) +> eraseNode :: INet -> Maybe INet+> eraseNode (netMap, maxID) =+> let bp' = filter ((i/=) . fst) bp+> ibp = zip [(maxID + 1) ..] bp'+> ers = map (\(u, (n, v)) -> insert u (Eraser, [(n, v)], Nothing)) ibp+> adjustments = map (\(u, (n, v)) -> +> adjust (replaceP v (u, 0)) n) ibp+> in Just ((foldr (.) id ers . foldr (.) id adjustments . delete i . delete j) netMap, +> maxID + length bp') -The prune rule removes all trees without the initiator. This is necessary for-garbage collecting self-looping components.- +The prune rule removes all nodes that are not "reachable" from the initiator. +This is necessary for garbage collecting self-looping components.++The traversal itself is guided by a stack as outlined in the lambdascope paper+section 6.2.1.++> data Dir = L | R deriving (Eq, Show)+> type Stack = (Int, [Level])+> data Level = Level Block [Level] deriving Eq+> type Block = (Int, [Dir])+> +> showBlock (i, d) = show i ++ concatMap show d+> showLevel (Level b l) = showBlock b ++ showLevels l+> showStack (i, l) = show i ++ "," ++ showLevels l+> showLevels [] = ""+> showLevels (x@(Level _ l):xs) = let s = showLevel x in (if length s == 1 then id else paren) s ++ showLevels xs+> where paren s = "(" ++ s ++ ")"++> -- FIXME: prune is actually incorrect if implemented using traverse! > prune :: Rule-> prune net =-> let Just (i, a) = findInitiator (toList net)-> visited = visit [] [i]-> net' = filterWithKey (\k _ -> elem k visited) net-> in (net', 0)+> prune net@(netMap, maxID) =+> let +> visited = traverse (\x@(i, u) (t, _, _) ->+> case (t, u) of+> (Duplicator (Cycle _), 1) -> []+> _ -> [i]) netMap+> netMap' = length visited `seq` filterWithKey (\k _ -> elem k visited) netMap+> net' = fixUp (netMap', maxID)+> in (net', size netMap - size (fst net'))+> where+> fixUp' x = let x' = traceShow ("before fixup:", x) $ fixUp x+> in traceShow ("after fixup", x') x'+> fixUp (netMap, maxID) = foldWithKey adjust (IntMap.empty, maxID) netMap+> where+> adjust i (t, p, v) (m, maxID) = +> let ((m', maxID'), p') = mapAccumR addEraser (m, maxID) $ zip [0..] p+> in (insert i (t, p', v) m', maxID')+> where+> addEraser acc@(m, maxID) (q, x@(j, u)) = +> if member j netMap then (acc, x)+> else let n = maxID + 1+> in ((insert n (Eraser, [(i, q)], Nothing) m, n), (n, 0))+++A generic traversal guided by the stack:++1. It reaches all node that it is reachable from Initiator.++2. It does not avoid circles (introduced by Cycle duplicator), + so potentially it may produce result that is infinite. ++> traverse :: Monoid m => (NetPort -> INetV -> m) -> INetMap -> m+> traverse f netMap = -- traceShow "======" $ +> visit (i, 1) (0, [Level (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)- +> Just (i, _) = findInitiator (toList netMap)+> visit x@(n, u) s = +> let a@(at, p, av) = netMap ! n+> defaultVisit = if u == 0 +> then mconcat $ map (`visit` s) $ tail p+> else visit (p!!0) s+> -- defaultVisit = error "not handled"+> visited = case --traceShow (showStack s, (at, u, av)) $ +> (at, u, av, s) of+> (Initiator, _, _, _) -> visit (p!!0) s+> (Applicator, 2, _, _) -> visit (p!!0) s `mappend` visit (p!!1) s+> (Abstractor, 0, _, (i, l)) -> visit (p!!1) (i+1, (Level (i+1,[]) []):l)+> (Abstractor, _, _, _) -> mempty+> (Delimiter, 0, Just 0, (i, l)) -> visit (p!!1) (i, (Level (0,[]) []):l)+> (Delimiter, 1, Just 0, (i, k:l)) -> visit (p!!0) (i, l)+> (Delimiter, 0, Just i, s) -> +> let (i', l) = s+> Level b (k:l') = l !! (i - 1)+> s' = (i', take (i-1) l ++ [Level b l', k] ++ drop i l)+> in visit (p!!1) s'+> (Delimiter, 1, Just i, s) -> +> let (i', l) = s+> Level b l' = l !! (i - 1)+> k = l !! i +> s' = (i', take (i-1) l ++ [Level b (k:l')] ++ drop (i+1) l)+> in visit (p!!0) s'+> (Duplicator _, 0, Just i, s) ->+> let (i', l) = s+> Level b l' = l !! i+> in case b of+> (j, R:d) -> visit (p!!1) (i', replace i (Level (j,d) l') l)+> (j, L:d) -> visit (p!!2) (i', replace i (Level (j,d) l') l)+> _ -> error "invalid" +> (Duplicator t, q, Just i, s) ->+> let (i', l) = s+> Level (j, d) l' = l !! i+> d' = (if q == 1 then R else L) : d+> in visit (p!!0) (i', replace i (Level (j,d') l') l)+> _ -> defaultVisit+> in f x a `mappend` visited+ 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)+> disintegrate (i, a@(at, ap@[(b,l), (c,u), (d,v)], av)) net@(netMap, maxID) = +> let (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+> in ((adjust (const (Applicator, [(b, l), (d2, 0), (d1, 0)], Nothing)) i .+> adjust (replaceP u (d1, 1)) c .+> adjust (replaceP v (d2, 1)) d .+> insert d1 d1_ . insert d2 d2_) netMap, maxID + 2) The beta rule aplies when Applicator meets Abstractor. -> beta net (i, a@(at, ap, _)) (j, b@(bt, bp, _)) =+> beta (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+> (True, Applicator, Abstractor) -> Just . beta' (i, a) (j, b) +> (True, Abstractor, Applicator) -> Just . beta' (j, b) (i, a) +> _ -> const 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)+> beta' (i, a@(at, [_, (c,u), (d,v)], av))+> (j, b@(bt, [_, (e,x), (f,y)], bv)) net@(netMap, maxID) = +> let (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+> in ((adjust (replaceP u (d2, 0)) c .+> adjust (replaceP v (d1, 0)) d .+> adjust (replaceP x (d1, 1)) e .+> adjust (replaceP y (d2, 1)) f .+> insert d1 d1_ . insert d2 d2_ . delete i . delete j) netMap, maxID + 2) > replace :: Int -> a -> [a] -> [a] > replace _ _ [] = [] > replace 0 v (x:xs) = v : xs > replace i v (x:xs) = x : replace (i - 1) v xs +> replaceP i u (t, p, v) = (t, replace i u p, v)+ 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+> tryBoth :: ((Int, INetV) -> INet -> Maybe INet) -> LocalRule +> tryBoth rule a@(i,_) b@(j,_) net = +> maybe (rule b net) (\net' -> Just $ fromMaybe net' $ rule (j,(fst net'!j)) net') $ rule a net -> upsideDown net (i, a@(at, _, _)) = +> unwind = tryBoth unwind'+> unwind' a@(_, (Delimiter, _, _)) net = Nothing+> unwind' a@(_, (Delimiter', _, _)) net = Nothing+> unwind' a@(_, (TwoPin _ _, _, _)) net = Nothing+> unwind' a@(_, (TwoPin' _ _, _, _)) net = Nothing+> unwind' a@(_, (Applicator', _, _)) net = Nothing+> unwind' (i, a@(Single l, p, Nothing)) net = Just $ first +> (adjust (\_ -> (Single' l, p, Nothing)) i) net+> unwind' a net = upsideDown a net++> upsideDown (i, a@(at, _, _)) net = > case at of > Applicator -> > let (_, [(b,u), (c,v), (d, w)], _) = a -> in Just $+> in Just $ first > (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+> adjust (replaceP u (i, 1)) b .+> adjust (replaceP v (i, 2)) c .+> adjust (replaceP w (i, 0)) d) net > Applicator' -> > let (_, [(b,u), (c,v), (d, w)], _) = a -> in Just $+> in Just $ first > (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+> adjust (replaceP u (i, 2)) b .+> adjust (replaceP v (i, 0)) c .+> adjust (replaceP w (i, 1)) 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) = +> upsideDown' at' a@(_, [(b,u),(c,v)], av) = first > (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+> adjust (replaceP u (i, 1)) b .+> adjust (replaceP v (i, 0)) c) net -> scope net (i, a@(Delimiter, [(b, u), (c, v)], Just av)) _ = upsideDown net (i, a)-> scope _ _ _ = Nothing+> scope = tryBoth scope'+> scope' (i, a@(TwoPin _ _, _, _)) = upsideDown (i, a)+> scope' (i, a@(Delimiter, _, _)) = upsideDown (i, a)+> scope' _ = const Nothing -> loopcut net (i, a@(Abstractor, [(b, u), (c, v), (d, w)], Nothing)) _ = -> let maxID = maximum (keys net)-> (e, f) = (maxID + 1, maxID + 2)+> loopcut = tryBoth loopcut'+> loopcut' (i, a@(Abstractor, [(b, u), (c, v), (d, w)], Nothing)) (net, maxID) = +> let (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 (\ (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+> insert e e_ . insert f f_) net, maxID + 2) > else Nothing-> loopcut _ _ _ = Nothing+> loopcut' _ _ = Nothing -> readback = applyRule cross . fst . applyRule loopcut . fst . -> applyRule cross . fst . applyRule scope . fst . -> applyRule cross . fst . applyRule unwind+> readback :: Monad m => RuleM m+> readback = +> apply' unwind >=> return . fst >=> +> apply' cross >=> return . fst >=>+> apply' scope >=> return . fst >=>+> apply' cross >=> return . fst >=>+> apply' loopcut >=> return . fst >=>+> apply' cross +> where apply' = applyRule . ruleM The Node representation helps to compose INet directly from let expressions. @@ -423,8 +681,10 @@ > return $ Node Abstractor i [abs, body, bind] Nothing > delimiter to from v = incS >>= \i -> > return $ Node Delimiter i [to, from] (Just v)+> cycle out right left v = incS >>= \i -> +> return $ Node (Duplicator (Cycle True)) i [out, right, left] (Just v) > duplicator out right left v = incS >>= \i -> -> return $ Node Duplicator i [out, right, left] (Just v)+> return $ Node (Duplicator Dup) i [out, right, left] (Just v) > eraser out = incS >>= \i -> > return $ Node Eraser i [out] Nothing > initiator out = incS >>= \i -> @@ -448,9 +708,9 @@ Converting from Node representation to INet (a tree in this case). -> nodeToNet node = removeDummy $ visit [] empty [node]+> nodeToNet node = let net = removeDummy $ visit [] empty [node] in (net, maximum $ 0:(keys net)) > where-> visit :: [Node] -> INet -> [Node] -> INet+> -- visit :: [Node] -> INet -> [Node] -> INet > visit visited net [] = net > visit visited net (x:xs) = > if elem x visited@@ -465,15 +725,15 @@ > 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 :: 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 .+> in (adjust (replaceP j (c, k)) b .+> adjust (replaceP k (b, j)) c . > delete i) net > _ -> net) net (toList net)
src/Lambda.lhs view
@@ -11,12 +11,12 @@ > pretty > ) where -> import Diagram hiding (S)+> -- import Diagram hiding (S) > import INet > import Control.Monad.Fix > import Data.IntMap hiding (map)-> import Prelude hiding (take, drop, head, tail)+> import Prelude hiding (take, drop, head, tail, cycle) > data Term = Z | S Term | Abs Term | App Term Term > | Y Term -- fix point@@ -41,7 +41,7 @@ > es <- erasers xs > return $ e : es -> termToNet i Z ps = debug ("termToNet: Z " ++ show i) $ do+> termToNet i Z ps = do > let inp = head ps > out = head (drop i ps) > mid = take (i - 1) (tail ps)@@ -49,7 +49,7 @@ > es <- erasers mid > return $ (a : es) ++ [a] -> termToNet i x@(S t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ do+> termToNet i x@(S t) ps = do > let inp = head ps > out = head (drop i ps) > mid = take (i - 1) (tail ps)@@ -58,14 +58,14 @@ > e <- eraser out > return $ (d : tail n) ++ [e] -> termToNet i x@(Abs t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ do+> termToNet i x@(Abs t) ps = do > let inp = head ps > rec 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) $ do+> termToNet i x@(App t1 t2) ps = do > let inp = head ps > rec a <- applicator (head m) (head n) inp > m <- termToNet i t1 (a : qs)@@ -79,15 +79,23 @@ > ds <- dup (i - 1) as bs cs > return $ d : ds -> termToNet i x@(Y t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ do+> {-+> termToNet i x@(Y t) ps = do > let inp = head ps-> rec d <- duplicator a b inp 0+> rec a <- bigY (head n) inp 0+> n <- termToNet i t (a : tail ps)+> return $ a : tail n+> -}++> termToNet i x@(Y t) ps = do+> let inp = head ps+> rec d <- cycle 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) $ do+> termToNet i x@(Tup t1 t2) ps = do > let inp = head ps > rec a <- tuple inp (head m) (head n) > m <- termToNet i t1 (a : qs)@@ -101,7 +109,7 @@ > ds <- dup (i - 1) as bs cs > return $ d : ds -> termToNet i x (inp:out) = debug ("termToNet: " ++ show x ++ " " ++ show i) $ +> termToNet i x (inp:out) = > case x of > Fst t -> do > rec a <- twopin 1 "fst" (head n) inp@@ -130,8 +138,8 @@ > return e > netToTerm :: INet -> Term-> netToTerm net = -> let Just (i, (_, [(b, u)], _)) = findInitiator (toList (debug1 "netToTerm net=" net))+> netToTerm (net, _) = +> let Just (i, (_, [(b, u)], _)) = findInitiator (toList net) > in toTerm (net ! b) > where > toTerm (Abstractor, [_, (b, _), _], _) = Abs (toTerm (net ! b))@@ -155,39 +163,36 @@ meta rules for tuple handling, etc. -> meta net (i, (TwoPin arity l, [_, (c, u)], _))-> (j, (bt, bp, _)) = +> meta (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+> ("fst", Constructor "T") -> Just . project 1+> ("snd", Constructor "T") -> Just . project 2+> (_, Single m) -> Just . applyFunc m+> _ -> const Nothing > where-> project n =+> project n (net, maxID) = > 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 .+> 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 ++ ")"+> insert f f_ . delete i . delete j) net, maxID + 1)+> applyFunc m (net, maxID) =+> let 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 .+> 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 .+> delete j) net, maxID + 1)+> 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+> insert f f_ . delete j) net, maxID + 1) -> meta net a b@(_, (TwoPin _ _, _, _)) = meta net b a-> meta _ _ _ = Nothing+> meta a b@(_, (TwoPin _ _, _, _)) = meta b a +> meta _ _ = const Nothing a pretty printer for generalized lambda terms.
src/Main.lhs view
@@ -1,27 +1,99 @@ The main program for Lambdascope -> {-# LANGUAGE DoRec,CPP #-}+> {-# LANGUAGE NoMonomorphismRestriction,DoRec,CPP #-} > module Main where > import INet > import Diagram hiding (S) > import Lambda+> import Grid > import Graphics.Rendering.OpenGL (($=), GLfloat) > import qualified Graphics.Rendering.OpenGL as GL > import qualified Graphics.UI.GLFW as GLFW+> import qualified Data.Map as Map > import Control.Monad.Fix-> import Control.Monad (when, unless)+> import Control.Monad.Task+> import Graphics.UI.GLFW.Task+> import Control.Monad.IO.Class+> import Control.Monad.Trans+> import Control.Monad.Trans.State+> import Control.Monad.Identity+> import Control.Monad > import Data.IORef-> import Data.IntMap hiding (lookup, mapMaybe)+> import qualified Data.Set as Set+> import qualified Data.IntMap as IntMap+> import Data.IntMap hiding (null, lookup, mapMaybe, map) > import Data.Maybe (mapMaybe, fromMaybe)-> import Prelude hiding (map)-> import System.IO.Unsafe+> import Control.Arrow (first, second)+> import Data.List (intercalate, sort) An interactive net is a mapping from node IDs to their connected (node ID, port No) pairs. +> type Clicks = Map.Map String Int ++> data MainState +> = MS { showHelp :: Bool -- whether to display help message +> , inet :: INet -- current INet being displayed +> , frame :: Frame -- single frame of display (for animation)+> , hlset :: Maybe ([(Int, Int)], HLSet) -- wires to highlight+> , backup :: [(INet, GridMap Direction, Clicks)] -- backups for undo/rollback+> , clicks :: Clicks -- collection of statistics+> , preset :: Int -- next preset to load+> , title :: String -- title of current inet+> }+> initState net = MS False net emptyFrame Nothing [] Map.empty 0 ""++> lift3 = lift . lift . lift+> toggleShowHelp = lift3 $ modify $ \s -> s { showHelp = not (showHelp s) }+> getShowHelp = lift3 $ get >>= return . showHelp++> modifyTitle f = lift3 $ modify $ \s -> s { title = f (title s) }+> getTitle = lift3 $ get >>= return . title+> setTitle = modifyTitle . const++> modifyINet f = lift3 $ modify $ \s -> s { inet = f (inet s) }+> setINet = modifyINet . const+> getINet = lift3 $ get >>= return . inet++> modifyFrame f = lift3 $ modify $ \s -> s { frame = f (frame s) }+> setFrame = modifyFrame . const+> getFrame = lift3 $ get >>= return . frame++> snapshot = do+> grid <- lift $ getGrid+> lift3 $ modify $ \s -> s { backup = take 10 $ (inet s, grid, clicks s) : backup s }+> rollback = do+> grid <- lift3 $ do+> b <- fmap backup get+> case b of+> [] -> return Nothing+> (i, g, c) : bs -> modify (\s -> s { inet = i, clicks = c, backup = bs }) >> return (Just g)+> maybe (return False) (\g -> lift (setGrid g) >> return True) grid++> click name f = lift3 $ modify $ \s -> s { clicks = click' (clicks s) }+> where click' m = maybe (inc 0) inc $ Map.lookup name m +> where inc x = Map.insert name (f x) m+> resetClicks = lift3 $ modify $ \s -> s { clicks = Map.empty }+> getClicks = do+> m <- lift3 $ get >>= return . clicks+> return $ intercalate ", " $ map (\(x, y) -> x ++ " " ++ show y) $ Map.toList m++> renderINet = getINet >>= setDiagram . netToDiagram++> loadPreset f = do+> i <- lift3 $ get >>= return . preset+> lift3 $ modify $ \s -> s { preset = f i, backup = [], clicks = Map.empty }+> let (title, inet) = presetINet (f i)+> setTitle title+> setINet inet+> lift clearGrid +> setDirty Dirty+> renderINet +> autoAdjust+ Main Program #ifdef _EnableGUI_@@ -31,217 +103,221 @@ > main = do #endif > GLFW.initialize-> initWindow w h-> showHelp <- newIORef False-> factor <- newIORef (0, 0, 1.0)-> netRef <- newIORef net-> let loop handle = do -> (UserAction handle', render) <- handle-> GL.clear [GL.ColorBuffer] -> (cx, cy, s) <- readIORef factor-> GL.preservingMatrix (do-> GL.translate (vector3 (cx / unit) (cy / unit) 0) -> GL.scale s s 1-> render)-> help <- readIORef showHelp -> GL.preservingMatrix (do-> GL.color $ color3 0.2 0.3 0.8-> GL.translate (vector3 (- fromIntegral w / unit / 2) (fromIntegral h / unit / 2 - 1.25) 0)-> GL.scale 0.8 0.8 (1::GLfloat)-> renderString "H toggles help, ESC quits"-> GL.translate $ vector3 0 (-1.25) 0-> when help $ renderText helpText)-> GLFW.swapBuffers-> GLFW.sleep 0.01-> exit <- GLFW.getKey GLFW.ESC -> unless (exit == GLFW.Press) $ loop handle'-> loop (handleUserAction factor (keyHandle showHelp netRef) (reduce netRef) d)+> dState <- initWindow w h+> evalStateT (evalStateT (evalGridT_ (runTask start) margin) dState) (initState emptyINet) > GLFW.closeWindow > GLFW.terminate > where > -- prepare an initial diagram to load-> net = nodeToNet (mkNode (termToNode t2')) --(App cube (VInt 3))))-> d = netToDiagram net+> -- net = nodeToNet $ mkNode . termToNode $ App cube (VInt 3) -- (termToNode t4)) -- (App cube (VInt 3)))) > w = 800 > h = 600+> start = do+> loadPreset id+> renderINet+> waitForEvents <- liftIO registerTaskCallbacks+> setupEvents $ (snapshot >>) . reduce+> fork $ forever $ watch (onKey >=> isPress >=> isKey 'H') >> toggleShowHelp >> setDirty Lightly+> fork $ forever $ watch (onKey >=> isPress >=> isKey 'L') >> snapshot >> lift clearGrid >> setDirty Dirty+> fork $ forever $ watch (onKey >=> isPress >=> isKey '[') >> loadPreset (\x -> x - 1) +> fork $ forever $ watch (onKey >=> isPress >=> isKey ']') >> loadPreset (+1)+> fork $ forever $ watch (onKey >=> isPress >=> isKey GLFW.BACKSPACE) >>+> rollback >> renderINet >> setDirty Dirty+> mapM_ (\(c, f) -> fork $ forever $ watch (onKey >=> isPress >=> isKey c) >> snapshot >> getINet >>= f >>= setINet >>+> renderINet >> setDirty Dirty)+> [('R', reduceAll),+> ('Y', resetAll),+> ('X', crossAll),+> ('B', betaAll),+> ('E', eraseAll),+> ('U', unwindAll),+> ('S', scopeAll),+> ('C', loopcutAll),+> ('T', toTerm),+> ('M', metaAll),+> -- ('P', pruneAll),+> ('O', outer), +> ('Q', outerRed), +> ('A', outerRedAll), +> ('D', demoteDup) ]+> forever $ do+> waitForEvents+> whenDirty renderAll+> setDirty None+> where+> renderAll = do+> title <- getTitle+> font <- getFont+> stats <- getClicks+> renderS <- fmap (renderScene font) getFactor +> renderH <- fmap (renderHelp font ("INet for (" ++ title ++ ") " ++ stats)) getShowHelp +> oldFrame <- getFrame+> newFrame <- getDiagram >>= renderDiagram +> setFrame newFrame+> d <- getDirty +> if d < Dirty+> then liftIO (clearAll >> renderS newFrame >> renderH)+> else do+> let f = betweenFrame oldFrame newFrame+> t0 <- liftIO $ GL.get GLFW.time +> let dur = 0.5+> animate t | t >= t0 + dur = return ()+> | otherwise = do+> t <- liftIO $ GL.get GLFW.time +> let p = realToFrac (t - t0) / dur+> g = f (if p > 1 then 1 else p)+> liftIO (clearAll >> renderS g >> renderH)+> animate t +> fork $ animate t0 +> clearAll = GL.clear [GL.ColorBuffer] +> renderScene font (cx, cy, s) f = GL.preservingMatrix (do+> GL.translate (vector3 (realToFrac (cx / unit)) (realToFrac (cy / unit)) 0) +> GL.scale (realToFrac s) (realToFrac s) (1 :: GL.GLfloat)+> renderFrame font Set.empty f)+> renderHelp font tagline help = do+> GL.Size w h <- GL.get GLFW.windowSize +> GL.preservingMatrix (do+> GL.color $ color3 0.2 0.3 0.8+> GL.translate (vector3 (- fromIntegral w / unit' / 2) (fromIntegral h / unit' / 2 - 1.25) 0)+> GL.scale 0.8 0.8 (1::GLfloat)+> renderString font ("H toggles help, ESC quits. " ++ tagline)+> GL.translate $ vector3 0 (-1.25) 0+> when help $ renderText font helpText)+> GLFW.swapBuffers > helpText = unlines -> [ "CTRL+ mouse pan"-> , "ALT + mouse zoom"-> , "Left click rotate node"-> , "Right click apply any rule to node"+> [ -- "CTRL+ mouse pan"+> -- , "ALT + mouse zoom"+> "Left click apply any rule to node" > , "Drag mouse move node"-> , "1 .. 9 load presets"+> , "[ or ] load presets" > , "Space auto zoom"+> , "BackSpace rollback one step (max 10)" > , "L auto layout all nodes" > , "R reduce to head normal form"-> , "X repeat outermost cross rule"+> , "X repeat cross rule everywhere" > , "B repeat beta rule everywhere" > , "E repeat erase rule everywhere" > , "U apply unwind rule everywhere" > , "S apply scope rule everywhere" > , "C apply loopcut rule everywhere"-> , "T unwind, cross, scope, cross, loopcut, cross"+> , "T print term from net (after loopcut)" > , "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"+> -- , "P prune all none root tree" -- temporarily disable prune since it is not implemented correctly+> , "O outermost reduction once"+> , "Q outermost reduction once (also goes under lambda)"+> , "A repeat outermost reduction (also goes under lambda)" > , "D zap duplicator's value (become call-by-need)"] > -> -> keyHandle showHelp netRef = (fst $ unzip ks, handle)+> presetINet i = (title, node) > where-> -- change the following line to load different programs for 1..9-> -- It currently loads the (opt N) lambda expression.-> ks = [(c, load $ opt $ fromEnum c - 48) | c <- ['1'..'9']] ++ -> [('R', reduceAll),-> ('X', crossAll),-> ('B', betaAll),-> ('E', eraseAll),-> ('U', unwindAll),-> ('S', scopeAll),-> ('C', loopcutAll),-> ('T', toTerm),-> ('M', metaAll),-> ('P', pruneAll),-> ('O', outer),-> ('V', viewCounter),-> ('L', reLayout),-> ('D', demoteDup),-> ('H', \n d r -> (n, d, r))]-> handle k d r = do-> net <- readIORef netRef-> when (k == 'H') $ (modifyIORef showHelp not)-> let (net', d', r') = maybe (net, d, r) (\f -> f net d r) (lookup k ks)-> writeIORef netRef net'-> return (d', r')+> (title, node) = inets !! (i `mod` n)+> n = length inets+> inets +> = [ ("test0", (testL0, 4))+> , ("trace0", cleanup $ nodeToNet $ mkNode $ termToNode (trace juggle))+> -- , ("ccaE", cleanup $ nodeToNet $ mkNode $ termToNode ccaE)+> , ("map2", nodeToNet $ mkNode $ termToNode map2)+> , ("exp", cleanup $ nodeToNet $ mkNode $ termToNode e)+> , ("test1", (testL1, 4))+> , ("test2", (testL2, 4))+> , ("test3", (testL3, 4))+> , ("test4", (testL4, 4))+> ] ++ map (second (nodeToNet . mkNode))+> [ ("2", termToNode t2)+> , ("2 2", termToNode t4)+> , ("opt 1", termToNode (opt 1))+> , ("opt 2", termToNode (opt 2))+> , ("opt 3", termToNode (opt 3))+> , ("one", termToNode one)+> -- , ("(\\x.x) x", termToNode (App (Abs Z) (VStr "x")))+> -- , ("cube 3", termToNode $ App cube (VInt 3))+> ] -> 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')+> cleanup = fst . runIdentity . repeatRule (applyRule (ruleM erase)) -> 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)+> demoteDup = return . first (IntMap.map demote)+> where +> demote a = case a of+> (Duplicator _, cp, cv) -> (Duplicator (Sup False), cp, cv)+> _ -> a +> reLayout net d = (net, d)+ activates a local rule to a node, and apply it once.+This will also revive dormant Cycle. -> reduce :: IORef INet -> Int -> IO ([Int], Diagram)-> reduce netRef i = do-> net <- readIORef netRef-> let a@(at, ap, av) = net ! i+> -- reduce :: Int -> IO ([Int], Diagram)+> reduce i = do+> -- traceShow ("NID", i)+> net@(netMap, _) <- getINet+> let a@(at, ap, av) = revive (netMap ! i) > (j, n) = head ap-> b@(bt, bp, bv) = 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')+> b@(bt, bp, bv) = revive (netMap ! j)+> when (ap == []) $ error "here!" -- delete i net+> net' <- localAll (i, a) (j, b) net >>= return . fromMaybe net +> -- traceShow ("reduced", net, net') +> setINet net'+> renderINet+> where+> revive (Duplicator (Cycle _), ap, v) = (Duplicator (Cycle True), ap, v)+> revive x = x -> localAll = meta_ ->- beta_ ->- cross_ ->- erase +> localAll = meta_ ->- beta_ ->- cross_ ->- erase_ -- ->- share_+ Note that in optimal reduction, the erase is a global rule rather than an outermost one because it'll otherwise results in redudant beta or meta reduction. -> reduceAll = wrapRule (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_))+> reduceAll = wrapRule (applyRule (ruleM resetCycle) +&+ +> repeatRule (applyRule meta_) +&+ +> repeatRule (applyRule beta_) +&+ +> repeatRule (applyRule cross_) +&+ +> repeatRule (applyRule erase_))+> resetAll = wrapRule (applyRule (ruleM resetCycle))+> crossAll = wrapRule (applyRule cross_)+> betaAll = wrapRule (applyRule beta_)+> eraseAll = wrapRule (applyRule erase_)+> metaAll = wrapRule (applyRule meta_)+> unwindAll = wrapRule (applyRule unwind_)+> scopeAll = wrapRule (applyRule scope_)+> loopcutAll = wrapRule (applyRule loopcut_) > outer = wrapRule (outermost localAll)-> 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)+> outerRed = wrapRule (outerReducible localAll)+> outerRedAll = wrapRule (repeatRule (outerReducible localAll))+> pruneAll = wrapRule (return . prune) -> incCounter c x y z = do-> m <- readIORef c-> let m' = m + 1-> m' `seq` writeIORef c m'+> readbackM = +> applyRule unwind_ >=> return . fst >=> +> applyRule scope_ >=> return . fst >=>+> wrapRule (repeatRule (applyRule cross_)) >=>+> applyRule loopcut_ >=> return . fst >=>+> wrapRule (repeatRule (applyRule cross_)) -> 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+> toTerm net = do+> net' <- readbackM net+> let t = netToTerm net'+> liftIO $ putStrLn ("toTerm = " ++ show t) +> return net' -> 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+> wrapRule f net = fmap fst (f net) -Customizd beta, meta and erase rules that track statistics.+Rules with click counters. -> 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+> cross_ = wrapClick "cross" cross+> beta_ = wrapClick "beta" beta+> meta_ = wrapClick "meta" meta+> erase_ = wrapClick "erase" erase+> unwind_ = wrapClick "unwind" unwind+> scope_ = wrapClick "scope" scope+> loopcut_ = wrapClick "loopcut" loopcut+> -- share_ = wrapClick "share" share+> wrapClick counter r a b c = do+> n <- ruleM r a b c+> click counter (maybe id (\_ -> (+1)) n)+> return n Testing =======@@ -265,7 +341,7 @@ > return a > four = do-> rec s <- eraser a+> rec s <- initiator a > a <- applicator b b s > b <- duplicator t a a 0 > t <- two b@@ -275,11 +351,12 @@ > x = VStr "x" > f = Abs (VFunc 1 "f" Z)+> g = Abs (VFunc 1 "g" Z) > t2 = church 2 > t2' = App (App (church 2) f) x --App (App (Abs (Abs (App (S Z) (App (S Z) Z)))) f) x -> t4 = App (Abs (App Z Z)) t2+> t4 = App t2 t2 > t4' = App (App t4 f) x > church n = Abs (Abs (app n (S Z) Z))@@ -306,7 +383,6 @@ Test for handling disconnected graph, rather than tree -> test :: INet > test = fromList [ > (0, (Eraser, [(1, 0)], Nothing)), > (1, (Eraser, [(0, 0)], Nothing)),@@ -328,45 +404,41 @@ 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))]+> (1, (Eraser, [(3, 2)], Nothing)),+> (2, (Delimiter, [(3, 1), (0, 0)], Just 0)),+> (3, (Duplicator Dup, [(4, 0), (2, 0), (1, 0)], Just 0)),+> (4, (Duplicator Dup, [(3, 0), (4, 2), (4, 1)], Just 0))] two duplicators wiring to each other on both sides -> testL1 :: INet > testL1 = fromList [-> (2, (Duplicator, [(3, 0), (2, 2), (2, 1)], Just 0)),-> (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]+> (2, (Duplicator Dup, [(3, 0), (2, 2), (2, 1)], Just 0)),+> (3, (Duplicator Dup, [(2, 0), (3, 2), (3, 1)], Just 0))] for commute: similar to testL0 -> testL2 :: 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))]+> (2, (Duplicator Dup, [(3, 0), (0, 0), (1, 0)], Just 1)),+> (3, (Duplicator Dup, [(2, 0), (3, 2), (3, 1)], Just 0))] similar to testL1 -> testL3 :: INet > testL3 = fromList [-> (2, (Duplicator, [(3, 0), (2, 2), (2, 1)], Just 1)),-> (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]+> (2, (Duplicator Dup, [(3, 0), (2, 2), (2, 1)], Just 1)),+> (3, (Duplicator Dup, [(2, 0), (3, 2), (3, 1)], Just 0))] when a single duplicator loops its two ports -> testL4 :: 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))]+> (2, (Duplicator Dup, [(1, 0), (2, 2), (2, 1)], Just 0))] These are tests for optimality. With church numbers, (n 2 i x) takes exponential time in call-by-need, but only linear to n@@ -414,8 +486,8 @@ 5 70 66 255 6 135 114 323 7 264 204 398-8 392 377 453-9 644 719 539+8 392 377 480+9 644 719 569 It's easy to tell that they are of O(n * 2^n), O(n^7) and O(n^2) respectively. It's also worth mentioning that if we only count the number of@@ -444,7 +516,7 @@ > (Fst (S Z)))) -- fst x > (App (Snd (S Z)) Z))))))) -- snd x dt -> e = Y (App integral (VInt 1))+> e = Y (App integral (VInt 1)) -- (1, \dt -> (next dt 1 1, snd e)) > unfold = Abs (App (Snd Z) (VStr "dt")) > expN n = Fst (app n unfold e) @@ -553,4 +625,71 @@ > (times Z (App (S (S Z)) (minus (S Z) (VInt 1)))))))) > cube = App power (VInt 3) > powerCube = cons power (cons cube (App cube (VInt 5)))- ++CCA Integral of Exp Example+===========================++GHC cannot give the most optimized result for the following expression:++ trace (juggle . ((dup . snd) `cross` id) . (swap `cross` id) . juggle . + ((((+1) `cross` id) . trace (juggle . (dup `cross` id) . swap . + (acc `cross` id) . juggle)) `cross` id) . juggle . + (swap `cross` id) . juggle)++ trace f x = let (y, z) = f (x, z) in y+ juggle ((x, y), z) = ((x, z), y)+ cross f g (x, y) = (f x, g y)+ acc (x, i) = i + dt * x+ assoc ((x,y),z) = (x,(y,z))+ unassoc (x,(y,z)) = ((x,y),z)++ trace f x = let g z = snd (f (x, z))+ in fst (f (x, (fix g)))++> trace = App $ Abs $ Abs $ Fst $ App (S Z) (Tup Z (Y (Abs $ Snd $ App (S (S Z)) (Tup (S Z) Z))))+> plus x y = App (VFunc 2 "+" x) y+> juggle = Abs $ Tup (Tup (Fst (Fst Z)) (Snd Z)) (Snd (Fst Z))+> across f g = Abs $ Tup (App f (Fst Z)) (App g (Snd Z))+> acc = Abs $ plus (Snd Z) (times (VStr "dt") (Fst Z))+> assoc = Abs $ Tup (Fst (Fst Z)) (Tup (Snd (Fst Z)) (Snd Z))+> unassoc = Abs $ Tup (Tup (Fst Z) (Fst (Snd Z))) (Snd (Snd Z))+> dup = Abs $ Tup Z Z+> f `dot` g = App (App (Abs $ Abs $ Abs $ App (S (S Z)) (App (S Z) Z)) f) g++> cca0 = assoc `dot` unassoc+> ccaE = trace (juggle `dot` +> ((dup `dot` snd) `across` id) `dot`+> (swap `across` id) `dot` juggle `dot`+> ((((Abs $ plus Z (VInt 1)) `across` id) `dot` +> trace (juggle `dot` (dup `across` id) `dot` swap `dot`+> (acc `across` id) `dot` juggle)) `across` id) `dot` +> juggle `dot` (swap `across` id) `dot` juggle)+> {-+> ccaE = trace+> (juggle `dot` (dup `across` id) `dot` swap `dot`+> (acc `across` id) `dot` juggle)+> -}+> where+> snd = Abs $ Snd Z+> id = Abs Z+> swap = Abs (Tup (Snd Z) (Fst Z))++toTerm = Abs (Tup (App (VFunc 2 "+" (Snd Z)) (VInt 1)) (App (VFunc 2 "+" (Snd Z)) (App (VFunc 1 "(* dt)" (VFunc 2 "+" (Snd Z))) (VInt 1))))++f (a, b) = (1 + b, dt * b + 1)+f (a, b) = (1 + b, b + dt * (1 + b))++Map Fusion+==========++ map f (x,y) = (f x, map f y)++> map' = Y $ Abs $ Abs $ Abs $ Tup (App (S Z) (Fst Z)) (App (App (S (S Z)) (S Z)) (Snd Z))+> map2 = App (Abs (App Z f `dot` App Z g)) map'+> map2' = App map' (f `dot` g)++(map f . map g) (x, y) = ((f . g) x, (map f ((map g) y)))++(map f . map g) = Y F + where F h (x, y) = ((f.g) x, h y)+