src/Lambda/Parser/Fancy.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind -fno-warn-orphans #-}
   2 {-# LANGUAGE PatternSynonyms #-}
   3
   4 -- |
   5 -- Module      :  Lambda.Parser.Fancy
   6 -- Copyright   :  Tomáš Musil 2014
   7 -- License     :  BSD-3
   8 --
   9 -- Maintainer  :  tomik.musil@gmail.com
  10 -- Stability   :  experimental
  11 --
  12 -- Parser for λ-terms. \'.\' in λ implies brackets to the end of the context.
  13
  14 -- TODO: proper documentation
  15
  16 module Lambda.Parser.Fancy
  17   (
  18   -- * Main parser
  19     tRead
  20   , parseTerm
  21   -- * Auxiliary parsers
  22   , parseVar
  23   )  where
  24
  25 import Data.Text as T hiding (map)
  26 import Data.Attoparsec.Text
  27 import Control.Applicative
  28
  29 import Lambda.Term
  30
  31 -- $setup
  32 -- >>> import Test.QuickCheck
  33 -- >>> import Test.Term
  34
  35 -- |
  36 -- >>> print $ Lambda "x" (Var "x")
  37 -- (λx.x)
  38
  39 instance Show Term where
  40   show (Var x) = x
  41   show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
  42   show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
  43   show (AppApp a b c) = show a ++ " " ++ braced (App b c)
  44   show (App t r) = show t ++ " " ++ show r
  45
  46 braced :: Term -> String
  47 braced t = "(" ++ show t ++ ")"
  48
  49 -- |
  50 -- prop> t == tRead (show (t :: Term))
  51
  52 tRead :: String -> Term
  53 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  54     (Right t) -> t
  55     (Left e) -> error e
  56
  57 parseVar :: Parser Term
  58 parseVar = do
  59   x <- many1 (letter <|> digit)
  60   return $! Var x
  61
  62 parseLambda :: Parser Term
  63 parseLambda = do
  64   char '\\' <|> char 'λ'
  65   vars <- sepBy1 parseVar (char ' ')
  66   char '.'
  67   t <- parseTerm
  68   return $! createLambda vars t
  69
  70 parseApp :: Parser Term
  71 parseApp = do
  72   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
  73   return $! createApp aps
  74
  75 parseBraces :: Parser Term
  76 parseBraces = do
  77   char '('
  78   t <- parseTerm
  79   char ')'
  80   return t
  81
  82 parseTerm :: Parser Term
  83 parseTerm = parseApp <|>
  84             parseBraces <|>
  85             parseLambda <|>
  86             parseVar
  87
  88 createLambda :: [Term] -> Term -> Term
  89 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
  90 createLambda [] t = t
  91 createLambda _ _ = error "createLambda failed"
  92
  93 createApp :: [Term] -> Term
  94 createApp [t] = t
  95 createApp (t:ts:tss) = createApp (App t ts : tss)
  96 createApp [] = error "empty createApp"
  97