Interactive Net for Lambdascope implmenetation

> {-# LANGUAGE TupleSections #-}
> module INet where

> import Diagram

> 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 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.

> type NetPort = (NodeID, Int)
> type NodeID = Int

> data NodeType = Applicator
>               | Applicator'                             -- flip of Applicator
>               | Abstractor 
>               | Delimiter 
>               | Delimiter'                              -- flip of Delimiter
>               | Duplicator DupKind
>               | Eraser
>               | Dummy                                   -- dummy for self-loop
>               | Initiator                               -- never destroyed
>               | 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

 netToDiagram :: Net -> Diagram

> netToDiagram net = 
>   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) [] $
>                 adjust $ 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 k -> drawDup (maybe "" show (v::Maybe Int)) k
>             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)
>         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, (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, _) = (fst 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 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 = (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.

> ruleM :: Monad m => LocalRule -> LocalRuleM m
> ruleM = (((return .) .) .)

> 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) = 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' :: 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 :: Monad m => LocalRuleM m -> RuleM m
> outermost rule net@(netMap, _) =
>   case findInitiator $ toList netMap of
>     Just (i, _) -> outermost' [] [i]
>     Nothing -> return (net, 0)
>   where 
>     outermost' _ [] = return (net, 0)
>     outermost' visited (i:is) =
>       let a@(at, ((j, _):ps), _) = netMap ! i      
>           b = netMap ! j
>       in if elem i visited
>         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 ->-
> (->-) :: 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 +>+
> (+>+) :: 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 :: LocalRule
> cross x@(i, a@(at, ap, av)) y@(j, b@(bt, bp, bv)) = 
>   if head bp == (i, 0)                          -- princple ports meet?
>     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) -> 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
>         (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 (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 $ 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' (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 (i, a) (j, b) 
>       else case (at, bt) of                     -- different type
>         (Delimiter, _) -> Just . commute (i, a) (j, b) 
>         (_, Delimiter) -> Just . commute (i, a) (j, b) 
>         _ -> const Nothing
>     else const Nothing

> {-

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 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 (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))
>          : 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' = 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) 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 (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 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 . 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 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@(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 
>     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 (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 (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 (i, a@(at, ap, _)) (j, b@(bt, bp, _)) =
>   case (head bp == (i, 0), at, bt) of
>     (True, Applicator, Abstractor) -> Just . beta' (i, a) (j, b) 
>     (True, Abstractor, Applicator) -> Just . beta' (j, b) (i, a) 
>     _ -> const Nothing

> 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 (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

> 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

> 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 $ first
>         (adjust (const (Applicator', [(d, w), (b, u), (c, v)], Nothing)) i .
>          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 $ first
>         (adjust (const (Applicator, [(c, v), (d, w), (b, u)], Nothing)) i .
>          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) = first
>       (adjust (const (at', [(c, v), (b, u)], av)) i .
>        adjust (replaceP u (i, 1)) b .
>        adjust (replaceP v (i, 0)) c) net

> scope = tryBoth scope'
> scope' (i, a@(TwoPin _ _, _, _)) = upsideDown (i, a)
> scope' (i, a@(Delimiter, _, _))  = upsideDown (i, a)
> scope' _ = const Nothing

> 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 (\ (dt, dp, dv) -> (dt, replace w (f, 0) dp, dv)) d .
>         insert e e_ . insert f f_) net, maxID + 2)
>      else Nothing
> loopcut' _ _ = Nothing

> 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.

> 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)
> 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 Dup) 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 = let net = removeDummy $ visit [] empty [node] in (net, maximum $ 0:(keys net))
>   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 (replaceP j (c, k)) b .
>               adjust (replaceP k (b, j)) c .
>               delete i) net
>         _ -> net) net (toList net)