module Agda.Syntax.Parser
    ( -- * Types
      Parser
      -- * Parse functions
    , Agda.Syntax.Parser.parse
    , Agda.Syntax.Parser.parseLiterate
    , Agda.Syntax.Parser.parsePosString
    , parseFile'
      -- * Parsers
    , moduleParser
    , exprParser
    , tokensParser
      -- * Parse errors
    , ParseError(..)
    ) where

import Control.Exception
import Data.List
import System.Directory

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.Strict
import Agda.Syntax.Concrete
import Agda.Syntax.Parser.Tokens

import Agda.Utils.FileName

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

wrap :: Strict a => ParseResult a -> a
wrap (ParseOk _ x)	= x
wrap (ParseFailed err)	= throw err

wrapM:: (Strict a, Monad m) => m (ParseResult a) -> m a
wrapM m =
    do	r <- m
	case r of
	    ParseOk _ x	    -> return x
	    ParseFailed err -> throw err

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

-- | Wrapped Parser type.

data Parser a = Parser
  { parser     :: M.Parser a
  , parseFlags :: ParseFlags
  }

parse :: Strict a => Parser a -> String -> IO a
parse p = wrapM . return . M.parse (parseFlags p) [normal] (parser p)

parseFile :: Strict a => Parser a -> AbsolutePath -> IO a
parseFile p = wrapM . M.parseFile (parseFlags p) [normal] (parser p)

parseLiterate :: Strict a => Parser a -> String -> IO a
parseLiterate p =
  wrapM . return . M.parse (parseFlags p) [literate, code] (parser p)

parseLiterateFile :: Strict a => Parser a -> AbsolutePath -> IO a
parseLiterateFile p =
  wrapM . M.parseFile (parseFlags p) [literate, code] (parser p)

parsePosString :: Strict a => Parser a -> Position -> String -> IO a
parsePosString p pos =
  wrapM . return . M.parsePosString pos (parseFlags p) [normal] (parser p)

parseFile' :: Strict a => Parser a -> AbsolutePath -> IO a
parseFile' p file =
  if "lagda" `isSuffixOf` filePath file then
    Agda.Syntax.Parser.parseLiterateFile p file
   else
    Agda.Syntax.Parser.parseFile p file

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

-- | Parses a module.

moduleParser :: Parser Module
moduleParser = Parser { parser = P.moduleParser
                      , parseFlags = withoutComments }

-- | Parses an expression.

exprParser :: Parser Expr
exprParser = Parser { parser = P.exprParser
                    , parseFlags = withoutComments }

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

tokensParser :: Parser [Token]
tokensParser = Parser { parser = P.tokensParser
                      , parseFlags = withComments }

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

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

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

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