{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

-- | Converting generic ranges to Agda's ranges.

module Agda.Interaction.Highlighting.Range
  ( module Agda.Utils.Range
  , rToR
  , rangeToRange
  ) where

import Agda.Syntax.Position qualified as P
import Agda.Utils.Range

-- | Converts a 'P.Range' to a 'Ranges'.

rToR :: P.Range -> Ranges
rToR :: Range -> Ranges
rToR Range
r = [Range] -> Ranges
Ranges ((Interval' () -> Range) -> [Interval' ()] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Interval' () -> Range
iToR (Range -> [Interval' ()]
forall a. Range' a -> [Interval' ()]
P.rangeIntervals Range
r))
  where
  iToR :: Interval' () -> Range
iToR (P.Interval () P.Pn{ posPos :: forall a. Position' a -> Word32
P.posPos = Word32
pos1 } P.Pn{ posPos :: forall a. Position' a -> Word32
P.posPos = Word32
pos2 }) =
    Range { from :: Int
from = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
pos1, to :: Int
to = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
pos2 }

-- | Converts a 'P.Range', seen as a continuous range, to a 'Range'.

rangeToRange :: P.Range -> Range
rangeToRange :: Range -> Range
rangeToRange Range
r =
  case Range -> Maybe (Interval' ())
forall a. Range' a -> Maybe (Interval' ())
P.rangeToInterval Range
r of
    Maybe (Interval' ())
Nothing -> Range { from :: Int
from = Int
0, to :: Int
to = Int
0 }
    Just (P.Interval ()
_ Position' ()
s Position' ()
e) -> Range
      { from :: Int
from = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ Position' () -> Word32
forall a. Position' a -> Word32
P.posPos Position' ()
s
      , to :: Int
to   = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ Position' () -> Word32
forall a. Position' a -> Word32
P.posPos Position' ()
e
      }