module Agda.Syntax.Parser
    ( -- * Types
      Parser
      -- * Parse functions
    , Agda.Syntax.Parser.parse
    , Agda.Syntax.Parser.parsePosString
    , parseFile
      -- * Parsers
    , moduleParser
    , moduleNameParser
    , acceptableFileExts
    , exprParser
    , exprWhereParser
    , holeContentParser
    , tokensParser
      -- * Reading files.
    , readFilePM
      -- * Parse errors
    , ParseError(..)
    , ParseWarning(..)
    , PM(..)
    , runPMIO
    ) where

import Control.Exception
import Control.Monad          ( forM_ )
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.IO.Class ( MonadIO(..) )

import Data.Bifunctor
import qualified Data.List as List
import Data.Text.Lazy (Text)

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Parser.Monad as M hiding (Parser, parseFlags)
import qualified Agda.Syntax.Parser.Monad as M
import qualified Agda.Syntax.Parser.Parser as P
import Agda.Syntax.Parser.Lexer
import Agda.Syntax.Parser.Literate
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Attribute
import Agda.Syntax.Parser.Tokens

import Agda.Utils.FileName
import Agda.Utils.IO.UTF8 (readTextFile)
import Agda.Utils.Maybe   (forMaybe)
import qualified Agda.Utils.Maybe.Strict as Strict

------------------------------------------------------------------------
-- Wrapping parse results

-- | A monad for handling parse errors and warnings.

newtype PM a = PM { forall a. PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a }
  deriving ( (forall a b. (a -> b) -> PM a -> PM b)
-> (forall a b. a -> PM b -> PM a) -> Functor PM
forall a b. a -> PM b -> PM a
forall a b. (a -> b) -> PM a -> PM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> PM a -> PM b
fmap :: forall a b. (a -> b) -> PM a -> PM b
$c<$ :: forall a b. a -> PM b -> PM a
<$ :: forall a b. a -> PM b -> PM a
Functor, Functor PM
Functor PM =>
(forall a. a -> PM a)
-> (forall a b. PM (a -> b) -> PM a -> PM b)
-> (forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c)
-> (forall a b. PM a -> PM b -> PM b)
-> (forall a b. PM a -> PM b -> PM a)
-> Applicative PM
forall a. a -> PM a
forall a b. PM a -> PM b -> PM a
forall a b. PM a -> PM b -> PM b
forall a b. PM (a -> b) -> PM a -> PM b
forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> PM a
pure :: forall a. a -> PM a
$c<*> :: forall a b. PM (a -> b) -> PM a -> PM b
<*> :: forall a b. PM (a -> b) -> PM a -> PM b
$cliftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
liftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
$c*> :: forall a b. PM a -> PM b -> PM b
*> :: forall a b. PM a -> PM b -> PM b
$c<* :: forall a b. PM a -> PM b -> PM a
<* :: forall a b. PM a -> PM b -> PM a
Applicative, Applicative PM
Applicative PM =>
(forall a b. PM a -> (a -> PM b) -> PM b)
-> (forall a b. PM a -> PM b -> PM b)
-> (forall a. a -> PM a)
-> Monad PM
forall a. a -> PM a
forall a b. PM a -> PM b -> PM b
forall a b. PM a -> (a -> PM b) -> PM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. PM a -> (a -> PM b) -> PM b
>>= :: forall a b. PM a -> (a -> PM b) -> PM b
$c>> :: forall a b. PM a -> PM b -> PM b
>> :: forall a b. PM a -> PM b -> PM b
$creturn :: forall a. a -> PM a
return :: forall a. a -> PM a
Monad, Monad PM
Monad PM => (forall a. IO a -> PM a) -> MonadIO PM
forall a. IO a -> PM a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> PM a
liftIO :: forall a. IO a -> PM a
MonadIO
           , MonadError ParseError, MonadState [ParseWarning]
           )

-- | Run a 'PM' computation, returning a list of warnings in first-to-last order
--   and either a parse error or the parsed thing.

