Interactive Net for Lambdascope implmenetation
> module INet where
> import Diagram
> import Data.IntMap as IntMap hiding (filter, map)
> import Data.Maybe (fromJust)
> import Control.Monad.State
Interactive Net is defined to be a table, that maps node IDs to
a triple that contains the node type, a list of ports (indexed
by the list index), and value.
> type INetV = (NodeType, [(NodeID, Int)], Maybe Int)
> type INet = IntMap INetV
A port is a pair of the other end's NodeID and port index.
> type NetPort = (NodeID, Int)
> type NodeID = Int
> data NodeType = Applicator
> | Applicator' -- flip of Applicator
> | Abstractor
> | Delimiter
> | Delimiter' -- flip of Delimiter
> | Duplicator
> | SuperDup -- dup everything
> | Eraser
> | Dummy -- dummy for self-loop
> | Initiator -- never destroyed
> | Constructor String -- data constructor
> | TwoPin Int String | TwoPin' Int String -- for meta function
> | Single String | Single' String -- for meta value
> deriving (Eq, Show)
> findInitiator [] = Nothing
> findInitiator (a@(i, (Initiator, [(b, u)], Nothing)):as) = Just a
> findInitiator (a:as) = findInitiator as
netToDiagram :: Net -> Diagram
> netToDiagram net =
> let list = toList net
> Just (init, _) = findInitiator list
> atoms = map toAtom list
> d = fromList (map (\a -> (atomID a, a)) atoms)
> heads = map (d!) $ foldl (\h i ->
> if any (\j -> reachable net [] [j] i) h then h else i : h) [] $
> ((init:) . filter (/=init)) $ map fst list
> in Diagram heads d
> where
> toAtom (i, (t, p, v)) =
> let a = Atom i l (map (toPort a t) (zip [0..] p)) (2, 2) (draw l)
> in a
> where
> (l, draw) =
> case t of
> Applicator -> ("@", drawApplicator)
> Applicator' -> ("@", drawAbstractor)
> Abstractor -> ("\x80", drawAbstractor)
> Delimiter -> (maybe "" show (v::Maybe Int), drawDelimiter)
> Duplicator -> (maybe "" show (v::Maybe Int), drawDuplicator)
> SuperDup -> ("*", drawDuplicator)
> Eraser -> ("", drawEraser)
> Initiator -> ("I", drawEraser)
> Delimiter' -> ("S", drawTwoPin)
> Constructor l -> (l, drawAbstractor)
> TwoPin _ l -> (l, drawTwoPin)
> TwoPin' _ l -> (l, drawTwoPin)
> Single l -> (l, drawSingle)
> Single' l -> (l, drawSingle)
> toPort a t (m, (j, n)) =
> let (d, p) = pos t m
> b = toAtom (j, (net ! j))
> in Port a (atomPorts b !! n) d p
> reachable :: INet -> [Int] -> [Int] -> Int -> Bool
> reachable d visited [] i = False
> reachable d visited (x:xs) i =
> let (_, ps, _) = (d ! x)
> js = map fst ps
> ks = filter (flip notElem visited) js
> in (x == i) || reachable d (x : visited) (xs ++ ks) i
> pos Applicator 0 = (S, (0, -2))
> pos Applicator 1 = (E, (2, 0))
> pos Applicator 2 = (N, (0, 2))
> pos Applicator' i = pos Abstractor i
> pos Abstractor 0 = (N, (0, 2))
> pos Abstractor 1 = (S, (0, -2))
> pos Abstractor 2 = (E, (2, 0))
> pos Delimiter 0 = (S, (0, -2))
> pos Delimiter 1 = (N, (0, 2))
> pos Duplicator 0 = (S, (0, -2))
> pos Duplicator 1 = (N, (1, 2))
> pos Duplicator 2 = (N, (-1, 2))
> pos SuperDup i = pos Duplicator i
> pos Eraser 0 = (S, (0, -2))
> pos Initiator 0 = (S, (0, -2))
> pos Delimiter' 0 = (N, (0, 2))
> pos Delimiter' 1 = (S, (0, -2))
> pos (Constructor _) i = pos Abstractor i
> pos (TwoPin arity l) i = pos Delimiter' i
> pos (TwoPin' arity l) i = pos Delimiter i
> pos (Single _) 0 = (N, (0, 2))
> pos (Single' _) 0 = (N, (0, 2))
> type LocalRule = INet -> (Int, INetV) -> (Int, INetV) -> Maybe INet
> type Rule = INet -> (INet, Int)
Make a local rule global by applying it once everywhere.
> applyRule :: LocalRule -> Rule
> applyRule rule net = applyRule' 0 rule (keys net) net
> applyRule' :: Int -> LocalRule -> [Int] -> Rule
> applyRule' num rule [] net = (net, num)
> applyRule' num rule (i:rs) net =
> let a@(at, ap, av) = net ! i
> (j, n) = head ap
> b@(bt, bp, bv) = net ! j
> r = rule net (i, a) (j, b)
> in if member i net
> then maybe (applyRule' num rule rs net) (applyRule' (num + 1) rule (filter (j/=) rs)) r
> else applyRule' num rule rs net
repeatedly apply a rule until it is no longer applicable.
> repeatRule = repeatRule' 0
> repeatRule' :: Int -> Rule -> Rule
> repeatRule' sum rule net =
> let (net', num) = rule net
> in if num == 0
> then (net, sum)
> else repeatRule' (sum + num) rule net'
Apply a local rule at the outermost position.
actually beta and meta can be performed simultaneously)
> outermost :: LocalRule -> Rule
> outermost rule net =
> case findInitiator $ toList net of
> Just (i, _) -> outermost' [] [i]
> Nothing -> (net, 0)
> where
> outermost' _ [] = (net, 0)
> outermost' visited (i:is) =
> let a@(at, ((j, _):ps), _) = net ! i
> b = net ! j
> in if elem i visited
> then (net, 0)
> else maybe (outermost' (i:visited) (j:is)) (\net -> (net, 1)) $ rule net (i, a) (j, b)
Compose two local rules together, try the first one, if it succeeds, just
return; otherwise, try the second one.
> infixr 5 ->-
> (->-) :: LocalRule -> LocalRule -> LocalRule
> (->-) r1 r2 net a b = maybe (r2 net a b) Just $ r1 net a b
> infixr 5 +>+
> (+>+) :: Rule -> Rule -> Rule
> (+>+) r1 r2 net =
> let r@(net', n) = r2 net
> in if n == 0 then r1 net else r
The cross rules: annihilate and commute.
> cross net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) =
> if head bp == (i, 0) -- princple ports meet?
> then if at == bt && av == bv -- same type and value?
> then Just $ annihilate net (i, a) (j, b)
> else case (at, bt) of -- different type
> (Applicator, Abstractor) -> Nothing -- leave the beta rule out
> (Abstractor, Applicator) -> Nothing
> (Constructor _, TwoPin _ _) -> Nothing -- leave the meta rule out
> (TwoPin _ _, Constructor _) -> Nothing
> (Single _, TwoPin _ _) -> Nothing -- FIXME: never cross single, but cross single'
> (TwoPin _ _, Single _) -> Nothing
> (Initiator, Delimiter) -> Just $ commute net (i, a) (j, b)
> (Delimiter, Initiator) -> Just $ commute net (i, a) (j, b)
> (Initiator, _) -> Nothing
> (_, Initiator) -> Nothing
> _ -> Just $ commute net (i, a) (j, b)
> else case (at, bt, snd (head ap)) of
> (SuperDup, Applicator, 2) -> Just $ superDup net (i, a) (j, b)
> (SuperDup, TwoPin _ _, 1) -> Just $ superDup net (i, a) (j, b)
> (SuperDup, Delimiter, 1) -> Just $ superDup net (i, a) (j, b)
> _ -> Nothing
cross from rear
> superDup net (i, a) (j, b) =
> let Just net' = upsideDown net (j, b)
> net'' = commute net' (i, a) (j, net'!j)
> ks = map fst $ filter (\ (i, (ct, _, _)) -> case ct of
> Applicator' -> True
> TwoPin' _ _ -> True
> Delimiter' -> True
> _ -> False) (toList net'')
> in foldr (\k net -> fromJust $ upsideDown net (k, net!k)) net'' ks
The modified cross rule, only moves delimiter or annihilates.
> cross' net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) =
> if head bp == (i, 0) -- princple ports meet?
> then if at == bt && av == bv -- same type and value?
> then Just $ annihilate net (i, a) (j, b)
> else case (at, bt) of -- different type
> (Delimiter, _) -> Just $ commute net (i, a) (j, b)
> (_, Delimiter) -> Just $ commute net (i, a) (j, b)
> _ -> Nothing
> else Nothing
> annihilate net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) =
> let pairup = zip (tail ap) (tail bp)
> pair' = fixLoop pairup pairup
> in foldr (\ ((c, u), (d, v)) ->
> adjust (\ (ct, cp, cv) -> (ct, replace u (d, v) cp, cv)) c .
> adjust (\ (dt, dp, dv) -> (dt, replace v (c, u) dp, dv)) d)
> ((delete i . delete j) net) pair'
> where
> fixLoop _ [] = []
> fixLoop pairs (x@(p@(c, u), q@(d, v)) : xs) =
> let p' = if c == i then snd (pairs!!(u-1)) else p
> q' = if d == j then fst (pairs!!(v-1)) else q
> in (p',q') : fixLoop pairs xs
The commute rule should also work for the Eraser so that the other thing
annihilates.
> commute net (i, a@(at, ap, av)) (j, b@(bt, bp, bv)) =
> let maxID = maximum (keys net)
> bs = take (length ap - 1) [(maxID + 1) .. ]
> as = take (length bp - 1) [(maxID + 1 + length bs) .. ]
> bs_ = map (\ (k, (c, u)) -> (bt',
> (if c == i then (bs!!(u-1), 0)
> else if c == j then (as!!(u-1), 0) else (c, u))
> : zip as (repeat k), bv')) (tail (zip [0..] ap))
> as_ = map (\ (k, (c, u)) -> (at',
> (if c == j then (as!!(u-1), 0)
> else if c == i then (bs!!(u-1), 0) else (c, u))
> : zip bs (repeat k), av'))
> (tail (zip [0..] bp))
> av' = maybe Nothing (\v -> Just $
> if bt == Abstractor ||
> (bt == Delimiter && v >= fromJust bv) then v + 1 else v) av
> bv' = maybe Nothing (\v -> Just $
> if at == Abstractor ||
> (at == Delimiter && v >= fromJust av) then v + 1 else v) bv
> at' = if at == Duplicator && av' == Nothing && bt == Abstractor then SuperDup else at
> bt' = if bt == Duplicator && bv' == Nothing && at == Abstractor then SuperDup else bt
> in (flip (foldr (\ (k, (c, u)) -> adjust (\ (ct, cp, cv) ->
> (ct, replace u (bs !! k, 0) cp, cv)) c)) (zip [0..] (tail ap)) .
> flip (foldr (\ (k, (c, u)) -> adjust (\ (ct, cp, cv) ->
> (ct, replace u (as !! k, 0) cp, cv)) c)) (zip [0..] (tail bp)) .
> flip (foldr (uncurry insert)) (zip bs bs_) .
> flip (foldr (uncurry insert)) (zip as as_) .
> delete i . delete j) net
The erase rule erase anything it sees.
> erase net (i, a@(at, ap@((_, n):_), av)) (j, b@(bt, bp, bv)) =
> case (at, bt, head bp == (i, 0)) of
Erase sharing is actually not strictly needed as they are not active pairs,
though it helps to speed up garbage collection and the reduction of degerated
(self-looping) components.
> (Eraser, Duplicator, False) -> eraseSharing
> (Eraser, SuperDup, False) -> eraseSharing
> (Eraser, _, True) -> cross net (i, a) (j, b) -- otherwise cross
> (_, Eraser, _) -> erase net (j, b) (i, a)
> _ -> Nothing
> where
> eraseSharing =
> let (c, u) = bp !! (3 - n)
> (d, v) = bp !! 0
> in Just $ (delete i . delete j .
> adjust (\ (ct, cp, cv) -> (ct, replace u (d, v) cp, cv)) c .
> adjust (\ (dt, dp, dv) -> (dt, replace v (c, u) dp, dv)) d) net
The prune rule removes all trees without the initiator. This is necessary for
garbage collecting self-looping components.
> prune :: Rule
> prune net =
> let Just (i, a) = findInitiator (toList net)
> visited = visit [] [i]
> net' = filterWithKey (\k _ -> elem k visited) net
> in (net', 0)
> where
> visit visited [] = visited
> visit visited (i:is) =
> let a@(_, p, _) = net ! i
> bs = filter (flip notElem visited) (map fst p)
> in visit (i:visited) (is ++ bs)
The disintegrate rule is never really used here, because we won't be able
to recover the Abstractor afterwards. (FIXME: to handle self-loop)
> disintegrate net (i, a@(at, ap@[(b,l), (c,u), (d,v)], av)) =
> let maxID = maximum (keys net)
> (d1, d2) = (maxID + 1, maxID + 2)
> d1_ = (Delimiter, [(i,2), (c, u)], Just 0)
> d2_ = (Delimiter, [(i,1), (d, v)], Just 0)
> in (adjust (const (Applicator, [(b, l), (d2, 0), (d1, 0)], Nothing)) i .
> adjust (\ (ct, cp, cv) -> (ct, replace u (d1, 1) cp, cv)) c .
> adjust (\ (dt, dp, dv) -> (dt, replace v (d2, 1) dp, dv)) d .
> insert d1 d1_ . insert d2 d2_) net
The beta rule aplies when Applicator meets Abstractor.
> beta net (i, a@(at, ap, _)) (j, b@(bt, bp, _)) =
> case (head bp == (i, 0), at, bt) of
> (True, Applicator, Abstractor) -> Just $ beta' net (i, a) (j, b)
> (True, Abstractor, Applicator) -> Just $ beta' net (j, b) (i, a)
> _ -> Nothing
> beta' net (i, a@(at, [_, (c,u), (d,v)], av))
> (j, b@(bt, [_, (e,x), (f,y)], bv)) =
> let maxID = maximum (keys net)
> (d1, d2) = (maxID + 1, maxID + 2)
> d1_ = (Delimiter, [(d, v), if e == j then (d2, 1) else (e, x)], Just 0)
> d2_ = (Delimiter, [(c, u), if f == j then (d1, 1) else (f, y)], Just 0)
> in (adjust (\ (ct, cp, cv) -> (ct, replace u (d2, 0) cp, cv)) c .
> adjust (\ (dt, dp, dv) -> (dt, replace v (d1, 0) dp, dv)) d .
> adjust (\ (et, ep, ev) -> (et, replace x (d1, 1) ep, ev)) e .
> adjust (\ (ft, fp, fv) -> (ft, replace y (d2, 1) fp, fv)) f .
> insert d1 d1_ . insert d2 d2_ . delete i . delete j) net
> replace :: Int -> a -> [a] -> [a]
> replace _ _ [] = []
> replace 0 v (x:xs) = v : xs
> replace i v (x:xs) = x : replace (i - 1) v xs
The following rules are for reading back
> unwind net a@(_, (Delimiter, _, _)) _ = Nothing
> unwind net a@(_, (Delimiter', _, _)) _ = Nothing
> unwind net a@(_, (TwoPin _ _, _, _)) _ = Nothing
> unwind net a@(_, (TwoPin' _ _, _, _)) _ = Nothing
> unwind net a@(_, (Applicator', _, _)) _ = Nothing
> unwind net (i, a@(Single l, p, Nothing)) _ = Just $
> adjust (\_ -> (Single' l, p, Nothing)) i net
> unwind net a b = upsideDown net a
> upsideDown net (i, a@(at, _, _)) =
> case at of
> Applicator ->
> let (_, [(b,u), (c,v), (d, w)], _) = a
> in Just $
> (adjust (const (Applicator', [(d, w), (b, u), (c, v)], Nothing)) i .
> adjust (\ (bt, bp, bv) -> (bt, replace u (i, 1) bp, bv)) b .
> adjust (\ (ct, cp, cv) -> (ct, replace v (i, 2) cp, cv)) c .
> adjust (\ (dt, dp, dv) -> (dt, replace w (i, 0) dp, dv)) d) net
> Applicator' ->
> let (_, [(b,u), (c,v), (d, w)], _) = a
> in Just $
> (adjust (const (Applicator, [(c, v), (d, w), (b, u)], Nothing)) i .
> adjust (\ (bt, bp, bv) -> (bt, replace u (i, 2) bp, bv)) b .
> adjust (\ (ct, cp, cv) -> (ct, replace v (i, 0) cp, cv)) c .
> adjust (\ (dt, dp, dv) -> (dt, replace w (i, 1) dp, dv)) d) net
> TwoPin arity l -> Just $ upsideDown' (TwoPin' arity l) a
> TwoPin' arity l -> Just $ upsideDown' (TwoPin arity l) a
> Delimiter -> Just $ upsideDown' Delimiter' a
> Delimiter' -> Just $ upsideDown' Delimiter a
> _ -> Nothing
> where
> upsideDown' at' a@(_, [(b,u),(c,v)], av) =
> (adjust (const (at', [(c, v), (b, u)], av)) i .
> adjust (\ (bt, bp, bv) -> (bt, replace u (i, 1) bp, bv)) b .
> adjust (\ (ct, cp, cv) -> (ct, replace v (i, 0) cp, cv)) c) net
> scope net (i, a@(Delimiter, [(b, u), (c, v)], Just av)) _ = upsideDown net (i, a)
> scope _ _ _ = Nothing
> loopcut net (i, a@(Abstractor, [(b, u), (c, v), (d, w)], Nothing)) _ =
> let maxID = maximum (keys net)
> (e, f) = (maxID + 1, maxID + 2)
> e_ = (Eraser, [(i, 2)], Nothing)
> f_ = (Eraser, [(d, w)], Nothing)
> (dt, _, _) = net ! d
> in if dt /= Eraser
> then Just $
> (adjust (\ (at, ap, av) -> (at, replace 2 (e, 0) ap, Nothing)) i .
> adjust (\ (dt, dp, dv) -> (dt, replace w (f, 0) dp, dv)) d .
> insert e e_ . insert f f_) net
> else Nothing
> loopcut _ _ _ = Nothing
> readback = applyRule cross . fst . applyRule loopcut . fst .
> applyRule cross . fst . applyRule scope . fst .
> applyRule cross . fst . applyRule unwind
The Node representation helps to compose INet directly from let expressions.
> data Node = Node {
> nodeType :: NodeType,
> nodeID :: Int,
> nodePorts :: [Node],
> nodeValue :: Maybe Int
> }
> instance Eq Node where
> a == b = nodeID a == nodeID b
> instance Show Node where
> show a = "(" ++ show (nodeID a) ++ ")"
to generate new Node, it requires a unique ID, which can be accomplished by
MonadState.
> applicator fun arg app = incS >>= \i ->
> return $ Node Applicator i [fun, arg, app] Nothing
> abstractor abs body bind = incS >>= \i ->
> return $ Node Abstractor i [abs, body, bind] Nothing
> delimiter to from v = incS >>= \i ->
> return $ Node Delimiter i [to, from] (Just v)
> duplicator out right left v = incS >>= \i ->
> return $ Node Duplicator i [out, right, left] (Just v)
> eraser out = incS >>= \i ->
> return $ Node Eraser i [out] Nothing
> initiator out = incS >>= \i ->
> return $ Node Initiator i [out] Nothing
> tuple top left right = incS >>= \i ->
> return $ Node (Constructor "T") i [top, left, right] Nothing
> twopin arity l top bot = incS >>= \i ->
> return $ Node (TwoPin arity l) i [top, bot] Nothing
> single l top = incS >>= \i ->
> return $ Node (Single l) i [top] Nothing
> dummy top bot = incS >>= \i ->
> return $ Node Dummy i [top, bot] Nothing
> incS :: State Int Int
> incS = do
> i <- get
> put (i + 1)
> return i
> mkNode x = evalState x 0
Converting from Node representation to INet (a tree in this case).
> nodeToNet node = removeDummy $ visit [] empty [node]
> where
> visit :: [Node] -> INet -> [Node] -> INet
> visit visited net [] = net
> visit visited net (x:xs) =
> if elem x visited
> then visit visited net xs
> else
> let ps = zip (nodePorts x) [0..]
> net' = setNet net x (map (\ (i, n) ->
> let i' = nodeID i
> k = nth i n ps
> p = nodePorts i
> qs = zip p [0..]
> j = snd (filter ((x==) . fst) qs !! k)
> in (i', j)) ps)
> in visit (x:visited) net' (xs ++ nodePorts x)
> setNet :: INet -> Node -> [(Int, Int)] -> INet
> setNet net (Node t id _ v) p = insert id (t, p, v) net
> nth i n = length . takeWhile (\ (_, m) -> m < n) . filter (\ (j, _) -> j == i)
> removeDummy net =
> foldr (\ (i, (t, p, v)) net -> case t of
> Dummy ->
> let [(b, j), (c, k)] = p
> in (adjust (\ (bt, bp, bv) -> (bt, replace j (c, k) bp, bv)) b .
> adjust (\ (ct, cp, cv) -> (ct, replace k (b, j) cp, cv)) c .
> delete i) net
> _ -> net) net (toList net)