{-# LANGUAGE CPP #-}

module Server.Handler where

import           Agda                           ( getCommandLineOptions
                                                , runAgda
                                                )
import qualified Agda.IR                       as IR
import           Agda.Interaction.Base          ( CommandM
                                                , CommandQueue(..)
                                                , CommandState(optionsOnReload)
                                                , Rewrite(AsIs)
                                                , initCommandState
                                                )
import           Agda.Interaction.BasicOps      ( atTopLevel
                                                , typeInCurrent
                                                )
import           Agda.Interaction.Highlighting.Precise
                                                ( HighlightingInfo )
import qualified Agda.Interaction.Imports      as Imp
import           Agda.Interaction.InteractionTop
                                                ( cmd_load'
                                                , localStateCommandM
                                                )
import           Agda.Interaction.Options       ( CommandLineOptions
                                                  ( optAbsoluteIncludePaths
                                                  )
                                                )
import qualified Agda.Parser                   as Parser
import           Agda.Position                  ( makeToOffset
                                                , toAgdaPositionWithoutFile
                                                )
import           Agda.Syntax.Abstract.Pretty    ( prettyATop )
import           Agda.Syntax.Parser             ( exprParser
                                                , parse
                                                )
import           Agda.Syntax.Translation.ConcreteToAbstract
                                                ( concreteToAbstract_ )
import           Agda.TypeChecking.Monad        ( HasOptions(commandLineOptions)
                                                , setInteractionOutputCallback
                                                )
import           Agda.TypeChecking.Warnings     ( runPM )
import           Agda.Utils.Pretty              ( render )
import           Control.Concurrent.STM
import           Control.Monad.Reader
import           Control.Monad.State
import           Data.Text                      ( Text
                                                , pack
                                                , unpack
                                                )
import qualified Data.Text                     as Text
import           Language.LSP.Server            ( LspM )
import qualified Language.LSP.Server           as LSP
import qualified Language.LSP.Types            as LSP
import qualified Language.LSP.VFS              as VFS
import           Monad
import           Options                        ( Config
                                                , Options(optRawAgdaOptions)
                                                )

initialiseCommandQueue :: IO CommandQueue
initialiseCommandQueue :: IO CommandQueue
initialiseCommandQueue = TChan (Integer, Command) -> TVar (Maybe Integer) -> CommandQueue
CommandQueue (TChan (Integer, Command) -> TVar (Maybe Integer) -> CommandQueue)
-> IO (TChan (Integer, Command))
-> IO (TVar (Maybe Integer) -> CommandQueue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (TChan (Integer, Command))
forall a. IO (TChan a)
newTChanIO IO (TVar (Maybe Integer) -> CommandQueue)
-> IO (TVar (Maybe Integer)) -> IO CommandQueue
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer -> IO (TVar (Maybe Integer))
forall a. a -> IO (TVar a)
newTVarIO Maybe Integer
forall a. Maybe a
Nothing

runCommandM :: CommandM a -> ServerM (LspM Config) (Either String a)
runCommandM :: forall a. CommandM a -> ServerM (LspM Config) (Either String a)
runCommandM CommandM a
program = do
  Env
env <- ReaderT Env (LspM Config) Env
forall r (m :: * -> *). MonadReader r m => m r
ask
  ServerM TCM a -> ServerM (LspM Config) (Either String a)
forall (m :: * -> *) a.
MonadIO m =>
ServerM TCM a -> ServerM m (Either String a)
runAgda (ServerM TCM a -> ServerM (LspM Config) (Either String a))
-> ServerM TCM a -> ServerM (LspM Config) (Either String a)
forall a b. (a -> b) -> a -> b
$ do
    -- get command line options
    CommandLineOptions
options <- ServerM TCM CommandLineOptions
forall (m :: * -> *).
(HasOptions m, MonadIO m) =>
ServerM m CommandLineOptions
getCommandLineOptions

    -- we need to set InteractionOutputCallback else it would panic
    TCM () -> ReaderT Env TCM ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT Env m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ReaderT Env TCM ()) -> TCM () -> ReaderT Env TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionOutputCallback -> TCM ()
setInteractionOutputCallback (InteractionOutputCallback -> TCM ())
-> InteractionOutputCallback -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Response
_response -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    -- setup the command state
    CommandQueue
commandQueue <- IO CommandQueue -> ReaderT Env TCM CommandQueue
forall a. IO a -> ReaderT Env TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO CommandQueue
initialiseCommandQueue
    let commandState :: CommandState
commandState = (CommandQueue -> CommandState
initCommandState CommandQueue
commandQueue)
          { optionsOnReload = options { optAbsoluteIncludePaths = [] }
          }

    TCM a -> ServerM TCM a
forall (m :: * -> *) a. Monad m => m a -> ReaderT Env m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM a -> ServerM TCM a) -> TCM a -> ServerM TCM a
forall a b. (a -> b) -> a -> b
$ CommandM a -> CommandState -> TCM a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandM a
program CommandState
commandState