runPMIO :: (MonadIO m) => PM a -> m (Either ParseError a, [ParseWarning])
runPMIO :: forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO = IO (Either ParseError a, [ParseWarning])
-> m (Either ParseError a, [ParseWarning])
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either ParseError a, [ParseWarning])
 -> m (Either ParseError a, [ParseWarning]))
-> (PM a -> IO (Either ParseError a, [ParseWarning]))
-> PM a
-> m (Either ParseError a, [ParseWarning])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Either ParseError a, [ParseWarning])
 -> (Either ParseError a, [ParseWarning]))
-> IO (Either ParseError a, [ParseWarning])
-> IO (Either ParseError a, [ParseWarning])
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([ParseWarning] -> [ParseWarning])
-> (Either ParseError a, [ParseWarning])
-> (Either ParseError a, [ParseWarning])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [ParseWarning] -> [ParseWarning]
forall a. [a] -> [a]
reverse) (IO (Either ParseError a, [ParseWarning])
 -> IO (Either ParseError a, [ParseWarning]))
-> (PM a -> IO (Either ParseError a, [ParseWarning]))
-> PM a
-> IO (Either ParseError a, [ParseWarning])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT [ParseWarning] IO (Either ParseError a)
 -> [ParseWarning] -> IO (Either ParseError a, [ParseWarning]))
-> [ParseWarning]
-> StateT [ParseWarning] IO (Either ParseError a)
-> IO (Either ParseError a, [ParseWarning])
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT [ParseWarning] IO (Either ParseError a)
-> [ParseWarning] -> IO (Either ParseError a, [ParseWarning])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT [] (StateT [ParseWarning] IO (Either ParseError a)
 -> IO (Either ParseError a, [ParseWarning]))
-> (PM a -> StateT [ParseWarning] IO (Either ParseError a))
-> PM a
-> IO (Either ParseError a, [ParseWarning])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT ParseError (StateT [ParseWarning] IO) a
-> StateT [ParseWarning] IO (Either ParseError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT ParseError (StateT [ParseWarning] IO) a
 -> StateT [ParseWarning] IO (Either ParseError a))
