module Agda.Syntax.Concrete.Pretty where
import Data.Char
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Fixity
import Agda.Syntax.Literal
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 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
arrow = text "\x2192"
lambda = text "\x03bb"
pHidden :: Pretty a => Hiding -> a -> Doc
pHidden Hidden = braces . pretty
pHidden NotHidden = pretty
instance Pretty Name where
pretty = text . show
instance Pretty QName where
pretty = text . show
instance Pretty Literal where
pretty (LitLevel _ n) = __IMPOSSIBLE__
pretty (LitInt _ n) = text $ show n
pretty (LitFloat _ x) = text $ show x
pretty (LitString _ s) = text $ showString' s ""
pretty (LitChar _ c) = text $ "'" ++ showChar' c "" ++ "'"
showString' :: String -> ShowS
showString' s =
foldr (.) id $ [ showString "\"" ] ++ map showChar' s ++ [ showString "\"" ]
showChar' :: Char -> ShowS
showChar' '"' = showString "\\\""
showChar' c
| escapeMe c = showLitChar c
| otherwise = showString [c]
where
escapeMe c = not (isPrint c) || c == '\\'
instance Pretty Induction where
pretty Inductive = text "data"
pretty CoInductive = text "codata"
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 -> text "_" <> maybe empty (text . show) n
App _ _ _ ->
case appView e of
AppView e1 args ->
fsep $ pretty e1 : map pretty args
RawApp _ es -> fsep $ map pretty es
OpApp _ (Name _ xs) es -> fsep $ prOp xs es
where
prOp (Hole : xs) (e : es) = pretty e : prOp xs es
prOp (Hole : _) [] = __IMPOSSIBLE__
prOp (Id x : xs) es = text x : prOp xs es
prOp [] es = map pretty es
OpApp _ (NoName _ _) _ -> __IMPOSSIBLE__
WithApp _ e es -> fsep $
pretty e : map ((text "|" <+>) . pretty) es
HiddenArg _ e -> braces $ pretty e
Lam _ bs e ->
sep [ lambda <+> fsep (map pretty bs) <+> arrow
, nest 2 $ pretty e
]
AbsurdLam _ NotHidden -> lambda <+> text "()"
AbsurdLam _ Hidden -> lambda <+> text "{}"
Fun _ e1 e2 ->
sep [ pretty e1 <+> arrow
, pretty e2
]
Pi tel e ->
sep [ fsep (map pretty 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"
, nest 2 $ braces $ fsep $ punctuate (text ";") $ map pr xs
]
where
pr (x, e) = sep [ pretty x <+> text "="
, nest 2 $ pretty e
]
ETel [] -> text "()"
ETel tel -> fsep $ map pretty tel
instance Pretty BoundName where
pretty = pretty . boundName
instance Pretty LamBinding where
pretty (DomainFree h x) = pHidden h (pretty x)
pretty (DomainFull b) = pretty b
instance Pretty TypedBindings where
pretty (TypedBindings _ h bs) =
bracks $ fsep $ punctuate semi $ map pretty bs
where
bracks = case h of
Hidden -> braces
NotHidden -> parens
instance Pretty TypedBinding where
pretty (TNoBind e) = pretty e
pretty (TBind _ xs e) =
sep [ fsep (punctuate comma $ map pretty xs)
, text ":" <+> pretty e
]
instance Pretty RHS where
pretty (RHS e) = text "=" <+> pretty e
pretty AbsurdRHS = empty
instance Pretty WhereClause where
pretty NoWhere = empty
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 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 Pretty [Declaration] where
pretty = vcat . map pretty
instance Pretty Declaration where
pretty d =
case d of
TypeSig x e -> sep [ pretty x <+> text ":"
, nest 2 $ pretty e
]
Field h x e -> sep [ text "field"
, nest 2 $ pHidden h (TypeSig x e)
]
FunClause lhs rhs wh ->
sep [ pretty lhs
, nest 2 $ pretty rhs
] $$ nest 2 (pretty wh)
Data _ ind x tel 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)
Record _ x con tel e cs ->
sep [ hsep [ text "record"
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ hsep
[ text ":"
, pretty e
, text "where"
]
] $$ nest 2 (vcat $ maybe [] (\c -> [text "constructor" <+> pretty c])
con ++
map pretty cs)
Infix f xs ->
pretty f <+> (fsep $ punctuate comma $ map pretty xs)
Mutual _ ds -> namedBlock "mutual" ds
Abstract _ ds -> namedBlock "abstract" ds
Private _ ds -> namedBlock "private" 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 tel e open i ->
sep [ pretty open <+> text "module" <+> pretty x <+> fcat (map pretty tel)
, nest 2 $ text "=" <+> pretty e <+> pretty i
]
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)
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 (CompiledPragma _ x hs) =
hsep [ text "COMPILED", 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 (ImportPragma _ i) =
hsep $ [text "IMPORT", text i]
pretty (ImpossiblePragma _) =
hsep $ [text "IMPOSSIBLE"]
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 e => Pretty (Arg e) where
pretty (Arg h e) = pHidden h e
instance Pretty e => Pretty (Named String e) where
pretty (Named Nothing e) = pretty e
pretty (Named (Just s) e) = sep [ text 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 _ (Name _ xs) ps -> fsep $ prOp xs ps
where
prOp (Hole : xs) (e : es) = pretty e : prOp xs es
prOp (Hole : _) [] = __IMPOSSIBLE__
prOp (Id x : xs) es = text x : prOp xs es
prOp [] [] = []
prOp [] (_ : _) = __IMPOSSIBLE__
OpAppP _ (NoName _ _) _ -> __IMPOSSIBLE__
HiddenP _ p -> braces $ pretty p
ParenP _ p -> parens $ pretty p
WildP _ -> text "_"
AsP _ x p -> pretty x <> text "@" <> pretty p
DotP _ p -> text "." <> pretty p
AbsurdP _ -> text "()"
LitP l -> pretty l
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