module Mikan.Syntax.Parser
    ( -- * Types
      Parser
      -- * Parse functions
    , parse
    , parsePosString
    , parseRangeString
    , parseFile
      -- * Parsers
    , moduleParser
    , moduleNameParser
    , agdaFileExtensions
    , exprParser
    , exprWhereParser
    , holeContentParser
    , tokensParser
      -- * 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 Control.Lens

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

import Mikan.Syntax.Common
import Mikan.Syntax.Position
import Mikan.Syntax.Parser.Monad
  ( ParseError(..), ParseWarning(..), ParseResult(..), ParseFlags, LexState
  , ParseState (parseWarnings, parseAttributes), defaultParseFlags, parseKeepComments
  )
import Mikan.Syntax.Parser.Monad qualified as M
import Mikan.Syntax.Parser.Parser qualified as P
import Mikan.Syntax.Parser.Lexer
import Mikan.Syntax.Parser.Literate
import Mikan.Syntax.Concrete
import Mikan.Syntax.Concrete.Attribute
import Mikan.Syntax.Parser.Tokens

import Mikan.Utils.FileName
import Mikan.Utils.IO.UTF8 (readTextFile)
import Mikan.Utils.Maybe   (forMaybe, fromMaybe)
import Mikan.Utils.Maybe.Strict qualified as Strict
import Mikan.Utils.Lens

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

------------------------------------------------------------------------
-- 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 -> SrcFile -> [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 -> Text -> PM (a, Attributes)
parse :: forall a. Parser a -> Text -> 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))
-> (Text -> IO (ParseResult a)) -> Text -> 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))
-> (Text -> ParseResult a) -> Text -> IO (ParseResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseFlags -> [LexState] -> Parser a -> Text -> ParseResult a
forall a.
ParseFlags -> [LexState] -> Parser a -> Text -> 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.
  -> Text    -- ^ Contents of source file.
  -> PM (a, Attributes)
parseFileFromString :: forall a. SrcFile -> Parser a -> Text -> 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))
-> (Text -> IO (ParseResult a)) -> Text -> 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))
-> (Text -> ParseResult a) -> Text -> IO (ParseResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseFlags
-> [LexState] -> Parser a -> SrcFile -> Text -> ParseResult a
forall a.
ParseFlags
-> [LexState] -> Parser a -> SrcFile -> Text -> 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 SrcFile
f [Layer]
layers = SrcFile -> Parser a -> Text -> PM (a, Attributes)
forall a. SrcFile -> Parser a -> Text -> PM (a, Attributes)
parseFileFromString SrcFile
f Parser a
p (Text -> PM (a, Attributes)) -> Text -> PM (a, Attributes)
forall a b. (a -> b) -> a -> b
$ [Layer] -> Text
illiterate [Layer]
layers

-- | Parse with top-level layout.

parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments Parser [Token]
p SrcFile
f [Layer]
layers = do
  (code, coh) <- LiterateParser [Token]
forall a. LiterateParser a
parseLiterateWithoutComments Parser [Token]
p SrcFile
f [Layer]
layers
  let 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 (terms, overlaps) = interleaveRanges (map Left code) (map Right literate)

  forM_ (map fst overlaps) $ \Either Token Layer
c ->
    ParseWarning -> PM ()
warning (ParseWarning -> PM ()) -> ParseWarning -> PM ()
forall a b. (a -> b) -> a -> b
$ OverlappingTokensWarning { warnRange :: Range' SrcFile
warnRange = SrcFile
f SrcFile -> Range' () -> Range' SrcFile
forall a b. a -> Range' b -> Range' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Either Token Layer -> Range' ()
forall a. HasRangeWithoutFile a => a -> Range' ()
getRangeWithoutFile Either Token Layer
c }

  return . (,coh) . forMaybe terms $ \case
      Left Token
t                           -> Token -> Maybe Token
forall a. a -> Maybe a
Just Token
t
      Right (Layer LayerRole
Comment IntervalWithoutFile
interval Text
s) -> Token -> Maybe Token
forall a. a -> Maybe a
Just (Token -> Maybe Token) -> Token -> Maybe Token
forall a b. (a -> b) -> a -> b
$ (Interval, Text) -> Token
TokTeX    (SrcFile
f SrcFile -> IntervalWithoutFile -> Interval
forall a b. a -> Interval' b -> Interval' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IntervalWithoutFile
interval, Text
s)
      Right (Layer LayerRole
Markup  IntervalWithoutFile
interval Text
s) -> Token -> Maybe Token
forall a. a -> Maybe a
Just (Token -> Maybe Token) -> Token -> Maybe Token
forall a b. (a -> b) -> a -> b
$ (Interval, Text) -> Token
TokMarkup (SrcFile
f SrcFile -> IntervalWithoutFile -> Interval
forall a b. a -> Interval' b -> Interval' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IntervalWithoutFile
interval, Text
s)
      Right (Layer LayerRole
Code IntervalWithoutFile
_ Text
_)           -> Maybe Token
forall a. Maybe a
Nothing


parseLiterateFile
  :: Processor
  -> Parser a
  -> RangeFile
     -- ^ The file.
  -> Text
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> PM (a, Attributes)
parseLiterateFile :: forall a.
Processor -> Parser a -> RangeFile -> Text -> 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 (RangeFile -> SrcFile
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeFile
path) ([Layer] -> PM (a, Attributes))
-> (Text -> [Layer]) -> Text -> PM (a, Attributes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Processor
po (() -> Position' ()
forall a. a -> Position' a
startPos' ())

parsePosString :: Parser a -> Position -> Text -> PM (a, Attributes)
parsePosString :: forall a. Parser a -> Position -> Text -> 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))
-> (Text -> IO (ParseResult a)) -> Text -> 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))
-> (Text -> ParseResult a) -> Text -> IO (ParseResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position
-> ParseFlags -> [LexState] -> Parser a -> Text -> ParseResult a
forall a.
Position
-> ParseFlags -> [LexState] -> Parser a -> Text -> 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)

