{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
module Render.Concrete where
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
import Agda.Utils.Float (toStringWithoutDotZero)
import Agda.Utils.Function
import Agda.Utils.Functor (dget, (<&>), for)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.List1 as List1 (fromList, toList, List1)
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Null
import Data.Maybe (isNothing, maybeToList)
import qualified Data.Strict.Maybe as Strict
import qualified Data.Text as T
import Render.Class
import Render.Common
import Render.Literal ()
import Render.Name ()
import Render.RichText
import Render.TypeChecking ()
import Prelude hiding (null)
import qualified Agda.Syntax.Common.Aspect as Asp
--------------------------------------------------------------------------------
#if MIN_VERSION_Agda(2,7,0)
instance (Render a) => Render (TacticAttribute' a) where
render (TacticAttribute t) =
ifNull (render t) empty $ \d -> "@" <> parens ("tactic" <+> d)
#endif
instance (Render a) => Render (Ranged a) where
render = render . rangedThing
instance (Render a) => Render (WithHiding a) where
render w = renderHiding w id $ render $ dget w
instance Render Modality where
render mod =
hsep
[ render (getRelevance mod),
render (getQuantity mod),
render (getCohesion mod)
]
-- | OpApp
instance Render (OpApp Expr) where
render (Ordinary e) = render e
render (SyntaxBindingLambda r bs e) = render (Lam r bs e)
-- | MaybePlaceholder
instance (Render a) => Render (MaybePlaceholder a) where
render Placeholder {} = "_"
render (NoPlaceholder _ e) = render e
--------------------------------------------------------------------------------
-- | InteractionId
instance Render InteractionId where
render (InteractionId i) = linkHole i
--------------------------------------------------------------------------------
-- | Expression
instance Render Expr where
render expr = case expr of
Ident qname -> render qname
Lit range lit -> render lit
-- no hole index, use LinkRange instead
QuestionMark range Nothing -> linkRange range "?"
QuestionMark _range (Just n) -> linkHole n
Underscore range n -> linkRange range $ maybe "_" text n
-- '_range' is almost always 'NoRange' :(
App _range _ _ ->
case appView expr of
AppView e1 args -> fsep $ render e1 : fmap render args
RawApp _ es -> fsep $ fmap render (List2.toList es)
#if MIN_VERSION_Agda(2,8,0)
OpApp _ q _ es -> fsep $ renderOpApp280 (Asp.Name Nothing True) q es
WithApp _ e es -> fsep $ render e : fmap (("|" <+>) . render) (toList es)
KnownOpApp nk _ q _ es -> fsep $ renderOpApp280 (Asp.Name (Just nk) True) q es
#else
OpApp _ q _ es -> fsep $ renderOpApp q es
WithApp _ e es -> fsep $ render e : fmap ((text' ["delimiter"] "|" <+>) . render) es
KnownOpApp _ _ q _ es -> fsep $ renderOpApp q es
#endif
HiddenArg _ e -> braces' $ render e
InstanceArg _ e -> dbraces $ render e
Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (fmap render (toList bs)) <+> absurd h
Lam _ bs e -> sep [lambda <+> fsep (fmap render (toList bs)) <+> arrow, render e]
AbsurdLam _ h -> lambda <+> absurd h
ExtendedLam range _ pes -> lambda <+> bracesAndSemicolons (fmap render (toList pes))
Fun _ e1 e2 ->
sep
[ renderCohesion e1 (renderQuantity e1 (render e1)) <+> arrow,
render e2
]
Pi tel e ->
sep
[ render (Tel $ smashTel (toList tel)) <+> arrow,
render e
]
Let _ ds me ->
sep
[ "let" <+> vcat (fmap render (toList ds)),
maybe mempty (\e -> "in" <+> render e) me
]
Paren _ e -> parens $ render e
IdiomBrackets _ exprs ->
case exprs of
[] -> emptyIdiomBrkt
[e] -> leftIdiomBrkt <+> render e <+> rightIdiomBrkt
e : es -> leftIdiomBrkt <+> render e <+> fsep (fmap (("|" <+>) . render) es) <+> rightIdiomBrkt
DoBlock _ ss -> "do" <+> vcat (fmap render (toList ss))
As _ x e -> render x <> "@" <> render e
Dot _ e -> "." <> render e
DoubleDot _ e -> ".." <> render e
Absurd _ -> "()"
#if MIN_VERSION_Agda(2,8,0)
Rec _ _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]
RecUpdate _ _ e xs ->
sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]
#else
Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]
RecUpdate _ e xs ->
sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]
#endif
Quote _ -> "quote"
QuoteTerm _ -> "quoteTerm"
Unquote _ -> "unquote"
Tactic _ t -> "tactic" <+> render t
-- Andreas, 2011-10-03 print irrelevant things as .(e)
DontCare e -> "." <> parens (render e)
Equal _ a b -> render a <+> "=" <+> render b
Ellipsis _ -> "..."
Generalized e -> render e
KnownIdent _ q -> render q
where
absurd NotHidden = "()"
absurd Instance {} = "{{}}"
absurd Hidden = "{}"
--------------------------------------------------------------------------------
instance (Render a, Render b) => Render (Either a b) where
render = either render render
instance (Render a) => Render (FieldAssignment' a) where
render (FieldAssignment x e) = sep [render x <+> "=", render e]
instance Render ModuleAssignment where
render (ModuleAssignment m es i) = fsep (render m : fmap render es) <+> render i
instance Render LamClause where
render (LamClause lhs rhs _) =
sep
[ render lhs,
render' rhs
]
where
render' (RHS e) = arrow <+> render e
render' AbsurdRHS = mempty
instance Render BoundName where
render BName {boundName = x} = render x
instance (Render a) => Render (Binder' a) where
#if MIN_VERSION_Agda(2,8,0)
render (Binder mpat UserBinderName n) =
applyWhenJust mpat (\ pat -> (<+> ("@" <+> parens (render pat)))) $ render n
render (Binder pat InsertedBinderName n) = case pat of
Just pat -> parens (render pat)
Nothing -> render n
#else
render (Binder mpat n) =
let d = render n
in case mpat of
Nothing -> d
Just pat -> d <+> "@" <+> parens (render pat)
#endif
--------------------------------------------------------------------------------
-- | NamedBinding
instance Render NamedBinding where
#if MIN_VERSION_Agda(2,8,0)
render (NamedBinding withH
x@(Arg (ArgInfo h (Modality r q c p) _o _fv (Annotation lock))
(Named _mn xb@(Binder _mp _ (BName _y _fix t _fin))))) =
applyWhen withH prH $
applyWhenJust (isLabeled x) (\ l -> (text l <+>) . ("=" <+>)) (render xb)
where
prH = renderRelevance r
. renderHiding h mparens
. (coh <+>)
. (qnt <+>)
. (pol <+>)
. (lck <+>)
. (tac <+>)
coh = render c
qnt = render q
pol = render p
tac = render t
lck = render lock
-- Parentheses are needed when an attribute @... is printed
mparens = applyUnless (null coh && null qnt && null lck && null tac && null pol) parens
#elif MIN_VERSION_Agda(2,7,0)
render
( NamedBinding
withH
x@( Arg
(ArgInfo h (Modality r q c) _o _fv (Annotation lock))
(Named _mn xb@(Binder _mp (BName _y _fix t _fin)))
)
) =
applyWhen withH prH $
applyWhenJust (isLabeled x) (\l -> (text l <+>) . ("=" <+>)) (render xb)
where
prH =
(render r <>)
. renderHiding h mparens
. (coh <+>)
. (qnt <+>)
. (lck <+>)
. (tac <+>)
coh = render c
qnt = render q
tac = render t
lck = render lock
-- Parentheses are needed when an attribute @... is printed
mparens = applyUnless (null coh && null qnt && null lck && null tac) parens
#else
render (NamedBinding withH x) =
prH $
if
| Just l <- isLabeled x -> text l <> " = " <> render xb
| otherwise -> render xb
where
xb = namedArg x
bn = binderName xb
prH
| withH =
renderRelevance x
. renderHiding x mparens'
. renderCohesion x
. renderQuantity x
. renderTactic bn
| otherwise = id
-- Parentheses are needed when an attribute @... is present
mparens'
| noUserQuantity x, Nothing <- bnameTactic bn = id
| otherwise = parens
#endif
renderTactic :: BoundName -> Inlines -> Inlines
renderTactic = renderTactic' . bnameTactic
renderTactic' :: TacticAttribute -> Inlines -> Inlines
#if MIN_VERSION_Agda(2,7,0)
renderTactic' t = (render t <+>)
#else
renderTactic' Nothing d = d
renderTactic' (Just t) d = "@" <> (parens ("tactic " <> render t) <+> d)
#endif
--------------------------------------------------------------------------------
-- | LamBinding
instance Render LamBinding where
render (DomainFree x) = render (NamedBinding True x)
render (DomainFull b) = render b
-- | TypedBinding
instance Render TypedBinding where
render (TLet _ ds) = parens $ "let" <+> vcat (fmap render (toList ds))
render (TBind _ xs (Underscore _ Nothing)) =
fsep (fmap (render . NamedBinding True) (toList xs))
render (TBind _ binders e) =
fsep
[ renderRelevance y $
renderHiding y parens $
renderCohesion y $
renderQuantity y $
renderTactic (binderName $ namedArg y) $
sep
[ fsep (fmap (render . NamedBinding False) ys),
":" <+> render e
]
| ys@(y : _) <- groupBinds (toList binders)
]
where
groupBinds [] = []
groupBinds (x : xs)
| Just {} <- isLabeled x = [x] : groupBinds xs
| otherwise = (x : ys) : groupBinds zs
where
(ys, zs) = span (same x) xs
same a b = getArgInfo a == getArgInfo b && isNothing (isLabeled b)
instance Render Tel where
render (Tel tel)
| any isMeta tel = forallQ <+> fsep (fmap render tel)
| otherwise = fsep (fmap render tel)
where
isMeta (TBind _ _ (Underscore _ Nothing)) = True
isMeta _ = False
smashTel :: Telescope -> Telescope
smashTel
( TBind r xs e
: TBind _ ys e'
: tel
)
| show e == show e' = smashTel (TBind r (fromList (toList xs ++ toList ys)) e : tel)
smashTel (b : tel) = b : smashTel tel
smashTel [] = []
instance Render RHS where
render (RHS e) = "=" <+> render e
render AbsurdRHS = mempty
instance Render WhereClause where
render NoWhere = mempty
render (AnyWhere _range [Module _ _ x [] ds])
| isNoName (unqualify x) =
vcat ["where", vcat $ fmap render ds]
render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds]
#if MIN_VERSION_Agda(2,7,0)
render (SomeWhere _ erased m a ds) =
vcat
[ hsep $
privateWhenUserWritten
a
["module", renderErased erased (render m), "where"],
vcat $ map render ds
]
where
privateWhenUserWritten = \case
PrivateAccess _ UserWritten -> ("private" :)
_ -> id
#else
render (SomeWhere _range _er m a ds) =
vcat
[ hsep $
applyWhen
(a == PrivateAccess UserWritten)
("private" :)
["module", render m, "where"],
vcat $ fmap render ds
]
#endif
instance Render LHS where
render (LHS p eqs es) =
sep
[ render p,
if null eqs then mempty else fsep $ fmap render eqs,
prefixedThings "with" (fmap renderWithd es)
]
where
renderWithd :: WithExpr -> Inlines
renderWithd (Named nm wh) =
let e = render wh
in case nm of
Nothing -> e
Just n -> render n <+> ":" <+> e
instance Render LHSCore where
render (LHSHead f ps) = sep $ render f : fmap (parens . render) ps
render (LHSProj d ps lhscore ps') =
sep $
render d
: fmap (parens . render) ps
++ parens (render lhscore)
: fmap (parens . render) ps'
render (LHSWith h wps ps) =
if null ps
then doc
else sep $ parens doc : fmap (parens . render) ps
where
doc = sep $ render h : fmap (("|" <+>) . render) (toList wps)
render (LHSEllipsis r p) = "..."
instance Render ModuleApplication where
#if MIN_VERSION_Agda(2,8,0)
render (SectionApp _ bs x es) = fsep $ concat
[ map render bs
, [ "=", render x ]
, map render es
]
#else
render (SectionApp _ bs e) = fsep (fmap render bs) <+> "=" <+> render e
#endif
render (RecordModuleInstance _ rec) = "=" <+> render rec <+> "{{...}}"
instance Render DoStmt where
render (DoBind _ p e cs) =
fsep [render p <+> "←", render e, prCs cs]
where
prCs [] = mempty
prCs cs' = fsep ["where", vcat (fmap render cs')]
render (DoThen e) = render e
render (DoLet _ ds) = "let" <+> vcat (render <$> toList ds)
instance Render Declaration where
render d =
case d of
TypeSig i tac x e ->
sep
[ renderTactic' tac $ renderRelevance i $ renderCohesion i $ renderQuantity i $ render x <+> ":",
render e
]
#if MIN_VERSION_Agda(2,8,0)
FieldSig inst tac x (Arg i e) ->
mkInst inst $ mkOverlap i $
-- We print relevance before hiding, need to clear it before printing the rest of the attributes with TypeSig.
renderRelevance i $ renderHiding i id $
render $ TypeSig (setRelevance relevant i) tac x e
#else
FieldSig inst tac x (Arg i e) ->
mkInst inst $
mkOverlap i $
renderRelevance i $
renderHiding i id $
renderCohesion i $
renderQuantity i $
render $
TypeSig (setRelevance Relevant i) tac x e
#endif
where
mkInst (InstanceDef _) f = sep ["instance", f]
mkInst NotInstanceDef f = f
#if MIN_VERSION_Agda(2,7,0)
mkOverlap i d
| isYesOverlap i = "overlap" <+> d
#else
mkOverlap i d | isOverlappable i = "overlap" <+> d
#endif
| otherwise = d
Field _ fs ->
sep
[ "field",
vcat (fmap render fs)
]
FunClause lhs rhs wh _ ->
sep
[ render lhs,
render rhs,
render wh
]
DataSig _ _er x tel e ->
fsep
[ hsep
[ "data",
render x,
fcat (fmap render tel)
],
hsep
[ ":",
render e
]
]
Data _ _er x tel e cs ->
fsep
[ hsep
[ "data",
render x,
fcat (fmap render tel)
],
hsep
[ ":",
render e,
"where"
],
vcat $ fmap render cs
]
DataDef _ x tel cs ->
sep
[ hsep
[ "data",
render x,
fcat (fmap render tel)
],
"where",
vcat $ fmap render cs
]
RecordSig _ _er x tel e ->
sep
[ hsep
[ "record",
render x,
fcat (fmap render tel)
],
hsep
[ ":",
render e
]
]
#if MIN_VERSION_Agda(2,7,0)
Record _ erased x dir tel e cs -> pRecord erased x dir tel (Just e) cs
#else
Record _ _er x dir tel e cs -> pRecord x dir tel (Just e) cs
#endif
#if MIN_VERSION_Agda(2,7,0)
RecordDef _ x dir tel cs -> pRecord defaultErased x dir tel Nothing cs
#else
RecordDef _ x dir tel cs -> pRecord x dir tel Nothing cs
#endif
#if !MIN_VERSION_Agda(2,7,0)
RecordDirective r -> pRecordDirective r
#endif
Infix f xs -> render f <+> fsep (punctuate "," $ fmap render (toList xs))
Syntax n _ -> "syntax" <+> render n <+> "..."
PatternSyn _ n as p ->
"pattern"
<+> render n
<+> fsep (fmap render as)
<+> "="
<+> render p
Mutual _ ds -> namedBlock "mutual" ds
InterleavedMutual _ ds -> namedBlock "interleaved mutual" ds
LoneConstructor _ ds -> namedBlock "constructor" ds
Abstract _ ds -> namedBlock "abstract" ds
Private _ _ ds -> namedBlock "private" ds
InstanceB _ ds -> namedBlock "instance" ds
Macro _ ds -> namedBlock "macro" ds
Postulate _ ds -> namedBlock "postulate" ds
Primitive _ ds -> namedBlock "primitive" ds
Generalize _ ds -> namedBlock "variable" ds
Module _ _er x tel ds ->
fsep
[ hsep
[ "module",
render x,
fcat (fmap render tel),
"where"
],
vcat $ fmap render ds
]
#if MIN_VERSION_Agda(2,8,0)
ModuleMacro _ NotErased{} x (SectionApp _ [] y es) DoOpen i
| isNoName x ->
sep [ render DoOpen
, fsep $ render y : map render es
, render i
]
ModuleMacro _ erased x (SectionApp _ tel y es) open i ->
sep [ render open <+> "module" <+>
renderErased erased (render x) <+> fsep (map render tel)
, fsep $ concat [ [ "=", render y ], map render es, [ render i ] ]
]
ModuleMacro _ erased x (RecordModuleInstance _ rec) open _i ->
sep [ render open <+> "module" <+> renderErased erased (render x)
, "=" <+> render rec <+> "{{...}}"
]
#else
ModuleMacro _ _er x m open i -> case m of
(SectionApp _ [] e)
| open == DoOpen,
isNoName x ->
fsep
[ render open,
render e,
render i
]
(SectionApp _ tel e) ->
fsep
[ render open <+> "module" <+> render x <+> fcat (fmap render tel),
"=" <+> render e <+> render i
]
(RecordModuleInstance _ rec) ->
fsep
[ render open <+> "module" <+> render x,
"=" <+> render rec <+> "{{...}}"
]
#endif
Open _ x i -> hsep ["open", render x, render i]
Import _ x rn open i ->
hsep [render open, "import", render x, as rn, render i]
where
as Nothing = mempty
as (Just y) = "as" <+> render (asName y)
UnquoteDecl _ xs t ->
fsep ["unquoteDecl" <+> fsep (fmap render xs) <+> "=", render t]
UnquoteDef _ xs t ->
fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t]
Pragma pr -> sep ["{-#" <+> render pr, "#-}"]
UnquoteData _ x xs e ->
fsep [hsep ["unquoteData", render x, fsep (fmap render xs), "="], render e]
Opaque _ ds ->
namedBlock "opaque" ds
Unfolding _ xs ->
fsep ("unfolding" : fmap render xs)
where
namedBlock s ds =
fsep
[ text s,
vcat $ fmap render ds
]
pHasEta0 :: HasEta0 -> Inlines
pHasEta0 = \case
YesEta -> "eta-equality"
NoEta () -> "no-eta-equality"
instance Render RecordDirective where
render = pRecordDirective
pRecordDirective ::
RecordDirective ->
Inlines
pRecordDirective = \case
Induction ind -> render ind
Constructor n inst -> hsep [pInst, "constructor", render n]
where
pInst = case inst of
InstanceDef {} -> "instance"
NotInstanceDef {} -> mempty
Eta eta -> pHasEta0 (rangedThing eta)
PatternOrCopattern {} -> "pattern"
#if MIN_VERSION_Agda(2,7,0)
pRecord ::
Erased ->
Name ->
[RecordDirective] ->
[LamBinding] ->
Maybe Expr ->
[Declaration] ->
Inlines
pRecord erased x directives tel me ds =
vcat
[ sep
[ hsep
[ "record",
renderErased erased (render x),
fsep (map render tel)
],
pType me
],
vcat $
concat
[ map render directives,
map render ds
]
]
where
pType (Just e) =
hsep
[ ":",
render e,
"where"
]
pType Nothing =
"where"
#else
pRecord ::
Name ->
RecordDirectives ->
[LamBinding] ->
Maybe Expr ->
[Declaration] ->
Inlines
pRecord x (RecordDirectives ind eta pat con) tel me cs =
sep
[ hsep
[ "record",
render x,
fcat (fmap render tel)
],
pType me,
vcat $
pInd
++ pEta
++ pCon
++ fmap render cs
]
where
pType (Just e) =
hsep
[ ":",
render e,
"where"
]
pType Nothing =
"where"
pInd = maybeToList $ text . show . rangedThing <$> ind
pEta =
maybeToList $
eta <&> \case
YesEta -> "eta-equality"
NoEta _ -> "no-eta-equality"
pCon = maybeToList $ (("constructor" <+>) . render) . fst <$> con
#endif
instance Render OpenShortHand where
render DoOpen = "open"
render DontOpen = mempty
instance Render Pragma where
render (OptionsPragma _ opts) = fsep $ fmap text $ "OPTIONS" : opts
render (BuiltinPragma _ b x) = hsep ["BUILTIN", text (rangedThing b), render x]
render (RewritePragma _ _ xs) =
hsep ["REWRITE", hsep $ fmap render xs]
#if MIN_VERSION_Agda(2,8,0)
render (CompilePragma _ b x e) =
hsep [ "COMPILE", render (rangedThing b), render x, textNonEmpty e ]
render (ForeignPragma _ b s) =
vcat $ hsep [ "FOREIGN", render (rangedThing b) ] : map text (lines s)
#else
render (CompilePragma _ b x e) =
hsep ["COMPILE", text (rangedThing b), render x, text e]
render (ForeignPragma _ b s) =
vcat $ text ("FOREIGN " ++ rangedThing b) : fmap text (lines s)
#endif
render (StaticPragma _ i) =
hsep ["STATIC", render i]
render (InjectivePragma _ i) =
hsep ["INJECTIVE", render i]
render (InlinePragma _ True i) =
hsep ["INLINE", render i]
render (InlinePragma _ False i) =
hsep ["NOINLINE", render i]
render (ImpossiblePragma _ strs) =
hsep $ "IMPOSSIBLE" : fmap text strs
render (EtaPragma _ x) =
hsep ["ETA", render x]
render (TerminationCheckPragma _ tc) =
case tc of
TerminationCheck -> __IMPOSSIBLE__
NoTerminationCheck -> "NO_TERMINATION_CHECK"
NonTerminating -> "NON_TERMINATING"
Terminating -> "TERMINATING"
TerminationMeasure _ x -> hsep ["MEASURE", render x]
render (NoCoverageCheckPragma _) = "NON_COVERING"
render (WarningOnUsage _ nm str) = hsep ["WARNING_ON_USAGE", render nm, text $ T.unpack str]
render (WarningOnImport _ str) = hsep ["WARNING_ON_IMPORT", text $ T.unpack str]
render (CatchallPragma _) = "CATCHALL"
render (DisplayPragma _ lhs rhs) = "DISPLAY" <+> fsep [render lhs <+> "=", render rhs]
render (NoPositivityCheckPragma _) = "NO_POSITIVITY_CHECK"
render (PolarityPragma _ q occs) =
hsep ("POLARITY" : render q : fmap render occs)
render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"
render (NotProjectionLikePragma _ q) =
hsep ["NOT_PROJECTION_LIKE", render q]
#if MIN_VERSION_Agda(2,7,0)
render (InjectiveForInferencePragma _ i) =
hsep ["INJECTIVE_FOR_INFERENCE", render i]
render (OverlapPragma _ x m) = hsep [render m, render x]
#endif
instance Render Fixity where
render (Fixity _ Unrelated _) = __IMPOSSIBLE__
render (Fixity _ (Related d) ass) = s <+> text (toStringWithoutDotZero d)
where
s = case ass of
LeftAssoc -> "infixl"
RightAssoc -> "infixr"
NonAssoc -> "infix"
instance Render NotationPart where
render = \case
IdPart x -> text $ rangedThing x
HolePart {} -> "_"
VarPart {} -> "_"
WildPart {} -> "_"
instance Render Fixity' where
render (Fixity' fix nota _)
| nota == noNotation = render fix
| otherwise = "syntax" <+> render nota
-- | Arg
instance (Render a) => Render (Arg a) where
renderPrec p (Arg ai e) = renderHiding ai localParens $ renderPrec p' e
where
p'
| visible ai = p
| otherwise = 0
localParens
| getOrigin ai == Substitution = parens
| otherwise = id
-- | Named NamedName (Named_)
instance (Render e) => Render (Named NamedName e) where
renderPrec p (Named nm e)
| Just s <- bareNameOf nm = mparens (p > 0) $ sep [text s <> " =", render e]
| otherwise = renderPrec p e
instance Render Pattern where
render = \case
IdentP _ x -> render x
AppP p1 p2 -> fsep [render p1, render p2]
RawAppP _ ps -> fsep $ fmap render (List2.toList ps)
OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) (toList ps))
HiddenP _ p -> braces' $ render p
InstanceP _ p -> dbraces $ render p
ParenP _ p -> parens $ render p
WildP _ -> "_"
AsP _ x p -> render x <> "@" <> render p
#if MIN_VERSION_Agda(2,8,0)
DotP _ _ p -> "." <> render p
#else
DotP _ p -> "." <> render p
#endif
AbsurdP _ -> "()"
LitP _ l -> render l
QuoteP _ -> "quote"
#if MIN_VERSION_Agda(2,8,0)
RecP _ _ fs -> sep [ "record", bracesAndSemicolons (map render fs) ]
EqualP _ es -> sep $ for (toList es) (\ (e1, e2) -> parens $ sep [render e1, "=", render e2])
#else
RecP _ fs -> sep ["record", bracesAndSemicolons (fmap render fs)]
EqualP _ es -> sep $ [parens (sep [render e1, "=", render e2]) | (e1, e2) <- es]
#endif
EllipsisP _ mp -> "..."
WithP _ p -> "|" <+> render p
bracesAndSemicolons :: [Inlines] -> Inlines
bracesAndSemicolons [] = "{}"
bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ fmap (";" <+>) ds ++ ["}"])
-- `prettyOpApp` for Agda 2.7.0.1 and below
renderOpApp ::
forall a.
(Render a) =>
QName ->
[NamedArg (MaybePlaceholder a)] ->
[Inlines]
renderOpApp q args = merge [] $ prOp moduleNames concreteNames args
where
-- ms: the module part of the name.
moduleNames = List1.init (qnameParts q)
-- xs: the concrete name (alternation of @Id@ and @Hole@)
concreteNames = case unqualify q of
Name _ _ xs -> List1.toList xs
NoName {} -> __IMPOSSIBLE__
prOp :: (Render a) => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]
prOp ms (Hole : xs) (e : es) =
case namedArg e of
Placeholder p -> (qual ms $ render e, Just p) : prOp [] xs es
NoPlaceholder {} -> (render e, Nothing) : prOp ms xs es
-- Module qualifier needs to go on section holes (#3072)
prOp _ (Hole : _) [] = __IMPOSSIBLE__
prOp ms (Id x : xs) es =
( qual ms $ render $ simpleName x,
Nothing
)
: prOp [] xs es
-- Qualify the name part with the module.
-- We then clear @ms@ such that the following name parts will not be qualified.
prOp _ [] es = fmap (\e -> (render e, Nothing)) es
qual ms' doc = hcat $ punctuate "." $ fmap render ms' ++ [doc]
-- Section underscores should be printed without surrounding
-- whitespace. This function takes care of that.
merge :: [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge before [] = reverse before
merge before ((d, Nothing) : after) = merge (d : before) after
merge before ((d, Just Beginning) : after) = mergeRight before d after
merge before ((d, Just End) : after) = case mergeLeft d before of
(d', bs) -> merge (d' : bs) after
merge before ((d, Just Middle) : after) = case mergeLeft d before of
(d', bs) -> mergeRight bs d' after
mergeRight before d after =
reverse before
++ case merge [] after of
[] -> [d]
a : as -> (d <> a) : as
mergeLeft d before = case before of
[] -> (d, [])
b : bs -> (b <> d, bs)
-- `prettyOpApp` for Agda 2.8.0 and above
renderOpApp280 ::
forall a.
(Render a) =>
Asp.Aspect ->
QName ->
List1 (NamedArg (MaybePlaceholder a)) ->
[Inlines]
renderOpApp280 asp q es = merge [] $ prOp ms xs $ List1.toList es
where
-- ms: the module part of the name.
ms = List1.init (qnameParts q)
-- xs: the concrete name (alternation of @Id@ and @Hole@)
xs = case unqualify q of
Name _ _ xs -> List1.toList xs
NoName{} -> __IMPOSSIBLE__
prOp :: (Render a) => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]
prOp ms (Hole : xs) (e : es) =
case namedArg e of
Placeholder p -> (qual ms $ render e, Just p) : prOp [] xs es
NoPlaceholder {} -> (render e, Nothing) : prOp ms xs es
-- Module qualifier needs to go on section holes (#3072)
prOp _ (Hole : _) [] = __IMPOSSIBLE__
prOp ms (Id x : xs) es = ( qual ms $ render $ simpleName x
, Nothing
) : prOp [] xs es
-- Qualify the name part with the module.
-- We then clear @ms@ such that the following name parts will not be qualified.
prOp _ [] es = map (\e -> (render e, Nothing)) es
qual ms doc = hcat $ punctuate "." $ map render ms ++ [doc]
-- Section underscores should be printed without surrounding
-- whitespace. This function takes care of that.
merge :: [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge before [] = reverse before
merge before ((d, Nothing) : after) = merge (d : before) after
merge before ((d, Just Beginning) : after) = mergeRight before d after
merge before ((d, Just End) : after) = case mergeLeft d before of
(d', bs) -> merge (d' : bs) after
merge before ((d, Just Middle) : after) = case mergeLeft d before of
(d', bs) -> mergeRight bs d' after
mergeRight before d after =
reverse before
++ case merge [] after of
[] -> [d]
a : as -> (d <> a) : as
mergeLeft d before = case before of
[] -> (d, [])
b : bs -> (b <> d, bs)
instance (Render a, Render b) => Render (ImportDirective' a b) where
render i =
sep
[ public (publicOpen i),
render $ using i,
renderHiding' $ hiding i,
rename $ impRenaming i
]
where
public Just {} = "public"
public Nothing = mempty
renderHiding' [] = mempty
renderHiding' xs = "hiding" <+> parens (fsep $ punctuate ";" $ fmap render xs)
rename [] = mempty
rename xs =
hsep
[ "renaming",
parens $ fsep $ punctuate ";" $ fmap render xs
]
instance (Render a, Render b) => Render (Using' a b) where
render UseEverything = mempty
render (Using xs) =
"using" <+> parens (fsep $ punctuate ";" $ fmap render xs)
instance (Render a, Render b) => Render (Renaming' a b) where
render (Renaming from to mfx _r) =
hsep
[ render from,
"to",
maybe mempty render mfx,
case to of
ImportedName a -> render a
ImportedModule b -> render b -- don't print "module" here
]
instance (Render a, Render b) => Render (ImportedName' a b) where
render (ImportedName a) = render a
render (ImportedModule b) = "module" <+> render b