{-# LANGUAGE FlexibleInstances #-}

module Render.Internal where

import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing))
import Agda.Syntax.Internal hiding (telToList)
import qualified Data.List as List
import Render.Class
import Render.Common (renderHiding)
import Render.Concrete ()
import Render.RichText
import qualified Data.Set as Set

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

instance Render a => Render (Substitution' a) where
  renderPrec :: Int -> Substitution' a -> Inlines
renderPrec = forall {t} {a}.
(Ord t, Num t, Render a) =>
t -> Substitution' a -> Inlines
pr
    where
      pr :: t -> Substitution' a -> Inlines
pr t
p Substitution' a
input = case Substitution' a
input of
        Substitution' a
IdS -> Inlines
"idS"
        EmptyS Impossible
_ -> Inlines
"emptyS"
        a
t :# Substitution' a
rho -> Bool -> Inlines -> Inlines
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
2) forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
sep [t -> Substitution' a -> Inlines
pr t
2 Substitution' a
rho forall a. Semigroup a => a -> a -> a
<> Inlines
",", forall a. Render a => Int -> a -> Inlines
renderPrec Int
3 a
t]
        Strengthen Impossible
_ Substitution' a
rho -> Bool -> Inlines -> Inlines
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$ Inlines
"strS" Inlines -> Inlines -> Inlines
<+> t -> Substitution' a -> Inlines
pr t
10 Substitution' a
rho
        Wk Int
