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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IO (TChan a)
newTChanIO forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> IO (TVar a)
newTVarIO 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 <- forall r (m :: * -> *). MonadReader r m => m r
ask
  forall (m :: * -> *) a.
MonadIO m =>
ServerM TCM a -> ServerM m (Either String a)
runAgda forall a b. (a -> b) -> a -> b
$ do
    -- get command line options 
    CommandLineOptions
options <- forall (m :: * -> *).
(HasOptions m, MonadIO m) =>
ServerM m CommandLineOptions
getCommandLineOptions

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

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

    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 = forall a. CommandM a -> ServerM (LspM Config) (Either String a)
runCommandM forall a b. (a -> b) -> a -> b
$ do
    -- load first
  forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
filepath [] Bool
True Mode
Imp.TypeCheck forall a b. (a -> b) -> a -> b
$ \CheckResult
_ -> 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 <- forall a. CommandM a -> CommandM a
localStateCommandM forall a b. (a -> b) -> a -> b
$ do
    Expr
e <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> String -> PM a
parse Parser Expr
exprParser (Text -> String
unpack Text
text)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
atTopLevel forall a b. (a -> b) -> a -> b
$ do
      forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract_ Expr
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm

  Doc -> String
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- 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   -> forall (m :: * -> *) a. Monad m => a -> m a
return 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             -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Just (Token
_token, Text
text) -> do
          case Uri -> Maybe String
LSP.uriToFilePath Uri
uri of
            Maybe String
Nothing       -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ Text -> Text -> MarkupContent
LSP.markedUpContent
                        Text
"agda-language-server"
                        (Text
"Error: " forall a. Semigroup a => a -> a -> a
<> String -> Text
pack String
err)
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ HoverContents -> Maybe Range -> Hover
LSP.Hover HoverContents
content (forall a. a -> Maybe a
Just Range
range)
                Right String
typeString -> do
                  let content :: HoverContents
content = MarkupContent -> HoverContents
LSP.HoverContents forall a b. (a -> b) -> a -> b
$ Text -> Text -> MarkupContent
LSP.markedUpContent
                        Text
"agda-language-server"
                        (String -> Text
pack String
typeString)
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ HoverContents -> Maybe Range -> Hover
LSP.Hover HoverContents
content (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
--       ]