{-# LANGUAGE CPP #-}

module Render.Common where

import Agda.Syntax.Common
    ( Named(namedThing),
      Hiding(NotHidden, Hidden, Instance),
      LensHiding(getHiding),
      RewriteEqn'(..),
      MetaId(MetaId),
      LensQuantity(getQuantity),
      Quantity(..),
      LensRelevance(getRelevance),
      Relevance(..),
      Induction(..),
      Cohesion(..),
      QωOrigin(..),
      LensCohesion(getCohesion),
      NameId(..) )
import qualified Agda.Utils.Null as Agda
import           Agda.Utils.List1 (toList)
import           Agda.Utils.Functor ((<&>))

import Render.Class
import Render.RichText

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

-- | NameId
instance Render NameId where
  render :: NameId -> Inlines
render (NameId Word64
n ModuleNameHash
m) = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Word64
n forall a. [a] -> [a] -> [a]
++ [Char]
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ModuleNameHash
m

-- | MetaId
instance Render MetaId where
#if MIN_VERSION_Agda(2,6,3)
  render :: MetaId -> Inlines
render (MetaId Word64
n ModuleNameHash
m) = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Word64
n forall a. [a] -> [a] -> [a]
++ [Char]
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ModuleNameHash
m
#else
  render (MetaId n) = text $ "_" ++ show n
#endif

-- | Relevance
instance Render Relevance where
  render :: Relevance -> Inlines
render Relevance
Relevant = forall a. Monoid a => a
mempty
  render Relevance
Irrelevant = Inlines
"."
  render Relevance
NonStrict = Inlines
".."

-- | Quantity
instance Render Quantity where
  render :: Quantity -> Inlines
render = \case
    Quantity0 Q0Origin
o ->
      let s :: [Char]
s = forall a. Show a => a -> [Char]
show Q0Origin
o
       in if forall a. Null a => a -> Bool
Agda.null Q0Origin
o
            then Inlines
"@0"
            else [Char] -> Inlines
text [Char]
s
    Quantity1 Q1Origin
o ->
      let s :: [Char]
s = forall a. Show a => a -> [Char]
show Q1Origin
o
       in if forall a. Null a => a -> Bool
Agda.null Q1Origin
o
            then Inlines
"@1"
            else [Char] -> Inlines
text [Char]
s
    Quantityω QωOrigin
o -> forall a. Render a => a -> Inlines
render QωOrigin
o

instance Render QωOrigin where
  render :: QωOrigin -> Inlines
render = \case
    QωOrigin
QωInferred -> forall a. Monoid a => a
mempty
    Qω{}       -> Inlines
"@ω"
    QωPlenty{} -> Inlines
"@plenty"

instance Render Cohesion where
  render :: Cohesion -> Inlines
render Cohesion
Flat   = Inlines
"@♭"
  render Cohesion
Continuous = forall a. Monoid a => a
mempty
  render Cohesion
Squash  = Inlines
"@⊤"

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

-- | From 'prettyHiding'
--   @renderHiding info visible text@ puts the correct braces
--   around @text@ according to info @info@ and returns
--   @visible text@ if the we deal with a visible thing.
renderHiding :: LensHiding a => a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding :: forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding a
a Inlines -> Inlines
parensF =
  case forall a. LensHiding a => a -> Hiding
getHiding a
a of
    Hiding
Hidden -> Inlines -> Inlines
braces'
    Instance {} -> Inlines -> Inlines
dbraces
    Hiding
NotHidden -> Inlines -> Inlines
parensF

renderRelevance :: LensRelevance a => a -> Inlines -> Inlines
renderRelevance :: forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance a
a Inlines
d =
  if forall a. Show a => a -> [Char]
show Inlines
d forall a. Eq a => a -> a -> Bool
== [Char]
"_" then Inlines
d else forall a. Render a => a -> Inlines
render (forall a. LensRelevance a => a -> Relevance
getRelevance a
a) forall a. Semigroup a => a -> a -> a
<> Inlines
d

renderQuantity :: LensQuantity a => a -> Inlines -> Inlines
renderQuantity :: forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity a
a Inlines
d =
  if forall a. Show a => a -> [Char]
show Inlines
d forall a. Eq a => a -> a -> Bool
== [Char]
"_" then Inlines
d else forall a. Render a => a -> Inlines
render (forall a. LensQuantity a => a -> Quantity
getQuantity a
a) Inlines -> Inlines -> Inlines
<+> Inlines
d

renderCohesion :: LensCohesion a => a -> Inlines -> Inlines
renderCohesion :: forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion a
a Inlines
d =
  if forall a. Show a => a -> [Char]
show Inlines
d forall a. Eq a => a -> a -> Bool
== [Char]
"_" then Inlines
d else forall a. Render a => a -> Inlines
render (forall a. LensCohesion a => a -> Cohesion
getCohesion a
a) Inlines -> Inlines -> Inlines
<+> Inlines
d

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


instance (Render p, Render e) => Render (RewriteEqn' qn nm p e) where
  render :: RewriteEqn' qn nm p e -> Inlines
render = \case
    Rewrite List1 (qn, e)
es   -> Inlines -> [Inlines] -> Inlines
prefixedThings ([Char] -> Inlines
text [Char]
"rewrite") (forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall l. IsList l => l -> [Item l]
toList List1 (qn, e)
es)
    Invert qn
_ List1 (Named nm (p, e))
pes -> Inlines -> [Inlines] -> Inlines
prefixedThings ([Char] -> Inlines
text [Char]
"invert") (forall l. IsList l => l -> [Item l]
toList List1 (Named nm (p, e))
pes forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (\ (p
p, e
e) -> forall a. Render a => a -> Inlines
render p
p Inlines -> Inlines -> Inlines
<+> Inlines
"<-" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render e
e) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing)

prefixedThings :: Inlines -> [Inlines] -> Inlines
prefixedThings :: Inlines -> [Inlines] -> Inlines
prefixedThings Inlines
kw = \case
  [] -> forall a. Monoid a => a
mempty
  (Inlines
doc : [Inlines]
docs) -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ (Inlines
kw Inlines -> Inlines -> Inlines
<+> Inlines
doc) forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines
"|" Inlines -> Inlines -> Inlines
<+>) [Inlines]
docs

instance Render Induction where
  render :: Induction -> Inlines
render Induction
Inductive   = Inlines
"inductive"
  render Induction
CoInductive = Inlines
"coinductive"