inferTypeOfText
  :: FilePath -> Text -> ServerM (LspM Config) (Either String String)
inferTypeOfText :: String -> Text -> ServerM (LspM Config) (Either String String)
inferTypeOfText String
filepath Text
text = CommandM String -> ServerM (LspM Config) (Either String String)
forall a. CommandM a -> ServerM (LspM Config) (Either String a)
runCommandM (CommandM String -> ServerM (LspM Config) (Either String String))
-> CommandM String -> ServerM (LspM Config) (Either String String)
forall a b. (a -> b) -> a -> b
$ do
    -- load first
  String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM ())
-> CommandM ()
forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
filepath [] Bool
True Mode
Imp.TypeCheck ((CheckResult -> CommandM ()) -> CommandM ())
-> (CheckResult -> CommandM ()) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \CheckResult
_ -> () -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- infer later
  let norm :: Rewrite
norm = Rewrite
AsIs
  -- localStateCommandM: restore TC state afterwards, do we need this here?
  Expr
typ <- CommandM Expr -> CommandM Expr
forall a. CommandM a -> CommandM a
localStateCommandM (CommandM Expr -> CommandM Expr) -> CommandM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ do
#if MIN_VERSION_Agda(2,6,3)
    (Expr
e, CohesionAttributes
_attrs)
#else
    e
#endif
       <- TCM (Expr, CohesionAttributes)
-> StateT CommandState TCM (Expr, CohesionAttributes)
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Expr, CohesionAttributes)
 -> StateT CommandState TCM (Expr, CohesionAttributes))
-> TCM (Expr, CohesionAttributes)
-> StateT CommandState TCM (Expr, CohesionAttributes)
forall a b. (a -> b) -> a -> b
$ PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes)
forall a. PM a -> TCM a
runPM (PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes))
-> PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes)
forall a b. (a -> b) -> a -> b
$ Parser Expr -> String -> PM (Expr, CohesionAttributes)
forall a. Parser a -> String -> PM (a, CohesionAttributes)
parse Parser Expr
exprParser (Text -> String
unpack Text
text)
    TCM Expr -> CommandM Expr
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ TCM Expr -> TCM Expr
forall a. TCM a -> TCM a
atTopLevel (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ do
      Expr -> ScopeM (AbsOfCon Expr)
forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract_ Expr
e TCM Expr -> (Expr -> TCM Expr) -> TCM Expr
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm

  Doc -> String
render (Doc -> String) -> StateT CommandState TCM Doc -> CommandM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT CommandState TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
typ

onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM Config) (Maybe LSP.Hover)
onHover :: Uri -> Position -> ServerM (LspM Config) (Maybe Hover)
onHover Uri
uri Position
pos = do
  Maybe VirtualFile
result <- NormalizedUri -> ReaderT Env (LspM Config) (Maybe VirtualFile)
forall config (m :: * -> *).
MonadLsp config m =>
NormalizedUri -> m (Maybe VirtualFile)
LSP.getVirtualFile (Uri -> NormalizedUri
LSP.toNormalizedUri Uri
uri)
  case Maybe VirtualFile
result of
    Maybe VirtualFile
Nothing   -> Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Hover
forall a. Maybe a
Nothing
    Just VirtualFile
file -> do
      let source :: Text
source      = VirtualFile -> Text
VFS.virtualFileText VirtualFile
file
      let offsetTable :: ToOffset
offsetTable = Text -> ToOffset
makeToOffset Text
source
      let agdaPos :: PositionWithoutFile