n Substitution' a
rho -> Bool -> Inlines -> Inlines
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$ [Char] -> Inlines
text ([Char]
"wkS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n) Inlines -> Inlines -> Inlines
<+> t -> Substitution' a -> Inlines
pr t
10 Substitution' a
rho
        Lift Int
n Substitution' a
rho -> Bool -> Inlines -> Inlines
mparens (t
p forall a. Ord a => a -> a -> Bool
> t
9) forall a b. (a -> b) -> a -> b
$ [Char] -> Inlines
text ([Char]
"liftS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n) Inlines -> Inlines -> Inlines
<+> t -> Substitution' a -> Inlines
pr t
10 Substitution' a
rho

-- | Term
instance Render Term where
  renderPrec :: Int -> Term -> Inlines
renderPrec Int
p Term
val =
    case Term
val of
      Var Int
x Elims
els -> [Char] -> Inlines
text ([Char]
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
x) forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
els
      Lam ArgInfo
ai Abs Term
b ->
        Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep
            [ Inlines
"λ" Inlines -> Inlines -> Inlines
<+> forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding ArgInfo
ai forall a. a -> a
id ([Char] -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> [Char]
absName forall a b. (a -> b) -> a -> b
$ Abs Term
b) Inlines -> Inlines -> Inlines
<+> Inlines
"->",
              forall a. Render a => a -> Inlines
render (forall a. Abs a -> a
unAbs Abs Term
b)
            ]
      Lit Literal
l -> forall a. Render a => a -> Inlines
render Literal
l
      Def QName
q Elims
els -> forall a. Render a => a -> Inlines
render QName
q forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
els
      Con ConHead
c ConInfo
_ Elims
vs -> forall a. Render a => a -> Inlines
render (ConHead -> QName
conName ConHead
c) forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
vs
      Pi Dom Type
a (NoAbs [Char]
_ Type
b) ->
        Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep
            [ forall a. Render a => Int -> a -> Inlines
renderPrec Int
1 (forall t e. Dom' t e -> e
unDom Dom Type
a) Inlines -> Inlines -> Inlines
<+> Inlines
"->",
              forall a. Render a => a -> Inlines
render Type
b
            ]
      Pi Dom Type
a Abs Type
b ->
        Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep
            [ forall a. LensHiding a => a -> Inlines -> Inlines
renderDom (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) ([Char] -> Inlines
text (forall a. Abs a -> [Char]
absName Abs Type
b) Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render (forall t e. Dom' t e -> e
unDom Dom Type
a)) Inlines -> Inlines -> Inlines
<+> Inlines
"->",
              forall a. Render a => a -> Inlines
render (forall a. Abs a -> a
unAbs Abs Type
b)
            ]
      Sort Sort
s -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Sort
s
      Level Level
l -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Level
l
      MetaV MetaId
x Elims
els -> forall a. Render a => a -> Inlines
render MetaId
x forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
els
      DontCare Term
v -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Term
v
      Dummy [Char]
s Elims
es -> Inlines -> Inlines
parens ([Char] -> Inlines
text [Char]
s) forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
es
    where
      pApp :: Inlines -> [a] -> Inlines
pApp Inlines
d [a]
els =
        Bool -> Inlines -> Inlines
mparens (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
els) Bool -> Bool -> Bool
&& Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep [Inlines
d, [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [a]
els)]

instance (Render t, Render e) => Render (Dom' t e) where
  render :: Dom' t e -> Inlines
render Dom' t e
dom = Inlines
pTac Inlines -> Inlines -> Inlines
<+> forall a. LensHiding a => a -> Inlines -> Inlines
renderDom Dom' t e
dom (forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t e
dom)
    where
      pTac :: Inlines
pTac
        | Just t
t <- forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom = Inlines
"@" forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens (Inlines
"tactic" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render t
t)
        | Bool
otherwise = forall a. Monoid a => a
mempty

renderDom :: LensHiding a => a -> Inlines -> Inlines
renderDom :: forall a. LensHiding a => a -> Inlines -> Inlines
renderDom a
i =
  case forall a. LensHiding a => a -> Hiding
getHiding a
i of
    Hiding
NotHidden -> Inlines -> Inlines
parens
    Hiding
Hidden -> Inlines -> Inlines
braces
    Instance {} -> Inlines -> Inlines
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inlines -> Inlines
braces

instance Render Clause where
  render :: Clause -> Inlines
render Clause {clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
body, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
ty} =
    [Inlines] -> Inlines
sep
      [ forall a. Render a => a -> Inlines
render Telescope
tel Inlines -> Inlines -> Inlines
<+> Inlines
"|-",
        [Inlines] -> Inlines
fsep
          [ [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) NAPs
ps) Inlines -> Inlines -> Inlines
<+> Inlines
"=",
            forall {a} {a}.
(Render a, Render a) =>
Maybe a -> Maybe a -> Inlines
pBody Maybe Term
body Maybe (Arg Type)
ty
          ]
      ]
    where
      pBody :: Maybe a -> Maybe a -> Inlines
pBody Maybe a
Nothing Maybe a
_ = Inlines
"(absurd)"
      pBody (Just a
b) Maybe a
Nothing = forall a. Render a => a -> Inlines
render a
b
      pBody (Just a
b) (Just a
t) = [Inlines] -> Inlines
fsep [forall a. Render a => a -> Inlines
render a
b Inlines -> Inlines -> Inlines
<+> Inlines
":", forall a. Render a => a -> Inlines
render a
t]

instance Render a => Render (Tele (Dom a)) where
  render :: Tele (Dom a) -> Inlines
render Tele (Dom a)
tel = [Inlines] -> Inlines
fsep [forall a. LensHiding a => a -> Inlines -> Inlines
renderDom Dom a
a ([Char] -> Inlines
text [Char]
x Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render (forall t e. Dom' t e -> e
unDom Dom a
a)) | ([Char]
x, Dom a
a) <- forall {b}. Tele b -> [([Char], b)]
telToList Tele (Dom a)
tel]
    where
      telToList :: Tele b -> [([Char], b)]
telToList Tele b
EmptyTel = []
      telToList (ExtendTel b
a Abs (Tele b)
tel') = (forall a. Abs a -> [Char]
absName Abs (Tele b)
tel', b
a) forall a. a -> [a] -> [a]
: Tele b -> [([Char], b)]
telToList (forall a. Abs a -> a
unAbs Abs (Tele b)
tel')

renderPrecLevelSucs :: Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs :: Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
p Integer
0 Int -> Inlines
d = Int -> Inlines
d Int
p
renderPrecLevelSucs Int
p Integer
n Int -> Inlines
d = Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Inlines
"lsuc" Inlines -> Inlines -> Inlines
<+> Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
10 (Integer
n forall a. Num a => a -> a -> a
- Integer
1) Int -> Inlines
d

instance Render Level where
  renderPrec :: Int -> Level -> Inlines
renderPrec Int
p (Max Integer
n [PlusLevel]
as) =
    case [PlusLevel]
as of
      [] -> Inlines
renderN
      [PlusLevel
a] | Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0 -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p PlusLevel
a
      [PlusLevel]
_ ->
        Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
          forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
List.foldr1 (\Inlines
a Inlines
b -> Inlines
"lub" Inlines -> Inlines -> Inlines
<+> Inlines
a Inlines -> Inlines -> Inlines
<+> Inlines
b) forall a b. (a -> b) -> a -> b
$
            [Inlines
renderN | Integer
n forall a. Ord a => a -> a -> Bool
> Integer
0] forall a. [a] -> [a] -> [a]
++ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [PlusLevel]
as
    where
      renderN :: Inlines
renderN = Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
p Integer
n (forall a b. a -> b -> a
const Inlines
"lzero")

instance Render PlusLevel where
  renderPrec :: Int -> PlusLevel -> Inlines
renderPrec Int
p (Plus Integer
n Term
a) = Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
p Integer
n forall a b. (a -> b) -> a -> b
$ \Int
p' -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p' Term
a

--instance Render LevelAtom where
-- LevelAtom is just Term
--  renderPrec p a =
--    case a of
--      MetaLevel x els -> renderPrec p (MetaV x els)
--      BlockedLevel _ v -> renderPrec p v
--      NeutralLevel _ v -> renderPrec p v
--      UnreducedLevel v -> renderPrec p v

instance Render Sort where
  renderPrec :: Int -> Sort -> Inlines
renderPrec Int
p Sort
srt =
    case Sort
srt of
      Type (ClosedLevel Integer
0) -> Inlines
"Set"
      Type (ClosedLevel Integer
n) -> [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
"Set" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
n
      Type Level
l -> Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Inlines
"Set" Inlines -> Inlines -> Inlines
<+> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Level
l
      Prop (ClosedLevel Integer
0) -> Inlines
"Prop"
      Prop (ClosedLevel Integer
n) -> [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
"Prop" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
n
      Prop Level
l -> Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Inlines
"Prop" Inlines -> Inlines -> Inlines
<+> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Level
l
      Inf IsFibrant
IsFibrant Integer
0 -> Inlines
"Setω"
      Inf IsFibrant
IsStrict Integer
0 -> Inlines
"SSetω"
      Inf IsFibrant
IsFibrant Integer
n -> [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
"Setω" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
n
      Inf IsFibrant
IsStrict Integer
n -> [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
"SSetω" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
n
      SSet Level
l -> Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Inlines
"SSet" Inlines -> Inlines -> Inlines
<+> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Level
l
      Sort
SizeUniv -> Inlines
"SizeUniv"
      Sort
LockUniv -> Inlines
"LockUniv"
      PiSort Dom' Term Term
a Sort
_s1 Abs Sort
s2 ->
        Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
          Inlines
"piSort" Inlines -> Inlines -> Inlines
<+> forall a. LensHiding a => a -> Inlines -> Inlines
renderDom (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Term
a) ([Char] -> Inlines
text (forall a. Abs a -> [Char]
absName Abs Sort
s2) Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render (forall t e. Dom' t e -> e
unDom Dom' Term Term
a))
            Inlines -> Inlines -> Inlines
<+> Inlines -> Inlines
parens
              ( [Inlines] -> Inlines
fsep
                  [ [Char] -> Inlines
text ([Char]
"λ " forall a. [a] -> [a] -> [a]
++ forall a. Abs a -> [Char]
absName Abs Sort
s2 forall a. [a] -> [a] -> [a]
++ [Char]
" ->"),
                    forall a. Render a => a -> Inlines
render (forall a. Abs a -> a
unAbs Abs Sort
s2)
                  ]
              )
      FunSort Sort
a Sort
b ->
        Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
          Inlines
"funSort" Inlines -> Inlines -> Inlines
<+> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Sort
a Inlines -> Inlines -> Inlines
<+> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Sort
b
      UnivSort Sort
s -> Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$ Inlines
"univSort" Inlines -> Inlines -> Inlines
<+> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Sort
s
      MetaS MetaId
x Elims
es -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
      DefS QName
d Elims
es -> forall a. Render a => Int -> a -> Inlines
renderPrec Int
p forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      DummyS [Char]
s -> Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ [Char] -> Inlines
text [Char]
s

instance Render Type where
  renderPrec :: Int -> Type -> Inlines
renderPrec Int
p (El Sort
_ Term
a) = forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Term
a

instance Render tm => Render (Elim' tm) where
  renderPrec :: Int -> Elim' tm -> Inlines
renderPrec Int
p (Apply Arg tm
v) = forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Arg tm
v
  renderPrec Int
_ (Proj ProjOrigin
_o QName
x) = Inlines
"." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render QName
x
  renderPrec Int
p (IApply tm
_ tm
_ tm
r) = forall a. Render a => Int -> a -> Inlines
renderPrec Int
p tm
r

instance Render DBPatVar where
  renderPrec :: Int -> DBPatVar -> Inlines
renderPrec Int
_ DBPatVar
x = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
patVarNameToString (DBPatVar -> [Char]
dbPatVarName DBPatVar
x) forall a. [a] -> [a] -> [a]
++ [Char]
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (DBPatVar -> Int
dbPatVarIndex DBPatVar
x)

instance Render a => Render (Pattern' a) where
  renderPrec :: Int -> Pattern' a -> Inlines
renderPrec Int
n (VarP PatternInfo
_o a
x) = forall a. Render a => Int -> a -> Inlines
renderPrec Int
n a
x
  renderPrec Int
_ (DotP PatternInfo
_o Term
t) = Inlines
"." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Term
t
  renderPrec Int
n (ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' a)]
nps) =
    Bool -> Inlines -> Inlines
mparens (Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg (Pattern' a)]
nps)) forall a b. (a -> b) -> a -> b
$
      (Inlines
lazy forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render (ConHead -> QName
conName ConHead
c)) Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [Arg (Pattern' a)]
ps)
    where
      ps :: [Arg (Pattern' a)]
ps = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
      lazy :: Inlines
lazy
        | ConPatternInfo -> Bool
conPLazy ConPatternInfo
i = Inlines
"~"
        | Bool
otherwise = forall a. Monoid a => a
mempty
  renderPrec Int
n (DefP PatternInfo
_ QName
q [NamedArg (Pattern' a)]
nps) =
    Bool -> Inlines -> Inlines
mparens (Int
n forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg (Pattern' a)]
nps)) forall a b. (a -> b) -> a -> b
$
      forall a. Render a => a -> Inlines
render QName
q Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [Arg (Pattern' a)]
ps)
    where
      ps :: [Arg (Pattern' a)]
ps = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
  -- -- Version with printing record type:
  -- renderPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
  --   text (show $ conName c) <+> fsep (fmap (render . namedArg) ps)
  --   where
  --     b = maybe False (== ConOSystem) $ conPRecord i
  --     prTy d = caseMaybe (conPType i) d $ \ t -> d  <+> ":" <+> render t
  renderPrec Int
_ (LitP PatternInfo
_ Literal
l) = forall a. Render a => a -> Inlines
render Literal
l
  renderPrec Int
_ (ProjP ProjOrigin
_o QName
q) = Inlines
"." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render QName
q
  renderPrec Int
n (IApplyP PatternInfo
_o Term
_ Term
_ a
x) = forall a. Render a => Int -> a -> Inlines
renderPrec Int
n a
x

--------------------------------------------------------------------------------
-- Agda.Syntax.Internal.Blockers

instance Render Blocker where
  render :: Blocker -> Inlines
render (UnblockOnAll Set Blocker
us)      = Inlines
"all" forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
us)
  render (UnblockOnAny Set Blocker
us)      = Inlines
"any" forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Blocker
us)
  render (UnblockOnMeta MetaId
m)      = forall a. Render a => a -> Inlines
render MetaId
m
  render (UnblockOnProblem ProblemId
pid) = Inlines
"problem" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render ProblemId
pid