content: {-# LANGUAGE CPP #-}
  
  module Render.Common where
  
  import Agda.Syntax.Common
    ( Cohesion (..),
      Erased (..),
      Hiding (Hidden, Instance, NotHidden),
      Induction (..),
      LensCohesion (getCohesion),
      LensHiding (getHiding),
      LensQuantity (getQuantity),
      LensRelevance (getRelevance),
      Lock (..),
  
      LockOrigin (..),
  
      MetaId (MetaId),
      NameId (..),
      Named (namedThing),
  #if MIN_VERSION_Agda(2,7,0)
      OverlapMode (..),
  #endif
  
      Quantity (..),
      QωOrigin (..),
      Relevance (..),
      RewriteEqn' (..),
      asQuantity,
  #if MIN_VERSION_Agda(2,8,0)
      OriginRelevant (..), 
      OriginIrrelevant (..), 
      OriginShapeIrrelevant (..), 
      PolarityModality (..),
      ModalPolarity (..),
  #endif
    )
  import Agda.Utils.Functor ((<&>))
  import Agda.Utils.List1 (toList)
  import qualified Agda.Utils.List1 as List1
  import qualified Agda.Utils.Null as Agda
  import Render.Class
  import Render.RichText
  import Data.Text (Text)
  
  --------------------------------------------------------------------------------
  
  -- | NameId
  instance Render NameId where
    render (NameId n m) = text $ show n ++ "@" ++ show m
  
  -- | MetaId
  instance Render MetaId where
    render (MetaId n m) = text $ "_" ++ show n ++ "@" ++ show m
  
  #if MIN_VERSION_Agda(2,8,0)
  -- | OriginRelevant
  instance Render OriginRelevant where
    render = \case
      ORelInferred {} -> mempty
      ORelRelevant {} -> "@relevant"
  
  instance Render OriginIrrelevant where
    render = \case
      OIrrInferred {} -> mempty
      OIrrDot {} -> "."
      OIrrIrr {} -> "@irr"
      OIrrIrrelevant {} -> "@irrelevant"
  
  instance Render OriginShapeIrrelevant where
    render = \case
      OShIrrInferred {} -> mempty
      OShIrrDotDot {} -> ".."
      OShIrrShIrr {} -> "@shirr"
      OShIrrShapeIrrelevant {} -> "@shape-irrelevant"
  #endif
  
  -- | Relevance
  #if MIN_VERSION_Agda(2,8,0)
  instance Render Relevance where
    render (Relevant o) = render o
    render (Irrelevant o) = Agda.ifNull (render o) "." id
    render (ShapeIrrelevant o) = Agda.ifNull (render o) ".." id
  #else
  instance Render Relevance where
    render Relevant = mempty
    render Irrelevant = "."
    render NonStrict = ".."
  #endif
  
  -- | Quantity
  instance Render Quantity where
    render = \case
      Quantity0 o ->
        let s = show o
         in if Agda.null o
              then "@0"
              else text s
      Quantity1 o ->
        let s = show o
         in if Agda.null o
              then "@1"
              else text s
      Quantityω o -> render o
  
  instance Render QωOrigin where
    render = \case
      QωInferred -> mempty
      Qω {} -> "@ω"
      QωPlenty {} -> "@plenty"
  
  instance Render Cohesion where
    render Flat = "@♭"
    render Continuous = mempty
    render Squash = "@⊤"
  
  -- | Polarity
  
  #if MIN_VERSION_Agda(2,8,0)
  instance Render ModalPolarity where
    render p = case p of
      UnusedPolarity -> "@unused"
      StrictlyPositive -> "@++"
      Positive -> "@+"
      Negative -> "@-"
      MixedPolarity -> mempty
  
  instance Render PolarityModality where
    render (PolarityModality p _ _) = render p
  #endif
  
  --------------------------------------------------------------------------------
  
  #if MIN_VERSION_Agda(2,7,0)
  instance Render OverlapMode where
    render = \case
      Overlappable -> "OVERLAPPABLE"
      Overlapping -> "OVERLAPPING"
      Incoherent -> "INCOHERENT"
      Overlaps -> "OVERLAPS"
      FieldOverlap -> "overlap"
      DefaultOverlap -> mempty
  #endif
  
  --------------------------------------------------------------------------------
  
  -- | 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 a parensF =
    case getHiding a of
      Hidden -> braces'
      Instance {} -> dbraces
      NotHidden -> parensF
  
  renderRelevance :: (LensRelevance a) => a -> Inlines -> Inlines
  renderRelevance a d =
    if show d == "_" then d else render (getRelevance a) <> d
  
  renderQuantity :: (LensQuantity a) => a -> Inlines -> Inlines
  renderQuantity a d =
    if show d == "_" then d else render (getQuantity a) <+> d
  
  instance Render Lock where
    render = \case
      IsLock LockOLock -> "@lock"
      IsLock LockOTick -> "@tick"
      IsNotLock -> mempty
  
  #if MIN_VERSION_Agda(2,7,0)
  renderErased :: Erased -> Inlines -> Inlines
  renderErased = renderQuantity . asQuantity
  #endif
  
  renderCohesion :: (LensCohesion a) => a -> Inlines -> Inlines
  renderCohesion a d =
    if show d == "_" then d else render (getCohesion a) <+> d
  
  --------------------------------------------------------------------------------
  
  instance (Render p, Render e) => Render (RewriteEqn' qn nm p e) where
    render = \case
      Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> toList es)
      Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\(p, e) -> render p <+> "<-" <+> render e) . namedThing)
  #if MIN_VERSION_Agda(2,7,0)
      LeftLet pes  -> prefixedThings (text "using") [render p <+> "<-" <+> render e | (p, e) <- List1.toList pes]
  #endif
  
  prefixedThings :: Inlines -> [Inlines] -> Inlines
  prefixedThings kw = \case
    [] -> mempty
    (doc : docs) -> fsep $ (kw <+> doc) : fmap ("|" <+>) docs
  
  instance Render Induction where
    render Inductive = "inductive"
    render CoInductive = "coinductive"
  