{-# 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 = Int -> a -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
0
  renderPrec = (a -> Inlines) -> Int -> a -> Inlines
forall a b. a -> b -> a
const a -> Inlines
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 = Inlines -> m Inlines
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inlines -> m Inlines) -> (a -> Inlines) -> a -> m Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Inlines
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 = Inlines -> m Inlines
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inlines -> m Inlines) -> (a -> Inlines) -> a -> m Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Inlines
text (String -> Inlines) -> (a -> String) -> a -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
Doc.render (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
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 = c -> Inlines
forall a. Render a => a -> Inlines
render (c -> Inlines) -> TCMT IO c -> TCM Inlines
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> TCMT IO (ConOfAbs a)
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 = c -> Inlines
forall a. Render a => a -> Inlines
render (c -> Inlines) -> TCMT IO c -> TCM Inlines
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> TCMT IO (ConOfAbs a)
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 (String -> Inlines) -> (Int -> String) -> Int -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show

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

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

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

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

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