module Render.TypeChecking where

import Agda.Syntax.Common
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Positivity.Occurrence
import Render.Class
import Render.RichText

instance Render NamedMeta where
  render :: NamedMeta -> Inlines
render (NamedMeta MetaNameSuggestion
"" (MetaId Int
x)) = forall a. Render a => a -> Inlines
render Int
x
  render (NamedMeta MetaNameSuggestion
"_" (MetaId Int
x)) = forall a. Render a => a -> Inlines
render Int
x
  render (NamedMeta MetaNameSuggestion
s (MetaId Int
x)) = Inlines
"_" forall a. Semigroup a => a -> a -> a
<> MetaNameSuggestion -> Inlines
text MetaNameSuggestion
s forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Int
x

instance Render Occurrence where
  render :: Occurrence -> Inlines
render =
    MetaNameSuggestion -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      Occurrence
Unused -> MetaNameSuggestion
"_"
      Occurrence
Mixed -> MetaNameSuggestion
"*"
      Occurrence
JustNeg -> MetaNameSuggestion
"-"
      Occurrence
JustPos -> MetaNameSuggestion
"+"
      Occurrence
StrictPos -> MetaNameSuggestion
"++"
      Occurrence
GuardPos -> MetaNameSuggestion
"g+"

instance Render ProblemId where
  render :: ProblemId -> Inlines
render (ProblemId Int
n) = forall a. Render a => a -> Inlines
render Int
n

instance Render Comparison where
  render :: Comparison -> Inlines
render Comparison
CmpEq = Inlines
"="
  render Comparison
CmpLeq = Inlines
"=<"

instance Render Polarity where
  render :: Polarity -> Inlines
render =
    MetaNameSuggestion -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      Polarity
Covariant -> MetaNameSuggestion
"+"
      Polarity
Contravariant -> MetaNameSuggestion
"-"
      Polarity
Invariant -> MetaNameSuggestion
"*"
      Polarity
Nonvariant -> MetaNameSuggestion
"_"