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   , parseTerm
  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 braced :: String -> String
  27 braced t = "(" ++ t ++ ")"
  28
  29 instance Show Term where
  30   show (Var x) = x
  31   show (Lam x (NTTerm (Lam y t))) = show (Lam (x ++ " " ++ y) t)
  32   show (Lam x t) = braced $ "λ" ++ x ++ "." ++ show t
  33   show (App a (NTTerm (App b c))) = show a ++ " " ++ braced ( show (App b c))
  34   show (App t r) = show t ++ " " ++ show r
  35   show (Let x e1 e2) = braced $ "LET " ++ x ++ " = " ++ show e1 ++ " IN " ++ show e2
  36
  37 instance Show TypedTerm where
  38   show (NTTerm t) = show t
  39   show (TTerm t tp) = braced $ show t ++ " :: " ++ show tp
  40
  41 instance Show Type where
  42   show (Primitive t) = t
  43   show (TypeVar t) = t
  44   show (TypeFunction a b) = braced $ show a ++ " -> " ++ show b
  45
  46 instance Show TypeScheme where
  47   show (TScheme t) = show t
  48   show (TSForAll x t) = braced $ "∀" ++ x ++ ": " ++ show t
  49
  50 tRead :: String -> TypedTerm
  51 tRead s = case parseOnly (parseTypedTerm <* endOfInput) (T.pack s) of
  52     (Right t) -> t
  53     (Left e) -> error e
  54
  55 parseTerm :: Parser Term
  56 parseTerm = parseLet <|>
  57             parseApp <|>
  58             parseVar <|>
  59             parseLambda
  60
  61 parseTermNA :: Parser Term
  62 parseTermNA = parseLet <|>
  63             parseVar <|>
  64             parseLambda
  65
  66 parseTypeAndTermNA :: Parser TypedTerm
  67 parseTypeAndTermNA = do
  68   term <- parseTermNA
  69   string " :: "
  70   tp <- parseTypeScheme
  71   return $! TTerm term tp
  72
  73 parseTypeAndTerm :: Parser TypedTerm
  74 parseTypeAndTerm = do
  75   term <- parseTerm
  76   string " :: "
  77   tp <- parseTypeScheme
  78   return $! TTerm term tp
  79
  80 parseTypedTermNA :: Parser TypedTerm
  81 parseTypedTermNA = parseBraces <|>
  82                    parseTypeAndTermNA <|>
  83                    (NTTerm <$> parseTerm)
  84
  85 parseTypedTerm :: Parser TypedTerm
  86 parseTypedTerm = parseBraces <|>
  87                 parseTypeAndTerm <|>
  88                 (NTTerm <$> parseTerm)
  89
  90 parseType :: Parser Type
  91 parseType = parsePrimitive <|>
  92             parseTypeVar <|>
  93             parseTypeFunction
  94
  95 parsePrimitive :: Parser Type
  96 parsePrimitive = do
  97   x <- many1 $ satisfy isAsciiUpper
  98   return $! Primitive x
  99
 100 parseTypeVar :: Parser Type
 101 parseTypeVar = do
 102   x <- many1 $ satisfy isAsciiLower
 103   return $! TypeVar x
 104
 105 parseTypeFunction :: Parser Type
 106 parseTypeFunction = do
 107   a <- parseType
 108   string " -> "
 109   b <- parseType
 110   return $! TypeFunction a b
 111
 112 parseTypeScheme :: Parser TypeScheme
 113 parseTypeScheme = parseForAll <|>
 114                   (TScheme <$> parseType)
 115
 116 parseForAll :: Parser TypeScheme
 117 parseForAll = do
 118   string "FORALL "
 119   (TypeVar x) <- parseTypeVar
 120   string "."
 121   t <- parseTypeScheme
 122   return $! TSForAll x t
 123
 124 parseBraces :: Parser TypedTerm
 125 parseBraces = do
 126   char '('
 127   t <- parseTypedTerm
 128   char ')'
 129   return t
 130
 131 parseLet :: Parser Term
 132 parseLet = do
 133   string "LET "
 134   (Var x) <- parseVar
 135   string " = "
 136   e1 <- parseTypedTerm
 137   string " IN "
 138   e2 <- parseTypedTerm
 139   return $! Let x e1 e2
 140
 141 parseVar :: Parser Term
 142 parseVar = do
 143   x <- many1 $ satisfy isAsciiLower
 144   return $! Var x
 145
 146 parseLambda :: Parser Term
 147 parseLambda = do
 148   char '\\' <|> char 'λ' <|> char 'L'
 149   vars <- sepBy1 parseVar (char ' ')
 150   char '.'
 151   t <- parseTypedTerm
 152   let (NTTerm l) = createLambda vars t
 153   return $! l
 154
 155 parseApp :: Parser Term
 156 parseApp = do
 157   aps <- sepBy1 parseTypedTermNA (char ' ')
 158   return $! createApp aps
 159
 160 createLambda :: [Term] -> TypedTerm -> TypedTerm
 161 createLambda (Var x : vs) t = NTTerm . Lam x $ createLambda vs t
 162 createLambda [] t = t
 163 createLambda _ _ = error "createLambda failed"
 164
 165 createApp :: [TypedTerm] -> Term
 166 createApp [t,ts] = App t ts
 167 createApp (t:ts:tss) = createApp (NTTerm (App t ts) : tss)
 168 createApp [] = error "empty createApp"
 169
 170
 171 -- |
 172 -- TODO prop> t == tRead (show (t :: Term))