{-# 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 ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Word64 -> [Char]
forall a. Show a => a -> [Char]
show Word64
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleNameHash -> [Char]
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 ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. Show a => a -> [Char]
show Word64
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleNameHash -> [Char]
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 = Inlines
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 = Q0Origin -> [Char]
forall a. Show a => a -> [Char]
show Q0Origin
o
       in if Q0Origin -> Bool
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 = Q1Origin -> [Char]
forall a. Show a => a -> [Char]
show Q1Origin
o
       in if Q1Origin -> Bool
forall a. Null a => a -> Bool
Agda.null Q1Origin
o
            then Inlines
"@1"
            else [Char] -> Inlines
text [Char]
s
    Quantityω QωOrigin
o -> QωOrigin -> Inlines
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 -> Inlines
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 = Inlines
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 a -> Hiding
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 Inlines -> [Char]
forall a. Show a => a -> [Char]
show Inlines
d [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"_" then Inlines
d else Relevance -> Inlines
forall a. Render a => a -> Inlines
render (a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance a
a) Inlines -> Inlines -> Inlines
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 Inlines -> [Char]
forall a. Show a => a -> [Char]
show Inlines
d [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"_" then Inlines
d else Quantity -> Inlines
forall a. Render a => a -> Inlines
render (a -> Quantity
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 Inlines -> [Char]
forall a. Show a => a -> [Char]
show Inlines
d [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"_" then Inlines
d else Cohesion -> Inlines
forall a. Render a => a -> Inlines
render (a -> Cohesion
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") (e -> Inlines
forall a. Render a => a -> Inlines
render (e -> Inlines) -> ((qn, e) -> e) -> (qn, e) -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (qn, e) -> e
forall a b. (a, b) -> b
snd ((qn, e) -> Inlines) -> [(qn, e)] -> [Inlines]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (qn, e) -> [Item (List1 (qn, e))]
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") (List1 (Named nm (p, e)) -> [Item (List1 (Named nm (p, e)))]
forall l. IsList l => l -> [Item l]
toList List1 (Named nm (p, e))
pes [Named nm (p, e)] -> (Named nm (p, e) -> Inlines) -> [Inlines]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (\ (p
p, e
e) -> p -> Inlines
forall a. Render a => a -> Inlines
render p
p Inlines -> Inlines -> Inlines
<+> Inlines
"<-" Inlines -> Inlines -> Inlines
<+> e -> Inlines
forall a. Render a => a -> Inlines
render e
e) ((p, e) -> Inlines)
-> (Named nm (p, e) -> (p, e)) -> Named nm (p, e) -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named nm (p, e) -> (p, e)
forall name a. Named name a -> a
namedThing)

prefixedThings :: Inlines -> [Inlines] -> Inlines
prefixedThings :: Inlines -> [Inlines] -> Inlines
prefixedThings Inlines
kw = \case
  [] -> Inlines
forall a. Monoid a => a
mempty
  (Inlines
doc : [Inlines]
docs) -> [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Inlines
kw Inlines -> Inlines -> Inlines
<+> Inlines
doc) Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (Inlines -> Inlines) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
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"