Split Lexer/Parser into two: Source(.idr) and Package(.ipkg)

idris2.ipkg

@@ -80,7 +80,14 @@ modules =
     Idris.Syntax,
     Idris.Version,
 
-    Parser.Lexer,
+    Parser.Lexer.Common,
+    Parser.Lexer.Source,
+    Parser.Lexer.Package,
+    Parser.Rules.Common,
+    Parser.Rules.Source,
+    Parser.Rules.Package,
+    Parser.Package,
+    Parser.Source,
     Parser.Support,
     Parser.Unlit,
 

idris2api.ipkg

@@ -76,7 +76,14 @@ modules =
     Idris.Syntax,
     Idris.Version,
 
-    Parser.Lexer,
+    Parser.Lexer.Common,
+    Parser.Lexer.Source,
+    Parser.Lexer.Package,
+    Parser.Rules.Common,
+    Parser.Rules.Source,
+    Parser.Rules.Package,
+    Parser.Package,
+    Parser.Source,
     Parser.Support,
     Parser.Unlit,
 

src/Core/Core.idr

@@ -1,12 +1,13 @@
 module Core.Core
 
+import public Control.Catchable
+import public Data.IORef
+
 import Core.Env
 import Core.TT
-import Data.Vect
-import Parser.Support
 
-import public Control.Catchable
-import public Data.IORef
+import Data.Vect
+import Parser.Source
 import System
 
 %default covering
@@ -94,7 +95,7 @@ data Error
     | GenericMsg FC String
     | TTCError TTCErrorMsg
     | FileErr String FileError
-    | ParseFail FC ParseError
+    | ParseFail FC (ParsingError SourceToken)
     | ModuleNotFound FC (List String)
     | CyclicImports (List (List String))
     | ForceNeeded

src/Core/Primitives.idr

@@ -32,7 +32,9 @@ unaryOp _ _ = Nothing
 castString : Vect 1 (NF vars) -> Maybe (NF vars)
 castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))
 castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))
-castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))
+castString [NPrimVal fc (Ch i)] = case isLTE 2 (length $ show i) of
+                                       Yes prf => Just $ NPrimVal fc (Str $ stripQuotes $ show i)
+                                       No  _   => Nothing
 castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))
 castString _ = Nothing
 

src/Idris/Desugar.idr

@@ -17,7 +17,7 @@ import Idris.Syntax
 import Idris.Elab.Implementation
 import Idris.Elab.Interface
 
-import Parser.Lexer
+import Parser.Lexer.Source
 
 import TTImp.BindImplicits
 import TTImp.Parser

src/Idris/Error.idr

@@ -9,7 +9,7 @@ import Core.Options
 import Idris.Resugar
 import Idris.Syntax
 
-import Parser.Support
+import Parser.Source
 
 %default covering
 

src/Idris/IDEMode/CaseSplit.idr

@@ -6,7 +6,7 @@ import Core.Metadata
 import Core.TT
 import Core.Value
 
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Unlit
 
 import TTImp.Interactive.CaseSplit

src/Idris/IDEMode/MakeClause.idr

@@ -1,7 +1,7 @@
 module Idris.IDEMode.MakeClause
 
 import Core.Name
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Unlit
 
 -- Implement make-with and make-case from the IDE mode

src/Idris/IDEMode/Parser.idr

@@ -6,26 +6,28 @@ module Idris.IDEMode.Parser
 import Idris.IDEMode.Commands
 
 import Text.Parser
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Support
 import Text.Lexer
 import Utils.Either
 import Utils.String
 
-%hide Lexer.symbols
+%hide Lexer.Source.symbols
 
-symbols : List String
-symbols = ["(", ":", ")"]
-
-ideTokens : TokenMap Token
+ideTokens : TokenMap SourceToken
 ideTokens =
     map (\x => (exact x, Symbol)) symbols ++
