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.Char (isAsciiLower)
  26 import Data.Text as T hiding (map)
  27 import Data.Attoparsec.Text
  28 import Control.Applicative
  29
  30 import Lambda.Term
  31
  32 -- $setup
  33 -- >>> import Test.QuickCheck
  34 -- >>> import Test.Term
  35
  36 -- |
  37 -- >>> print $ Lambda "x" (Var "x")
  38 -- (λx.x)
  39
  40 instance Show Term where
  41   show (Var x) = x
  42   show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
  43   show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
  44   show (AppApp a b c) = show a ++ " " ++ braced (App b c)
  45   show (App t r) = show t ++ " " ++ show r
  46
  47 braced :: Term -> String
  48 braced t = "(" ++ show t ++ ")"
  49
  50 -- |
  51 -- prop> t == tRead (show (t :: Term))
  52
  53 tRead :: String -> Term
  54 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  55     (Right t) -> t
  56     (Left e) -> error e
  57
  58 parseVar :: Parser Term
  59 parseVar = do
  60   x <- many1 letter
  61   return $! Var x
  62
  63 parseLambda :: Parser Term
  64 parseLambda = do
  65   char '\\' <|> char 'λ' <|> char 'L'
  66   vars <- sepBy1 parseVar (char ' ')
  67   char '.'
  68   t <- parseTerm
  69   return $! createLambda vars t
  70
  71 parseApp :: Parser Term
  72 parseApp = do
  73   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
  74   return $! createApp aps
  75
  76 parseBraces :: Parser Term
  77 parseBraces = do
  78   char '('
  79   t <- parseTerm
  80   char ')'
  81   return t
  82
  83 parseTerm :: Parser Term
  84 parseTerm = parseApp <|>
  85             parseBraces <|>
  86             parseLambda <|>
  87             parseVar
  88
  89 createLambda :: [Term] -> Term -> Term
  90 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
  91 createLambda [] t = t
  92 createLambda _ _ = error "createLambda failed"
  93
  94 createApp :: [Term] -> Term
  95 createApp [t] = t
  96 createApp (t:ts:tss) = createApp (App t ts : tss)
  97 createApp [] = error "empty createApp"
  98