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.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 (AbsolutePath path))
(Seq.singleton interval)
where
interval :: IntervalWithoutFile
interval = Interval (toAgdaPositionWithoutFile table start)
(toAgdaPositionWithoutFile table end)
-- | LSP Position -> Agda PositionWithoutFile
toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
toAgdaPositionWithoutFile table (LSP.Position line col) = Pn
()
(fromIntegral (toOffset table (line, 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)