{-# LANGUAGE CPP #-}
{-# 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 (String -> Inlines)
-> (AbsolutePath -> String) -> AbsolutePath -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath

#if MIN_VERSION_Agda(2,6,3)
instance Render RangeFile where
  render :: RangeFile -> Inlines
render = AbsolutePath -> Inlines
forall a. Render a => a -> Inlines
render (AbsolutePath -> Inlines)
-> (RangeFile -> AbsolutePath) -> RangeFile -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeFile -> AbsolutePath
rangeFilePath  -- TODO rangeFileName ?
#endif

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

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) = Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
l Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"," Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
c
  render (Pn (Strict.Just a
f) Int32
_ Int32
l Int32
c) =
    a -> Inlines
forall a. Render a => a -> Inlines
render a
f Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
":" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
l Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"," Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
c

instance Render PositionWithoutFile where
  render :: PositionWithoutFile -> Inlines
render (Pn () Int32
_ Int32
l Int32
c) = Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
l Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"," Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
c

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

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

      end :: Inlines
end
        | Int32
sl Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
== Int32
el = Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
ec
        | Bool
otherwise = Int32 -> Inlines
forall a. Render a => a -> Inlines
render Int32
el Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"," Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Int32 -> Inlines
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 Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> IntervalWithoutFile -> Inlines
forall a. Render a => a -> Inlines
render (() -> Interval' (Maybe a) -> IntervalWithoutFile
forall a b. a -> Interval' b -> Interval' a
setIntervalFile () Interval' (Maybe a)
i)
    where
      file :: Inlines
      file :: Inlines
file = case Position' (Maybe a) -> Maybe a
forall a. Position' a -> a
srcFile Position' (Maybe a)
s of
        Maybe a
Strict.Nothing -> Inlines
forall a. Monoid a => a
mempty
        Strict.Just a
f -> a -> Inlines
forall a. Render a => a -> Inlines
render a
f Inlines -> Inlines -> Inlines
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 = Inlines
-> (Interval' (Maybe a) -> Inlines)
-> Maybe (Interval' (Maybe a))
-> Inlines
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Inlines
forall a. Monoid a => a
mempty Interval' (Maybe a) -> Inlines
forall a. Render a => a -> Inlines
render (Range' (Maybe a) -> Maybe (Interval' (Maybe a))
forall a. Range' a -> Maybe (Interval' a)
rangeToIntervalWithFile Range' (Maybe a)
r)