{-# LANGUAGE CPP #-}
{-# 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 = Int -> Substitution' a -> Inlines
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 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
2) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
sep [t -> Substitution' a -> Inlines
pr t
2 Substitution' a
rho Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
",", Int -> a -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
3 a
t]
#if MIN_VERSION_Agda(2,6,3)
        Strengthen Impossible
_ Int
_ Substitution' a
rho ->
#else
        Strengthen _ rho ->
#endif
          Bool -> Inlines -> Inlines
mparens (t
p t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9) (Inlines -> Inlines) -> Inlines -> Inlines
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 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char] -> Inlines
text ([Char]
"wkS " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char] -> Inlines
text ([Char]
"liftS " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
x) Inlines -> Elims -> Inlines
forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
els
      Lam ArgInfo
ai Abs Term
b ->
        Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep
            [ Inlines
"λ" Inlines -> Inlines -> Inlines
<+> ArgInfo -> (Inlines -> Inlines) -> Inlines -> Inlines
forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding ArgInfo
ai Inlines -> Inlines
forall a. a -> a
id ([Char] -> Inlines
text ([Char] -> Inlines) -> (Abs Term -> [Char]) -> Abs Term -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs Term -> [Char]
forall a. Abs a -> [Char]
absName (Abs Term -> Inlines) -> Abs Term -> Inlines
forall a b. (a -> b) -> a -> b
$ Abs Term
b) Inlines -> Inlines -> Inlines
<+> Inlines
"->",
              Term -> Inlines
forall a. Render a => a -> Inlines
render (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
            ]
      Lit Literal
l -> Literal -> Inlines
forall a. Render a => a -> Inlines
render Literal
l
      Def QName
q Elims
els -> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
q Inlines -> Elims -> Inlines
forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
els
      Con ConHead
c ConInfo
_ Elims
vs -> QName -> Inlines
forall a. Render a => a -> Inlines
render (ConHead -> QName
conName ConHead
c) Inlines -> Elims -> Inlines
forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
vs
      Pi Dom Type
a (NoAbs [Char]
_ Type
b) ->
        Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep
            [ Int -> Type -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
1 (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) Inlines -> Inlines -> Inlines
<+> Inlines
"->",
              Type -> Inlines
forall a. Render a => a -> Inlines
render Type
b
            ]
      Pi Dom Type
a Abs Type
b ->
        Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep
            [ ArgInfo -> Inlines -> Inlines
forall a. LensHiding a => a -> Inlines -> Inlines
renderDom (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) ([Char] -> Inlines
text (Abs Type -> [Char]
forall a. Abs a -> [Char]
absName Abs Type
b) Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> Type -> Inlines
forall a. Render a => a -> Inlines
render (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) Inlines -> Inlines -> Inlines
<+> Inlines
"->",
              Type -> Inlines
forall a. Render a => a -> Inlines
render (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)
            ]
      Sort Sort
s -> Int -> Sort -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Sort
s
      Level Level
l -> Int -> Level -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Level
l
      MetaV MetaId
x Elims
els -> MetaId -> Inlines
forall a. Render a => a -> Inlines
render MetaId
x Inlines -> Elims -> Inlines
forall {a}. Render a => Inlines -> [a] -> Inlines
`pApp` Elims
els
      DontCare Term
v -> Int -> Term -> Inlines
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) Inlines -> Elims -> Inlines
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 ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
els) Bool -> Bool -> Bool
&& Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          [Inlines] -> Inlines
fsep [Inlines
d, [Inlines] -> Inlines
fsep ((a -> Inlines) -> [a] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> a -> Inlines
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
<+> Dom' t e -> Inlines -> Inlines
forall a. LensHiding a => a -> Inlines -> Inlines
renderDom Dom' t e
dom (e -> Inlines
forall a. Render a => a -> Inlines
render (e -> Inlines) -> e -> Inlines
forall a b. (a -> b) -> a -> b
$ Dom' t e -> e
forall t e. Dom' t e -> e
unDom Dom' t e
dom)
    where
      pTac :: Inlines
pTac
        | Just t
t <- Dom' t e -> Maybe t
forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom = Inlines
"@" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens (Inlines
"tactic" Inlines -> Inlines -> Inlines
<+> t -> Inlines
forall a. Render a => a -> Inlines
render t
t)
        | Bool
otherwise = Inlines
forall a. Monoid a => a
mempty

renderDom :: LensHiding a => a -> Inlines -> Inlines
renderDom :: forall a. LensHiding a => a -> Inlines -> Inlines
renderDom a
i =
  case a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding a
i of
    Hiding
NotHidden -> Inlines -> Inlines
parens
    Hiding
Hidden -> Inlines -> Inlines
braces
    Instance {} -> Inlines -> Inlines
braces (Inlines -> Inlines) -> (Inlines -> Inlines) -> Inlines -> Inlines
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
      [ Telescope -> Inlines
forall a. Render a => a -> Inlines
render Telescope
tel Inlines -> Inlines -> Inlines
<+> Inlines
"|-",
        [Inlines] -> Inlines
fsep
          [ [Inlines] -> Inlines
fsep ((NamedArg DeBruijnPattern -> Inlines) -> NAPs -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> NamedArg DeBruijnPattern -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) NAPs
ps) Inlines -> Inlines -> Inlines
<+> Inlines
"=",
            Maybe Term -> Maybe (Arg Type) -> 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 = a -> Inlines
forall a. Render a => a -> Inlines
render a
b
      pBody (Just a
b) (Just a
t) = [Inlines] -> Inlines
fsep [a -> Inlines
forall a. Render a => a -> Inlines
render a
b Inlines -> Inlines -> Inlines
<+> Inlines
":", a -> 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 [Dom a -> Inlines -> Inlines
forall a. LensHiding a => a -> Inlines -> Inlines
renderDom Dom a
a ([Char] -> Inlines
text [Char]
x Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> a -> Inlines
forall a. Render a => a -> Inlines
render (Dom a -> a
forall t e. Dom' t e -> e
unDom Dom a
a)) | ([Char]
x, Dom a
a) <- Tele (Dom a) -> [([Char], Dom 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') = (Abs (Tele b) -> [Char]
forall a. Abs a -> [Char]
absName Abs (Tele b)
tel', b
a) ([Char], b) -> [([Char], b)] -> [([Char], b)]
forall a. a -> [a] -> [a]
: Tele b -> [([Char], b)]
telToList (Abs (Tele b) -> Tele b
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"lsuc" Inlines -> Inlines -> Inlines
<+> Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
10 (Integer
n Integer -> Integer -> Integer
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' Term]
as) =
    case [PlusLevel' Term]
as of
      [] -> Inlines
renderN
      [PlusLevel' Term
a] | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> Int -> PlusLevel' Term -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p PlusLevel' Term
a
      [PlusLevel' Term]
_ ->
        Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          (Inlines -> Inlines -> Inlines) -> [Inlines] -> Inlines
forall a. (a -> a -> a) -> [a] -> a
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) ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$
            [Inlines
renderN | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0] [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ (PlusLevel' Term -> Inlines) -> [PlusLevel' Term] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> PlusLevel' Term -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [PlusLevel' Term]
as
    where
      renderN :: Inlines
renderN = Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
p Integer
n (Inlines -> Int -> Inlines
forall a b. a -> b -> a
const Inlines
"lzero")

instance Render PlusLevel where
  renderPrec :: Int -> PlusLevel' Term -> Inlines
renderPrec Int
p (Plus Integer
n Term
a) = Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs Int
p Integer
n ((Int -> Inlines) -> Inlines) -> (Int -> Inlines) -> Inlines
forall a b. (a -> b) -> a -> b
$ \Int
p' -> Int -> Term -> Inlines
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 ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char]
"Set" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n
      Type Level
l -> Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"Set" Inlines -> Inlines -> Inlines
<+> Int -> Level -> 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 ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char]
"Prop" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n
      Prop Level
l -> Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"Prop" Inlines -> Inlines -> Inlines
<+> Int -> Level -> 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 ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char]
"Setω" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n
      Inf IsFibrant
IsStrict Integer
n -> [Char] -> Inlines
text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char]
"SSetω" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n
      SSet Level
l -> Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"SSet" Inlines -> Inlines -> Inlines
<+> Int -> Level -> 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          Inlines
"piSort" Inlines -> Inlines -> Inlines
<+> ArgInfo -> Inlines -> Inlines
forall a. LensHiding a => a -> Inlines -> Inlines
renderDom (Dom' Term Term -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term Term
a) ([Char] -> Inlines
text (Abs Sort -> [Char]
forall a. Abs a -> [Char]
absName Abs Sort
s2) Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> Term -> Inlines
forall a. Render a => a -> Inlines
render (Dom' Term Term -> Term
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]
"λ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Abs Sort -> [Char]
forall a. Abs a -> [Char]
absName Abs Sort
s2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ->"),
                    Sort -> Inlines
forall a. Render a => a -> Inlines
render (Abs Sort -> Sort
forall a. Abs a -> a
unAbs Abs Sort
s2)
                  ]
              )
      FunSort Sort
a Sort
b ->
        Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          Inlines
"funSort" Inlines -> Inlines -> Inlines
<+> Int -> Sort -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Sort
a Inlines -> Inlines -> Inlines
<+> Int -> Sort -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Sort
b
      UnivSort Sort
s -> Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"univSort" Inlines -> Inlines -> Inlines
<+> Int -> Sort -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10 Sort
s
      MetaS MetaId
x Elims
es -> Int -> Term -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p (Term -> Inlines) -> Term -> Inlines
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
      DefS QName
d Elims
es -> Int -> Term -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p (Term -> Inlines) -> Term -> Inlines
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      DummyS [Char]
s -> Inlines -> Inlines
parens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char] -> Inlines
text [Char]
s
#if MIN_VERSION_Agda(2,6,3)
      Sort
IntervalUniv -> Inlines
"IntervalUniv"
#endif

instance Render Type where
  renderPrec :: Int -> Type -> Inlines
renderPrec Int
p (El Sort
_ Term
a) = Int -> Term -> Inlines
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) = Int -> Arg tm -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p Arg tm
v
  renderPrec Int
_ (Proj ProjOrigin
_o QName
x) = Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x
  renderPrec Int
p (IApply tm
_ tm
_ tm
r) = Int -> tm -> Inlines
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 ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
patVarNameToString (DBPatVar -> [Char]
dbPatVarName DBPatVar
x) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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) = Int -> a -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
n a
x
  renderPrec Int