-    [(digits, \x => Literal (cast x)),
-     (stringLit, \x => StrLit (stripQuotes x)),
+    [(digits, \x => IntegerLit (cast x)),
+     (stringLit, \x => case (isLTE 2 $ length x) of
+                            Yes prf => StringLit (stripQuotes x)
+                            No  _   => Unrecognised x),
      (identAllowDashes, \x => NSIdent [x]),
      (space, Comment)]
+  where
+    symbols : List String
+    symbols = ["(", ":", ")"]
 
-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
@@ -34,7 +36,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
@@ -56,7 +58,7 @@ sexp
          symbol ")"
          pure (SExpList xs)
 
-ideParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty
+ideParser : String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
 ideParser str p
     = do toks   <- mapError LexFail $ idelex str
          parsed <- mapError mapParseError $ parse p toks

src/Idris/IDEMode/TokenLine.idr

@@ -1,7 +1,7 @@
 ||| Tokenise a source line for easier processing
 module Idris.IDEMode.TokenLine
 
-import Parser.Lexer
+import Parser.Lexer.Source
 import Text.Lexer
 
 public export

src/Idris/Package.idr

@@ -21,8 +21,7 @@ import Idris.REPLOpts
 import Idris.SetOptions
 import Idris.Syntax
 import Idris.Version
-import Parser.Lexer
-import Parser.Support
+import Parser.Package
 import Utils.Binary
 
 import System
@@ -111,7 +110,7 @@ data DescField : Type where
   PPreclean    : FC -> String -> DescField
   PPostclean   : FC -> String -> DescField
 
-field : String -> Rule DescField
+field : String -> PackageRule DescField
 field fname
       = strField PVersion "version"
     <|> strField PAuthors "authors"
@@ -131,42 +130,41 @@ field fname
     <|> strField PPostinstall "postinstall"
     <|> strField PPreclean "preclean"
     <|> strField PPostclean "postclean"
-    <|> do exactIdent "depends"; symbol "="
+    <|> do property "depends"; assignment
            ds <- sepBy1 (symbol ",") unqualifiedName
            pure (PDepends ds)
-    <|> do exactIdent "modules"; symbol "="
+    <|> do property "modules"; assignment
            ms <- sepBy1 (symbol ",")
-                      (do start <- location
+                      (do start <- location PackageToken
                           ns <- nsIdent
-                          end <- location
+                          end <- location PackageToken
                           pure (MkFC fname start end, ns))
            pure (PModules ms)
-    <|> do exactIdent "main"; symbol "="
-           start <- location
+    <|> do property "main"; assignment
+           start <- location PackageToken
            m <- nsIdent
-           end <- location
+           end <- location PackageToken
            pure (PMainMod (MkFC fname start end) m)
-    <|> do exactIdent "executable"; symbol "="
+    <|> do property "executable"; assignment
            e <- unqualifiedName
            pure (PExec e)
   where
     getStr : (FC -> String -> DescField) -> FC ->
-             String -> Constant -> EmptyRule DescField
-    getStr p fc fld (Str s) = pure (p fc s)
-    getStr p fc fld _ = fail $ fld ++ " field must be a string"
+             String -> String -> EmptyPackageRule DescField
+    getStr p fc fld s = pure (p fc s)
 
-    strField : (FC -> String -> DescField) -> String -> Rule DescField
+    strField : (FC -> String -> DescField) -> String -> PackageRule DescField
     strField p f
-        = do start <- location
-             exactIdent f
-             symbol "="
-             c <- constant
-             end <- location
+        = do start <- location PackageToken
+             property f
+             assignment
+             c <- string
+             end <- location PackageToken
              getStr p (MkFC fname start end) f c
 
-parsePkgDesc : String -> Rule (String, List DescField)
+parsePkgDesc : String -> PackageRule (String, List DescField)
 parsePkgDesc fname
-    = do exactIdent "package"
+    = do property "package"
          name <- unqualifiedName
          fields <- many (field fname)
          pure (name, fields)
@@ -432,9 +430,9 @@ processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  PkgCommand -> String -> Core ()
 processPackage cmd file
-    = do Right (pname, fs) <- coreLift $ parseFile file
+    = do Right (pname, fs) <- coreLift $ parsePackageFile file
                                   (do desc <- parsePkgDesc file
-                                      eoi
+                                      eof
                                       pure desc)
              | Left err => throw (ParseFail (getParseErrorLoc file err) err)
          pkg <- addFields fs (initPkgDesc pname)
@@ -478,9 +476,9 @@ findIpkg fname
    = do Just (dir, ipkgn, up) <- coreLift findIpkgFile
              | Nothing => pure fname
         coreLift $ changeDir dir
-        Right (pname, fs) <- coreLift $ parseFile ipkgn
+        Right (pname, fs) <- coreLift $ parsePackageFile ipkgn
                                  (do desc <- parsePkgDesc ipkgn
-                                     eoi
+                                     eof
                                      pure desc)
               | Left err => throw (ParseFail (getParseErrorLoc ipkgn err) err)
         pkg <- addFields fs (initPkgDesc pname)