[ create a new paste ] login | about

Link: http://codepad.org/OxSlVOOP    [ raw code | fork ]

Haskell, pasted on May 1:
-- A Lambda Calculator.

module Main where
import Control.Monad (ap)
import Control.Applicative ((<$>),(<*>))
import Control.Monad.State
import Text.ParserCombinators.Parsec hiding (getInput, State)
import Network.CGI
import System.IO
import System.Process (runInteractiveProcess, waitForProcess)
import qualified Data.ByteString.Lazy as L
import qualified Data.ByteString as B
import qualified Data.ByteString.UTF8 as BU
import qualified Data.ByteString.Lazy.UTF8 as LU 
import Codec.Binary.UTF8.String (decodeString, encodeString)
import Data.Char (isLower)
import Data.Maybe (fromMaybe)
import Text.XHtml
import Test.QuickCheck 
import Numeric (readDec)
import Data.List (delete, union)

-- The main data type Term is inductively defined.
data Term = Var Var | Lam Var Term | App Term Term deriving Eq
newtype Var = V String deriving (Eq, Show)

-- Generic traversal (or map) on Term. 
imap, everywhere :: (Term -> Term) -> Term -> Term
imap h (Lam v e) = Lam v (imap h e)
imap h (App f e) = App (imap h f) (imap h e)
imap h e = e
-- Top-down traversal.
everywhere h e = imap (everywhere h) (h e)
-- Top-down traversal that can optionally be stopped.
everywhere' :: (Term -> Maybe Term) -> Term -> Term
everywhere' h e = maybe e (imap (everywhere' h)) (h e)
-- Monadic top-down traversal.
imapM, everywhereM :: Monad m => (Term -> m Term) -> Term -> m Term
imapM h (Lam v e) = return (Lam v) `ap` imapM h e
imapM h (App f e) = return App `ap` imapM h f `ap` imapM h e
imapM h e = return e
everywhereM h e = h e >>= imapM (everywhereM h)

