Guest User

Untitled

a guest
Feb 11th, 2014
44
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module Main where
  2.  
  3. import Data.List
  4. import Control.Monad
  5. import Text.Parsec
  6. import Text.Parsec.String
  7.  
  8. -- Definition
  9.  
  10. type Sym = String
  11.  
  12. data Term = Var Sym | Lam Sym Term | App Term Term
  13.  
  14. -- Substituion
  15.  
  16. freeVars (Var s) = [s]
  17. freeVars (Lam s e) = freeVars e \\ [s]
  18. freeVars (App e1 e2) = freeVars e1 `union` freeVars e2
  19.  
  20. subst s1 e2 = subst' where
  21. subst' e1@(Var s1')
  22. | s1 == s1' = e2
  23. | otherwise = e1
  24. subst' e1@(Lam s1' e1')
  25. | s1 == s1' = e1
  26. | s1' == "_" || s1' `notElem` frees_e2 = Lam s1' (subst' e1')
  27. | otherwise = Lam s1'' e1'' where
  28. frees_e2 = freeVars e2
  29. frees_e2_e1' = frees_e2 `union` freeVars e1'
  30. s1'' = until (`notElem` frees_e2_e1') ('\'':) s1'
  31. e1'' = subst' (subst s1' (Var s1'') e1')
  32. subst' (App e1'1 e1'2) = App (subst' e1'1) (subst' e1'2)
  33.  
  34. -- Beta-reduction
  35.  
  36. eager into (App e1 e2) = case (eager into e1, eager into e2) of
  37. (Lam s1 e1, e2') -> eager into (subst s1 e2' e1)
  38. (e1' , e2') -> App e1' e2'
  39. eager into l@(Lam s e) = if into then Lam s (eager into e) else l
  40. eager _ v = v
  41.  
  42. byvalue = eager False
  43. full = eager True
  44.  
  45. -- Printing
  46.  
  47. pretty = tail . pretty' where
  48. pretty' (Var s) = " " ++ s
  49. pretty' (App e1 e2) = (case e1 of
  50. Lam _ _ -> " (" ++ pretty e1 ++ ") "
  51. _ -> " " ++ pretty e1 ++ " "
  52. ) ++ case e2 of
  53. Var s2 -> s2
  54. _ -> "(" ++ pretty e2 ++ ")"
  55. pretty' e = " \\" ++ tail (pretty'' e) where
  56. pretty'' (Lam s e) = " " ++ s ++ pretty'' e
  57. pretty'' e = ". " ++ pretty e
  58.  
  59. -- Parsing
  60.  
  61. betweenSpaces = spaces `between` spaces
  62. sep1Spaces p = spaces >> (p `sepEndBy1` spaces)
  63.  
  64. ident = string "where!" <|> liftM2 (:) (char '_' <|> letter) (many $ alphaNum <|> oneOf "_\'")
  65.  
  66. parseOne = liftM Var (try ident) <|> (char '(' `between` char ')' $ parseTerm)
  67.  
  68. parseAlone = liftM2 (flip $ foldr Lam)
  69. (spaces >> (option [] $ char '\\' `between` char '.' $ sep1Spaces ident))
  70. (try (liftM (foldl1 App) $ sep1Spaces parseOne) <|> parseAlone)
  71.  
  72. parseAss = betweenSpaces $ liftM2 (,) ident (betweenSpaces (char '=') >> parseTerm)
  73.  
  74. parseTerm :: Parser Term
  75. parseTerm = liftM2 (foldr $ \(s, e2) e1 -> App (Lam s e1) e2) parseAlone
  76. (option [] $ string "where" `between` char '.' $ parseAss `sepBy` (betweenSpaces $ char ';'))
  77.  
  78. -- Example
  79.  
  80. evalAndPrint s = case parse parseTerm "" s of
  81. Left err -> error $ show err
  82. Right res -> putStrLn $ pretty $ full $ byvalue res
  83.  
  84. main = readFile "term.txt" >>= evalAndPrint
RAW Paste Data