-> (PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a)
-> PM a
-> StateT [ParseWarning] IO (Either ParseError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
forall a. PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
unPM

-- | Add a 'ParseWarning'.

warning :: ParseWarning -> PM ()
warning :: ParseWarning -> PM ()
warning ParseWarning
w = ExceptT ParseError (StateT [ParseWarning] IO) () -> PM ()
forall a. ExceptT ParseError (StateT [ParseWarning] IO) a -> PM a
PM (([ParseWarning] -> [ParseWarning])
-> ExceptT ParseError (StateT [ParseWarning] IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (ParseWarning
wParseWarning -> [ParseWarning] -> [ParseWarning]
forall a. a -> [a] -> [a]
:))

-- | Embed a 'ParseResult' as 'PM' computation.

wrap :: ParseResult a -> PM (a, Attributes)
wrap :: forall a. ParseResult a -> PM (a, Attributes)
wrap (ParseFailed ParseError
err)  = ParseError -> PM (a, Attributes)
forall a. ParseError -> PM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ParseError
err
wrap (ParseOk ParseState
s a
x)      = do
  ([ParseWarning] -> [ParseWarning]) -> PM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (ParseState -> [ParseWarning]
parseWarnings ParseState
s [ParseWarning] -> [ParseWarning] -> [ParseWarning]
forall a. [a] -> [a] -> [a]
++)
  (a, Attributes) -> PM (a, Attributes)
forall a. a -> PM a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, ParseState -> Attributes
parseAttributes ParseState
s)

wrapM :: IO (ParseResult a) -> PM (a, Attributes)
wrapM :: forall a. IO (ParseResult a) -> PM (a, Attributes)
wrapM IO (ParseResult a)
m = IO (ParseResult a) -> PM (ParseResult a)
forall a. IO a -> PM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (ParseResult a)
m PM (ParseResult a)
-> (ParseResult a -> PM (a, Attributes)) -> PM (a, Attributes)
forall a b. PM a -> (a -> PM b) -> PM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ParseResult a -> PM (a, Attributes)
forall a. ParseResult a -> PM (a, Attributes)
wrap

-- | Returns the contents of the given file.

readFilePM :: RangeFile -> PM Text
readFilePM :: RangeFile -> PM Text
readFilePM RangeFile
file =
  (IOError -> ParseError) -> IO Text -> PM Text
forall e (m :: * -> *) a.
(MonadError e m, MonadIO m) =>
(IOError -> e) -> IO a -> m a
wrapIOM (RangeFile -> IOError -> ParseError
ReadFileError RangeFile
file) (IO Text -> PM Text) -> IO Text -> PM Text
forall a b. (a -> b) -> a -> b
$
  String -> IO Text
readTextFile (AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ RangeFile -> AbsolutePath
rangeFilePath RangeFile
file)

wrapIOM :: (MonadError e m, MonadIO m) => (IOError -> e) -> IO a -> m a
wrapIOM :: forall e (m :: * -> *) a.
(MonadError e m, MonadIO m) =>
(IOError -> e) -> IO a -> m a
wrapIOM IOError -> e
f IO a
m = do
  Either IOError a
a <- IO (Either IOError a) -> m (Either IOError a)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either IOError a) -> m (Either IOError a))
-> IO (Either IOError a) -> m (Either IOError a)
forall a b. (a -> b) -> a -> b
$ (a -> Either IOError a
forall a b. b -> Either a b
Right (a -> Either IOError a) -> IO a -> IO (Either IOError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO a
m) IO (Either IOError a)
-> (IOError -> IO (Either IOError a)) -> IO (Either IOError a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\ IOError
err -> Either IOError a -> IO (Either IOError a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IOError a -> IO (Either IOError a))
-> Either IOError a -> IO (Either IOError a)
forall a b. (a -> b) -> a -> b
$ IOError -> Either IOError a
forall a b. a -> Either a b
Left (IOError
err :: IOError))
  case Either IOError a
a of
    Right a
x  -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    Left IOError
err -> e -> m a
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (IOError -> e
f IOError
err)

------------------------------------------------------------------------
-- Parse functions

-- | Wrapped Parser type.

data Parser a = Parser
  { forall a. Parser a -> Parser a
parser         :: M.Parser a
  , forall a. Parser a -> ParseFlags
parseFlags     :: ParseFlags
  , forall a. Parser a -> LiterateParser a
parseLiterate  :: LiterateParser a
  }

type LiterateParser a =
  Parser a -> [Layer] -> PM (a, Attributes)

-- | Initial state for lexing.

normalLexState :: [LexState]
normalLexState :: [LexState]
normalLexState = [LexState
normal]

-- | Initial state for lexing with top-level layout.

layoutLexState :: [LexState]
layoutLexState :: [LexState]
layoutLexState = [LexState
layout, LexState
normal]

-- | Parse without top-level layout.

parse :: Parser a -> String -> PM (a, Attributes)
parse :: forall a. Parser a -> String -> PM (a, Attributes)
parse Parser a
p = IO (ParseResult a) -> PM (a, Attributes)
forall a. IO (ParseResult a) -> PM (a, Attributes)
wrapM (IO (ParseResult a) -> PM (a, Attributes))
-> (String -> IO (ParseResult a)) -> String -> PM (a, Attributes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult a -> IO (ParseResult a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseResult a -> IO (ParseResult a))
-> (String -> ParseResult a) -> String -> IO (ParseResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
forall a.
ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
M.parse (Parser a -> ParseFlags
forall a. Parser a -> ParseFlags
parseFlags Parser a
p) [LexState]
normalLexState (Parser a -> Parser a
forall a. Parser a -> Parser a
parser Parser a
p)

-- | Parse with top-level layout.

parseFileFromString
  :: SrcFile   -- ^ Name of source file.
  -> Parser a  -- ^ Parser to use.
  -> String    -- ^ Contents of source file.
  -> PM (a, Attributes)
parseFileFromString :: forall a. SrcFile -> Parser a -> String -> PM (a, Attributes)
parseFileFromString SrcFile
src Parser a
p = IO (ParseResult a) -> PM (a, Attributes)
forall a. IO (ParseResult a) -> PM (a, Attributes)
wrapM (IO (ParseResult a) -> PM (a, Attributes))
-> (String -> IO (ParseResult a)) -> String -> PM (a, Attributes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult a -> IO (ParseResult a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseResult a -> IO (ParseResult a))
-> (String -> ParseResult a) -> String -> IO (ParseResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseFlags
-> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
forall a.
ParseFlags
-> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
M.parseFromSrc (Parser a -> ParseFlags
forall a. Parser a -> ParseFlags
parseFlags Parser a
p) [LexState]
layoutLexState (Parser a -> Parser a
forall a. Parser a -> Parser a
parser Parser a
p) SrcFile
src

-- | Parse with top-level layout.

parseLiterateWithoutComments :: LiterateParser a
parseLiterateWithoutComments :: forall a. LiterateParser a
parseLiterateWithoutComments Parser a
p [Layer]
layers = SrcFile -> Parser a -> String -> PM (a, Attributes)
forall a. SrcFile -> Parser a -> String -> PM (a, Attributes)
parseFileFromString ([Layer] -> SrcFile
literateSrcFile [Layer]
layers) Parser a
p (String -> PM (a, Attributes)) -> String -> PM (a, Attributes)
forall a b. (a -> b) -> a -> b
$ [Layer] -> String
illiterate [Layer]
layers

-- | Parse with top-level layout.

parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments Parser [Token]
p [Layer]
layers = do
  ([Token]
code, Attributes
coh) <- LiterateParser [Token]
forall a. LiterateParser a
parseLiterateWithoutComments Parser [Token]
p [Layer]
layers
  let literate :: [Layer]
literate = (Layer -> Bool) -> [Layer] -> [Layer]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Layer -> Bool) -> Layer -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layer -> Bool
isCodeLayer) [Layer]
layers
  let ([Either Token Layer]
terms, [(Either Token Layer, Either Token Layer)]
overlaps) = [Either Token Layer]
-> [Either Token Layer]
-> ([Either Token Layer],
    [(Either Token Layer, Either Token Layer)])
forall a. HasRange a => [a] -> [a] -> ([a], [(a, a)])
interleaveRanges ((Token -> Either Token Layer) -> [Token] -> [Either Token Layer]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Either Token Layer
forall a b. a -> Either a b
Left [Token]
code) ((Layer -> Either Token Layer) -> [Layer] -> [Either Token Layer]
forall a b. (a -> b) -> [a] -> [b]
map Layer -> Either Token Layer
forall a b. b -> Either a b
Right [Layer]
literate)

  [Either Token Layer] -> (Either Token Layer -> PM ()) -> PM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (((Either Token Layer, Either Token Layer) -> Either Token Layer)
-> [(Either Token Layer, Either Token Layer)]
-> [Either Token Layer]
forall a b. (a -> b) -> [a] -> [b]
map (Either Token Layer, Either Token Layer) -> Either Token Layer
forall a b. (a, b) -> a
fst [(Either Token Layer, Either Token Layer)]
overlaps) ((Either Token Layer -> PM ()) -> PM ())
-> (Either Token Layer -> PM ()) -> PM ()
forall a b. (a -> b) -> a -> b
$ \Either Token Layer
c ->
    ParseWarning -> PM ()
warning (ParseWarning -> PM ()) -> ParseWarning -> PM ()
forall a b. (a -> b) -> a -> b
$ OverlappingTokensWarning { warnRange :: Range' SrcFile
warnRange = Either Token Layer -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Either Token Layer
c }

  (, Attributes
coh) ([Token] -> ([Token], Attributes))
-> PM [Token] -> PM ([Token], Attributes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Token] -> PM [Token]
forall a. a -> PM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> PM [Token]) -> [Token] -> PM [Token]
forall a b. (a -> b) -> a -> b
$ [Either Token Layer]
-> (Either Token Layer -> Maybe Token) -> [Token]
forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [Either Token Layer]
terms ((Either Token Layer -> Maybe Token) -> [Token])
-> (Either Token Layer -> Maybe Token) -> [Token]
forall a b. (a -> b) -> a -> b
$ \case
    Left Token
t                           -> Token -> Maybe Token
forall a. a -> Maybe a
Just Token
t
    Right (Layer LayerRole
Comment Interval
interval String
s) -> Token -> Maybe Token
forall a. a -> Maybe a
Just (Token -> Maybe Token) -> Token -> Maybe Token
forall a b. (a -> b) -> a -> b
$ (Interval, String) -> Token
TokTeX    (Interval
interval, String
s)
    Right (Layer LayerRole
Markup  Interval
interval String
s) -> Token -> Maybe Token
forall a. a -> Maybe a
Just (Token -> Maybe Token) -> Token -> Maybe Token
forall a b. (a -> b) -> a -> b
$ (Interval, String) -> Token
TokMarkup (Interval
interval, String
s)
    Right (Layer LayerRole
Code Interval
_ String
_)           -> Maybe Token
forall a. Maybe a
Nothing)


parseLiterateFile
  :: Processor
  -> Parser a
  -> RangeFile
     -- ^ The file.
  -> String
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> PM (a, Attributes)
parseLiterateFile :: forall a.
Processor -> Parser a -> RangeFile -> String -> PM (a, Attributes)
parseLiterateFile Processor
po Parser a
p RangeFile
path = Parser a -> LiterateParser a
forall a. Parser a -> LiterateParser a
parseLiterate Parser a
p Parser a
p ([Layer] -> PM (a, Attributes))
-> (String -> [Layer]) -> String -> PM (a, Attributes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Processor
po (Maybe RangeFile -> Position
startPos (RangeFile -> Maybe RangeFile
forall a. a -> Maybe a
Just RangeFile
path))

parsePosString ::
  Parser a -> Position -> String -> PM (a, Attributes)
parsePosString :: forall a. Parser a -> Position -> String -> PM (a, Attributes)
parsePosString Parser a
p Position
pos = IO (ParseResult a) -> PM (a, Attributes)
forall a. IO (ParseResult a) -> PM (a, Attributes)
wrapM (IO (ParseResult a) -> PM (a, Attributes))
-> (String -> IO (ParseResult a)) -> String -> PM (a, Attributes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult a -> IO (ParseResult a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseResult a -> IO (ParseResult a))
-> (String -> ParseResult a) -> String -> IO (ParseResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position
-> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
forall a.
Position
-> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
M.parsePosString Position
pos (Parser a -> ParseFlags
forall a. Parser a -> ParseFlags
parseFlags Parser a
p) [LexState]
normalLexState (Parser a -> Parser a
forall a. Parser a -> Parser a
parser Parser a
p)

-- | Extensions supported by `parseFile`.

acceptableFileExts :: [String]
acceptableFileExts :: [String]
acceptableFileExts = String
".agda" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((String, (Processor, FileType)) -> String
forall a b. (a, b) -> a
fst ((String, (Processor, FileType)) -> String)
-> [(String, (Processor, FileType))] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, (Processor, FileType))]
literateProcessors)

parseFile
  :: Show a
  => Parser a
  -> RangeFile
     -- ^ The file.
  -> String
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> PM ((a, Attributes), FileType)
parseFile :: forall a.
Show a =>
Parser a -> RangeFile -> String -> PM ((a, Attributes), FileType)
parseFile Parser a
p RangeFile
file String
input =
  if String
".agda" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` String
path then
    (, FileType
AgdaFileType) ((a, Attributes) -> ((a, Attributes), FileType))
-> PM (a, Attributes) -> PM ((a, Attributes), FileType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcFile -> Parser a -> String -> PM (a, Attributes)
forall a. SrcFile -> Parser a -> String -> PM (a, Attributes)
parseFileFromString (RangeFile -> SrcFile
forall a. a -> Maybe a
Strict.Just RangeFile
file) Parser a
p String
input
  else
    [(String, (Processor, FileType))] -> PM ((a, Attributes), FileType)
go [(String, (Processor, FileType))]
literateProcessors
  where
    path :: String
path = AbsolutePath -> String
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
file)

    go :: [(String, (Processor, FileType))] -> PM ((a, Attributes), FileType)
go [] = ParseError -> PM ((a, Attributes), FileType)
forall a. ParseError -> PM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvalidExtensionError
                   { errPath :: RangeFile
errPath = RangeFile
file
                   , errValidExts :: [String]
errValidExts = [String]
acceptableFileExts
                   }
    go ((String
ext, (Processor
po, FileType
ft)) : [(String, (Processor, FileType))]
pos)
      | String
ext String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` String
path =
          (, FileType
ft) ((a, Attributes) -> ((a, Attributes), FileType))
-> PM (a, Attributes) -> PM ((a, Attributes), FileType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Processor -> Parser a -> RangeFile -> String -> PM (a, Attributes)
forall a.
Processor -> Parser a -> RangeFile -> String -> PM (a, Attributes)
parseLiterateFile Processor
po Parser a
p RangeFile
file String
input
      | Bool
otherwise = [(String, (Processor, FileType))] -> PM ((a, Attributes), FileType)
go [(String, (Processor, FileType))]
pos

------------------------------------------------------------------------
-- Specific parsers

-- | Parses a module.

moduleParser :: Parser Module
moduleParser :: Parser Module
moduleParser = Parser
  { parser :: Parser Module
parser        = Parser Module
P.moduleParser
  , parseFlags :: ParseFlags
parseFlags    = ParseFlags
withoutComments
  , parseLiterate :: LiterateParser Module
parseLiterate = LiterateParser Module
forall a. LiterateParser a
parseLiterateWithoutComments
  }

-- | Parses a module name.

moduleNameParser :: Parser QName
moduleNameParser :: Parser QName
moduleNameParser = Parser
  { parser :: Parser QName
parser        = Parser QName
P.moduleNameParser
  , parseFlags :: ParseFlags
parseFlags    = ParseFlags
withoutComments
  , parseLiterate :: LiterateParser QName
parseLiterate = LiterateParser QName
forall a. LiterateParser a
parseLiterateWithoutComments
  }

-- | Parses an expression.

exprParser :: Parser Expr
exprParser :: Parser Expr
exprParser = Parser
  { parser :: Parser Expr
parser        = Parser Expr
P.exprParser
  , parseFlags :: ParseFlags
parseFlags    = ParseFlags
withoutComments
  , parseLiterate :: LiterateParser Expr
parseLiterate = LiterateParser Expr
forall a. LiterateParser a
parseLiterateWithoutComments
  }

-- | Parses an expression followed by a where clause.

exprWhereParser :: Parser ExprWhere
exprWhereParser :: Parser ExprWhere
exprWhereParser = Parser
  { parser :: Parser ExprWhere
parser        = Parser ExprWhere
P.exprWhereParser
  , parseFlags :: ParseFlags
parseFlags    = ParseFlags
withoutComments
  , parseLiterate :: LiterateParser ExprWhere
parseLiterate = LiterateParser ExprWhere
forall a. LiterateParser a
parseLiterateWithoutComments
  }

-- | Parses an expression or some other content of an interaction hole.

holeContentParser :: Parser HoleContent
holeContentParser :: Parser HoleContent
holeContentParser = Parser
  { parser :: Parser HoleContent
parser        = Parser HoleContent
P.holeContentParser
  , parseFlags :: ParseFlags
parseFlags    = ParseFlags
withoutComments
  , parseLiterate :: LiterateParser HoleContent
parseLiterate = LiterateParser HoleContent
forall a. LiterateParser a
parseLiterateWithoutComments
  }

-- | Gives the parsed token stream (including comments).

tokensParser :: Parser [Token]
tokensParser :: Parser [Token]
tokensParser = Parser
  { parser :: Parser [Token]
parser        = Parser [Token]
P.tokensParser
  , parseFlags :: ParseFlags
parseFlags    = ParseFlags
withComments
  , parseLiterate :: LiterateParser [Token]
parseLiterate = LiterateParser [Token]
parseLiterateWithComments
  }

-- | Keep comments in the token stream generated by the lexer.

withComments :: ParseFlags
withComments :: ParseFlags
withComments = ParseFlags
defaultParseFlags { parseKeepComments = True }

-- | Do not keep comments in the token stream generated by the lexer.

withoutComments :: ParseFlags
withoutComments :: ParseFlags
withoutComments = ParseFlags
defaultParseFlags { parseKeepComments = False }