-- Generic fold on Term.
fold :: (Var -> a) -> (Var -> a -> a) -> (a -> a -> a) -> Term -> a
fold i g h = fold'
  where
    fold' (Var v)   = i v
    fold' (Lam v e) = g v (fold' e)
    fold' (App f e) = h (fold' f) (fold' e)

-- Render a Term to string, and only use paranthesis when necessary.
pr s = "(" ++ s ++ ")" 
render = snd . fold i g h
  where 
    i (V v)       = (either id id, v)
    g (V v) (_,e) = (either pr pr, "λ" ++ v ++ "." ++ e)
    h (b,f) (d,e) = (either id pr, b (Left f) ++ " " ++ d (Right e))

instance Show Term where
  show = render

-- Compute free variables in a term.
freeVars = fold (:[]) delete union

-- Reduce at a particular redex: if it requires alpha renaming
-- before the beta reduction, it'll only alpha rename; otherwise,
-- it'll beta reduce.
reduce :: Term -> Integer -> Term
reduce t i = evalState (beta t) 0
  where
    beta (Var v)   = return $ Var v
    beta (Lam v e) = Lam v <$> beta e 
    beta (App f e) =
      let doit = App <$> beta f <*> beta e 
      in case f of
        Lam v b -> do
          j <- get
          if j == i
            then let b' = prepare e b
                 in return $ if b == b' then subst v e b'
                                        else App (Lam v b') e
            else put (j + 1) >> doit
        _       -> doit

-- Alpha rename all free variable u with w.

alpha :: Var -> Var -> Term -> Term
alpha u w = subst u (Var w)

{-
subst :: Var -> Term -> Term -> Term
subst u w (Var v) = if v == u then w else Var v
subst u w (Lam v e) = if v == u then Lam v e else Lam v (subst u w e)
subst u w (App f e) = App (subst u w f) (subst u w e)
-}
subst u w e = everywhere' h e
  where h (Var v)   | v == u = Just w 
        h (Lam v e) | v == u = Nothing
        h e = Just e

-- Alpha rename term b by avoiding capturing free variables in e.

prepare :: Term -> Term -> Term
prepare e b = evalState (recurse [] b) vars
  where
    fs = freeVars e
    atoz = ['a' .. 'z']
    full = map V (map (:[]) atoz ++ [ v : show m | v <- atoz, m <- [0..]])
    vars = [ v | v <- full, v `notElem` fs]
    recurse _   (Var v) = return $ Var v
    recurse env (Lam u w) = do
      (u', w') <- if u `elem` fs
        then do
          (v:vs) <- filter (`notElem` env) <$> get
          put vs
          return (v, alpha u v w)
        else return (u, w)
      Lam u' <$> recurse (u':env) w'
    recurse env (App f e) = App <$> recurse env f <*> recurse env e

-- Prepare term for QuickCheck.

instance Arbitrary Var where
  arbitrary = do
    f <- choose ('a', 'z')
    c <- choose (False, True)
    d <- choose (0::Int, 100)
    return $ V $ if c then [f] else f : show d

instance Arbitrary Term where
  arbitrary = do
    i <- choose (0::Int, 2)
    case i of
      0 -> Var <$> arbitrary 
      1 -> Lam <$> arbitrary <*> arbitrary 
      2 -> App <$> arbitrary <*> arbitrary

--We also provide a Parsec parser to read in Term.

parens = between (char '(') (char ')')
pTerm = pVarOrApp <|> pLam <|> parens pTerm

pVar = Var . V <$> pLit 
pNum = many1 digit
pLit = do
 c <- satisfy (\c -> isLower c && c /= 'λ')
 n <- optionMaybe pNum
 notFollowedBy digit
 case n of
   Just x  -> return (c : x)
   Nothing -> return [c]

pLam = do
 char '\\' <|> char 'λ'
 spaces
 v <- pLit
 spaces
 char '.'
 spaces
 t <- pTerm
 return (Lam (V v) t)

pVarOrApp = do
  f <- pVar <|> parens pTerm
  e <- many (many1 space >> (pVar <|> parens pTerm <|> pLam))
  return $ if null e then f else foldl App f e

parseTerm :: String -> Either ParseError Term
parseTerm e = parse (pTerm >>= \e -> eof >> return e) e e

--The following property should pass for Quickcheck, which can be
--verified by "quickCheck propTerm".

propTerm :: Term -> Bool
propTerm t = either (const False) (t==) (parseTerm (show t))

--Additionally, we want to display the Term as a hierachical tree
--using DOT. It means we need to serialize a Term value as a graph
--specification written in the DOT language.

type NodeId     = Int
newtype Node  a = Node (NodeId, a)
newtype Edge    = Edge ((NodeId, NodeId), NodeId)
newtype Graph a = Graph ([Node a], [Edge])
type M a = State (NodeId, Graph String) a

--We use a state monad to generate unique IDs for each node in the
--Term, and with which we'll be able to label the edges.

newNodeId = get >>= \(i, g) -> put (i + 1, g) >> return i
putNode n = get >>= \(i, Graph (ns, es)) -> put (i, Graph (n:ns, es))
putEdge e = get >>= \(i, Graph (ns, es)) -> put (i, Graph (ns, e:es))

toNode :: Term -> M NodeId
toNode e = do
  n <- newNodeId
  case e of
    Var (V v) -> putNode (Node (n, v))
    Lam (V v) t -> do
      i <- toNode (Var (V v))
      j <- toNode t
      putNode $ Node (n, "λ . ")
      putEdge $ Edge ((n, 1), i)
      putEdge $ Edge ((n, 3), j)
    App f e -> do
      i <- toNode f
      j <- toNode e
      putNode $ Node (n, "   ")
      putEdge $ Edge ((n, 0), i)
      putEdge $ Edge ((n, 2), j)
  return n

toGraph :: Term -> Graph String
toGraph e = snd $ snd $ runState (toNode e) (0, Graph ([],[]))

toDot :: Term -> String
toDot e = unlines $
  ["digraph g {"
  ,"node [shape = record, color = lightgrey, height = .06 ];" ] ++
  map showNode ns ++
  map showEdge es ++ ["}"]
  where
    Graph (ns, es) = toGraph e
    showNode (Node (i, s)) = "node" ++ show i ++
      if length s == 1 then "[label=\"" ++ s ++ "\", shape = none]"
                       else "[label=\"" ++ toGrid 0 s ++ "\"];"
    showEdge (Edge ((i, p), j)) = "\"node" ++ show i ++ "\":f" ++ show p ++
      " -> \"node" ++ show j ++ "\" [ color = lightgrey, arrowsize = 0.5];"
    toGrid _ []       = ""
    toGrid f (c:xs) = "<f" ++ show f ++ "> " ++
      (c : if null xs then "" else '|' : toGrid (f + 1) xs)

--Next, we want to render a Term as a clickable HTML string, with mouseover
--to highlight a redex, and mouseclick to perform alpha or beta reduction.
--This is similar to serializing a Term as a strings with proper parenthesis
--grouping, except that such a string must be broken into parts to insert
--various HTML/Javascript fragments to enable the highlighting, and clicking.

markRedex :: Term -> String
markRedex (Var (V v)) = v
markRedex (Lam (V v) e) = "λ" ++ v ++ "." ++ markRedex e
markRedex (App f e) =
  let s = markRedex f
      t = markRedex e
      pr s = "(" ++ s ++ ")"
      r = case f of { Lam _ _ -> pr s; _ -> s } ++ " " ++
          case e of { Var _   -> t; _ -> pr t }
  in case f of
       Lam _ _ -> "[" ++ r ++ "]"
       _       -> r

quoteAnchor h _ s | null s = noHtml
quoteAnchor h level s =
  (anchor << s) !
    [ theclass "normal",
      href (h ++ "&r=" ++ i),
      strAttr "onmouseover" $ "javascript:redexOver(" ++ i ++ ");",
      strAttr "onmouseout"  $ "javascript:redexOut(" ++ i ++ ");",
      name l]
  where i = show (head level)
        l = concatMap (\i -> ':' : show i) level ++ ":"

annotate :: String -> Int -> [Int] -> Html -> String -> String -> Html
annotate h n l pre word ('[':s) | not (null l) =
  annotate h (n+1) (n:l) (pre +++ quoteAnchor h l (reverse word)) "" s
annotate h n l pre word ('[':s) =
  annotate h (n+1) (n:l) (pre +++ reverse word) "" s
annotate h n l pre word (']':s) =
  annotate h n (tail l) (pre +++ quoteAnchor h l (reverse word)) "" s
annotate h n l pre word (c:s) = annotate h n l pre (c:word) s
annotate _ _ _ pre word [] = pre +++ stringToHtml (reverse word)

--We also produce some lines to show the levels of redexes.

levels :: Int -> [Int] -> String -> [Int]
levels n l ('[':s) = levels (n + 1) l s
levels n l (']':s) = levels (n - 1) l s
levels n l (c:s)   = levels n (n : l) s
levels _ l [] = reverse l

toLines :: [Int] -> [String]
toLines l = if all (==0) l' then [s] else s : toLines l'
  where
    mkLine = unzip . map (\x -> if x > 0 then ('_', x - 1) else (' ', x))
    (s, l') = mkLine l

toScript :: String -> Term -> Html
toScript e exp =
  thediv ! [theclass "front mono", identifier "exp"] <<
  annotate href 0 [] noHtml "" exp' +++ thediv ! [theclass "back mono"] <<
  unlines (toLines (levels 0 [] exp'))
  where
    exp'  = markRedex exp
    href  = "?term=" ++ e

--Eventually, we want to run the dot command from the system, render
--the graph as a PNG, and read it back as binary data.

toPNG :: (String -> IO a) -> Term -> IO L.ByteString
toPNG err e = do
  let input = toDot e
  (inp, out, _, proc) <- runInteractiveProcess "/usr/local/bin/dot" ["-Tpng"]
                           Nothing Nothing
  s <- catch (do
         B.hPutStrLn inp (BU.fromString input)
         B.hPutStrLn inp B.empty
         hClose inp
         L.hGetContents out)
       (\e -> err "Broken Pipe: perhaps your path to dot is wrong?" >>
              return L.empty)
  err $ show $ L.length s
  exitcode <- waitForProcess proc
  err $ show exitcode
  return s

--Finally, we run the entire process as a CGI program.

htmlHeader = setContentType "text/html; charset=utf-8"
textHeader = setContentType "text/plain; charset=utf-8"
setContentType = setHeader "Content-Type"

inputForm e = form <<
  [ olist << map (li <<) introtext
  , textfield "term" ! [ theclass "mono", value e ], submit "" "Submit"]

page e redex =
  header << (thetitle << "Lambda Viewer" +++ sty +++ js) +++ body <<
  if null e
    then inputForm e
    else case parseTerm e of
      Left err  -> inputForm e +++ paragraph << show err
      Right exp -> case redex of
        Just r  -> let e = reduce exp r
                       s = show e
                   in inputForm s +++ display s e
        Nothing -> inputForm e +++ display e exp
  where
    sty = style << primHtml stylesheet
    js  = (script << primHtml javascript)  !
            [ strAttr "language" "JavaScript"]
    display s e = toScript s e +++
      paragraph (image ! [src ("/cgi-bin/lambda?s=" ++ s)])

trimHead = dropWhile (==' ')
trim = trimHead . reverse . trimHead . reverse

cgiMain = do
  t <- getInput "term"
  r <- getInput "r"
  s <- getInput "s"
  let term  = trim (decodeString(fromMaybe "" t))
      readInt s = case readDec s of { [(i,_)] -> i; _ -> 0 }
      redex = fmap readInt r
  case s of
    Nothing -> htmlHeader >> (outputFPS $ LU.fromString $ renderHtml (page term redex))
    Just s0 ->
      case parseTerm (decodeString s0) of
        Left err -> textHeader >> (outputFPS $ LU.fromString $ show err)
        Right e  -> do
          f <- liftIO $ toPNG (\_ -> return ()) e
          setHeader "Content-type" "image/png"
          outputFPS f

main = runCGI $ handleErrors cgiMain

-- The rest are the introduction text, style sheet and java script.

introtext  =
  [ "You may use \\ for the λ symbol, and ( and ) to group lambda terms."
  , "A space is required to denote application."
  , "The scope of abstraction extends to the rightmost."
  , "Application is left associative."
  ]
stylesheet = concat
  [ "#term { width : 30em; }"
  , "#exp { color: blue; }"
  , ".normal { color: blue; }"
  , ".bright { color: purple; }"
  , ".mono { font-size: 11pt; font-family: monospace; }"
  , ".front { position: relative; z-index: 2; margin-top: 5pt;"
  ,         " white-space: pre; }"
  , ".back  { position: relative; top: -6pt; color: lightgrey;"
  ,         " z-index: 1; white-space: pre; line-height: 3px; }"
  , "a:link, a:visited, a:active, a:hover { text-decoration: none; }"
  ]
javascript = concat
  [ "function redex(id, name) { var i, a;"
  , "for (i = 0; (a = document.getElementsByTagName('a')[i]); i++) { "
  , "  if (a.getAttribute('name').indexOf(':' + id + ':') >= 0) "
  , "     { a.className=name; }}}"
  , "function redexOver(id) { redex(id,'bright') }"
  , "function redexOut(id)  { redex(id,'normal') }"
  ]


Create a new paste based on this one


Comments: