    {-# OPTIONS_GHC -fno-warn-orphans #-}

    {-| Pretty printer for the concrete syntax.
    -}
    module Agda.Syntax.Concrete.Pretty
      ( module Agda.Syntax.Concrete.Pretty
      , module Agda.Syntax.Concrete.Glyph
      ) where

    import Prelude hiding ( null )

    import Data.Maybe
    import qualified Data.Foldable  as Fold
    import qualified Data.Semigroup as Semigroup
    import qualified Data.Strict.Maybe as Strict
    import qualified Data.Text as T

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Glyph

    import Agda.Utils.Float (toStringWithoutDotZero)
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.List2 as List2
    import Agda.Utils.Maybe
    import Agda.Utils.Null
    import qualified Agda.Syntax.Common.Aspect as Asp
    import Agda.Syntax.Common.Pretty
    import Agda.Interaction.Options ( HasOptions(pragmaOptions), optPolarity )

    import Agda.Utils.Impossible

    deriving instance Show Expr
    deriving instance (Show a) => Show (OpApp a)
    deriving instance Show Declaration
    deriving instance Show Pattern
    deriving instance Show a => Show (Binder' a)
    deriving instance Show TypedBinding
    deriving instance Show LamBinding
    deriving instance Show BoundName
    deriving instance Show ModuleAssignment
    deriving instance Show Pragma
    deriving instance Show RHS
    deriving instance Show LHS
    deriving instance Show LHSCore
    deriving instance Show LamClause
    deriving instance Show WhereClause
    deriving instance Show ModuleApplication
    deriving instance Show DoStmt
    deriving instance Show Module

    -- Lays out a list of documents [d₁, d₂, …] in the following way:
    -- @
    --   { d₁
    --   ; d₂
    --   ⋮
    --   }
    -- @
    -- If the list is empty, then the notation @{}@ is used.

    bracesAndSemicolons :: Foldable t => t Doc -> Doc
    bracesAndSemicolons :: forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons t Doc
    ts = case t Doc -> [Doc]
    forall a. t a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList t Doc
    ts of
      []       -> Doc
    "{}"
      (Doc
    d : [Doc]
    ds) -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep ([Doc
    "{" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    d] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc
    ";" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) [Doc]
    ds [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc
    "}"])

    prettyTactic :: BoundName -> Doc -> Doc
    prettyTactic :: BoundName -> Doc -> Doc
    prettyTactic = TacticAttribute -> Doc -> Doc
    prettyTactic' (TacticAttribute -> Doc -> Doc)
    -> (BoundName -> TacticAttribute) -> BoundName -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BoundName -> TacticAttribute
    bnameTactic

    prettyFiniteness :: BoundName -> Doc -> Doc
    prettyFiniteness :: BoundName -> Doc -> Doc
    prettyFiniteness BoundName
    name
      | BoundName -> Bool
    bnameIsFinite BoundName
    name = (Doc
    "@finite" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)
      | Bool
    otherwise = Doc -> Doc
    forall a. a -> a
    id

    prettyTactic' :: TacticAttribute -> Doc -> Doc
    prettyTactic' :: TacticAttribute -> Doc -> Doc
    prettyTactic' TacticAttribute
    t = (TacticAttribute -> Doc
    forall a. Pretty a => a -> Doc
    pretty TacticAttribute
    t Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)

    instance Pretty a => Pretty (TacticAttribute' a) where
      pretty :: TacticAttribute' a -> Doc
    pretty (TacticAttribute Maybe (Ranged a)
    t) =
        Doc -> Doc -> (Doc -> Doc) -> Doc
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull (Maybe (Ranged a) -> Doc
    forall a. Pretty a => a -> Doc
    pretty Maybe (Ranged a)
    t) Doc
    forall a. Null a => a
    empty \ Doc
    d -> Doc
    "@" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    parens (Doc
    "tactic" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    d)

    instance Pretty (ThingWithFixity Name) where
        pretty :: ThingWithFixity Name -> Doc
    pretty (ThingWithFixity Name
    n Fixity'
    _) = Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n

    -- | Show the attributes necessary to recover a modality, in long-form
    -- (e.g. using at-syntax rather than dots). For the default modality,
    -- the result is at-ω (rather than the empty document). Suitable for
    -- showing modalities outside of binders.
    attributesForModality :: HasOptions m => Modality -> m Doc
    attributesForModality :: forall (m :: * -> *). HasOptions m => Modality -> m Doc
    attributesForModality mod :: Modality
    mod@(Modality Relevance
    r Quantity
    q Cohesion
    c PolarityModality
    p)
      | Modality
    mod Modality -> [Modality] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Modality
    defaultCheckModality, Modality
    defaultModality] = do
          showPolarity <- PragmaOptions -> Bool
    optPolarity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
          pure $ text "@ω" <+> if showPolarity then polarity else empty
      | Bool
    otherwise = Doc -> m Doc
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc -> m Doc) -> Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Maybe Doc] -> [Doc]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe Doc
    relevance, Maybe Doc
    quantity, Maybe Doc
    cohesion, Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    polarity]
      where
        relevance :: Maybe Doc
    relevance = case Relevance
    r of
          Relevant        {} -> Maybe Doc
    forall a. Maybe a
    Nothing
          Irrelevant      {} -> Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    "@irrelevant"
          ShapeIrrelevant {} -> Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    "@shape-irrelevant"
        quantity :: Maybe Doc
    quantity = case Quantity
    q of
          Quantity0{} -> Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    "@0"
          Quantity1{} -> Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    "@1"
          Quantityω{} -> Maybe Doc
    forall a. Maybe a
    Nothing
        cohesion :: Maybe Doc
    cohesion = case Cohesion
    c of
          Flat{}       -> Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    "@♭"
          Continuous{} -> Maybe Doc
    forall a. Maybe a
    Nothing
          Squash{}     -> Doc -> Maybe Doc
    forall a. a -> Maybe a
    Just Doc
    "@⊤"
        polarity :: Doc
    polarity = case PolarityModality -> ModalPolarity
    modPolarityAnn PolarityModality
    p of
          ModalPolarity
    MixedPolarity    -> Doc
    "@mixed"
          ModalPolarity
    Positive         -> Doc
    "@+"
          ModalPolarity
    Negative         -> Doc
    "@-"
          ModalPolarity
    StrictlyPositive -> Doc
    "@++"
          ModalPolarity
    UnusedPolarity   -> Doc
    "@unused"

    instance Pretty (OpApp Expr) where
      pretty :: OpApp Expr -> Doc
    pretty (Ordinary Expr
    e) = Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
      pretty (SyntaxBindingLambda Range
    r List1 LamBinding
    bs Expr
    e) = Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Range -> List1 LamBinding -> Expr -> Expr
    Lam Range
    r List1 LamBinding
    bs Expr
    e)

    instance Pretty a => Pretty (MaybePlaceholder a) where
      pretty :: MaybePlaceholder a -> Doc
    pretty Placeholder{}       = Doc
    "_"
      pretty (NoPlaceholder Maybe PositionInName
    _ a
    e) = a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e

    instance Pretty Expr where
        pretty :: Expr -> Doc
    pretty = \case
                Ident QName
    x          -> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
                KnownIdent NameKind
    nk QName
    x  -> Aspect -> Doc -> Doc
    annotateAspect (Maybe NameKind -> Bool -> Aspect
    Asp.Name (NameKind -> Maybe NameKind
    forall a. a -> Maybe a
    Just NameKind
    nk) Bool
    False) (QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x)
                Lit Range
    _ Literal
    l          -> Literal -> Doc
    forall a. Pretty a => a -> Doc
    pretty Literal
    l
                QuestionMark Range
    _ Maybe Int
    n -> Doc -> Doc
    hlSymbol Doc
    "?" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> (Int -> Doc) -> Maybe Int -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Null a => a
    empty (String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> (Int -> String) -> Int -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> String
    forall a. Show a => a -> String
    show) Maybe Int
    n
                Underscore Range
    _ Maybe String
    n   -> Doc -> (String -> Doc) -> Maybe String -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Underscore a => a
    underscore String -> Doc
    forall a. String -> Doc a
    text Maybe String
    n
                e :: Expr
    e@(App Range
    _ Expr
    _ NamedArg Expr
    _)    ->
                    case Expr -> AppView
    appView Expr
    e of
                        AppView Expr
    e1 [NamedArg Expr]
    args     ->
                            [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e1 Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (NamedArg Expr -> Doc) -> [NamedArg Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [NamedArg Expr]
    args
    --                      sep [ pretty e1
    --                          , nest 2 $ fsep $ map pretty args
    --                          ]
                RawApp Range
    _ List2 Expr
    es    -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty ([Expr] -> [Doc]) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ List2 Expr -> [Item (List2 Expr)]
    forall l. IsList l => l -> [Item l]
    List2.toList List2 Expr
    es
                OpApp Range
    _ QName
    q Set1 Name
    _ OpAppArgs
    es         -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Aspect -> QName -> OpAppArgs -> [Doc]
    forall a.
    Pretty a =>
    Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
    prettyOpApp (Maybe NameKind -> Bool -> Aspect
    Asp.Name Maybe NameKind
    forall a. Maybe a
    Nothing Bool
    True) QName
    q OpAppArgs
    es
                KnownOpApp NameKind
    nk Range
    _ QName
    q Set1 Name
    _ OpAppArgs
    es -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Aspect -> QName -> OpAppArgs -> [Doc]
    forall a.
    Pretty a =>
    Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
    prettyOpApp (Maybe NameKind -> Bool -> Aspect
    Asp.Name (NameKind -> Maybe NameKind
    forall a. a -> Maybe a
    Just NameKind
    nk) Bool
    True) QName
    q OpAppArgs
    es

                WithApp Range
    _ Expr
    e List1 Expr
    es -> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
                  Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> NonEmpty Doc -> NonEmpty Doc
    forall a. a -> NonEmpty a -> NonEmpty a
    <| (Expr -> Doc) -> List1 Expr -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc -> Doc
    hlSymbol Doc
    "|" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc -> Doc) -> (Expr -> Doc) -> Expr -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty) List1 Expr
    es

                HiddenArg Range
    _ Named_ Expr
    e -> Doc -> Doc
    braces' (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Named_ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Named_ Expr
    e
                InstanceArg Range
    _ Named_ Expr
    e -> Doc -> Doc
    dbraces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Named_ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Named_ Expr
    e
                Lam Range
    _ List1 LamBinding
    bs (AbsurdLam Range
    _ Hiding
    h) -> Doc
    lambda Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> List1 LamBinding -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 LamBinding
    bs) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Hiding -> Doc
    absurd Hiding
    h
                Lam Range
    _ List1 LamBinding
    bs Expr
    e ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    lambda Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> List1 LamBinding -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 LamBinding
    bs) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    arrow
                        , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                        ]
                AbsurdLam Range
    _ Hiding
    h -> Doc
    lambda Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Hiding -> Doc
    absurd Hiding
    h
                ExtendedLam Range
    _ Erased
    e List1 LamClause
    pes ->
                  Doc
    lambda Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>
                  Erased -> Doc -> Doc
    prettyErased Erased
    e (NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons ((LamClause -> Doc) -> List1 LamClause -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LamClause -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 LamClause
    pes))
                Fun Range
    _ Arg Expr
    e1 Expr
    e2 ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Modality -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Arg Expr -> Modality
    forall a. LensModality a => a -> Modality
    getModality Arg Expr
    e1) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Arg Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Arg Expr
    e1 Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    arrow
                        , Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e2
                        ]
                Pi Telescope1
    tel Expr
    e ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Tel -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Telescope -> Tel
    Tel (Telescope -> Tel) -> Telescope -> Tel
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Telescope
    smashTel (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Telescope1 -> [Item Telescope1]
    forall l. IsList l => l -> [Item l]
    List1.toList Telescope1
    tel) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    arrow
                        , Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                        ]
                Let Range
    _ List1 Declaration
    ds Maybe Expr
    me  ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc -> Doc
    hlKeyword Doc
    "let" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> List1 Declaration -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 Declaration
    ds)
                        , Doc -> (Expr -> Doc) -> Maybe Expr -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Null a => a
    empty (\ Expr
    e -> Doc -> Doc
    hlKeyword Doc
    "in" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e) Maybe Expr
    me
                        ]
                Paren Range
    _ Expr
    e -> Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                IdiomBrackets Range
    _ [Expr]
    es ->
                  case [Expr]
    es of
                    []   -> Doc
    emptyIdiomBrkt
                    [Expr
    e]  -> Doc
    leftIdiomBrkt Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    rightIdiomBrkt
                    Expr
    e:[Expr]
    es -> Doc
    leftIdiomBrkt Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Doc
    "|" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc -> Doc) -> (Expr -> Doc) -> Expr -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty) [Expr]
    es) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    rightIdiomBrkt
                DoBlock Range
    _ List1 DoStmt
    ss -> Doc -> Doc
    hlKeyword Doc
    "do" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((DoStmt -> Doc) -> List1 DoStmt -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DoStmt -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 DoStmt
    ss)
                As Range
    _ Name
    x Expr
    e  -> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    hlSymbol Doc
    "@" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                Dot KwRange
    _ Expr
    e   -> Doc -> Doc
    hlSymbol Doc
    "." Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                DoubleDot KwRange
    _ Expr
    e  -> Doc -> Doc
    hlSymbol Doc
    ".." Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                Absurd Range
    _  -> Doc -> Doc
    hlSymbol Doc
    "()"
                Rec KwRange
    _ Range
    _ RecordAssignments
    xs ->
                  [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [Doc -> Doc
    hlKeyword Doc
    "record", [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons ((Either FieldAssignment ModuleAssignment -> Doc)
    -> RecordAssignments -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Either FieldAssignment ModuleAssignment -> Doc
    forall a. Pretty a => a -> Doc
    pretty RecordAssignments
    xs)]
                RecUpdate KwRange
    _ Range
    _ Expr
    e [FieldAssignment]
    xs ->
                  [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [Doc -> Doc
    hlKeyword Doc
    "record" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e, [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons ((FieldAssignment -> Doc) -> [FieldAssignment] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FieldAssignment -> Doc
    forall a. Pretty a => a -> Doc
    pretty [FieldAssignment]
    xs)]
                Quote Range
    _ -> Doc -> Doc
    hlKeyword Doc
    "quote"
                QuoteTerm Range
    _ -> Doc -> Doc
    hlKeyword Doc
    "quoteTerm"
                Unquote Range
    _  -> Doc -> Doc
    hlKeyword Doc
    "unquote"
                Tactic Range
    _ Expr
    t -> Doc -> Doc
    hlKeyword Doc
    "tactic" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    t
                -- Andreas, 2011-10-03 print irrelevant things as .(e)
                DontCare Expr
    e -> Doc -> Doc
    hlSymbol Doc
    "." Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    parens (Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e)
                Equal Range
    _ Expr
    a Expr
    b -> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    a Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    equals Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    b
                Ellipsis Range
    _  -> Doc -> Doc
    hlSymbol Doc
    "..."
                Generalized Expr
    e -> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
            where
              absurd :: Hiding -> Doc
    absurd Hiding
    NotHidden  = Doc -> Doc
    parens Doc
    forall a. Monoid a => a
    mempty
              absurd Instance{} = Doc -> Doc
    dbraces Doc
    forall a. Monoid a => a
    mempty
              absurd Hiding
    Hidden     = Doc -> Doc
    braces Doc
    forall a. Monoid a => a
    mempty

    instance (Pretty a, Pretty b) => Pretty (Either a b) where
      pretty :: Either a b -> Doc
    pretty = (a -> Doc) -> (b -> Doc) -> Either a b -> Doc
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> Doc
    forall a. Pretty a => a -> Doc
    pretty b -> Doc
    forall a. Pretty a => a -> Doc
    pretty

    instance Pretty a => Pretty (FieldAssignment' a) where
      pretty :: FieldAssignment' a -> Doc
    pretty (FieldAssignment Name
    x a
    e) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=" , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e ]

    instance Pretty ModuleAssignment where
      pretty :: ModuleAssignment -> Doc
    pretty (ModuleAssignment QName
    m [Expr]
    es ImportDirective
    i) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    m Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Expr]
    es) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i

    instance Pretty LamClause where
      pretty :: LamClause -> Doc
    pretty (LamClause [Pattern]
    ps RHS
    rhs Catchall
    _) =
        [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Pattern -> Doc) -> [Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Pattern]
    ps)
            , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ RHS -> Doc
    forall {a}. Pretty a => RHS' a -> Doc
    pretty' RHS
    rhs
            ]
        where
          pretty' :: RHS' a -> Doc
    pretty' (RHS a
    e)   = Doc
    arrow Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e
          pretty' RHS' a
    AbsurdRHS = Doc
    forall a. Null a => a
    empty

    -- Andreas, 2024-02-25
    -- Q: Can we always ignore the tactic and the finiteness here?
    instance Pretty BoundName where
      pretty :: BoundName -> Doc
    pretty (BName Name
    x Fixity'
    _fix TacticAttribute
    _tac Bool
    _fin) = Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x

    data NamedBinding = NamedBinding
      { NamedBinding -> Bool
    withHiding   :: Bool
      , NamedBinding -> NamedArg Binder
    namedBinding :: NamedArg Binder
      }

    isLabeled :: NamedArg Binder -> Maybe ArgName
    isLabeled :: NamedArg Binder -> Maybe String
    isLabeled NamedArg Binder
    x
      | NamedArg Binder -> Bool
    forall a. LensHiding a => a -> Bool
    visible NamedArg Binder
    x              = Maybe String
    forall a. Maybe a
    Nothing  -- Ignore labels on visible arguments
      | Just String
    l <- NamedArg Binder -> Maybe String
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
    bareNameOf NamedArg Binder
    x = Bool -> String -> Maybe String
    forall a. Bool -> a -> Maybe a
    boolToMaybe (String
    l String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Name -> String
    nameToRawName (BoundName -> Name
    boundName (BoundName -> Name) -> BoundName -> Name
    forall a b. (a -> b) -> a -> b
    $ Binder -> BoundName
    forall a. Binder' a -> a
    binderName (Binder -> BoundName) -> Binder -> BoundName
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    x)) String
    l
      | Bool
    otherwise              = Maybe String
    forall a. Maybe a
    Nothing

    instance Pretty a => Pretty (Binder' a) where
      pretty :: Binder' a -> Doc
    pretty (Binder Maybe Pattern
    mpat BinderNameOrigin
    UserBinderName a
    n) =
        Maybe Pattern -> (Pattern -> Doc -> Doc) -> Doc -> Doc
    forall b a. Maybe b -> (b -> a -> a) -> a -> a
    applyWhenJust Maybe Pattern
    mpat (\ Pattern
    pat -> (Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> (Doc
    "@" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc -> Doc
    parens (Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    pat)))) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    n

      pretty (Binder Maybe Pattern
    pat BinderNameOrigin
    InsertedBinderName a
    n) = case Maybe Pattern
    pat of
        Just Pattern
    pat -> Doc -> Doc
    parens (Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    pat)
        Maybe Pattern
    Nothing  -> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    n

    instance Pretty NamedBinding where
      pretty :: NamedBinding -> Doc
    pretty (NamedBinding Bool
    withH
               x :: NamedArg Binder
    x@(Arg (ArgInfo Hiding
    h (Modality Relevance
    r Quantity
    q Cohesion
    c PolarityModality
    p) Origin
    _o FreeVariables
    _fv (Annotation Lock
    lock))
                   (Named Maybe NamedName
    _mn xb :: Binder
    xb@(Binder Maybe Pattern
    _mp BinderNameOrigin
    _ (BName Name
    _y Fixity'
    _fix TacticAttribute
    t Bool
    _fin))))) =
        Bool -> (Doc -> Doc) -> Doc -> Doc
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    withH Doc -> Doc
    prH (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
        Maybe String -> (String -> Doc -> Doc) -> Doc -> Doc
    forall b a. Maybe b -> (b -> a -> a) -> a -> a
    applyWhenJust (NamedArg Binder -> Maybe String
    isLabeled NamedArg Binder
    x) (\ String
    l -> (String -> Doc
    forall a. String -> Doc a
    text String
    l Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)) (Binder -> Doc
    forall a. Pretty a => a -> Doc
    pretty Binder
    xb)
          -- isLabeled looks at _mn and _y
          -- pretty xb prints also the pattern _mp
        where
        prH :: Doc -> Doc
    prH = Relevance -> Doc -> Doc
    forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance Relevance
    r
            (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Hiding -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding Hiding
    h Doc -> Doc
    mparens
            (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc
    coh Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)
            (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc
    qnt Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)
            (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc
    pol Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)
            (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc
    lck Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)
            (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Doc
    tac Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>)
        coh :: Doc
    coh = Cohesion -> Doc
    forall a. Pretty a => a -> Doc
    pretty Cohesion
    c
        qnt :: Doc
    qnt = Quantity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Quantity
    q
        pol :: Doc
    pol = PolarityModality -> Doc
    forall a. Pretty a => a -> Doc
    pretty PolarityModality
    p
        tac :: Doc
    tac = TacticAttribute -> Doc
    forall a. Pretty a => a -> Doc
    pretty TacticAttribute
    t
        lck :: Doc
    lck = Lock -> Doc
    forall a. Pretty a => a -> Doc
    pretty Lock
    lock
        -- Parentheses are needed when an attribute @... is printed
        mparens :: Doc -> Doc
    mparens = Bool -> (Doc -> Doc) -> Doc -> Doc
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Doc -> Bool
    forall a. Null a => a -> Bool
    null Doc
    coh Bool -> Bool -> Bool
    && Doc -> Bool
    forall a. Null a => a -> Bool
    null Doc
    qnt Bool -> Bool -> Bool
    && Doc -> Bool
    forall a. Null a => a -> Bool
    null Doc
    lck Bool -> Bool -> Bool
    && Doc -> Bool
    forall a. Null a => a -> Bool
    null Doc
    tac Bool -> Bool -> Bool
    && Doc -> Bool
    forall a. Null a => a -> Bool
    null Doc
    pol) Doc -> Doc
    parens

    instance Pretty LamBinding where
        pretty :: LamBinding -> Doc
    pretty (DomainFree NamedArg Binder
    x) = NamedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Bool -> NamedArg Binder -> NamedBinding
    NamedBinding Bool
    True NamedArg Binder
    x)
        pretty (DomainFull TypedBinding' Expr
    b) = TypedBinding' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty TypedBinding' Expr
    b

    instance Pretty TypedBinding where
        pretty :: TypedBinding' Expr -> Doc
    pretty (TLet Range
    _ List1 Declaration
    ds) = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "let" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> List1 Declaration -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 Declaration
    ds)
        pretty (TBind Range
    _ List1 (NamedArg Binder)
    xs (Underscore Range
    _ Maybe String
    Nothing)) =
          NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((NamedArg Binder -> Doc) -> List1 (NamedArg Binder) -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NamedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty (NamedBinding -> Doc)
    -> (NamedArg Binder -> NamedBinding) -> NamedArg Binder -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> NamedArg Binder -> NamedBinding
    NamedBinding Bool
    True) List1 (NamedArg Binder)
    xs)
        pretty (TBind Range
    _ List1 (NamedArg Binder)
    xs Expr
    e) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep
          [ NamedArg Binder -> Doc -> Doc
    forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance NamedArg Binder
    y
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding NamedArg Binder
    y Doc -> Doc
    parens
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ BoundName -> Doc -> Doc
    prettyFiniteness (Binder -> BoundName
    forall a. Binder' a -> a
    binderName (Binder -> BoundName) -> Binder -> BoundName
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    y)
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Doc -> Doc
    forall a. LensCohesion a => a -> Doc -> Doc
    prettyCohesion NamedArg Binder
    y
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Doc -> Doc
    forall a. LensQuantity a => a -> Doc -> Doc
    prettyQuantity NamedArg Binder
    y
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Doc -> Doc
    forall a. LensLock a => a -> Doc -> Doc
    prettyLock NamedArg Binder
    y
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Doc -> Doc
    forall a. LensModalPolarity a => a -> Doc -> Doc
    prettyPolarity NamedArg Binder
    y
            (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ BoundName -> Doc -> Doc
    prettyTactic (Binder -> BoundName
    forall a. Binder' a -> a
    binderName (Binder -> BoundName) -> Binder -> BoundName
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    y) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
            [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((NamedArg Binder -> Doc) -> [NamedArg Binder] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty (NamedBinding -> Doc)
    -> (NamedArg Binder -> NamedBinding) -> NamedArg Binder -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> NamedArg Binder -> NamedBinding
    NamedBinding Bool
    False) [NamedArg Binder]
    ys)
                , Doc
    ":" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e ]
          | ys :: [NamedArg Binder]
    ys@(NamedArg Binder
    y : [NamedArg Binder]
    _) <- [NamedArg Binder] -> [[NamedArg Binder]]
    groupBinds ([NamedArg Binder] -> [[NamedArg Binder]])
    -> [NamedArg Binder] -> [[NamedArg Binder]]
    forall a b. (a -> b) -> a -> b
    $ List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (NamedArg Binder)
    xs ]
          where
            groupBinds :: [NamedArg Binder] -> [[NamedArg Binder]]
    groupBinds [] = []
            groupBinds (NamedArg Binder
    x : [NamedArg Binder]
    xs)
              | Just{} <- NamedArg Binder -> Maybe String
    isLabeled NamedArg Binder
    x = [NamedArg Binder
    x] [NamedArg Binder] -> [[NamedArg Binder]] -> [[NamedArg Binder]]
    forall a. a -> [a] -> [a]
    : [NamedArg Binder] -> [[NamedArg Binder]]
    groupBinds [NamedArg Binder]
    xs
              | Bool
    otherwise   = (NamedArg Binder
    x NamedArg Binder -> [NamedArg Binder] -> [NamedArg Binder]
    forall a. a -> [a] -> [a]
    : [NamedArg Binder]
    ys) [NamedArg Binder] -> [[NamedArg Binder]] -> [[NamedArg Binder]]
    forall a. a -> [a] -> [a]
    : [NamedArg Binder] -> [[NamedArg Binder]]
    groupBinds [NamedArg Binder]
    zs
              where ([NamedArg Binder]
    ys, [NamedArg Binder]
    zs) = (NamedArg Binder -> Bool)
    -> [NamedArg Binder] -> ([NamedArg Binder], [NamedArg Binder])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (NamedArg Binder -> NamedArg Binder -> Bool
    forall {a}. LensArgInfo a => a -> NamedArg Binder -> Bool
    same NamedArg Binder
    x) [NamedArg Binder]
    xs
                    same :: a -> NamedArg Binder -> Bool
    same a
    x NamedArg Binder
    y = a -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo a
    x ArgInfo -> ArgInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == NamedArg Binder -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo NamedArg Binder
    y Bool -> Bool -> Bool
    && Maybe String -> Bool
    forall a. Maybe a -> Bool
    isNothing (NamedArg Binder -> Maybe String
    isLabeled NamedArg Binder
    y)

    newtype Tel = Tel Telescope

    instance Pretty Tel where
        pretty :: Tel -> Doc
    pretty (Tel Telescope
    tel)
          | (TypedBinding' Expr -> Bool) -> Telescope -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any TypedBinding' Expr -> Bool
    isMeta Telescope
    tel = Doc
    forallQ Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
          | Bool
    otherwise      = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
          where
            isMeta :: TypedBinding' Expr -> Bool
    isMeta (TBind Range
    _ List1 (NamedArg Binder)
    _ (Underscore Range
    _ Maybe String
    Nothing)) = Bool
    True
            isMeta TypedBinding' Expr
    _ = Bool
    False

    smashTel :: Telescope -> Telescope
    smashTel :: Telescope -> Telescope
    smashTel (TBind Range
    r List1 (NamedArg Binder)
    xs Expr
    e  :
              TBind Range
    _ List1 (NamedArg Binder)
    ys Expr
    e' : Telescope
    tel)
      | Expr -> String
    forall a. Pretty a => a -> String
    prettyShow Expr
    e String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == Expr -> String
    forall a. Pretty a => a -> String
    prettyShow Expr
    e' = Telescope -> Telescope
    smashTel (Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    r (List1 (NamedArg Binder)
    xs List1 (NamedArg Binder)
    -> List1 (NamedArg Binder) -> List1 (NamedArg Binder)
    forall a. Semigroup a => a -> a -> a
    Semigroup.<> List1 (NamedArg Binder)
    ys) Expr
    e TypedBinding' Expr -> Telescope -> Telescope
    forall a. a -> [a] -> [a]
    : Telescope
    tel)
    smashTel (TypedBinding' Expr
    b : Telescope
    tel) = TypedBinding' Expr
    b TypedBinding' Expr -> Telescope -> Telescope
    forall a. a -> [a] -> [a]
    : Telescope -> Telescope
    smashTel Telescope
    tel
    smashTel [] = []

    instance Pretty RHS where
        pretty :: RHS -> Doc
    pretty (RHS Expr
    e)   = Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
        pretty RHS
    AbsurdRHS = Doc
    forall a. Null a => a
    empty

    instance Pretty WhereClause where
      pretty :: WhereClause -> Doc
    pretty  WhereClause
    NoWhere = Doc
    forall a. Null a => a
    empty
      pretty (AnyWhere Range
    _ [Module Range
    _ NotErased{} QName
    x [] [Declaration]
    ds])
        | Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName (QName -> Name
    unqualify QName
    x)
                           = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ Doc
    "where", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    ds) ]
      pretty (AnyWhere Range
    _ [Declaration]
    ds) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ Doc
    "where", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    ds) ]
      pretty (SomeWhere Range
    _ Erased
    erased Name
    m Access
    a [Declaration]
    ds) =
        [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Access -> [Doc] -> [Doc]
    privateWhenUserWritten Access
    a
                 [ Doc
    "module", Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    m), Doc
    "where" ]
             , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    ds)
             ]
        where
          privateWhenUserWritten :: Access -> [Doc] -> [Doc]
    privateWhenUserWritten = \case
            PrivateAccess KwRange
    _ Origin
    UserWritten -> (Doc
    "private" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    :)
            Access
    _ -> [Doc] -> [Doc]
    forall a. a -> a
    id

    instance Pretty LHS where
      pretty :: LHS -> Doc
    pretty (LHS Pattern
    p [RewriteEqn]
    eqs [WithExpr]
    es) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
        [ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p
        , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ if [RewriteEqn] -> Bool
    forall a. Null a => a -> Bool
    null [RewriteEqn]
    eqs then Doc
    forall a. Null a => a
    empty else [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (RewriteEqn -> Doc) -> [RewriteEqn] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map RewriteEqn -> Doc
    forall a. Pretty a => a -> Doc
    pretty [RewriteEqn]
    eqs
        , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> Doc
    prefixedThings Doc
    "with" ((WithExpr -> Doc) -> [WithExpr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map WithExpr -> Doc
    prettyWithd [WithExpr]
    es)
        ] where

        prettyWithd :: WithExpr -> Doc
        prettyWithd :: WithExpr -> Doc
    prettyWithd (Named Maybe Name
    nm Arg Expr
    wh) =
          let e :: Doc
    e = Arg Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Arg Expr
    wh in
          case Maybe Name
    nm of
            Maybe Name
    Nothing -> Doc
    e
            Just Name
    n  -> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    ":" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    e

    instance Pretty LHSCore where
      pretty :: LHSCore -> Doc
    pretty (LHSHead QName
    f [NamedArg Pattern]
    ps) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    f Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc
    parens (Doc -> Doc)
    -> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty) [NamedArg Pattern]
    ps
      pretty (LHSProj QName
    d [NamedArg Pattern]
    ps NamedArg LHSCore
    lhscore [NamedArg Pattern]
    ps') = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
        QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    d Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc
    parens (Doc -> Doc)
    -> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty) [NamedArg Pattern]
    ps [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
        Doc -> Doc
    parens (NamedArg LHSCore -> Doc
    forall a. Pretty a => a -> Doc
    pretty NamedArg LHSCore
    lhscore) Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc
    parens (Doc -> Doc)
    -> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty) [NamedArg Pattern]
    ps'
      pretty (LHSWith LHSCore
    h List1 Pattern
    wps [NamedArg Pattern]
    ps) = if [NamedArg Pattern] -> Bool
    forall a. Null a => a -> Bool
    null [NamedArg Pattern]
    ps then Doc
    doc else
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc
    parens Doc
    doc Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> Doc
    parens (Doc -> Doc)
    -> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty) [NamedArg Pattern]
    ps
        where
        doc :: Doc
    doc = NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ LHSCore -> Doc
    forall a. Pretty a => a -> Doc
    pretty LHSCore
    h Doc -> NonEmpty Doc -> NonEmpty Doc
    forall a b. a -> NonEmpty b -> NonEmpty a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ (Pattern -> Doc) -> List1 Pattern -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc
    "|" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc -> Doc) -> (Pattern -> Doc) -> Pattern -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty) List1 Pattern
    wps
      pretty (LHSEllipsis Range
    r LHSCore
    p) = Doc
    "..."

    instance Pretty ModuleApplication where
      pretty :: ModuleApplication -> Doc
    pretty (SectionApp Range
    _ Telescope
    bs QName
    x [Expr]
    es) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
        [ (TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    bs
        , [ Doc
    "=", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x ]
        , (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Expr]
    es
        ]
      pretty (RecordModuleInstance Range
    _ QName
    x) = Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "{{...}}"

    instance Pretty DoStmt where
      pretty :: DoStmt -> Doc
    pretty (DoBind Range
    _ Pattern
    p Expr
    e [LamClause]
    cs) =
        ((Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "←") Doc -> Doc -> Doc
    <?> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e) Doc -> Doc -> Doc
    <?> [LamClause] -> Doc
    forall {a}. Pretty a => [a] -> Doc
    prCs [LamClause]
    cs
        where
          prCs :: [a] -> Doc
    prCs [] = Doc
    forall a. Null a => a
    empty
          prCs [a]
    cs = Doc
    "where" Doc -> Doc -> Doc
    <?> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. Pretty a => a -> Doc
    pretty [a]
    cs)
      pretty (DoThen Expr
    e) = Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
      pretty (DoLet Range
    _ List1 Declaration
    ds) = Doc
    "let" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> List1 Declaration -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 Declaration
    ds)

    instance Pretty Declaration where
      prettyList :: [Declaration] -> Doc
    prettyList = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> ([Declaration] -> [Doc]) -> [Declaration] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty
      pretty :: Declaration -> Doc
    pretty = \case
        TypeSig ArgInfo
    i TacticAttribute
    tac Name
    x Expr
    e ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ TacticAttribute -> Doc -> Doc
    prettyTactic' TacticAttribute
    tac (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Doc -> Doc
    forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance ArgInfo
    i (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Doc -> Doc
    forall a. LensCohesion a => a -> Doc -> Doc
    prettyCohesion ArgInfo
    i (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Doc -> Doc
    forall a. LensQuantity a => a -> Doc -> Doc
    prettyQuantity ArgInfo
    i (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Doc -> Doc
    forall a. LensModalPolarity a => a -> Doc -> Doc
    prettyPolarity ArgInfo
    i (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    ":"
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
              ]
        FieldSig IsInstance
    inst TacticAttribute
    tac Name
    x (Arg ArgInfo
    i Expr
    e) ->
          IsInstance -> Doc -> Doc
    mkInst IsInstance
    inst (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Doc -> Doc
    forall {a} {a}. LensHiding a => a -> Doc a -> Doc a
    mkOverlap ArgInfo
    i (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
          -- We print relevance before hiding, need to clear it before printing the rest of the attributes with TypeSig.
          ArgInfo -> Doc -> Doc
    forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance ArgInfo
    i (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding ArgInfo
    i Doc -> Doc
    forall a. a -> a
    id (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
          Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Declaration -> Doc) -> Declaration -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig (Relevance -> ArgInfo -> ArgInfo
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    relevant ArgInfo
    i) TacticAttribute
    tac Name
    x Expr
    e
          where
            mkInst :: IsInstance -> Doc -> Doc
    mkInst (InstanceDef KwRange
    _) Doc
    d = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "instance", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 Doc
    d ]
            mkInst IsInstance
    NotInstanceDef  Doc
    d = Doc
    d

            mkOverlap :: a -> Doc a -> Doc a
    mkOverlap a
    i Doc a
    d | a -> Bool
    forall a. LensHiding a => a -> Bool
    isYesOverlap a
    i = Doc a
    "overlap" Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc a
    d
                          | Bool
    otherwise      = Doc a
    d
        Field KwRange
    _ [Declaration]
    fs ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "field"
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    fs)
              ]
        FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    _ ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ LHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty LHS
    lhs
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ RHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty RHS
    rhs
              ] Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    $$ Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (WhereClause -> Doc
    forall a. Pretty a => a -> Doc
    pretty WhereClause
    wh)
        DataSig Range
    _ Erased
    erased Name
    x [LamBinding]
    tel Expr
    e ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep  [ Doc
    "data"
                      , Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x)
                      , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty [LamBinding]
    tel)
                      ]
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
                      [ Doc
    ":"
                      , Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                      ]
              ]
        Data Range
    _ Erased
    erased Name
    x [LamBinding]
    tel Expr
    e [Declaration]
    cs ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep  [ Doc
    "data"
                      , Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x)
                      , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty [LamBinding]
    tel)
                      ]
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
                      [ Doc
    ":"
                      , Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                      , Doc
    "where"
                      ]
              ] Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    $$ Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    cs)
        DataDef Range
    _ Name
    x [LamBinding]
    tel [Declaration]
    cs ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep  [ Doc
    "data"
                      , Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
                      , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty [LamBinding]
    tel)
                      ]
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "where"
              ] Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    $$ Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    cs)
        RecordSig Range
    _ Erased
    erased Name
    x [LamBinding]
    tel Expr
    e ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep  [ Doc
    "record"
                      , Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x)
                      , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty [LamBinding]
    tel)
                      ]
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
                      [ Doc
    ":"
                      , Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                      ]
              ]
        Record Range
    _ Erased
    erased Name
    x [RecordDirective]
    dir [LamBinding]
    tel Expr
    e [Declaration]
    cs ->
          Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Maybe Expr
    -> [Declaration]
    -> Doc
    pRecord Erased
    erased Name
    x [RecordDirective]
    dir [LamBinding]
    tel (Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    e) [Declaration]
    cs
        RecordDef Range
    _ Name
    x [RecordDirective]
    dir [LamBinding]
    tel [Declaration]
    cs ->
          Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Maybe Expr
    -> [Declaration]
    -> Doc
    pRecord Erased
    defaultErased Name
    x [RecordDirective]
    dir [LamBinding]
    tel Maybe Expr
    forall a. Maybe a
    Nothing [Declaration]
    cs
        Infix Fixity
    f List1 Name
    xs  ->
          Fixity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Fixity
    f Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (Doc -> NonEmpty Doc -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma (NonEmpty Doc -> [Doc]) -> NonEmpty Doc -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc) -> List1 Name -> NonEmpty Doc
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty List1 Name
    xs)
        Syntax Name
    n Notation
    xs -> Doc
    "syntax" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "..."
        PatternSyn Range
    _ Name
    n [WithHiding Name]
    as Pattern
    p -> Doc
    "pattern" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((WithHiding Name -> Doc) -> [WithHiding Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map WithHiding Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [WithHiding Name]
    as)
                                 Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p
        Mutual KwRange
    _ [Declaration]
    ds     -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "mutual" [Declaration]
    ds
        InterleavedMutual KwRange
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "interleaved mutual" [Declaration]
    ds
        LoneConstructor KwRange
    _ [Declaration]
    ds -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "data _ where" [Declaration]
    ds
        Abstract KwRange
    _ [Declaration]
    ds   -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "abstract" [Declaration]
    ds
        Private KwRange
    _ Origin
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "private" [Declaration]
    ds
        InstanceB KwRange
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "instance" [Declaration]
    ds
        Macro KwRange
    _ [Declaration]
    ds      -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "macro" [Declaration]
    ds
        Postulate KwRange
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "postulate" [Declaration]
    ds
        Primitive KwRange
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "primitive" [Declaration]
    ds
        Generalize KwRange
    _ [Declaration]
    ds -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "variable" [Declaration]
    ds
        Opaque KwRange
    _ [Declaration]
    ds     -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "opaque" [Declaration]
    ds
        Unfolding KwRange
    _ [QName]
    rs  -> Doc
    "unfolding" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc -> Doc
    braces ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    semi (QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (QName -> Doc) -> [QName] -> [Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [QName]
    rs)))
        Module Range
    _ Erased
    erased QName
    x Telescope
    tel [Declaration]
    ds ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "module"
               , Erased -> Doc -> Doc
    prettyErased Erased
    erased (QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x)
               , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
               , Doc
    "where"
               ] Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    $$ Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    ds)
        ModuleMacro Range
    _ NotErased{} Name
    x (SectionApp Range
    _ [] QName
    y [Expr]
    es) OpenShortHand
    DoOpen ImportDirective
    i
          | Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ OpenShortHand -> Doc
    forall a. Pretty a => a -> Doc
    pretty OpenShortHand
    DoOpen
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    y Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Expr]
    es
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    4 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i
              ]
        ModuleMacro Range
    _ Erased
    erased Name
    x (SectionApp Range
    _ Telescope
    tel QName
    y [Expr]
    es) OpenShortHand
    open ImportDirective
    i ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ OpenShortHand -> Doc
    forall a. Pretty a => a -> Doc
    pretty OpenShortHand
    open Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "module" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+>
                Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [ Doc
    "=", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    y ], (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Expr]
    es, [ ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i ] ]
              ]
        ModuleMacro Range
    _ Erased
    erased Name
    x (RecordModuleInstance Range
    _ QName
    rec) OpenShortHand
    open ImportDirective
    i ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ OpenShortHand -> Doc
    forall a. Pretty a => a -> Doc
    pretty OpenShortHand
    open Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "module" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x)
              , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    rec Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "{{...}}"
              ]
        Open Range
    _ QName
    x ImportDirective
    i  -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "open", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x, ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i ]
        Import Range
    _ QName
    x Maybe AsName
    rn OpenShortHand
    open ImportDirective
    i   ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ OpenShortHand -> Doc
    forall a. Pretty a => a -> Doc
    pretty OpenShortHand
    open, Doc
    "import", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x, Maybe AsName -> Doc
    forall {a}. Pretty a => Maybe (AsName' a) -> Doc
    as Maybe AsName
    rn, ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i ]
          where
            as :: Maybe (AsName' a) -> Doc
    as Maybe (AsName' a)
    Nothing  = Doc
    forall a. Null a => a
    empty
            as (Just AsName' a
    x) = Doc
    "as" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty (AsName' a -> a
    forall a. AsName' a -> a
    asName AsName' a
    x)
        UnquoteDecl Range
    _ [Name]
    xs Expr
    t ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "unquoteDecl" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    t ]
        UnquoteDef Range
    _ [Name]
    xs Expr
    t ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "unquoteDef" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    t ]
        UnquoteData Range
    _ Name
    x [Name]
    xs Expr
    t ->
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "unquoteData" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    xs) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    t ]
        Pragma Pragma
    pr   -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "{-#" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Pragma -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pragma
    pr, Doc
    "#-}" ]
        where
          namedBlock :: String -> [a] -> Doc
    namedBlock String
    s [a]
    ds =
              [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ String -> Doc
    forall a. String -> Doc a
    text String
    s
                  , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. Pretty a => a -> Doc
    pretty [a]
    ds
                  ]

    pHasEta0 :: HasEta0 -> Doc
    pHasEta0 :: HasEta0 -> Doc
    pHasEta0 = \case
      HasEta0
    YesEta   -> Doc
    "eta-equality"
      NoEta () -> Doc
    "no-eta-equality"

    instance Pretty RecordDirective where
      pretty :: RecordDirective -> Doc
    pretty = RecordDirective -> Doc
    pRecordDirective

    pRecordDirective :: RecordDirective -> Doc
    pRecordDirective :: RecordDirective -> Doc
    pRecordDirective = \case
      Induction Ranged Induction
    ind -> Induction -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Ranged Induction -> Induction
    forall a. Ranged a -> a
    rangedThing Ranged Induction
    ind)
      Constructor Name
    n IsInstance
    inst -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    pInst, Doc
    "constructor", Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n ] where
        pInst :: Doc
    pInst = case IsInstance
    inst of
          InstanceDef{} -> Doc
    "instance"
          NotInstanceDef{} -> Doc
    forall a. Null a => a
    empty
      Eta Ranged HasEta0
    eta -> HasEta0 -> Doc
    pHasEta0 (Ranged HasEta0 -> HasEta0
    forall a. Ranged a -> a
    rangedThing Ranged HasEta0
    eta)
      PatternOrCopattern{} -> Doc
    "pattern"

    pRecord
      :: Erased
      -> Name
      -> [RecordDirective]
      -> [LamBinding]
      -> Maybe Expr
      -> [Declaration]
      -> Doc
    pRecord :: Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Maybe Expr
    -> [Declaration]
    -> Doc
    pRecord Erased
    erased Name
    x [RecordDirective]
    directives [LamBinding]
    tel Maybe Expr
    me [Declaration]
    ds = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
        [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep
          [ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep  [ Doc
    "record"
                  , Erased -> Doc -> Doc
    prettyErased Erased
    erased (Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x)
                  , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map LamBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty [LamBinding]
    tel)
                  ]
          , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Maybe Expr -> Doc
    forall {a}. Pretty a => Maybe a -> Doc
    pType Maybe Expr
    me
          ]
        , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
          [ (RecordDirective -> Doc) -> [RecordDirective] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map RecordDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty [RecordDirective]
    directives
          , (Declaration -> Doc) -> [Declaration] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Declaration]
    ds
          ]
        ]
      where pType :: Maybe a -> Doc
    pType (Just a
    e) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
                    [ Doc
    ":"
                    , a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e
                    , Doc
    "where"
                    ]
            pType Maybe a
    Nothing  =
                      Doc
    "where"

    instance Pretty OpenShortHand where
        pretty :: OpenShortHand -> Doc
    pretty OpenShortHand
    DoOpen = Doc
    "open"
        pretty OpenShortHand
    DontOpen = Doc
    forall a. Null a => a
    empty

    instance Pretty Pragma where
        pretty :: Pragma -> Doc
    pretty (OptionsPragma Range
    _ [String]
    opts)  = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc
    forall a. String -> Doc a
    text ([String] -> [Doc]) -> [String] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ String
    "OPTIONS" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    opts
        pretty (BuiltinPragma Range
    _ Ranged String
    b QName
    x)   = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "BUILTIN", String -> Doc
    forall a. String -> Doc a
    text (Ranged String -> String
    forall a. Ranged a -> a
    rangedThing Ranged String
    b), QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x ]
        pretty (RewritePragma Range
    _ Range
    _ [QName]
    xs)    =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "REWRITE", [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (QName -> Doc) -> [QName] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty [QName]
    xs ]
        pretty (CompilePragma Range
    _ Ranged BackendName
    b QName
    x String
    e) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "COMPILE", BackendName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Ranged BackendName -> BackendName
    forall a. Ranged a -> a
    rangedThing Ranged BackendName
    b), QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x, String -> Doc
    textNonEmpty String
    e ]
        pretty (ForeignPragma Range
    _ Ranged BackendName
    b String
    s) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "FOREIGN", BackendName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Ranged BackendName -> BackendName
    forall a. Ranged a -> a
    rangedThing Ranged BackendName
    b) ] Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc
    forall a. String -> Doc a
    text (String -> [String]
    lines String
    s)
        pretty (StaticPragma Range
    _ QName
    i) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "STATIC", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    i]
        pretty (InjectivePragma Range
    _ QName
    i) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "INJECTIVE", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    i]
        pretty (InjectiveForInferencePragma Range
    _ QName
    i) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "INJECTIVE_FOR_INFERENCE", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    i]
        pretty (InlinePragma Range
    _ Bool
    True QName
    i) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "INLINE", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    i]
        pretty (NotProjectionLikePragma Range
    _ QName
    i) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "NOT_PROJECTION_LIKE", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    i]
        pretty (InlinePragma Range
    _ Bool
    False QName
    i) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "NOINLINE", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    i]
        pretty (ImpossiblePragma Range
    _ [String]
    strs) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "IMPOSSIBLE"] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc
    forall a. String -> Doc a
    text [String]
    strs
        pretty (EtaPragma Range
    _ QName
    x) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "ETA", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x]
        pretty (TerminationCheckPragma Range
    _ TerminationCheck Name
    tc) =
          case TerminationCheck Name
    tc of
            TerminationCheck Name
    TerminationCheck       -> Doc
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            TerminationCheck Name
    NoTerminationCheck     -> Doc
    "NO_TERMINATION_CHECK"
            TerminationCheck Name
    NonTerminating         -> Doc
    "NON_TERMINATING"
            TerminationCheck Name
    Terminating            -> Doc
    "TERMINATING"
            TerminationMeasure Range
    _ Name
    x -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc
    "MEASURE", Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x]
        pretty (NoCoverageCheckPragma Range
    _) = Doc
    "NON_COVERING"
        pretty (WarningOnUsage Range
    _ QName
    nm BackendName
    str) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "WARNING_ON_USAGE", QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    nm, String -> Doc
    forall a. String -> Doc a
    text (BackendName -> String
    forall a. Show a => a -> String
    show BackendName
    str) ]
        pretty (WarningOnImport Range
    _ BackendName
    str)   = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "WARNING_ON_IMPORT", String -> Doc
    forall a. String -> Doc a
    text (BackendName -> String
    forall a. Show a => a -> String
    show BackendName
    str) ]
        pretty (CatchallPragma Range
    _) = Doc
    "CATCHALL"
        pretty (DisplayPragma Range
    _ Pattern
    lhs Expr
    rhs) = Doc
    "DISPLAY" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    lhs Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "=", Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    rhs ]
        pretty (NoPositivityCheckPragma Range
    _) = Doc
    "NO_POSITIVITY_CHECK"
        pretty (PolarityPragma Range
    _ Name
    q [Ranged Occurrence]
    occs) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep (Doc
    "POLARITY" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    q Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Ranged Occurrence -> Doc) -> [Ranged Occurrence] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Ranged Occurrence -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Ranged Occurrence]
    occs)
        pretty (NoUniverseCheckPragma Range
    _) = Doc
    "NO_UNIVERSE_CHECK"
        pretty (OverlapPragma Range
    _ [QName]
    x OverlapMode
    m) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [OverlapMode -> Doc
    forall a. Pretty a => a -> Doc
    pretty OverlapMode
    m, [QName] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [QName]
    x]

    instance Pretty NotationPart where
        pretty :: NotationPart -> Doc
    pretty (IdPart Ranged String
    x) = String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Ranged String -> String
    forall a. Ranged a -> a
    rangedThing Ranged String
    x
        pretty HolePart{} = Doc
    forall a. Underscore a => a
    underscore
        pretty VarPart{}  = Doc
    forall a. Underscore a => a
    underscore
        pretty WildPart{} = Doc
    forall a. Underscore a => a
    underscore

        prettyList :: Notation -> Doc
    prettyList = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat ([Doc] -> Doc) -> (Notation -> [Doc]) -> Notation -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NotationPart -> Doc) -> Notation -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NotationPart -> Doc
    forall a. Pretty a => a -> Doc
    pretty

    instance Pretty Fixity' where
        pretty :: Fixity' -> Doc
    pretty (Fixity' Fixity
    fix Notation
    nota Range
    _range)
          | Notation -> Bool
    forall a. Null a => a -> Bool
    null Notation
    nota = Fixity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Fixity
    fix
          | Bool
    otherwise = Doc
    "syntax" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Notation -> Doc
    forall a. Pretty a => a -> Doc
    pretty Notation
    nota

    instance Pretty Pattern where
        prettyList :: [Pattern] -> Doc
    prettyList = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> ([Pattern] -> [Doc]) -> [Pattern] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> Doc) -> [Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty
        pretty :: Pattern -> Doc
    pretty = \case
                IdentP Bool
    _ QName
    x      -> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
                AppP Pattern
    p1 NamedArg Pattern
    p2      -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p1, Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty NamedArg Pattern
    p2 ]
                RawAppP Range
    _ List2 Pattern
    ps    -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Doc) -> [Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty ([Pattern] -> [Doc]) -> [Pattern] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ List2 Pattern -> [Item (List2 Pattern)]
    forall l. IsList l => l -> [Item l]
    List2.toList List2 Pattern
    ps
                OpAppP Range
    _ QName
    q Set1 Name
    _ List1 (NamedArg Pattern)
    ps -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Aspect
    -> QName -> List1 (NamedArg (MaybePlaceholder Pattern)) -> [Doc]
    forall a.
    Pretty a =>
    Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
    prettyOpApp (Maybe NameKind -> Bool -> Aspect
    Asp.Name Maybe NameKind
    forall a. Maybe a
    Nothing Bool
    True) QName
    q (List1 (NamedArg (MaybePlaceholder Pattern)) -> [Doc])
    -> List1 (NamedArg (MaybePlaceholder Pattern)) -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg (MaybePlaceholder Pattern))
    -> List1 (NamedArg Pattern)
    -> List1 (NamedArg (MaybePlaceholder Pattern))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named_ Pattern -> Named_ (MaybePlaceholder Pattern))
    -> NamedArg Pattern -> NamedArg (MaybePlaceholder Pattern)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Pattern -> MaybePlaceholder Pattern)
    -> Named_ Pattern -> Named_ (MaybePlaceholder Pattern)
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Maybe PositionInName -> Pattern -> MaybePlaceholder Pattern
    forall e. Maybe PositionInName -> e -> MaybePlaceholder e
    NoPlaceholder Maybe PositionInName
    forall a. Maybe a
    Strict.Nothing))) List1 (NamedArg Pattern)
    ps
                HiddenP Range
    _ Named_ Pattern
    p     -> Doc -> Doc
    braces' (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Named_ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Named_ Pattern
    p
                InstanceP Range
    _ Named_ Pattern
    p   -> Doc -> Doc
    dbraces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Named_ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Named_ Pattern
    p
                ParenP Range
    _ Pattern
    p      -> Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p
                WildP Range
    _         -> Doc
    forall a. Underscore a => a
    underscore
                AsP Range
    _ Name
    x Pattern
    p       -> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "@" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p
                DotP KwRange
    _ Range
    _ Expr
    p      -> Doc
    "." Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    p
                AbsurdP Range
    _       -> Doc
    "()"
                LitP Range
    _ Literal
    l        -> Literal -> Doc
    forall a. Pretty a => a -> Doc
    pretty Literal
    l
                QuoteP Range
    _        -> Doc
    "quote"
                RecP KwRange
    _ Range
    _ [FieldAssignment' Pattern]
    fs     -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "record", [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons ((FieldAssignment' Pattern -> Doc)
    -> [FieldAssignment' Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map FieldAssignment' Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty [FieldAssignment' Pattern]
    fs) ]
                EqualP Range
    _ List1 (Expr, Expr)
    es     -> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ List1 (Expr, Expr) -> ((Expr, Expr) -> Doc) -> NonEmpty Doc
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for List1 (Expr, Expr)
    es \ (Expr
    e1, Expr
    e2) -> Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e1, Doc
    "=", Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e2]
                EllipsisP Range
    _ Maybe Pattern
    mp  -> Doc
    "..."
                WithP Range
    _ Pattern
    p       -> Doc
    "|" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p

    prettyOpApp :: forall a .
      Pretty a => Asp.Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
    prettyOpApp :: forall a.
    Pretty a =>
    Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
    prettyOpApp Aspect
    asp QName
    q List1 (NamedArg (MaybePlaceholder a))
    es = [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge [] ([(Doc, Maybe PositionInName)] -> [Doc])
    -> [(Doc, Maybe PositionInName)] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ [Name]
    -> [NamePart]
    -> [NamedArg (MaybePlaceholder a)]
    -> [(Doc, Maybe PositionInName)]
    prOp [Name]
    ms [Item NameParts]
    [NamePart]
    xs ([NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)])
    -> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
    forall a b. (a -> b) -> a -> b
    $ List1 (NamedArg (MaybePlaceholder a))
    -> [Item (List1 (NamedArg (MaybePlaceholder a)))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (NamedArg (MaybePlaceholder a))
    es
      where
        -- ms: the module part of the name.
        ms :: [Name]
    ms = List1 Name -> [Name]
    forall a. NonEmpty a -> [a]
    List1.init (QName -> List1 Name
    qnameParts QName
    q)
        -- xs: the concrete name (alternation of @Id@ and @Hole@)
        xs :: [Item NameParts]
    xs = case QName -> Name
    unqualify QName
    q of
               Name Range
    _ NameInScope
    _ NameParts
    xs    -> NameParts -> [Item NameParts]
    forall l. IsList l => l -> [Item l]
    List1.toList NameParts
    xs
               NoName{}       -> [Item NameParts]
    [NamePart]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        prOp :: [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
        prOp :: [Name]
    -> [NamePart]
    -> [NamedArg (MaybePlaceholder a)]
    -> [(Doc, Maybe PositionInName)]
    prOp [Name]
    ms (NamePart
    Hole : [NamePart]
    xs) (NamedArg (MaybePlaceholder a)
    e : [NamedArg (MaybePlaceholder a)]
    es) =
          case NamedArg (MaybePlaceholder a) -> MaybePlaceholder a
    forall a. NamedArg a -> a
    namedArg NamedArg (MaybePlaceholder a)
    e of
            Placeholder PositionInName
    p   -> ([Name] -> Doc -> Doc
    forall {a}. Pretty a => [a] -> Doc -> Doc
    qual [Name]
    ms (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ NamedArg (MaybePlaceholder a) -> Doc
    forall a. Pretty a => a -> Doc
    pretty NamedArg (MaybePlaceholder a)
    e, PositionInName -> Maybe PositionInName
    forall a. a -> Maybe a
    Just PositionInName
    p) (Doc, Maybe PositionInName)
    -> [(Doc, Maybe PositionInName)] -> [(Doc, Maybe PositionInName)]
    forall a. a -> [a] -> [a]
    : [Name]
    -> [NamePart]
    -> [NamedArg (MaybePlaceholder a)]
    -> [(Doc, Maybe PositionInName)]
    prOp [] [NamePart]
    xs [NamedArg (MaybePlaceholder a)]
    es
            NoPlaceholder{} -> (NamedArg (MaybePlaceholder a) -> Doc
    forall a. Pretty a => a -> Doc
    pretty NamedArg (MaybePlaceholder a)
    e, Maybe PositionInName
    forall a. Maybe a
    Nothing) (Doc, Maybe PositionInName)
    -> [(Doc, Maybe PositionInName)] -> [(Doc, Maybe PositionInName)]
    forall a. a -> [a] -> [a]
    : [Name]
    -> [NamePart]
    -> [NamedArg (MaybePlaceholder a)]
    -> [(Doc, Maybe PositionInName)]
    prOp [Name]
    ms [NamePart]
    xs [NamedArg (MaybePlaceholder a)]
    es
              -- Module qualifier needs to go on section holes (#3072)
        prOp [Name]
    _  (NamePart
    Hole : [NamePart]
    _)  []       = [(Doc, Maybe PositionInName)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        prOp [Name]
    ms (Id String
    x : [NamePart]
    xs) [NamedArg (MaybePlaceholder a)]
    es       = ( [Name] -> Doc -> Doc
    forall {a}. Pretty a => [a] -> Doc -> Doc
    qual [Name]
    ms (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Aspect -> Doc -> Doc
    annotateAspect Aspect
    asp (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Name -> Doc) -> Name -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Name
    simpleName String
    x
                                       , Maybe PositionInName
    forall a. Maybe a
    Nothing
                                       ) (Doc, Maybe PositionInName)
    -> [(Doc, Maybe PositionInName)] -> [(Doc, Maybe PositionInName)]
    forall a. a -> [a] -> [a]
    : [Name]
    -> [NamePart]
    -> [NamedArg (MaybePlaceholder a)]
    -> [(Doc, Maybe PositionInName)]
    prOp [] [NamePart]
    xs [NamedArg (MaybePlaceholder a)]
    es
          -- Qualify the name part with the module.
          -- We then clear @ms@ such that the following name parts will not be qualified.

        prOp [Name]
    _  []       [NamedArg (MaybePlaceholder a)]
    es          = (NamedArg (MaybePlaceholder a) -> (Doc, Maybe PositionInName))
    -> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\NamedArg (MaybePlaceholder a)
    e -> (NamedArg (MaybePlaceholder a) -> Doc
    forall a. Pretty a => a -> Doc
    pretty NamedArg (MaybePlaceholder a)
    e, Maybe PositionInName
    forall a. Maybe a
    Nothing)) [NamedArg (MaybePlaceholder a)]
    es

        qual :: [a] -> Doc -> Doc
    qual [a]
    ms Doc
    doc = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    "." ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. Pretty a => a -> Doc
    pretty [a]
    ms [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc
    doc]

        -- Section underscores should be printed without surrounding
        -- whitespace. This function takes care of that.
        merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
        merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge [Doc]
    before []                            = [Doc] -> [Doc]
    forall a. [a] -> [a]
    reverse [Doc]
    before
        merge [Doc]
    before ((Doc
    d, Maybe PositionInName
    Nothing) : [(Doc, Maybe PositionInName)]
    after)        = [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge (Doc
    d Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : [Doc]
    before) [(Doc, Maybe PositionInName)]
    after
        merge [Doc]
    before ((Doc
    d, Just PositionInName
    Beginning) : [(Doc, Maybe PositionInName)]
    after) = [Doc] -> Doc -> [(Doc, Maybe PositionInName)] -> [Doc]
    mergeRight [Doc]
    before Doc
    d [(Doc, Maybe PositionInName)]
    after
        merge [Doc]
    before ((Doc
    d, Just PositionInName
    End)       : [(Doc, Maybe PositionInName)]
    after) = case Doc -> [Doc] -> (Doc, [Doc])
    forall {a}. Semigroup a => a -> [a] -> (a, [a])
    mergeLeft Doc
    d [Doc]
    before of
                                                       (Doc
    d, [Doc]
    bs) -> [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge (Doc
    d Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : [Doc]
    bs) [(Doc, Maybe PositionInName)]
    after
        merge [Doc]
    before ((Doc
    d, Just PositionInName
    Middle)    : [(Doc, Maybe PositionInName)]
    after) = case Doc -> [Doc] -> (Doc, [Doc])
    forall {a}. Semigroup a => a -> [a] -> (a, [a])
    mergeLeft Doc
    d [Doc]
    before of
                                                       (Doc
    d, [Doc]
    bs) -> [Doc] -> Doc -> [(Doc, Maybe PositionInName)] -> [Doc]
    mergeRight [Doc]
    bs Doc
    d [(Doc, Maybe PositionInName)]
    after

        mergeRight :: [Doc] -> Doc -> [(Doc, Maybe PositionInName)] -> [Doc]
    mergeRight [Doc]
    before Doc
    d [(Doc, Maybe PositionInName)]
    after =
          [Doc] -> [Doc]
    forall a. [a] -> [a]
    reverse [Doc]
    before [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
          case [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge [] [(Doc, Maybe PositionInName)]
    after of
            []     -> [Doc
    d]
            Doc
    a : [Doc]
    as -> (Doc
    d Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    a) Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : [Doc]
    as

        mergeLeft :: a -> [a] -> (a, [a])
    mergeLeft a
    d [a]
    before = case [a]
    before of
          []     -> (a
    d,      [])
          a
    b : [a]
    bs -> (a
    b a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    d, [a]
    bs)