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 -> 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
<$ :: forall a b. a -> PM b -> PM a
$c<$ :: forall a b. a -> PM b -> PM a
fmap :: forall a b. (a -> b) -> PM a -> PM b
$cfmap :: forall a b. (a -> b) -> PM a -> PM b
Functor, Functor 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
<* :: forall a b. PM a -> PM b -> PM a
$c<* :: forall a b. PM a -> PM b -> PM a
*> :: forall a b. PM a -> PM b -> PM b
$c*> :: forall a b. PM a -> PM b -> PM b
liftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
$cliftA2 :: forall a b c. (a -> b -> c) -> PM a -> PM b -> PM c
<*> :: forall a b. PM (a -> b) -> PM a -> PM b
$c<*> :: forall a b. PM (a -> b) -> PM a -> PM b
pure :: forall a. a -> PM a
$cpure :: forall a. a -> PM a
Applicative, Applicative 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
return :: forall a. a -> PM a
$creturn :: forall a. a -> PM a
>> :: forall a b. PM a -> PM b -> PM b
$c>> :: forall a b. PM a -> PM b -> PM b
>>= :: forall a b. PM a -> (a -> PM b) -> PM b
$c>>= :: forall a b. PM a -> (a -> PM b) -> PM b
Monad, Monad PM
forall a. IO a -> PM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> PM a
$cliftIO :: 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 = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. [a] -> [a]
reverse) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PM a -> ExceptT ParseError (StateT [ParseWarning] IO) a
unPM

-- | Add a 'ParseWarning'.

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

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

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

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

-- | Returns the contents of the given file.

readFilePM :: RangeFile -> PM Text
readFilePM :: RangeFile -> PM Text
readFilePM RangeFile
file =
  forall e (m :: * -> *) a.
(MonadError e m, MonadIO m) =>
(IOError -> e) -> IO a -> m a
wrapIOM (RangeFile -> IOError -> ParseError
ReadFileError RangeFile
file) forall a b. (a -> b) -> a -> b
$
  String -> IO Text
readTextFile (AbsolutePath -> String
filePath 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIOforall a b. (a -> b) -> a -> b
$ (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO a
m) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\IOError
err -> forall (m :: * -> *) a. Monad m => a -> m a
returnforall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (IOError
err :: IOError))
  case Either IOError a
a of
    Right a
x  -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    Left IOError
err -> 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, CohesionAttributes)

-- | 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, CohesionAttributes)
parse :: forall a. Parser a -> String -> PM (a, CohesionAttributes)
parse Parser a
p = forall a. IO (ParseResult a) -> PM (a, CohesionAttributes)
wrapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
M.parse (forall a. Parser a -> ParseFlags
parseFlags Parser a
p) [LexState]
normalLexState (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, CohesionAttributes)
parseFileFromString :: forall a.
SrcFile -> Parser a -> String -> PM (a, CohesionAttributes)
parseFileFromString SrcFile
src Parser a
p = forall a. IO (ParseResult a) -> PM (a, CohesionAttributes)
wrapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
ParseFlags
-> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
M.parseFromSrc (forall a. Parser a -> ParseFlags
parseFlags Parser a
p) [LexState]
layoutLexState (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 = forall a.
SrcFile -> Parser a -> String -> PM (a, CohesionAttributes)
parseFileFromString ([Layer] -> SrcFile
literateSrcFile [Layer]
layers) Parser a
p 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, CohesionAttributes
coh) <- forall a. LiterateParser a
parseLiterateWithoutComments Parser [Token]
p [Layer]
layers
  let literate :: [Layer]
literate = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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) = forall a. HasRange a => [a] -> [a] -> ([a], [(a, a)])
interleaveRanges (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Token]
code) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. b -> Either a b
Right [Layer]
literate)

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

  (, CohesionAttributes
coh) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [Either Token Layer]
terms forall a b. (a -> b) -> a -> b
$ \case
    Left Token
t                           -> forall a. a -> Maybe a
Just Token
t
    Right (Layer LayerRole
Comment Interval
interval String
s) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (Interval, String) -> Token
TokTeX    (Interval
interval, String
s)
    Right (Layer LayerRole
Markup  Interval
interval String
s) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (Interval, String) -> Token
TokMarkup (Interval
interval, String
s)
    Right (Layer LayerRole
Code Interval
_ String
_)           -> 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, CohesionAttributes)
parseLiterateFile :: forall a.
Processor
-> Parser a -> RangeFile -> String -> PM (a, CohesionAttributes)
parseLiterateFile Processor
po Parser a
p RangeFile
path = forall a. Parser a -> LiterateParser a
parseLiterate Parser a
p Parser a
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. Processor
po (Maybe RangeFile -> Position
startPos (forall a. a -> Maybe a
Just RangeFile
path))

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

-- | Extensions supported by `parseFile`.

acceptableFileExts :: [String]
acceptableFileExts :: [String]
acceptableFileExts = String
".agda" forall a. a -> [a] -> [a]
: (forall a b. (a, b) -> a
fst 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, CohesionAttributes), FileType)
parseFile :: forall a.
Show a =>
Parser a
-> RangeFile -> String -> PM ((a, CohesionAttributes), FileType)
parseFile Parser a
p RangeFile
file String
input =
  if String
".agda" forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` String
path then
    (, FileType
AgdaFileType) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
SrcFile -> Parser a -> String -> PM (a, CohesionAttributes)
parseFileFromString (forall a. a -> Maybe a
Strict.Just RangeFile
file) Parser a
p String
input
  else
    [(String, (Processor, FileType))]
-> PM ((a, CohesionAttributes), FileType)
go [(String, (Processor, FileType))]
literateProcessors
  where
    path :: String
path = AbsolutePath -> String
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
file)

    go :: [(String, (Processor, FileType))]
-> PM ((a, CohesionAttributes), FileType)
go [] = 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 forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` String
path =
          (, FileType
ft) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Processor
-> Parser a -> RangeFile -> String -> PM (a, CohesionAttributes)
parseLiterateFile Processor
po Parser a
p RangeFile
file String
input
      | Bool
otherwise = [(String, (Processor, FileType))]
-> PM ((a, CohesionAttributes), 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 = 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 = 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 = 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 = 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 = 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 :: 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 }