agda-language-server-7: src/Agda/Position.hs

{-# LANGUAGE CPP #-}

module Agda.Position
  ( ToOffset (..),
    makeToOffset,
    toOffset,
    FromOffset (..),
    makeFromOffset,
    fromOffset,
    toAgdaPositionWithoutFile,
    toAgdaRange,
    prettyPositionWithoutFile,
    -- , toLSPRange
    -- , toLSPPosition
  )
where

import Agda.Syntax.Position
import Agda.Utils.FileName (AbsolutePath (AbsolutePath))
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.Sequence as Seq
import qualified Data.Strict.Maybe as Strict
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Language.LSP.Protocol.Types as LSP

-- Note:  LSP srclocs are 0-base
--        Agda srclocs are 1-base

--------------------------------------------------------------------------------

-- | LSP source locations => Agda source locations

-- | LSP Range -> Agda Range
toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range
toAgdaRange table path (LSP.Range start end) =
  Range
    (Strict.Just $ mkRangeFile $ AbsolutePath path)
    (Seq.singleton interval)
  where
    interval :: IntervalWithoutFile
    interval =
      Interval
#if MIN_VERSION_Agda(2,8,0)
          ()
#endif
        (toAgdaPositionWithoutFile table start)
        (toAgdaPositionWithoutFile table end)
    mkRangeFile path = RangeFile path Nothing

-- | LSP Position -> Agda PositionWithoutFile
toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
toAgdaPositionWithoutFile table (LSP.Position line col) =
  Pn
    ()
    (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)
    (fromIntegral line + 1)
    (fromIntegral col + 1)

prettyPositionWithoutFile :: PositionWithoutFile -> String
prettyPositionWithoutFile pos@(Pn () offset _line _col) =
  "[" <> show pos <> "-" <> show offset <> "]"

--------------------------------------------------------------------------------

-- | Positon => Offset convertion

-- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")
--
--  Example text      corresponding entry of IntMap
--  >abc\n               (1, 4)
--  >def123\r\n          (2, 11)
--  >ghi\r               (3, 15)
--
newtype ToOffset = ToOffset {unToOffset :: IntMap Int}

data Accum = Accum
  { accumPreviousChar :: Maybe Char,
    accumCurrentOffset :: Int,
    accumCurrentLine :: Int,
    accumResult :: IntMap Int
  }

-- | Return a list of offsets of linebreaks ("\n", "\r" or "\r\n")
makeToOffset :: Text -> ToOffset
makeToOffset = ToOffset . accumResult . Text.foldl' go initAccum
  where
    initAccum :: Accum
    initAccum = Accum Nothing 0 0 IntMap.empty

    go :: Accum -> Char -> Accum
    go (Accum (Just '\r') n l table) '\n' =
      Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)
    go (Accum previous n l table) '\n' =
      Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
    go (Accum previous n l table) '\r' =
      Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
    go (Accum previous n l table) char = Accum (Just char) (1 + n) l table

-- | (line, col) => offset (zero-based)
toOffset :: ToOffset -> (Int, Int) -> Int
toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of
  Nothing -> col
  Just offset -> offset + col

--------------------------------------------------------------------------------

-- | Offset => Position convertion

-- An IntMap for speeding up Offset => Position convertion
-- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")
--
--  Example text      corresponding entry of IntMap
--  >abc\n               (4, 1)
--  >def123\r\n          (11, 2)
--  >ghi\r               (15, 3)
--
newtype FromOffset = FromOffset {unFromOffset :: IntMap Int}

fromOffset :: FromOffset -> Int -> (Int, Int)
fromOffset (FromOffset table) offset = case IntMap.lookupLE offset table of
  Nothing -> (0, offset) -- no previous lines
  Just (offsetOfFirstChar, lineNo) -> (lineNo, offset - offsetOfFirstChar)

makeFromOffset :: Text -> FromOffset
makeFromOffset =
  FromOffset
    . accumResult
    . Text.foldl'
      go
      (Accum Nothing 0 0 IntMap.empty)
  where
    go :: Accum -> Char -> Accum
    -- encountered a "\r\n", update the latest entry
    go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of
      ((offset, lineNo), table') ->
        Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')
    -- encountered a line break, add a new entry
    go (Accum previous n l table) '\n' =
      Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
    go (Accum previous n l table) '\r' =
      Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
    go (Accum previous n l table) char = Accum (Just char) (1 + n) l table

-- --------------------------------------------------------------------------------
-- -- | Agda Highlighting Range -> Agda Range

-- fromAgdaHighlightingRangeToLSPRange :: Range -> LSP.Range
-- fromAgdaHighlightingRangeToLSPRange range = case rangeToIntervalWithFile range of
--   Nothing -> LSP.Range (LSP.Position (-1) (-1)) (LSP.Position (-1) (-1))
--   Just (Interval start end) -> LSP.Range (toLSPPosition start) (toLSPPosition end)

-- toLSPPosition :: Position -> LSP.Position
-- toLSPPosition (Pn _ offset line col) = LSP.Position (fromIntegral line - 1) (fromIntegral col - 1)