Generalized Lambda for Lambdascope

> {-# LANGUAGE DoRec #-}

> module Lambda (
>   Term(..),
>   termToNet,
>   termToNode,
>   netToTerm,
>   meta,
>   pretty
>   ) where

> -- import Diagram hiding (S)
> import INet

> import Control.Monad.Fix
> import Data.IntMap hiding (map)
> import Prelude hiding (take, drop, head, tail, cycle)

> data Term = Z | S Term | Abs Term | App Term Term 
>           | Y Term                                -- fix point
>           | Tup Term Term | Fst Term | Snd Term   -- tuple
>           | VInt Int | VStr String                -- value
>           | VFunc Int String Term                 -- function
>   deriving (Eq, Show)

We need less strict list operators in order for the recursive do to work.

> head ~(x:xs) = x
> tail ~(x:xs) = xs

> take 0 x = []
> take i x = head x : take (i - 1) (tail x)
> drop 0 x = x
> drop i x = drop (i - 1) (tail x)

> erasers [] = return []
> erasers (x:xs) = do
>   rec e <- eraser x
>       es <- erasers xs
>   return $ e : es

> termToNet i Z ps = do
>   let inp = head ps
>       out = head (drop i ps)
>       mid = take (i - 1) (tail ps)
>   a <- dummy inp out     -- dummy used here for proper self-loop
>   es <- erasers mid
>   return $ (a : es) ++ [a]

> termToNet i x@(S t) ps = do
>   let inp = head ps
>       out = head (drop i ps)
>       mid = take (i - 1) (tail ps)
>   rec d <- delimiter (head n) inp 0
>       n <- termToNet (i - 1) t (d : mid)
>       e <- eraser out
>   return $ (d : tail n) ++ [e]

> 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 = do
>   let inp = head ps
>   rec a <- applicator (head m) (head n) inp
>       m <- termToNet i t1 (a : qs)
>       n <- termToNet i t2 (a : qs)
>       qs <- dup i (tail m) (tail n) (tail ps)
>   return $ a : qs
>   where 
>     dup 0 _ _ _ = return []
>     dup i ~(a:as) ~(b:bs) ~(c:cs) = do
>       d <- duplicator c b a 0
>       ds <- dup (i - 1) as bs cs
>       return $ d : ds

> {-
> termToNet i x@(Y t) ps = do
>   let inp = head ps
>   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 = do
>   let inp = head ps
>   rec a <- tuple inp (head m) (head n) 
>       m <- termToNet i t1 (a : qs)
>       n <- termToNet i t2 (a : qs)
>       qs <- dup i (tail m) (tail n) (tail ps)
>   return $ a : qs
>   where 
>     dup 0 _ _ _ = return []
>     dup i ~(a:as) ~(b:bs) ~(c:cs) = do
>       d <- duplicator c b a 0
>       ds <- dup (i - 1) as bs cs
>       return $ d : ds

> termToNet i x (inp:out) = 
>   case x of 
>     Fst t -> do
>       rec a <- twopin 1 "fst" (head n) inp
>           n <- termToNet i t (a:out)
>       return $ a : tail n
>     Snd t -> do
>       rec a <- twopin 1 "snd" (head n) inp
>           n <- termToNet i t (a:out)
>       return $ a : tail n
>     VInt i -> do
>       rec a <- single (show i) inp
>           n <- erasers out
>       return $ a : n
>     VStr s -> do
>       rec a <- single s inp
>           n <- erasers out
>       return $ a : n
>     VFunc arity l t -> do
>       rec a <- twopin arity l (head n) inp
>           n <- termToNet i t (a:out)
>       return $ a : tail n

> termToNode t = do
>   rec e <- initiator a 
>       [a] <- termToNet 0 t [e]
>   return e

> netToTerm :: INet -> Term
> netToTerm (net, _) = 
>   let Just (i, (_, [(b, u)], _)) = findInitiator (toList net)
>   in toTerm (net ! b)
>   where
>     toTerm (Abstractor, [_, (b, _), _], _) = Abs (toTerm (net ! b))
>     toTerm (Applicator', [_, (b, _), (c, _)], _) = App (toTerm (net ! b)) (toTerm (net ! c))
>     toTerm (Delimiter', [_, (b, _)], _) = S (toTerm (net ! b))
>     toTerm (Eraser, _, _) = Z
>     toTerm (Constructor l, xs, _) = 
>       case l of 
>         "T" -> Tup (toTerm (net ! fst (xs !! 1))) (toTerm (net ! fst (xs !! 2)))
>     toTerm (TwoPin' arity l, p, _) = 
>       case l of
>         "fst" -> Fst (toTerm (net ! fst (p !! 1))) 
>         "snd" -> Snd (toTerm (net ! fst (p !! 1))) 
>         l -> VFunc arity l (toTerm (net ! fst (p !! 1)))
>     toTerm (Single' l, p, _) =
>       case l of
>         (a:as) -> if a >= '0' && a <= '9' 
>           then VInt (read l)
>           else VStr l 
>     toTerm n = error $ "illegal toTerm input: " ++ show n

meta rules for tuple handling, etc.

> 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
>     _ -> const Nothing
>   where
>     project n (net, maxID) =
>       let (d, v) = bp !! n
>           (e, w) = bp !! (3 - n)
>           f = maxID + 1
>           f_ = (Eraser, [(e, w)], Nothing)
>       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, 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 .
>           adjust (\ (ct, cp, cv) -> (ct, replace u (i, 0) cp, cv)) c .
>           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, maxID + 1)

> meta a b@(_, (TwoPin _ _, _, _)) = meta b a 
> meta _ _ = const Nothing

a pretty printer for generalized lambda terms.

> show' (x:xs) vars Z = x
> show' (x:xs) vars (S t) = show' xs vars t
> show' env (v:vs) (Abs t) = "(\\" ++ v ++ "." ++ show' (v:env) vs t ++ ")"
> show' env vars (App t t') = "(" ++ show' env vars t ++ " " ++ show' env vars t' ++ ")"
> show' env vars (Y t) = "Y(\\" ++ show' env vars t ++ ")"
> show' env vars (Tup t t') = "(" ++ show' env vars t ++ ", " ++ show' env vars t' ++ ")"
> show' env vars (Fst t) = "(fst " ++ show' env vars t ++ ")"
> show' env vars (Snd t) = "(snd " ++ show' env vars t ++ ")"
> show' env vars (VInt i) = show i
> show' env vars (VStr s) = show s
> show' env vars (VFunc i s t) = s ++ "(" ++ show' env vars t ++ ")"

> pretty = show' [] freshVars

Fresh variables

> freshVars = atoz ++ map (\[x,y]->y++x) (sequence [nats, atoz])
>  where
>    atoz = map (\x -> ['_', x]) ['a' .. 'z']
>    nats = map show [0..]