module Agda.Parser where

--------------------------------------------------------------------------------

import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
import Agda.Syntax.Parser.Tokens (Token)
import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
import Agda.Utils.FileName (mkAbsolute)
import Monad ( ServerM )
import Control.Monad.State
import Data.List (find)
import Data.Maybe (fromMaybe)
import Data.Text (Text, unpack)
import qualified Data.Text as Text
import Language.LSP.Server (LspM)
import qualified Language.LSP.Types as LSP
import Options (Config)

--------------------------------------------------------------------------------

tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Maybe (Token, Text))
tokenAt uri source position = case LSP.uriToFilePath uri of
  Nothing -> return Nothing
  Just filepath -> do
    (result, _warnings) <- liftIO $
      runPMIO $ do
        -- parse the file and get all tokens
        (tokens, _fileType) <- parseFile tokensParser (mkAbsolute filepath) (unpack source)
        -- find the token at the position
        return $ find (pointedBy position) tokens
    case result of
      Left _err -> return Nothing
      Right Nothing -> return Nothing
      Right (Just token) -> do
        -- get the range of the token
        case tokenOffsets token of
          Nothing -> return Nothing
          Just (start, end) -> do
            -- get the text from the range of the token
            let text = Text.drop (start - 1) (Text.take (end - 1) source)
            return $ Just (token, text)
  where
    startAndEnd :: Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
    startAndEnd range = do
      start <- rStart' range
      end <- rEnd' range
      return (start, end)

    pointedBy :: PositionWithoutFile -> Token -> Bool
    pointedBy pos token = fromMaybe False $ do
      (start, end) <- startAndEnd (getRange token)
      return $ start <= pos && pos < end

    tokenOffsets :: Token -> Maybe (Int, Int)
    tokenOffsets token = do
      (start, end) <- startAndEnd (getRange token)
      return (fromIntegral (posPos start), fromIntegral (posPos end))