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

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

import Prelude hiding ( null )

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

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

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

import Agda.Utils.Impossible

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

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

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

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

prettyRelevance :: LensRelevance a => a -> Doc -> Doc
prettyRelevance :: forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance a
a = (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
<>)

prettyQuantity :: LensQuantity a => a -> Doc -> Doc
prettyQuantity :: forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity a
a = (Quantity -> Doc
forall a. Pretty a => a -> Doc
pretty (a -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity a
a) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>)

prettyLock :: LensLock a => a -> Doc -> Doc
prettyLock :: forall a. LensLock a => a -> Doc -> Doc
prettyLock a
a Doc
doc = case a -> Lock
forall a. LensLock a => a -> Lock
getLock a
a of
  IsLock LockOrigin
LockOLock -> Doc
"@lock" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
doc
  IsLock LockOrigin
LockOTick -> Doc
"@tick" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
doc
  Lock
IsNotLock -> Doc
doc

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

prettyCohesion :: LensCohesion a => a -> Doc -> Doc
prettyCohesion :: forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion a
a = (Cohesion -> Doc
forall a. Pretty a => a -> Doc
pretty (a -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion a
a) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>)

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

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

prettyTactic' :: TacticAttribute -> Doc -> Doc
prettyTactic' :: TacticAttribute -> Doc -> Doc
prettyTactic' TacticAttribute
Nothing  Doc
d = Doc
d
prettyTactic' (Just Ranged Expr
t) Doc
d = Doc
"@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (Doc -> Doc
parens (Doc
"tactic" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Ranged Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Ranged Expr
t) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> 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
forall a. Doc a -> Doc a -> Doc a
<+> 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 Erased where
  pretty :: Erased -> Doc
pretty = Quantity -> Doc
forall a. Pretty a => a -> Doc
pretty (Quantity -> Doc) -> (Erased -> Quantity) -> Erased -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Erased -> Quantity
asQuantity

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)
    ]

-- | Show the attributes necessary to recover a modality, in long-form
-- (e.g. using at-syntax rather than dots). For the default modality,
-- the result is at-ω (rather than the empty document). Suitable for
-- showing modalities outside of binders.
attributesForModality :: Modality -> Doc
attributesForModality :: Modality -> Doc
attributesForModality Modality
mod
  | Modality
mod Modality -> Modality -> Bool
forall a. Eq a => a -> a -> Bool
== Modality
defaultModality = String -> Doc
forall a. String -> Doc a
text String
"@ω"
  | Bool
otherwise = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Maybe Doc] -> [Doc]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Doc
relevance, Maybe Doc
quantity, Maybe Doc
cohesion]
  where
    relevance :: Maybe Doc
relevance = case Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod of
      Relevance
Relevant   -> Maybe Doc
forall a. Maybe a
Nothing
      Relevance
Irrelevant -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"@irrelevant"
      Relevance
NonStrict  -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"@shape-irrelevant"
    quantity :: Maybe Doc
quantity = case Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod of
      Quantity0{} -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"@0"
      Quantity1{} -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"@1"
      Quantityω{} -> Maybe Doc
forall a. Maybe a
Nothing
    cohesion :: Maybe Doc
cohesion = case Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
mod of
      Flat{}       -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"@♭"
      Continuous{} -> Maybe Doc
forall a. Maybe a
Nothing
      Squash{}     -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
"@⊤"

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
            KnownIdent NameKind
nk QName
x  -> Aspect -> Doc -> Doc
annotateAspect (Maybe NameKind -> Bool -> Aspect
Asp.Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
nk) Bool
False) (QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x)
            Lit Range
_ Literal
l          -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
            QuestionMark Range
_ Maybe Int
n -> Doc -> Doc
hlSymbol Doc
"?" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (Int -> Doc) -> Maybe Int -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty (String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (Int -> String) -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) Maybe Int
n
            Underscore Range
_ Maybe String
n   -> Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Underscore a => a
underscore String -> Doc
forall a. String -> Doc a
text Maybe String
n
            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
$ Aspect -> QName -> OpAppArgs -> [Doc]
forall a.
Pretty a =>
Aspect -> QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp (Maybe NameKind -> Bool -> Aspect
Asp.Name Maybe NameKind
forall a. Maybe a
Nothing Bool
True) QName
q OpAppArgs
es
            KnownOpApp NameKind
nk Range
_ QName
q 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
$ Aspect -> QName -> OpAppArgs -> [Doc]
forall a.
Pretty a =>
Aspect -> QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp (Maybe NameKind -> Bool -> Aspect
Asp.Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
nk) Bool
True) QName
q OpAppArgs
es

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

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

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

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

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

