module Agda.Syntax.Concrete.Pretty where
import Prelude hiding (null)
import Data.Functor
import Data.Maybe
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Position
import Agda.Utils.Functor
import Agda.Utils.Null
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 (Pretty a, Pretty b) => Show (ImportDirective' a b)
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"
prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding a parens =
case getHiding a of
Hidden -> braces'
Instance -> dbraces
NotHidden -> parens
prettyRelevance :: LensRelevance a => a -> Doc -> Doc
prettyRelevance a d =
if render d == "_" then d else pretty (getRelevance a) <> 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 a => Pretty (WithHiding a) where
pretty w = prettyHiding w id $ pretty $ dget w
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 a => Pretty (MaybePlaceholder a) where
pretty Placeholder{} = text "_"
pretty (NoPlaceholder e) = pretty 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 pretty xs)]
RecUpdate _ e xs ->
sep [text "record" <+> pretty e, bracesAndSemicolons (map pretty xs)]
ETel [] -> text "()"
ETel tel -> fsep $ map pretty tel
QuoteGoal _ x e -> sep [text "quoteGoal" <+> pretty x <+> text "in",
nest 2 $ pretty e]
QuoteContext _ -> text "quoteContext"
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
instance (Pretty a, Pretty b) => Pretty (Either a b) where
pretty = either pretty pretty
instance Pretty a => Pretty (FieldAssignment' a) where
pretty (FieldAssignment x e) = sep [ pretty x <+> text "=" , nest 2 $ pretty e ]
instance Pretty ModuleAssignment where
pretty (ModuleAssignment m es i) = (fsep $ pretty m : map pretty es) <+> pretty i
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) = prettyRelevance i $ prettyHiding i id $ pretty x
pretty (DomainFull b) = pretty b
instance Pretty TypedBindings where
pretty (TypedBindings _ a) = prettyRelevance a $ prettyHiding a p $
pretty $ unArg a
where
p | isUnderscore (unArg a) = id
| otherwise = parens
isUnderscore (TBind _ _ (Underscore _ Nothing)) = True
isUnderscore _ = 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 _ (Arg _ (TBind _ _ (Underscore _ Nothing)))) = True
isMeta _ = False
instance Pretty TypedBinding where
pretty (TBind _ xs (Underscore _ Nothing)) =
fsep (map pretty xs)
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 (Arg i (TBind r' xs e)) :
TypedBindings _ (Arg i' (TBind _ ys e')) : tel)
| show i == show i' && show e == show e' && all (isUnnamed . dget) (xs ++ ys) =
smashTel (TypedBindings r (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 [ prettyRelevance i $ pretty x <+> text ":"
, nest 2 $ pretty e
]
Field inst x (Arg i e) ->
sep [ text "field"
, nest 2 $ mkInst inst $
prettyRelevance i $ prettyHiding i id $
pretty $ TypeSig (i {argInfoRelevance = Relevant}) x e
]
where
mkInst InstanceDef d = sep [ text "instance", nest 2 d ]
mkInst NotInstanceDef d = d
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 eta con tel me cs ->
sep [ hsep [ text "record"
, pretty x
, fcat (map pretty tel)
]
, nest 2 $ pType me
] $$ nest 2 (vcat $ pInd ++
pEta ++
pCon ++
map pretty cs)
where pType (Just e) = hsep
[ text ":"
, pretty e
, text "where"
]
pType Nothing =
text "where"
pInd = maybeToList $ text . show . rangedThing <$> ind
pEta = maybeToList $ (\x -> if x then text "eta-equality" else text "no-eta-equality") <$> eta
pCon = maybeToList $ (text "constructor" <+>) . pretty <$> fst <$> 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
Macro _ ds -> namedBlock "macro" 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 _ xs t ->
sep [ text "unquoteDecl" <+> fsep (map pretty xs) <+> text "=", nest 2 $ pretty t ]
UnquoteDef _ xs t ->
sep [ text "unquoteDef" <+> fsep (map pretty xs) <+> 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 (CompiledDeclareDataPragma _ x hs) =
hsep [ text "COMPILED_DECLARE_DATA", 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 (CompiledUHCPragma _ x e) =
hsep [ text "COMPILED_UHC", pretty x, text e ]
pretty (CompiledDataUHCPragma _ x crd crcs) =
hsep $ [ text "COMPILED_DATA_UHC", pretty x] ++ map text (crd : crcs)
pretty (HaskellCodePragma _ s) =
vcat (text "HASKELL" : map text (lines s))
pretty (NoSmashingPragma _ i) =
hsep $ [text "NO_SMASHING", pretty i]
pretty (StaticPragma _ i) =
hsep $ [text "STATIC", pretty i]
pretty (InlinePragma _ i) =
hsep $ [text "INLINE", pretty i]
pretty (ImportPragma _ i) =
hsep $ [text "IMPORT", text i]
pretty (ImportUHCPragma _ i) =
hsep $ [text "IMPORT_UHC", text i]
pretty (ImpossiblePragma _) =
hsep $ [text "IMPOSSIBLE"]
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]
pretty (CatchallPragma _) = text "CATCHALL"
pretty (DisplayPragma _ lhs rhs) = text "DISPLAY" <+> sep [ pretty lhs <+> text "=", nest 2 $ pretty rhs ]
pretty (NoPositivityCheckPragma _) = text "NO_POSITIVITY_CHECK"
instance Pretty Fixity where
pretty (Fixity _ Unrelated _) = __IMPOSSIBLE__
pretty (Fixity _ (Related n) ass) = text s <+> text (show n)
where
s = case ass of
LeftAssoc -> "infixl"
RightAssoc -> "infixr"
NonAssoc -> "infix"
instance Pretty GenPart where
pretty (IdPart x) = text x
pretty BindHole{} = underscore
pretty NormalHole{} = underscore
pretty WildHole{} = underscore
instance Pretty Notation where
pretty = hcat . map pretty
instance Pretty Fixity' where
pretty (Fixity' fix nota)
| nota == noNotation = pretty fix
| otherwise = text "syntax" <+> pretty nota
instance Pretty e => Pretty (Arg e) where
pretty a =
prettyHiding (argInfo a) id $ pretty $ 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 (fmap (fmap (fmap NoPlaceholder)) 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"
RecP _ fs -> sep [ text "record", bracesAndSemicolons (map pretty fs) ]
prettyOpApp ::
Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp q es = merge [] $ 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, case namedArg e of
Placeholder p -> Just p
_ -> Nothing) :
prOp ms xs es
prOp _ (Hole : _) [] = __IMPOSSIBLE__
prOp ms (Id x : xs) es = ( pretty (foldr Qual (QName (Name noRange $ [Id x])) ms)
, Nothing
) : prOp [] xs es
prOp _ [] [] = []
prOp _ [] es = map (\e -> (pretty e, Nothing)) es
merge :: [Doc] -> [(Doc, Maybe Placeholder)] -> [Doc]
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 (Pretty a, Pretty b) => Pretty (ImportDirective' a b) where
pretty i =
sep [ public (publicOpen i)
, pretty $ using i
, prettyHiding $ hiding i
, rename $ impRenaming i
]
where
public True = text "public"
public False = empty
prettyHiding [] = empty
prettyHiding xs = text "hiding" <+> parens (fsep $ punctuate (text ";") $ map pretty xs)
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 a, Pretty b) => Pretty (Using' a b) where
pretty UseEverything = empty
pretty (Using xs) =
text "using" <+> parens (fsep $ punctuate (text ";") $ map pretty xs)
instance (Pretty a, Pretty b) => Pretty (ImportedName' a b) where
pretty (ImportedName x) = pretty x
pretty (ImportedModule x) = text "module" <+> pretty x