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)