{-# 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 :: 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 :: 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 :: 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 :: 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 :: 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 = TacticAttribute -> Doc -> Doc
prettyTactic' (TacticAttribute -> Doc -> Doc)
-> (BoundName -> TacticAttribute) -> BoundName -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundName -> TacticAttribute
bnameTactic

prettyTactic' :: TacticAttribute -> Doc -> Doc
prettyTactic' :: TacticAttribute -> Doc -> Doc
prettyTactic' TacticAttribute
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 ([TypedBinding] -> Tel
Tel ([TypedBinding] -> Tel) -> [TypedBinding] -> Tel
forall a b. (a -> b) -> a -> b
$ [TypedBinding] -> [TypedBinding]
smashTel ([TypedBinding] -> [TypedBinding])
-> [TypedBinding] -> [TypedBinding]
forall a b. (a -> b) -> a -> b
$ Telescope1 -> [TypedBinding]
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 TacticAttribute
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) -> TacticAttribute -> 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) TacticAttribute
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 ((RecordAssignment -> Doc) -> RecordAssignments -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map RecordAssignment -> 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 [TypedBinding]
tel -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
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, TacticAttribute
Nothing <- BoundName -> TacticAttribute
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 [TypedBinding]
tel)
      | (TypedBinding -> Bool) -> [TypedBinding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypedBinding -> Bool
isMeta [TypedBinding]
tel = Doc
forallQ Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
tel)
      | Bool
otherwise      = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
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 :: [TypedBinding] -> [TypedBinding]
smashTel (TBind Range
r List1 (NamedArg Binder)
xs Expr
e  :
          TBind Range
_ List1 (NamedArg Binder)
ys Expr
e' : [TypedBinding]
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' = [TypedBinding] -> [TypedBinding]
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 -> [TypedBinding] -> [TypedBinding]
forall a. a -> [a] -> [a]
: [TypedBinding]
tel)
smashTel (TypedBinding
b : [TypedBinding]
tel) = TypedBinding
b TypedBinding -> [TypedBinding] -> [TypedBinding]
forall a. a -> [a] -> [a]
: [TypedBinding] -> [TypedBinding]
smashTel [TypedBinding]
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
_ [TypedBinding]
bs Expr
e) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
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 TacticAttribute
tac Name
x Expr
e ->
                [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ TacticAttribute -> Doc -> Doc
prettyTactic' TacticAttribute
tac (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 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 TacticAttribute
tac Name
x (Arg ArgInfo
i Expr
e) ->
                IsInstance -> Doc -> Doc
mkInst IsInstance
inst (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. 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 -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Relevant ArgInfo
i) TacticAttribute
tac Name
x Expr
e

                where

                  mkInst :: IsInstance -> Doc -> Doc
mkInst (InstanceDef 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]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x RecordDirectives
dir [LamBinding]
tel (Expr -> TacticAttribute
forall a. a -> Maybe a
Just Expr
e) [Declaration]
cs
            RecordDef Range
_ Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs ->
              Name
-> RecordDirectives
-> [LamBinding]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x RecordDirectives
dir [LamBinding]
tel TacticAttribute
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 [TypedBinding]
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) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
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
_ [TypedBinding]
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) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
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]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x (RecordDirectives Maybe (Ranged Induction)
ind Maybe HasEta0
eta Maybe Range
pat Maybe (Name, IsInstance)
con) [LamBinding]
tel TacticAttribute
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
$ TacticAttribute -> Doc
forall a. Pretty a => Maybe a -> Doc
pType TacticAttribute
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
_ RString
b QName
x)   = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"BUILTIN", String -> Doc
text (RString -> String
forall a. Ranged a -> a
rangedThing RString
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
_ RString
b QName
x String
e) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"COMPILE", String -> Doc
text (RString -> String
forall a. Ranged a -> a
rangedThing RString
b), QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, String -> Doc
text String
e ]
    pretty (ForeignPragma Range
_ RString
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]
++ RString -> String
forall a. Ranged a -> a
rangedThing RString
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 RString
x)   = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ RString -> String
forall a. Ranged a -> a
rangedThing RString
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 NamedName 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 NamedName 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 NamedName Pattern
p     -> Doc -> Doc
braces' (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Named NamedName Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Named NamedName Pattern
p
            InstanceP Range
_ Named NamedName Pattern
p   -> Doc -> Doc
dbraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Named NamedName Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Named NamedName 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 :: 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