instance Pretty LamClause where
  pretty :: LamClause -> Doc
pretty (LamClause [Pattern]
ps RHS
rhs 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
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ RHS -> Doc
forall {a}. Pretty a => RHS' a -> Doc
pretty' RHS
rhs
        ]
    where
      pretty' :: RHS' a -> Doc
pretty' (RHS a
e)   = Doc
arrow Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e
      pretty' RHS' a
AbsurdRHS = Doc
forall a. Null a => a
empty

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
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"@" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc -> Doc
parens (Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
pat)

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
forall a. String -> Doc a
text String
l Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> 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' Expr
b) = TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty TypedBinding' Expr
b

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

newtype Tel = Tel Telescope

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

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


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

instance Pretty WhereClause where
  pretty :: WhereClause -> Doc
pretty  WhereClause
NoWhere = Doc
forall a. Null a => a
empty
  pretty (AnyWhere Range
_ [Module Range
_ NotErased{} QName
x [] [Declaration]
ds])
    | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName (QName -> Name
unqualify QName
x)
                       = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ Doc
"where", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
ds) ]
  pretty (AnyWhere Range
_ [Declaration]
ds) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ Doc
"where", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
ds) ]
  pretty (SomeWhere Range
_ Erased
erased Name
m Access
a [Declaration]
ds) =
    [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall b a. IsBool b => b -> (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", Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
m), Doc
"where" ]
         , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
ds)
         ]

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

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

instance Pretty LHSCore where
  pretty :: LHSCore -> Doc
pretty (LHSHead QName
f [NamedArg Pattern]
ps) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc)
-> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps
  pretty (LHSProj QName
d [NamedArg Pattern]
ps NamedArg LHSCore
lhscore [NamedArg Pattern]
ps') = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
d Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc)
-> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
    Doc -> Doc
parens (NamedArg LHSCore -> Doc
forall a. Pretty a => a -> Doc
pretty NamedArg LHSCore
lhscore) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (NamedArg Pattern -> Doc) -> [NamedArg Pattern] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc)
-> (NamedArg Pattern -> Doc) -> NamedArg Pattern -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps'
  pretty (LHSWith LHSCore
h [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
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc -> Doc) -> (Pattern -> Doc) -> Pattern -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty) [Pattern]
wps
  pretty (LHSEllipsis Range
r LHSCore
p) = Doc
"..."

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

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

instance Pretty Declaration where
  prettyList :: [Declaration] -> Doc
prettyList = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> ([Declaration] -> [Doc]) -> [Declaration] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty
  pretty :: Declaration -> Doc
pretty = \case
    TypeSig ArgInfo
i TacticAttribute
tac Name
x Expr
e ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ TacticAttribute -> Doc -> Doc
prettyTactic' TacticAttribute
tac (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
":"
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
          ]
    FieldSig IsInstance
inst TacticAttribute
tac Name
x (Arg ArgInfo
i Expr
e) ->
      IsInstance -> Doc -> Doc
mkInst IsInstance
inst (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall {a} {a}. LensHiding a => a -> Doc a -> Doc a
mkOverlap ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
      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
forall a. Int -> Doc a -> Doc a
nest Int
2 Doc
d ]
        mkInst IsInstance
NotInstanceDef  Doc
d = Doc
d

        mkOverlap :: a -> Doc a -> Doc a
mkOverlap a
i Doc a
d | a -> Bool
forall a. LensHiding a => a -> Bool
isOverlappable a
i = Doc a
"overlap" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> Doc a
d
                      | Bool
otherwise        = Doc a
d
    Field Range
_ [Declaration]
fs ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"field"
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ((Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
fs)
          ]
    FunClause LHS
lhs RHS
rhs WhereClause
wh 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
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ RHS -> Doc
forall a. Pretty a => a -> Doc
pretty RHS
rhs
          ] Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (WhereClause -> Doc
forall a. Pretty a => a -> Doc
pretty WhereClause
wh)
    DataSig Range
_ Erased
erased Name
x [LamBinding]
tel Expr
e ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"data"
                  , Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x)
                  , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                  [ Doc
":"
                  , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                  ]
          ]
    Data Range
_ Erased
erased Name
x [LamBinding]
tel Expr
e [Declaration]
cs ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"data"
                  , Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x)
                  , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                  [ Doc
":"
                  , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                  , Doc
"where"
                  ]
          ] Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
cs)
    DataDef Range
