{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
module Render.Internal where
import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing))
import Agda.Syntax.Internal hiding (telToList)
import Agda.Utils.Function (applyWhen)
import Control.Monad
import qualified Data.List as List
import qualified Data.Set as Set
import Render.Class
import Render.Common (renderHiding)
import Render.Concrete ()
import Render.RichText
--------------------------------------------------------------------------------
instance (Render a) => Render (Substitution' a) where
renderPrec = pr
where
pr p input = case input of
IdS -> "idS"
EmptyS _ -> "emptyS"
t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]
Strengthen _ _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho
Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho
-- | Term
instance Render Term where
renderPrec p val =
case val of
Var x els -> text ("@" ++ show x) `pApp` els
Lam ai b ->
mparens (p > 0) $
fsep
[ "λ" <+> renderHiding ai id (text . absName $ b) <+> "->",
render (unAbs b)
]
Lit l -> render l
Def q els -> render q `pApp` els
Con c _ vs -> render (conName c) `pApp` vs
Pi a (NoAbs _ b) ->
mparens (p > 0) $
fsep
[ renderPrec 1 (unDom a) <+> "->",
render b
]
Pi a b ->
mparens (p > 0) $
fsep
[ renderDom (domInfo a) (text (absName b) <+> ":" <+> render (unDom a)) <+> "->",
render (unAbs b)
]
Sort s -> renderPrec p s
Level l -> renderPrec p l
MetaV x els -> render x `pApp` els
DontCare v -> renderPrec p v
Dummy s es -> parens (text s) `pApp` es
where
pApp d els =
mparens (not (null els) && p > 9) $
fsep [d, fsep (fmap (renderPrec 10) els)]
instance (Render t, Render e) => Render (Dom' t e) where
render dom = pTac <+> renderDom dom (render $ unDom dom)
where
pTac
| Just t <- domTactic dom = "@" <> parens ("tactic" <+> render t)
| otherwise = mempty
renderDom :: (LensHiding a) => a -> Inlines -> Inlines
renderDom i =
case getHiding i of
NotHidden -> parens
Hidden -> braces
Instance {} -> braces . braces
instance Render Clause where
render Clause {clauseTel = tel, namedClausePats = ps, clauseBody = body, clauseType = ty} =
sep
[ render tel <+> "|-",
fsep
[ fsep (fmap (renderPrec 10) ps) <+> "=",
pBody body ty
]
]
where
pBody Nothing _ = "(absurd)"
pBody (Just b) Nothing = render b
pBody (Just b) (Just t) = fsep [render b <+> ":", render t]
instance (Render a) => Render (Tele (Dom a)) where
render tel = fsep [renderDom a (text x <+> ":" <+> render (unDom a)) | (x, a) <- telToList tel]
where
telToList EmptyTel = []
telToList (ExtendTel a tel') = (absName tel', a) : telToList (unAbs tel')
renderPrecLevelSucs :: Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs p 0 d = d p
renderPrecLevelSucs p n d = mparens (p > 9) $ "lsuc" <+> renderPrecLevelSucs 10 (n - 1) d
instance Render Level where
renderPrec p (Max n as) =
case as of
[] -> renderN
[a] | n == 0 -> renderPrec p a
_ ->
mparens (p > 9) $
List.foldr1 (\a b -> "lub" <+> a <+> b) $
[renderN | n > 0] ++ fmap (renderPrec 10) as
where
renderN = renderPrecLevelSucs p n (const "lzero")
instance Render PlusLevel where
renderPrec p (Plus n a) = renderPrecLevelSucs p n $ \p' -> renderPrec p' 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 p = \case
Univ u (ClosedLevel n) -> text $ suffix n $ showUniv u
Univ u l -> mparens (p > 9) $ text (showUniv u) <+> renderPrec 10 l
Inf u n -> text $ suffix n $ showUniv u ++ "ω"
LevelUniv -> "LevelUniv"
SizeUniv -> "SizeUniv"
LockUniv -> "LockUniv"
PiSort a _s1 s2 ->
mparens (p > 9) $
"piSort"
<+> renderDom (domInfo a) (text (absName s2) <+> ":" <+> render (unDom a))
<+> parens
( fsep
[ text ("λ " ++ absName s2 ++ " ->"),
render (unAbs s2)
]
)
FunSort a b ->
mparens (p > 9) $
"funSort" <+> renderPrec 10 a <+> renderPrec 10 b
UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s
MetaS x es -> renderPrec p $ MetaV x es
DefS d es -> renderPrec p $ Def d es
DummyS s -> parens $ text s
IntervalUniv -> "IntervalUniv"
where
suffix n = applyWhen (n /= 0) (++ show n)
instance Render Type where
renderPrec p (El _ a) = renderPrec p a
instance (Render tm) => Render (Elim' tm) where
renderPrec p (Apply v) = renderPrec p v
renderPrec _ (Proj _o x) = "." <> render x
renderPrec p (IApply _ _ r) = renderPrec p r
instance Render DBPatVar where
renderPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x)
instance (Render a) => Render (Pattern' a) where
renderPrec n (VarP _o x) = renderPrec n x
renderPrec _ (DotP _o t) = "." <> renderPrec 10 t
renderPrec n (ConP c i nps) =
mparens (n > 0 && not (null nps)) $
(lazy <> render (conName c)) <+> fsep (fmap (renderPrec 10) ps)
where
ps = fmap (fmap namedThing) nps
lazy
| conPLazy i = "~"
| otherwise = mempty
renderPrec n (DefP _ q nps) =
mparens (n > 0 && not (null nps)) $
render q <+> fsep (fmap (renderPrec 10) ps)
where
ps = fmap (fmap namedThing) 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 _ (LitP _ l) = render l
renderPrec _ (ProjP _o q) = "." <> render q
renderPrec n (IApplyP _o _ _ x) = renderPrec n x
--------------------------------------------------------------------------------
-- Agda.Syntax.Internal.Blockers
instance Render Blocker where
render (UnblockOnAll us) = "all" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
render (UnblockOnAny us) = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)
render (UnblockOnMeta m) = render m
render (UnblockOnProblem pid) = "problem" <+> render pid
render (UnblockOnDef q) = "definition" <+> render q