_ (DotP PatternInfo
_o Term
t) = Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Int -> Term -> Inlines
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not ([NamedArg (Pattern' a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg (Pattern' a)]
nps)) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
      (Inlines
lazy Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> QName -> Inlines
forall a. Render a => a -> Inlines
render (ConHead -> QName
conName ConHead
c)) Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep ((Arg (Pattern' a) -> Inlines) -> [Arg (Pattern' a)] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Arg (Pattern' a) -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [Arg (Pattern' a)]
ps)
    where
      ps :: [Arg (Pattern' a)]
ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
nps
      lazy :: Inlines
lazy
        | ConPatternInfo -> Bool
conPLazy ConPatternInfo
i = Inlines
"~"
        | Bool
otherwise = Inlines
forall a. Monoid a => a
mempty
  renderPrec Int
n (DefP PatternInfo
_ QName
q [NamedArg (Pattern' a)]
nps) =
    Bool -> Inlines -> Inlines
mparens (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
not ([NamedArg (Pattern' a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg (Pattern' a)]
nps)) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
      QName -> Inlines
forall a. Render a => a -> Inlines
render QName
q Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep ((Arg (Pattern' a) -> Inlines) -> [Arg (Pattern' a)] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Arg (Pattern' a) -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
10) [Arg (Pattern' a)]
ps)
    where
      ps :: [Arg (Pattern' a)]
ps = (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [Arg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
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) = Literal -> Inlines
forall a. Render a => a -> Inlines
render Literal
l
  renderPrec Int
_ (ProjP ProjOrigin
_o QName
q) = Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
q
  renderPrec Int
n (IApplyP PatternInfo
_o Term
_ Term
_ a
x) = Int -> a -> Inlines
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" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ (Blocker -> Inlines) -> [Blocker] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Inlines
forall a. Render a => a -> Inlines
render ([Blocker] -> [Inlines]) -> [Blocker] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us)
  render (UnblockOnAny Set Blocker
us)      = Inlines
"any" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ (Blocker -> Inlines) -> [Blocker] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
map Blocker -> Inlines
forall a. Render a => a -> Inlines
render ([Blocker] -> [Inlines]) -> [Blocker] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us)
  render (UnblockOnMeta MetaId
m)      = MetaId -> Inlines
forall a. Render a => a -> Inlines
render MetaId
m
  render (UnblockOnProblem ProblemId
pid) = Inlines
"problem" Inlines -> Inlines -> Inlines
<+> ProblemId -> Inlines
forall a. Render a => a -> Inlines
render ProblemId
pid
#if MIN_VERSION_Agda(2,6,3)
  render (UnblockOnDef QName
q)       = Inlines
"definition" Inlines -> Inlines -> Inlines
<+> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
q
#endif