_ Name
x [LamBinding]
tel [Declaration]
cs ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"data"
                  , Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
                  , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"where"
          ] Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
cs)
    RecordSig Range
_ Erased
erased Name
x [LamBinding]
tel Expr
e ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"record"
                  , Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x)
                  , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                  [ Doc
":"
                  , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                  ]
          ]
    Record Range
_ Erased
erased Name
x RecordDirectives
dir [LamBinding]
tel Expr
e [Declaration]
cs ->
      Erased
-> Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Doc
pRecord Erased
erased Name
x RecordDirectives
dir [LamBinding]
tel (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e) [Declaration]
cs
    RecordDef Range
_ Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs ->
      Erased
-> Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Doc
pRecord Erased
defaultErased Name
x RecordDirectives
dir [LamBinding]
tel Maybe Expr
forall a. Maybe a
Nothing [Declaration]
cs
    RecordDirective RecordDirective
r -> RecordDirective -> Doc
pRecordDirective RecordDirective
r
    Infix Fixity
f List1 Name
xs  ->
      Fixity -> Doc
forall a. Pretty a => a -> Doc
pretty Fixity
f Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (Doc -> NonEmpty Doc -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma (NonEmpty Doc -> [Doc]) -> NonEmpty Doc -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> List1 Name -> NonEmpty Doc
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Doc
forall a. Pretty a => a -> Doc
pretty List1 Name
xs)
    Syntax Name
n Notation
xs -> Doc
"syntax" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"..."
    PatternSyn Range
_ Name
n [Arg Name]
as Pattern
p -> Doc
"pattern" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((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
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
    Mutual 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
    Opaque Range
_ [Declaration]
ds     -> String -> [Declaration] -> Doc
forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"opaque" [Declaration]
ds
    Unfolding Range
_ [QName]
rs  -> Doc
"unfolding" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc -> Doc
braces ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
semi (QName -> Doc
forall a. Pretty a => a -> Doc
pretty (QName -> Doc) -> [QName] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QName]
rs)))
    Module Range
_ Erased
erased QName
x Telescope
tel [Declaration]
ds ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"module"
           , Erased -> Doc -> Doc
prettyErased Erased
erased (QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x)
           , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
tel)
           , Doc
"where"
           ] Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
ds)
    ModuleMacro Range
_ NotErased{} Name
x (SectionApp Range
_ [] 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
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i
          ]
    ModuleMacro Range
_ Erased
erased Name
x (SectionApp Range
_ Telescope
tel 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
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"module" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>
            Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((TypedBinding' Expr -> Doc) -> Telescope -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
tel)
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"=" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i
          ]
    ModuleMacro Range
_ Erased
erased Name
x (RecordModuleInstance Range
_ QName
rec) OpenShortHand
open ImportDirective
i ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"module" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x)
          , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"=" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
rec Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"{{...}}"
          ]
    Open Range
_ QName
x ImportDirective
i  -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"open", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i ]
    Import Range
