From 6a5d6647c1dbd8708a851ec1c287a6946dab248b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Wed, 20 May 2020 12:17:06 -0500 Subject: [PATCH] Split Parser.Support --- idris2.ipkg | 2 + idris2api.ipkg | 2 + idris2rkt.ipkg | 2 + src/Core/Core.idr | 2 +- src/Idris/Error.idr | 2 +- src/Idris/IDEMode/Parser.idr | 10 +- src/Idris/Package.idr | 2 +- src/Idris/Parser.idr | 2 +- src/Idris/ProcessIdr.idr | 2 +- src/Parser/Lexer.idr | 49 ++-- src/Parser/Rule.idr | 417 ++++++++++++++++++++++++++++++++ src/Parser/Source.idr | 34 +++ src/Parser/Support.idr | 447 +---------------------------------- src/TTImp/Parser.idr | 2 +- src/TTImp/ProcessDecls.idr | 2 +- src/Yaffle/Main.idr | 2 +- src/Yaffle/REPL.idr | 2 +- 17 files changed, 505 insertions(+), 476 deletions(-) create mode 100644 src/Parser/Rule.idr create mode 100644 src/Parser/Source.idr diff --git a/idris2.ipkg b/idris2.ipkg index f54db6b17..41d09b197 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -83,6 +83,8 @@ modules = Idris.Version, Parser.Lexer, + Parser.Rule, + Parser.Source, Parser.Support, Parser.Unlit, diff --git a/idris2api.ipkg b/idris2api.ipkg index 88374b82b..648db2e26 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -83,6 +83,8 @@ modules = Idris.Version, Parser.Lexer, + Parser.Rule, + Parser.Source, Parser.Support, Parser.Unlit, diff --git a/idris2rkt.ipkg b/idris2rkt.ipkg index 2e2b97ff7..afc5fbf34 100644 --- a/idris2rkt.ipkg +++ b/idris2rkt.ipkg @@ -83,6 +83,8 @@ modules = Idris.Version, Parser.Lexer, + Parser.Rule, + Parser.Source, Parser.Support, Parser.Unlit, diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 1da905d47..8f48dd32c 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -4,7 +4,7 @@ import Core.Env import Core.TT import Data.List import Data.Vect -import Parser.Support +import Parser.Source import public Data.IORef import System diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index e9fbdda05..78bd38dc0 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -9,7 +9,7 @@ import Core.Options import Idris.Resugar import Idris.Syntax -import Parser.Support +import Parser.Source import Data.List diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr index c8e11fb80..a03703965 100644 --- a/src/Idris/IDEMode/Parser.idr +++ b/src/Idris/IDEMode/Parser.idr @@ -7,7 +7,7 @@ import Idris.IDEMode.Commands import Text.Parser import Parser.Lexer -import Parser.Support +import Parser.Source import Text.Lexer import Utils.Either import Utils.String @@ -21,7 +21,7 @@ import Data.Strings symbols : List String symbols = ["(", ":", ")"] -ideTokens : TokenMap Token +ideTokens : TokenMap SourceToken ideTokens = map (\x => (exact x, Symbol)) symbols ++ [(digits, \x => Literal (cast x)), @@ -29,7 +29,7 @@ ideTokens = (identAllowDashes, \x => NSIdent [x]), (space, Comment)] -idelex : String -> Either (Int, Int, String) (List (TokenData Token)) +idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken)) idelex str = case lex ideTokens str of -- Add the EndInput token so that we'll have a line and column @@ -38,7 +38,7 @@ idelex str [MkToken l c EndInput]) (_, fail) => Left fail where - notComment : TokenData Token -> Bool + notComment : TokenData SourceToken -> Bool notComment t = case tok t of Comment _ => False _ => True @@ -61,7 +61,7 @@ sexp pure (SExpList xs) ideParser : {e : _} -> - String -> Grammar (TokenData Token) e ty -> Either ParseError ty + String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty ideParser str p = do toks <- mapError LexFail $ idelex str parsed <- mapError mapParseError $ parse p toks diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index d8c3046b9..c14571c67 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -24,7 +24,7 @@ import Idris.SetOptions import Idris.Syntax import Idris.Version import Parser.Lexer -import Parser.Support +import Parser.Source import Utils.Binary import System diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 95bf60577..dc114c5ad 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -2,7 +2,7 @@ module Idris.Parser import Core.Options import Idris.Syntax -import public Parser.Support +import public Parser.Source import Parser.Lexer import TTImp.TTImp diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 9c846038d..7aa9e4968 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -193,7 +193,7 @@ readHeader path where -- Stop at the first :, that's definitely not part of the header, to -- save lexing the whole file unnecessarily - isColon : TokenData Token -> Bool + isColon : TokenData SourceToken -> Bool isColon t = case tok t of Symbol ":" => True diff --git a/src/Parser/Lexer.idr b/src/Parser/Lexer.idr index 76fdbec42..c5dd6505d 100644 --- a/src/Parser/Lexer.idr +++ b/src/Parser/Lexer.idr @@ -11,24 +11,25 @@ import Utils.String %default total public export -data Token = NSIdent (List String) - | HoleIdent String - | Literal Integer - | StrLit String - | CharLit String - | DoubleLit Double - | Symbol String - | Keyword String - | Unrecognised String - | Comment String - | DocComment String - | CGDirective String - | RecordField String - | Pragma String - | EndInput +data SourceToken + = NSIdent (List String) + | HoleIdent String + | Literal Integer + | StrLit String + | CharLit String + | DoubleLit Double + | Symbol String + | Keyword String + | Unrecognised String + | Comment String + | DocComment String + | CGDirective String + | RecordField String + | Pragma String + | EndInput export -Show Token where +Show SourceToken where show (HoleIdent x) = "hole identifier " ++ x show (Literal x) = "literal " ++ show x show (StrLit x) = "string " ++ show x @@ -179,7 +180,7 @@ cgDirective is '}') <|> many (isNot '\n')) -mkDirective : String -> Token +mkDirective : String -> SourceToken mkDirective str = CGDirective (trim (substr 3 (length str) str)) -- Reserved words @@ -242,7 +243,7 @@ fromOctLit str Nothing => 0 -- can't happen if the literal lexed correctly Just n => cast n -rawTokens : TokenMap Token +rawTokens : TokenMap SourceToken rawTokens = [(comment, Comment), (blockComment, Comment), @@ -264,18 +265,18 @@ rawTokens = (validSymbol, Symbol), (symbol, Unrecognised)] where - parseNSIdent : String -> Token + parseNSIdent : String -> SourceToken parseNSIdent = NSIdent . reverse . split (== '.') - parseIdent : String -> Token + parseIdent : String -> SourceToken parseIdent x = if x `elem` keywords then Keyword x else NSIdent [x] export -lexTo : (TokenData Token -> Bool) -> - String -> Either (Int, Int, String) (List (TokenData Token)) +lexTo : (TokenData SourceToken -> Bool) -> + String -> Either (Int, Int, String) (List (TokenData SourceToken)) lexTo pred str = case lexTo pred rawTokens str of -- Add the EndInput token so that we'll have a line and column @@ -284,12 +285,12 @@ lexTo pred str [MkToken l c EndInput]) (_, fail) => Left fail where - notComment : TokenData Token -> Bool + notComment : TokenData SourceToken -> Bool notComment t = case tok t of Comment _ => False DocComment _ => False -- TODO! _ => True export -lex : String -> Either (Int, Int, String) (List (TokenData Token)) +lex : String -> Either (Int, Int, String) (List (TokenData SourceToken)) lex = lexTo (const False) diff --git a/src/Parser/Rule.idr b/src/Parser/Rule.idr new file mode 100644 index 000000000..782d4ef2a --- /dev/null +++ b/src/Parser/Rule.idr @@ -0,0 +1,417 @@ +module Parser.Rule + +import public Parser.Lexer +import public Parser.Support +import public Text.Lexer +import public Text.Parser + +import Core.TT + +%default total + +public export +Rule : Type -> Type +Rule ty = Grammar (TokenData SourceToken) True ty + +public export +EmptyRule : Type -> Type +EmptyRule ty = Grammar (TokenData SourceToken) False ty + +-- Some basic parsers used by all the intermediate forms + +export +location : EmptyRule (Int, Int) +location + = do tok <- peek + pure (line tok, col tok) + +export +column : EmptyRule Int +column + = do (line, col) <- location + pure col + +export +eoi : EmptyRule () +eoi + = do nextIs "Expected end of input" (isEOI . tok) + pure () + where + isEOI : SourceToken -> Bool + isEOI EndInput = True + isEOI _ = False + +export +constant : Rule Constant +constant + = terminal "Expected constant" + (\x => case tok x of + Literal i => Just (BI i) + StrLit s => case escape s of + Nothing => Nothing + Just s' => Just (Str s') + CharLit c => case getCharLit c of + Nothing => Nothing + Just c' => Just (Ch c') + DoubleLit d => Just (Db d) + NSIdent ["Int"] => Just IntType + NSIdent ["Integer"] => Just IntegerType + NSIdent ["String"] => Just StringType + NSIdent ["Char"] => Just CharType + NSIdent ["Double"] => Just DoubleType + _ => Nothing) + +export +intLit : Rule Integer +intLit + = terminal "Expected integer literal" + (\x => case tok x of + Literal i => Just i + _ => Nothing) + +export +strLit : Rule String +strLit + = terminal "Expected string literal" + (\x => case tok x of + StrLit s => Just s + _ => Nothing) + +export +recField : Rule Name +recField + = terminal "Expected record field" + (\x => case tok x of + RecordField s => Just (RF s) + _ => Nothing) + +export +symbol : String -> Rule () +symbol req + = terminal ("Expected '" ++ req ++ "'") + (\x => case tok x of + Symbol s => if s == req then Just () + else Nothing + _ => Nothing) + +export +keyword : String -> Rule () +keyword req + = terminal ("Expected '" ++ req ++ "'") + (\x => case tok x of + Keyword s => if s == req then Just () + else Nothing + _ => Nothing) + +export +exactIdent : String -> Rule () +exactIdent req + = terminal ("Expected " ++ req) + (\x => case tok x of + NSIdent [s] => if s == req then Just () + else Nothing + _ => Nothing) + +export +pragma : String -> Rule () +pragma n = + terminal ("Expected pragma " ++ n) + (\x => case tok x of + Pragma s => + if s == n + then Just () + else Nothing + _ => Nothing) + +export +operator : Rule Name +operator + = terminal "Expected operator" + (\x => case tok x of + Symbol s => + if s `elem` reservedSymbols + then Nothing + else Just (UN s) + _ => Nothing) + +identPart : Rule String +identPart + = terminal "Expected name" + (\x => case tok x of + NSIdent [str] => Just str + _ => Nothing) + +export +nsIdent : Rule (List String) +nsIdent + = terminal "Expected namespaced name" + (\x => case tok x of + NSIdent ns => Just ns + _ => Nothing) + +export +unqualifiedName : Rule String +unqualifiedName = identPart + +export +holeName : Rule String +holeName + = terminal "Expected hole name" + (\x => case tok x of + HoleIdent str => Just str + _ => Nothing) + +reservedNames : List String +reservedNames + = ["Type", "Int", "Integer", "String", "Char", "Double", + "Lazy", "Inf", "Force", "Delay"] + +export +name : Rule Name +name = opNonNS <|> do + ns <- nsIdent + opNS ns <|> nameNS ns + where + reserved : String -> Bool + reserved n = n `elem` reservedNames + + nameNS : List String -> Grammar (TokenData SourceToken) False Name + nameNS [] = pure $ UN "IMPOSSIBLE" + nameNS [x] = + if reserved x + then fail $ "can't use reserved name " ++ x + else pure $ UN x + nameNS (x :: xs) = + if reserved x + then fail $ "can't use reserved name " ++ x + else pure $ NS xs (UN x) + + opNonNS : Rule Name + opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")" + + opNS : List String -> Rule Name + opNS ns = do + symbol ".(" + n <- (operator <|> recField) + symbol ")" + pure (NS ns n) + +export +IndentInfo : Type +IndentInfo = Int + +export +init : IndentInfo +init = 0 + +continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule () +continueF err indent + = do eoi; err + <|> do keyword "where"; err + <|> do col <- Rule.column + if col <= indent + then err + else pure () + +||| Fail if this is the end of a block entry or end of file +export +continue : (indent : IndentInfo) -> EmptyRule () +continue = continueF (fail "Unexpected end of expression") + +||| As 'continue' but failing is fatal (i.e. entire parse fails) +export +mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule () +mustContinue indent Nothing + = continueF (fatalError "Unexpected end of expression") indent +mustContinue indent (Just req) + = continueF (fatalError ("Expected '" ++ req ++ "'")) indent + +data ValidIndent = + ||| In {}, entries can begin in any column + AnyIndent | + ||| Entry must begin in a specific column + AtPos Int | + ||| Entry can begin in this column or later + AfterPos Int | + ||| Block is finished + EndOfBlock + +Show ValidIndent where + show AnyIndent = "[any]" + show (AtPos i) = "[col " ++ show i ++ "]" + show (AfterPos i) = "[after " ++ show i ++ "]" + show EndOfBlock = "[EOB]" + +checkValid : ValidIndent -> Int -> EmptyRule () +checkValid AnyIndent c = pure () +checkValid (AtPos x) c = if c == x + then pure () + else fail "Invalid indentation" +checkValid (AfterPos x) c = if c >= x + then pure () + else fail "Invalid indentation" +checkValid EndOfBlock c = fail "End of block" + +||| Any token which indicates the end of a statement/block +isTerminator : SourceToken -> Bool +isTerminator (Symbol ",") = True +isTerminator (Symbol "]") = True +isTerminator (Symbol ";") = True +isTerminator (Symbol "}") = True +isTerminator (Symbol ")") = True +isTerminator (Symbol "|") = True +isTerminator (Keyword "in") = True +isTerminator (Keyword "then") = True +isTerminator (Keyword "else") = True +isTerminator (Keyword "where") = True +isTerminator EndInput = True +isTerminator _ = False + +||| Check we're at the end of a block entry, given the start column +||| of the block. +||| It's the end if we have a terminating token, or the next token starts +||| in or before indent. Works by looking ahead but not consuming. +export +atEnd : (indent : IndentInfo) -> EmptyRule () +atEnd indent + = eoi + <|> do nextIs "Expected end of block" (isTerminator . tok) + pure () + <|> do col <- Rule.column + if (col <= indent) + then pure () + else fail "Not the end of a block entry" + +-- Check we're at the end, but only by looking at indentation +export +atEndIndent : (indent : IndentInfo) -> EmptyRule () +atEndIndent indent + = eoi + <|> do col <- Rule.column + if col <= indent + then pure () + else fail "Not the end of a block entry" + + +-- Parse a terminator, return where the next block entry +-- must start, given where the current block entry started +terminator : ValidIndent -> Int -> EmptyRule ValidIndent +terminator valid laststart + = do eoi + pure EndOfBlock + <|> do symbol ";" + pure (afterSemi valid) + <|> do col <- column + afterDedent valid col + <|> pure EndOfBlock + where + -- Expected indentation for the next token can either be anything (if + -- we're inside a brace delimited block) or anywhere after the initial + -- column (if we're inside an indentation delimited block) + afterSemi : ValidIndent -> ValidIndent + afterSemi AnyIndent = AnyIndent -- in braces, anything goes + afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position + afterSemi (AfterPos c) = AfterPos c + afterSemi EndOfBlock = EndOfBlock + + -- Expected indentation for the next token can either be anything (if + -- we're inside a brace delimited block) or in exactly the initial column + -- (if we're inside an indentation delimited block) + afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent + afterDedent AnyIndent col + = if col <= laststart + then pure AnyIndent + else fail "Not the end of a block entry" + afterDedent (AfterPos c) col + = if col <= laststart + then pure (AtPos c) + else fail "Not the end of a block entry" + afterDedent (AtPos c) col + = if col <= laststart + then pure (AtPos c) + else fail "Not the end of a block entry" + afterDedent EndOfBlock col = pure EndOfBlock + +-- Parse an entry in a block +blockEntry : ValidIndent -> (IndentInfo -> Rule ty) -> + Rule (ty, ValidIndent) +blockEntry valid rule + = do col <- column + checkValid valid col + p <- rule col + valid' <- terminator valid col + pure (p, valid') + +blockEntries : ValidIndent -> (IndentInfo -> Rule ty) -> + EmptyRule (List ty) +blockEntries valid rule + = do eoi; pure [] + <|> do res <- blockEntry valid rule + ts <- blockEntries (snd res) rule + pure (fst res :: ts) + <|> pure [] + +export +block : (IndentInfo -> Rule ty) -> EmptyRule (List ty) +block item + = do symbol "{" + commit + ps <- blockEntries AnyIndent item + symbol "}" + pure ps + <|> do col <- column + blockEntries (AtPos col) item + + +||| `blockAfter col rule` parses a `rule`-block indented by at +||| least `col` spaces (unless the block is explicitly delimited +||| by curly braces). `rule` is a function of the actual indentation +||| level. +export +blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty) +blockAfter mincol item + = do symbol "{" + commit + ps <- blockEntries AnyIndent item + symbol "}" + pure ps + <|> do col <- Rule.column + if col <= mincol + then pure [] + else blockEntries (AtPos col) item + +export +blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty) +blockWithOptHeaderAfter {ty} mincol header item + = do symbol "{" + commit + hidt <- optional $ blockEntry AnyIndent header + restOfBlock hidt + <|> do col <- Rule.column + if col <= mincol + then pure (Nothing, []) + else do hidt <- optional $ blockEntry (AtPos col) header + ps <- blockEntries (AtPos col) item + pure (map fst hidt, ps) + where + restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty) + restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item + symbol "}" + pure (Just h, ps) + restOfBlock Nothing = do ps <- blockEntries AnyIndent item + symbol "}" + pure (Nothing, ps) + +export +nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty) +nonEmptyBlock item + = do symbol "{" + commit + res <- blockEntry AnyIndent item + ps <- blockEntries (snd res) item + symbol "}" + pure (fst res :: ps) + <|> do col <- column + res <- blockEntry (AtPos col) item + ps <- blockEntries (snd res) item + pure (fst res :: ps) diff --git a/src/Parser/Source.idr b/src/Parser/Source.idr new file mode 100644 index 000000000..917ba3f71 --- /dev/null +++ b/src/Parser/Source.idr @@ -0,0 +1,34 @@ +module Parser.Source + +import public Parser.Lexer +import public Parser.Rule +import public Parser.Unlit +import public Text.Lexer +import public Text.Parser + +import System.File +import Utils.Either + +%default total + +export +runParserTo : {e : _} -> + Maybe LiterateStyle -> (TokenData SourceToken -> Bool) -> + String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty +runParserTo lit pred str p + = do str <- mapError LitFail $ unlit lit str + toks <- mapError LexFail $ lexTo pred str + parsed <- mapError mapParseError $ parse p toks + Right (fst parsed) + +export +runParser : {e : _} -> + Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty +runParser lit = runParserTo lit (const False) + +export +parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty) +parseFile fn p + = do Right str <- readFile fn + | Left err => pure (Left (FileFail err)) + pure (runParser (isLitFile fn) str p) diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index cdbca3586..0fd4a8ad2 100644 --- a/src/Parser/Support.idr +++ b/src/Parser/Support.idr @@ -1,28 +1,19 @@ module Parser.Support -import public Text.Lexer import public Parser.Lexer -import public Parser.Unlit +import public Text.Lexer import public Text.Parser import Core.TT import Data.List import Data.List.Views -import Utils.Either +import Parser.Unlit import System.File %default total public export -Rule : Type -> Type -Rule ty = Grammar (TokenData Token) True ty - -public export -EmptyRule : Type -> Type -EmptyRule ty = Grammar (TokenData Token) False ty - -public export -data ParseError = ParseFail String (Maybe (Int, Int)) (List Token) +data ParseError = ParseFail String (Maybe (Int, Int)) (List SourceToken) | LexFail (Int, Int, String) | FileFail FileError | LitFail LiterateError @@ -40,57 +31,11 @@ Show ParseError where = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str export -eoi : EmptyRule () -eoi - = do nextIs "Expected end of input" (isEOI . tok) - pure () - where - isEOI : Token -> Bool - isEOI EndInput = True - isEOI _ = False - -export -mapParseError : ParseError (TokenData Token) -> ParseError +mapParseError : ParseError (TokenData SourceToken) -> ParseError mapParseError (Error err []) = ParseFail err Nothing [] mapParseError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts)) export -runParserTo : {e : _} -> - Maybe LiterateStyle -> (TokenData Token -> Bool) -> - String -> Grammar (TokenData Token) e ty -> Either ParseError ty -runParserTo lit pred str p - = do str <- mapError LitFail $ unlit lit str - toks <- mapError LexFail $ lexTo pred str - parsed <- mapError mapParseError $ parse p toks - Right (fst parsed) - -export -runParser : {e : _} -> - Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty -runParser lit = runParserTo lit (const False) - -export -parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty) -parseFile fn p - = do Right str <- readFile fn - | Left err => pure (Left (FileFail err)) - pure (runParser (isLitFile fn) str p) - - --- Some basic parsers used by all the intermediate forms - -export -location : EmptyRule (Int, Int) -location - = do tok <- peek - pure (line tok, col tok) - -export -column : EmptyRule Int -column - = do (line, col) <- location - pure col - hex : Char -> Maybe Int hex '0' = Just 0 hex '1' = Just 1 @@ -110,6 +55,7 @@ hex 'e' = Just 14 hex 'f' = Just 15 hex _ = Nothing +export dec : Char -> Maybe Int dec '0' = Just 0 dec '1' = Just 1 @@ -123,6 +69,7 @@ dec '8' = Just 8 dec '9' = Just 9 dec _ = Nothing +export oct : Char -> Maybe Int oct '0' = Just 0 oct '1' = Just 1 @@ -134,6 +81,7 @@ oct '6' = Just 6 oct '7' = Just 7 oct _ = Nothing +export getEsc : String -> Maybe Char getEsc "NUL" = Just '\NUL' getEsc "SOH" = Just '\SOH' @@ -221,9 +169,11 @@ escape' ('\\' :: xs) !(assert_total (escape' rest)) escape' (x :: xs) = Just $ x :: !(escape' xs) +export escape : String -> Maybe String escape x = pure $ pack !(escape' (unpack x)) +export getCharLit : String -> Maybe Char getCharLit str = do e <- escape str @@ -232,382 +182,3 @@ getCharLit str else if length e == 0 -- parsed the NULL character that terminated the string! then Just '\0000' else Nothing - -export -constant : Rule Constant -constant - = terminal "Expected constant" - (\x => case tok x of - Literal i => Just (BI i) - StrLit s => case escape s of - Nothing => Nothing - Just s' => Just (Str s') - CharLit c => case getCharLit c of - Nothing => Nothing - Just c' => Just (Ch c') - DoubleLit d => Just (Db d) - NSIdent ["Int"] => Just IntType - NSIdent ["Integer"] => Just IntegerType - NSIdent ["String"] => Just StringType - NSIdent ["Char"] => Just CharType - NSIdent ["Double"] => Just DoubleType - _ => Nothing) - -export -intLit : Rule Integer -intLit - = terminal "Expected integer literal" - (\x => case tok x of - Literal i => Just i - _ => Nothing) - -export -strLit : Rule String -strLit - = terminal "Expected string literal" - (\x => case tok x of - StrLit s => Just s - _ => Nothing) - -export -recField : Rule Name -recField - = terminal "Expected record field" - (\x => case tok x of - RecordField s => Just (RF s) - _ => Nothing) - -export -symbol : String -> Rule () -symbol req - = terminal ("Expected '" ++ req ++ "'") - (\x => case tok x of - Symbol s => if s == req then Just () - else Nothing - _ => Nothing) - -export -keyword : String -> Rule () -keyword req - = terminal ("Expected '" ++ req ++ "'") - (\x => case tok x of - Keyword s => if s == req then Just () - else Nothing - _ => Nothing) - -export -exactIdent : String -> Rule () -exactIdent req - = terminal ("Expected " ++ req) - (\x => case tok x of - NSIdent [s] => if s == req then Just () - else Nothing - _ => Nothing) - -export -pragma : String -> Rule () -pragma n = - terminal ("Expected pragma " ++ n) - (\x => case tok x of - Pragma s => - if s == n - then Just () - else Nothing - _ => Nothing) - -export -operator : Rule Name -operator - = terminal "Expected operator" - (\x => case tok x of - Symbol s => - if s `elem` reservedSymbols - then Nothing - else Just (UN s) - _ => Nothing) - -identPart : Rule String -identPart - = terminal "Expected name" - (\x => case tok x of - NSIdent [str] => Just str - _ => Nothing) - -%hide Prelude.(>>=) - -export -nsIdent : Rule (List String) -nsIdent - = terminal "Expected namespaced name" - (\x => case tok x of - NSIdent ns => Just ns - _ => Nothing) - -export -unqualifiedName : Rule String -unqualifiedName = identPart - -export -holeName : Rule String -holeName - = terminal "Expected hole name" - (\x => case tok x of - HoleIdent str => Just str - _ => Nothing) - -reservedNames : List String -reservedNames - = ["Type", "Int", "Integer", "String", "Char", "Double", - "Lazy", "Inf", "Force", "Delay"] - -export -name : Rule Name -name = opNonNS <|> do - ns <- nsIdent - opNS ns <|> nameNS ns - where - reserved : String -> Bool - reserved n = n `elem` reservedNames - - nameNS : List String -> Grammar (TokenData Token) False Name - nameNS [] = pure $ UN "IMPOSSIBLE" - nameNS [x] = - if reserved x - then fail $ "can't use reserved name " ++ x - else pure $ UN x - nameNS (x :: xs) = - if reserved x - then fail $ "can't use reserved name " ++ x - else pure $ NS xs (UN x) - - opNonNS : Rule Name - opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")" - - opNS : List String -> Rule Name - opNS ns = do - symbol ".(" - n <- (operator <|> recField) - symbol ")" - pure (NS ns n) - -export -IndentInfo : Type -IndentInfo = Int - -export -init : IndentInfo -init = 0 - -%hide Prelude.pure - -continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule () -continueF err indent - = do eoi; err - <|> do keyword "where"; err - <|> do col <- Support.column - if col <= indent - then err - else pure () - -||| Fail if this is the end of a block entry or end of file -export -continue : (indent : IndentInfo) -> EmptyRule () -continue = continueF (fail "Unexpected end of expression") - -||| As 'continue' but failing is fatal (i.e. entire parse fails) -export -mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule () -mustContinue indent Nothing - = continueF (fatalError "Unexpected end of expression") indent -mustContinue indent (Just req) - = continueF (fatalError ("Expected '" ++ req ++ "'")) indent - -data ValidIndent = - ||| In {}, entries can begin in any column - AnyIndent | - ||| Entry must begin in a specific column - AtPos Int | - ||| Entry can begin in this column or later - AfterPos Int | - ||| Block is finished - EndOfBlock - -Show ValidIndent where - show AnyIndent = "[any]" - show (AtPos i) = "[col " ++ show i ++ "]" - show (AfterPos i) = "[after " ++ show i ++ "]" - show EndOfBlock = "[EOB]" - -checkValid : ValidIndent -> Int -> EmptyRule () -checkValid AnyIndent c = pure () -checkValid (AtPos x) c = if c == x - then pure () - else fail "Invalid indentation" -checkValid (AfterPos x) c = if c >= x - then pure () - else fail "Invalid indentation" -checkValid EndOfBlock c = fail "End of block" - -||| Any token which indicates the end of a statement/block -isTerminator : Token -> Bool -isTerminator (Symbol ",") = True -isTerminator (Symbol "]") = True -isTerminator (Symbol ";") = True -isTerminator (Symbol "}") = True -isTerminator (Symbol ")") = True -isTerminator (Symbol "|") = True -isTerminator (Keyword "in") = True -isTerminator (Keyword "then") = True -isTerminator (Keyword "else") = True -isTerminator (Keyword "where") = True -isTerminator EndInput = True -isTerminator _ = False - -||| Check we're at the end of a block entry, given the start column -||| of the block. -||| It's the end if we have a terminating token, or the next token starts -||| in or before indent. Works by looking ahead but not consuming. -export -atEnd : (indent : IndentInfo) -> EmptyRule () -atEnd indent - = eoi - <|> do nextIs "Expected end of block" (isTerminator . tok) - pure () - <|> do col <- Support.column - if (col <= indent) - then pure () - else fail "Not the end of a block entry" - --- Check we're at the end, but only by looking at indentation -export -atEndIndent : (indent : IndentInfo) -> EmptyRule () -atEndIndent indent - = eoi - <|> do col <- Support.column - if col <= indent - then pure () - else fail "Not the end of a block entry" - - --- Parse a terminator, return where the next block entry --- must start, given where the current block entry started -terminator : ValidIndent -> Int -> EmptyRule ValidIndent -terminator valid laststart - = do eoi - pure EndOfBlock - <|> do symbol ";" - pure (afterSemi valid) - <|> do col <- column - afterDedent valid col - <|> pure EndOfBlock - where - -- Expected indentation for the next token can either be anything (if - -- we're inside a brace delimited block) or anywhere after the initial - -- column (if we're inside an indentation delimited block) - afterSemi : ValidIndent -> ValidIndent - afterSemi AnyIndent = AnyIndent -- in braces, anything goes - afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position - afterSemi (AfterPos c) = AfterPos c - afterSemi EndOfBlock = EndOfBlock - - -- Expected indentation for the next token can either be anything (if - -- we're inside a brace delimited block) or in exactly the initial column - -- (if we're inside an indentation delimited block) - afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent - afterDedent AnyIndent col - = if col <= laststart - then pure AnyIndent - else fail "Not the end of a block entry" - afterDedent (AfterPos c) col - = if col <= laststart - then pure (AtPos c) - else fail "Not the end of a block entry" - afterDedent (AtPos c) col - = if col <= laststart - then pure (AtPos c) - else fail "Not the end of a block entry" - afterDedent EndOfBlock col = pure EndOfBlock - --- Parse an entry in a block -blockEntry : ValidIndent -> (IndentInfo -> Rule ty) -> - Rule (ty, ValidIndent) -blockEntry valid rule - = do col <- column - checkValid valid col - p <- rule col - valid' <- terminator valid col - pure (p, valid') - -blockEntries : ValidIndent -> (IndentInfo -> Rule ty) -> - EmptyRule (List ty) -blockEntries valid rule - = do eoi; pure [] - <|> do res <- blockEntry valid rule - ts <- blockEntries (snd res) rule - pure (fst res :: ts) - <|> pure [] - -export -block : (IndentInfo -> Rule ty) -> EmptyRule (List ty) -block item - = do symbol "{" - commit - ps <- blockEntries AnyIndent item - symbol "}" - pure ps - <|> do col <- column - blockEntries (AtPos col) item - - -||| `blockAfter col rule` parses a `rule`-block indented by at -||| least `col` spaces (unless the block is explicitly delimited -||| by curly braces). `rule` is a function of the actual indentation -||| level. -export -blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty) -blockAfter mincol item - = do symbol "{" - commit - ps <- blockEntries AnyIndent item - symbol "}" - pure ps - <|> do col <- Support.column - if col <= mincol - then pure [] - else blockEntries (AtPos col) item - -export -blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty) -blockWithOptHeaderAfter {ty} mincol header item - = do symbol "{" - commit - hidt <- optional $ blockEntry AnyIndent header - restOfBlock hidt - <|> do col <- Support.column - if col <= mincol - then pure (Nothing, []) - else do hidt <- optional $ blockEntry (AtPos col) header - ps <- blockEntries (AtPos col) item - pure (map fst hidt, ps) - where - restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty) - restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item - symbol "}" - pure (Just h, ps) - restOfBlock Nothing = do ps <- blockEntries AnyIndent item - symbol "}" - pure (Nothing, ps) - -export -nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty) -nonEmptyBlock item - = do symbol "{" - commit - res <- blockEntry AnyIndent item - ps <- blockEntries (snd res) item - symbol "}" - pure (fst res :: ps) - <|> do col <- column - res <- blockEntry (AtPos col) item - ps <- blockEntries (snd res) item - pure (fst res :: ps) diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 3469148d4..b8dd1444a 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -4,7 +4,7 @@ import Core.Context import Core.Core import Core.Env import Core.TT -import Parser.Support +import Parser.Source import TTImp.TTImp import public Text.Parser diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 8b554e8f0..8de85f854 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -6,7 +6,7 @@ import Core.Env import Core.Metadata import Core.UnifyState -import Parser.Support +import Parser.Source import TTImp.BindImplicits import TTImp.Elab.Check diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index d7ecd2ba2..b7d981e51 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -1,6 +1,6 @@ module Yaffle.Main -import Parser.Support +import Parser.Source import Core.Binary import Core.Context diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr index 72eb038a9..adadd448a 100644 --- a/src/Yaffle/REPL.idr +++ b/src/Yaffle/REPL.idr @@ -21,7 +21,7 @@ import TTImp.ProcessDecls import TTImp.TTImp import TTImp.Unelab -import Parser.Support +import Parser.Source %default covering