summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Concrete/Pretty.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Concrete/Pretty.hs')
-rw-r--r--src/full/Agda/Syntax/Concrete/Pretty.hs53
1 files changed, 35 insertions, 18 deletions
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
index 6683057..92922a4 100644
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -1,8 +1,6 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
{-| Pretty printer for the concrete syntax.
-}
@@ -20,6 +18,9 @@ import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Position
+import Agda.TypeChecking.Positivity.Occurrence
+
+import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty
@@ -162,6 +163,7 @@ instance Pretty Expr where
, text "in" <+> pretty e
]
Paren _ e -> parens $ pretty e
+ IdiomBrackets _ e -> text "(|" <+> pretty e <+> text "|)"
As _ x e -> pretty x <> text "@" <> pretty e
Dot _ e -> text "." <> pretty e
Absurd _ -> text "()"
@@ -255,8 +257,9 @@ instance Pretty WhereClause where
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" ]
+ pretty (SomeWhere m a ds) =
+ vcat [ hsep $ applyWhen (a == PrivateAccess UserWritten) (text "private" :)
+ [ text "module", pretty m, text "where" ]
, nest 2 (vcat $ map pretty ds)
]
@@ -300,13 +303,16 @@ instance Pretty Declaration where
]
Field inst x (Arg i e) ->
sep [ text "field"
- , nest 2 $ mkInst inst $
+ , nest 2 $ mkInst inst $ mkOverlap i $
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
+
+ mkOverlap i d | argInfoOverlappable i = text "overlap" <+> d
+ | otherwise = d
FunClause lhs rhs wh _ ->
sep [ pretty lhs
, nest 2 $ pretty rhs
@@ -376,7 +382,7 @@ instance Pretty Declaration where
<+> text "=" <+> pretty p
Mutual _ ds -> namedBlock "mutual" ds
Abstract _ ds -> namedBlock "abstract" ds
- Private _ ds -> namedBlock "private" ds
+ Private _ _ ds -> namedBlock "private" ds
InstanceB _ ds -> namedBlock "instance" ds
Macro _ ds -> namedBlock "macro" ds
Postulate _ ds -> namedBlock "postulate" ds
@@ -424,8 +430,8 @@ instance Pretty OpenShortHand where
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 (RewritePragma _ xs) =
+ hsep [ text "REWRITE", hsep $ map pretty xs ]
pretty (CompiledPragma _ x hs) =
hsep [ text "COMPILED", pretty x, text hs ]
pretty (CompiledExportPragma _ x hs) =
@@ -446,8 +452,6 @@ instance Pretty Pragma where
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) =
@@ -468,6 +472,8 @@ instance Pretty Pragma where
pretty (CatchallPragma _) = text "CATCHALL"
pretty (DisplayPragma _ lhs rhs) = text "DISPLAY" <+> sep [ pretty lhs <+> text "=", nest 2 $ pretty rhs ]
pretty (NoPositivityCheckPragma _) = text "NO_POSITIVITY_CHECK"
+ pretty (PolarityPragma _ q occs) =
+ hsep (text "NO_POSITIVITY_CHECK" : pretty q : map pretty occs)
instance Pretty Fixity where
pretty (Fixity _ Unrelated _) = __IMPOSSIBLE__
@@ -478,6 +484,17 @@ instance Pretty Fixity where
RightAssoc -> "infixr"
NonAssoc -> "infix"
+instance Pretty Occurrence where
+ pretty Unused = text "_"
+ pretty Mixed = text "*"
+ pretty JustNeg = text "-"
+ pretty JustPos = text "+"
+ pretty StrictPos = text "++"
+
+ -- No syntax has been assigned to GuardPos.
+
+ pretty GuardPos = __IMPOSSIBLE__
+
instance Pretty GenPart where
pretty (IdPart x) = text x
pretty BindHole{} = underscore
@@ -488,20 +505,20 @@ instance Pretty Notation where
pretty = hcat . map pretty
instance Pretty Fixity' where
- pretty (Fixity' fix nota)
+ pretty (Fixity' fix nota _)
| nota == noNotation = pretty fix
| otherwise = text "syntax" <+> pretty nota
-instance Pretty e => Pretty (Arg e) where
-- Andreas 2010-09-21: do not print relevance in general, only in function types!
-- Andreas 2010-09-24: and in record fields
- pretty a = -- pRelevance r $
- -- TODO guilhem: print colors
- prettyHiding (argInfo a) id $ pretty $ unArg a
+instance Pretty a => Pretty (Arg a) where
+ prettyPrec p (Arg ai e) = prettyHiding ai id $ prettyPrec p' e
+ where p' | getHiding ai == NotHidden = p
+ | otherwise = 0
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 ]
+ prettyPrec p (Named Nothing e) = prettyPrec p e
+ prettyPrec p (Named (Just s) e) = mparens (p > 0) $ sep [ text (rawNameToString $ rangedThing s) <+> text "=", pretty e ]
instance Pretty [Pattern] where
pretty = fsep . map pretty
@@ -518,7 +535,7 @@ instance Pretty Pattern where
ParenP _ p -> parens $ pretty p
WildP _ -> underscore
AsP _ x p -> pretty x <> text "@" <> pretty p
- DotP _ p -> text "." <> pretty p
+ DotP _ _ p -> text "." <> pretty p
AbsurdP _ -> text "()"
LitP l -> pretty l
QuoteP _ -> text "quote"