agdaPos     = ToOffset -> Position -> PositionWithoutFile
toAgdaPositionWithoutFile ToOffset
offsetTable Position
pos
      Maybe (Token, Text)
lookupResult <- Uri
-> Text
-> PositionWithoutFile
-> ServerM (LspM Config) (Maybe (Token, Text))
Parser.tokenAt Uri
uri Text
source PositionWithoutFile
agdaPos
      case Maybe (Token, Text)
lookupResult of
        Maybe (Token, Text)
Nothing             -> Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Hover
forall a. Maybe a
Nothing
        Just (Token
_token, Text
text) -> do
          case Uri -> Maybe String
LSP.uriToFilePath Uri
uri of
            Maybe String
Nothing       -> Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Hover
forall a. Maybe a
Nothing
            Just String
filepath -> do
              let range :: Range
range = Position -> Position -> Range
LSP.Range Position
pos Position
pos

              Either String String
inferResult <- String -> Text -> ServerM (LspM Config) (Either String String)
inferTypeOfText String
filepath Text
text
              case Either String String
inferResult of
                Left String
err -> do
                  let content :: HoverContents
content = MarkupContent -> HoverContents
LSP.HoverContents (MarkupContent -> HoverContents) -> MarkupContent -> HoverContents
forall a b. (a -> b) -> a -> b
$ Text -> Text -> MarkupContent
LSP.markedUpContent
                        Text
"agda-language-server"
                        (Text
"Error: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
pack String
err)
                  Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Hover -> ServerM (LspM Config) (Maybe Hover))
-> Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a b. (a -> b) -> a -> b
$ Hover -> Maybe Hover
forall a. a -> Maybe a
Just (Hover -> Maybe Hover) -> Hover -> Maybe Hover
forall a b. (a -> b) -> a -> b
$ HoverContents -> Maybe Range -> Hover
LSP.Hover HoverContents
content (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
range)
                Right String
typeString -> do
                  let content :: HoverContents
content = MarkupContent -> HoverContents
LSP.HoverContents (MarkupContent -> HoverContents) -> MarkupContent -> HoverContents
forall a b. (a -> b) -> a -> b
$ Text -> Text -> MarkupContent
LSP.markedUpContent
                        Text
"agda-language-server"
                        (String -> Text
pack String
typeString)
                  Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a. a -> ReaderT Env (LspM Config) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Hover -> ServerM (LspM Config) (Maybe Hover))
-> Maybe Hover -> ServerM (LspM Config) (Maybe Hover)
forall a b. (a -> b) -> a -> b
$ Hover -> Maybe Hover
forall a. a -> Maybe a
Just (Hover -> Maybe Hover) -> Hover -> Maybe Hover
forall a b. (a -> b) -> a -> b
$ HoverContents -> Maybe Range -> Hover
LSP.Hover HoverContents
content (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
range)

--------------------------------------------------------------------------------
-- Helper functions for converting stuff to SemanticTokenAbsolute


fromHighlightingInfo :: IR.HighlightingInfo -> LSP.SemanticTokenAbsolute
fromHighlightingInfo :: HighlightingInfo -> SemanticTokenAbsolute
fromHighlightingInfo (IR.HighlightingInfo Int
start Int
end [String]
aspects Bool
isTokenBased String
note Maybe (String, Int)
defSrc)
  = UInt
-> UInt
-> UInt
-> SemanticTokenTypes
-> [SemanticTokenModifiers]
-> SemanticTokenAbsolute
LSP.SemanticTokenAbsolute UInt
1 UInt
1 UInt
3 SemanticTokenTypes
LSP.SttKeyword []

-- HighlightingInfo
--       Int -- starting offset
--       Int -- ending offset
--       [String] -- list of names of aspects
--       Bool -- is token based?
--       String -- note
--       (Maybe (FilePath, Int)) -- the defining module of the token and its position in that module

-- toToken
--   :: Ranged a
--   => J.SemanticTokenTypes
--   -> [J.SemanticTokenModifiers]
--   -> a
--   -> [J.SemanticTokenAbsolute]
-- toToken types modifiers x =
--   let range = rangeOf x
--   in  [ J.SemanticTokenAbsolute (posLine (rangeStart range) - 1)
--                                 (posCol (rangeStart range) - 1)
--                                 (rangeSpan range)
--                                 types
--                                 modifiers
--       ]