diff --git a/LambdaINet.cabal b/LambdaINet.cabal --- a/LambdaINet.cabal +++ b/LambdaINet.cabal @@ -1,5 +1,5 @@ name: LambdaINet -version: 0.1.2.1 +version: 0.2.0.0 homepage: not available maintainer: Paul H. Liu 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 diff --git a/README b/README --- a/README +++ b/README @@ -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. diff --git a/src/Diagram.lhs b/src/Diagram.lhs --- a/src/Diagram.lhs +++ b/src/Diagram.lhs @@ -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 diff --git a/src/Grid.lhs b/src/Grid.lhs new file mode 100644 --- /dev/null +++ b/src/Grid.lhs @@ -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) diff --git a/src/INet.lhs b/src/INet.lhs --- a/src/INet.lhs +++ b/src/INet.lhs @@ -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) diff --git a/src/Lambda.lhs b/src/Lambda.lhs --- a/src/Lambda.lhs +++ b/src/Lambda.lhs @@ -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. diff --git a/src/Main.lhs b/src/Main.lhs --- a/src/Main.lhs +++ b/src/Main.lhs @@ -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) +