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


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

import Prelude hiding ( null )

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

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

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

import Agda.Utils.Impossible

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

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

bracesAndSemicolons :: Foldable t => t Doc -> Doc
bracesAndSemicolons :: forall (t :: * -> *). Foldable t => t Doc -> Doc
bracesAndSemicolons t Doc
ts = case forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList t Doc
ts of
  []       -> Doc
"{}"
  (Doc
d : [Doc]
ds) -> forall (t :: * -> *). Foldable t => t Doc -> Doc
sep ([Doc
"{" Doc -> Doc -> Doc
<+> Doc
d] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Doc
";" Doc -> Doc -> Doc
<+>) [Doc]
ds 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 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 = (forall a. Pretty a => a -> Doc
pretty (forall a. LensRelevance a => a -> Relevance
getRelevance a
a) forall a. Semigroup a => a -> a -> a
<>)

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

prettyErased :: Erased -> Doc -> Doc
prettyErased :: Erased -> Doc -> Doc
prettyErased = forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity 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 = (forall a. Pretty a => a -> Doc
pretty (forall a. LensCohesion a => a -> Cohesion
getCohesion a
a) Doc -> Doc -> Doc
<+>)

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

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

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

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

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

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

instance Pretty Relevance where
  pretty :: Relevance -> Doc
pretty Relevance
Relevant   = 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 -> forall a. Null a => a
empty
    Q0{}       -> Doc
"@0"
    Q0Erased{} -> Doc
"@erased"

instance Pretty Q1Origin where
  pretty :: Q1Origin -> Doc
pretty = \case
    Q1Origin
Q1Inferred -> 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 -> forall a. Null a => a
empty
    Qω{}       -> Doc
"@ω"
    QωPlenty{} -> Doc
"@plenty"

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

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

instance Pretty Modality where
  pretty :: Modality -> Doc
pretty Modality
mod = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
    [ forall a. Pretty a => a -> Doc
pretty (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod)
    , forall a. Pretty a => a -> Doc
pretty (forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod)
    , forall a. Pretty a => a -> Doc
pretty (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 forall a. Eq a => a -> a -> Bool
== Modality
defaultModality = String -> Doc
text String
"@ω"
  | Bool
otherwise = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe Doc
relevance, Maybe Doc
quantity, Maybe Doc
cohesion]
  where
    relevance :: Maybe Doc
relevance = case forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod of
      Relevance
Relevant   -> forall a. Maybe a
Nothing
      Relevance
Irrelevant -> forall a. a -> Maybe a
Just Doc
"@irrelevant"
      Relevance
NonStrict  -> forall a. a -> Maybe a
Just Doc
"@shape-irrelevant"
    quantity :: Maybe Doc
quantity = case forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod of
      Quantity0{} -> forall a. a -> Maybe a
Just Doc
"@0"
      Quantity1{} -> forall a. a -> Maybe a
Just Doc
"@1"
      Quantityω{} -> forall a. Maybe a
Nothing
    cohesion :: Maybe Doc
cohesion = case forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
mod of
      Flat{}       -> forall a. a -> Maybe a
Just Doc
"@♭"
      Continuous{} -> forall a. Maybe a
Nothing
      Squash{}     -> forall a. a -> Maybe a
Just Doc
"@⊤"

instance Pretty (OpApp Expr) where
  pretty :: OpApp Expr -> Doc
pretty (Ordinary Expr
e) = forall a. Pretty a => a -> Doc
pretty Expr
e
  pretty (SyntaxBindingLambda Range
r List1 LamBinding
bs Expr
e) = 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) = 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          -> forall a. Pretty a => a -> Doc
pretty QName
x
            Lit Range
_ Literal
l          -> forall a. Pretty a => a -> Doc
pretty Literal
l
            QuestionMark Range
