agda-language-server-7: src/Render/Class.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}

module Render.Class
  ( Render (..),
    -- RenderTCM (..),
    renderM,
    renderP,
    renderA,
    renderATop,
  )
where

import Agda.Syntax.Fixity (Precedence (TopCtx))
import qualified Agda.Syntax.Translation.AbstractToConcrete as A
import qualified Agda.TypeChecking.Monad.Base as A
import Agda.Utils.List1 (List1)
import Agda.Utils.List2 (List2)
import           Agda.Syntax.Common.Pretty (Doc)
import qualified Agda.Syntax.Common.Pretty as Doc

import Data.Int (Int32)
import Data.Text (Text)
import Data.Word (Word32)
import GHC.Exts (IsList (toList))
import Render.RichText

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

-- | Typeclass for rendering Inlines
class Render a where
  render :: a -> Inlines
  renderPrec :: Int -> a -> Inlines

  render = renderPrec 0
  renderPrec = const render

-- | Rendering undersome context
-- class RenderTCM a where
--   renderTCM :: a -> Agda.TCM Inlines

-- | Simply "pure . render"
renderM :: (Applicative m, Render a) => a -> m Inlines
renderM = pure . render

-- | Render instances of Pretty
renderP :: (Applicative m, Doc.Pretty a) => a -> m Inlines
renderP = pure . text . Doc.render . Doc.pretty

-- | like 'prettyA'
renderA :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines
renderA x = render <$> A.abstractToConcrete_ x

-- | like 'prettyATop'
renderATop :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines
renderATop x = render <$> A.abstractToConcreteCtx TopCtx x

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

-- | Other instances of Render
instance Render Int where
  render = text . show

instance Render Int32 where
  render = text . show

instance Render Word32 where
  render = text . show

instance Render Integer where
  render = text . show

instance Render Bool where
  render = text . show

instance Render Text where
  render = text . show

instance Render Doc where
  render = text . Doc.render

instance (Render a) => Render (Maybe a) where
  renderPrec p Nothing = mempty
  renderPrec p (Just x) = renderPrec p x

instance (Render a) => Render [a] where
  render xs = "[" <> fsep (punctuate "," (fmap render xs)) <> "]"

instance (Render a) => Render (List1 a) where
  render = render . toList

instance (Render a) => Render (List2 a) where
  render = render . toList