module Render.TypeChecking where

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

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

instance Render Occurrence where
  render :: Occurrence -> Inlines
render =
    MetaNameSuggestion -> Inlines
text (MetaNameSuggestion -> Inlines)
-> (Occurrence -> MetaNameSuggestion) -> Occurrence -> Inlines
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) = Int -> Inlines
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 (MetaNameSuggestion -> Inlines)
-> (Polarity -> MetaNameSuggestion) -> Polarity -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      Polarity
Covariant -> MetaNameSuggestion
"+"
      Polarity
Contravariant -> MetaNameSuggestion
"-"
      Polarity
Invariant -> MetaNameSuggestion
"*"
      Polarity
Nonvariant -> MetaNameSuggestion
"_"