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