src/Lambda/Parser/Simple.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind -fno-warn-orphans #-}
   2
   3 -- |
   4 -- Module      :  Lambda.Parser.Simple
   5 -- Copyright   :  Tomáš Musil 2014
   6 -- License     :  BSD-3
   7 --
   8 -- Maintainer  :  tomik.musil@gmail.com
   9 -- Stability   :  experimental
  10 --
  11 -- Simple parser for λ-terms. Corresponds to the recursive λ-term definition. Application is always in brackets, nothing else is.
  12
  13
  14 module Lambda.Parser.Simple
  15   ( tRead
  16   , parseTerm
  17   )  where
  18
  19 import Data.Text as T
  20 import Data.Attoparsec.Text
  21 import Control.Applicative
  22
  23 import Lambda.Term
  24
  25 -- $setup
  26 -- >>> import Test.QuickCheck
  27 -- >>> import Test.Term hiding (tRead, parseTerm)
  28
  29 -- |
  30 -- >>> tShow $ Lambda "x" (Var "x")
  31 -- "\\x.x"
  32 -- >>> tShow $ App (Var "x") (Var "y")
  33 -- "(x y)"
  34
  35 tShow :: Term -> String
  36 tShow (Var x) = x
  37 tShow (Lambda x t) = "\\" ++ x ++ "." ++ tShow t
  38 tShow (App t r) = "(" ++ tShow t ++ " " ++ tShow r ++ ")"
  39
  40 -- |
  41 -- prop> t == tRead (tShow t)
  42
  43 tRead :: String -> Term
  44 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  45     (Right t) -> t
  46     (Left e) -> error e
  47
  48 parseVar :: Parser Term
  49 parseVar = do
  50   x <- many1 letter
  51   return $! Var x
  52
  53 parseLambda :: Parser Term
  54 parseLambda = do
  55   char '\\'
  56   (Var x) <- parseVar
  57   char '.'
  58   t <- parseTerm
  59   return $! Lambda x t
  60
  61 parseApp :: Parser Term
  62 parseApp = do
  63   char '('
  64   t <- parseTerm
  65   char ' '
  66   r <- parseTerm
  67   char ')'
  68   return $! App t r
  69
  70 parseTerm :: Parser Term
  71 parseTerm = parseVar <|> parseLambda <|> parseApp
  72
  73