Split Parser.Support

idris2.ipkg

@@ -83,6 +83,8 @@ modules =
     Idris.Version,
 
     Parser.Lexer,
+    Parser.Rule,
+    Parser.Source,
     Parser.Support,
     Parser.Unlit,
 

idris2api.ipkg

@@ -83,6 +83,8 @@ modules =
     Idris.Version,
 
     Parser.Lexer,
+    Parser.Rule,
+    Parser.Source,
     Parser.Support,
     Parser.Unlit,
 

idris2rkt.ipkg

@@ -83,6 +83,8 @@ modules =
     Idris.Version,
 
     Parser.Lexer,
+    Parser.Rule,
+    Parser.Source,
     Parser.Support,
     Parser.Unlit,
 

src/Core/Core.idr

@@ -4,7 +4,7 @@ import Core.Env
 import Core.TT
 import Data.List
 import Data.Vect
-import Parser.Support
+import Parser.Source
 
 import public Data.IORef
 import System

src/Idris/Error.idr

@@ -9,7 +9,7 @@ import Core.Options
 import Idris.Resugar
 import Idris.Syntax
 
-import Parser.Support
+import Parser.Source
 
 import Data.List
 

src/Idris/IDEMode/Parser.idr

@@ -7,7 +7,7 @@ import Idris.IDEMode.Commands
 
 import Text.Parser
 import Parser.Lexer
-import Parser.Support
+import Parser.Source
 import Text.Lexer
 import Utils.Either
 import Utils.String
@@ -21,7 +21,7 @@ import Data.Strings
 symbols : List String
 symbols = ["(", ":", ")"]
 
-ideTokens : TokenMap Token
+ideTokens : TokenMap SourceToken
 ideTokens =
     map (\x => (exact x, Symbol)) symbols ++
     [(digits, \x => Literal (cast x)),
@@ -29,7 +29,7 @@ ideTokens =
      (identAllowDashes, \x => NSIdent [x]),
      (space, Comment)]
 
-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
@@ -38,7 +38,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
@@ -61,7 +61,7 @@ sexp
          pure (SExpList xs)
 
 ideParser : {e : _} ->
-            String -> Grammar (TokenData Token) e ty -> Either ParseError ty
+            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/Package.idr

@@ -24,7 +24,7 @@ import Idris.SetOptions
 import Idris.Syntax
 import Idris.Version
 import Parser.Lexer
-import Parser.Support
+import Parser.Source
 import Utils.Binary
 
 import System

src/Idris/Parser.idr

@@ -2,7 +2,7 @@ module Idris.Parser
 
 import        Core.Options
 import        Idris.Syntax
-import public Parser.Support
+import public Parser.Source
 import        Parser.Lexer
 import        TTImp.TTImp
 

src/Idris/ProcessIdr.idr

@@ -193,7 +193,7 @@ readHeader path
   where
     -- Stop at the first :, that's definitely not part of the header, to
     -- save lexing the whole file unnecessarily
-    isColon : TokenData Token -> Bool
+    isColon : TokenData SourceToken -> Bool
     isColon t
         = case tok t of
                Symbol ":" => True

src/Parser/Lexer.idr

@@ -11,24 +11,25 @@ import Utils.String
 %default total
 
 public export
-data Token = NSIdent (List String)
-           | HoleIdent String
-           | Literal Integer
-           | StrLit String
-           | CharLit String
-           | DoubleLit Double
-           | Symbol String
-           | Keyword String
-           | Unrecognised String
-           | Comment String
-           | DocComment String
-           | CGDirective String
-           | RecordField String
-           | Pragma String
-           | EndInput
+data SourceToken
+  = NSIdent (List String)
+  | HoleIdent String
+  | Literal Integer
+  | StrLit String
+  | CharLit String
+  | DoubleLit Double
+  | Symbol String
+  | Keyword String
+  | Unrecognised String
+  | Comment String
+  | DocComment String
+  | CGDirective String
+  | RecordField String
+  | Pragma String
+  | EndInput
 
 export
-Show Token where
+Show SourceToken where
   show (HoleIdent x) = "hole identifier " ++ x
   show (Literal x) = "literal " ++ show x
   show (StrLit x) = "string " ++ show x
@@ -179,7 +180,7 @@ cgDirective
            is '}')
          <|> many (isNot '\n'))
 
-mkDirective : String -> Token
+mkDirective : String -> SourceToken
 mkDirective str = CGDirective (trim (substr 3 (length str) str))
 
 -- Reserved words
