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 :: ToOffset -> Text -> Range -> Range
toAgdaRange ToOffset
table Text
path (LSP.Range Position
start Position
end) = Maybe AbsolutePath -> Seq IntervalWithoutFile -> Range
forall a. a -> Seq IntervalWithoutFile -> Range' a
Range
  (AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Strict.Just (Text -> AbsolutePath
AbsolutePath Text
path))
  (IntervalWithoutFile -> Seq IntervalWithoutFile
forall a. a -> Seq a
Seq.singleton IntervalWithoutFile
interval)
 where
  interval :: IntervalWithoutFile
  interval :: IntervalWithoutFile
interval = Position' () -> Position' () -> IntervalWithoutFile
forall a. Position' a -> Position' a -> Interval' a
Interval (ToOffset -> Position -> Position' ()
toAgdaPositionWithoutFile ToOffset
table Position
start)
                      (ToOffset -> Position -> Position' ()
toAgdaPositionWithoutFile ToOffset
table Position
end)

-- | LSP Position -> Agda PositionWithoutFile
toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
toAgdaPositionWithoutFile :: ToOffset -> Position -> Position' ()
toAgdaPositionWithoutFile ToOffset
table (LSP.Position Int
line Int
col) = () -> Int32 -> Int32 -> Int32 -> Position' ()
forall a. a -> Int32 -> Int32 -> Int32 -> Position' a
Pn
  ()
  (Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ToOffset -> (Int, Int) -> Int
toOffset ToOffset
table (Int
line, Int
col)) Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
  (Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
line Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)
  (Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
col Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
1)

prettyPositionWithoutFile :: PositionWithoutFile -> String
prettyPositionWithoutFile :: Position' () -> String
prettyPositionWithoutFile pos :: Position' ()
pos@(Pn () Int32
offset Int32
_line Int32
_col) =
  String
"[" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Position' () -> String
forall a. Show a => a -> String
show Position' ()
pos String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"-" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int32 -> String
forall a. Show a => a -> String
show Int32
offset String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"]"

--------------------------------------------------------------------------------
-- | 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 { ToOffset -> IntMap Int
unToOffset :: IntMap Int }

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

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

  go :: Accum -> Char -> Accum
  go :: Accum -> Char -> Accum
go (Accum (Just Char
'\r') Int
n Int
l IntMap Int
table) Char
'\n' =
    Maybe Char -> Int -> Int -> IntMap Int -> Accum
Accum (Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\n') (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Int
l ((Int -> Maybe Int) -> IntMap Int -> IntMap Int
forall a. (a -> Maybe a) -> IntMap a -> IntMap a
IntMap.updateMax (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
succ) IntMap Int
table)
  go (Accum Maybe Char
previous Int
n Int
l IntMap Int
table) Char
'\n' =
    Maybe Char -> Int -> Int -> IntMap Int -> Accum
Accum (Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\n') (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) IntMap Int
table)
  go (Accum Maybe Char
previous Int
n Int
l IntMap Int
table) Char
'\r' =
    Maybe Char -> Int -> Int -> IntMap Int -> Accum
Accum (Char -> Maybe Char
forall a. a -> Maybe a
Just Char
'\r') (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l) (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) IntMap Int
table)
  go (Accum Maybe Char
previous Int
n Int
l IntMap Int
table) Char
char = Maybe Char -> Int -> Int -> IntMap Int -> Accum
Accum (Char -> Maybe Char
forall a. a -> Maybe a
Just Char
char) (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Int
l IntMap Int
table

-- | (line, col) => offset (zero-based)
toOffset :: ToOffset -> (Int, Int) -> Int
toOffset :: ToOffset -> (Int, Int) -> Int
toOffset (ToOffset IntMap Int
table) (Int
line, Int
col) = case Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
line IntMap Int
table of
  Maybe Int
Nothing     -> Int
col
  Just Int
offset -> Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 { FromOffset -> IntMap Int
unFromOffset :: IntMap Int }

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

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