{-# LANGUAGE GeneralizedNewtypeDeriving #-}

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.Arrow (second)
import Control.Exception
import Control.Monad (forM_)
import Control.Monad.State

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

import Agda.Utils.Except
  ( ExceptT
  , MonadError(throwError)
  , runExceptT
  )
import Agda.Utils.FileName
import Agda.Utils.IO.UTF8 (readTextFile)
import qualified Agda.Utils.Maybe.Strict as Strict

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

wrap :: ParseResult a -> PM a
wrap :: ParseResult a -> PM a
wrap (ParseOk ParseState
_ a
x)      = a -> PM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
wrap (ParseFailed ParseError
err)  = ParseError -> PM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ParseError
err

wrapIOM :: (MonadError e m, MonadIO m) => (IOError -> e) -> IO a -> m a
wrapIOM :: (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return a
x
    Left IOError
err -> e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (IOError -> e
f IOError
err)

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

-- | A monad for handling parse results
newtype PM a = PM { PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a }
               deriving (a -> PM b -> PM a
(a -> b) -> PM a -> PM b
(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
<$ :: a -> PM b -> PM a
$c<$ :: forall a b. a -> PM b -> PM a
fmap :: (a -> b) -> PM a -> PM b
$cfmap :: forall a b. (a -> b) -> PM a -> PM b
Functor, Functor PM
a -> PM a
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
PM a -> PM b -> PM b
PM a -> PM b -> PM a
PM (a -> b) -> PM a -> PM b
(a -> b -> c) -> PM a -> PM b -> PM c
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
<* :: PM a -> PM b -> PM a
$c<* :: forall a b. PM a -> PM b -> PM a
*> :: PM a -> PM b -> PM b
$c*> :: forall a b. PM a -> PM b -> PM b
liftA2 :: (a -> b -> c) -> PM a -> PM b -> PM c
$cliftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
<*> :: PM (a -> b) -> PM a -> PM b
$c<*> :: forall a b. PM (a -> b) -> PM a -> PM b
pure :: a -> PM a
$cpure :: forall a. a -> PM a
$cp1Applicative :: Functor PM
Applicative, Applicative PM
a -> PM a
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
PM a -> (a -> PM b) -> PM b
PM a -> PM b -> PM b
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
return :: a -> PM a
$creturn :: forall a. a -> PM a
>> :: PM a -> PM b -> PM b
$c>> :: forall a b. PM a -> PM b -> PM b
>>= :: PM a -> (a -> PM b) -> PM b
$c>>= :: forall a b. PM a -> (a -> PM b) -> PM b
$cp1Monad :: Applicative PM
Monad,
                         MonadError ParseError, Monad PM
Monad PM -> (forall a. IO a -> PM a) -> MonadIO PM
IO a -> PM a
forall a. IO a -> PM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> PM a
$cliftIO :: forall a. IO a -> PM a
$cp1MonadIO :: Monad PM
MonadIO)

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]
:))

runPMIO :: (MonadIO m) => PM a -> m (Either ParseError a, [ParseWarning])
runPMIO :: PM a -> m (Either ParseError a, [ParseWarning])
runPMIO = IO (Either ParseError a, [ParseWarning])
-> m (Either ParseError a, [ParseWarning])
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([ParseWarning] -> [ParseWarning])
-> (Either ParseError a, [ParseWarning])
-> (Either ParseError a, [ParseWarning])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, 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

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

-- | Wrapped Parser type.

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

type LiterateParser a = Parser a -> [Layer] -> PM a

parse :: Parser a -> String -> PM a
parse :: Parser a -> String -> PM a
parse Parser a
p = IO (ParseResult a) -> PM a
forall a. IO (ParseResult a) -> PM a
wrapM (IO (ParseResult a) -> PM a)
-> (String -> IO (ParseResult a)) -> String -> PM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult a -> IO (ParseResult 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
normal] (Parser a -> Parser a
forall a. Parser a -> Parser a
parser Parser a
p)

parseStringFromFile :: SrcFile -> Parser a -> String -> PM a
parseStringFromFile :: SrcFile -> Parser a -> String -> PM a
parseStringFromFile SrcFile
src Parser a
p = IO (ParseResult a) -> PM a
forall a. IO (ParseResult a) -> PM a
wrapM (IO (ParseResult a) -> PM a)
-> (String -> IO (ParseResult a)) -> String -> PM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult a -> IO (ParseResult 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
layout, LexState
normal] (Parser a -> Parser a
forall a. Parser a -> Parser a
parser Parser a
p) SrcFile
src

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

parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments :: LiterateParser [Token]
parseLiterateWithComments Parser [Token]
p [Layer]
layers = do
  [Either Token Layer]
code <- (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] -> [Either Token Layer])
-> PM [Token] -> PM [Either Token Layer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LiterateParser [Token]
forall a. LiterateParser a
parseLiterateWithoutComments Parser [Token]
p [Layer]
layers
  let literate :: [Either a Layer]
literate = Layer -> Either a Layer
forall a b. b -> Either a b
Right (Layer -> Either a Layer) -> [Layer] -> [Either a Layer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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 [Either Token Layer]
code [Either Token Layer]
forall a. [Either a 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 :: Range' SrcFile -> ParseWarning
OverlappingTokensWarning { warnRange :: Range' SrcFile
warnRange = Either Token Layer -> Range' SrcFile
forall t. HasRange t => t -> Range' SrcFile
getRange Either Token Layer
c }

  [Token] -> PM [Token]
forall (m :: * -> *) a. Monad m => a -> m a
return([Token] -> PM [Token]) -> [Token] -> PM [Token]
forall a b. (a -> b) -> a -> b
$ [[Token]] -> [Token]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ case Either Token Layer
m of
                       Left Token
t -> [Token
t]
                       Right (Layer LayerRole
Comment Interval
interval String
s) -> [(Interval, String) -> Token
TokTeX (Interval
interval, String
s)]
                       Right (Layer LayerRole
Markup Interval
interval String
s) -> [(Interval, String) -> Token
TokMarkup (Interval
interval, String
s)]
                       Right (Layer LayerRole
Code Interval
_ String
_) -> []
                   | Either Token Layer
m <- [Either Token Layer]
terms ]

-- | Returns the contents of the given file.

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

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

parsePosString :: Parser a -> Position -> String -> PM a
parsePosString :: Parser a -> Position -> String -> PM a
parsePosString Parser a
p Position
pos = IO (ParseResult a) -> PM a
forall a. IO (ParseResult a) -> PM a
wrapM (IO (ParseResult a) -> PM a)
-> (String -> IO (ParseResult a)) -> String -> PM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult a -> IO (ParseResult 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
normal] (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
  -> AbsolutePath
     -- ^ The path to the file.
  -> String
     -- ^ The file contents. Note that the file is /not/ read from
     -- disk.
  -> PM (a, FileType)
parseFile :: Parser a -> AbsolutePath -> String -> PM (a, FileType)
parseFile Parser a
p AbsolutePath
file String
input =
  if String
".agda" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` AbsolutePath -> String
filePath AbsolutePath
file then
    (, FileType
AgdaFileType) (a -> (a, FileType)) -> PM a -> PM (a, FileType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcFile -> Parser a -> String -> PM a
forall a. SrcFile -> Parser a -> String -> PM a
Agda.Syntax.Parser.parseStringFromFile
                         (AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file) Parser a
p String
input
  else
    [(String, (Processor, FileType))] -> PM (a, FileType)
forall t. [(String, (Processor, t))] -> PM (a, t)
go [(String, (Processor, FileType))]
literateProcessors
  where
    go :: [(String, (Processor, t))] -> PM (a, t)
go [] = ParseError -> PM (a, t)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvalidExtensionError :: AbsolutePath -> [String] -> ParseError
InvalidExtensionError
                   { errPath :: AbsolutePath
errPath = AbsolutePath
file
                   , errValidExts :: [String]
errValidExts = [String]
acceptableFileExts
                   }
    go ((String
ext, (Processor
po, t
ft)) : [(String, (Processor, t))]
pos)
      | String
ext String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` AbsolutePath -> String
filePath AbsolutePath
file =
          (, t
ft) (a -> (a, t)) -> PM a -> PM (a, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Processor -> Parser a -> AbsolutePath -> String -> PM a
forall a. Processor -> Parser a -> AbsolutePath -> String -> PM a
parseLiterateFile Processor
po Parser a
p AbsolutePath
file String
input
      | Bool
otherwise = [(String, (Processor, t))] -> PM (a, t)
go [(String, (Processor, t))]
pos

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

-- | Parses a module.

moduleParser :: Parser Module
moduleParser :: Parser Module
moduleParser = Parser :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
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 :: forall a. Parser a -> ParseFlags -> LiterateParser a -> Parser a
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 :: Bool
parseKeepComments = Bool
True }

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

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