@@ -242,7 +243,7 @@ fromOctLit str
                   Nothing => 0 -- can't happen if the literal lexed correctly
                   Just n => cast n
 
-rawTokens : TokenMap Token
+rawTokens : TokenMap SourceToken
 rawTokens =
     [(comment, Comment),
      (blockComment, Comment),
@@ -264,18 +265,18 @@ rawTokens =
      (validSymbol, Symbol),
      (symbol, Unrecognised)]
   where
-    parseNSIdent : String -> Token
+    parseNSIdent : String -> SourceToken
     parseNSIdent = NSIdent . reverse . split (== '.')
 
-    parseIdent : String -> Token
+    parseIdent : String -> SourceToken
     parseIdent x =
       if x `elem` keywords
         then Keyword x
         else NSIdent [x]
 
 export
-lexTo : (TokenData Token -> Bool) ->
-        String -> Either (Int, Int, String) (List (TokenData Token))
+lexTo : (TokenData SourceToken -> Bool) ->
+        String -> Either (Int, Int, String) (List (TokenData SourceToken))
 lexTo pred str
     = case lexTo pred rawTokens str of
            -- Add the EndInput token so that we'll have a line and column
@@ -284,12 +285,12 @@ lexTo pred 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
                           DocComment _ => False -- TODO!
                           _ => True
 
 export
-lex : String -> Either (Int, Int, String) (List (TokenData Token))
+lex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
 lex = lexTo (const False)

src/Parser/Rule.idr