_ Maybe Int
n -> Doc
"?" forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty (String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Maybe Int
n
            Underscore Range
_ Maybe String
n   -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Underscore a => a
underscore String -> Doc
text Maybe String
n
            App Range
_ Expr
_ NamedArg Expr
_        ->
                case Expr -> AppView
appView Expr
e of
                    AppView Expr
e1 [NamedArg Expr]
args     ->
                        forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Expr
e1 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [NamedArg Expr]
args
--                      sep [ pretty e1
--                          , nest 2 $ fsep $ map pretty args
--                          ]
            RawApp Range
_ List2 Expr
es    -> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List2.toList List2 Expr
es
            OpApp Range
_ QName
q Set Name
_ OpAppArgs
es -> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall a.
Pretty a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp QName
q OpAppArgs
es

            WithApp Range
_ Expr
e [Expr]
es -> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$
              forall a. Pretty a => a -> Doc
pretty Expr
e forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"|" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) [Expr]
es

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

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

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

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

instance Pretty LamClause where
  pretty :: LamClause -> Doc
pretty (LamClause [Pattern]
ps RHS
rhs Bool
_) =
    forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Pattern]
ps)
        , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ 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. Pretty a => a -> Doc
pretty a
e
      pretty' RHS' a
AbsurdRHS = forall a. Null a => a
empty

instance Pretty BoundName where
  pretty :: BoundName -> Doc
pretty BName{ boundName :: BoundName -> Name
boundName = Name
x } = 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
  | forall a. LensHiding a => a -> Bool
visible NamedArg Binder
x              = forall a. Maybe a
Nothing  -- Ignore labels on visible arguments
  | Just String
l <- forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf NamedArg Binder
x = forall a. Bool -> a -> Maybe a
boolToMaybe (String
l forall a. Eq a => a -> a -> Bool
/= Name -> String
nameToRawName (BoundName -> Name
boundName forall a b. (a -> b) -> a -> b
$ forall a. Binder' a -> a
binderName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
x)) String
l
  | Bool
otherwise              = 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 = forall a. Pretty a => a -> Doc
pretty a
n in case Maybe Pattern
mpat of
    Maybe Pattern
Nothing  -> Doc
d
    Just Pattern
pat -> Doc
d Doc -> Doc -> Doc
<+> Doc
"@" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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 forall a b. (a -> b) -> a -> b
$
    if | Just String
l <- NamedArg Binder -> Maybe String
isLabeled NamedArg Binder
x -> String -> Doc
text String
l Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Binder
xb
       | Bool
otherwise             -> forall a. Pretty a => a -> Doc
pretty Binder
xb

    where

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

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

instance Pretty TypedBinding where
    pretty :: TypedBinding -> Doc
pretty (TLet Range
_ List1 Declaration
ds) = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ Doc
"let" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> Doc
pretty List1 Declaration
ds)
    pretty (TBind Range
_ List1 (NamedArg Binder)
xs (Underscore Range
_ Maybe String
Nothing)) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Pretty a => a -> Doc
pretty 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) = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep
      [ forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance NamedArg Binder
y
        forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding NamedArg Binder
y Doc -> Doc
parens
        forall a b. (a -> b) -> a -> b
$ BoundName -> Doc -> Doc
prettyFiniteness (forall a. Binder' a -> a
binderName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
y)
        forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion NamedArg Binder
y
        forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity NamedArg Binder
y
        forall a b. (a -> b) -> a -> b
$ BoundName -> Doc -> Doc
prettyTactic (forall a. Binder' a -> a
binderName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
y) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => a -> Doc
pretty 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. Pretty a => a -> Doc
pretty Expr
e ]
      | ys :: [NamedArg Binder]
ys@(NamedArg Binder
y : [NamedArg Binder]
_) <- [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds forall a b. (a -> b) -> a -> b
$ 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] forall a. a -> [a] -> [a]
: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
xs
          | Bool
otherwise   = (NamedArg Binder
x forall a. a -> [a] -> [a]
: [NamedArg Binder]
ys) forall a. a -> [a] -> [a]
: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
zs
          where ([NamedArg Binder]
ys, [NamedArg Binder]
zs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (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 = forall a. LensArgInfo a => a -> ArgInfo
getArgInfo a
x forall a. Eq a => a -> a -> Bool
== forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Binder
y Bool -> Bool -> 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)
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypedBinding -> Bool
isMeta Telescope
tel = Doc
forallQ Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty Telescope
tel)
      | Bool
