diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler/Lexer.hs | 15 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 16 |
2 files changed, 18 insertions, 13 deletions
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs index c47ba1ce..fe3015a6 100644 --- a/src/LambdaCube/Compiler/Lexer.hs +++ b/src/LambdaCube/Compiler/Lexer.hs | |||
@@ -141,7 +141,16 @@ lexemeWithoutSpace p = do | |||
141 | 141 | ||
142 | -- TODO?: eliminate; when eliminated, the SPos in parser state can be eliminated too | 142 | -- TODO?: eliminate; when eliminated, the SPos in parser state can be eliminated too |
143 | appRange :: Parse r w (SI -> a) -> Parse r w a | 143 | appRange :: Parse r w (SI -> a) -> Parse r w a |
144 | appRange p = (\fi p1 a p2 -> a $ RangeSI $ Range fi p1 p2) <$> asks fileInfo <*> getSPos <*> p <*> get | 144 | appRange p = (\fi p1 a p2 -> a $ RangeSI $ Range fi p1 p2) <$> asks fileInfo <*> getSPos <*> p <*> getLexemeEnd |
145 | |||
146 | getLexemeEnd = get | ||
147 | |||
148 | noSpaceBefore p = try $ do | ||
149 | pos <- getLexemeEnd | ||
150 | x <- p | ||
151 | guard $ case sourceInfo x of | ||
152 | RangeSI (Range _ pos' _) -> pos == pos' | ||
153 | return x | ||
145 | 154 | ||
146 | lexeme_ p = lexemeWithoutSpace p <* whiteSpace | 155 | lexeme_ p = lexemeWithoutSpace p <* whiteSpace |
147 | 156 | ||
@@ -224,9 +233,9 @@ upperLower = lowerCase <|> upperCase_ <|> parens symbols | |||
224 | 233 | ||
225 | ----------------------------------------------------------- operators and identifiers | 234 | ----------------------------------------------------------- operators and identifiers |
226 | 235 | ||
227 | reservedOp name = lexeme $ try $ string name *> notFollowedBy opLetter | 236 | reservedOp name = fst <$> lexeme_ (try $ string name *> notFollowedBy opLetter) |
228 | 237 | ||
229 | reserved name = lexeme $ try $ string name *> notFollowedBy identLetter | 238 | reserved name = fst <$> lexeme_ (try $ string name *> notFollowedBy identLetter) |
230 | 239 | ||
231 | expect msg p i = i >>= \n -> if p n then unexpected (msg ++ " " ++ show n) else return n | 240 | expect msg p i = i >>= \n -> if p n then unexpected (msg ++ " " ++ show n) else return n |
232 | 241 | ||
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index 1d5139b8..79975251 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -172,8 +172,7 @@ parseTermLam = | |||
172 | <|> mkIf <$ reserved "if" <*> setR parseTermLam | 172 | <|> mkIf <$ reserved "if" <*> setR parseTermLam |
173 | <* reserved "then" <*> setR parseTermLam | 173 | <* reserved "then" <*> setR parseTermLam |
174 | <* reserved "else" <*> setR parseTermLam | 174 | <* reserved "else" <*> setR parseTermLam |
175 | <|> do reserved "forall" | 175 | <|> do (fe, ts) <- reserved "forall" *> telescope (Just $ Wildcard SType) |
176 | (fe, ts) <- telescope $ Just $ Wildcard SType | ||
177 | f <- SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->" | 176 | f <- SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->" |
178 | t' <- deBruijnify fe <$> setR parseTermLam | 177 | t' <- deBruijnify fe <$> setR parseTermLam |
179 | return $ foldr (uncurry f) t' ts | 178 | return $ foldr (uncurry f) t' ts |
@@ -329,7 +328,7 @@ parsePatApp = | |||
329 | PConSimp <$> addConsInfo upperCase_ <*> many (setR parsePatAt) | 328 | PConSimp <$> addConsInfo upperCase_ <*> many (setR parsePatAt) |
330 | <|> parsePatAt | 329 | <|> parsePatAt |
331 | 330 | ||
332 | parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (reservedOp "@") | 331 | parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (noSpaceBefore $ reservedOp "@") |
333 | where | 332 | where |
334 | concatParPats ps = ParPat $ concat [p | ParPat p <- ps] | 333 | concatParPats ps = ParPat $ concat [p | ParPat p <- ps] |
335 | 334 | ||
@@ -373,7 +372,7 @@ parsePatAtom = | |||
373 | longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id) | 372 | longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id) |
374 | 373 | ||
375 | telescopePat = do | 374 | telescopePat = do |
376 | (a, b) <- fmap (reverse . foldMap (getPVars . snd) &&& id) $ many $ uncurry f <$> hiddenTerm (setR parsePatAtom) (setR parsePatAtom) | 375 | (a, b) <- fmap (reverse . foldMap (getPVars . snd) &&& id) $ many $ uncurry f <$> hiddenTerm (setR parsePatAt) (setR parsePatAt) |
377 | checkPattern a | 376 | checkPattern a |
378 | return (a, b) | 377 | return (a, b) |
379 | where | 378 | where |
@@ -468,8 +467,7 @@ parseRHS :: String -> BodyParser GuardTrees | |||
468 | parseRHS tok = do | 467 | parseRHS tok = do |
469 | mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs) | 468 | mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs) |
470 | <|> do | 469 | <|> do |
471 | reservedOp tok | 470 | rhs <- reservedOp tok *> setR parseTermLam |
472 | rhs <- setR parseTermLam | ||
473 | f <- option id $ mkLets <$ reserved "where" <*> parseDefs | 471 | f <- option id $ mkLets <$ reserved "where" <*> parseDefs |
474 | noGuards <$> trackSI (pure $ f rhs) | 472 | noGuards <$> trackSI (pure $ f rhs) |
475 | where | 473 | where |
@@ -493,8 +491,7 @@ funAltDef parseOpName parseName = do | |||
493 | Just opName -> try_ "operator definition" $ do | 491 | Just opName -> try_ "operator definition" $ do |
494 | (e', a1) <- longPattern | 492 | (e', a1) <- longPattern |
495 | n <- opName | 493 | n <- opName |
496 | (e'', a2) <- longPattern | 494 | (e'', a2) <- longPattern <* lookAhead (reservedOp "=" <|> reservedOp "|") |
497 | lookAhead $ reservedOp "=" <|> reservedOp "|" | ||
498 | let fee = e'' <> e' | 495 | let fee = e'' <> e' |
499 | checkPattern fee | 496 | checkPattern fee |
500 | return (n, (fee, (,) (Visible, Wildcard SType) <$> [a1, deBruijnify e' a2])) | 497 | return (n, (fee, (,) (Visible, Wildcard SType) <$> [a1, deBruijnify e' a2])) |
@@ -539,8 +536,7 @@ parseModule = do | |||
539 | whiteSpace | 536 | whiteSpace |
540 | header <- optional $ do | 537 | header <- optional $ do |
541 | modn <- reserved "module" *> moduleName | 538 | modn <- reserved "module" *> moduleName |
542 | exps <- optional (parens $ commaSep parseExport) | 539 | exps <- optional (parens $ commaSep parseExport) <* reserved "where" |
543 | reserved "where" | ||
544 | return (modn, exps) | 540 | return (modn, exps) |
545 | let mkIDef _ n i h _ = (n, f i h) | 541 | let mkIDef _ n i h _ = (n, f i h) |
546 | where | 542 | where |