diff options
Diffstat (limited to 'src/LambdaCube/Compiler/Infer.hs')
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 408 |
1 files changed, 196 insertions, 212 deletions
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 2fbeec92..f0e2e9de 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -38,11 +38,12 @@ import Control.Monad.Writer | |||
38 | import Control.Monad.State | 38 | import Control.Monad.State |
39 | import Control.Monad.Identity | 39 | import Control.Monad.Identity |
40 | import Control.Arrow hiding ((<+>)) | 40 | import Control.Arrow hiding ((<+>)) |
41 | import Control.Applicative hiding (optional) | 41 | import Control.Applicative |
42 | import Control.Exception hiding (try) | 42 | import Control.Exception hiding (try) |
43 | 43 | ||
44 | import Text.Parsec hiding (label, Empty, State, (<|>), many, optional) | 44 | import Text.Parsec hiding (label, Empty, State, (<|>), many) |
45 | import qualified Text.Parsec.Token as Pa | 45 | import qualified Text.Parsec.Token as Pa |
46 | import qualified Text.ParserCombinators.Parsec.Language as Pa | ||
46 | import Text.Parsec.Pos | 47 | import Text.Parsec.Pos |
47 | import Text.Parsec.Indentation hiding (Any) | 48 | import Text.Parsec.Indentation hiding (Any) |
48 | import Text.Parsec.Indentation.Char | 49 | import Text.Parsec.Indentation.Char |
@@ -53,6 +54,11 @@ import qualified LambdaCube.Compiler.Pretty as P | |||
53 | import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) | 54 | import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) |
54 | import LambdaCube.Compiler.Token | 55 | import LambdaCube.Compiler.Token |
55 | 56 | ||
57 | -------------------------------------------------------------------------------- utils | ||
58 | |||
59 | (<&>) = flip (<$>) | ||
60 | |||
61 | |||
56 | -------------------------------------------------------------------------------- source data | 62 | -------------------------------------------------------------------------------- source data |
57 | 63 | ||
58 | type SName = String | 64 | type SName = String |
@@ -197,7 +203,7 @@ data Exp | |||
197 | | Con ConName [Exp] | 203 | | Con ConName [Exp] |
198 | | TyCon TyConName [Exp] | 204 | | TyCon TyConName [Exp] |
199 | | ELit Lit | 205 | | ELit Lit |
200 | | Assign !Int Exp Exp -- De Bruijn index decreasing assign operator, only for metavariables (non-recursive) -- TODO: remove | 206 | | Assign !Int Exp Exp -- De Bruijn index decreasing assign reservedOp, only for metavariables (non-recursive) -- TODO: remove |
201 | | Label LabelKind Exp{-function alternatives are obeyed during reduction-} Exp{-functions are treated like constants-} | 207 | | Label LabelKind Exp{-function alternatives are obeyed during reduction-} Exp{-functions are treated like constants-} |
202 | -- label is used also for getting fixity info | 208 | -- label is used also for getting fixity info |
203 | | LabelEnd Exp | 209 | | LabelEnd Exp |
@@ -1356,73 +1362,75 @@ removeHiddenUnit (Pi Hidden Unit (downE 0 -> Just t)) = removeHiddenUnit t | |||
1356 | removeHiddenUnit (Pi h a b) = Pi h a $ removeHiddenUnit b | 1362 | removeHiddenUnit (Pi h a b) = Pi h a $ removeHiddenUnit b |
1357 | removeHiddenUnit t = t | 1363 | removeHiddenUnit t = t |
1358 | 1364 | ||
1359 | -------------------------------------------------------------------------------- parser | 1365 | --------------------------------------------------------------------------------------- |
1366 | -------------------------------------- parser ----------------------------------------- | ||
1360 | 1367 | ||
1361 | addForalls :: Extensions -> [SName] -> SExp -> SExp | 1368 | -- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602 |
1362 | addForalls exs defined x = foldl f x [v | v@(vh:_) <- reverse $ freeS x, v `notElem'` defined, isLower vh || NoConstructorNamespace `elem` exs] | 1369 | try' s m = try m <?> s |
1363 | where | ||
1364 | f e v = SPi Hidden (Wildcard SType) $ substSG0 v e | ||
1365 | 1370 | ||
1366 | defined defs = ("'Type":) $ flip foldMap defs $ \case | 1371 | check msg p m = try' msg $ mfilter p m |
1367 | TypeAnn (_, x) _ -> [x] | 1372 | |
1368 | Let (_, x) _ _ _ _ -> [x] | 1373 | -------------------------------------------------------------------------------- parser type |
1369 | Data (_, x) _ _ _ cs -> x: map (snd . fst) cs | ||
1370 | Class (_, x) _ cs -> x: map (snd . fst) cs | ||
1371 | TypeFamily (_, x) _ _ -> [x] | ||
1372 | x -> error $ unwords ["defined: Impossible", show x, "cann't be here"] | ||
1373 | 1374 | ||
1374 | type InnerP = Reader GlobalEnv' | 1375 | type P = ParsecT (IndentStream (CharIndentStream String)) SourcePos (Reader GlobalEnv') |
1375 | 1376 | ||
1376 | type P = ParsecT (IndentStream (CharIndentStream String)) SourcePos InnerP | ||
1377 | 1377 | ||
1378 | lexer :: Pa.GenTokenParser (IndentStream (CharIndentStream String)) SourcePos InnerP | 1378 | -------------------------------------------------------------------------------- lexing |
1379 | |||
1380 | lexer :: Pa.GenTokenParser (IndentStream (CharIndentStream String)) SourcePos (Reader GlobalEnv') | ||
1379 | lexer = makeTokenParser lexeme $ makeIndentLanguageDef style | 1381 | lexer = makeTokenParser lexeme $ makeIndentLanguageDef style |
1380 | where | 1382 | where |
1381 | lexeme p | 1383 | lexeme p = p <* (getPosition >>= setState >> whiteSpace) |
1382 | = do{ x <- p; getPosition >>= setState; whiteSpace; return x } | ||
1383 | 1384 | ||
1384 | style = Pa.LanguageDef | 1385 | style = Pa.LanguageDef |
1385 | { Pa.commentStart = "{-" | 1386 | { Pa.commentStart = Pa.commentStart Pa.haskellDef |
1386 | , Pa.commentEnd = "-}" | 1387 | , Pa.commentEnd = Pa.commentEnd Pa.haskellDef |
1387 | , Pa.commentLine = "--" | 1388 | , Pa.commentLine = Pa.commentLine Pa.haskellDef |
1388 | , Pa.nestedComments = True | 1389 | , Pa.nestedComments = Pa.nestedComments Pa.haskellDef |
1389 | , Pa.identStart = letter <|> oneOf "_" | 1390 | , Pa.identStart = letter <|> char '_' -- '_' is included also |
1390 | , Pa.identLetter = alphaNum <|> oneOf "_'" | 1391 | , Pa.identLetter = alphaNum <|> oneOf "_'#" |
1391 | , Pa.opStart = Pa.opLetter style | 1392 | , Pa.opStart = Pa.opLetter style |
1392 | , Pa.opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~" | 1393 | , Pa.opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~" |
1393 | , Pa.reservedOpNames= ["->", "=>", "~", "\\", "|", "::", "<-", "=", "@", ".."] | 1394 | , Pa.reservedOpNames = Pa.reservedOpNames Pa.haskellDef |
1394 | , Pa.reservedNames = | 1395 | , Pa.reservedNames = Pa.reservedNames Pa.haskellDef |
1395 | [ "case", "class", "data", "type", | 1396 | , Pa.caseSensitive = Pa.caseSensitive Pa.haskellDef |
1396 | "else", "forall", "if", "import", "infix", "in", "infixl", "infixr", | ||
1397 | "instance", "let", "module", "of", "then", "qualified", | ||
1398 | "where", "_" | ||
1399 | ] | ||
1400 | , Pa.caseSensitive = True | ||
1401 | } | 1397 | } |
1402 | 1398 | ||
1403 | position :: P SourcePos | 1399 | parens = Pa.parens lexer |
1404 | position = getPosition | 1400 | braces = Pa.braces lexer |
1405 | 1401 | brackets = Pa.brackets lexer | |
1406 | positionBeforeSpace :: P SourcePos | 1402 | commaSep = Pa.commaSep lexer |
1407 | positionBeforeSpace = getState | 1403 | commaSep1 = Pa.commaSep1 lexer |
1404 | dot = Pa.dot lexer | ||
1405 | comma = Pa.comma lexer | ||
1406 | colon = Pa.colon lexer | ||
1407 | natural = Pa.natural lexer | ||
1408 | integer = Pa.integer lexer | ||
1409 | float = Pa.float lexer | ||
1410 | charLiteral = Pa.charLiteral lexer | ||
1411 | stringLiteral = Pa.stringLiteral lexer | ||
1412 | whiteSpace = Pa.whiteSpace lexer | ||
1413 | operator = Pa.operator lexer | ||
1414 | reserved = Pa.reserved lexer | ||
1415 | reservedOp = Pa.reservedOp lexer | ||
1416 | identifier = Pa.identifier lexer | ||
1417 | |||
1418 | appRange :: P (SI -> a) -> P a | ||
1419 | appRange p = (\p1 a p2 -> a (Range (p1,p2))) <$> getPosition <*> p <*> getState | ||
1408 | 1420 | ||
1409 | optional :: P a -> P (Maybe a) | 1421 | withRange :: (SI -> a -> b) -> P a -> P b |
1410 | optional = optionMaybe | 1422 | withRange f p = appRange $ flip f <$> p |
1411 | 1423 | ||
1412 | keyword :: String -> P () | 1424 | infix 9 `withRange` |
1413 | keyword = Pa.reserved lexer | ||
1414 | 1425 | ||
1415 | operator :: String -> P () | 1426 | -------------------------------------------------------------------------------- namespace handling |
1416 | operator = Pa.reservedOp lexer | ||
1417 | 1427 | ||
1418 | data Level | 1428 | data Level |
1419 | = TypeLevel | 1429 | = TypeLevel |
1420 | | ExpLevel | 1430 | | ExpLevel |
1421 | deriving (Eq, Show) | 1431 | deriving (Eq, Show) |
1422 | 1432 | ||
1423 | levelElim | 1433 | levelElim typeLevel expLevel = \case |
1424 | typeLevel | ||
1425 | expLevel = \case | ||
1426 | TypeLevel -> typeLevel | 1434 | TypeLevel -> typeLevel |
1427 | ExpLevel -> expLevel | 1435 | ExpLevel -> expLevel |
1428 | 1436 | ||
@@ -1453,58 +1461,28 @@ tick _ n = n | |||
1453 | 1461 | ||
1454 | tick' = tick . fromMaybe ExpLevel . namespaceLevel | 1462 | tick' = tick . fromMaybe ExpLevel . namespaceLevel |
1455 | 1463 | ||
1456 | ident = Pa.identifier lexer | 1464 | tickIdent ns = tick' ns <$> identifier |
1457 | tickIdent ns = tick' ns <$> ident | ||
1458 | |||
1459 | lcOps = Pa.operator lexer | ||
1460 | |||
1461 | parens = Pa.parens lexer | ||
1462 | braces = Pa.braces lexer | ||
1463 | brackets = Pa.brackets lexer | ||
1464 | commaSep = Pa.commaSep lexer | ||
1465 | commaSep1 = Pa.commaSep1 lexer | ||
1466 | dot = Pa.dot lexer | ||
1467 | comma = Pa.comma lexer | ||
1468 | colon = Pa.colon lexer | ||
1469 | natural = Pa.natural lexer | ||
1470 | integer = Pa.integer lexer | ||
1471 | float = Pa.float lexer | ||
1472 | charLiteral = Pa.charLiteral lexer | ||
1473 | stringLiteral = Pa.stringLiteral lexer | ||
1474 | whiteSpace = Pa.whiteSpace lexer | ||
1475 | |||
1476 | data Extension | ||
1477 | = NoImplicitPrelude | ||
1478 | | NoTypeNamespace | ||
1479 | | NoConstructorNamespace | ||
1480 | | TraceTypeCheck | ||
1481 | deriving (Enum, Eq, Ord, Show) | ||
1482 | |||
1483 | type Name = String | ||
1484 | type DefinitionR = Stmt | ||
1485 | |||
1486 | data Export = ExportModule Name | ExportId Name | ||
1487 | type Extensions = [Extension] | ||
1488 | 1465 | ||
1489 | data ImportItems | 1466 | -------------------------------------------------------------------------------- identifiers |
1490 | = ImportAllBut [Name] | ||
1491 | | ImportJust [Name] | ||
1492 | |||
1493 | data ModuleR | ||
1494 | = Module | ||
1495 | { extensions :: Extensions | ||
1496 | , moduleImports :: [(Name, ImportItems)] -- TODO | ||
1497 | , moduleExports :: Maybe [Export] | ||
1498 | , definitions :: GlobalEnv' -> Either String [DefinitionR] | ||
1499 | , sourceCode :: String | ||
1500 | } | ||
1501 | 1467 | ||
1502 | (<&>) = flip (<$>) | 1468 | --upperCase, lowerCase, symbols, colonSymbols :: P String |
1469 | upperCase NonTypeNamespace = mzero -- todo | ||
1470 | upperCase ns = (if caseSensitiveNS ns then check "uppercase ident" (isUpper . head') else id) $ tickIdent ns | ||
1471 | lowerCase ns = (if caseSensitiveNS ns then check "lowercase ident" (isLower . head') else id) identifier <|> try (('_':) <$ char '_' <*> identifier) | ||
1472 | symbols = check "symbols" ((/=':') . head) operator | ||
1473 | colonSymbols = "Cons" <$ reservedOp ":" <|> check "symbols" ((==':') . head) operator | ||
1503 | 1474 | ||
1504 | -------------------------------------------------------------------------------- parser combinators | 1475 | var ns = lowerCase ns |
1476 | patVar ns = lowerCase ns <|> "" <$ reserved "_" | ||
1477 | qIdent ns = {-qualified_ todo-} (var ns <|> upperCase ns) | ||
1478 | conOperator = colonSymbols | ||
1479 | varId ns = var ns <|> parens operatorT | ||
1480 | backquotedIdent = try' "backquoted" $ char '`' *> ((:) <$> satisfy isAlpha <*> many (satisfy isAlphaNum)) <* char '`' <* whiteSpace | ||
1481 | operatorT = symbols | ||
1482 | <|> conOperator | ||
1483 | <|> backquotedIdent | ||
1484 | moduleName = {-qualified_ todo-} upperCase (Namespace ExpLevel True) | ||
1505 | 1485 | ||
1506 | -- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602 | ||
1507 | try' s m = try m <?> s | ||
1508 | {- | 1486 | {- |
1509 | qualified_ id = do | 1487 | qualified_ id = do |
1510 | q <- try' "qualification" $ upperCase' <* dot | 1488 | q <- try' "qualification" $ upperCase' <* dot |
@@ -1516,60 +1494,49 @@ qualified_ id = do | |||
1516 | upperCase' = (:) <$> satisfy isUpper <*> many (satisfy isAlphaNum) | 1494 | upperCase' = (:) <$> satisfy isUpper <*> many (satisfy isAlphaNum) |
1517 | -} | 1495 | -} |
1518 | 1496 | ||
1519 | optionTry p = optionMaybe (try p) | ||
1520 | |||
1521 | -------------------------------------------------------------------------------- identifiers | ||
1522 | |||
1523 | check msg p m = try' msg $ do | ||
1524 | x <- m | ||
1525 | if p x then return x else fail $ msg ++ " expected" | ||
1526 | |||
1527 | head' ('\'': c: _) = c | 1497 | head' ('\'': c: _) = c |
1528 | head' (c: _) = c | 1498 | head' (c: _) = c |
1529 | 1499 | ||
1530 | --upperCase, lowerCase, symbols, colonSymbols :: P String | ||
1531 | upperCase NonTypeNamespace = mzero -- todo | ||
1532 | upperCase ns = (if caseSensitiveNS ns then check "uppercase ident" (isUpper . head') else id) $ tickIdent ns | ||
1533 | lowerCase ns = (if caseSensitiveNS ns then check "lowercase ident" (isLower . head') else id) ident <|> try (('_':) <$ char '_' <*> ident) | ||
1534 | symbols = check "symbols" ((/=':') . head) lcOps | ||
1535 | colonSymbols = "Cons" <$ operator ":" <|> check "symbols" ((==':') . head) lcOps | ||
1536 | |||
1537 | -------------------------------------------------------------------------------- | ||
1538 | |||
1539 | pattern ExpN' :: String -> P.Doc -> String | ||
1540 | pattern ExpN' s p <- ((,) undefined -> (p, s)) where ExpN' s p = s | ||
1541 | pattern ExpN s = s | ||
1542 | |||
1543 | var ns = lowerCase ns | ||
1544 | patVar ns = lowerCase ns <|> "" <$ keyword "_" | ||
1545 | qIdent ns = {-qualified_ todo-} (var ns <|> upperCase ns) | ||
1546 | conOperator = colonSymbols | ||
1547 | varId ns = var ns <|> parens operator' | ||
1548 | backquotedIdent = try' "backquoted" $ char '`' *> (ExpN <$> ((:) <$> satisfy isAlpha <*> many (satisfy isAlphaNum))) <* char '`' <* whiteSpace | ||
1549 | operator' = symbols | ||
1550 | <|> conOperator | ||
1551 | <|> backquotedIdent | ||
1552 | moduleName = {-qualified_ todo-} upperCase (Namespace ExpLevel True) | ||
1553 | |||
1554 | -------------------------------------------------------------------------------- fixity declarations | 1500 | -------------------------------------------------------------------------------- fixity declarations |
1555 | 1501 | ||
1556 | fixityDef :: P [DefinitionR] | 1502 | fixityDef :: P [Stmt] |
1557 | fixityDef = do | 1503 | fixityDef = do |
1558 | dir <- Infix <$ keyword "infix" | 1504 | dir <- Infix <$ reserved "infix" |
1559 | <|> InfixL <$ keyword "infixl" | 1505 | <|> InfixL <$ reserved "infixl" |
1560 | <|> InfixR <$ keyword "infixr" | 1506 | <|> InfixR <$ reserved "infixr" |
1561 | localIndentation Gt $ do | 1507 | localIndentation Gt $ do |
1562 | i <- fromIntegral <$> natural | 1508 | i <- fromIntegral <$> natural |
1563 | ns <- commaSep1 (siName operator') | 1509 | ns <- commaSep1 (siName operatorT) |
1564 | return $ PrecDef <$> ns <*> pure (dir, i) | 1510 | return $ PrecDef <$> ns <*> pure (dir, i) |
1565 | 1511 | ||
1566 | -------------------------------------------------------------------------------- | 1512 | -------------------------------------------------------------------------------- export |
1513 | |||
1514 | data Export = ExportModule SName | ExportId SName | ||
1567 | 1515 | ||
1568 | export :: Namespace -> P Export | 1516 | parseExport :: Namespace -> P Export |
1569 | export ns = | 1517 | parseExport ns = |
1570 | ExportModule <$ keyword "module" <*> moduleName | 1518 | ExportModule <$ reserved "module" <*> moduleName |
1571 | <|> ExportId <$> varId ns | 1519 | <|> ExportId <$> varId ns |
1572 | 1520 | ||
1521 | -------------------------------------------------------------------------------- import | ||
1522 | |||
1523 | data ImportItems | ||
1524 | = ImportAllBut [SName] | ||
1525 | | ImportJust [SName] | ||
1526 | |||
1527 | importlist ns = parens (commaSep (varId ns <|> upperCase ns)) | ||
1528 | |||
1529 | -------------------------------------------------------------------------------- extensions | ||
1530 | |||
1531 | type Extensions = [Extension] | ||
1532 | |||
1533 | data Extension | ||
1534 | = NoImplicitPrelude | ||
1535 | | NoTypeNamespace | ||
1536 | | NoConstructorNamespace | ||
1537 | | TraceTypeCheck | ||
1538 | deriving (Enum, Eq, Ord, Show) | ||
1539 | |||
1573 | parseExtensions :: P [Extension] | 1540 | parseExtensions :: P [Extension] |
1574 | parseExtensions | 1541 | parseExtensions |
1575 | = try (string "{-#") *> simpleSpace *> string "LANGUAGE" *> simpleSpace *> commaSep ext <* simpleSpace <* string "#-}" <* simpleSpace | 1542 | = try (string "{-#") *> simpleSpace *> string "LANGUAGE" *> simpleSpace *> commaSep ext <* simpleSpace <* string "#-}" <* simpleSpace |
@@ -1584,7 +1551,16 @@ parseExtensions | |||
1584 | (fail $ "language extension expected instead of " ++ s) | 1551 | (fail $ "language extension expected instead of " ++ s) |
1585 | (Map.lookup s extensionMap) | 1552 | (Map.lookup s extensionMap) |
1586 | 1553 | ||
1587 | importlist ns = parens (commaSep (varId ns <|> upperCase ns)) | 1554 | -------------------------------------------------------------------------------- modules |
1555 | |||
1556 | data ModuleR | ||
1557 | = Module | ||
1558 | { extensions :: Extensions | ||
1559 | , moduleImports :: [(SName, ImportItems)] | ||
1560 | , moduleExports :: Maybe [Export] | ||
1561 | , definitions :: GlobalEnv' -> Either String [Stmt] | ||
1562 | , sourceCode :: String | ||
1563 | } | ||
1588 | 1564 | ||
1589 | parseLC :: MonadError ErrorMsg m => FilePath -> String -> m ModuleR | 1565 | parseLC :: MonadError ErrorMsg m => FilePath -> String -> m ModuleR |
1590 | parseLC f str = either (throwError . ErrorMsg . show) return . flip runReader (error "globalenv used") . runParserT p (newPos "" 0 0) f . mkIndentStream 0 infIndentation True Ge . mkCharIndentStream $ str | 1566 | parseLC f str = either (throwError . ErrorMsg . show) return . flip runReader (error "globalenv used") . runParserT p (newPos "" 0 0) f . mkIndentStream 0 infIndentation True Ge . mkCharIndentStream $ str |
@@ -1597,10 +1573,10 @@ parseLC f str = either (throwError . ErrorMsg . show) return . flip runReader (e | |||
1597 | then NonTypeNamespace | 1573 | then NonTypeNamespace |
1598 | else Namespace ExpLevel (not $ NoConstructorNamespace `elem` exts) | 1574 | else Namespace ExpLevel (not $ NoConstructorNamespace `elem` exts) |
1599 | whiteSpace | 1575 | whiteSpace |
1600 | header <- optional $ do | 1576 | header <- optionMaybe $ do |
1601 | modn <- keyword "module" *> moduleName | 1577 | modn <- reserved "module" *> moduleName |
1602 | exps <- optional (parens $ commaSep $ export ns) | 1578 | exps <- optionMaybe (parens $ commaSep $ parseExport ns) |
1603 | keyword "where" | 1579 | reserved "where" |
1604 | return (modn, exps) | 1580 | return (modn, exps) |
1605 | let mkIDef _ n i h _ = (n, f i h) | 1581 | let mkIDef _ n i h _ = (n, f i h) |
1606 | where | 1582 | where |
@@ -1608,11 +1584,11 @@ parseLC f str = either (throwError . ErrorMsg . show) return . flip runReader (e | |||
1608 | f (Just h) Nothing = ImportAllBut h | 1584 | f (Just h) Nothing = ImportAllBut h |
1609 | f Nothing (Just i) = ImportJust i | 1585 | f Nothing (Just i) = ImportJust i |
1610 | idefs <- many $ | 1586 | idefs <- many $ |
1611 | mkIDef <$> (keyword "import" *> (optionTry $ keyword "qualified")) | 1587 | mkIDef <$> (reserved "import" *> (optionMaybe $ try $ reserved "qualified")) |
1612 | <*> moduleName | 1588 | <*> moduleName |
1613 | <*> (optionTry $ keyword "hiding" *> importlist ns) | 1589 | <*> (optionMaybe $ try $ reserved "hiding" *> importlist ns) |
1614 | <*> (optionTry $ importlist ns) | 1590 | <*> (optionMaybe $ try $ importlist ns) |
1615 | <*> (optionTry $ keyword "as" *> moduleName) | 1591 | <*> (optionMaybe $ try $ reserved "as" *> moduleName) |
1616 | st <- getParserState | 1592 | st <- getParserState |
1617 | 1593 | ||
1618 | let defs ge = (show +++ id) . flip runReader ge . runParserT p (newPos "" 0 0) f . mkIndentStream 0 infIndentation True Ge . mkCharIndentStream $ "" | 1594 | let defs ge = (show +++ id) . flip runReader ge . runParserT p (newPos "" 0 0) f . mkIndentStream 0 infIndentation True Ge . mkCharIndentStream $ "" |
@@ -1630,7 +1606,9 @@ parseLC f str = either (throwError . ErrorMsg . show) return . flip runReader (e | |||
1630 | , sourceCode = str | 1606 | , sourceCode = str |
1631 | } | 1607 | } |
1632 | 1608 | ||
1633 | parseType ns mb vs = maybe id option mb $ operator "::" *> parseTTerm ns PrecLam vs | 1609 | -------------------------------------------------------------------------------- |
1610 | |||
1611 | parseType ns mb vs = maybe id option mb $ reservedOp "::" *> parseTTerm ns PrecLam vs | ||
1634 | typedIds ns mb vs = (,) <$> commaSep1 (siName (varId ns <|> patVar ns <|> upperCase ns)) | 1612 | typedIds ns mb vs = (,) <$> commaSep1 (siName (varId ns <|> patVar ns <|> upperCase ns)) |
1635 | <*> localIndentation Gt {-TODO-} (parseType ns mb vs) | 1613 | <*> localIndentation Gt {-TODO-} (parseType ns mb vs) |
1636 | 1614 | ||
@@ -1642,7 +1620,7 @@ telescope ns mb vs = (map removeSI *** id) <$> telescopeSI ns mb (map addSI vs) | |||
1642 | telescopeSI :: Namespace -> Maybe SExp -> [SIName] -> P ([SIName], [(Visibility, SExp)]) -- todo: refactor to [(SIName, (Visibility, SExp))] | 1620 | telescopeSI :: Namespace -> Maybe SExp -> [SIName] -> P ([SIName], [(Visibility, SExp)]) -- todo: refactor to [(SIName, (Visibility, SExp))] |
1643 | telescopeSI ns mb vs = option (vs, []) $ do | 1621 | telescopeSI ns mb vs = option (vs, []) $ do |
1644 | (si, (x, vt)) <- withSI | 1622 | (si, (x, vt)) <- withSI |
1645 | ( operator "@" *> (maybe empty (\x -> flip (,) (Hidden, x) <$> patVar ns) mb <|> parens (typedId Hidden)) | 1623 | ( reservedOp "@" *> (maybe empty (\x -> flip (,) (Hidden, x) <$> patVar ns) mb <|> parens (typedId Hidden)) |
1646 | <|> try (parens $ typedId Visible) | 1624 | <|> try (parens $ typedId Visible) |
1647 | <|> maybe ((,) "" . (,) Visible <$> parseTerm ns PrecAtom (map removeSI vs)) | 1625 | <|> maybe ((,) "" . (,) Visible <$> parseTerm ns PrecAtom (map removeSI vs)) |
1648 | (\x -> flip (,) (Visible, x) <$> patVar ns) | 1626 | (\x -> flip (,) (Visible, x) <$> patVar ns) |
@@ -1658,7 +1636,7 @@ telescopeSI ns mb vs = option (vs, []) $ do | |||
1658 | parseClause ns e = do | 1636 | parseClause ns e = do |
1659 | (fe, p) <- pattern' ns e | 1637 | (fe, p) <- pattern' ns e |
1660 | localIndentation Gt $ do | 1638 | localIndentation Gt $ do |
1661 | x <- operator "->" *> parseETerm ns PrecLam fe | 1639 | x <- reservedOp "->" *> parseETerm ns PrecLam fe |
1662 | f <- parseWhereBlock ns fe | 1640 | f <- parseWhereBlock ns fe |
1663 | return (p, f x) | 1641 | return (p, f x) |
1664 | 1642 | ||
@@ -1692,7 +1670,7 @@ mkTupPat ns ps = PCon (debugSI "", tick' ns $ "Tuple" ++ show (length ps)) (ParP | |||
1692 | pattern' ns vs = | 1670 | pattern' ns vs = |
1693 | pCon <$> (siName $ upperCase ns) <*> patterns ns vs | 1671 | pCon <$> (siName $ upperCase ns) <*> patterns ns vs |
1694 | <|> pCon <$> try (withSI (char '\'' *> upperCase (switchNS ns))) <*> patterns ns vs | 1672 | <|> pCon <$> try (withSI (char '\'' *> upperCase (switchNS ns))) <*> patterns ns vs |
1695 | <|> (patternAtom ns vs >>= \(vs, p) -> option (vs, p) ((id *** (\p' -> PCon (debugSI "pattern'","Cons") (ParPat . (:[]) <$> [p, p']))) <$ operator ":" <*> pattern' ns vs)) | 1673 | <|> (patternAtom ns vs >>= \(vs, p) -> option (vs, p) ((id *** (\p' -> PCon (debugSI "pattern'","Cons") (ParPat . (:[]) <$> [p, p']))) <$ reservedOp ":" <*> pattern' ns vs)) |
1696 | 1674 | ||
1697 | pCon i (vs, x) = (vs, PCon i x) | 1675 | pCon i (vs, x) = (vs, PCon i x) |
1698 | 1676 | ||
@@ -1713,7 +1691,7 @@ commaSepUnfold p vs = commaSepUnfold1 p vs <|> pure (vs, []) | |||
1713 | 1691 | ||
1714 | telescope' ns vs = option (vs, []) $ do | 1692 | telescope' ns vs = option (vs, []) $ do |
1715 | (vs', vt) <- | 1693 | (vs', vt) <- |
1716 | operator "@" *> (f Hidden <$> patternAtom ns vs) | 1694 | reservedOp "@" *> (f Hidden <$> patternAtom ns vs) |
1717 | <|> f Visible <$> patternAtom ns vs | 1695 | <|> f Visible <$> patternAtom ns vs |
1718 | (id *** (vt:)) <$> telescope' ns vs' | 1696 | (id *** (vt:)) <$> telescope' ns vs' |
1719 | where | 1697 | where |
@@ -1770,7 +1748,7 @@ compileGuardTrees True ulend lend ge alts = foldr1 SParEval $ compileGuardTree u | |||
1770 | 1748 | ||
1771 | parseDef :: Namespace -> DBNames -> P [Stmt] | 1749 | parseDef :: Namespace -> DBNames -> P [Stmt] |
1772 | parseDef ns e = | 1750 | parseDef ns e = |
1773 | do keyword "data" | 1751 | do reserved "data" |
1774 | localIndentation Gt $ do | 1752 | localIndentation Gt $ do |
1775 | (si,x) <- siName $ upperCase (typeNS ns) | 1753 | (si,x) <- siName $ upperCase (typeNS ns) |
1776 | (nps, ts) <- telescopeSI (typeNS ns) (Just SType) (dbToSINames "parseDef data" e) | 1754 | (nps, ts) <- telescopeSI (typeNS ns) (Just SType) (dbToSINames "parseDef data" e) |
@@ -1780,58 +1758,58 @@ parseDef ns e = | |||
1780 | ( if mk then Just $ diffDBNames nps' npsd else Nothing | 1758 | ( if mk then Just $ diffDBNames nps' npsd else Nothing |
1781 | , foldr (uncurry SPi) (foldl SAppV (SGlobal (si,x)) $ downToS (length ts') $ length ts) ts') | 1759 | , foldr (uncurry SPi) (foldl SAppV (SGlobal (si,x)) $ downToS (length ts') $ length ts) ts') |
1782 | (af, cs) <- | 1760 | (af, cs) <- |
1783 | do (,) True <$ keyword "where" <*> localIndentation Ge (localAbsoluteIndentation $ many $ | 1761 | do (,) True <$ reserved "where" <*> localIndentation Ge (localAbsoluteIndentation $ many $ |
1784 | (id *** (,) Nothing) <$> typedIds ns Nothing npsd) | 1762 | (id *** (,) Nothing) <$> typedIds ns Nothing npsd) |
1785 | <|> do (,) False <$ operator "=" <*> | 1763 | <|> do (,) False <$ reservedOp "=" <*> |
1786 | sepBy1 ((,) <$> (pure <$> siName (upperCase ns)) | 1764 | sepBy1 ((,) <$> (pure <$> siName (upperCase ns)) |
1787 | <*> ( braces (mkConTy True <$> (telescopeDataFields (typeNS ns) nps)) | 1765 | <*> ( braces (mkConTy True <$> (telescopeDataFields (typeNS ns) nps)) |
1788 | <|> (mkConTy False <$> telescopeSI (typeNS ns) Nothing nps)) ) | 1766 | <|> (mkConTy False <$> telescopeSI (typeNS ns) Nothing nps)) ) |
1789 | (operator "|") | 1767 | (reservedOp "|") |
1790 | <|> pure (True, []) | 1768 | <|> pure (True, []) |
1791 | ge <- ask | 1769 | ge <- ask |
1792 | return $ mkData ge (si,x) ts t af $ concatMap (\(vs, t) -> (,) <$> vs <*> pure t) $ cs | 1770 | return $ mkData ge (si,x) ts t af $ concatMap (\(vs, t) -> (,) <$> vs <*> pure t) $ cs |
1793 | <|> do keyword "class" | 1771 | <|> do reserved "class" |
1794 | localIndentation Gt $ do | 1772 | localIndentation Gt $ do |
1795 | x <- siName $ upperCase (typeNS ns) | 1773 | x <- siName $ upperCase (typeNS ns) |
1796 | (nps, ts) <- telescope (typeNS ns) (Just SType) e | 1774 | (nps, ts) <- telescope (typeNS ns) (Just SType) e |
1797 | cs <- | 1775 | cs <- |
1798 | do keyword "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedIds ns Nothing nps) | 1776 | do reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedIds ns Nothing nps) |
1799 | <|> pure [] | 1777 | <|> pure [] |
1800 | return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure t) cs) | 1778 | return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure t) cs) |
1801 | <|> do keyword "instance" | 1779 | <|> do reserved "instance" |
1802 | let ns' = typeNS ns | 1780 | let ns' = typeNS ns |
1803 | localIndentation Gt $ do | 1781 | localIndentation Gt $ do |
1804 | constraints <- option [] $ try $ getTTuple' <$> parseTerm ns' PrecEq e <* operator "=>" | 1782 | constraints <- option [] $ try $ getTTuple' <$> parseTerm ns' PrecEq e <* reservedOp "=>" |
1805 | (si,x) <- siName $ upperCase ns' | 1783 | (si,x) <- siName $ upperCase ns' |
1806 | (nps, args) <- telescope' ns' e | 1784 | (nps, args) <- telescope' ns' e |
1807 | cs <- option [] $ keyword "where" *> localIndentation Ge (localAbsoluteIndentation $ some $ | 1785 | cs <- option [] $ reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ some $ |
1808 | funAltDef (varId ns) ns nps) | 1786 | funAltDef (varId ns) ns nps) |
1809 | <|> pure [] | 1787 | <|> pure [] |
1810 | ge <- ask | 1788 | ge <- ask |
1811 | return $ pure $ Instance (si,x) ({-todo-}map snd args) (deBruinify (diffDBNames nps e ++ [x]) <$> constraints) $ compileFunAlts' id{-TODO-} ge cs | 1789 | return $ pure $ Instance (si,x) ({-todo-}map snd args) (deBruinify (diffDBNames nps e ++ [x]) <$> constraints) $ compileFunAlts' id{-TODO-} ge cs |
1812 | <|> do try (keyword "type" >> keyword "family") | 1790 | <|> do try (reserved "type" >> reserved "family") |
1813 | let ns' = typeNS ns | 1791 | let ns' = typeNS ns |
1814 | localIndentation Gt $ do | 1792 | localIndentation Gt $ do |
1815 | (si, x) <- siName $ upperCase ns' | 1793 | (si, x) <- siName $ upperCase ns' |
1816 | (nps, ts) <- telescope ns' (Just SType) e | 1794 | (nps, ts) <- telescope ns' (Just SType) e |
1817 | t <- parseType ns' (Just SType) nps | 1795 | t <- parseType ns' (Just SType) nps |
1818 | option {-open type family-}[TypeFamily (si, x) ts t] $ do | 1796 | option {-open type family-}[TypeFamily (si, x) ts t] $ do |
1819 | cs <- keyword "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ | 1797 | cs <- reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ |
1820 | funAltDef (upperCase ns' >>= \x' -> guard (x == x') >> return x') ns' e) | 1798 | funAltDef (upperCase ns' >>= \x' -> guard (x == x') >> return x') ns' e) |
1821 | ge <- ask | 1799 | ge <- ask |
1822 | -- closed type family desugared here | 1800 | -- closed type family desugared here |
1823 | return $ compileFunAlts False id SLabelEnd ge [TypeAnn (si, x) $ addParamsS ts t] cs | 1801 | return $ compileFunAlts False id SLabelEnd ge [TypeAnn (si, x) $ addParamsS ts t] cs |
1824 | <|> do keyword "type" | 1802 | <|> do reserved "type" |
1825 | let ns' = typeNS ns | 1803 | let ns' = typeNS ns |
1826 | localIndentation Gt $ do | 1804 | localIndentation Gt $ do |
1827 | (si, x) <- siName $ upperCase ns' | 1805 | (si, x) <- siName $ upperCase ns' |
1828 | let addSI n = (debugSI "type telescope", n) | 1806 | let addSI n = (debugSI "type telescope", n) |
1829 | (nps, ts) <- telescopeSI ns' (Just (Wildcard SType)) (map addSI{-todo: remove-} e) | 1807 | (nps, ts) <- telescopeSI ns' (Just (Wildcard SType)) (map addSI{-todo: remove-} e) |
1830 | operator "=" | 1808 | reservedOp "=" |
1831 | rhs <- parseTerm ns' PrecLam $ map snd nps | 1809 | rhs <- parseTerm ns' PrecLam $ map snd nps |
1832 | ge <- ask | 1810 | ge <- ask |
1833 | return $ compileFunAlts False id SLabelEnd ge [{-TypeAnn (si, x) $ addParamsS ts $ SType-}{-todo-}] [FunAlt (si, x) (reverse $ zip (reverse ts) $ map PVar nps) Nothing rhs] | 1811 | return $ compileFunAlts False id SLabelEnd ge [{-TypeAnn (si, x) $ addParamsS ts $ SType-}{-todo-}] [FunAlt (si, x) (reverse $ zip (reverse ts) $ map PVar nps) Nothing rhs] |
1834 | <|> do try (keyword "type" >> keyword "instance") | 1812 | <|> do try (reserved "type" >> reserved "instance") |
1835 | let ns' = typeNS ns | 1813 | let ns' = typeNS ns |
1836 | pure <$> localIndentation Gt (funAltDef (upperCase ns') ns' e) | 1814 | pure <$> localIndentation Gt (funAltDef (upperCase ns') ns' e) |
1837 | <|> do (vs, t) <- try $ typedIds ns Nothing [] | 1815 | <|> do (vs, t) <- try $ typedIds ns Nothing [] |
@@ -1842,7 +1820,7 @@ parseDef ns e = | |||
1842 | where | 1820 | where |
1843 | telescopeDataFields ns vs = option (vs, []) $ do | 1821 | telescopeDataFields ns vs = option (vs, []) $ do |
1844 | (x, vt) <- do name <- siName $ var (expNS ns) | 1822 | (x, vt) <- do name <- siName $ var (expNS ns) |
1845 | operator "::" | 1823 | reservedOp "::" |
1846 | term <- parseTerm ns PrecLam (siToDBNames vs) | 1824 | term <- parseTerm ns PrecLam (siToDBNames vs) |
1847 | return (name, (Visible, term)) | 1825 | return (name, (Visible, term)) |
1848 | (id *** (vt:)) <$> (comma *> telescopeDataFields ns (x: vs) <|> pure (vs, [])) | 1826 | (id *** (vt:)) <$> (comma *> telescopeDataFields ns (x: vs) <|> pure (vs, [])) |
@@ -1852,18 +1830,18 @@ funAltDef parseName ns e = do -- todo: use ns to determine parseName | |||
1852 | do try' "operator definition" $ do | 1830 | do try' "operator definition" $ do |
1853 | (e', a1) <- patternAtom ns ("": e) | 1831 | (e', a1) <- patternAtom ns ("": e) |
1854 | localIndentation Gt $ do | 1832 | localIndentation Gt $ do |
1855 | (si,n) <- siName $ operator' | 1833 | (si,n) <- siName $ operatorT |
1856 | (e'', a2) <- patternAtom ns $ init (diffDBNames e' e) ++ n: e | 1834 | (e'', a2) <- patternAtom ns $ init (diffDBNames e' e) ++ n: e |
1857 | lookAhead $ operator "=" <|> operator "|" | 1835 | lookAhead $ reservedOp "=" <|> reservedOp "|" |
1858 | return ((si, n), (e'', (,) (Visible, Wildcard SType) <$> [a1, a2])) | 1836 | return ((si, n), (e'', (,) (Visible, Wildcard SType) <$> [a1, a2])) |
1859 | <|> do try $ do | 1837 | <|> do try $ do |
1860 | (si,n) <- siName $ parseName | 1838 | (si,n) <- siName $ parseName |
1861 | localIndentation Gt $ (,) (si, n) <$> telescope' ns (n: e) <* (lookAhead $ operator "=" <|> operator "|") | 1839 | localIndentation Gt $ (,) (si, n) <$> telescope' ns (n: e) <* (lookAhead $ reservedOp "=" <|> reservedOp "|") |
1862 | localIndentation Gt $ do | 1840 | localIndentation Gt $ do |
1863 | gu <- option Nothing $ do | 1841 | gu <- option Nothing $ do |
1864 | operator "|" | 1842 | reservedOp "|" |
1865 | Just <$> parseTerm ns PrecOp fe | 1843 | Just <$> parseTerm ns PrecOp fe |
1866 | operator "=" | 1844 | reservedOp "=" |
1867 | rhs <- parseTerm ns PrecLam []--fe | 1845 | rhs <- parseTerm ns PrecLam []--fe |
1868 | f <- parseWhereBlock ns fe | 1846 | f <- parseWhereBlock ns fe |
1869 | return $ FunAlt n ts gu $ deBruinify' fe {-hack-} $ f rhs | 1847 | return $ FunAlt n ts gu $ deBruinify' fe {-hack-} $ f rhs |
@@ -1877,7 +1855,7 @@ mkData ge x ts t af cs = [Data x ts t af $ (id *** snd) <$> cs] ++ concatMap mkP | |||
1877 | mkProj _ = [] | 1855 | mkProj _ = [] |
1878 | 1856 | ||
1879 | parseWhereBlock ns fe = option id $ do | 1857 | parseWhereBlock ns fe = option id $ do |
1880 | keyword "where" | 1858 | reserved "where" |
1881 | dcls <- localIndentation Ge (localAbsoluteIndentation $ parseDefs id ns fe) | 1859 | dcls <- localIndentation Ge (localAbsoluteIndentation $ parseDefs id ns fe) |
1882 | ge <- ask | 1860 | ge <- ask |
1883 | return $ mkLets ge dcls | 1861 | return $ mkLets ge dcls |
@@ -1892,7 +1870,7 @@ type DBNames = [SName] -- De Bruijn variable names | |||
1892 | 1870 | ||
1893 | valueDef :: Namespace -> DBNames -> P ((DBNames, Pat), SExp) | 1871 | valueDef :: Namespace -> DBNames -> P ((DBNames, Pat), SExp) |
1894 | valueDef ns e = do | 1872 | valueDef ns e = do |
1895 | (e', p) <- try $ pattern' ns e <* operator "=" | 1873 | (e', p) <- try $ pattern' ns e <* reservedOp "=" |
1896 | localIndentation Gt $ do | 1874 | localIndentation Gt $ do |
1897 | ex <- parseETerm ns PrecLam e | 1875 | ex <- parseETerm ns PrecLam e |
1898 | return ((diffDBNames e' e, p), ex) | 1876 | return ((diffDBNames e' e, p), ex) |
@@ -1904,39 +1882,38 @@ parseETerm ns = parseTerm $ expNS ns | |||
1904 | 1882 | ||
1905 | parseTerm :: Namespace -> Prec -> DBNames -> P SExp | 1883 | parseTerm :: Namespace -> Prec -> DBNames -> P SExp |
1906 | parseTerm ns PrecLam e = | 1884 | parseTerm ns PrecLam e = |
1907 | mkIf `withRange` ((,,) <$ keyword "if" <*> parseTerm ns PrecLam e <* keyword "then" <*> parseTerm ns PrecLam e <* keyword "else" <*> parseTerm ns PrecLam e) | 1885 | mkIf `withRange` ((,,) <$ reserved "if" <*> parseTerm ns PrecLam e <* reserved "then" <*> parseTerm ns PrecLam e <* reserved "else" <*> parseTerm ns PrecLam e) |
1908 | <|> do (tok, ns) <- (SPi . const Hidden <$ operator "." <|> SPi . const Visible <$ operator "->", typeNS ns) <$ keyword "forall" | 1886 | <|> do (tok, ns) <- (SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->", typeNS ns) <$ reserved "forall" |
1909 | (fe, ts) <- telescope ns (Just $ Wildcard SType) e | 1887 | (fe, ts) <- telescope ns (Just $ Wildcard SType) e |
1910 | f <- tok | 1888 | f <- tok |
1911 | t' <- parseTerm ns PrecLam fe | 1889 | t' <- parseTerm ns PrecLam fe |
1912 | return $ foldr (uncurry f) t' ts | 1890 | return $ foldr (uncurry f) t' ts |
1913 | <|> do sPos <- position | 1891 | <|> do appRange $ do |
1914 | (tok, ns) <- (asks (\a r -> patLam_ r id a) <* operator "->", expNS ns) <$ operator "\\" | 1892 | (tok, ns) <- (asks (\a r -> patLam_ r id a) <* reservedOp "->", expNS ns) <$ reservedOp "\\" |
1915 | (fe, ts) <- telescope' ns e | 1893 | (fe, ts) <- telescope' ns e |
1916 | f <- tok | 1894 | f <- tok |
1917 | t' <- parseTerm ns PrecLam fe | 1895 | t' <- parseTerm ns PrecLam fe |
1918 | ePos <- positionBeforeSpace | 1896 | return $ \r -> foldr (uncurry (f r)) t' ts |
1919 | return $ foldr (uncurry (f $ Range (sPos,ePos))) t' ts | 1897 | <|> do (asks compileCase) <* reserved "case" <*> parseETerm ns PrecLam e |
1920 | <|> do (asks compileCase) <* keyword "case" <*> parseETerm ns PrecLam e | 1898 | <* reserved "of" <*> localIndentation Ge (localAbsoluteIndentation $ some $ parseClause ns e) |
1921 | <* keyword "of" <*> localIndentation Ge (localAbsoluteIndentation $ some $ parseClause ns e) | ||
1922 | <|> do (asks $ \ge -> compileGuardTree id id ge . Alts) <*> parseSomeGuards ns (const True) e | 1899 | <|> do (asks $ \ge -> compileGuardTree id id ge . Alts) <*> parseSomeGuards ns (const True) e |
1923 | <|> do t <- parseTerm ns PrecEq e | 1900 | <|> do t <- parseTerm ns PrecEq e |
1924 | option t $ mkPi <$> (Visible <$ operator "->" <|> Hidden <$ operator "=>") <*> pure t <*> parseTTerm ns PrecLam e | 1901 | option t $ mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm ns PrecLam e |
1925 | parseTerm ns PrecEq e = parseTerm ns PrecAnn e >>= \t -> option t $ SCstr t <$ operator "~" <*> parseTTerm ns PrecAnn e | 1902 | parseTerm ns PrecEq e = parseTerm ns PrecAnn e >>= \t -> option t $ SCstr t <$ reservedOp "~" <*> parseTTerm ns PrecAnn e |
1926 | parseTerm ns PrecAnn e = parseTerm ns PrecOp e >>= \t -> option t $ SAnn t <$> parseType ns Nothing e | 1903 | parseTerm ns PrecAnn e = parseTerm ns PrecOp e >>= \t -> option t $ SAnn t <$> parseType ns Nothing e |
1927 | parseTerm ns PrecOp e = (asks $ \dcls -> calculatePrecs dcls e) <*> p' where | 1904 | parseTerm ns PrecOp e = (asks $ \dcls -> calculatePrecs dcls e) <*> p' where |
1928 | p' = ((\si (t, xs) -> (mkNat ns si 0, ("-!", t): xs)) `withRange` (operator "-" *> p_)) | 1905 | p' = ((\si (t, xs) -> (mkNat ns si 0, ("-!", t): xs)) `withRange` (reservedOp "-" *> p_)) |
1929 | <|> p_ | 1906 | <|> p_ |
1930 | p_ = (,) <$> parseTerm ns PrecApp e <*> (option [] $ operator' >>= p) | 1907 | p_ = (,) <$> parseTerm ns PrecApp e <*> (option [] $ operatorT >>= p) |
1931 | p op = do (exp, op') <- try ((,) <$> parseTerm ns PrecApp e <*> operator') | 1908 | p op = do (exp, op') <- try ((,) <$> parseTerm ns PrecApp e <*> operatorT) |
1932 | ((op, exp):) <$> p op' | 1909 | ((op, exp):) <$> p op' |
1933 | <|> pure . (,) op <$> parseTerm ns PrecLam e | 1910 | <|> pure . (,) op <$> parseTerm ns PrecLam e |
1934 | parseTerm ns PrecApp e = | 1911 | parseTerm ns PrecApp e = |
1935 | try {- TODO: adjust try for better error messages e.g. don't use braces -} | 1912 | try {- TODO: adjust try for better error messages e.g. don't use braces -} |
1936 | (foldl sapp <$> (sVar e `withRange` upperCase ns) <*> braces (commaSep $ lowerCase ns *> operator "=" *> ((,) Visible <$> parseTerm ns PrecLam e))) <|> | 1913 | (foldl sapp <$> (sVar e `withRange` upperCase ns) <*> braces (commaSep $ lowerCase ns *> reservedOp "=" *> ((,) Visible <$> parseTerm ns PrecLam e))) <|> |
1937 | (foldl sapp <$> parseTerm ns PrecSwiz e <*> many | 1914 | (foldl sapp <$> parseTerm ns PrecSwiz e <*> many |
1938 | ( (,) Visible <$> parseTerm ns PrecSwiz e | 1915 | ( (,) Visible <$> parseTerm ns PrecSwiz e |
1939 | <|> (,) Hidden <$ operator "@" <*> parseTTerm ns PrecSwiz e)) | 1916 | <|> (,) Hidden <$ reservedOp "@" <*> parseTTerm ns PrecSwiz e)) |
1940 | parseTerm ns PrecSwiz e = do | 1917 | parseTerm ns PrecSwiz e = do |
1941 | t <- parseTerm ns PrecProj e | 1918 | t <- parseTerm ns PrecProj e |
1942 | try (mkSwizzling t `withRange` (char '%' *> manyNM 1 4 (satisfy (`elem` ("xyzwrgba" :: [Char]))) <* whiteSpace)) <|> pure t | 1919 | try (mkSwizzling t `withRange` (char '%' *> manyNM 1 4 (satisfy (`elem` ("xyzwrgba" :: [Char]))) <* whiteSpace)) <|> pure t |
@@ -1949,20 +1926,20 @@ parseTerm ns PrecAtom e = | |||
1949 | <|> sLit `withRange` (LFloat <$> try float) | 1926 | <|> sLit `withRange` (LFloat <$> try float) |
1950 | <|> sLit `withRange` (LInt . fromIntegral <$ char '#' <*> natural) | 1927 | <|> sLit `withRange` (LInt . fromIntegral <$ char '#' <*> natural) |
1951 | <|> mkNat ns `withRange` natural | 1928 | <|> mkNat ns `withRange` natural |
1952 | <|> Wildcard (Wildcard SType) <$ keyword "_" | 1929 | <|> Wildcard (Wildcard SType) <$ reserved "_" |
1953 | <|> char '\'' *> parseTerm (switchNS ns) PrecAtom e | 1930 | <|> char '\'' *> parseTerm (switchNS ns) PrecAtom e |
1954 | <|> sVar e `withRange` (try (varId ns) <|> upperCase ns) | 1931 | <|> sVar e `withRange` (try (varId ns) <|> upperCase ns) |
1955 | <|> mkDotDot <$> try (operator "[" *> parseTerm ns PrecLam e <* operator ".." ) <*> parseTerm ns PrecLam e <* operator "]" | 1932 | <|> mkDotDot <$> try (reservedOp "[" *> parseTerm ns PrecLam e <* reservedOp ".." ) <*> parseTerm ns PrecLam e <* reservedOp "]" |
1956 | <|> listCompr ns e | 1933 | <|> listCompr ns e |
1957 | <|> mkList ns `withRange` brackets (commaSep $ parseTerm ns PrecLam e) | 1934 | <|> mkList ns `withRange` brackets (commaSep $ parseTerm ns PrecLam e) |
1958 | <|> mkLeftSection `withRange` try{-todo: better try-} (parens $ (,) <$> withRange (,) (guardM (/= "-") operator') <*> parseTerm ns PrecLam e) | 1935 | <|> mkLeftSection `withRange` try{-todo: better try-} (parens $ (,) <$> siName (guardM (/= "-") operatorT) <*> parseTerm ns PrecLam e) |
1959 | <|> mkRightSection `withRange` try{-todo: better try!-} (parens $ (,) <$> parseTerm ns PrecApp e <*> withRange (,) operator') | 1936 | <|> mkRightSection `withRange` try{-todo: better try!-} (parens $ (,) <$> parseTerm ns PrecApp e <*> siName operatorT) |
1960 | <|> mkTuple ns `withRange` parens (commaSep $ parseTerm ns PrecLam e) | 1937 | <|> mkTuple ns `withRange` parens (commaSep $ parseTerm ns PrecLam e) |
1961 | <|> mkRecord `withRange` braces (commaSep $ ((,) <$> lowerCase ns <* colon <*> parseTerm ns PrecLam e)) | 1938 | <|> mkRecord `withRange` braces (commaSep $ ((,) <$> lowerCase ns <* colon <*> parseTerm ns PrecLam e)) |
1962 | <|> do keyword "let" | 1939 | <|> do reserved "let" |
1963 | dcls <- localIndentation Ge (localAbsoluteIndentation $ parseDefs id ns e) | 1940 | dcls <- localIndentation Ge (localAbsoluteIndentation $ parseDefs id ns e) |
1964 | ge <- ask | 1941 | ge <- ask |
1965 | mkLets ge dcls <$ keyword "in" <*> parseTerm ns PrecLam e | 1942 | mkLets ge dcls <$ reserved "in" <*> parseTerm ns PrecLam e |
1966 | 1943 | ||
1967 | guardM p m = m >>= \x -> if p x then return x else fail "guardM" | 1944 | guardM p m = m >>= \x -> if p x then return x else fail "guardM" |
1968 | 1945 | ||
@@ -2011,11 +1988,6 @@ mkList _ si xs = error "mkList" | |||
2011 | mkNat (Namespace ExpLevel _) si n = SGlobal (noSI,"fromInt") `SAppV` sLit si (LInt $ fromIntegral n) | 1988 | mkNat (Namespace ExpLevel _) si n = SGlobal (noSI,"fromInt") `SAppV` sLit si (LInt $ fromIntegral n) |
2012 | mkNat _ _ n = toNat n | 1989 | mkNat _ _ n = toNat n |
2013 | 1990 | ||
2014 | infix 9 `withRange` | ||
2015 | |||
2016 | withRange :: (SI -> a -> b) -> P a -> P b | ||
2017 | withRange f p = (\p1 a p2 -> f (Range (p1,p2)) a) <$> position <*> p <*> positionBeforeSpace | ||
2018 | |||
2019 | siName :: P SName -> P SIName | 1991 | siName :: P SName -> P SIName |
2020 | siName = withSI | 1992 | siName = withSI |
2021 | 1993 | ||
@@ -2038,7 +2010,7 @@ manyNM n m p = do | |||
2038 | 2010 | ||
2039 | generator, letdecl, boolExpression :: Namespace -> DBNames -> P (DBNames, SExp -> SExp) | 2011 | generator, letdecl, boolExpression :: Namespace -> DBNames -> P (DBNames, SExp -> SExp) |
2040 | generator ns dbs = do | 2012 | generator ns dbs = do |
2041 | (dbs', pat) <- try $ pattern' ns dbs <* operator "<-" | 2013 | (dbs', pat) <- try $ pattern' ns dbs <* reservedOp "<-" |
2042 | exp <- parseTerm ns PrecLam dbs | 2014 | exp <- parseTerm ns PrecLam dbs |
2043 | ge <- ask | 2015 | ge <- ask |
2044 | return $ (,) dbs' $ \e -> application | 2016 | return $ (,) dbs' $ \e -> application |
@@ -2050,7 +2022,7 @@ generator ns dbs = do | |||
2050 | , exp | 2022 | , exp |
2051 | ] | 2023 | ] |
2052 | 2024 | ||
2053 | letdecl ns dbs = ask >>= \ge -> keyword "let" *> ((\((dbs', p), e) -> (dbs, \exp -> mkLets ge [ValueDef (dbs', p) e] exp)) <$> valueDef ns dbs) | 2025 | letdecl ns dbs = ask >>= \ge -> reserved "let" *> ((\((dbs', p), e) -> (dbs, \exp -> mkLets ge [ValueDef (dbs', p) e] exp)) <$> valueDef ns dbs) |
2054 | 2026 | ||
2055 | boolExpression ns dbs = do | 2027 | boolExpression ns dbs = do |
2056 | pred <- parseTerm ns PrecLam dbs | 2028 | pred <- parseTerm ns PrecLam dbs |
@@ -2060,8 +2032,8 @@ application = foldl1 SAppV | |||
2060 | 2032 | ||
2061 | listCompr :: Namespace -> DBNames -> P SExp | 2033 | listCompr :: Namespace -> DBNames -> P SExp |
2062 | listCompr ns dbs = (\e (dbs', fs) -> foldr ($) (deBruinify (diffDBNames dbs' dbs) e) fs) | 2034 | listCompr ns dbs = (\e (dbs', fs) -> foldr ($) (deBruinify (diffDBNames dbs' dbs) e) fs) |
2063 | <$> try' "List comprehension" ((SGlobal (noSI, "singleton") `SAppV`) <$ operator "[" <*> parseTerm ns PrecLam dbs <* operator "|") | 2035 | <$> try' "List comprehension" ((SGlobal (noSI, "singleton") `SAppV`) <$ reservedOp "[" <*> parseTerm ns PrecLam dbs <* reservedOp "|") |
2064 | <*> commaSepUnfold (liftA2 (<|>) (generator ns) $ liftA2 (<|>) (letdecl ns) (boolExpression ns)) dbs <* operator "]" | 2036 | <*> commaSepUnfold (liftA2 (<|>) (generator ns) $ liftA2 (<|>) (letdecl ns) (boolExpression ns)) dbs <* reservedOp "]" |
2065 | 2037 | ||
2066 | -- todo: make it more efficient | 2038 | -- todo: make it more efficient |
2067 | diffDBNames xs ys = take (length xs - length ys) xs | 2039 | diffDBNames xs ys = take (length xs - length ys) xs |
@@ -2171,15 +2143,15 @@ patLam_ :: SI -> (SExp -> SExp) -> GlobalEnv' -> (Visibility, SExp) -> Pat -> SE | |||
2171 | patLam_ si f ge (v, t) p e = SLam_ si v t $ compileGuardTree f f ge $ compilePatts [(p, 0)] Nothing e | 2143 | patLam_ si f ge (v, t) p e = SLam_ si v t $ compileGuardTree f f ge $ compilePatts [(p, 0)] Nothing e |
2172 | 2144 | ||
2173 | parseSomeGuards ns f e = do | 2145 | parseSomeGuards ns f e = do |
2174 | pos <- sourceColumn <$> getPosition <* operator "|" | 2146 | pos <- sourceColumn <$> getPosition <* reservedOp "|" |
2175 | guard $ f pos | 2147 | guard $ f pos |
2176 | (e', f) <- | 2148 | (e', f) <- |
2177 | do (e', PCon (_, p) vs) <- try $ pattern' ns e <* operator "<-" | 2149 | do (e', PCon (_, p) vs) <- try $ pattern' ns e <* reservedOp "<-" |
2178 | x <- parseETerm ns PrecEq e | 2150 | x <- parseETerm ns PrecEq e |
2179 | return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs) | 2151 | return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs) |
2180 | <|> do x <- parseETerm ns PrecEq e | 2152 | <|> do x <- parseETerm ns PrecEq e |
2181 | return (e, \gs' gs -> [GuardNode x "True" [] $ Alts gs', GuardNode x "False" [] $ Alts gs]) | 2153 | return (e, \gs' gs -> [GuardNode x "True" [] $ Alts gs', GuardNode x "False" [] $ Alts gs]) |
2182 | f <$> (parseSomeGuards ns (> pos) e' <|> (:[]) . GuardLeaf <$ operator "->" <*> parseETerm ns PrecLam e') | 2154 | f <$> (parseSomeGuards ns (> pos) e' <|> (:[]) . GuardLeaf <$ reservedOp "->" <*> parseETerm ns PrecLam e') |
2183 | <*> (parseSomeGuards ns (== pos) e <|> pure []) | 2155 | <*> (parseSomeGuards ns (== pos) e <|> pure []) |
2184 | 2156 | ||
2185 | toNat 0 = SGlobal (debugSI "toNat","Zero") | 2157 | toNat 0 = SGlobal (debugSI "toNat","Zero") |
@@ -2189,6 +2161,18 @@ toNatP si = run where | |||
2189 | run 0 = PCon (si, "Zero") [] | 2161 | run 0 = PCon (si, "Zero") [] |
2190 | run n | n > 0 = PCon (si, "Succ") [ParPat [run $ n-1]] | 2162 | run n | n > 0 = PCon (si, "Succ") [ParPat [run $ n-1]] |
2191 | 2163 | ||
2164 | addForalls :: Extensions -> [SName] -> SExp -> SExp | ||
2165 | addForalls exs defined x = foldl f x [v | v@(vh:_) <- reverse $ freeS x, v `notElem'` defined, isLower vh || NoConstructorNamespace `elem` exs] | ||
2166 | where | ||
2167 | f e v = SPi Hidden (Wildcard SType) $ substSG0 v e | ||
2168 | |||
2169 | defined defs = ("'Type":) $ flip foldMap defs $ \case | ||
2170 | TypeAnn (_, x) _ -> [x] | ||
2171 | Let (_, x) _ _ _ _ -> [x] | ||
2172 | Data (_, x) _ _ _ cs -> x: map (snd . fst) cs | ||
2173 | Class (_, x) _ cs -> x: map (snd . fst) cs | ||
2174 | TypeFamily (_, x) _ _ -> [x] | ||
2175 | x -> error $ unwords ["defined: Impossible", show x, "cann't be here"] | ||
2192 | -------------------------------------------------------------------------------- | 2176 | -------------------------------------------------------------------------------- |
2193 | 2177 | ||
2194 | class SourceInfo si where | 2178 | class SourceInfo si where |
@@ -2230,7 +2214,7 @@ patSI = \case | |||
2230 | PatType ps e -> sourceInfo ps <> sourceInfo e | 2214 | PatType ps e -> sourceInfo ps <> sourceInfo e |
2231 | 2215 | ||
2232 | data GuardTree | 2216 | data GuardTree |
2233 | = GuardNode SExp Name [ParPat] GuardTree -- _ <- _ | 2217 | = GuardNode SExp SName [ParPat] GuardTree -- _ <- _ |
2234 | | Alts [GuardTree] -- _ | _ | 2218 | | Alts [GuardTree] -- _ | _ |
2235 | | GuardLeaf SExp -- _ -> e | 2219 | | GuardLeaf SExp -- _ -> e |
2236 | deriving Show | 2220 | deriving Show |