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 (RawName -> Inlines) -> RawName -> Inlines
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 (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
forall a. Monoid a => [a] -> a
mconcat ((NamePart -> Inlines) -> [NamePart] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamePart -> Inlines
forall a. Render a => a -> Inlines
render ([NamePart] -> [Inlines]) -> [NamePart] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ NameParts -> [Item NameParts]
forall l. IsList l => l -> [Item l]
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)
    | Name -> Bool
forall a. Underscore a => a -> Bool
C.isUnderscore Name
m = QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x -- don't print anonymous modules
    | Bool
otherwise      = Name -> Inlines
forall a. Render a => a -> Inlines
render Name
m Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x
  render (C.QName Name
x)  = Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x


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

-- | Abstract 
instance Render A.Name where
  render :: Name -> Inlines
render = Name -> Inlines
forall a. Render a => a -> Inlines
render (Name -> Inlines) -> (Name -> Name) -> Name -> Inlines
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 ([Inlines] -> Inlines) -> (QName -> [Inlines]) -> QName -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"." ([Inlines] -> [Inlines])
-> (QName -> [Inlines]) -> QName -> [Inlines]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Inlines) -> [Name] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Inlines
forall a. Render a => a -> Inlines
render ([Name] -> [Inlines]) -> (QName -> [Name]) -> QName -> [Inlines]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Name -> [Item (List1 Name)]
List1 Name -> [Name]
forall l. IsList l => l -> [Item l]
Agda.toList (List1 Name -> [Name]) -> (QName -> List1 Name) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 Name
A.qnameToList