src/Lambda/Parser/Fancy.hs

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