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