{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeSynonymInstances #-}
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.Utils.Pretty (Doc)
import qualified Agda.Utils.Pretty as Doc

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

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

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

  render = forall a. Render a => Int -> a -> Inlines
renderPrec Int
0
  renderPrec = forall a b. a -> b -> a
const forall a. Render a => a -> Inlines
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 :: forall (m :: * -> *) a. (Applicative m, Render a) => a -> m Inlines
renderM = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render

-- | Render instances of Pretty
renderP :: (Applicative m, Doc.Pretty a) => a -> m Inlines
renderP :: forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Inlines
renderP = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
Doc.render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
Doc.pretty

-- | like 'prettyA'
renderA :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines
renderA :: forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderA a
x = forall a. Render a => a -> Inlines
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
A.abstractToConcrete_ a
x 

-- | like 'prettyATop'
renderATop :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines
renderATop :: forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop a
x = forall a. Render a => a -> Inlines
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
Precedence -> a -> m (ConOfAbs a)
A.abstractToConcreteCtx Precedence
TopCtx a
x

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

-- | Other instances of Render
instance Render Int where
  render :: Int -> Inlines
render = String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

instance Render Int32 where
  render :: Int32 -> Inlines
render = String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

instance Render Integer where
  render :: Integer -> Inlines
render = String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

instance Render Bool where
  render :: Bool -> Inlines
render = String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

instance Render Doc where
  render :: Doc -> Inlines
render = String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
Doc.render

instance Render a => Render [a] where
  render :: [a] -> Inlines
render [a]
xs = Inlines
"[" forall a. Semigroup a => a -> a -> a
<> [Inlines] -> Inlines
fsep (Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
xs)) forall a. Semigroup a => a -> a -> a
<> Inlines
"]"
instance Render a => Render (List1 a) where
  render :: List1 a -> Inlines
render = forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
toList

instance Render a => Render (List2 a) where
  render :: List2 a -> Inlines
render = forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
toList