diff --git a/idris2.ipkg b/idris2.ipkg index 54b6c23d065..a30c5b2b1bd 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -83,9 +83,12 @@ modules = Idris.Version, Parser.Lexer.Common, + Parser.Lexer.Package, Parser.Lexer.Source, Parser.Rule.Common, + Parser.Rule.Package, Parser.Rule.Source, + Parser.Package, Parser.Source, Parser.Support, Parser.Unlit, diff --git a/idris2api.ipkg b/idris2api.ipkg index e530493e72a..3b6cff3afcc 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -83,9 +83,12 @@ modules = Idris.Version, Parser.Lexer.Common, + Parser.Lexer.Package, Parser.Lexer.Source, Parser.Rule.Common, + Parser.Rule.Package, Parser.Rule.Source, + Parser.Package, Parser.Source, Parser.Support, Parser.Unlit, diff --git a/idris2rkt.ipkg b/idris2rkt.ipkg index 04aeb9011d7..b30ab8a9e37 100644 --- a/idris2rkt.ipkg +++ b/idris2rkt.ipkg @@ -83,9 +83,12 @@ modules = Idris.Version, Parser.Lexer.Common, + Parser.Lexer.Package, Parser.Lexer.Source, Parser.Rule.Common, + Parser.Rule.Package, Parser.Rule.Source, + Parser.Package, Parser.Source, Parser.Support, Parser.Unlit, diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 8f48dd32c48..9c1f2d1c65a 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -119,7 +119,8 @@ data Error : Type where GenericMsg : FC -> String -> Error TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error - ParseFail : FC -> ParseError -> Error + ParseFail : Show token => + FC -> ParseError token -> Error ModuleNotFound : FC -> List String -> Error CyclicImports : List (List String) -> Error ForceNeeded : Error diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr index 7dfeceb537b..b067bcecd16 100644 --- a/src/Idris/IDEMode/Parser.idr +++ b/src/Idris/IDEMode/Parser.idr @@ -5,16 +5,15 @@ module Idris.IDEMode.Parser import Idris.IDEMode.Commands -import Text.Parser +import Data.List +import Data.Strings import Parser.Lexer.Source import Parser.Source import Text.Lexer +import Text.Parser import Utils.Either import Utils.String -import Data.List -import Data.Strings - %hide Text.Lexer.symbols %hide Parser.Lexer.Source.symbols @@ -60,15 +59,14 @@ sexp symbol ")" pure (SExpList xs) -ideParser : {e : _} -> - String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty +ideParser : {e : _} -> String -> Grammar (TokenData SourceToken) e ty -> Either (ParseError SourceToken) ty ideParser str p = do toks <- mapError LexFail $ idelex str - parsed <- mapError mapParseError $ parse p toks + parsed <- mapError toGenericParsingError $ parse p toks Right (fst parsed) export -parseSExp : String -> Either ParseError SExp +parseSExp : String -> Either (ParseError SourceToken) SExp parseSExp inp = ideParser inp (do c <- sexp; eoi; pure c) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 05d5b1fd905..07e6590f87c 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -15,6 +15,12 @@ import Data.Strings import Data.StringTrie import Data.These +import Parser.Package +import System +import Text.Parser +import Utils.Binary +import Utils.String + import Idris.CommandLine import Idris.ModTree import Idris.ProcessIdr @@ -23,13 +29,6 @@ import Idris.REPLOpts import Idris.SetOptions import Idris.Syntax import Idris.Version -import Parser.Lexer.Source -import Parser.Source -import Utils.Binary - -import System -import Text.Parser - import IdrisPaths %default covering @@ -114,7 +113,7 @@ data DescField : Type where PPreclean : FC -> String -> DescField PPostclean : FC -> String -> DescField -field : String -> SourceRule DescField +field : String -> PackageRule DescField field fname = strField PVersion "version" <|> strField PAuthors "authors" @@ -134,43 +133,35 @@ field fname <|> strField PPostinstall "postinstall" <|> strField PPreclean "preclean" <|> strField PPostclean "postclean" - <|> do exactIdent "depends"; symbol "=" - ds <- sepBy1 (symbol ",") unqualifiedName + <|> do exactProperty "depends" + ds <- sep (map dotSep moduleIdent) pure (PDepends ds) - <|> do exactIdent "modules"; symbol "=" - ms <- sepBy1 (symbol ",") - (do start <- location - ns <- namespacedIdent - end <- location - Parser.Core.pure (MkFC fname start end, ns)) - Parser.Core.pure (PModules ms) - <|> do exactIdent "main"; symbol "=" + <|> do exactProperty "modules" + ms <- sep (do start <- location + m <- moduleIdent + end <- location + pure (MkFC fname start end, m)) + pure (PModules ms) + <|> do exactProperty "main" start <- location m <- namespacedIdent end <- location - Parser.Core.pure (PMainMod (MkFC fname start end) m) - <|> do exactIdent "executable"; symbol "=" - e <- unqualifiedName - Parser.Core.pure (PExec e) + pure (PMainMod (MkFC fname start end) m) + <|> do exactProperty "executable" + e <- getString + pure (PExec e) where - getStr : (FC -> String -> DescField) -> FC -> - String -> Constant -> SourceEmptyRule DescField - getStr p fc fld (Str s) = pure (p fc s) - getStr p fc fld _ = fail $ fld ++ " field must be a string" - - strField : (FC -> String -> DescField) -> String -> SourceRule DescField + strField : (FC -> String -> DescField) -> String -> PackageRule DescField strField p f = do start <- location - exactIdent f - symbol "=" - c <- constant + exactProperty f + str <- getString end <- location - getStr p (MkFC fname start end) f c + pure $ p (MkFC fname start end) str -parsePkgDesc : String -> SourceRule (String, List DescField) +parsePkgDesc : String -> PackageRule (String, List DescField) parsePkgDesc fname - = do exactIdent "package" - name <- unqualifiedName + = do name <- packageName fields <- many (field fname) pure (name, fields) @@ -425,6 +416,12 @@ clean pkg delete $ ttFile ++ ".ttc" delete $ ttFile ++ ".ttm" +getParseErrorLoc : String -> ParseError PackageToken -> FC +getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos +getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c) +getParseErrorLoc fname (LitFail _) = MkFC fname (0, 0) (0, 0) -- TODO: Remove this unused case +getParseErrorLoc fname _ = replFC + -- Just load the 'Main' module, if it exists, which will involve building -- it if necessary runRepl : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index b2ec3851364..e9544bbe923 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -177,7 +177,7 @@ modTime fname pure (cast t) export -getParseErrorLoc : String -> ParseError -> FC +getParseErrorLoc : String -> ParseError SourceToken -> FC getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c) getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index b04ca9970c2..e7cc22583f4 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -749,7 +749,7 @@ parseCmd : SourceEmptyRule (Maybe REPLCmd) parseCmd = do c <- command; eoi; pure $ Just c export -parseRepl : String -> Either ParseError (Maybe REPLCmd) +parseRepl : String -> Either (ParseError SourceToken) (Maybe REPLCmd) parseRepl inp = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd) diff --git a/src/Parser/Lexer/Common.idr b/src/Parser/Lexer/Common.idr index 7f811db2ae5..bacf7faeff9 100644 --- a/src/Parser/Lexer/Common.idr +++ b/src/Parser/Lexer/Common.idr @@ -72,10 +72,17 @@ namespaceIdent' b = ident Capitalised <+> many leavingLastIdent leavingLastIdent = if b then (is '.' <+> ident Capitalised) else (is '.' <+> ident Capitalised <+> expect (is '.')) -export namespaceIdent : Lexer namespaceIdent = namespaceIdent' False +export +namespacedIdent : Lexer +namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal) + export moduleIdent : Lexer moduleIdent = namespaceIdent' True + +export +spaceOrNewline : Lexer +spaceOrNewline = some (is ' ' <|> is '\t' <|> is '\n') diff --git a/src/Parser/Lexer/Package.idr b/src/Parser/Lexer/Package.idr index 30cf105ef41..e92de2b6c34 100644 --- a/src/Parser/Lexer/Package.idr +++ b/src/Parser/Lexer/Package.idr @@ -1,13 +1,76 @@ module Parser.Lexer.Package +import public Parser.Lexer.Common import public Text.Lexer import public Text.Parser +import Data.List +import Data.Strings +import Data.String.Extra +import Utils.String + %default total public export data PackageToken - = Comment - | Ident - | Module - | StringLit + = Comment String + | EndOfInput + | NamespacedIdent (List String) + | Module (List String) + | PackageName String + | Property String + | Separator + | Space + | StringLit String + +public export +Show PackageToken where + show (Comment str) = "Comment: " ++ str + show EndOfInput = "EndOfInput" + show (NamespacedIdent nsid) = "Identifier " ++ dotSep nsid + show (Module m) = "Module: " ++ dotSep m + show (PackageName n) = "Package name: " ++ n + show (Property p) = "Property: " ++ p + show Separator = "Separator" + show Space = "Space" + show (StringLit s) = "StringLit: " ++ s + +packageIdent : Lexer +packageIdent = exact "package" <+> is ' ' <+> identAllowDashes + +propertyAssignment : Lexer +propertyAssignment = identAllowDashes <+> many (space <|> newline) <+> is '=' + +separator : Lexer +separator = is ',' + +rawTokens : TokenMap PackageToken +rawTokens = + [ (comment, Comment . drop 2) + , (moduleIdent, Module . splitNamespace) + , (namespacedIdent, NamespacedIdent . splitNamespace) + , (packageIdent, PackageName . drop 8) + , (propertyAssignment, \x => case head' . words $ x of + Just p => Property p + -- TODO: Mark as impossible case due to ident lexer. + Nothing => Property "") + , (separator, const Separator) + , (spaceOrNewline, const Space) + , (stringLit, \s => StringLit (stripQuotes s)) + ] + where + splitNamespace : String -> List String + splitNamespace = Data.Strings.split (== '.') + +export +lex : String -> Either (Int, Int, String) (List (TokenData PackageToken)) +lex str = + case lexTo (const False) rawTokens str of + (tokenData, (l, c, "")) => + Right $ (filter (useful . tok) tokenData) ++ [MkToken l c EndOfInput] + (_, fail) => Left fail + where + useful : PackageToken -> Bool + useful (Comment c) = False + useful Space = False + useful _ = True diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 77800cbd293..90938b1c98f 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -109,9 +109,6 @@ docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n') holeIdent : Lexer holeIdent = is '?' <+> identNormal -namespacedIdent : Lexer -namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal) - recField : Lexer recField = is '.' <+> identNormal diff --git a/src/Parser/Package.idr b/src/Parser/Package.idr new file mode 100644 index 00000000000..00f69b5055c --- /dev/null +++ b/src/Parser/Package.idr @@ -0,0 +1,24 @@ +module Parser.Package + +import public Parser.Lexer.Package +import public Parser.Rule.Package +import public Text.Lexer +import public Text.Parser +import public Parser.Support + +import System.File +import Utils.Either + +export +runParser : String -> PackageRule ty -> Either (ParseError PackageToken) ty +runParser str p + = do toks <- mapError LexFail $ lex str + parsed <- mapError toGenericParsingError $ parse p toks + Right (fst parsed) + +export +parseFile : (fn : String) -> PackageRule ty -> IO (Either (ParseError PackageToken) ty) +parseFile fn p + = do Right str <- readFile fn + | Left err => pure (Left (FileFail err)) + pure (runParser str p) diff --git a/src/Parser/Rule/Package.idr b/src/Parser/Rule/Package.idr new file mode 100644 index 00000000000..c4e4e499419 --- /dev/null +++ b/src/Parser/Rule/Package.idr @@ -0,0 +1,69 @@ +module Parser.Rule.Package + +import public Parser.Lexer.Package +import public Parser.Rule.Common + +import Data.List + +%default total + +public export +PackageRule : Type -> Type +PackageRule = Rule PackageToken + +public export +PackageEmptyRule : Type -> Type +PackageEmptyRule = EmptyRule PackageToken + +export +eoi : PackageRule () +eoi = terminal "Expected end of input" + (\x => case tok x of + EndOfInput => Just () + _ => Nothing) + +export +exactProperty : String -> PackageRule String +exactProperty p = terminal "Expected property assignment" + (\x => case tok x of + Property p' => if p == p' then Just p + else Nothing + _ => Nothing) + +export +getString : PackageRule String +getString = terminal "Expected string" + (\x => case tok x of + StringLit str => Just str + _ => Nothing) + +export +namespacedIdent : PackageRule (List String) +namespacedIdent = terminal "Expected namespaced identifier" + (\x => case tok x of + NamespacedIdent nsid => Just $ reverse nsid + _ => Nothing) + +export +moduleIdent : PackageRule (List String) +moduleIdent = terminal "Expected module identifier" + (\x => case tok x of + Module m => Just $ reverse m + _ => Nothing) + +export +packageName : PackageRule String +packageName = terminal "Expected package name" + (\x => case tok x of + PackageName str => Just str + _ => Nothing) + +sep' : PackageRule () +sep' = terminal "Expected separator" + (\x => case tok x of + Separator => Just () + _ => Nothing) + +export +sep : PackageRule t -> PackageRule (List t) +sep rule = sepBy1 sep' rule diff --git a/src/Parser/Source.idr b/src/Parser/Source.idr index cbf5f83149a..91a5e981bd8 100644 --- a/src/Parser/Source.idr +++ b/src/Parser/Source.idr @@ -3,8 +3,6 @@ module Parser.Source import public Parser.Lexer.Source import public Parser.Rule.Source import public Parser.Unlit -import public Text.Lexer -import public Text.Parser import System.File import Utils.Either @@ -14,20 +12,20 @@ import Utils.Either export runParserTo : {e : _} -> Maybe LiterateStyle -> (TokenData SourceToken -> Bool) -> - String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty + String -> Grammar (TokenData SourceToken) e ty -> Either (ParseError SourceToken) 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 + parsed <- mapError toGenericParsingError $ parse p toks Right (fst parsed) export runParser : {e : _} -> - Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty + Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either (ParseError SourceToken) ty runParser lit = runParserTo lit (const False) export -parseFile : (fn : String) -> SourceRule ty -> IO (Either ParseError ty) +parseFile : (fn : String) -> SourceRule ty -> IO (Either (ParseError SourceToken) ty) parseFile fn p = do Right str <- readFile fn | Left err => pure (Left (FileFail err)) diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index 2246dbce4a3..a09594b04cd 100644 --- a/src/Parser/Support.idr +++ b/src/Parser/Support.idr @@ -13,13 +13,14 @@ import System.File %default total public export -data ParseError = ParseFail String (Maybe (Int, Int)) (List SourceToken) - | LexFail (Int, Int, String) - | FileFail FileError - | LitFail LiterateError +data ParseError tok + = ParseFail String (Maybe (Int, Int)) (List tok) + | LexFail (Int, Int, String) + | FileFail FileError + | LitFail LiterateError export -Show ParseError where +Show tok => Show (ParseError tok) where show (ParseFail err loc toks) = "Parse error: " ++ err ++ " (next tokens: " ++ show (take 10 toks) ++ ")" @@ -31,9 +32,9 @@ Show ParseError where = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str export -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)) +toGenericParsingError : ParsingError (TokenData token) -> ParseError token +toGenericParsingError (Error err []) = ParseFail err Nothing [] +toGenericParsingError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts)) export hex : Char -> Maybe Int diff --git a/src/Text/Parser/Core.idr b/src/Text/Parser/Core.idr index e3e948770b4..67769b5059d 100644 --- a/src/Text/Parser/Core.idr +++ b/src/Text/Parser/Core.idr @@ -276,14 +276,14 @@ mutual -- doParse _ _ _ = Failure True True "Help the coverage checker!" [] public export -data ParseError tok = Error String (List tok) +data ParsingError tok = Error String (List tok) ||| Parse a list of tokens according to the given grammar. If successful, ||| returns a pair of the parse result and the unparsed tokens (the remaining ||| input). export parse : {c : Bool} -> (act : Grammar tok c ty) -> (xs : List tok) -> - Either (ParseError tok) (ty, List tok) + Either (ParsingError tok) (ty, List tok) parse act xs = case doParse False act xs of Failure _ _ msg ts => Left (Error msg ts)