otherwise      = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty Telescope
tel)
      where
        isMeta :: TypedBinding -> Bool
isMeta (TBind Range
_ List1 (NamedArg Binder)
_ (Underscore Range
_ Maybe String
Nothing)) = Bool
True
        isMeta TypedBinding
_ = Bool
False

smashTel :: Telescope -> Telescope
smashTel :: Telescope -> Telescope
smashTel (TBind Range
r List1 (NamedArg Binder)
xs Expr
e  :
          TBind Range
_ List1 (NamedArg Binder)
ys Expr
e' : Telescope
tel)
  | forall a. Pretty a => a -> String
prettyShow Expr
e forall a. Eq a => a -> a -> Bool
== forall a. Pretty a => a -> String
prettyShow Expr
e' = Telescope -> Telescope
smashTel (forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r (List1 (NamedArg Binder)
xs forall a. Semigroup a => a -> a -> a
Semigroup.<> List1 (NamedArg Binder)
ys) Expr
e forall a. a -> [a] -> [a]
: Telescope
tel)
smashTel (TypedBinding
b : Telescope
tel) = TypedBinding
b 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. Pretty a => a -> Doc
pretty Expr
e
    pretty RHS
AbsurdRHS = forall a. Null a => a
empty

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

instance Pretty LHS where
  pretty :: LHS -> Doc
pretty (LHS Pattern
p [RewriteEqn]
eqs [WithExpr]
es) = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
    [ forall a. Pretty a => a -> Doc
pretty Pattern
p
    , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null [RewriteEqn]
eqs then forall a. Null a => a
empty else forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [RewriteEqn]
eqs
    , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
prefixedThings Doc
"with" (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 = forall a. Pretty a => a -> Doc
pretty Arg Expr
wh in
      case Maybe Name
nm of
        Maybe Name
Nothing -> Doc
e
        Just Name
n  -> forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Doc
e

instance Pretty LHSCore where
  pretty :: LHSCore -> Doc
pretty (LHSHead QName
f [NamedArg Pattern]
ps) = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty QName
f forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps
  pretty (LHSProj QName
d [NamedArg Pattern]
ps NamedArg LHSCore
lhscore [NamedArg Pattern]
ps') = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep forall a b. (a -> b) -> a -> b
$
    forall a. Pretty a => a -> Doc
pretty QName
d forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps forall a. [a] -> [a] -> [a]
++
    Doc -> Doc
parens (forall a. Pretty a => a -> Doc
pretty NamedArg LHSCore
lhscore) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps'
  pretty (LHSWith LHSCore
h [Pattern]
wps [NamedArg Pattern]
ps) = if forall a. Null a => a -> Bool
null [NamedArg Pattern]
ps then Doc
doc else
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens Doc
doc forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) [NamedArg Pattern]
ps
    where
    doc :: Doc
doc = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty LHSCore
h forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"|" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty Telescope
bs) Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Expr
e
  pretty (RecordModuleInstance Range
_ QName
rec) = Doc
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
rec Doc -> Doc -> Doc
<+> Doc
"{{...}}"

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

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

        mkOverlap :: a -> Doc -> Doc
mkOverlap a
i Doc
d | forall a. LensHiding a => a -> Bool
isOverlappable a
i = Doc
"overlap" Doc -> Doc -> Doc
<+> Doc
d
                      | Bool
otherwise        = Doc
d
    Field Range
_ [Declaration]
fs ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"field"
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Declaration]
fs)
          ]
    FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
_ ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty LHS
lhs
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty RHS
rhs
          ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (forall a. Pretty a => a -> Doc
pretty WhereClause
wh)
    DataSig Range
_ Name
x [LamBinding]
tel Expr
e ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"data"
                  , forall a. Pretty a => a -> Doc
pretty Name
x
                  , [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                  [ Doc
":"
                  , forall a. Pretty a => a -> Doc
pretty Expr
e
                  ]
          ]
    Data Range
_ Name
x [LamBinding]
tel Expr
e [Declaration]
cs ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"data"
                  , forall a. Pretty a => a -> Doc