@@ -0,0 +1,417 @@
+module Parser.Rule
+
+import public Parser.Lexer
+import public Parser.Support
+import public Text.Lexer
+import public Text.Parser
+
+import Core.TT
+
+%default total
+
+public export
+Rule : Type -> Type
+Rule ty = Grammar (TokenData SourceToken) True ty
+
+public export
+EmptyRule : Type -> Type
+EmptyRule ty = Grammar (TokenData SourceToken) False ty
+
+-- Some basic parsers used by all the intermediate forms
+
+export
+location : EmptyRule (Int, Int)
+location
+    = do tok <- peek
+         pure (line tok, col tok)
+
+export
+column : EmptyRule Int
+column
+    = do (line, col) <- location
+         pure col
+
+export
+eoi : EmptyRule ()
+eoi
+    = do nextIs "Expected end of input" (isEOI . tok)
+         pure ()
+  where
+    isEOI : SourceToken -> Bool
+    isEOI EndInput = True
+    isEOI _ = False
+
+export
+constant : Rule Constant
+constant
+    = terminal "Expected constant"
+               (\x => case tok x of
+                           Literal i => Just (BI i)
+                           StrLit s => case escape s of
+                                            Nothing => Nothing
+                                            Just s' => Just (Str s')
+                           CharLit c => case getCharLit c of
+                                             Nothing => Nothing
+                                             Just c' => Just (Ch c')
+                           DoubleLit d => Just (Db d)
+                           NSIdent ["Int"] => Just IntType
+                           NSIdent ["Integer"] => Just IntegerType
+                           NSIdent ["String"] => Just StringType
+                           NSIdent ["Char"] => Just CharType
+                           NSIdent ["Double"] => Just DoubleType
+                           _ => Nothing)
+
+export
+intLit : Rule Integer
+intLit
+    = terminal "Expected integer literal"
+               (\x => case tok x of
+                           Literal i => Just i
+                           _ => Nothing)
+
+export
+strLit : Rule String
+strLit
+    = terminal "Expected string literal"
+               (\x => case tok x of
+                           StrLit s => Just s
+                           _ => Nothing)
+
+export
+recField : Rule Name
+recField
+    = terminal "Expected record field"
+               (\x => case tok x of
+                           RecordField s => Just (RF s)
+                           _ => Nothing)
+
+export
+symbol : String -> Rule ()
+symbol req
+    = terminal ("Expected '" ++ req ++ "'")
+               (\x => case tok x of
+                           Symbol s => if s == req then Just ()
+                                                   else Nothing
+                           _ => Nothing)
+
+export
+keyword : String -> Rule ()
+keyword req
+    = terminal ("Expected '" ++ req ++ "'")
+               (\x => case tok x of
+                           Keyword s => if s == req then Just ()
+                                                    else Nothing
+                           _ => Nothing)
+
+export
+exactIdent : String -> Rule ()
+exactIdent req
+    = terminal ("Expected " ++ req)
+               (\x => case tok x of
+                           NSIdent [s] => if s == req then Just ()
+                                                      else Nothing
+                           _ => Nothing)
+
+export
+pragma : String -> Rule ()
+pragma n =
+  terminal ("Expected pragma " ++ n)
+    (\x => case tok x of
+      Pragma s =>
+        if s == n
+          then Just ()
+          else Nothing
+      _ => Nothing)
+
+export
+operator : Rule Name
+operator
+    = terminal "Expected operator"
+               (\x => case tok x of
+                           Symbol s =>
+                                if s `elem` reservedSymbols
+                                   then Nothing
+                                   else Just (UN s)
+                           _ => Nothing)
+
+identPart : Rule String
+identPart
+    = terminal "Expected name"
+               (\x => case tok x of
+                           NSIdent [str] => Just str
+                           _ => Nothing)
+
+export
+nsIdent : Rule (List String)
+nsIdent
+    = terminal "Expected namespaced name"
+        (\x => case tok x of
+            NSIdent ns => Just ns
+            _ => Nothing)
+
+export
+unqualifiedName : Rule String
+unqualifiedName = identPart
+
+export
+holeName : Rule String
+holeName
+    = terminal "Expected hole name"
+               (\x => case tok x of
+                           HoleIdent str => Just str
+                           _ => Nothing)
+
+reservedNames : List String
+reservedNames
+    = ["Type", "Int", "Integer", "String", "Char", "Double",
+       "Lazy", "Inf", "Force", "Delay"]
+
+export
+name : Rule Name
+name = opNonNS <|> do
+  ns <- nsIdent
+  opNS ns <|> nameNS ns
+ where
+  reserved : String -> Bool
+  reserved n = n `elem` reservedNames
+
+  nameNS : List String -> Grammar (TokenData SourceToken) False Name
+  nameNS [] = pure $ UN "IMPOSSIBLE"
+  nameNS [x] = 
+    if reserved x
+      then fail $ "can't use reserved name " ++ x
+      else pure $ UN x
+  nameNS (x :: xs) =
+    if reserved x
+      then fail $ "can't use reserved name " ++ x
+      else pure $ NS xs (UN x)
+
+  opNonNS : Rule Name
+  opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
+
+  opNS : List String -> Rule Name
+  opNS ns = do
+    symbol ".("
+    n <- (operator <|> recField)
+    symbol ")"
+    pure (NS ns n)
+
+export
+IndentInfo : Type
+IndentInfo = Int
+
+export
+init : IndentInfo
+init = 0
+
+continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
+continueF err indent
+    = do eoi; err
+  <|> do keyword "where"; err
+  <|> do col <- Rule.column
+         if col <= indent
+            then err
+            else pure ()
+
+||| Fail if this is the end of a block entry or end of file
+export
+continue : (indent : IndentInfo) -> EmptyRule ()
+continue = continueF (fail "Unexpected end of expression")
+
+||| As 'continue' but failing is fatal (i.e. entire parse fails)
+export
+mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()
+mustContinue indent Nothing
+   = continueF (fatalError "Unexpected end of expression") indent
+mustContinue indent (Just req)
+   = continueF (fatalError ("Expected '" ++ req ++ "'")) indent
+
+data ValidIndent =
+  |||  In {}, entries can begin in any column
+  AnyIndent |
+  ||| Entry must begin in a specific column
+  AtPos Int |
+  ||| Entry can begin in this column or later
+  AfterPos Int |
+  ||| Block is finished
+  EndOfBlock
+
+Show ValidIndent where
+  show AnyIndent = "[any]"
+  show (AtPos i) = "[col " ++ show i ++ "]"
+  show (AfterPos i) = "[after " ++ show i ++ "]"
+  show EndOfBlock = "[EOB]"
+
+checkValid : ValidIndent -> Int -> EmptyRule ()
+checkValid AnyIndent c = pure ()
+checkValid (AtPos x) c = if c == x
+                            then pure ()
+                            else fail "Invalid indentation"
+checkValid (AfterPos x) c = if c >= x
+                               then pure ()
+                               else fail "Invalid indentation"
+checkValid EndOfBlock c = fail "End of block"
+
+||| Any token which indicates the end of a statement/block
+isTerminator : SourceToken -> Bool
+isTerminator (Symbol ",") = True
+isTerminator (Symbol "]") = True
+isTerminator (Symbol ";") = True
+isTerminator (Symbol "}") = True
+isTerminator (Symbol ")") = True
+isTerminator (Symbol "|") = True
+isTerminator (Keyword "in") = True
+isTerminator (Keyword "then") = True
+isTerminator (Keyword "else") = True
+isTerminator (Keyword "where") = True
+isTerminator EndInput = True
+isTerminator _ = False
+
+||| Check we're at the end of a block entry, given the start column
+||| of the block.
+||| It's the end if we have a terminating token, or the next token starts
+||| in or before indent. Works by looking ahead but not consuming.
+export
+atEnd : (indent : IndentInfo) -> EmptyRule ()
+atEnd indent
+    = eoi
+  <|> do nextIs "Expected end of block" (isTerminator . tok)
+         pure ()
+  <|> do col <- Rule.column
+         if (col <= indent)
+            then pure ()
+            else fail "Not the end of a block entry"
+
+-- Check we're at the end, but only by looking at indentation
+export
+atEndIndent : (indent : IndentInfo) -> EmptyRule ()
+atEndIndent indent
+    = eoi
+  <|> do col <- Rule.column
+         if col <= indent
+            then pure ()
+            else fail "Not the end of a block entry"
+
+
+-- Parse a terminator, return where the next block entry
+-- must start, given where the current block entry started
+terminator : ValidIndent -> Int -> EmptyRule ValidIndent
+terminator valid laststart
+    = do eoi
+         pure EndOfBlock
+  <|> do symbol ";"
+         pure (afterSemi valid)
+  <|> do col <- column
+         afterDedent valid col
+  <|> pure EndOfBlock
+ where
+   -- Expected indentation for the next token can either be anything (if
+   -- we're inside a brace delimited block) or anywhere after the initial
+   -- column (if we're inside an indentation delimited block)
+   afterSemi : ValidIndent -> ValidIndent
+   afterSemi AnyIndent = AnyIndent -- in braces, anything goes
+   afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position
+   afterSemi (AfterPos c) = AfterPos c
+   afterSemi EndOfBlock = EndOfBlock
+
+   -- Expected indentation for the next token can either be anything (if
+   -- we're inside a brace delimited block) or in exactly the initial column
+   -- (if we're inside an indentation delimited block)
+   afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent
+   afterDedent AnyIndent col
+       = if col <= laststart
+            then pure AnyIndent
+            else fail "Not the end of a block entry"
+   afterDedent (AfterPos c) col
+       = if col <= laststart
+            then pure (AtPos c)
+            else fail "Not the end of a block entry"
+   afterDedent (AtPos c) col
+       = if col <= laststart
+            then pure (AtPos c)
+            else fail "Not the end of a block entry"
+   afterDedent EndOfBlock col = pure EndOfBlock
+
+-- Parse an entry in a block
+blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
+             Rule (ty, ValidIndent)
+blockEntry valid rule
+    = do col <- column
+         checkValid valid col
+         p <- rule col
+         valid' <- terminator valid col
+         pure (p, valid')
+
+blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
+               EmptyRule (List ty)
+blockEntries valid rule
+     = do eoi; pure []
+   <|> do res <- blockEntry valid rule
+          ts <- blockEntries (snd res) rule
+          pure (fst res :: ts)
+   <|> pure []
+
+export
+block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)
+block item
+    = do symbol "{"
+         commit
+         ps <- blockEntries AnyIndent item
+         symbol "}"
+         pure ps
+  <|> do col <- column
+         blockEntries (AtPos col) item
+
+
+||| `blockAfter col rule` parses a `rule`-block indented by at
+||| least `col` spaces (unless the block is explicitly delimited
+||| by curly braces). `rule` is a function of the actual indentation
+||| level.
+export
+blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)
+blockAfter mincol item
+    = do symbol "{"
+         commit
+         ps <- blockEntries AnyIndent item
+         symbol "}"
+         pure ps
+  <|> do col <- Rule.column
+         if col <= mincol
+            then pure []
+            else blockEntries (AtPos col) item
+
+export
+blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty)
+blockWithOptHeaderAfter {ty} mincol header item
+    = do symbol "{"
+         commit
+         hidt <- optional $ blockEntry AnyIndent header
+         restOfBlock hidt
+  <|> do col <- Rule.column
+         if col <= mincol
+            then pure (Nothing, [])
+            else do hidt <- optional $ blockEntry (AtPos col) header
+                    ps <- blockEntries (AtPos col) item
+                    pure (map fst hidt, ps)
+  where
+  restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
+  restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
+                                   symbol "}"
+                                   pure (Just h, ps)
+  restOfBlock Nothing = do ps <- blockEntries AnyIndent item
+                           symbol "}"
+                           pure (Nothing, ps)
+
+export
+nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
+nonEmptyBlock item
+    = do symbol "{"
+         commit
+         res <- blockEntry AnyIndent item
+         ps <- blockEntries (snd res) item
+         symbol "}"
+         pure (fst res :: ps)
+  <|> do col <- column
+         res <- blockEntry (AtPos col) item
+         ps <- blockEntries (snd res) item
+         pure (fst res :: ps)

src/Parser/Source.idr

@@ -0,0 +1,34 @@
+module Parser.Source
+
+import public Parser.Lexer
+import public Parser.Rule
+import public Parser.Unlit
+import public Text.Lexer
+import public Text.Parser
+
+import System.File
+import Utils.Either
+
+%default total
+
+export
+runParserTo : {e : _} ->
+              Maybe LiterateStyle -> (TokenData SourceToken -> Bool) ->
+              String -> Grammar (TokenData SourceToken) e ty -> Either ParseError 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
+         Right (fst parsed)
+
+export
+runParser : {e : _} ->
+            Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
+runParser lit = runParserTo lit (const False)
+
+export
+parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
+parseFile fn p
+    = do Right str <- readFile fn
+             | Left err => pure (Left (FileFail err))
+         pure (runParser (isLitFile fn) str p)

src/Parser/Support.idr

@@ -1,28 +1,19 @@
 module Parser.Support
 
-import public Text.Lexer
 import public Parser.Lexer
-import public Parser.Unlit
+import public Text.Lexer
 import public Text.Parser
 
 import Core.TT
 import Data.List
 import Data.List.Views
-import Utils.Either
+import Parser.Unlit
 import System.File
 
 %default total
 
 public export
-Rule : Type -> Type
-Rule ty = Grammar (TokenData Token) True ty
-
-public export
-EmptyRule : Type -> Type
-EmptyRule ty = Grammar (TokenData Token) False ty
-
-public export
-data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
+data ParseError = ParseFail String (Maybe (Int, Int)) (List SourceToken)
                 | LexFail (Int, Int, String)
                 | FileFail FileError
                 | LitFail LiterateError
@@ -40,57 +31,11 @@ Show ParseError where
       = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str
 
 export
-eoi : EmptyRule ()
-eoi
-    = do nextIs "Expected end of input" (isEOI . tok)
-         pure ()
-  where
-    isEOI : Token -> Bool
-    isEOI EndInput = True
-    isEOI _ = False
-
-export
-mapParseError : ParseError (TokenData Token) -> ParseError
+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))
 
 export
