Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Split Source and Package Parser (Part 2) #113

Merged
merged 1 commit into from
May 24, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/source/reference/records.rst
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Lexical structure
constructor ``RF "foo"``)

* ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
identifier: ``NSIdent ["baz", "bar", "Foo"]``
identifier: ``DotSepIdent ["baz", "bar", "Foo"]``

* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
``.bar``, ``.baz``
Expand Down
3 changes: 3 additions & 0 deletions idris2.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
3 changes: 3 additions & 0 deletions idris2api.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
3 changes: 2 additions & 1 deletion src/Core/Core.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
28 changes: 13 additions & 15 deletions src/Idris/IDEMode/Parser.idr
Original file line number Diff line number Diff line change
Expand Up @@ -5,31 +5,30 @@ 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

symbols : List String
symbols = ["(", ":", ")"]

ideTokens : TokenMap SourceToken
ideTokens : TokenMap Token
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(identAllowDashes, \x => NSIdent [x]),
[(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(identAllowDashes, \x => Ident x),
(space, Comment)]

idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
idelex : String -> Either (Int, Int, String) (List (TokenData Token))
idelex str
= case lex ideTokens str of
-- Add the EndInput token so that we'll have a line and column
Expand All @@ -38,12 +37,12 @@ idelex str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData SourceToken -> Bool
notComment : TokenData Token -> Bool
notComment t = case tok t of
Comment _ => False
_ => True

sexp : SourceRule SExp
sexp : Rule SExp
sexp
= do symbol ":"; exactIdent "True"
pure (BoolAtom True)
Expand All @@ -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 Token) e ty -> Either (ParseError Token) 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 Token) SExp
parseSExp inp
= ideParser inp (do c <- sexp; eoi; pure c)
77 changes: 40 additions & 37 deletions src/Idris/Package.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -114,7 +113,7 @@ data DescField : Type where
PPreclean : FC -> String -> DescField
PPostclean : FC -> String -> DescField

field : String -> SourceRule DescField
field : String -> Rule DescField
field fname
= strField PVersion "version"
<|> strField PAuthors "authors"
Expand All @@ -134,43 +133,41 @@ field fname
<|> strField PPostinstall "postinstall"
<|> strField PPreclean "preclean"
<|> strField PPostclean "postclean"
<|> do exactIdent "depends"; symbol "="
ds <- sepBy1 (symbol ",") unqualifiedName
<|> do exactProperty "depends"
equals
ds <- sep packageName
pure (PDepends ds)
<|> do exactIdent "modules"; symbol "="
ms <- sepBy1 (symbol ",")
(do start <- location
ns <- nsIdent
end <- location
Parser.Core.pure (MkFC fname start end, ns))
Parser.Core.pure (PModules ms)
<|> do exactIdent "main"; symbol "="
<|> do exactProperty "modules"
equals
ms <- sep (do start <- location
m <- moduleIdent
end <- location
pure (MkFC fname start end, m))
pure (PModules ms)
<|> do exactProperty "main"
equals
start <- location
m <- nsIdent
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"
equals
e <- (stringLit <|> packageName)
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 p f
strField : (FC -> String -> DescField) -> String -> Rule DescField
strField fieldConstructor fieldName
fabianhjr marked this conversation as resolved.
Show resolved Hide resolved
= do start <- location
exactIdent f
symbol "="
c <- constant
exactProperty fieldName
equals
str <- stringLit
end <- location
getStr p (MkFC fname start end) f c
pure $ fieldConstructor (MkFC fname start end) str

parsePkgDesc : String -> SourceRule (String, List DescField)
parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
= do exactIdent "package"
name <- unqualifiedName
= do exactProperty "package"
name <- packageName
fields <- many (field fname)
pure (name, fields)

Expand Down Expand Up @@ -425,6 +422,12 @@ clean pkg
delete $ ttFile ++ ".ttc"
delete $ ttFile ++ ".ttm"

getParseErrorLoc : String -> ParseError Token -> 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
ziman marked this conversation as resolved.
Show resolved Hide resolved
getParseErrorLoc fname _ = replFC

-- Just load the 'Main' module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->
Expand Down
Loading