content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DerivingVia #-}
  {-# LANGUAGE RoleAnnotations #-}
  {-# LANGUAGE TypeFamilies #-}
  
  -- | Strongly typed indices and offsets.
  --
  -- The goal of this module is to make it as easy as possible to keep track
  -- of the various indexing schemes used by functions in the nvim API.
  --
  -- The core abstraction is the type 'Index' tagged with the sort of things it
  -- is indexing (@Byte@, @CodePoint@, @Line@) and whether things are 0-indexed
  -- or 1-indexed.
  --
  -- Two constructors and two destructors are provided: 'toZeroIndexed',
  -- 'toOneIndexed', 'fromZeroIndexed', and 'fromOneIndexed'.  They should only
  -- be used to make external API calls, to unwrap input indices and to wrap
  -- output indices. The names of those functions are self-documenting, indicating
  -- the indexing scheme used by every index that goes in and out of the external
  -- API.
  --
  -- Within Cornelis, indices remain typed at all times, using dedicated functions
  -- to convert between 0/1-indexing ('zeroIndex', 'oneIndex') and between
  -- @Byte@ and @CodePoint@ indexing ('toByte', 'fromByte').
  --
  -- Usually, indices are relative to a common origin (beginning of the same buffer
  -- or line), so it doesn't make sense to add them. There is a separate type of
  -- 'Offset' which can be added to indices using the operator @('.+')@.
  -- And @('.-.')@ gives the offset between two indices.
  --
  -- @
  -- i :: Index 'Byte 'ZeroIndexed
  -- i .+ Offset 42 :: Index 'Byte 'ZeroIndexed
  -- @
  --
  -- Types of 'Pos'isitions (pairs of line and column indices) and 'Interval's
  -- (pairs of positions or indices) are also provided, and should be used
  -- as much as possible to reduce the likelihood of mixing up indices.
  --
  -- When talking about 'Pos', "(i,j)-indexed" means "i-indexed lines, j-indexed
  -- columns".
  --
  -- Agda's indexing scheme (codepoints, (1,1)-indexed) is the preferred one
  -- (0- vs 1-indexing is heavily checked, so it doesn't matter much which
  -- we choose; codepoint indexing is preferred for manipulating unicode text
  -- (fewer invalid states than byte indexing)).
  --
  -- A secondary indexing scheme is bytes, (0,0)-indexed, used as a unified
  -- low-level representation right before talking to the nvim API.
  module Cornelis.Offsets
    ( Index()
    , Indexing(..)
    , Unit(..)
    , Offset(..)
    , Pos(..)
    , Interval(..)
    , LineNumber
    , AgdaIndex
    , AgdaOffset
    , AgdaPos
    , AgdaInterval
    , VimIndex
    , VimOffset
    , VimPos
    , VimInterval
    , toZeroIndexed
    , toOneIndexed
    , fromZeroIndexed
    , fromOneIndexed
    , zeroIndex
    , oneIndex
    , incIndex
    , (.+)
    , (.-.)
    , offsetPlus
    , textToBytes
    , charToBytes
    , toBytes
    , fromBytes
    , containsPoint
    , addCol
    ) where
  
  import           Data.Aeson (FromJSON)
  import qualified Data.ByteString as BS
  import           Data.Coerce (coerce)
  import           Data.Monoid (Sum(..))
  import qualified Data.Text as T
  import           Data.Text.Encoding (encodeUtf8)
  import           GHC.Generics (Generic)
  import           GHC.Stack (HasCallStack)
  import           GHC.Show (showSpace)
  import           Prettyprinter (Pretty)
  import qualified DiffLoc as D
  
  -- | Indexing scheme: whether the first index is zero or one.
  data Indexing = OneIndexed | ZeroIndexed
  
  -- | What are we counting?
  data Unit = Byte | CodePoint | Line
  
  -- | The constructor is hidden, use 'toZeroIndexed' and 'toOneIndexed' to construct it,
  -- and 'fromZeroIndexed' and 'fromOneIndexed' to destruct it.
  newtype Index (e :: Unit) (i :: Indexing) = Index Int
    deriving newtype (Eq, Ord, Show, Read, FromJSON, Pretty)
  
  type role Index nominal nominal
  
  -- | It doesn't seem worth the trouble to hide this constructor.
  newtype Offset (e :: Unit) = Offset Int
    deriving newtype (Eq, Ord, Show, Read, FromJSON, Pretty)
    deriving (Semigroup, Monoid) via Sum Int
  
  type role Offset nominal
  
  -- | Position in a text file as line-column numbers. This type is indexed by
  -- the units of the columns (@Byte@ or @CodePoint@) and by the indexing scheme
  -- of lines and columns.
  data Pos e i j = Pos
    { p_line :: Index 'Line i
    , p_col :: Index e j
    } deriving (Eq, Ord, Generic)
  
  instance Show (Pos e i j) where
    showsPrec n (Pos l c) =
      showParen (n >= 11) $ showString "Pn () 0 " . showsPrec 11 l . showSpace . showsPrec 11 c
  
  data Interval p = Interval { iStart, iEnd :: !p }
    deriving (Eq, Ord, Functor, Foldable, Traversable, Generic)
  
  instance Show p => Show (Interval p) where
    showsPrec n (Interval s e) =
      showParen (n >= 11) $ showString "Interval () " . showsPrec 11 s . showSpace . showsPrec 11 e
  
  -- Common specializations
  
  type LineNumber = Index 'Line
  
  type AgdaIndex = Index 'CodePoint 'OneIndexed
  type AgdaOffset = Offset 'CodePoint
  type AgdaPos = Pos 'CodePoint 'OneIndexed 'OneIndexed
  type AgdaInterval = Interval AgdaPos
  
  type VimIndex = Index 'Byte 'ZeroIndexed
  type VimOffset = Offset 'Byte
  type VimPos = Pos 'Byte 'ZeroIndexed 'ZeroIndexed
  type VimInterval = Interval VimPos
  
  -- To pass indices to and from external sources.
  
  -- | Mark a raw index as zero-indexed.
  toZeroIndexed :: Integral a => a -> Index e 'ZeroIndexed
  toZeroIndexed a = Index (fromIntegral a)
  
  -- | Mark a raw index as one-indexed.
  toOneIndexed :: Integral a => a -> Index e 'OneIndexed
  toOneIndexed a = Index (fromIntegral a)
  
  -- | Unwrap a raw zero-indexed index.
  fromZeroIndexed :: Num a => Index e 'ZeroIndexed -> a
  fromZeroIndexed (Index a) = fromIntegral a
  
  -- | Unwrap a raw zero-indexed index.
  fromOneIndexed :: Num a => Index e 'OneIndexed -> a
  fromOneIndexed (Index a) = fromIntegral a
  
  -- | Convert from one- to zero-indexed.
  zeroIndex :: Index e 'OneIndexed -> Index e 'ZeroIndexed
  zeroIndex (Index i) = Index (i - 1)
  
  -- | Convert from zero- to one-indexed.
  oneIndex :: Index e 'ZeroIndexed -> Index e 'OneIndexed
  oneIndex (Index i) = Index (i + 1)
  
  -- | Increment index.
  incIndex :: Index e i -> Index e i
  incIndex (Index i) = Index (i + 1)
  
  -- | Add an offset to an index.
  (.+) :: Index e i -> Offset e -> Index e i
  Index i .+ Offset n = Index (i + n)
  
  (.-.) :: Index e i -> Index e i -> Offset e
  Index i .-. Index j = Offset (i - j)
  
  --
  
  offsetPlus :: Offset a -> Offset a -> Offset a
  offsetPlus = coerce $ (+) @Int
  
  --
  
  containsPoint :: Ord p => Interval p -> p -> Bool
  containsPoint (Interval s e) p = s <= p && p < e
  
  -- | Number of bytes in a 'T.Text'.
  textToBytes :: T.Text -> Int
  textToBytes t = BS.length (encodeUtf8 t)
  
  -- | Number of bytes in a 'Char'.
  charToBytes :: Char -> Int
  charToBytes c = textToBytes (T.singleton c)
  
  ------------------------------------------------------------------------------
  -- | Convert a character-based index into a byte-indexed one
  toBytes :: T.Text -> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed
  toBytes s (Index i) = Index $ textToBytes $ T.take (fromIntegral i) s
  
  ------------------------------------------------------------------------------
  -- | Convert a byte-based index into a character-indexed one.
  fromBytes :: HasCallStack => T.Text -> Index 'Byte 'ZeroIndexed -> Index 'CodePoint 'ZeroIndexed
  fromBytes t (Index i) | i < 0 = error $ "from bytes underflow" <> show (t, i)
  fromBytes _ (Index 0) = Index 0
  fromBytes t (Index i) | Just (c, str) <- T.uncons t =
    let diff = BS.length $ encodeUtf8 $ T.singleton c
     in case i - diff >= 0 of
          True -> Index $ 1 + coerce (fromBytes str (Index (i - diff)))
          -- We ran out of bytes in the middle of a multibyte character. Just
          -- return the one we're on, and don't underflow!
          False -> Index 0
  fromBytes t i = error $ "missing bytes: " <> show (t, i)
  
  addCol :: Pos e i j -> Offset e -> Pos e i j
  addCol (Pos l c) dc = Pos l (c .+ dc)
  
  -- | Ordered monoid action of offsets on indices.
  instance D.Amor (Index e i) where
    type Trans (Index e i) = Offset e
    (.+) = (Cornelis.Offsets..+)
    i .-.? j | i >= j = Just (i .-. j)
             | otherwise = Nothing
  
  -- | The zero in zero-indexing.
  instance D.Origin (Index e 'ZeroIndexed) where
    origin = toZeroIndexed (0 :: Int)
  