{-# LANGUAGE FlexibleInstances #-}

module Render.Position where

import Agda.Syntax.Position
import Agda.Utils.FileName
import qualified Data.Strict.Maybe as Strict
import Render.Class
import Render.RichText

instance Render AbsolutePath where
  render :: AbsolutePath -> Inlines
render = String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath

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

instance Render a => Render (Position' (Strict.Maybe a)) where
  render :: Position' (Maybe a) -> Inlines
render (Pn Maybe a
Strict.Nothing Int32
_ Int32
l Int32
c) = forall a. Render a => a -> Inlines
render Int32
l forall a. Semigroup a => a -> a -> a
<> Inlines
"," forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Int32
c
  render (Pn (Strict.Just a
f) Int32
_ Int32
l Int32
c) =
    forall a. Render a => a -> Inlines
render a
f forall a. Semigroup a => a -> a -> a
<> Inlines
":" forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Int32
l forall a. Semigroup a => a -> a -> a
<> Inlines
"," forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Int32
c

instance Render PositionWithoutFile where
  render :: PositionWithoutFile -> Inlines
render PositionWithoutFile
p = forall a. Render a => a -> Inlines
render (PositionWithoutFile
p {srcFile :: Maybe AbsolutePath
srcFile = forall a. Maybe a
Strict.Nothing} :: Position)

instance Render IntervalWithoutFile where
  render :: IntervalWithoutFile -> Inlines
render (Interval PositionWithoutFile
s PositionWithoutFile
e) = Inlines
start forall a. Semigroup a => a -> a -> a
<> Inlines
"-" forall a. Semigroup a => a -> a -> a
<> Inlines
end
    where
      sl :: Int32
sl = forall a. Position' a -> Int32
posLine PositionWithoutFile
s
      el :: Int32
el = forall a. Position' a -> Int32
posLine PositionWithoutFile
e
      sc :: Int32
sc = forall a. Position' a -> Int32
posCol PositionWithoutFile
s
      ec :: Int32
ec = forall a. Position' a -> Int32
posCol PositionWithoutFile
e

      start :: Inlines
start = forall a. Render a => a -> Inlines
render Int32
sl forall a. Semigroup a => a -> a -> a
<> Inlines
"," forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Int32
sc

      end :: Inlines
end
        | Int32
sl forall a. Eq a => a -> a -> Bool
== Int32
el = forall a. Render a => a -> Inlines
render Int32
ec
        | Bool
otherwise = forall a. Render a => a -> Inlines
render Int32
el forall a. Semigroup a => a -> a -> a
<> Inlines
"," forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Int32
ec

instance Render a => Render (Interval' (Strict.Maybe a)) where
  render :: Interval' (Maybe a) -> Inlines
render i :: Interval' (Maybe a)
i@(Interval Position' (Maybe a)
s Position' (Maybe a)
_) = Inlines
file forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render (forall a b. a -> Interval' b -> Interval' a
setIntervalFile () Interval' (Maybe a)
i)
    where
      file :: Inlines
      file :: Inlines
file = case forall a. Position' a -> a
srcFile Position' (Maybe a)
s of
        Maybe a
Strict.Nothing -> forall a. Monoid a => a
mempty
        Strict.Just a
f -> forall a. Render a => a -> Inlines
render a
f forall a. Semigroup a => a -> a -> a
<> Inlines
":"

instance Render a => Render (Range' (Strict.Maybe a)) where
  render :: Range' (Maybe a) -> Inlines
render Range' (Maybe a)
r = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. Render a => a -> Inlines
render (forall a. Range' a -> Maybe (Interval' a)
rangeToIntervalWithFile Range' (Maybe a)
r)