Skip to content

Commit

Permalink
Merge pull request #113 from LibreCybernetics/split-parser-2
Browse files Browse the repository at this point in the history
Split Source and Package Parser (Part 2)
  • Loading branch information
ziman committed May 24, 2020
2 parents 1ea54e7 + 731a416 commit 730726c
Show file tree
Hide file tree
Showing 20 changed files with 538 additions and 349 deletions.
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
= 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
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

0 comments on commit 730726c

Please sign in to comment.