_ QName
x Maybe AsName
rn OpenShortHand
open ImportDirective
i   ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open, Doc
"import", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, Maybe AsName -> Doc
forall {a}. Pretty a => Maybe (AsName' a) -> Doc
as Maybe AsName
rn, ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i ]
      where
        as :: Maybe (AsName' a) -> Doc
as Maybe (AsName' a)
Nothing  = Doc
forall a. Null a => a
empty
        as (Just AsName' a
x) = Doc
"as" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty (AsName' a -> a
forall a. AsName' a -> a
asName AsName' a
x)
    UnquoteDecl Range
_ [Name]
xs Expr
t ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"unquoteDecl" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
    UnquoteDef Range
_ [Name]
xs Expr
t ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"unquoteDef" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
    UnquoteData Range
_ Name
x [Name]
xs Expr
t ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"unquoteData" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
    Pragma Pragma
pr   -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"{-#" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Pragma -> Doc
forall a. Pretty a => a -> Doc
pretty Pragma
pr, Doc
"#-}" ]
    where
      namedBlock :: String -> [a] -> Doc
namedBlock String
s [a]
ds =
          [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
forall a. String -> Doc a
text String
s
              , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
ds
              ]

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

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

pRecord
  :: Erased
  -> Name
  -> RecordDirectives
  -> [LamBinding]
  -> Maybe Expr
  -> [Declaration]
  -> Doc
pRecord :: Erased
-> Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Doc
pRecord Erased
erased Name
x (RecordDirectives Maybe (Ranged Induction)
ind Maybe HasEta0
eta Maybe Range
pat Maybe (Name, IsInstance)
con) [LamBinding]
tel Maybe Expr
me [Declaration]
ds = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
      [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"record"
              , Erased -> Doc -> Doc
prettyErased Erased
erased (Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x)
              , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
              ]
      , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Maybe Expr -> Doc
forall {a}. Pretty a => Maybe a -> Doc
pType Maybe Expr
me
      ]
    , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 a b. a -> Maybe b -> Maybe a
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
forall a. Doc a -> Doc a -> Doc a
<+>) (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
forall a. String -> Doc a
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String
"OPTIONS" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
opts
    pretty (BuiltinPragma Range
_ Ranged String
b QName
x)   = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"BUILTIN", String -> Doc
forall a. String -> Doc a
text (Ranged String -> String
forall a. Ranged a -> a
rangedThing Ranged String
b), QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x ]
    pretty (RewritePragma Range
_ Range
_ [QName]
xs)    =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"REWRITE", [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (QName -> Doc) -> [QName] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Doc
forall a. Pretty a => a -> Doc
pretty [QName]
xs ]
    pretty (CompilePragma Range
_ Ranged String
b QName
x String
e) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"COMPILE", String -> Doc
forall a. String -> Doc a
text (Ranged String -> String
forall a. Ranged a -> a
rangedThing Ranged String
b), QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, String -> Doc
forall a. String -> Doc a
text String
e ]
    pretty (ForeignPragma Range
_ Ranged String
b String
s) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
text (String
"FOREIGN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ranged String -> String
forall a. Ranged a -> a
rangedThing Ranged String
b) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
forall a. String -> Doc a
text (String -> [String]
lines String
s)
    pretty (StaticPragma Range
_ QName
i) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"STATIC", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InjectivePragma Range
_ QName
i) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"INJECTIVE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InlinePragma Range
_ Bool
True QName
i) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"INLINE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (NotProjectionLikePragma Range
_ QName
i) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"NOT_PROJECTION_LIKE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InlinePragma Range
_ Bool
False QName
i) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"NOINLINE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (ImpossiblePragma Range
_ [String]
strs) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"IMPOSSIBLE"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
forall a. String -> Doc a
text [String]
strs
    pretty (EtaPragma Range
_ QName
x) =
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"ETA", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x]
    pretty (TerminationCheckPragma Range
_ TerminationCheck Name
tc) =
      case TerminationCheck Name
tc of
        TerminationCheck Name
TerminationCheck       -> Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
        TerminationCheck Name
NoTerminationCheck     -> Doc
"NO_TERMINATION_CHECK"
        TerminationCheck Name
NonTerminating         -> Doc
"NON_TERMINATING"
        TerminationCheck Name
Terminating            -> Doc
"TERMINATING"
        TerminationMeasure Range
_ Name
x -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"MEASURE", Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x]
    pretty (NoCoverageCheckPragma Range
_) = Doc
"NON_COVERING"
    pretty (WarningOnUsage Range
_ QName
nm 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
forall a. String -> Doc a
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
forall a. String -> Doc a
text (Text -> String
T.unpack Text
str) ]
    pretty (CatchallPragma Range
_) = Doc
"CATCHALL"
    pretty (DisplayPragma Range
_ Pattern
lhs Expr
rhs) = Doc
"DISPLAY" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
lhs Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
rhs ]
    pretty (NoPositivityCheckPragma Range
_) = Doc
"NO_POSITIVITY_CHECK"
    pretty (PolarityPragma Range
_ Name
q [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
forall a. String -> Doc a
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
forall a. Doc a -> Doc a -> Doc a
<+> FixityLevel -> Doc
forall a. Pretty a => a -> Doc
pretty FixityLevel
level

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

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

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

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

prettyOpApp :: forall a .
  Pretty a => Asp.Aspect -> QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp :: forall a.
Pretty a =>
Aspect -> QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp Aspect
asp 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 [Item NameParts]
[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 :: [Item NameParts]
xs = case QName -> Name
unqualify QName
q of
           Name Range
_ NameInScope
_ NameParts
xs    -> NameParts -> [Item NameParts]
forall l. IsList l => l -> [Item l]
List1.toList NameParts
xs
           NoName{}       -> [Item NameParts]
[NamePart]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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 {a} {a}. (IsString a, Null a) => Maybe a -> a
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 -> a
public Just{}  = a
"public"
            public Maybe a
Nothing = a
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
forall a. Doc a -> Doc a -> Doc a
<+> 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
forall a. Doc a -> Doc a -> Doc a
<+> 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
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b