-- | Calls 'parsePosString' with 'Position' extracted from the Range.
parseRangeString :: Parser a -> Range -> Text -> PM (a, Attributes)
parseRangeString :: forall a. Parser a -> Range' SrcFile -> Text -> PM (a, Attributes)
parseRangeString Parser a
p = Parser a -> Position -> Text -> PM (a, Attributes)
forall a. Parser a -> Position -> Text -> PM (a, Attributes)
parsePosString Parser a
p (Position -> Text -> PM (a, Attributes))
-> (Range' SrcFile -> Position)
-> Range' SrcFile
-> Text
-> PM (a, Attributes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position -> Maybe Position -> Position
forall a. a -> Maybe a -> a
fromMaybe (Maybe RangeFile -> Position
startPos Maybe RangeFile
forall a. Maybe a
Nothing) (Maybe Position -> Position)
-> (Range' SrcFile -> Maybe Position) -> Range' SrcFile -> Position
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range' SrcFile -> Maybe Position
forall a. Range' a -> Maybe (Position' a)
rStart

-- | Extensions supported by `parseFile`.

agdaFileExtensions :: [String]
agdaFileExtensions :: [String]
agdaFileExtensions = String
".mkn" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
".agda" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Bool -> [(String, Processor, FileType)]
literateProcessors Bool
True [(String, Processor, FileType)]
-> Getting (Endo [String]) [(String, Processor, FileType)] String
-> [String]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. ((String, Processor, FileType)
 -> Const (Endo [String]) (String, Processor, FileType))
-> [(String, Processor, FileType)]
-> Const (Endo [String]) [(String, Processor, FileType)]
forall s t a b. Each s t a b => Traversal s t a b
Traversal
  [(String, Processor, FileType)]
  [(String, Processor, FileType)]
  (String, Processor, FileType)
  (String, Processor, FileType)
each (((String, Processor, FileType)
  -> Const (Endo [String]) (String, Processor, FileType))
 -> [(String, Processor, FileType)]
 -> Const (Endo [String]) [(String, Processor, FileType)])
-> ((String -> Const (Endo [String]) String)
    -> (String, Processor, FileType)
    -> Const (Endo [String]) (String, Processor, FileType))
-> Getting (Endo [String]) [(String, Processor, FileType)] String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Const (Endo [String]) String)
-> (String, Processor, FileType)
-> Const (Endo [String]) (String, Processor, FileType)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (String, Processor, FileType)
  (String, Processor, FileType)
  String
  String
_1

-- | Parse a file.
--
--   The 'Bool' parameter controls whether only @```agda@ blocks
--   are treated as Agda code in Markdown/Typst files.
--   When @True@, only blocks marked @```agda@ are considered code.
--   When @False@, both @```@ and @```agda@ blocks are code (default).

parseFile ::
     Bool
     -- ^ When @True@, only treat @```agda@ blocks as code in Markdown/Typst.
  -> Parser a
  -> RangeFile
     -- ^ The file.
  -> Text
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> PM ((a, Attributes), FileType)
parseFile :: forall a.
Bool
-> Parser a -> RangeFile -> Text -> PM ((a, Attributes), FileType)
parseFile Bool
onlyAgdaBlocks Parser a
p RangeFile
file Text
input
  | String
".mkn" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` String
path =
    (, 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 -> Text -> PM (a, Attributes)
forall a. SrcFile -> Parser a -> Text -> PM (a, Attributes)
parseFileFromString (RangeFile -> SrcFile
forall a. a -> Maybe a
Strict.Just RangeFile
file) Parser a
p Text
input
  | String
".agda" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` String
path =
    -- TODO: warning for using the legacy extension
    (, 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 -> Text -> PM (a, Attributes)
forall a. SrcFile -> Parser a -> Text -> PM (a, Attributes)
parseFileFromString (RangeFile -> SrcFile
forall a. a -> Maybe a
Strict.Just RangeFile
file) Parser a
p Text
input
  | Bool
otherwise =
    [(String, Processor, FileType)] -> PM ((a, Attributes), FileType)
tryLiterate (Bool -> [(String, Processor, FileType)]
literateProcessors Bool
onlyAgdaBlocks)
  where
    path :: String
path = AbsolutePath -> String
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
file)

    tryLiterate :: [(String, Processor, FileType)] -> PM ((a, Attributes), FileType)
tryLiterate [] =
      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]
agdaFileExtensions
        }
    tryLiterate ((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 -> Text -> PM (a, Attributes)
forall a.
Processor -> Parser a -> RangeFile -> Text -> PM (a, Attributes)
parseLiterateFile Processor
po Parser a
p RangeFile
file Text
input
      | Bool
otherwise = [(String, Processor, FileType)] -> PM ((a, Attributes), FileType)
tryLiterate [(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 }