pretty Name
x
                  , [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                  [ Doc
":"
                  , forall a. Pretty a => a -> Doc
pretty Expr
e
                  , Doc
"where"
                  ]
          ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Declaration]
cs)
    DataDef Range
_ Name
x [LamBinding]
tel [Declaration]
cs ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"data"
                  , forall a. Pretty a => a -> Doc
pretty Name
x
                  , [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ Doc
"where"
          ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Declaration]
cs)
    RecordSig Range
_ Name
x [LamBinding]
tel Expr
e ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"record"
                  , forall a. Pretty a => a -> Doc
pretty Name
x
                  , [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                  ]
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                  [ Doc
":"
                  , forall a. Pretty a => a -> Doc
pretty Expr
e
                  ]
          ]
    Record Range
_ Name
x RecordDirectives
dir [LamBinding]
tel Expr
e [Declaration]
cs ->
      Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Doc
pRecord Name
x RecordDirectives
dir [LamBinding]
tel (forall a. a -> Maybe a
Just Expr
e) [Declaration]
cs
    RecordDef Range
_ Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs ->
      Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Doc
pRecord Name
x RecordDirectives
dir [LamBinding]
tel forall a. Maybe a
Nothing [Declaration]
cs
    RecordDirective RecordDirective
r -> RecordDirective -> Doc
pRecordDirective RecordDirective
r
    Infix Fixity
f List1 Name
xs  ->
      forall a. Pretty a => a -> Doc
pretty Fixity
f Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> Doc
pretty List1 Name
xs)
    Syntax Name
n Notation
xs -> Doc
"syntax" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
<+> Doc
"..."
    PatternSyn Range
_ Name
n [Arg Name]
as Pattern
p -> Doc
"pattern" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Arg Name]
as)
                             Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Pattern
p
    Mutual Range
_ [Declaration]
ds     -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"mutual" [Declaration]
ds
    InterleavedMutual Range
_ [Declaration]
ds  -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"interleaved mutual" [Declaration]
ds
    LoneConstructor Range
_ [Declaration]
ds -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"constructor" [Declaration]
ds
    Abstract Range
_ [Declaration]
ds   -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"abstract" [Declaration]
ds
    Private Range
_ Origin
_ [Declaration]
ds  -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"private" [Declaration]
ds
    InstanceB Range
_ [Declaration]
ds  -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"instance" [Declaration]
ds
    Macro Range
_ [Declaration]
ds      -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"macro" [Declaration]
ds
    Postulate Range
_ [Declaration]
ds  -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"postulate" [Declaration]
ds
    Primitive Range
_ [Declaration]
ds  -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"primitive" [Declaration]
ds
    Generalize Range
_ [Declaration]
ds -> forall {a}. Pretty a => String -> [a] -> Doc
namedBlock String
"variable" [Declaration]
ds
    Module Range
_ QName
x Telescope
tel [Declaration]
ds ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"module"
           , forall a. Pretty a => a -> Doc
pretty QName
x
           , [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty Telescope
tel)
           , Doc
"where"
           ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Declaration]
ds)
    ModuleMacro Range
_ Name
x (SectionApp Range
_ [] Expr
e) OpenShortHand
DoOpen ImportDirective
i | forall a. IsNoName a => a -> Bool
isNoName Name
x ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty OpenShortHand
DoOpen
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Expr
e
          , Int -> Doc -> Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty ImportDirective
i
          ]
    ModuleMacro Range
_ Name
x (SectionApp Range
_ Telescope
tel Expr
e) OpenShortHand
open ImportDirective
i ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty OpenShortHand
open Doc -> Doc -> Doc
<+> Doc
"module" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty Telescope
tel)
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ Doc
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Expr
e Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty ImportDirective
i
          ]
    ModuleMacro Range
_ Name
x (RecordModuleInstance Range
_ QName
rec) OpenShortHand
open ImportDirective
i ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty OpenShortHand
open Doc -> Doc -> Doc
<+> Doc
"module" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
x
          , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ Doc
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
rec Doc -> Doc -> Doc
<+> Doc
"{{...}}"
          ]
    Open Range
