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
-> Text
-> PositionWithoutFile
-> ServerM (LspM Config) (Maybe (Token, Text))
tokenAt Uri
uri Text
source PositionWithoutFile
position = case Uri -> Maybe FilePath
LSP.uriToFilePath Uri
uri of
  Maybe FilePath
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  Just FilePath
filepath -> do
    (Either ParseError (Maybe Token)
result, [ParseWarning]
_warnings) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO forall a b. (a -> b) -> a -> b
$ do
        -- parse the file and get all tokens
        ([Token]
tokens, FileType
_fileType) <- forall a.
Show a =>
Parser a -> AbsolutePath -> FilePath -> PM (a, FileType)
parseFile Parser [Token]
tokensParser (FilePath -> AbsolutePath
mkAbsolute FilePath
filepath) (Text -> FilePath
unpack Text
source)
        -- find the token at the position
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (PositionWithoutFile -> Token -> Bool
pointedBy PositionWithoutFile
position) [Token]
tokens
    case Either ParseError (Maybe Token)
result of
      Left ParseError
_err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Right Maybe Token
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Right (Just Token
token) -> do
        -- get the range of the token
        case Token -> Maybe (Int, Int)
tokenOffsets Token
token of
          Maybe (Int, Int)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
          Just (Int
start, Int
end) -> do
            -- get the text from the range of the token
            let text :: Text
text = Int -> Text -> Text
Text.drop (Int
start forall a. Num a => a -> a -> a
- Int
1) (Int -> Text -> Text
Text.take (Int
end forall a. Num a => a -> a -> a
- Int
1) Text
source)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Token
token, Text
text)
  where
    startAndEnd :: Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
    startAndEnd :: Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
startAndEnd Range
range = do
      PositionWithoutFile
start <- forall a. Range' a -> Maybe PositionWithoutFile
rStart' Range
range
      PositionWithoutFile
end <- forall a. Range' a -> Maybe PositionWithoutFile
rEnd' Range
range
      forall (m :: * -> *) a. Monad m => a -> m a
return (PositionWithoutFile
start, PositionWithoutFile
end)

    pointedBy :: PositionWithoutFile -> Token -> Bool
    pointedBy :: PositionWithoutFile -> Token -> Bool
pointedBy PositionWithoutFile
pos Token
token = forall a. a -> Maybe a -> a
fromMaybe Bool
False forall a b. (a -> b) -> a -> b
$ do
      (PositionWithoutFile
start, PositionWithoutFile
end) <- Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
startAndEnd (forall a. HasRange a => a -> Range
getRange Token
token)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PositionWithoutFile
start forall a. Ord a => a -> a -> Bool
<= PositionWithoutFile
pos Bool -> Bool -> Bool
&& PositionWithoutFile
pos forall a. Ord a => a -> a -> Bool
< PositionWithoutFile
end

    tokenOffsets :: Token -> Maybe (Int, Int)
    tokenOffsets :: Token -> Maybe (Int, Int)
tokenOffsets Token
token = do
      (PositionWithoutFile
start, PositionWithoutFile
end) <- Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
startAndEnd (forall a. HasRange a => a -> Range
getRange Token
token)
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Position' a -> Int32
posPos PositionWithoutFile
start), forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Position' a -> Int32
posPos PositionWithoutFile
end))