module Agda.Syntax.Concrete.Pretty where
import Data.Char
import Data.Functor
import Data.Maybe
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import Agda.Syntax.Concrete
import Agda.Syntax.Fixity
import Agda.Syntax.Literal
import Agda.Syntax.Notation
import Agda.Syntax.Position
import Agda.Utils.Pretty
import Agda.Utils.String
#include "undefined.h"
import Agda.Utils.Impossible
instance Show Expr where show = show . pretty
instance Show Declaration where show = show . pretty
instance Show Pattern where show = show . pretty
instance Show TypedBinding where show = show . pretty
instance Show TypedBindings where show = show . pretty
instance Show LamBinding where show = show . pretty
instance Show ImportDirective where show = show . pretty
instance Show Pragma where show = show . pretty
instance Show RHS where show = show . pretty
braces' :: Doc -> Doc
braces' d = case render d of
'-':_ -> braces (text " " <> d)
_ -> braces d
dbraces :: Doc -> Doc
dbraces = braces . braces'
bracesAndSemicolons :: [Doc] -> Doc
bracesAndSemicolons [] = text "{}"
bracesAndSemicolons (d : ds) =
sep ([text "{" <+> d] ++ map (text ";" <+>) ds ++ [text "}"])
arrow, lambda :: Doc
arrow = text "\x2192"
lambda = text "\x03bb"
pHidden :: Pretty a => ArgInfo -> a -> Doc
pHidden i = bracks h . pretty
where bracks Hidden = braces'
bracks Instance = dbraces
bracks NotHidden= id
h = argInfoHiding i
pRelevance :: Pretty a => ArgInfo -> a -> Doc
pRelevance i a =
let d = pretty a
in if render d == "_" then d else pretty (argInfoRelevance i) <> d
instance (Pretty a, Pretty b) => Pretty (a, b) where
pretty (a, b) = parens $ pretty a <> comma <+> pretty b
instance Pretty (ThingWithFixity Name) where
pretty (ThingWithFixity n _) = pretty n
instance Pretty Relevance where
pretty Forced = empty
pretty UnusedArg = empty
pretty Relevant = empty
pretty Irrelevant = text "."
pretty NonStrict = text ".."
instance Pretty Induction where
pretty Inductive = text "data"
pretty CoInductive = text "codata"
instance Pretty (OpApp Expr) where
pretty (Ordinary e) = pretty e
pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)
instance Pretty Expr where
pretty e =
case e of
Ident x -> pretty x
Lit l -> pretty l
QuestionMark _ n -> text "?" <> maybe empty (text . show) n
Underscore _ n -> maybe underscore text n
App _ _ _ ->
case appView e of
AppView e1 args ->
fsep $ pretty e1 : map pretty args
RawApp _ es -> fsep $ map pretty es
OpApp _ q es -> fsep $ prettyOpApp q es
WithApp _ e es -> fsep $
pretty e : map ((text "|" <+>) . pretty) es
HiddenArg _ e -> braces' $ pretty e
InstanceArg _ e -> dbraces $ pretty e
Lam _ bs e ->
sep [ lambda <+> fsep (map pretty bs) <+> arrow
, nest 2 $ pretty e
]
AbsurdLam _ NotHidden -> lambda <+> text "()"
AbsurdLam _ Instance -> lambda <+> text "{{}}"
AbsurdLam _ Hidden -> lambda <+> text "{}"
ExtendedLam _ pes ->
lambda <+> bracesAndSemicolons (map (\(x,y,z) -> prettyClause x y z) pes)
where prettyClause lhs rhs wh = sep [ pretty lhs
, nest 2 $ pretty' rhs
] $$ nest 2 (pretty wh)
pretty' (RHS e) = arrow <+> pretty e
pretty' AbsurdRHS = empty
Fun _ e1 e2 ->
sep [ pretty e1 <+> arrow
, pretty e2
]
Pi tel e ->
sep [ pretty (Tel $ smashTel tel) <+> arrow
, pretty e
]
Set _ -> text "Set"
Prop _ -> text "Prop"
SetN _ n -> text "Set" <> text (showIndex n)
Let _ ds e ->
sep [ text "let" <+> vcat (map pretty ds)
, text "in" <+> pretty e
]
Paren _ e -> parens $ pretty e
As _ x e -> pretty x <> text "@" <> pretty e
Dot _ e -> text "." <> pretty e
Absurd _ -> text "()"
Rec _ xs -> sep [text "record", bracesAndSemicolons (map recPr xs)]
RecUpdate _ e xs ->
sep [text "record" <+> pretty e, bracesAndSemicolons (map recPr xs)]
ETel [] -> text "()"
ETel tel -> fsep $ map pretty tel
QuoteGoal _ x e -> sep [text "quoteGoal" <+> pretty x <+> text "in",
nest 2 $ pretty e]
QuoteContext _ x e -> sep [text "quoteContext" <+> pretty x <+> text "in",
nest 2 $ pretty e]
Quote _ -> text "quote"
QuoteTerm _ -> text "quoteTerm"
Unquote _ -> text "unquote"
Tactic _ t es ->
sep [ text "tactic" <+> pretty t
, fsep [ text "|" <+> pretty e | e <- es ]
]
DontCare e -> text "." <> parens (pretty e)
Equal _ a b -> pretty a <+> text "=" <+> pretty b
where
recPr (x, e) = sep [ pretty x <+> text "=" , nest 2 $ pretty e ]
instance Pretty BoundName where
pretty BName{ boundName = x, boundLabel = l }
| x == l = pretty x
| otherwise = pretty l <+> text "=" <+> pretty x
instance Pretty LamBinding where
pretty (DomainFree i x) = pRelevance i $ pHidden i $ pretty x
pretty (DomainFull b) = pretty b
instance Pretty TypedBindings where
pretty (TypedBindings _ a) =
pRelevance (argInfo a) $ bracks $ pretty $ WithColors (argColors a) $ unArg a
where
bracks = case getHiding a of
Hidden -> braces'
Instance -> dbraces
NotHidden | isMeta (unArg a) -> id
| otherwise -> parens
isMeta (TBind _ _ (Underscore _ Nothing)) = True
isMeta _ = False
newtype Tel = Tel Telescope
instance Pretty Tel where
pretty (Tel tel)
| any isMeta tel = text "∀" <+> fsep (map pretty tel)
| otherwise = fsep (map pretty tel)
where
isMeta (TypedBindings _ (Common.Arg _ (TBind _ _ (Underscore _ Nothing)))) = True
isMeta _ = False
instance Pretty ColoredTypedBinding where
pretty (WithColors [] (TBind _ xs (Underscore _ Nothing))) =
fsep (map pretty xs)
pretty (WithColors [] (TLet _ ds)) =
text "let" <+> vcat (map pretty ds)
pretty (WithColors _ (TLet _ _)) = __IMPOSSIBLE__
pretty (WithColors cs (TBind _ xs e)) =
sep [ fsep (map pretty xs)
, pColors ":" cs <+> pretty e
]
pColors :: String -> [Color] -> Doc
pColors s [] = text s
pColors s cs = text (s ++ "{") <+> fsep (map pretty cs) <+> text "}"
instance Pretty TypedBinding where
pretty (TBind _ xs e) =
sep [ fsep (map pretty xs)
, text ":" <+> pretty e
]
pretty (TLet _ ds) =
text "let" <+> vcat (map pretty ds)
smashTel :: Telescope -> Telescope
smashTel (TypedBindings r (Common.Arg i (TBind r' xs e)) :
TypedBindings _ (Common.Arg i' (TBind _ ys e')) : tel)
| show i == show i' && show e == show e' && all isUnnamed (xs ++ ys) =
smashTel (TypedBindings r (Common.Arg i (TBind r' (xs ++ ys) e)) : tel)
where
isUnnamed x = boundLabel x == boundName x
smashTel (b : tel) = b : smashTel tel
smashTel [] = []
instance Pretty RHS where
pretty (RHS e) = text "=" <+> pretty e
pretty AbsurdRHS = empty
instance Show WhereClause where show = show . pretty
instance Pretty WhereClause where
pretty NoWhere = empty
pretty (AnyWhere [Module _ x [] ds]) | isNoName (unqualify x)
= vcat [ text "where", nest 2 (vcat $ map pretty ds) ]
pretty (AnyWhere ds) = vcat [ text "where", nest 2 (vcat $ map pretty ds) ]
pretty (SomeWhere m ds) =
vcat [ hsep [ text "module", pretty m, text "where" ]
, nest 2 (vcat $ map pretty ds)
]
instance Show LHS where show = show . pretty
instance Pretty LHS where
pretty lhs = case lhs of
LHS p ps eqs es -> pr (pretty p) ps eqs es
Ellipsis _ ps eqs es -> pr (text "...") ps eqs es
where
pr d ps eqs es =
sep [ d
, nest 2 $ fsep $ map ((text "|" <+>) . pretty) ps
, nest 2 $ pThing "rewrite" eqs
, nest 2 $ pThing "with" es
]
pThing thing [] = empty
pThing thing (e : es) = fsep $ (text thing <+> pretty e)
: map ((text "|" <+>) . pretty) es
instance Show LHSCore where show = show . pretty
instance Pretty LHSCore where
pretty (LHSHead f ps) = sep $ pretty f : map (parens . pretty) ps
pretty (LHSProj d ps lhscore ps') = sep $
pretty d : map (parens . pretty) ps ++
parens (pretty lhscore) : map (parens . pretty) ps'
instance Pretty [Declaration] where
pretty = vcat . map pretty
instance Show ModuleApplication where show = show . pretty
instance Pretty ModuleApplication where
pretty (SectionApp _ bs e) = fsep (map pretty bs) <+> text "=" <+> pretty e
pretty (RecordModuleIFS _ rec) = text "=" <+> pretty rec <+> text "{{...}}"
instance Pretty Declaration where
pretty d =
case d of
TypeSig i x e ->
sep [ pRelevance i $ pretty x <+> pColors ":" (argInfoColors i)
, nest 2 $ pretty e
]
Field x (Common.Arg i e) ->
sep [ text "field"
, nest 2 $ pRelevance i $ pHidden i $
TypeSig (i {argInfoRelevance = Relevant}) x e
]
FunClause lhs rhs wh ->
sep [ pretty lhs
, nest 2 $ pretty rhs
] $$ nest 2 (pretty wh)
DataSig _ ind x tel e ->
sep [ hsep [ pretty ind
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ hsep
[ text ":"
, pretty e
]
]
Data _ ind x tel (Just e) cs ->
sep [ hsep [ pretty ind
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ hsep
[ text ":"
, pretty e
, text "where"
]
] $$ nest 2 (vcat $ map pretty cs)
Data _ ind x tel Nothing cs ->
sep [ hsep [ pretty ind
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ text "where"
] $$ nest 2 (vcat $ map pretty cs)
RecordSig _ x tel e ->
sep [ hsep [ text "record"
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ hsep
[ text ":"
, pretty e
]
]
Record _ x ind con tel me cs ->
sep [ hsep [ text "record"
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ pType me
] $$ nest 2 (vcat $ pInd ++
pCon ++
map pretty cs)
where pType (Just e) = hsep
[ text ":"
, pretty e
, text "where"
]
pType Nothing =
text "where"
pInd = maybeToList $ text . show . rangedThing <$> ind
pCon = maybeToList $ (text "constructor" <+>) . pretty <$> con
Infix f xs ->
pretty f <+> (fsep $ punctuate comma $ map pretty xs)
Syntax n xs -> text "syntax" <+> pretty n <+> text "..."
PatternSyn _ n as p -> text "pattern" <+> pretty n <+> fsep (map pretty as)
<+> text "=" <+> pretty p
Mutual _ ds -> namedBlock "mutual" ds
Abstract _ ds -> namedBlock "abstract" ds
Private _ ds -> namedBlock "private" ds
InstanceB _ ds -> namedBlock "instance" ds
Postulate _ ds -> namedBlock "postulate" ds
Primitive _ ds -> namedBlock "primitive" ds
Module _ x tel ds ->
hsep [ text "module"
, pretty x
, fcat (map pretty tel)
, text "where"
] $$ nest 2 (vcat $ map pretty ds)
ModuleMacro _ x (SectionApp _ [] e) DoOpen i | isNoName x ->
sep [ pretty DoOpen
, nest 2 $ pretty e
, nest 4 $ pretty i
]
ModuleMacro _ x (SectionApp _ tel e) open i ->
sep [ pretty open <+> text "module" <+> pretty x <+> fcat (map pretty tel)
, nest 2 $ text "=" <+> pretty e <+> pretty i
]
ModuleMacro _ x (RecordModuleIFS _ rec) open i ->
sep [ pretty open <+> text "module" <+> pretty x
, nest 2 $ text "=" <+> pretty rec <+> text "{{...}}"
]
Open _ x i -> hsep [ text "open", pretty x, pretty i ]
Import _ x rn open i ->
hsep [ pretty open, text "import", pretty x, as rn, pretty i ]
where
as Nothing = empty
as (Just x) = text "as" <+> pretty (asName x)
UnquoteDecl _ x t ->
sep [ text "unquoteDecl" <+> pretty x <+> text "=", nest 2 $ pretty t ]
Pragma pr -> sep [ text "{-#" <+> pretty pr, text "#-}" ]
where
namedBlock s ds =
sep [ text s
, nest 2 $ vcat $ map pretty ds
]
instance Pretty OpenShortHand where
pretty DoOpen = text "open"
pretty DontOpen = empty
instance Pretty Pragma where
pretty (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts
pretty (BuiltinPragma _ b x) = hsep [ text "BUILTIN", text b, pretty x ]
pretty (RewritePragma _ x) =
hsep [ text "REWRITE", pretty x ]
pretty (CompiledPragma _ x hs) =
hsep [ text "COMPILED", pretty x, text hs ]
pretty (CompiledExportPragma _ x hs) =
hsep [ text "COMPILED_EXPORT", pretty x, text hs ]
pretty (CompiledTypePragma _ x hs) =
hsep [ text "COMPILED_TYPE", pretty x, text hs ]
pretty (CompiledDataPragma _ x hs hcs) =
hsep $ [text "COMPILED_DATA", pretty x] ++ map text (hs : hcs)
pretty (CompiledEpicPragma _ x e) =
hsep [ text "COMPILED_EPIC", pretty x, text e ]
pretty (CompiledJSPragma _ x e) =
hsep [ text "COMPILED_JS", pretty x, text e ]
pretty (StaticPragma _ i) =
hsep $ [text "STATIC", pretty i]
pretty (ImportPragma _ i) =
hsep $ [text "IMPORT", text i]
pretty (ImpossiblePragma _) =
hsep $ [text "IMPOSSIBLE"]
pretty (EtaPragma _ x) =
hsep $ [text "ETA", pretty x]
pretty (TerminationCheckPragma _ tc) =
case tc of
TerminationCheck -> __IMPOSSIBLE__
NoTerminationCheck -> text "NO_TERMINATION_CHECK"
NonTerminating -> text "NON_TERMINATING"
Terminating -> text "TERMINATING"
TerminationMeasure _ x -> hsep $ [text "MEASURE", pretty x]
instance Pretty Fixity where
pretty (LeftAssoc _ n) = text "infixl" <+> text (show n)
pretty (RightAssoc _ n) = text "infixr" <+> text (show n)
pretty (NonAssoc _ n) = text "infix" <+> text (show n)
instance Pretty GenPart where
pretty (IdPart x) = text x
pretty BindHole{} = underscore
pretty NormalHole{} = underscore
instance Pretty Notation where
pretty = hcat . map pretty
instance Pretty Fixity' where
pretty (Fixity' fix nota)
| nota == defaultNotation = pretty fix
| otherwise = text "syntax" <+> pretty nota
instance Pretty e => Pretty (Arg e) where
pretty a =
pHidden (argInfo a) $ unArg a
instance Pretty e => Pretty (Named_ e) where
pretty (Named Nothing e) = pretty e
pretty (Named (Just s) e) = sep [ text (rawNameToString $ rangedThing s) <+> text "=", pretty e ]
instance Pretty [Pattern] where
pretty = fsep . map pretty
instance Pretty Pattern where
pretty p =
case p of
IdentP x -> pretty x
AppP p1 p2 -> sep [ pretty p1, nest 2 $ pretty p2 ]
RawAppP _ ps -> fsep $ map pretty ps
OpAppP _ q ps -> fsep $ prettyOpApp q ps
HiddenP _ p -> braces' $ pretty p
InstanceP _ p -> dbraces $ pretty p
ParenP _ p -> parens $ pretty p
WildP _ -> underscore
AsP _ x p -> pretty x <> text "@" <> pretty p
DotP _ p -> text "." <> pretty p
AbsurdP _ -> text "()"
LitP l -> pretty l
QuoteP _ -> text "quote"
prettyOpApp :: Pretty a => QName -> [a] -> [Doc]
prettyOpApp q es = prOp ms xs es
where
ms = init (qnameParts q)
xs = case unqualify q of
Name _ xs -> xs
NoName{} -> __IMPOSSIBLE__
prOp ms (Hole : xs) (e : es) = pretty e : prOp ms xs es
prOp _ (Hole : _) [] = __IMPOSSIBLE__
prOp ms (Id x : xs) es = pretty (foldr Qual (QName (Name noRange $ [Id x])) ms) : prOp [] xs es
prOp _ [] [] = []
prOp _ [] es = map pretty es
instance Pretty ImportDirective where
pretty i =
sep [ public (publicOpen i)
, pretty $ usingOrHiding i
, rename $ renaming i
]
where
public True = text "public"
public False = empty
rename [] = empty
rename xs = hsep [ text "renaming"
, parens $ fsep $ punctuate (text ";") $ map pr xs
]
pr r = hsep [ pretty (renFrom r), text "to", pretty (renTo r) ]
instance Pretty UsingOrHiding where
pretty (Hiding []) = empty
pretty (Hiding xs) =
text "hiding" <+> parens (fsep $ punctuate (text ";") $ map pretty xs)
pretty (Using xs) =
text "using" <+> parens (fsep $ punctuate (text ";") $ map pretty xs)
instance Pretty ImportedName where
pretty (ImportedName x) = pretty x
pretty (ImportedModule x) = text "module" <+> pretty x