_ QName
x ImportDirective
i  -> forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"open", forall a. Pretty a => a -> Doc
pretty QName
x, forall a. Pretty a => a -> Doc
pretty ImportDirective
i ]
    Import Range
_ QName
x Maybe AsName
rn OpenShortHand
open ImportDirective
i   ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ forall a. Pretty a => a -> Doc
pretty OpenShortHand
open, Doc
"import", forall a. Pretty a => a -> Doc
pretty QName
x, forall {a}. Pretty a => Maybe (AsName' a) -> Doc
as Maybe AsName
rn, forall a. Pretty a => a -> Doc
pretty ImportDirective
i ]
      where
        as :: Maybe (AsName' a) -> Doc
as Maybe (AsName' a)
Nothing  = forall a. Null a => a
empty
        as (Just AsName' a
x) = Doc
"as" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty (forall a. AsName' a -> a
asName AsName' a
x)
    UnquoteDecl Range
_ [Name]
xs Expr
t ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"unquoteDecl" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Expr
t ]
    UnquoteDef Range
_ [Name]
xs Expr
t ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"unquoteDef" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Expr
t ]
    UnquoteData Range
_ Name
x [Name]
xs Expr
t ->
      forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"unquoteData" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Expr
t ]
    Pragma Pragma
pr   -> forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"{-#" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Pragma
pr, Doc
"#-}" ]
    where
      namedBlock :: String -> [a] -> Doc
namedBlock String
s [a]
ds =
          forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text String
s
              , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 -> forall a. Pretty a => a -> Doc
pretty (forall a. Ranged a -> a
rangedThing Ranged Induction
ind)
  Constructor Name
n IsInstance
inst -> forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
pInst, Doc
"constructor", forall a. Pretty a => a -> Doc
pretty Name
n ] where
    pInst :: Doc
pInst = case IsInstance
inst of
      InstanceDef{} -> Doc
"instance"
      NotInstanceDef{} -> forall a. Null a => a
empty
  Eta Ranged HasEta0
eta -> HasEta0 -> Doc
pHasEta0 (forall a. Ranged a -> a
rangedThing Ranged HasEta0
eta)
  PatternOrCopattern{} -> Doc
"pattern"

pRecord
  :: Name
  -> RecordDirectives
  -> [LamBinding]
  -> Maybe Expr
  -> [Declaration]
  -> Doc
pRecord :: Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Doc
pRecord Name
x (RecordDirectives Maybe (Ranged Induction)
ind Maybe HasEta0
eta Maybe Range
pat Maybe (Name, IsInstance)
con) [LamBinding]
tel Maybe Expr
me [Declaration]
ds = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
      [ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep  [ Doc
"record"
              , forall a. Pretty a => a -> Doc
pretty Name
x
              , [Doc] -> Doc
fcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
              ]
      , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall {a}. Pretty a => Maybe a -> Doc
pType Maybe Expr
me
      ]
    , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [Doc]
pInd
      , [Doc]
pEta
      , [Doc]
pPat
      , [Doc]
pCon
      , forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Declaration]
ds
      ]
    ]
  where pType :: Maybe a -> Doc
pType (Just a
e) = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
                [ Doc
":"
                , forall a. Pretty a => a -> Doc
pretty a
e
                , Doc
"where"
                ]
        pType Maybe a
Nothing  =
                  Doc
"where"
        pInd :: [Doc]
pInd = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ranged a -> a
rangedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged Induction)
ind
        pEta :: [Doc]
pEta = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ Maybe HasEta0
eta forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> HasEta0 -> Doc
pHasEta0
        pPat :: [Doc]
