1{-# OPTIONS_GHC -fno-warn-orphans #-}
2
3
4{-| Pretty printer for the concrete syntax.
5-}
6module Agda.Syntax.Concrete.Pretty
7  ( module Agda.Syntax.Concrete.Pretty
8  , module Agda.Syntax.Concrete.Glyph
9  ) where
10
11import Prelude hiding ( null )
12
13import Data.Maybe
14import qualified Data.Foldable  as Fold
15import qualified Data.Semigroup as Semigroup
16import qualified Data.Strict.Maybe as Strict
17import qualified Data.Text as T
18
19import Agda.Syntax.Common
20import Agda.Syntax.Concrete
21import Agda.Syntax.Position
22import Agda.Syntax.Concrete.Glyph
23
24import Agda.Utils.Float (toStringWithoutDotZero)
25import Agda.Utils.Function
26import Agda.Utils.Functor
27import Agda.Utils.List1 ( List1, pattern (:|) )
28import qualified Agda.Utils.List1 as List1
29import qualified Agda.Utils.List2 as List2
30import Agda.Utils.Maybe
31import Agda.Utils.Null
32import Agda.Utils.Pretty
33
34import Agda.Utils.Impossible
35
36deriving instance Show Expr
37deriving instance (Show a) => Show (OpApp a)
38deriving instance Show Declaration
39deriving instance Show Pattern
40deriving instance Show a => Show (Binder' a)
41deriving instance Show TypedBinding
42deriving instance Show LamBinding
43deriving instance Show BoundName
44deriving instance Show ModuleAssignment
45deriving instance (Show a, Show b) => Show (ImportDirective' a b)
46deriving instance (Show a, Show b) => Show (Using' a b)
47deriving instance (Show a, Show b) => Show (Renaming' a b)
48deriving instance Show Pragma
49deriving instance Show RHS
50deriving instance Show LHS
51deriving instance Show LHSCore
52deriving instance Show LamClause
53deriving instance Show WhereClause
54deriving instance Show ModuleApplication
55deriving instance Show DoStmt
56deriving instance Show Module
57
58-- Lays out a list of documents [d₁, d₂, …] in the following way:
59-- @
60--   { d₁
61--   ; d₂
62--   ⋮
63--   }
64-- @
65-- If the list is empty, then the notation @{}@ is used.
66
67bracesAndSemicolons :: Foldable t => t Doc -> Doc
68bracesAndSemicolons ts = case Fold.toList ts of
69  []       -> "{}"
70  (d : ds) -> sep (["{" <+> d] ++ map (";" <+>) ds ++ ["}"])
71
72-- | @prettyHiding info visible doc@ puts the correct braces
73--   around @doc@ according to info @info@ and returns
74--   @visible doc@ if the we deal with a visible thing.
75prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
76prettyHiding a parens =
77  case getHiding a of
78    Hidden     -> braces'
79    Instance{} -> dbraces
80    NotHidden  -> parens
81
82prettyRelevance :: LensRelevance a => a -> Doc -> Doc
83prettyRelevance a d =
84  if render d == "_" then d else pretty (getRelevance a) <> d
85
86prettyQuantity :: LensQuantity a => a -> Doc -> Doc
87prettyQuantity a d =
88  if render d == "_" then d else pretty (getQuantity a) <+> d
89
90prettyErased :: Erased -> Doc -> Doc
91prettyErased = prettyQuantity . asQuantity
92
93prettyCohesion :: LensCohesion a => a -> Doc -> Doc
94prettyCohesion a d =
95  if render d == "_" then d else pretty (getCohesion a) <+> d
96
97prettyTactic :: BoundName -> Doc -> Doc
98prettyTactic = prettyTactic' . bnameTactic
99
100prettyTactic' :: TacticAttribute -> Doc -> Doc
101prettyTactic' Nothing  d = d
102prettyTactic' (Just t) d = "@" <> (parens ("tactic" <+> pretty t) <+> d)
103
104instance (Pretty a, Pretty b) => Pretty (a, b) where
105    pretty (a, b) = parens $ (pretty a <> comma) <+> pretty b
106
107instance Pretty (ThingWithFixity Name) where
108    pretty (ThingWithFixity n _) = pretty n
109
110instance Pretty a => Pretty (WithHiding a) where
111  pretty w = prettyHiding w id $ pretty $ dget w
112
113instance Pretty Relevance where
114  pretty Relevant   = empty
115  pretty Irrelevant = "."
116  pretty NonStrict  = ".."
117
118instance Pretty Q0Origin where
119  pretty = \case
120    Q0Inferred -> empty
121    Q0{}       -> "@0"
122    Q0Erased{} -> "@erased"
123
124instance Pretty Q1Origin where
125  pretty = \case
126    Q1Inferred -> empty
127    Q1{}       -> "@1"
128    Q1Linear{} -> "@linear"
129
130instance Pretty QωOrigin where
131  pretty = \case
132    QωInferred -> empty
133    Qω{}       -> "@ω"
134    QωPlenty{} -> "@plenty"
135
136instance Pretty Quantity where
137  pretty = \case
138    Quantity0 o -> ifNull (pretty o) "@0" id
139    Quantity1 o -> ifNull (pretty o) "@1" id
140    Quantityω o -> pretty o
141
142instance Pretty Cohesion where
143  pretty Flat   = "@♭"
144  pretty Continuous = mempty
145  pretty Squash  = "@⊤"
146
147instance Pretty Modality where
148  pretty mod = hsep
149    [ pretty (getRelevance mod)
150    , pretty (getQuantity mod)
151    , pretty (getCohesion mod)
152    ]
153
154instance Pretty (OpApp Expr) where
155  pretty (Ordinary e) = pretty e
156  pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)
157
158instance Pretty a => Pretty (MaybePlaceholder a) where
159  pretty Placeholder{}       = "_"
160  pretty (NoPlaceholder _ e) = pretty e
161
162instance Pretty Expr where
163    pretty e =
164        case e of
165            Ident x          -> pretty x
166            Lit _ l          -> pretty l
167            QuestionMark _ n -> "?" <> maybe empty (text . show) n
168            Underscore _ n   -> maybe underscore text n
169            App _ _ _        ->
170                case appView e of
171                    AppView e1 args     ->
172                        fsep $ pretty e1 : map pretty args
173--                      sep [ pretty e1
174--                          , nest 2 $ fsep $ map pretty args
175--                          ]
176            RawApp _ es    -> fsep $ map pretty $ List2.toList es
177            OpApp _ q _ es -> fsep $ prettyOpApp q es
178
179            WithApp _ e es -> fsep $
180              pretty e : map (("|" <+>) . pretty) es
181
182            HiddenArg _ e -> braces' $ pretty e
183            InstanceArg _ e -> dbraces $ pretty e
184            Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (fmap pretty bs) <+> absurd h
185            Lam _ bs e ->
186                sep [ lambda <+> fsep (fmap pretty bs) <+> arrow
187                    , nest 2 $ pretty e
188                    ]
189            AbsurdLam _ h -> lambda <+> absurd h
190            ExtendedLam _ e pes ->
191              lambda <+>
192              prettyErased e (bracesAndSemicolons (fmap pretty pes))
193            Fun _ e1 e2 ->
194                sep [ prettyCohesion e1 (prettyQuantity e1 (pretty e1)) <+> arrow
195                    , pretty e2
196                    ]
197            Pi tel e ->
198                sep [ pretty (Tel $ smashTel $ List1.toList tel) <+> arrow
199                    , pretty e
200                    ]
201            Let _ ds me  ->
202                sep [ "let" <+> vcat (fmap pretty ds)
203                    , maybe empty (\ e -> "in" <+> pretty e) me
204                    ]
205            Paren _ e -> parens $ pretty e
206            IdiomBrackets _ es ->
207              case es of
208                []   -> emptyIdiomBrkt
209                [e]  -> leftIdiomBrkt <+> pretty e <+> rightIdiomBrkt
210                e:es -> leftIdiomBrkt <+> pretty e <+> fsep (map (("|" <+>) . pretty) es) <+> rightIdiomBrkt
211            DoBlock _ ss -> "do" <+> vcat (fmap pretty ss)
212            As _ x e  -> pretty x <> "@" <> pretty e
213            Dot _ e   -> "." <> pretty e
214            DoubleDot _ e  -> ".." <> pretty e
215            Absurd _  -> "()"
216            Rec _ xs  -> sep ["record", bracesAndSemicolons (map pretty xs)]
217            RecUpdate _ e xs ->
218              sep ["record" <+> pretty e, bracesAndSemicolons (map pretty xs)]
219            ETel []  -> "()"
220            ETel tel -> fsep $ map pretty tel
221            Quote _ -> "quote"
222            QuoteTerm _ -> "quoteTerm"
223            Unquote _  -> "unquote"
224            Tactic _ t -> "tactic" <+> pretty t
225            -- Andreas, 2011-10-03 print irrelevant things as .(e)
226            DontCare e -> "." <> parens (pretty e)
227            Equal _ a b -> pretty a <+> "=" <+> pretty b
228            Ellipsis _  -> "..."
229            Generalized e -> pretty e
230        where
231          absurd NotHidden  = "()"
232          absurd Instance{} = "{{}}"
233          absurd Hidden     = "{}"
234
235instance (Pretty a, Pretty b) => Pretty (Either a b) where
236  pretty = either pretty pretty
237
238instance Pretty a => Pretty (FieldAssignment' a) where
239  pretty (FieldAssignment x e) = sep [ pretty x <+> "=" , nest 2 $ pretty e ]
240
241instance Pretty ModuleAssignment where
242  pretty (ModuleAssignment m es i) = fsep (pretty m : map pretty es) <+> pretty i
243
244instance Pretty LamClause where
245  pretty (LamClause ps rhs _) =
246    sep [ fsep (map pretty ps)
247        , nest 2 $ pretty' rhs
248        ]
249    where
250      pretty' (RHS e)   = arrow <+> pretty e
251      pretty' AbsurdRHS = empty
252
253instance Pretty BoundName where
254  pretty BName{ boundName = x } = pretty x
255
256data NamedBinding = NamedBinding
257  { withHiding   :: Bool
258  , namedBinding :: NamedArg Binder
259  }
260
261isLabeled :: NamedArg Binder -> Maybe ArgName
262isLabeled x
263  | visible x              = Nothing  -- Ignore labels on visible arguments
264  | Just l <- bareNameOf x = boolToMaybe (l /= nameToRawName (boundName $ binderName $ namedArg x)) l
265  | otherwise              = Nothing
266
267instance Pretty a => Pretty (Binder' a) where
268  pretty (Binder mpat n) = let d = pretty n in case mpat of
269    Nothing  -> d
270    Just pat -> d <+> "@" <+> parens (pretty pat)
271
272instance Pretty NamedBinding where
273  pretty (NamedBinding withH x) = prH $
274    if | Just l <- isLabeled x -> text l <+> "=" <+> pretty xb
275       | otherwise             -> pretty xb
276
277    where
278
279    xb = namedArg x
280    bn = binderName xb
281    prH | withH     = prettyRelevance x
282                    . prettyHiding x mparens
283                    . prettyCohesion x
284                    . prettyQuantity x
285                    . prettyTactic bn
286        | otherwise = id
287    -- Parentheses are needed when an attribute @... is present
288    mparens
289      | noUserQuantity x, Nothing <- bnameTactic bn = id
290      | otherwise = parens
291
292instance Pretty LamBinding where
293    pretty (DomainFree x) = pretty (NamedBinding True x)
294    pretty (DomainFull b) = pretty b
295
296instance Pretty TypedBinding where
297    pretty (TLet _ ds) = parens $ "let" <+> vcat (fmap pretty ds)
298    pretty (TBind _ xs (Underscore _ Nothing)) =
299      fsep (fmap (pretty . NamedBinding True) xs)
300    pretty (TBind _ xs e) = fsep
301      [ prettyRelevance y
302        $ prettyHiding y parens
303        $ prettyCohesion y
304        $ prettyQuantity y
305        $ prettyTactic (binderName $ namedArg y) $
306        sep [ fsep (map (pretty . NamedBinding False) ys)
307            , ":" <+> pretty e ]
308      | ys@(y : _) <- groupBinds $ List1.toList xs ]
309      where
310        groupBinds [] = []
311        groupBinds (x : xs)
312          | Just{} <- isLabeled x = [x] : groupBinds xs
313          | otherwise   = (x : ys) : groupBinds zs
314          where (ys, zs) = span (same x) xs
315                same x y = getArgInfo x == getArgInfo y && isNothing (isLabeled y)
316
317newtype Tel = Tel Telescope
318
319instance Pretty Tel where
320    pretty (Tel tel)
321      | any isMeta tel = forallQ <+> fsep (map pretty tel)
322      | otherwise      = fsep (map pretty tel)
323      where
324        isMeta (TBind _ _ (Underscore _ Nothing)) = True
325        isMeta _ = False
326
327smashTel :: Telescope -> Telescope
328smashTel (TBind r xs e  :
329          TBind _ ys e' : tel)
330  | prettyShow e == prettyShow e' = smashTel (TBind r (xs Semigroup.<> ys) e : tel)
331smashTel (b : tel) = b : smashTel tel
332smashTel [] = []
333
334
335instance Pretty RHS where
336    pretty (RHS e)   = "=" <+> pretty e
337    pretty AbsurdRHS = empty
338
339instance Pretty WhereClause where
340  pretty  NoWhere = empty
341  pretty (AnyWhere _ [Module _ x [] ds]) | isNoName (unqualify x)
342                       = vcat [ "where", nest 2 (vcat $ map pretty ds) ]
343  pretty (AnyWhere _ ds) = vcat [ "where", nest 2 (vcat $ map pretty ds) ]
344  pretty (SomeWhere _ m a ds) =
345    vcat [ hsep $ applyWhen (a == PrivateAccess UserWritten) ("private" :)
346             [ "module", pretty m, "where" ]
347         , nest 2 (vcat $ map pretty ds)
348         ]
349
350instance Pretty LHS where
351  pretty (LHS p eqs es) = sep
352    [ pretty p
353    , nest 2 $ if null eqs then empty else fsep $ map pretty eqs
354    , nest 2 $ prefixedThings "with" (map prettyWithd es)
355    ] where
356
357    prettyWithd :: WithExpr -> Doc
358    prettyWithd (Named nm wh) =
359      let e = pretty wh in
360      case nm of
361        Nothing -> e
362        Just n  -> pretty n <+> ":" <+> e
363
364instance Pretty LHSCore where
365  pretty (LHSHead f ps) = sep $ pretty f : map (parens . pretty) ps
366  pretty (LHSProj d ps lhscore ps') = sep $
367    pretty d : map (parens . pretty) ps ++
368    parens (pretty lhscore) : map (parens . pretty) ps'
369  pretty (LHSWith h wps ps) = if null ps then doc else
370      sep $ parens doc : map (parens . pretty) ps
371    where
372    doc = sep $ pretty h : map (("|" <+>) . pretty) wps
373  pretty (LHSEllipsis r p) = "..."
374
375instance Pretty ModuleApplication where
376  pretty (SectionApp _ bs e) = fsep (map pretty bs) <+> "=" <+> pretty e
377  pretty (RecordModuleInstance _ rec) = "=" <+> pretty rec <+> "{{...}}"
378
379instance Pretty DoStmt where
380  pretty (DoBind _ p e cs) =
381    ((pretty p <+> "←") <?> pretty e) <?> prCs cs
382    where
383      prCs [] = empty
384      prCs cs = "where" <?> vcat (map pretty cs)
385  pretty (DoThen e) = pretty e
386  pretty (DoLet _ ds) = "let" <+> vcat (fmap pretty ds)
387
388instance Pretty Declaration where
389    prettyList = vcat . map pretty
390    pretty d =
391        case d of
392            TypeSig i tac x e ->
393                sep [ prettyTactic' tac $ prettyRelevance i $ prettyCohesion i $ prettyQuantity i $ pretty x <+> ":"
394                    , nest 2 $ pretty e
395                    ]
396
397            FieldSig inst tac x (Arg i e) ->
398                mkInst inst $ mkOverlap i $
399                prettyRelevance i $ prettyHiding i id $ prettyCohesion i $ prettyQuantity i $
400                pretty $ TypeSig (setRelevance Relevant i) tac x e
401
402                where
403
404                  mkInst (InstanceDef _) d = sep [ "instance", nest 2 d ]
405                  mkInst NotInstanceDef  d = d
406
407                  mkOverlap i d | isOverlappable i = "overlap" <+> d
408                                | otherwise        = d
409
410            Field _ fs ->
411              sep [ "field"
412                  , nest 2 $ vcat (map pretty fs)
413                  ]
414            FunClause lhs rhs wh _ ->
415                sep [ pretty lhs
416                    , nest 2 $ pretty rhs
417                    ] $$ nest 2 (pretty wh)
418            DataSig _ x tel e ->
419                sep [ hsep  [ "data"
420                            , pretty x
421                            , fcat (map pretty tel)
422                            ]
423                    , nest 2 $ hsep
424                            [ ":"
425                            , pretty e
426                            ]
427                    ]
428            Data _ x tel e cs ->
429                sep [ hsep  [ "data"
430                            , pretty x
431                            , fcat (map pretty tel)
432                            ]
433                    , nest 2 $ hsep
434                            [ ":"
435                            , pretty e
436                            , "where"
437                            ]
438                    ] $$ nest 2 (vcat $ map pretty cs)
439            DataDef _ x tel cs ->
440                sep [ hsep  [ "data"
441                            , pretty x
442                            , fcat (map pretty tel)
443                            ]
444                    , nest 2 $ "where"
445                    ] $$ nest 2 (vcat $ map pretty cs)
446            RecordSig _ x tel e ->
447                sep [ hsep  [ "record"
448                            , pretty x
449                            , fcat (map pretty tel)
450                            ]
451                    , nest 2 $ hsep
452                            [ ":"
453                            , pretty e
454                            ]
455                    ]
456            Record _ x dir tel e cs ->
457              pRecord x dir tel (Just e) cs
458            RecordDef _ x dir tel cs ->
459              pRecord x dir tel Nothing cs
460            RecordDirective r -> pRecordDirective r
461            Infix f xs  ->
462                pretty f <+> fsep (punctuate comma $ fmap pretty xs)
463            Syntax n xs -> "syntax" <+> pretty n <+> "..."
464            PatternSyn _ n as p -> "pattern" <+> pretty n <+> fsep (map pretty as)
465                                     <+> "=" <+> pretty p
466            Mutual _ ds     -> namedBlock "mutual" ds
467            InterleavedMutual _ ds  -> namedBlock "interleaved mutual" ds
468            LoneConstructor _ ds -> namedBlock "constructor" ds
469            Abstract _ ds   -> namedBlock "abstract" ds
470            Private _ _ ds  -> namedBlock "private" ds
471            InstanceB _ ds  -> namedBlock "instance" ds
472            Macro _ ds      -> namedBlock "macro" ds
473            Postulate _ ds  -> namedBlock "postulate" ds
474            Primitive _ ds  -> namedBlock "primitive" ds
475            Generalize _ ds -> namedBlock "variable" ds
476            Module _ x tel ds ->
477                hsep [ "module"
478                     , pretty x
479                     , fcat (map pretty tel)
480                     , "where"
481                     ] $$ nest 2 (vcat $ map pretty ds)
482            ModuleMacro _ x (SectionApp _ [] e) DoOpen i | isNoName x ->
483                sep [ pretty DoOpen
484                    , nest 2 $ pretty e
485                    , nest 4 $ pretty i
486                    ]
487            ModuleMacro _ x (SectionApp _ tel e) open i ->
488                sep [ pretty open <+> "module" <+> pretty x <+> fcat (map pretty tel)
489                    , nest 2 $ "=" <+> pretty e <+> pretty i
490                    ]
491            ModuleMacro _ x (RecordModuleInstance _ rec) open i ->
492                sep [ pretty open <+> "module" <+> pretty x
493                    , nest 2 $ "=" <+> pretty rec <+> "{{...}}"
494                    ]
495            Open _ x i  -> hsep [ "open", pretty x, pretty i ]
496            Import _ x rn open i   ->
497                hsep [ pretty open, "import", pretty x, as rn, pretty i ]
498                where
499                    as Nothing  = empty
500                    as (Just x) = "as" <+> pretty (asName x)
501            UnquoteDecl _ xs t ->
502              sep [ "unquoteDecl" <+> fsep (map pretty xs) <+> "=", nest 2 $ pretty t ]
503            UnquoteDef _ xs t ->
504              sep [ "unquoteDef" <+> fsep (map pretty xs) <+> "=", nest 2 $ pretty t ]
505            Pragma pr   -> sep [ "{-#" <+> pretty pr, "#-}" ]
506        where
507            namedBlock s ds =
508                sep [ text s
509                    , nest 2 $ vcat $ map pretty ds
510                    ]
511
512pHasEta0 :: HasEta0 -> Doc
513pHasEta0 = \case
514  YesEta   -> "eta-equality"
515  NoEta () -> "no-eta-equality"
516
517pRecordDirective :: RecordDirective -> Doc
518pRecordDirective = \case
519  Induction ind -> pretty (rangedThing ind)
520  Constructor n inst -> hsep [ pInst, "constructor", pretty n ] where
521    pInst = case inst of
522      InstanceDef{} -> "instance"
523      NotInstanceDef{} -> empty
524  Eta eta -> pHasEta0 (rangedThing eta)
525  PatternOrCopattern{} -> "pattern"
526
527pRecord
528  :: Name
529  -> RecordDirectives
530  -> [LamBinding]
531  -> Maybe Expr
532  -> [Declaration]
533  -> Doc
534pRecord x (RecordDirectives ind eta pat con) tel me ds = vcat
535    [ sep
536      [ hsep  [ "record"
537              , pretty x
538              , fcat (map pretty tel)
539              ]
540      , nest 2 $ pType me
541      ]
542    , nest 2 $ vcat $ concat
543      [ pInd
544      , pEta
545      , pPat
546      , pCon
547      , map pretty ds
548      ]
549    ]
550  where pType (Just e) = hsep
551                [ ":"
552                , pretty e
553                , "where"
554                ]
555        pType Nothing  =
556                  "where"
557        pInd = maybeToList $ pretty . rangedThing <$> ind
558        pEta = maybeToList $ eta <&> pHasEta0
559        pPat = maybeToList $ "pattern" <$ pat
560        -- pEta = caseMaybe eta [] $ \case
561        --   YesEta -> [ "eta-equality" ]
562        --   NoEta  -> "no-eta-equality" : pPat
563        -- pPat = \case
564        --   PatternMatching   -> [ "pattern" ]
565        --   CopatternMatching -> []
566        pCon = maybeToList $ (("constructor" <+>) . pretty) . fst <$> con
567
568instance Pretty OpenShortHand where
569    pretty DoOpen = "open"
570    pretty DontOpen = empty
571
572instance Pretty Pragma where
573    pretty (OptionsPragma _ opts)  = fsep $ map text $ "OPTIONS" : opts
574    pretty (BuiltinPragma _ b x)   = hsep [ "BUILTIN", text (rangedThing b), pretty x ]
575    pretty (RewritePragma _ _ xs)    =
576      hsep [ "REWRITE", hsep $ map pretty xs ]
577    pretty (CompilePragma _ b x e) =
578      hsep [ "COMPILE", text (rangedThing b), pretty x, text e ]
579    pretty (ForeignPragma _ b s) =
580      vcat $ text ("FOREIGN " ++ rangedThing b) : map text (lines s)
581    pretty (StaticPragma _ i) =
582      hsep $ ["STATIC", pretty i]
583    pretty (InjectivePragma _ i) =
584      hsep $ ["INJECTIVE", pretty i]
585    pretty (InlinePragma _ True i) =
586      hsep $ ["INLINE", pretty i]
587    pretty (InlinePragma _ False i) =
588      hsep $ ["NOINLINE", pretty i]
589    pretty (ImpossiblePragma _ strs) =
590      hsep $ ["IMPOSSIBLE"] ++ map text strs
591    pretty (EtaPragma _ x) =
592      hsep $ ["ETA", pretty x]
593    pretty (TerminationCheckPragma _ tc) =
594      case tc of
595        TerminationCheck       -> __IMPOSSIBLE__
596        NoTerminationCheck     -> "NO_TERMINATION_CHECK"
597        NonTerminating         -> "NON_TERMINATING"
598        Terminating            -> "TERMINATING"
599        TerminationMeasure _ x -> hsep $ ["MEASURE", pretty x]
600    pretty (NoCoverageCheckPragma _) = "NON_COVERING"
601    pretty (WarningOnUsage _ nm str) = hsep [ "WARNING_ON_USAGE", pretty nm, text (T.unpack str) ]
602    pretty (WarningOnImport _ str)   = hsep [ "WARNING_ON_IMPORT", text (T.unpack str) ]
603    pretty (CatchallPragma _) = "CATCHALL"
604    pretty (DisplayPragma _ lhs rhs) = "DISPLAY" <+> sep [ pretty lhs <+> "=", nest 2 $ pretty rhs ]
605    pretty (NoPositivityCheckPragma _) = "NO_POSITIVITY_CHECK"
606    pretty (PolarityPragma _ q occs) =
607      hsep ("POLARITY" : pretty q : map pretty occs)
608    pretty (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"
609
610instance Pretty Associativity where
611  pretty = \case
612    LeftAssoc  -> "infixl"
613    RightAssoc -> "infixr"
614    NonAssoc   -> "infix"
615
616instance Pretty FixityLevel where
617  pretty = \case
618    Unrelated  -> empty
619    Related d  -> text $ toStringWithoutDotZero d
620
621instance Pretty Fixity where
622  pretty (Fixity _ level ass) = case level of
623    Unrelated  -> empty
624    Related{}  -> pretty ass <+> pretty level
625
626instance Pretty GenPart where
627    pretty (IdPart x)   = text $ rangedThing x
628    pretty BindHole{}   = underscore
629    pretty NormalHole{} = underscore
630    pretty WildHole{}   = underscore
631
632    prettyList = hcat . map pretty
633
634instance Pretty Fixity' where
635    pretty (Fixity' fix nota _range)
636      | null nota = pretty fix
637      | otherwise = "syntax" <+> pretty nota
638
639 -- Andreas 2010-09-21: do not print relevance in general, only in function types!
640 -- Andreas 2010-09-24: and in record fields
641instance Pretty a => Pretty (Arg a) where
642  prettyPrec p (Arg ai e) = prettyHiding ai localParens $ prettyPrec p' e
643      where p' | visible ai = p
644               | otherwise  = 0
645            localParens | getOrigin ai == Substitution = parens
646                        | otherwise = id
647
648instance Pretty e => Pretty (Named_ e) where
649  prettyPrec p (Named nm e)
650    | Just s <- bareNameOf nm = mparens (p > 0) $ sep [ text s <+> "=", pretty e ]
651    | otherwise               = prettyPrec p e
652
653instance Pretty Pattern where
654    prettyList = fsep . map pretty
655    pretty = \case
656            IdentP x        -> pretty x
657            AppP p1 p2      -> sep [ pretty p1, nest 2 $ pretty p2 ]
658            RawAppP _ ps    -> fsep $ map pretty $ List2.toList ps
659            OpAppP _ q _ ps -> fsep $ prettyOpApp q $ fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps
660            HiddenP _ p     -> braces' $ pretty p
661            InstanceP _ p   -> dbraces $ pretty p
662            ParenP _ p      -> parens $ pretty p
663            WildP _         -> underscore
664            AsP _ x p       -> pretty x <> "@" <> pretty p
665            DotP _ p        -> "." <> pretty p
666            AbsurdP _       -> "()"
667            LitP _ l        -> pretty l
668            QuoteP _        -> "quote"
669            RecP _ fs       -> sep [ "record", bracesAndSemicolons (map pretty fs) ]
670            EqualP _ es     -> sep $ [ parens (sep [pretty e1, "=", pretty e2]) | (e1,e2) <- es ]
671            EllipsisP _ mp  -> "..."
672            WithP _ p       -> "|" <+> pretty p
673
674prettyOpApp :: forall a .
675  Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
676prettyOpApp q es = merge [] $ prOp ms xs es
677  where
678    -- ms: the module part of the name.
679    ms = List1.init (qnameParts q)
680    -- xs: the concrete name (alternation of @Id@ and @Hole@)
681    xs = case unqualify q of
682           Name _ _ xs    -> List1.toList xs
683           NoName{}       -> __IMPOSSIBLE__
684
685    prOp :: [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
686    prOp ms (Hole : xs) (e : es) =
687      case namedArg e of
688        Placeholder p   -> (qual ms $ pretty e, Just p) : prOp [] xs es
689        NoPlaceholder{} -> (pretty e, Nothing) : prOp ms xs es
690          -- Module qualifier needs to go on section holes (#3072)
691    prOp _  (Hole : _)  []       = __IMPOSSIBLE__
692    prOp ms (Id x : xs) es       = ( qual ms $ pretty $ simpleName x
693                                   , Nothing
694                                   ) : prOp [] xs es
695      -- Qualify the name part with the module.
696      -- We then clear @ms@ such that the following name parts will not be qualified.
697
698    prOp _  []       es          = map (\e -> (pretty e, Nothing)) es
699
700    qual ms doc = hcat $ punctuate "." $ map pretty ms ++ [doc]
701
702    -- Section underscores should be printed without surrounding
703    -- whitespace. This function takes care of that.
704    merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
705    merge before []                            = reverse before
706    merge before ((d, Nothing) : after)        = merge (d : before) after
707    merge before ((d, Just Beginning) : after) = mergeRight before d after
708    merge before ((d, Just End)       : after) = case mergeLeft d before of
709                                                   (d, bs) -> merge (d : bs) after
710    merge before ((d, Just Middle)    : after) = case mergeLeft d before of
711                                                   (d, bs) -> mergeRight bs d after
712
713    mergeRight before d after =
714      reverse before ++
715      case merge [] after of
716        []     -> [d]
717        a : as -> (d <> a) : as
718
719    mergeLeft d before = case before of
720      []     -> (d,      [])
721      b : bs -> (b <> d, bs)
722
723instance (Pretty a, Pretty b) => Pretty (ImportDirective' a b) where
724    pretty i =
725        sep [ public (publicOpen i)
726            , pretty $ using i
727            , prettyHiding $ hiding i
728            , rename $ impRenaming i
729            ]
730        where
731            public Just{}  = "public"
732            public Nothing = empty
733
734            prettyHiding [] = empty
735            prettyHiding xs = "hiding" <+> parens (fsep $ punctuate ";" $ map pretty xs)
736
737            rename [] = empty
738            rename xs = hsep [ "renaming"
739                             , parens $ fsep $ punctuate ";" $ map pretty xs
740                             ]
741
742instance (Pretty a, Pretty b) => Pretty (Using' a b) where
743    pretty UseEverything = empty
744    pretty (Using xs)    =
745        "using" <+> parens (fsep $ punctuate ";" $ map pretty xs)
746
747instance (Pretty a, Pretty b) => Pretty (Renaming' a b) where
748    pretty (Renaming from to mfx _r) = hsep
749      [ pretty from
750      , "to"
751      , maybe empty pretty mfx
752      , case to of
753          ImportedName a   -> pretty a
754          ImportedModule b -> pretty b   -- don't print "module" here
755      ]
756
757instance (Pretty a, Pretty b) => Pretty (ImportedName' a b) where
758    pretty (ImportedName   a) = pretty a
759    pretty (ImportedModule b) = "module" <+> pretty b
760