diff options
Diffstat (limited to 'src/full/Agda/Syntax/Concrete/Pretty.hs')
| -rw-r--r-- | src/full/Agda/Syntax/Concrete/Pretty.hs | 53 |
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" |