pPat = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ Doc
"pattern" 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 = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ ((Doc
"constructor" Doc -> Doc -> Doc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst 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 = forall a. Null a => a
empty

instance Pretty Pragma where
    pretty :: Pragma -> Doc
pretty (OptionsPragma Range
_ [String]
opts)  = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"OPTIONS" forall a. a -> [a] -> [a]
: [String]
opts
    pretty (BuiltinPragma Range
_ Ranged String
b QName
x)   = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"BUILTIN", String -> Doc
text (forall a. Ranged a -> a
rangedThing Ranged String
b), forall a. Pretty a => a -> Doc
pretty QName
x ]
    pretty (RewritePragma Range
_ Range
_ [QName]
xs)    =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"REWRITE", forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [QName]
xs ]
    pretty (CompilePragma Range
_ Ranged String
b QName
x String
e) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"COMPILE", String -> Doc
text (forall a. Ranged a -> a
rangedThing Ranged String
b), forall a. Pretty a => a -> Doc
pretty QName
x, String -> Doc
text String
e ]
    pretty (ForeignPragma Range
_ Ranged String
b String
s) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
"FOREIGN " forall a. [a] -> [a] -> [a]
++ forall a. Ranged a -> a
rangedThing Ranged String
b) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text (String -> [String]
lines String
s)
    pretty (StaticPragma Range
_ QName
i) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"STATIC", forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InjectivePragma Range
_ QName
i) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"INJECTIVE", forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InlinePragma Range
_ Bool
True QName
i) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"INLINE", forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (NotProjectionLikePragma Range
_ QName
i) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"NOT_PROJECTION_LIKE", forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InlinePragma Range
_ Bool
False QName
i) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"NOINLINE", forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (ImpossiblePragma Range
_ [String]
strs) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"IMPOSSIBLE"] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text [String]
strs
    pretty (EtaPragma Range
_ QName
x) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"ETA", forall a. Pretty a => a -> Doc
pretty QName
x]
    pretty (TerminationCheckPragma Range
_ TerminationCheck Name
tc) =
      case TerminationCheck Name
tc of
        TerminationCheck Name
TerminationCheck       -> 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 -> forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [Doc
"MEASURE", forall a. Pretty a => a -> Doc
pretty Name
x]
    pretty (NoCoverageCheckPragma Range
_) = Doc
"NON_COVERING"
    pretty (WarningOnUsage Range
_ QName
nm Text
str) = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"WARNING_ON_USAGE", forall a. Pretty a => a -> Doc
pretty QName
nm, String -> Doc
text (Text -> String
T.unpack Text
str) ]
    pretty (WarningOnImport Range
_ Text
str)   = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"WARNING_ON_IMPORT", String -> Doc
text (Text -> String
T.unpack Text
str) ]
    pretty (CatchallPragma Range
_) = Doc
"CATCHALL"
    pretty (DisplayPragma Range
_ Pattern
lhs Expr
rhs) = Doc
"DISPLAY" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => a -> Doc
pretty Pattern
lhs Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Expr
rhs ]
    pretty (NoPositivityCheckPragma Range
_) = Doc
"NO_POSITIVITY_CHECK"
    pretty (PolarityPragma Range
_ Name
q [Occurrence]
occs) =
      forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep (Doc
"POLARITY" forall a. a -> [a] -> [a]
: forall a. Pretty a => a -> Doc
pretty Name
q forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map 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  -> forall a. Null a => a
empty
    Related PrecedenceLevel
d  -> String -> Doc
text 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  -> forall a. Null a => a
empty
    Related{}  -> forall a. Pretty a => a -> Doc
pretty Associativity
ass Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty FixityLevel
level

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

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

instance Pretty Fixity' where
    pretty :: Fixity' -> Doc
pretty (Fixity' Fixity
fix Notation
nota Range
_range)
      | forall a. Null a => a -> Bool
null Notation
nota = forall a. Pretty a => a -> Doc
pretty Fixity
fix
      | Bool
otherwise = Doc
"syntax" Doc -> Doc -> 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) = forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding ArgInfo
ai Doc -> Doc
localParens forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p' a
e
      where p' :: Int
p' | forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = Int
p
               | Bool
otherwise  = Int
0
            localParens :: Doc -> Doc
localParens | forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai forall a. Eq a => a -> a -> Bool
== Origin
Substitution = Doc -> Doc
parens
                        | Bool
otherwise = 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 <- forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf Maybe NamedName
nm = Bool -> Doc -> Doc
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text String
s Doc -> Doc -> Doc
<+> Doc
"=", forall a. Pretty a => a -> Doc
pretty e
e ]
    | Bool
otherwise               = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p e
e

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

