Parser.hs (5780B)
1 module Parser where 2 import Control.Applicative 3 import Control.Monad 4 import Control.Monad.Identity 5 import Control.Monad.Reader 6 import Data.Char 7 import Data.ByteString (ByteString) 8 import Data.Function ((&)) 9 import Sparsec 10 11 import Qul (Qul) 12 import qualified Qul 13 import Qular (Qular) 14 import qualified Qular 15 import Common 16 import Surface 17 18 data Err = ErrUtf8 Loc | Err deriving Show -- TODO 19 20 instance Utf8Error Err where 21 utf8Error = ErrUtf8 22 23 type P q a = ParseT Err (Reader (Parse Err q)) a 24 25 runP :: P q a -> Parse Err q -> ByteString -> Result Err a 26 runP p pq input = runParseT p input locZero `runReader` pq 27 28 pQul :: Parse Err Qul 29 pQul = pWord "bot" *> pure Qul.Alpha 30 <|> pWord "0" *> pure Qul.Zero 31 <|> pWord "1" *> pure Qul.One 32 <|> pWord "top" *> pure Qul.Omega 33 34 pQular :: Parse Err Qular 35 pQular = pWord "bot" *> pure Qular.Alpha 36 <|> pWord "0" *> pure Qular.Zero 37 <|> pWord "1" *> pure Qular.One 38 <|> pWord "top" *> pure Qular.Omega 39 -- TODO: syntax for Aff and Rel 40 41 -------------------------------------------------------------------------------- 42 -- General lexical elements 43 44 isWordStart :: Char -> Bool 45 isWordStart c = isLetter c || isDigit c || c == '_' 46 47 isWordCont :: Char -> Bool 48 isWordCont c = isLetter c || isDigit c || c == '_' || c == '\'' 49 50 isIdentStart :: Char -> Bool 51 isIdentStart c = isLetter c || c == '_' 52 53 isIdentCont :: Char -> Bool 54 isIdentCont = isWordCont 55 56 isReservedIdent :: ByteString -> Bool 57 isReservedIdent s = s == "bot" || s == "top" || s == "let" 58 59 pWs :: Monad m => ParseT Err m ByteString 60 pWs = charWhile isSpace 61 62 pToken :: Monad m => ParseT Err m a -> ParseT Err m a 63 pToken p = p <* pWs 64 65 pSym :: Monad m => String -> ParseT Err m () 66 pSym s = pToken (string s) *> pure () 67 68 pAnyWord :: Monad m => ParseT Err m ByteString 69 pAnyWord = snd <$> pToken (bytesOf $ charIf isWordStart *> charWhile isWordCont) 70 71 pWord :: Monad m => ByteString -> ParseT Err m () 72 pWord w = do 73 w' <- pAnyWord 74 guard (w' == w) 75 76 pAnyIdent :: Monad m => ParseT Err m ByteString 77 pAnyIdent = do 78 x <- snd <$> pToken (bytesOf $ charIf isIdentStart *> charWhile isIdentCont) 79 guard $ not $ isReservedIdent x 80 pure x 81 82 pDelim :: Monad m => String -> ParseT Err m a -> String -> ParseT Err m a 83 pDelim l p r = pSym l *> (p <* pSym r) `cut` Err 84 85 pTop :: Monad m => ParseT Err m a -> ParseT Err m a 86 pTop p = pWs *> p <* eof `cut` Err 87 88 -------------------------------------------------------------------------------- 89 -- Kinds 90 91 pKind :: P q Kind 92 pKind = match pKind_atom [pKindArrow, pure] 93 94 pKind_atom :: P q Kind 95 pKind_atom = 96 choice [ 97 pSym "$%" *> pure KindQT, 98 pSym "$" *> pure KindQ, 99 pSym "%" *> pure KindT, 100 pDelim "(" pKind ")" 101 ] 102 103 pKindArrow :: Kind -> P q Kind 104 pKindArrow dom = pSym "->" *> (KindArrow dom <$> pKind) `cut` Err 105 106 -------------------------------------------------------------------------------- 107 -- Types 108 109 pTypeName :: P q TypeName 110 pTypeName = TypeName <$> pAnyIdent 111 112 pType :: P q (Type q) 113 pType = match pType_abs [pTypeAnnot, pure] 114 115 pType_abs :: P q (Type q) 116 pType_abs = pTypeArrowAbs <|> pType_arrow 117 118 pType_arrow :: P q (Type q) 119 pType_arrow = pTypeTForall <|> match pType_pair [pTypeTArrow, pure] 120 121 pType_pair :: P q (Type q) 122 pType_pair = match pType_add [pTypeQTPair, pure] 123 124 pType_add :: P q (Type q) 125 pType_add = chainl TypeQAdd pType_mul (pSym "+" *> pType_mul `cut` Err) 126 127 pType_mul :: P q (Type q) 128 pType_mul = chainl TypeQMul pType_app (pSym "*" *> pType_app `cut` Err) 129 130 pType_app :: P q (Type q) 131 pType_app = chainl TypeArrowApp pType_proj pType_proj 132 133 pType_proj :: P q (Type q) 134 pType_proj = chainl (&) pType_atom (pSym ".$" *> pure TypeQTFst 135 <|> pSym ".%" *> pure TypeQTSnd) 136 137 pType_atom :: P q (Type q) 138 pType_atom = TypeVar <$> pTypeName <|> pTypeQ <|> pDelim "(" pType ")" 139 140 pTypeAnnot :: Type q -> P q (Type q) 141 pTypeAnnot a = pSym ":" *> (TypeAnnot a <$> pKind) `cut` Err 142 143 pTypeArrowAbs :: P q (Type q) 144 pTypeArrowAbs = do 145 pSym "\\" 146 binders <- some (TypeArrowAbs <$> pTypeName) `cut` Err 147 pSym "=>" `cut` Err 148 body <- pType_abs `cut` Err 149 pure $ foldr1 (.) binders body 150 151 pTypeTArrow :: Type q -> P q (Type q) 152 pTypeTArrow dom = pSym "->" *> (TypeTArrow dom <$> pType_arrow) `cut` Err 153 154 pTypeTForall :: P q (Type q) 155 pTypeTForall = do 156 pSym "@" 157 x <- pTypeName `cut` Err 158 k <- branch (pSym ":") (pKind_atom `cut` Err) (pure KindQT) 159 pSym "->" `cut` Err 160 body <- pType_arrow `cut` Err 161 pure $ TypeTForall x k body 162 163 pTypeQ :: P q (Type q) 164 pTypeQ = mapParseT (pure . runIdentity) . fmap TypeQ =<< ask 165 166 pTypeQTPair :: Type q -> P q (Type q) 167 pTypeQTPair q = pSym "!" *> (TypeQTPair q <$> pType_add) `cut` Err 168 169 -------------------------------------------------------------------------------- 170 -- Terms 171 172 pTermName :: P q TermName 173 pTermName = TermName <$> pAnyIdent 174 175 pTerm :: P q (Term q) 176 pTerm = pTermLet <|> match pTerm_abs [pTermAnnot, pure] 177 178 pTerm_abs :: P q (Term q) 179 pTerm_abs = pTermAbs <|> pTerm_app 180 181 pTerm_app :: P q (Term q) 182 pTerm_app = chainl (&) pTerm_atom (flip TermArrowApp <$> pTerm_atom 183 <|> flip TermForallApp <$> pDelim "[" pType "]") 184 185 pTerm_atom :: P q (Term q) 186 pTerm_atom = TermVar <$> pTermName <|> pDelim "(" pTerm ")" 187 188 pTermAnnot :: Term q -> P q (Term q) 189 pTermAnnot t = pSym ":" *> (TermAnnot t <$> pType) `cut` Err 190 191 pTermLet :: P q (Term q) 192 pTermLet = do 193 pWord "let" 194 x <- pTermName `cut` Err 195 pSym ":" `cut` Err 196 qa <- pType `cut` Err 197 pSym "=" `cut` Err 198 arg <- pTerm `cut` Err 199 pSym ";" `cut` Err 200 body <- pTerm `cut` Err 201 pure $ TermLet x arg qa body 202 203 pTermAbs :: P q (Term q) 204 pTermAbs = do 205 pSym "\\" 206 binders <- some (TermArrowAbs <$> pTermName 207 <|> TermForallAbs <$> pDelim "[" pTypeName "]") `cut` Err 208 pSym "=>" `cut` Err 209 body <- pTerm_abs `cut` Err 210 pure $ foldr1 (.) binders body