Create Package Specific Lexer/Rules and Refactor Idris/Package

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,

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,

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,

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

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)

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} ->

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)

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)

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')

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

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
 

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)