src/HM/Parser.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind -fno-warn-orphans #-}
   2 {-# LANGUAGE OverloadedStrings #-}
   3
   4 -- |
   5 -- Module      :  HM.Parser
   6 -- Copyright   :  Tomáš Musil 2014
   7 -- License     :  BSD-3
   8 --
   9 -- Maintainer  :  tomik.musil@gmail.com
  10 -- Stability   :  experimental
  11 --
  12 -- Parser for Hindley-Milner terms and types.
  13
  14 module HM.Parser
  15   ( tRead
  16   , parseTypedTerm
  17   )  where
  18
  19 import Data.Char (isAsciiLower, isAsciiUpper)
  20 import Data.Text as T hiding (map)
  21 import Data.Attoparsec.Text
  22 import Control.Applicative
  23
  24 import HM.Term
  25
  26 -- $setup
  27 -- >>> import Test.QuickCheck
  28 -- >>> import Test.HM.Term
  29
  30 -- |
  31 -- >>> print $ Lam "x" (Var "x")
  32 -- (λx.x)
  33
  34
  35
  36 braced :: String -> String
  37 braced t = "(" ++ t ++ ")"
  38
  39 instance Show Term where
  40   show (Var x) = x
  41   show (Lam x (NTTerm (Lam y t))) = show (Lam (x ++ " " ++ y) t)
  42   show (Lam x t) = braced $ "λ" ++ x ++ "." ++ show t
  43   show (App a (NTTerm (App b c))) = show a ++ " " ++ braced ( show (App b c))
  44   show (App t r) = show t ++ " " ++ show r
  45   show (Let x e1 e2) = braced $ "LET " ++ x ++ " = " ++ show e1 ++ " IN " ++ show e2
  46
  47 instance Show TypedTerm where
  48   show (NTTerm t) = show t
  49   show (TTerm (Var x) tp) = x ++ " :: " ++ show tp
  50   show (TTerm t tp) = braced (show t) ++ " :: " ++ show tp
  51
  52 instance Show Type where
  53   show (Primitive t) = t
  54   show (TypeVar t) = t
  55   show (TypeFunction a b) = braced $ show a ++ " -> " ++ show b
  56
  57 instance Show TypeScheme where
  58   show (TScheme t) = show t
  59   show (TSForAll x t) = braced $ "∀" ++ x ++ ": " ++ show t
  60
  61 tRead :: String -> TypedTerm
  62 tRead s = case parseOnly (parseTypedTerm <* endOfInput) (T.pack s) of
  63     (Right t) -> t
  64     (Left e) -> error e
  65
  66 parseTerm :: Parser Term
  67 parseTerm = parseLet <|>
  68             parseApp <|>
  69             parseBraces parseTerm <|>
  70             parseVar <|>
  71             parseLambda
  72
  73 parseTermNoApp :: Parser Term
  74 parseTermNoApp = parseBraces parseTerm <|>
  75             parseLet <|>
  76             parseVar <|>
  77             parseLambda
  78
  79 parseTypeAndTerm :: Parser Term -> Parser TypedTerm
  80 parseTypeAndTerm p = do
  81   term <- p
  82   string " :: "
  83   tp <- parseTypeScheme
  84   return $! TTerm term tp
  85
  86
  87 parseTypedTermNoApp :: Parser TypedTerm
  88 parseTypedTermNoApp = parseTypeAndTerm parseTermNoApp <|>
  89                       parseBraces parseTypedTerm <|>
  90                       (NTTerm <$> parseTermNoApp)
  91
  92 parseTypedTerm :: Parser TypedTerm
  93 parseTypedTerm = parseTypeAndTerm parseTerm <|>
  94                  parseBraces parseTypedTerm <|>
  95                  (NTTerm <$> parseTerm)
  96
  97 parseType :: Parser Type
  98 parseType = parseBraces parseType <|>
  99             parseTypeFunction <|>
 100             parsePrimitive <|>
 101             parseTypeVar
 102
 103 parsePrimitive :: Parser Type
 104 parsePrimitive = do
 105   x <- many1 $ satisfy isAsciiUpper
 106   return $! Primitive x
 107
 108 parseTypeVar :: Parser Type
 109 parseTypeVar = do
 110   x <- many1 $ satisfy isAsciiLower
 111   return $! TypeVar x
 112
 113 parseTypeFunction :: Parser Type
 114 parseTypeFunction = do
 115   a <- parseBraces parseType <|> parsePrimitive <|> parseTypeVar
 116   string " -> "
 117   b <- parseType
 118   return $! TypeFunction a b
 119
 120 parseTypeScheme :: Parser TypeScheme
 121 parseTypeScheme = parseBraces parseTypeScheme <|>
 122                   parseForAll <|>
 123                   (TScheme <$> parseType)
 124
 125 parseForAll :: Parser TypeScheme
 126 parseForAll = do
 127   string "FORALL "
 128   (TypeVar x) <- parseTypeVar
 129   string ": "
 130   t <- parseTypeScheme
 131   return $! TSForAll x t
 132
 133 parseBraces :: Parser a -> Parser a
 134 parseBraces p = do
 135   char '('
 136   t <- p
 137   char ')'
 138   return t
 139
 140 parseLet :: Parser Term
 141 parseLet = do
 142   string "LET "
 143   (Var x) <- parseVar
 144   string " = "
 145   e1 <- parseTypedTerm
 146   string " IN "
 147   e2 <- parseTypedTerm
 148   return $! Let x e1 e2
 149
 150 parseVar :: Parser Term
 151 parseVar = do
 152   x <- many1 $ satisfy isAsciiLower
 153   return $! Var x
 154
 155 parseLambda :: Parser Term
 156 parseLambda = do
 157   char '\\' <|> char 'λ' <|> char 'L'
 158   vars <- sepBy1 parseVar (char ' ')
 159   char '.'
 160   t <- parseTypedTerm
 161   let (NTTerm l) = createLambda vars t
 162   return $! l
 163
 164 parseApp :: Parser Term
 165 parseApp = do
 166   aps <- sepBy1 parseTypedTermNoApp (char ' ')
 167   createApp aps
 168
 169 createLambda :: [Term] -> TypedTerm -> TypedTerm
 170 createLambda (Var x : vs) t = NTTerm . Lam x $ createLambda vs t
 171 createLambda [] t = t
 172 createLambda _ _ = error "createLambda failed"
 173
 174 createApp :: [TypedTerm] -> Parser Term
 175 createApp [t,ts] = return $ App t ts
 176 createApp (t:ts:tss) = createApp (NTTerm (App t ts) : tss)
 177 createApp _ = fail "not App"
 178
 179
 180 -- |
 181 -- TODO prop> t == tRead (show (t :: Term))