    {-# 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.Position
    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 Agda.Utils.Pretty

    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 a, Show b) => Show (ImportDirective' a b)
    deriving instance (Show a, Show b) => Show (Using' a b)
    deriving instance (Show a, Show b) => Show (Renaming' a b)
    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 (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
    <+> 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
    <+>) [Doc]
    ds [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc
    "}"])

    -- | @prettyHiding info visible doc@ puts the correct braces
    --   around @doc@ according to info @info@ and returns
    --   @visible doc@ if the we deal with a visible thing.
    prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding :: forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding a
    a Doc -> Doc
    parens =
      case a -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding a
    a of
        Hiding
    Hidden     -> Doc -> Doc
    braces'
        Instance{} -> Doc -> Doc
    dbraces
        Hiding
    NotHidden  -> Doc -> Doc
    parens

    prettyRelevance :: LensRelevance a => a -> Doc -> Doc
    prettyRelevance :: forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance a
    a Doc
    d =
      if Doc -> String
    render Doc
    d String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "_" then Doc
    d else Relevance -> Doc
    forall a. Pretty a => a -> Doc
    pretty (a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance a
    a) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    d

    prettyQuantity :: LensQuantity a => a -> Doc -> Doc
    prettyQuantity :: forall a. LensQuantity a => a -> Doc -> Doc
    prettyQuantity a
    a Doc
    d =
      if Doc -> String
    render Doc
    d String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "_" then Doc
    d else Quantity -> Doc
    forall a. Pretty a => a -> Doc
    pretty (a -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity a
    a) Doc -> Doc -> Doc
    <+> Doc
    d

    prettyErased :: Erased -> Doc -> Doc
    prettyErased :: Erased -> Doc -> Doc
    prettyErased = Quantity -> Doc -> Doc
    forall a. LensQuantity a => a -> Doc -> Doc
    prettyQuantity (Quantity -> Doc -> Doc)
    -> (Erased -> Quantity) -> Erased -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Erased -> Quantity
    asQuantity

    prettyCohesion :: LensCohesion a => a -> Doc -> Doc
    prettyCohesion :: forall a. LensCohesion a => a -> Doc -> Doc
    prettyCohesion a
    a Doc
    d =
      if Doc -> String
    render Doc
    d String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "_" then Doc
    d else Cohesion -> Doc
    forall a. Pretty a => a -> Doc
    pretty (a -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion a
    a) Doc -> Doc -> Doc
    <+> Doc
    d

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

    prettyTactic' :: TacticAttribute -> Doc -> Doc
    prettyTactic' :: Maybe Expr -> Doc -> Doc
    prettyTactic' Maybe Expr
    Nothing  Doc
    d = Doc
    d
    prettyTactic' (Just Expr
    t) Doc
    d = Doc
    "@" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> (Doc -> Doc
    parens (Doc
    "tactic" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    t) Doc -> Doc -> Doc
    <+> Doc
    d)

    instance (Pretty a, Pretty b) => Pretty (a, b) where
        pretty :: (a, b) -> Doc
    pretty (a
    a, b
    b) = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    comma) Doc -> Doc -> Doc
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    b

    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

    instance Pretty a => Pretty (WithHiding a) where
      pretty :: WithHiding a -> Doc
    pretty WithHiding a
    w = WithHiding a -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding WithHiding a
    w Doc -> Doc
    forall a. a -> a
    id (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ a -> Doc
    forall a. Pretty a => a -> Doc
    pretty (a -> Doc) -> a -> Doc
    forall a b. (a -> b) -> a -> b
    $ WithHiding a -> a
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget WithHiding a
    w

    instance Pretty Relevance where
      pretty :: Relevance -> Doc
    pretty Relevance
    Relevant   = Doc
    forall a. Null a => a
    empty
      pretty Relevance
    Irrelevant = Doc
    "."
      pretty Relevance
    NonStrict  = Doc
    ".."

    instance Pretty Q0Origin where
      pretty :: Q0Origin -> Doc
    pretty = \case
        Q0Origin
    Q0Inferred -> Doc
    forall a. Null a => a
    empty
        Q0{}       -> Doc
    "@0"
        Q0Erased{} -> Doc
    "@erased"

    instance Pretty Q1Origin where
      pretty :: Q1Origin -> Doc
    pretty = \case
        Q1Origin
    Q1Inferred -> Doc
    forall a. Null a => a
    empty
        Q1{}       -> Doc
    "@1"
        Q1Linear{} -> Doc
    "@linear"

    instance Pretty QωOrigin where
      pretty :: QωOrigin -> Doc
    pretty = \case
        QωOrigin
    QωInferred -> Doc
    forall a. Null a => a
    empty
        Qω{}       -> Doc
    "@ω"
        QωPlenty{} -> Doc
    "@plenty"

    instance Pretty Quantity where
      pretty :: Quantity -> Doc
    pretty = \case
        Quantity0 Q0Origin
    o -> Doc -> Doc -> (Doc -> Doc) -> Doc
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull (Q0Origin -> Doc
    forall a. Pretty a => a -> Doc
    pretty Q0Origin
    o) Doc
    "@0" Doc -> Doc
    forall a. a -> a
    id
        Quantity1 Q1Origin
    o -> Doc -> Doc -> (Doc -> Doc) -> Doc
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull (Q1Origin -> Doc
    forall a. Pretty a => a -> Doc
    pretty Q1Origin
    o) Doc
    "@1" Doc -> Doc
    forall a. a -> a
    id
        Quantityω QωOrigin
    o -> QωOrigin -> Doc
    forall a. Pretty a => a -> Doc
    pretty QωOrigin
    o

    instance Pretty Cohesion where
      pretty :: Cohesion -> Doc
    pretty Cohesion
    Flat   = Doc
    "@♭"
      pretty Cohesion
    Continuous = Doc
    forall a. Monoid a => a
    mempty
      pretty Cohesion
    Squash  = Doc
    "@⊤"

    instance Pretty Modality where
      pretty :: Modality -> Doc
    pretty Modality
    mod = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
        [ Relevance -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod)
        , Quantity -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Modality
    mod)
        , Cohesion -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Modality -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion Modality
    mod)
        ]

    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 Expr
    e =
            case Expr
    e of
                Ident QName
    x          -> 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 -> 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
    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
    text Maybe String
    n
                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 Set Name
    _ OpAppArgs
    es -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ QName -> OpAppArgs -> [Doc]
    forall a.
    Pretty a =>
    QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
    prettyOpApp QName
    q OpAppArgs
    es

                WithApp Range
    _ Expr
    e [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
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Expr -> Doc) -> [Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Doc
    "|" Doc -> Doc -> Doc
    <+>) (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

                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
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> List1 LamBinding -> NonEmpty Doc
    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
    <+> Hiding -> Doc
    forall {p}. IsString p => Hiding -> p
    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
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((LamBinding -> Doc) -> List1 LamBinding -> NonEmpty Doc
    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
    <+> Doc
    arrow
                        , Int -> Doc -> Doc
    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
    <+> Hiding -> Doc
    forall {p}. IsString p => Hiding -> p
    absurd Hiding
    h
                ExtendedLam Range
    _ Erased
    e List1 LamClause
    pes ->
                  Doc
    lambda Doc -> Doc -> Doc
    <+>
                  Erased -> Doc -> Doc
    prettyErased Erased
    e (NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    bracesAndSemicolons ((LamClause -> Doc) -> List1 LamClause -> NonEmpty Doc
    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 [ Arg Expr -> Doc -> Doc
    forall a. LensCohesion a => a -> Doc -> Doc
    prettyCohesion Arg Expr
    e1 (Arg Expr -> Doc -> Doc
    forall a. LensQuantity a => a -> Doc -> Doc
    prettyQuantity Arg Expr
    e1 (Arg Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Arg Expr
    e1)) Doc -> Doc -> Doc
    <+> 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 -> Telescope
    forall a. NonEmpty a -> [a]
    List1.toList Telescope1
    tel) Doc -> Doc -> Doc
    <+> 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
    "let" Doc -> Doc -> Doc
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> List1 Declaration -> NonEmpty Doc
    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
    "in" Doc -> Doc -> Doc
    <+> 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
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> Doc -> Doc
    <+> Doc
    rightIdiomBrkt
                    Expr
    e:[Expr]
    es -> Doc
    leftIdiomBrkt Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> Doc -> Doc
    <+> [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
    <+>) (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
    <+> Doc
    rightIdiomBrkt
                DoBlock Range
    _ List1 DoStmt
    ss -> Doc
    "do" Doc -> Doc -> Doc
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((DoStmt -> Doc) -> List1 DoStmt -> NonEmpty Doc
    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 -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                Dot Range
    _ Expr
    e   -> Doc
    "." Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
                DoubleDot Range
    _ Expr
    e  -> 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
    "()"
                Rec Range
    _ RecordAssignments
    xs  -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [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 Range
    _ Expr
    e [FieldAssignment]
    xs ->
                  [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [Doc
    "record" Doc -> Doc -> Doc
    <+> 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)]
                ETel []  -> Doc
    "()"
                ETel Telescope
    tel -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (TypedBinding -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel
                Quote Range
    _ -> Doc
    "quote"
                QuoteTerm Range
    _ -> Doc
    "quoteTerm"
                Unquote Range
    _  -> Doc
    "unquote"
                Tactic Range
    _ Expr
    t -> Doc
    "tactic" Doc -> Doc -> Doc
    <+> 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 -> 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
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    b
                Ellipsis Range
    _  -> Doc
    "..."
                Generalized Expr
    e -> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
            where
              absurd :: Hiding -> p
    absurd Hiding
    NotHidden  = p
    "()"
              absurd Instance{} = p
    "{{}}"
              absurd Hiding
    Hidden     = p
    "{}"

    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
    <+> Doc
    "=" , Int -> Doc -> Doc
    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
    <+> ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i

    instance Pretty LamClause where
      pretty :: LamClause -> Doc
    pretty (LamClause [Pattern]
    ps RHS
    rhs Bool
    _) =
        [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
    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
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    e
          pretty' RHS' a
    AbsurdRHS = Doc
    forall a. Null a => a
    empty

    instance Pretty BoundName where
      pretty :: BoundName -> Doc
    pretty BName{ boundName :: BoundName -> Name
    boundName = Name
    x } = 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 a
    n) = let d :: Doc
    d = a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    n in case Maybe Pattern
    mpat of
        Maybe Pattern
    Nothing  -> Doc
    d
        Just Pattern
    pat -> Doc
    d Doc -> Doc -> Doc
    <+> Doc
    "@" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    pat)

    instance Pretty NamedBinding where
      pretty :: NamedBinding -> Doc
    pretty (NamedBinding Bool
    withH NamedArg Binder
    x) = Doc -> Doc
    prH (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $
        if | Just String
    l <- NamedArg Binder -> Maybe String
    isLabeled NamedArg Binder
    x -> String -> Doc
    text String
    l Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Binder -> Doc
    forall a. Pretty a => a -> Doc
    pretty Binder
    xb
           | Bool
    otherwise             -> Binder -> Doc
    forall a. Pretty a => a -> Doc
    pretty Binder
    xb

        where

        xb :: Binder
    xb = NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    x
        bn :: BoundName
    bn = Binder -> BoundName
    forall a. Binder' a -> a
    binderName Binder
    xb
        prH :: Doc -> Doc
    prH | Bool
    withH     = NamedArg Binder -> Doc -> Doc
    forall a. LensRelevance a => a -> Doc -> Doc
    prettyRelevance NamedArg Binder
    x
                        (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Binder -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding NamedArg Binder
    x Doc -> Doc
    mparens
                        (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Binder -> Doc -> Doc
    forall a. LensCohesion a => a -> Doc -> Doc
    prettyCohesion NamedArg Binder
    x
                        (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Binder -> Doc -> Doc
    forall a. LensQuantity a => a -> Doc -> Doc
    prettyQuantity NamedArg Binder
    x
                        (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BoundName -> Doc -> Doc
    prettyTactic BoundName
    bn
            | Bool
    otherwise = Doc -> Doc
    forall a. a -> a
    id
        -- Parentheses are needed when an attribute @... is present
        mparens :: Doc -> Doc
    mparens
          | NamedArg Binder -> Bool
    forall a. LensQuantity a => a -> Bool
    noUserQuantity NamedArg Binder
    x, Maybe Expr
    Nothing <- BoundName -> Maybe Expr
    bnameTactic BoundName
    bn = Doc -> Doc
    forall a. a -> a
    id
          | Bool
    otherwise = 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
    b) = TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty TypedBinding
    b

    instance Pretty TypedBinding where
        pretty :: TypedBinding -> 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
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> List1 Declaration -> NonEmpty Doc
    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 (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
    $ 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
    $ 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
    <+> 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) -> [NamedArg Binder]
    forall a. NonEmpty a -> [a]
    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 -> Bool) -> Telescope -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any TypedBinding -> Bool
    isMeta Telescope
    tel = Doc
    forallQ Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
          | Bool
    otherwise      = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
          where
            isMeta :: TypedBinding -> Bool
    isMeta (TBind Range
    _ List1 (NamedArg Binder)
    _ (Underscore Range
    _ Maybe String
    Nothing)) = Bool
    True
            isMeta TypedBinding
    _ = 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
    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 -> Telescope -> Telescope
    forall a. a -> [a] -> [a]
    : Telescope
    tel)
    smashTel (TypedBinding
    b : Telescope
    tel) = TypedBinding
    b TypedBinding -> 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
    <+> 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
    _ 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
    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
    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
    _ 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
    $ Bool -> ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (Access
    a Access -> Access -> Bool
    forall a. Eq a => a -> a -> Bool
    == Origin -> Access
    PrivateAccess Origin
    UserWritten) (Doc
    "private" Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    :)
                 [ Doc
    "module", Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    m, Doc
    "where" ]
             , Int -> Doc -> Doc
    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)
             ]

    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
    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
    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
    <+> Doc
    ":" Doc -> Doc -> Doc
    <+> 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 [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 = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ LHSCore -> Doc
    forall a. Pretty a => a -> Doc
    pretty LHSCore
    h Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (Pattern -> Doc) -> [Pattern] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Doc
    "|" Doc -> Doc -> Doc
    <+>) (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) [Pattern]
    wps
      pretty (LHSEllipsis Range
    r LHSCore
    p) = Doc
    "..."

    instance Pretty ModuleApplication where
      pretty :: ModuleApplication -> Doc
    pretty (SectionApp Range
    _ Telescope
    bs Expr
    e) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((TypedBinding -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    bs) Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
      pretty (RecordModuleInstance Range
    _ QName
    rec) = Doc
    "=" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    rec Doc -> Doc -> Doc
    <+> 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
    <+> 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
    <+> NonEmpty Doc -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((Declaration -> Doc) -> List1 Declaration -> NonEmpty Doc
    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 Declaration
    d =
            case Declaration
    d of
                TypeSig ArgInfo
    i Maybe Expr
    tac Name
    x Expr
    e ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Maybe Expr -> Doc -> Doc
    prettyTactic' Maybe Expr
    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
    $ Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> Doc
    ":"
                        , Int -> Doc -> Doc
    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 Maybe Expr
    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}. LensHiding a => a -> Doc -> Doc
    mkOverlap ArgInfo
    i (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) -> 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
    $ 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
    $
                    Declaration -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Declaration -> Doc) -> Declaration -> Doc
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
    TypeSig (Relevance -> ArgInfo -> ArgInfo
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    Relevant ArgInfo
    i) Maybe Expr
    tac Name
    x Expr
    e

                    where

                      mkInst :: IsInstance -> Doc -> Doc
    mkInst (InstanceDef Range
    _) Doc
    d = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "instance", Int -> Doc -> Doc
    nest Int
    2 Doc
    d ]
                      mkInst IsInstance
    NotInstanceDef  Doc
    d = Doc
    d

                      mkOverlap :: a -> Doc -> Doc
    mkOverlap a
    i Doc
    d | a -> Bool
    forall a. LensHiding a => a -> Bool
    isOverlappable a
    i = Doc
    "overlap" Doc -> Doc -> Doc
    <+> Doc
    d
                                    | Bool
    otherwise        = Doc
    d

                Field Range
    _ [Declaration]
    fs ->
                  [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "field"
                      , Int -> Doc -> Doc
    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 Bool
    _ ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ LHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty LHS
    lhs
                        , Int -> Doc -> Doc
    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
    $$ Int -> Doc -> Doc
    nest Int
    2 (WhereClause -> Doc
    forall a. Pretty a => a -> Doc
    pretty WhereClause
    wh)
                DataSig Range
    _ 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"
                                , Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
                                , [Doc] -> Doc
    fcat ((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
    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
    _ 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"
                                , Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
                                , [Doc] -> Doc
    fcat ((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
    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
    $$ Int -> Doc -> Doc
    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
    fcat ((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
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "where"
                        ] Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    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
    _ 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"
                                , Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
                                , [Doc] -> Doc
    fcat ((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
    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
    _ Name
    x RecordDirectives
    dir [LamBinding]
    tel Expr
    e [Declaration]
    cs ->
                  Name
    -> RecordDirectives
    -> [LamBinding]
    -> Maybe Expr
    -> [Declaration]
    -> Doc
    pRecord Name
    x RecordDirectives
    dir [LamBinding]
    tel (Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    e) [Declaration]
    cs
                RecordDef Range
    _ Name
    x RecordDirectives
    dir [LamBinding]
    tel [Declaration]
    cs ->
                  Name
    -> RecordDirectives
    -> [LamBinding]
    -> Maybe Expr
    -> [Declaration]
    -> Doc
    pRecord Name
    x RecordDirectives
    dir [LamBinding]
    tel Maybe Expr
    forall a. Maybe a
    Nothing [Declaration]
    cs
                RecordDirective RecordDirective
    r -> RecordDirective -> Doc
    pRecordDirective RecordDirective
    r
                Infix Fixity
    f List1 Name
    xs  ->
                    Fixity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Fixity
    f Doc -> Doc -> Doc
    <+> [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 (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
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n Doc -> Doc -> Doc
    <+> Doc
    "..."
                PatternSyn Range
    _ Name
    n [Arg Name]
    as Pattern
    p -> Doc
    "pattern" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    n Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ((Arg Name -> Doc) -> [Arg Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Arg Name]
    as)
                                         Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p
                Mutual Range
    _ [Declaration]
    ds     -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "mutual" [Declaration]
    ds
                InterleavedMutual Range
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "interleaved mutual" [Declaration]
    ds
                LoneConstructor Range
    _ [Declaration]
    ds -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "constructor" [Declaration]
    ds
                Abstract Range
    _ [Declaration]
    ds   -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "abstract" [Declaration]
    ds
                Private Range
    _ Origin
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "private" [Declaration]
    ds
                InstanceB Range
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "instance" [Declaration]
    ds
                Macro Range
    _ [Declaration]
    ds      -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "macro" [Declaration]
    ds
                Postulate Range
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "postulate" [Declaration]
    ds
                Primitive Range
    _ [Declaration]
    ds  -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "primitive" [Declaration]
    ds
                Generalize Range
    _ [Declaration]
    ds -> String -> [Declaration] -> Doc
    forall {a}. Pretty a => String -> [a] -> Doc
    namedBlock String
    "variable" [Declaration]
    ds
                Module Range
    _ QName
    x Telescope
    tel [Declaration]
    ds ->
                    [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "module"
                         , QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
                         , [Doc] -> Doc
    fcat ((TypedBinding -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
                         , Doc
    "where"
                         ] Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    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
    _ Name
    x (SectionApp Range
    _ [] Expr
    e) 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
    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
                        , Int -> Doc -> Doc
    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
    _ Name
    x (SectionApp Range
    _ Telescope
    tel Expr
    e) 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
    <+> Doc
    "module" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    fcat ((TypedBinding -> Doc) -> Telescope -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> Doc
    forall a. Pretty a => a -> Doc
    pretty Telescope
    tel)
                        , Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "=" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e Doc -> Doc -> Doc
    <+> ImportDirective -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportDirective
    i
                        ]
                ModuleMacro Range
    _ 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
    <+> Doc
    "module" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
                        , Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "=" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    rec Doc -> Doc -> Doc
    <+> 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
    <+> 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
    <+> [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
    <+> Doc
    "=", Int -> Doc -> Doc
    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
    <+> [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
    <+> Doc
    "=", Int -> Doc -> Doc
    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
    <+> 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
    text String
    s
                        , Int -> Doc -> Doc
    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"

    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
      :: Name
      -> RecordDirectives
      -> [LamBinding]
      -> Maybe Expr
      -> [Declaration]
      -> Doc
    pRecord :: Name
    -> RecordDirectives
    -> [LamBinding]
    -> Maybe Expr
    -> [Declaration]
    -> Doc
    pRecord Name
    x (RecordDirectives Maybe (Ranged Induction)
    ind Maybe HasEta0
    eta Maybe Range
    pat Maybe (Name, IsInstance)
    con) [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"
                  , Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
                  , [Doc] -> Doc
    fcat ((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
    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
    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
          [ [Doc]
    pInd
          , [Doc]
    pEta
          , [Doc]
    pPat
          , [Doc]
    pCon
          , (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"
            pInd :: [Doc]
    pInd = Maybe Doc -> [Doc]
    forall a. Maybe a -> [a]
    maybeToList (Maybe Doc -> [Doc]) -> Maybe Doc -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ Induction -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Induction -> Doc)
    -> (Ranged Induction -> Induction) -> Ranged Induction -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ranged Induction -> Induction
    forall a. Ranged a -> a
    rangedThing (Ranged Induction -> Doc) -> Maybe (Ranged Induction) -> Maybe Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Ranged Induction)
    ind
            pEta :: [Doc]
    pEta = Maybe Doc -> [Doc]
    forall a. Maybe a -> [a]
    maybeToList (Maybe Doc -> [Doc]) -> Maybe Doc -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ Maybe HasEta0
    eta Maybe HasEta0 -> (HasEta0 -> Doc) -> Maybe Doc
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> HasEta0 -> Doc
    pHasEta0
            pPat :: [Doc]
    pPat = Maybe Doc -> [Doc]
    forall a. Maybe a -> [a]
    maybeToList (Maybe Doc -> [Doc]) -> Maybe Doc -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ Doc
    "pattern" Doc -> Maybe Range -> Maybe Doc
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe Range
    pat
            -- pEta = caseMaybe eta [] $ \case
            --   YesEta -> [ "eta-equality" ]
            --   NoEta  -> "no-eta-equality" : pPat
            -- pPat = \case
            --   PatternMatching   -> [ "pattern" ]
            --   CopatternMatching -> []
            pCon :: [Doc]
    pCon = Maybe Doc -> [Doc]
    forall a. Maybe a -> [a]
    maybeToList (Maybe Doc -> [Doc]) -> Maybe Doc -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ ((Doc
    "constructor" Doc -> Doc -> Doc
    <+>) (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty) (Name -> Doc)
    -> ((Name, IsInstance) -> Name) -> (Name, IsInstance) -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, IsInstance) -> Name
    forall a b. (a, b) -> a
    fst ((Name, IsInstance) -> Doc)
    -> Maybe (Name, IsInstance) -> Maybe Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Name, IsInstance)
    con

    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
    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
    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 String
    b QName
    x String
    e) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "COMPILE", String -> Doc
    text (Ranged String -> String
    forall a. Ranged a -> a
    rangedThing Ranged String
    b), QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x, String -> Doc
    text String
    e ]
        pretty (ForeignPragma Range
    _ Ranged String
    b String
    s) =
          [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text (String
    "FOREIGN " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Ranged String -> String
    forall a. Ranged a -> a
    rangedThing Ranged String
    b) Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : (String -> Doc) -> [String] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Doc
    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 (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 (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
    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 Text
    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
    text (Text -> String
    T.unpack Text
    str) ]
        pretty (WarningOnImport Range
    _ Text
    str)   = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "WARNING_ON_IMPORT", String -> Doc
    text (Text -> String
    T.unpack Text
    str) ]
        pretty (CatchallPragma Range
    _) = Doc
    "CATCHALL"
        pretty (DisplayPragma Range
    _ Pattern
    lhs Expr
    rhs) = Doc
    "DISPLAY" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    lhs Doc -> Doc -> Doc
    <+> Doc
    "=", Int -> Doc -> Doc
    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 [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]
    : (Occurrence -> Doc) -> [Occurrence] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Occurrence -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Occurrence]
    occs)
        pretty (NoUniverseCheckPragma Range
    _) = Doc
    "NO_UNIVERSE_CHECK"

    instance Pretty Associativity where
      pretty :: Associativity -> Doc
    pretty = \case
        Associativity
    LeftAssoc  -> Doc
    "infixl"
        Associativity
    RightAssoc -> Doc
    "infixr"
        Associativity
    NonAssoc   -> Doc
    "infix"

    instance Pretty FixityLevel where
      pretty :: FixityLevel -> Doc
    pretty = \case
        FixityLevel
    Unrelated  -> Doc
    forall a. Null a => a
    empty
        Related PrecedenceLevel
    d  -> String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ PrecedenceLevel -> String
    toStringWithoutDotZero PrecedenceLevel
    d

    instance Pretty Fixity where
      pretty :: Fixity -> Doc
    pretty (Fixity Range
    _ FixityLevel
    level Associativity
    ass) = case FixityLevel
    level of
        FixityLevel
    Unrelated  -> Doc
    forall a. Null a => a
    empty
        Related{}  -> Associativity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Associativity
    ass Doc -> Doc -> Doc
    <+> FixityLevel -> Doc
    forall a. Pretty a => a -> Doc
    pretty FixityLevel
    level

    instance Pretty GenPart where
        pretty :: GenPart -> Doc
    pretty (IdPart Ranged String
    x)   = String -> Doc
    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 BindHole{}   = Doc
    forall a. Underscore a => a
    underscore
        pretty NormalHole{} = Doc
    forall a. Underscore a => a
    underscore
        pretty WildHole{}   = 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
    . (GenPart -> Doc) -> Notation -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map GenPart -> 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
    <+> Notation -> Doc
    forall a. Pretty a => a -> Doc
    pretty Notation
    nota

     -- Andreas 2010-09-21: do not print relevance in general, only in function types!
     -- Andreas 2010-09-24: and in record fields
    instance Pretty a => Pretty (Arg a) where
      prettyPrec :: Int -> Arg a -> Doc
    prettyPrec Int
    p (Arg ArgInfo
    ai a
    e) = ArgInfo -> (Doc -> Doc) -> Doc -> Doc
    forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
    prettyHiding ArgInfo
    ai Doc -> Doc
    localParens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> a -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p' a
    e
          where p' :: Int
    p' | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    visible ArgInfo
    ai = Int
    p
                   | Bool
    otherwise  = Int
    0
                localParens :: Doc -> Doc
    localParens | ArgInfo -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin ArgInfo
    ai Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    == Origin
    Substitution = Doc -> Doc
    parens
                            | Bool
    otherwise = Doc -> Doc
    forall a. a -> a
    id

    instance Pretty e => Pretty (Named_ e) where
      prettyPrec :: Int -> Named_ e -> Doc
    prettyPrec Int
    p (Named Maybe NamedName
    nm e
    e)
        | Just String
    s <- Maybe NamedName -> Maybe String
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
    bareNameOf Maybe NamedName
    nm = Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ String -> Doc
    text String
    s Doc -> Doc -> Doc
    <+> Doc
    "=", e -> Doc
    forall a. Pretty a => a -> Doc
    pretty e
    e ]
        | Bool
    otherwise               = Int -> e -> Doc
    forall a. Pretty a => Int -> a -> Doc
    prettyPrec Int
    p e
    e

    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 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
    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 Set Name
    _ [NamedArg Pattern]
    ps -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ QName -> [NamedArg (MaybePlaceholder Pattern)] -> [Doc]
    forall a.
    Pretty a =>
    QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
    prettyOpApp QName
    q ([NamedArg (MaybePlaceholder Pattern)] -> [Doc])
    -> [NamedArg (MaybePlaceholder Pattern)] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> NamedArg (MaybePlaceholder Pattern))
    -> [NamedArg Pattern] -> [NamedArg (MaybePlaceholder Pattern)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named_ Pattern -> Named NamedName (MaybePlaceholder Pattern))
    -> NamedArg Pattern -> NamedArg (MaybePlaceholder Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Pattern -> MaybePlaceholder Pattern)
    -> Named_ Pattern -> Named NamedName (MaybePlaceholder Pattern)
    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))) [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 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 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
    _ [(Expr, Expr)]
    es     -> [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
    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]) | (Expr
    e1,Expr
    e2) <- [(Expr, Expr)]
    es ]
                EllipsisP Range
    _ Maybe Pattern
    mp  -> Doc
    "..."
                WithP Range
    _ Pattern
    p       -> Doc
    "|" Doc -> Doc -> Doc
    <+> Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p

    prettyOpApp :: forall a .
      Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
    prettyOpApp :: forall a.
    Pretty a =>
    QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
    prettyOpApp QName
    q [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 [NamePart]
    xs [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 :: [NamePart]
    xs = case QName -> Name
    unqualify QName
    q of
               Name Range
    _ NameInScope
    _ NameParts
    xs    -> NameParts -> [NamePart]
    forall a. NonEmpty a -> [a]
    List1.toList NameParts
    xs
               NoName{}       -> [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
    $ 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)

    instance (Pretty a, Pretty b) => Pretty (ImportDirective' a b) where
        pretty :: ImportDirective' a b -> Doc
    pretty ImportDirective' a b
    i =
            [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Maybe Range -> Doc
    forall {p} {a}. (IsString p, Null p) => Maybe a -> p
    public (ImportDirective' a b -> Maybe Range
    forall n m. ImportDirective' n m -> Maybe Range
    publicOpen ImportDirective' a b
    i)
                , Using' a b -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Using' a b -> Doc) -> Using' a b -> Doc
    forall a b. (a -> b) -> a -> b
    $ ImportDirective' a b -> Using' a b
    forall n m. ImportDirective' n m -> Using' n m
    using ImportDirective' a b
    i
                , [ImportedName' a b] -> Doc
    forall {a}. Pretty a => [a] -> Doc
    prettyHiding ([ImportedName' a b] -> Doc) -> [ImportedName' a b] -> Doc
    forall a b. (a -> b) -> a -> b
    $ ImportDirective' a b -> [ImportedName' a b]
    forall n m. ImportDirective' n m -> HidingDirective' n m
    hiding ImportDirective' a b
    i
                , [Renaming' a b] -> Doc
    forall {a}. Pretty a => [a] -> Doc
    rename ([Renaming' a b] -> Doc) -> [Renaming' a b] -> Doc
    forall a b. (a -> b) -> a -> b
    $ ImportDirective' a b -> [Renaming' a b]
    forall n m. ImportDirective' n m -> RenamingDirective' n m
    impRenaming ImportDirective' a b
    i
                ]
            where
                public :: Maybe a -> p
    public Just{}  = p
    "public"
                public Maybe a
    Nothing = p
    forall a. Null a => a
    empty

                prettyHiding :: [a] -> Doc
    prettyHiding [] = Doc
    forall a. Null a => a
    empty
                prettyHiding [a]
    xs = Doc
    "hiding" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([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]
    xs)

                rename :: [a] -> Doc
    rename [] = Doc
    forall a. Null a => a
    empty
                rename [a]
    xs = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep [ Doc
    "renaming"
                                 , Doc -> Doc
    parens (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] -> [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]
    xs
                                 ]

    instance (Pretty a, Pretty b) => Pretty (Using' a b) where
        pretty :: Using' a b -> Doc
    pretty Using' a b
    UseEverything = Doc
    forall a. Null a => a
    empty
        pretty (Using [ImportedName' a b]
    xs)    =
            Doc
    "using" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([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
    $ (ImportedName' a b -> Doc) -> [ImportedName' a b] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ImportedName' a b -> Doc
    forall a. Pretty a => a -> Doc
    pretty [ImportedName' a b]
    xs)

    instance (Pretty a, Pretty b) => Pretty (Renaming' a b) where
        pretty :: Renaming' a b -> Doc
    pretty (Renaming ImportedName' a b
    from ImportedName' a b
    to Maybe Fixity
    mfx Range
    _r) = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
          [ ImportedName' a b -> Doc
    forall a. Pretty a => a -> Doc
    pretty ImportedName' a b
    from
          , Doc
    "to"
          , Doc -> (Fixity -> Doc) -> Maybe Fixity -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Null a => a
    empty Fixity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Maybe Fixity
    mfx
          , case ImportedName' a b
    to of
              ImportedName a
    a   -> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a
              ImportedModule b
    b -> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    b   -- don't print "module" here
          ]

    instance (Pretty a, Pretty b) => Pretty (ImportedName' a b) where
        pretty :: ImportedName' a b -> Doc
    pretty (ImportedName   a
    a) = a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    a
        pretty (ImportedModule b
    b) = Doc
    "module" Doc -> Doc -> Doc
    <+> b -> Doc
    forall a. Pretty a => a -> Doc
    pretty b
    b