-runParserTo : {e : _} ->
-              Maybe LiterateStyle -> (TokenData Token -> Bool) ->
-              String -> Grammar (TokenData Token) e ty -> Either ParseError 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
-         Right (fst parsed)
-
-export
-runParser : {e : _} ->
-            Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty
-runParser lit = runParserTo lit (const False)
-
-export
-parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
-parseFile fn p
-    = do Right str <- readFile fn
-             | Left err => pure (Left (FileFail err))
-         pure (runParser (isLitFile fn) str p)
-
-
--- Some basic parsers used by all the intermediate forms
-
-export
-location : EmptyRule (Int, Int)
-location
-    = do tok <- peek
-         pure (line tok, col tok)
-
-export
-column : EmptyRule Int
-column
-    = do (line, col) <- location
-         pure col
-
 hex : Char -> Maybe Int
 hex '0' = Just 0
 hex '1' = Just 1
@@ -110,6 +55,7 @@ hex 'e' = Just 14
 hex 'f' = Just 15
 hex _ = Nothing
 
+export
 dec : Char -> Maybe Int
 dec '0' = Just 0
 dec '1' = Just 1
@@ -123,6 +69,7 @@ dec '8' = Just 8
 dec '9' = Just 9
 dec _ = Nothing
 
+export
 oct : Char -> Maybe Int
 oct '0' = Just 0
 oct '1' = Just 1