prettyOpApp :: forall a .
  Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp :: forall a.
Pretty a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp QName
q [NamedArg (MaybePlaceholder a)]
es = [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
merge [] forall a b. (a -> b) -> a -> b
$ [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Doc, Maybe PositionInName)]
prOp [Name]
ms [Item NameParts]
xs [NamedArg (MaybePlaceholder a)]
es
  where
    -- ms: the module part of the name.
    ms :: [Name]
ms = 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    -> forall l. IsList l => l -> [Item l]
List1.toList NameParts
xs
           NoName{}       -> 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 forall a. NamedArg a -> a
namedArg NamedArg (MaybePlaceholder a)
e of
        Placeholder PositionInName
p   -> (forall {a}. Pretty a => [a] -> Doc -> Doc
qual [Name]
ms forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty NamedArg (MaybePlaceholder a)
e, forall a. a -> Maybe a
Just PositionInName
p) forall a. a -> [a] -> [a]
: [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Doc, Maybe PositionInName)]
prOp [] [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
        NoPlaceholder{} -> (forall a. Pretty a => a -> Doc
pretty NamedArg (MaybePlaceholder a)
e, forall a. Maybe a
Nothing) 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]
_)  []       = forall a. HasCallStack => a
__IMPOSSIBLE__
    prOp [Name]
ms (Id String
x : [NamePart]
xs) [NamedArg (MaybePlaceholder a)]
es       = ( forall {a}. Pretty a => [a] -> Doc -> Doc
qual [Name]
ms forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ String -> Name
simpleName String
x
                                   , forall a. Maybe a
Nothing
                                   ) 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          = forall a b. (a -> b) -> [a] -> [b]
map (\NamedArg (MaybePlaceholder a)
e -> (forall a. Pretty a => a -> Doc
pretty NamedArg (MaybePlaceholder a)
e, forall a. Maybe a
Nothing)) [NamedArg (MaybePlaceholder a)]
es

    qual :: [a] -> Doc -> Doc
qual [a]
ms Doc
doc = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [a]
ms 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 []                            = 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 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 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 forall a. a -> [a] -> [a]
: [Doc]
bs) [(Doc, Maybe PositionInName)]
after
    merge [Doc]
before ((Doc
d, Just PositionInName
Middle)    : [(Doc, Maybe PositionInName)]
after) = case 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 =
      forall a. [a] -> [a]
reverse [Doc]
before 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 forall a. Semigroup a => a -> a -> a
<> Doc
a) 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 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 =
        forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall {a} {a}. (IsString a, Null a) => Maybe a -> a
public (forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective' a b
i)
            , forall a. Pretty a => a -> Doc
pretty forall a b. (a -> b) -> a -> b
$ forall n m. ImportDirective' n m -> Using' n m
using ImportDirective' a b
i
            , forall {a}. Pretty a => [a] -> Doc
prettyHiding forall a b. (a -> b) -> a -> b
$ forall n m. ImportDirective' n m -> HidingDirective' n m
hiding ImportDirective' a b
i
            , forall {a}. Pretty a => [a] -> Doc
rename forall a b. (a -> b) -> 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 = forall a. Null a => a
empty

            prettyHiding :: [a] -> Doc
prettyHiding [] = forall a. Null a => a
empty
            prettyHiding [a]
xs = Doc
"hiding" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
";" forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [a]
xs)

            rename :: [a] -> Doc
rename [] = forall a. Null a => a
empty
            rename [a]
xs = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"renaming"
                             , Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
";" forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 = forall a. Null a => a
empty
    pretty (Using [ImportedName' a b]
xs)    =
        Doc
"using" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
";" forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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) = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
      [ forall a. Pretty a => a -> Doc
pretty ImportedName' a b
from
      , Doc
"to"
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty forall a. Pretty a => a -> Doc
pretty Maybe Fixity
mfx
      , case ImportedName' a b
to of
          ImportedName a
a   -> forall a. Pretty a => a -> Doc
pretty a
a
          ImportedModule b
b -> 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) = forall a. Pretty a => a -> Doc
pretty a
a
    pretty (ImportedModule b
b) = Doc
"module" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty b
b