LambdaINet-0.1.0: src/Lambda.lhs

Generalized Lambda for Lambdascope

> {-# LANGUAGE RecursiveDo #-}

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

> 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) = mdo
>   e <- eraser x
>   es <- erasers xs
>   return $ e : es

> termToNet i Z ps = debug ("termToNet: Z " ++ show i) $ mdo
>   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 = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo
>   let inp = head ps
>       out = head (drop i ps)
>       mid = take (i - 1) (tail ps)
>   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 = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo
>   let inp = head ps
>   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) $ mdo
>   let inp = head ps
>   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) = mdo
>       d <- duplicator c b a 0
>       ds <- dup (i - 1) as bs cs
>       return $ d : ds

> termToNet i x@(Y t) ps = debug ("termToNet: " ++ show x ++ " " ++ show i) $ mdo
>   let inp = head ps
>   d <- duplicator 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) $ mdo
>   let inp = head ps
>   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) = mdo
>       d <- duplicator c b a 0
>       ds <- dup (i - 1) as bs cs
>       return $ d : ds

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

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

> netToTerm :: INet -> Term
> netToTerm net = 
>   let Just (i, (_, [(b, u)], _)) = findInitiator (toList (debug1 "netToTerm net=" 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 net (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
>   where
>     project n =
>       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 .
>         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 ++ ")"
>           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
>         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

> meta net a b@(_, (TwoPin _ _, _, _)) = meta net b a
> meta _ _ _ = 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..]