module Render.Name where

import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Common   as C
import qualified Agda.Utils.List1     as Agda

import Render.Class
import Render.RichText

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

-- | Concrete 
instance Render C.NamePart where
  render :: NamePart -> Inlines
render NamePart
C.Hole = Inlines
"_"
  render (C.Id RawName
s) = RawName -> Inlines
text forall a b. (a -> b) -> a -> b
$ RawName -> RawName
C.rawNameToString RawName
s

-- glueing name parts together 
instance Render C.Name where
  render :: Name -> Inlines
render (C.Name Range
range NameInScope
_inScope NameParts
xs) = Range -> Inlines -> Inlines
linkRange Range
range forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
Agda.toList NameParts
xs)
  render (C.NoName Range
_ NameId
_) = Inlines
"_"

instance Render C.QName where
  render :: QName -> Inlines
render (C.Qual Name
m QName
x)
    | forall a. Underscore a => a -> Bool
C.isUnderscore Name
m = forall a. Render a => a -> Inlines
render QName
x -- don't print anonymous modules
    | Bool
otherwise      = forall a. Render a => a -> Inlines
render Name
m forall a. Semigroup a => a -> a -> a
<> Inlines
"." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render QName
x
  render (C.QName Name
x)  = forall a. Render a => a -> Inlines
render Name
x


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

-- | Abstract 
instance Render A.Name where
  render :: Name -> Inlines
render = forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete

instance Render A.QName where
  render :: QName -> Inlines
render = [Inlines] -> Inlines
hcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
Agda.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 Name
A.qnameToList