@@ -134,6 +81,7 @@ oct '6' = Just 6
 oct '7' = Just 7
 oct _ = Nothing
 
+export
 getEsc : String -> Maybe Char
 getEsc "NUL" = Just '\NUL'
 getEsc "SOH" = Just '\SOH'
@@ -221,9 +169,11 @@ escape' ('\\' :: xs)
                                  !(assert_total (escape' rest))
 escape' (x :: xs) = Just $ x :: !(escape' xs)
 
+export
 escape : String -> Maybe String
 escape x = pure $ pack !(escape' (unpack x))
 
+export
 getCharLit : String -> Maybe Char
 getCharLit str
    = do e <- escape str
@@ -232,382 +182,3 @@ getCharLit str
            else if length e == 0 -- parsed the NULL character that terminated the string!
                    then Just '\0000'
                    else Nothing
-
-export
-constant : Rule Constant
-constant
-    = terminal "Expected constant"
-               (\x => case tok x of
-                           Literal i => Just (BI i)
-                           StrLit s => case escape s of
-                                            Nothing => Nothing
-                                            Just s' => Just (Str s')
-                           CharLit c => case getCharLit c of
-                                             Nothing => Nothing
-                                             Just c' => Just (Ch c')
-                           DoubleLit d => Just (Db d)
-                           NSIdent ["Int"] => Just IntType
-                           NSIdent ["Integer"] => Just IntegerType
-                           NSIdent ["String"] => Just StringType
-                           NSIdent ["Char"] => Just CharType
-                           NSIdent ["Double"] => Just DoubleType
-                           _ => Nothing)
-
-export
-intLit : Rule Integer
-intLit
-    = terminal "Expected integer literal"
-               (\x => case tok x of
-                           Literal i => Just i
-                           _ => Nothing)
-
-export
-strLit : Rule String
-strLit
-    = terminal "Expected string literal"
-               (\x => case tok x of
-                           StrLit s => Just s
-                           _ => Nothing)
-
-export
-recField : Rule Name
-recField
-    = terminal "Expected record field"
-               (\x => case tok x of
-                           RecordField s => Just (RF s)
-                           _ => Nothing)
-
-export
-symbol : String -> Rule ()
-symbol req
-    = terminal ("Expected '" ++ req ++ "'")
-               (\x => case tok x of
-                           Symbol s => if s == req then Just ()
-                                                   else Nothing
-                           _ => Nothing)
-
-export
-keyword : String -> Rule ()
-keyword req
-    = terminal ("Expected '" ++ req ++ "'")
-               (\x => case tok x of
-                           Keyword s => if s == req then Just ()
-                                                    else Nothing
-                           _ => Nothing)
-
-export
-exactIdent : String -> Rule ()
-exactIdent req
-    = terminal ("Expected " ++ req)
-               (\x => case tok x of
-                           NSIdent [s] => if s == req then Just ()
-                                                      else Nothing
-                           _ => Nothing)
-
-export
-pragma : String -> Rule ()
-pragma n =
-  terminal ("Expected pragma " ++ n)
-    (\x => case tok x of
-      Pragma s =>
-        if s == n
-          then Just ()
-          else Nothing
-      _ => Nothing)
-
-export
-operator : Rule Name
-operator
-    = terminal "Expected operator"
-               (\x => case tok x of
-                           Symbol s =>
-                                if s `elem` reservedSymbols
-                                   then Nothing
-                                   else Just (UN s)
-                           _ => Nothing)
-
-identPart : Rule String
-identPart
-    = terminal "Expected name"
-               (\x => case tok x of
-                           NSIdent [str] => Just str
-                           _ => Nothing)
-
-%hide Prelude.(>>=)
-
-export
-nsIdent : Rule (List String)
-nsIdent
-    = terminal "Expected namespaced name"
-        (\x => case tok x of
-            NSIdent ns => Just ns
-            _ => Nothing)
-
-export
-unqualifiedName : Rule String
-unqualifiedName = identPart
-
-export
-holeName : Rule String
-holeName
-    = terminal "Expected hole name"
-               (\x => case tok x of
-                           HoleIdent str => Just str
-                           _ => Nothing)
-
-reservedNames : List String
-reservedNames
-    = ["Type", "Int", "Integer", "String", "Char", "Double",
-       "Lazy", "Inf", "Force", "Delay"]
-
-export
-name : Rule Name
-name = opNonNS <|> do
-  ns <- nsIdent
-  opNS ns <|> nameNS ns
- where
-  reserved : String -> Bool
-  reserved n = n `elem` reservedNames
-
-  nameNS : List String -> Grammar (TokenData Token) False Name
-  nameNS [] = pure $ UN "IMPOSSIBLE"
-  nameNS [x] = 
-    if reserved x
-      then fail $ "can't use reserved name " ++ x
-      else pure $ UN x
-  nameNS (x :: xs) =
-    if reserved x
-      then fail $ "can't use reserved name " ++ x
-      else pure $ NS xs (UN x)
-
-  opNonNS : Rule Name
-  opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
-
-  opNS : List String -> Rule Name
-  opNS ns = do
-    symbol ".("
-    n <- (operator <|> recField)
-    symbol ")"
-    pure (NS ns n)
-
-export
-IndentInfo : Type
-IndentInfo = Int
-
-export
-init : IndentInfo
-init = 0
-
-%hide Prelude.pure
-
-continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
-continueF err indent
-    = do eoi; err
-  <|> do keyword "where"; err
-  <|> do col <- Support.column
-         if col <= indent
-            then err
-            else pure ()
-
-||| Fail if this is the end of a block entry or end of file
-export
-continue : (indent : IndentInfo) -> EmptyRule ()
-continue = continueF (fail "Unexpected end of expression")
-
-||| As 'continue' but failing is fatal (i.e. entire parse fails)
-export
-mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()
-mustContinue indent Nothing
-   = continueF (fatalError "Unexpected end of expression") indent
-mustContinue indent (Just req)
-   = continueF (fatalError ("Expected '" ++ req ++ "'")) indent
-
-data ValidIndent =
-  |||  In {}, entries can begin in any column
-  AnyIndent |
-  ||| Entry must begin in a specific column
-  AtPos Int |
-  ||| Entry can begin in this column or later
-  AfterPos Int |
-  ||| Block is finished
-  EndOfBlock
-
-Show ValidIndent where
-  show AnyIndent = "[any]"
-  show (AtPos i) = "[col " ++ show i ++ "]"
-  show (AfterPos i) = "[after " ++ show i ++ "]"
-  show EndOfBlock = "[EOB]"
-
-checkValid : ValidIndent -> Int -> EmptyRule ()
-checkValid AnyIndent c = pure ()
-checkValid (AtPos x) c = if c == x
-                            then pure ()
-                            else fail "Invalid indentation"
-checkValid (AfterPos x) c = if c >= x
-                               then pure ()
-                               else fail "Invalid indentation"
-checkValid EndOfBlock c = fail "End of block"
-
-||| Any token which indicates the end of a statement/block
-isTerminator : Token -> Bool
-isTerminator (Symbol ",") = True
-isTerminator (Symbol "]") = True
-isTerminator (Symbol ";") = True
-isTerminator (Symbol "}") = True
-isTerminator (Symbol ")") = True
-isTerminator (Symbol "|") = True
-isTerminator (Keyword "in") = True
-isTerminator (Keyword "then") = True
-isTerminator (Keyword "else") = True
-isTerminator (Keyword "where") = True
-isTerminator EndInput = True
-isTerminator _ = False
-
-||| Check we're at the end of a block entry, given the start column
-||| of the block.
-||| It's the end if we have a terminating token, or the next token starts
-||| in or before indent. Works by looking ahead but not consuming.
-export
-atEnd : (indent : IndentInfo) -> EmptyRule ()
-atEnd indent
-    = eoi
-  <|> do nextIs "Expected end of block" (isTerminator . tok)
-         pure ()
-  <|> do col <- Support.column
-         if (col <= indent) 
-            then pure ()
-            else fail "Not the end of a block entry"
-
--- Check we're at the end, but only by looking at indentation
-export
-atEndIndent : (indent : IndentInfo) -> EmptyRule ()
-atEndIndent indent
-    = eoi
-  <|> do col <- Support.column
-         if col <= indent
-            then pure ()
-            else fail "Not the end of a block entry"
-
-
--- Parse a terminator, return where the next block entry
--- must start, given where the current block entry started
-terminator : ValidIndent -> Int -> EmptyRule ValidIndent
-terminator valid laststart
-    = do eoi
-         pure EndOfBlock
-  <|> do symbol ";"
-         pure (afterSemi valid)
-  <|> do col <- column
-         afterDedent valid col
-  <|> pure EndOfBlock
- where
-   -- Expected indentation for the next token can either be anything (if
-   -- we're inside a brace delimited block) or anywhere after the initial
-   -- column (if we're inside an indentation delimited block)
-   afterSemi : ValidIndent -> ValidIndent
-   afterSemi AnyIndent = AnyIndent -- in braces, anything goes
-   afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position
-   afterSemi (AfterPos c) = AfterPos c
-   afterSemi EndOfBlock = EndOfBlock
-
-   -- Expected indentation for the next token can either be anything (if
-   -- we're inside a brace delimited block) or in exactly the initial column
-   -- (if we're inside an indentation delimited block)
-   afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent
-   afterDedent AnyIndent col
-       = if col <= laststart
-            then pure AnyIndent
-            else fail "Not the end of a block entry"
-   afterDedent (AfterPos c) col
-       = if col <= laststart
-            then pure (AtPos c)
-            else fail "Not the end of a block entry"
-   afterDedent (AtPos c) col
-       = if col <= laststart
-            then pure (AtPos c)
-            else fail "Not the end of a block entry"
-   afterDedent EndOfBlock col = pure EndOfBlock
-
--- Parse an entry in a block
-blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
-             Rule (ty, ValidIndent)
-blockEntry valid rule
-    = do col <- column
-         checkValid valid col
-         p <- rule col
-         valid' <- terminator valid col
-         pure (p, valid')
-
-blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
-               EmptyRule (List ty)
-blockEntries valid rule
-     = do eoi; pure []
-   <|> do res <- blockEntry valid rule
-          ts <- blockEntries (snd res) rule
-          pure (fst res :: ts)
-   <|> pure []
-
-export
-block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)
-block item
-    = do symbol "{"
-         commit
-         ps <- blockEntries AnyIndent item
-         symbol "}"
-         pure ps
-  <|> do col <- column
-         blockEntries (AtPos col) item
-
-
-||| `blockAfter col rule` parses a `rule`-block indented by at
-||| least `col` spaces (unless the block is explicitly delimited
-||| by curly braces). `rule` is a function of the actual indentation
-||| level.
-export
-blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)
-blockAfter mincol item
-    = do symbol "{"
-         commit
-         ps <- blockEntries AnyIndent item
-         symbol "}"
-         pure ps
-  <|> do col <- Support.column
-         if col <= mincol
-            then pure []
-            else blockEntries (AtPos col) item
-
-export
-blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty)
-blockWithOptHeaderAfter {ty} mincol header item
-    = do symbol "{"
-         commit
-         hidt <- optional $ blockEntry AnyIndent header
-         restOfBlock hidt
-  <|> do col <- Support.column
-         if col <= mincol
-            then pure (Nothing, [])
-            else do hidt <- optional $ blockEntry (AtPos col) header
-                    ps <- blockEntries (AtPos col) item
-                    pure (map fst hidt, ps)
-  where
-  restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
-  restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
-                                   symbol "}"
-                                   pure (Just h, ps)
-  restOfBlock Nothing = do ps <- blockEntries AnyIndent item
-                           symbol "}"
-                           pure (Nothing, ps)
-
-export
-nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
-nonEmptyBlock item
-    = do symbol "{"
-         commit
-         res <- blockEntry AnyIndent item
-         ps <- blockEntries (snd res) item
-         symbol "}"
-         pure (fst res :: ps)
-  <|> do col <- column
-         res <- blockEntry (AtPos col) item
-         ps <- blockEntries (snd res) item
-         pure (fst res :: ps)

src/TTImp/Parser.idr

@@ -4,7 +4,7 @@ import Core.Context
 import Core.Core
 import Core.Env
 import Core.TT
-import Parser.Support
+import Parser.Source
 import TTImp.TTImp
 
 import public Text.Parser

src/TTImp/ProcessDecls.idr

@@ -6,7 +6,7 @@ import Core.Env
 import Core.Metadata
 import Core.UnifyState
 
-import Parser.Support
+import Parser.Source
 
 import TTImp.BindImplicits
 import TTImp.Elab.Check

src/Yaffle/Main.idr

@@ -1,6 +1,6 @@
 module Yaffle.Main
 
-import Parser.Support
+import Parser.Source
 
 import Core.Binary
 import Core.Context

src/Yaffle/REPL.idr

@@ -21,7 +21,7 @@ import TTImp.ProcessDecls
 import TTImp.TTImp
 import TTImp.Unelab
 
-import Parser.Support
+import Parser.Source
 
 %default covering