{-# LANGUAGE CPP #-}

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')
#if MIN_VERSION_Agda(2,6,3)
import Agda.Syntax.Position (RangeFile(RangeFile))
#endif
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 -> Maybe (Token, Text) -> ServerM (LspM Config) (Maybe (Token, Text))
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Token, Text)
forall a. Maybe a
Nothing
  Just FilePath
filepath -> do
    let file :: RangeFile
file =
#if MIN_VERSION_Agda(2,6,3)
          AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
RangeFile (FilePath -> AbsolutePath
mkAbsolute FilePath
filepath) Maybe TopLevelModuleName
forall a. Maybe a
Nothing
#else
          mkAbsolute filepath
#endif
    (Either ParseError (Maybe Token)
result, [ParseWarning]
_warnings) <- IO (Either ParseError (Maybe Token), [ParseWarning])
-> ReaderT
     Env (LspM Config) (Either ParseError (Maybe Token), [ParseWarning])
forall a. IO a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either ParseError (Maybe Token), [ParseWarning])
 -> ReaderT
      Env
      (LspM Config)
      (Either ParseError (Maybe Token), [ParseWarning]))
-> IO (Either ParseError (Maybe Token), [ParseWarning])
-> ReaderT
     Env (LspM Config) (Either ParseError (Maybe Token), [ParseWarning])
forall a b. (a -> b) -> a -> b
$
      PM (Maybe Token)
-> IO (Either ParseError (Maybe Token), [ParseWarning])
forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO (PM (Maybe Token)
 -> IO (Either ParseError (Maybe Token), [ParseWarning]))
-> PM (Maybe Token)
-> IO (Either ParseError (Maybe Token), [ParseWarning])
forall a b. (a -> b) -> a -> b
$ do
        -- parse the file and get all tokens
        (([Token], CohesionAttributes)
r, FileType
_fileType) <- Parser [Token]
-> RangeFile
-> FilePath
-> PM (([Token], CohesionAttributes), FileType)
forall a.
Show a =>
Parser a
-> RangeFile -> FilePath -> PM ((a, CohesionAttributes), FileType)
parseFile Parser [Token]
tokensParser RangeFile
file (Text -> FilePath
unpack Text
source)
        let tokens :: [Token]
tokens =
#if MIN_VERSION_Agda(2,6,3)
              ([Token], CohesionAttributes) -> [Token]
forall a b. (a, b) -> a
fst ([Token], CohesionAttributes)
r
#else
              r
#endif
        -- find the token at the position
        Maybe Token -> PM (Maybe Token)
forall a. a -> PM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Token -> PM (Maybe Token))
-> Maybe Token -> PM (Maybe Token)
forall a b. (a -> b) -> a -> b
$ (Token -> Bool) -> [Token] -> Maybe Token
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 -> Maybe (Token, Text) -> ServerM (LspM Config) (Maybe (Token, Text))
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Token, Text)
forall a. Maybe a
Nothing
      Right Maybe Token
Nothing -> Maybe (Token, Text) -> ServerM (LspM Config) (Maybe (Token, Text))
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Token, Text)
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 -> Maybe (Token, Text) -> ServerM (LspM Config) (Maybe (Token, Text))
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Token, Text)
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Text -> Text
Text.take (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Text
source)
            Maybe (Token, Text) -> ServerM (LspM Config) (Maybe (Token, Text))
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Token, Text)
 -> ServerM (LspM Config) (Maybe (Token, Text)))
-> Maybe (Token, Text)
-> ServerM (LspM Config) (Maybe (Token, Text))
forall a b. (a -> b) -> a -> b
$ (Token, Text) -> Maybe (Token, Text)
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 <- Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rStart' Range
range
      PositionWithoutFile
end <- Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rEnd' Range
range
      (PositionWithoutFile, PositionWithoutFile)
-> Maybe (PositionWithoutFile, PositionWithoutFile)
forall a. a -> Maybe a
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 = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
      (PositionWithoutFile
start, PositionWithoutFile
end) <- Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
startAndEnd (Token -> Range
forall a. HasRange a => a -> Range
getRange Token
token)
      Bool -> Maybe Bool
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ PositionWithoutFile
start PositionWithoutFile -> PositionWithoutFile -> Bool
forall a. Ord a => a -> a -> Bool
<= PositionWithoutFile
pos Bool -> Bool -> Bool
&& PositionWithoutFile
pos PositionWithoutFile -> PositionWithoutFile -> Bool
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 (Token -> Range
forall a. HasRange a => a -> Range
getRange Token
token)
      (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (PositionWithoutFile -> Int32
forall a. Position' a -> Int32
posPos PositionWithoutFile
start), Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (PositionWithoutFile -> Int32
forall a. Position' a -> Int32
posPos PositionWithoutFile
end))