content: {-# LANGUAGE CPP #-}
  
  module Server.Handler where
  
  import           Agda                           ( getCommandLineOptions
                                                  , runAgda
                                                  )
  import qualified Agda.IR                       as IR
  
  import           Agda.Interaction.Base          ( CommandQueue(..)
  #if MIN_VERSION_Agda(2,7,0)
  #else
                                                  , CommandM
  #endif
                                                  , 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'
  #if MIN_VERSION_Agda(2,8,0)
  #else
                                                  , localStateCommandM
  #endif
  
  #if MIN_VERSION_Agda(2,8,0)
  #elif MIN_VERSION_Agda(2,7,0)
                                                  , CommandM
  #else
  #endif
                                                  )
  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
                                                  )
  #if MIN_VERSION_Agda(2,8,0)
  import           Agda.Interaction.Command       ( CommandM, localStateCommandM )
  import           Agda.TypeChecking.Monad.Trace  ( runPM )
  #endif
  #if MIN_VERSION_Agda(2,8,0)
  #else
  import           Agda.TypeChecking.Warnings     ( runPM )
  #endif
  import           Agda.Syntax.Common.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.Protocol.Types   as LSP
  import qualified Language.LSP.VFS              as VFS
  import           Monad
  import           Options                        ( Config
                                                  , Options(optRawAgdaOptions)
                                                  )
  
  initialiseCommandQueue :: IO CommandQueue
  initialiseCommandQueue = CommandQueue <$> newTChanIO <*> newTVarIO Nothing
  
  runCommandM :: CommandM a -> ServerM (LspM Config) (Either String a)
  runCommandM program = do
    env <- ask
    runAgda $ do
      -- get command line options
      options <- getCommandLineOptions
  
      -- we need to set InteractionOutputCallback else it would panic
      lift $ setInteractionOutputCallback $ \_response -> return ()
  
      -- setup the command state
      commandQueue <- liftIO initialiseCommandQueue
      let commandState = (initCommandState commandQueue)
            { optionsOnReload = options { optAbsoluteIncludePaths = [] }
            }
  
      lift $ evalStateT program commandState
  
  inferTypeOfText
    :: FilePath -> Text -> ServerM (LspM Config) (Either String String)
  inferTypeOfText filepath text = runCommandM $ do
      -- load first
    cmd_load' filepath [] True Imp.TypeCheck $ \_ -> return ()
    -- infer later
    let norm = AsIs
    -- localStateCommandM: restore TC state afterwards, do we need this here?
    typ <- localStateCommandM $ do
      (e, _attrs) <- lift $ runPM $ parse exprParser (unpack text)
      lift $ atTopLevel $ do
        concreteToAbstract_ e >>= typeInCurrent norm
  
    render <$> prettyATop typ
  
  onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM Config) (LSP.Hover LSP.|? LSP.Null)
  onHover uri pos = do
    result <- LSP.getVirtualFile (LSP.toNormalizedUri uri)
    case result of
      Nothing   -> return $ LSP.InR LSP.Null
      Just file -> do
        let source      = VFS.virtualFileText file
        let offsetTable = makeToOffset source
        let agdaPos     = toAgdaPositionWithoutFile offsetTable pos
        lookupResult <- Parser.tokenAt uri source agdaPos
        case lookupResult of
          Nothing             -> return $ LSP.InR LSP.Null
          Just (_token, text) -> do
            case LSP.uriToFilePath uri of
              Nothing       -> return $ LSP.InR LSP.Null
              Just filepath -> do
                let range = LSP.Range pos pos
                inferResult <- inferTypeOfText filepath text
                case inferResult of
                  Left err -> do
                    let content = hoverContent $ "Error: " <> pack err
                    return $ LSP.InL $ LSP.Hover content (Just range)
                  Right typeString -> do
                    let content = hoverContent $ pack typeString
                    return $ LSP.InL $ LSP.Hover content (Just range)
    where
        hoverContent =
          LSP.InL . LSP.mkMarkdownCodeBlock "agda-language-server"
  --------------------------------------------------------------------------------
  -- Helper functions for converting stuff to SemanticTokenAbsolute
  
  
  fromHighlightingInfo :: IR.HighlightingInfo -> LSP.SemanticTokenAbsolute
  fromHighlightingInfo (IR.HighlightingInfo start end aspects isTokenBased note defSrc)
    = LSP.SemanticTokenAbsolute 1 1 3 kw []
    where
      kw = LSP.SemanticTokenTypes_Keyword
  
  -- 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
  --       ]
  