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


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

import Prelude hiding ( null )

import Data.IORef
import Data.Maybe
import qualified Data.Strict.Maybe as Strict

import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Position

import Agda.Interaction.Options.IORefs (UnicodeOrAscii(..), unicodeOrAscii)

import Agda.Utils.Float (toStringWithoutDotZero)
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String

import Agda.Utils.Impossible

import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)

-- Andreas, 2017-10-02, TODO: restore Show to its original purpose
--
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

-- instance Show Expr            where show = show . pretty
-- instance Show Declaration     where show = show . pretty
-- instance Show Pattern         where show = show . pretty
-- instance Show TypedBinding    where show = show . pretty
-- instance Show LamBinding      where show = show . pretty
-- instance (Pretty a, Pretty b) => Show (ImportDirective' a b)
--                               where show = show . pretty
-- instance Show Pragma          where show = show . pretty
-- instance Show RHS             where show = show . pretty
-- instance Show LHS where show = show . pretty
-- instance Show LHSCore where show = show . pretty
-- instance Show WhereClause where show = show . pretty
-- instance Show ModuleApplication where show = show . pretty


-- | Picking the appropriate set of special characters depending on
-- whether we are allowed to use unicode or have to limit ourselves
-- to ascii.

data SpecialCharacters = SpecialCharacters
  { SpecialCharacters -> Doc -> Doc
_dbraces :: Doc -> Doc
  , SpecialCharacters -> Doc
_lambda  :: Doc
  , SpecialCharacters -> Doc
_arrow   :: Doc
  , SpecialCharacters -> Doc
_forallQ :: Doc
  , SpecialCharacters -> Doc
_leftIdiomBrkt  :: Doc
  , SpecialCharacters -> Doc
_rightIdiomBrkt :: Doc
  , SpecialCharacters -> Doc
_emptyIdiomBrkt :: Doc
  }

{-# NOINLINE specialCharacters #-}
specialCharacters :: SpecialCharacters
specialCharacters :: SpecialCharacters
specialCharacters =
  let opt :: UnicodeOrAscii
opt = IO UnicodeOrAscii -> UnicodeOrAscii
forall a. IO a -> a
UNSAFE.unsafePerformIO (IORef UnicodeOrAscii -> IO UnicodeOrAscii
forall a. IORef a -> IO a
readIORef IORef UnicodeOrAscii
unicodeOrAscii) in
  case UnicodeOrAscii
opt of
    UnicodeOrAscii
UnicodeOk -> SpecialCharacters :: (Doc -> Doc)
-> Doc -> Doc -> Doc -> Doc -> Doc -> Doc -> SpecialCharacters
SpecialCharacters { _dbraces :: Doc -> Doc
_dbraces = ((Doc
"\x2983 " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>) (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" \x2984"))
                                   , _lambda :: Doc
_lambda  = Doc
"\x03bb"
                                   , _arrow :: Doc
_arrow   = Doc
"\x2192"
                                   , _forallQ :: Doc
_forallQ = Doc
"\x2200"
                                   , _leftIdiomBrkt :: Doc
_leftIdiomBrkt  = Doc
"\x2987"
                                   , _rightIdiomBrkt :: Doc
_rightIdiomBrkt = Doc
"\x2988"
                                   , _emptyIdiomBrkt :: Doc
_emptyIdiomBrkt = Doc
"\x2987\x2988"
                                   }
    UnicodeOrAscii
AsciiOnly -> SpecialCharacters :: (Doc -> Doc)
-> Doc -> Doc -> Doc -> Doc -> Doc -> Doc -> SpecialCharacters
SpecialCharacters { _dbraces :: Doc -> Doc
_dbraces = Doc -> Doc
braces (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
braces'
                                   , _lambda :: Doc
_lambda  = Doc
"\\"
                                   , _arrow :: Doc
_arrow   = Doc
"->"
                                   , _forallQ :: Doc
_forallQ = Doc
"forall"
                                   , _leftIdiomBrkt :: Doc
_leftIdiomBrkt  = Doc
"(|"
                                   , _rightIdiomBrkt :: Doc
_rightIdiomBrkt = Doc
"|)"
                                   , _emptyIdiomBrkt :: Doc
_emptyIdiomBrkt = Doc
"(|)"
                                   }

braces' :: Doc -> Doc
braces' :: Doc -> Doc
braces' Doc
d = String -> Doc -> (String -> Doc) -> Doc
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Doc -> String
render Doc
d) (Doc -> Doc
braces Doc
d) {-else-} ((String -> Doc) -> Doc) -> (String -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \ String
s ->
  Doc -> Doc
braces (Char -> Doc
forall p. (IsString p, Null p) => Char -> p
spaceIfDash (String -> Char
forall a. [a] -> a
head String
s) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Char -> Doc
forall p. (IsString p, Null p) => Char -> p
spaceIfDash (String -> Char
forall a. [a] -> a
last String
s))
  -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
  -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
  where
  spaceIfDash :: Char -> p
spaceIfDash Char
'-' = p
" "
  spaceIfDash Char
_   = p
forall a. Null a => a
empty

-- double braces...
dbraces :: Doc -> Doc
dbraces :: Doc -> Doc
dbraces = SpecialCharacters -> Doc -> Doc
_dbraces SpecialCharacters
specialCharacters

-- forall quantifier
forallQ :: Doc
forallQ :: Doc
forallQ = SpecialCharacters -> Doc
_forallQ SpecialCharacters
specialCharacters

-- left, right, and empty idiom bracket
leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Doc
leftIdiomBrkt :: Doc
leftIdiomBrkt  = SpecialCharacters -> Doc
_leftIdiomBrkt  SpecialCharacters
specialCharacters
rightIdiomBrkt :: Doc
rightIdiomBrkt = SpecialCharacters -> Doc
_rightIdiomBrkt SpecialCharacters
specialCharacters
emptyIdiomBrkt :: Doc
emptyIdiomBrkt = SpecialCharacters -> Doc
_emptyIdiomBrkt SpecialCharacters
specialCharacters

-- 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 :: [Doc] -> Doc
bracesAndSemicolons :: [Doc] -> Doc
bracesAndSemicolons []       = Doc
"{}"
bracesAndSemicolons (Doc
d : [Doc]
ds) =
  [Doc] -> Doc
sep ([Doc
"{" Doc -> Doc -> Doc
<+> Doc
d] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc
";" Doc -> Doc -> Doc
<+>) [Doc]
ds [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
"}"])

arrow, lambda :: Doc
arrow :: Doc
arrow  = SpecialCharacters -> Doc
_arrow SpecialCharacters
specialCharacters
lambda :: Doc
lambda = SpecialCharacters -> Doc
_lambda SpecialCharacters
specialCharacters

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Pretty (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 [LamBinding]
bs Expr
e) = Expr -> Doc
forall a. Pretty a => a -> Doc
pretty (Range -> [LamBinding] -> Expr -> Expr
Lam Range
r [LamBinding]
bs Expr
e)

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

instance Pretty Expr where
    pretty :: Expr -> Doc
pretty Expr
e =
        case Expr
e of
            Ident QName
x          -> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
            Lit Literal
l            -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
            QuestionMark Range
_ Maybe Int
n -> Doc
"?" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (Int -> Doc) -> Maybe Int -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty (String -> Doc
text (String -> Doc) -> (Int -> String) -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) Maybe Int
n
            Underscore Range
_ Maybe String
n   -> Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Underscore a => a
underscore String -> Doc
text Maybe String
n
            App Range
_ Expr
_ NamedArg Expr
_        ->
                case Expr -> AppView
appView Expr
e of
                    AppView Expr
e1 [NamedArg Expr]
args     ->
                        [Doc] -> Doc
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
_ [Expr]
es    -> [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]
es
            OpApp Range
_ QName
q Set Name
_ [NamedArg (MaybePlaceholder (OpApp Expr))]
es -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg (MaybePlaceholder (OpApp Expr))] -> [Doc]
forall a.
Pretty a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp QName
q [NamedArg (MaybePlaceholder (OpApp Expr))]
es

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

            HiddenArg Range
_ Named_ Expr
e -> Doc -> Doc
braces' (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Named_ Expr
e
            InstanceArg Range
_ Named_ Expr
e -> Doc -> Doc
dbraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Named_ Expr
e
            Lam Range
_ [LamBinding]
bs (AbsurdLam Range
_ Hiding
h) -> Doc
lambda Doc -> Doc -> Doc
<+> [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]
bs) Doc -> Doc -> Doc
<+> Hiding -> Doc
forall p. IsString p => Hiding -> p
absurd Hiding
h
            Lam Range
_ [LamBinding]
bs Expr
e ->
                [Doc] -> Doc
sep [ Doc
lambda Doc -> Doc -> Doc
<+> [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]
bs) Doc -> Doc -> Doc
<+> Doc
arrow
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                    ]
            AbsurdLam Range
_ Hiding
h -> Doc
lambda Doc -> Doc -> Doc
<+> Hiding -> Doc
forall p. IsString p => Hiding -> p
absurd Hiding
h
            ExtendedLam Range
_ [LamClause]
pes -> Doc
lambda Doc -> Doc -> Doc
<+> [Doc] -> Doc
bracesAndSemicolons ((LamClause -> Doc) -> [LamClause] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamClause -> Doc
forall a. Pretty a => a -> Doc
pretty [LamClause]
pes)
            Fun Range
_ Arg Expr
e1 Expr
e2 ->
                [Doc] -> Doc
sep [ Arg Expr -> Doc -> Doc
forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion Arg Expr
e1 (Arg Expr -> Doc -> Doc
forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity Arg Expr
e1 (Arg Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Arg Expr
e1)) Doc -> Doc -> Doc
<+> Doc
arrow
                    , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e2
                    ]
            Pi [TypedBinding]
tel Expr
e ->
                [Doc] -> Doc
sep [ Tel -> Doc
forall a. Pretty a => a -> Doc
pretty ([TypedBinding] -> Tel
Tel ([TypedBinding] -> Tel) -> [TypedBinding] -> Tel
forall a b. (a -> b) -> a -> b
$ [TypedBinding] -> [TypedBinding]
smashTel [TypedBinding]
tel) Doc -> Doc -> Doc
<+> Doc
arrow
                    , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                    ]
            Set Range
_   -> Doc
"Set"
            Prop Range
_  -> Doc
"Prop"
            SetN Range
_ Integer
n    -> Doc
"Set" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (Integer -> String
forall i. (Show i, Integral i) => i -> String
showIndex Integer
n)
            PropN Range
_ Integer
n   -> Doc
"Prop" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (Integer -> String
forall i. (Show i, Integral i) => i -> String
showIndex Integer
n)
            Let Range
_ [Declaration]
ds TacticAttribute
me  ->
                [Doc] -> Doc
sep [ Doc
"let" Doc -> Doc -> Doc
<+> [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]
ds)
                    , Doc -> (Expr -> Doc) -> TacticAttribute -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty (\ Expr
e -> Doc
"in" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e) TacticAttribute
me
                    ]
            Paren Range
_ Expr
e -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
            IdiomBrackets Range
_ [Expr]
es ->
              case [Expr]
es of
                []   -> Doc
emptyIdiomBrkt
                [Expr
e]  -> Doc
leftIdiomBrkt Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e Doc -> Doc -> Doc
<+> Doc
rightIdiomBrkt
                Expr
e:[Expr]
es -> Doc
leftIdiomBrkt Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"|" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (Expr -> Doc) -> Expr -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Doc
forall a. Pretty a => a -> Doc
pretty) [Expr]
es) Doc -> Doc -> Doc
<+> Doc
rightIdiomBrkt
            DoBlock Range
_ [DoStmt]
ss -> Doc
"do" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat ((DoStmt -> Doc) -> [DoStmt] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DoStmt -> Doc
forall a. Pretty a => a -> Doc
pretty [DoStmt]
ss)
            As Range
_ Name
x Expr
e  -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
            Dot Range
_ Expr
e   -> Doc
"." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
            DoubleDot Range
_ Expr
e  -> Doc
".." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
            Absurd Range
_  -> Doc
"()"
            Rec Range
_ RecordAssignments
xs  -> [Doc] -> Doc
sep [Doc
"record", [Doc] -> Doc
bracesAndSemicolons ((RecordAssignment -> Doc) -> RecordAssignments -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map RecordAssignment -> Doc
forall a. Pretty a => a -> Doc
pretty RecordAssignments
xs)]
            RecUpdate Range
_ Expr
e [FieldAssignment]
xs ->
              [Doc] -> Doc
sep [Doc
"record" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e, [Doc] -> Doc
bracesAndSemicolons ((FieldAssignment -> Doc) -> [FieldAssignment] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FieldAssignment -> Doc
forall a. Pretty a => a -> Doc
pretty [FieldAssignment]
xs)]
            ETel []  -> Doc
"()"
            ETel [TypedBinding]
tel -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
tel
            Quote Range
_ -> Doc
"quote"
            QuoteTerm Range
_ -> Doc
"quoteTerm"
            Unquote Range
_  -> Doc
"unquote"
            Tactic Range
_ Expr
t -> Doc
"tactic" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t
            -- Andreas, 2011-10-03 print irrelevant things as .(e)
            DontCare Expr
e -> Doc
"." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e)
            Equal Range
_ Expr
a Expr
b -> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
a Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
b
            Ellipsis Range
_  -> Doc
"..."
            Generalized Expr
e -> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
        where
          absurd :: Hiding -> p
absurd Hiding
NotHidden  = p
"()"
          absurd Instance{} = p
"{{}}"
          absurd Hiding
Hidden     = p
"{}"

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

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

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

instance Pretty LamClause where
  pretty :: LamClause -> Doc
pretty (LamClause LHS
lhs RHS
rhs WhereClause
wh Bool
_) =
    [Doc] -> Doc
sep [ LHS -> Doc
forall a. Pretty a => a -> Doc
pretty LHS
lhs
        , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ RHS -> Doc
forall a. Pretty a => RHS' a -> Doc
pretty' RHS
rhs
        ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (WhereClause -> Doc
forall a. Pretty a => a -> Doc
pretty WhereClause
wh)
    where
      pretty' :: RHS' a -> Doc
pretty' (RHS a
e)   = Doc
arrow Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e
      pretty' RHS' a
AbsurdRHS = Doc
forall a. Null a => a
empty

instance Pretty BoundName where
  pretty :: BoundName -> Doc
pretty BName{ boundName :: BoundName -> Name
boundName = Name
x } = Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x

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

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

instance Pretty a => Pretty (Binder' a) where
  pretty :: Binder' a -> Doc
pretty (Binder Maybe Pattern
mpat a
n) = let d :: Doc
d = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
n in case Maybe Pattern
mpat of
    Maybe Pattern
Nothing  -> Doc
d
    Just Pattern
pat -> Doc
d Doc -> Doc -> Doc
<+> Doc
"@" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
pat)

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

    where

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

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

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

newtype Tel = Tel Telescope

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

smashTel :: Telescope -> Telescope
smashTel :: [TypedBinding] -> [TypedBinding]
smashTel (TBind Range
r [NamedArg Binder]
xs Expr
e  :
          TBind Range
_ [NamedArg Binder]
ys Expr
e' : [TypedBinding]
tel)
  | Expr -> String
forall a. Show a => a -> String
show Expr
e String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> String
forall a. Show a => a -> String
show Expr
e' = [TypedBinding] -> [TypedBinding]
smashTel (Range -> [NamedArg Binder] -> Expr -> TypedBinding
forall e. Range -> [NamedArg Binder] -> e -> TypedBinding' e
TBind Range
r ([NamedArg Binder]
xs [NamedArg Binder] -> [NamedArg Binder] -> [NamedArg Binder]
forall a. [a] -> [a] -> [a]
++ [NamedArg Binder]
ys) Expr
e TypedBinding -> [TypedBinding] -> [TypedBinding]
forall a. a -> [a] -> [a]
: [TypedBinding]
tel)
smashTel (TypedBinding
b : [TypedBinding]
tel) = TypedBinding
b TypedBinding -> [TypedBinding] -> [TypedBinding]
forall a. a -> [a] -> [a]
: [TypedBinding] -> [TypedBinding]
smashTel [TypedBinding]
tel
smashTel [] = []


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

instance Pretty WhereClause where
  pretty :: WhereClause -> Doc
pretty  WhereClause
NoWhere = Doc
forall a. Null a => a
empty
  pretty (AnyWhere [Module Range
_ QName
x [] [Declaration]
ds]) | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName (QName -> Name
unqualify QName
x)
                       = [Doc] -> Doc
vcat [ Doc
"where", Int -> Doc -> Doc
nest Int
2 ([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 [Declaration]
ds) = [Doc] -> Doc
vcat [ Doc
"where", Int -> Doc -> Doc
nest Int
2 ([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 Name
m Access
a [Declaration]
ds) =
    [Doc] -> Doc
vcat [ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a. Bool -> (a -> a) -> a -> a
applyWhen (Access
a Access -> Access -> Bool
forall a. Eq a => a -> a -> Bool
== Origin -> Access
PrivateAccess Origin
UserWritten) (Doc
"private" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:)
             [ Doc
"module", Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
m, Doc
"where" ]
         , Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
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 [WithHiding Expr]
es ExpandedEllipsis
ell) = [Doc] -> Doc
sep
    [ Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ if [RewriteEqn] -> Bool
forall a. Null a => a -> Bool
null [RewriteEqn]
eqs then Doc
forall a. Null a => a
empty else [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (RewriteEqn -> Doc) -> [RewriteEqn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map RewriteEqn -> Doc
forall a. Pretty a => a -> Doc
pretty [RewriteEqn]
eqs
    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
prefixedThings Doc
"with" ((WithHiding Expr -> Doc) -> [WithHiding Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [WithHiding Expr]
es)
    ]

instance Pretty LHSCore where
  pretty :: LHSCore -> Doc
pretty (LHSHead QName
f [NamedArg Pattern]
ps) = [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
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
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
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ LHSCore -> Doc
forall a. Pretty a => a -> Doc
pretty LHSCore
h Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Pattern -> Doc) -> [Pattern] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"|" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (Pattern -> Doc) -> Pattern -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty) [Pattern]
wps

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

instance Pretty DoStmt where
  pretty :: DoStmt -> Doc
pretty (DoBind Range
_ Pattern
p Expr
e [LamClause]
cs) =
    ((Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p Doc -> Doc -> Doc
<+> Doc
"←") Doc -> Doc -> Doc
<?> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e) Doc -> Doc -> Doc
<?> [LamClause] -> Doc
forall a. Pretty a => [a] -> Doc
prCs [LamClause]
cs
    where
      prCs :: [a] -> Doc
prCs [] = Doc
forall a. Null a => a
empty
      prCs [a]
cs = Doc
"where" Doc -> Doc -> Doc
<?> [Doc] -> Doc
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
_ [Declaration]
ds) = Doc
"let" Doc -> Doc -> Doc
<+> [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]
ds)

instance Pretty Declaration where
    prettyList :: [Declaration] -> Doc
prettyList = [Doc] -> Doc
vcat ([Doc] -> Doc) -> ([Declaration] -> [Doc]) -> [Declaration] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty
    pretty :: Declaration -> Doc
pretty Declaration
d =
        case Declaration
d of
            TypeSig ArgInfo
i TacticAttribute
tac Name
x Expr
e ->
                [Doc] -> Doc
sep [ TacticAttribute -> Doc -> Doc
prettyTactic' TacticAttribute
tac (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
":"
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                    ]

            FieldSig IsInstance
inst TacticAttribute
tac Name
x (Arg ArgInfo
i Expr
e) ->
                IsInstance -> Doc -> Doc
mkInst IsInstance
inst (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensHiding a => a -> Doc -> Doc
mkOverlap ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                ArgInfo -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding ArgInfo
i Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensCohesion a => a -> Doc -> Doc
prettyCohesion ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Doc -> Doc
forall a. LensQuantity a => a -> Doc -> Doc
prettyQuantity ArgInfo
i (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty (Declaration -> Doc) -> Declaration -> Doc
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Relevant ArgInfo
i) TacticAttribute
tac Name
x Expr
e

                where

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

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

            Field Range
_ [Declaration]
fs ->
              [Doc] -> Doc
sep [ Doc
"field"
                  , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [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
sep [ LHS -> Doc
forall a. Pretty a => a -> Doc
pretty LHS
lhs
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ RHS -> Doc
forall a. Pretty a => a -> Doc
pretty RHS
rhs
                    ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (WhereClause -> Doc
forall a. Pretty a => a -> Doc
pretty WhereClause
wh)
            DataSig Range
_ Name
x [LamBinding]
tel Expr
e ->
                [Doc] -> Doc
sep [ [Doc] -> Doc
hsep  [ Doc
"data"
                            , Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
                            , [Doc] -> Doc
fcat ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                            ]
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
                            [ Doc
":"
                            , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                            ]
                    ]
            Data Range
_ Name
x [LamBinding]
tel Expr
e [Declaration]
cs ->
                [Doc] -> Doc
sep [ [Doc] -> Doc
hsep  [ Doc
"data"
                            , Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
                            , [Doc] -> Doc
fcat ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                            ]
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
                            [ Doc
":"
                            , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                            , Doc
"where"
                            ]
                    ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
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
sep [ [Doc] -> Doc
hsep  [ Doc
"data"
                            , Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
                            , [Doc] -> Doc
fcat ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                            ]
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"where"
                    ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
cs)
            RecordSig Range
_ Name
x [LamBinding]
tel Expr
e ->
                [Doc] -> Doc
sep [ [Doc] -> Doc
hsep  [ Doc
"record"
                            , Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
                            , [Doc] -> Doc
fcat ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
                            ]
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
                            [ Doc
":"
                            , Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                            ]
                    ]
            Record Range
_ Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding]
tel Expr
e [Declaration]
cs ->
              Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding]
tel (Expr -> TacticAttribute
forall a. a -> Maybe a
Just Expr
e) [Declaration]
cs
            RecordDef Range
_ Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding]
tel [Declaration]
cs ->
              Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding]
tel TacticAttribute
forall a. Maybe a
Nothing [Declaration]
cs
            Infix Fixity
f [Name]
xs  ->
                Fixity -> Doc
forall a. Pretty a => a -> Doc
pretty Fixity
f Doc -> Doc -> Doc
<+> ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs)
            Syntax Name
n Notation
xs -> Doc
"syntax" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
<+> Doc
"..."
            PatternSyn Range
_ Name
n [Arg Name]
as Pattern
p -> Doc
"pattern" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Arg Name -> Doc) -> [Arg Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Arg Name]
as)
                                     Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
            Mutual Range
_ [Declaration]
ds     -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"mutual" [Declaration]
ds
            Abstract Range
_ [Declaration]
ds   -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"abstract" [Declaration]
ds
            Private Range
_ Origin
_ [Declaration]
ds  -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"private" [Declaration]
ds
            InstanceB Range
_ [Declaration]
ds  -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"instance" [Declaration]
ds
            Macro Range
_ [Declaration]
ds      -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"macro" [Declaration]
ds
            Postulate Range
_ [Declaration]
ds  -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"postulate" [Declaration]
ds
            Primitive Range
_ [Declaration]
ds  -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"primitive" [Declaration]
ds
            Generalize Range
_ [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock String
"variable" [Declaration]
ds
            Module Range
_ QName
x [TypedBinding]
tel [Declaration]
ds ->
                [Doc] -> Doc
hsep [ Doc
"module"
                     , QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
                     , [Doc] -> Doc
fcat ((TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
tel)
                     , Doc
"where"
                     ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
ds)
            ModuleMacro Range
_ Name
x (SectionApp Range
_ [] Expr
e) OpenShortHand
DoOpen ImportDirective
i | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x ->
                [Doc] -> Doc
sep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
DoOpen
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
                    , Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i
                    ]
            ModuleMacro Range
_ Name
x (SectionApp Range
_ [TypedBinding]
tel Expr
e) OpenShortHand
open ImportDirective
i ->
                [Doc] -> Doc
sep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open Doc -> Doc -> Doc
<+> Doc
"module" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> [Doc] -> Doc
fcat ((TypedBinding -> Doc) -> [TypedBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding]
tel)
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e Doc -> Doc -> Doc
<+> ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i
                    ]
            ModuleMacro Range
_ Name
x (RecordModuleInstance Range
_ QName
rec) OpenShortHand
open ImportDirective
i ->
                [Doc] -> Doc
sep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open Doc -> Doc -> Doc
<+> Doc
"module" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"=" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
rec Doc -> Doc -> Doc
<+> Doc
"{{...}}"
                    ]
            Open Range
_ QName
x ImportDirective
i  -> [Doc] -> Doc
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
hsep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open, Doc
"import", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, Maybe AsName -> Doc
forall a. Pretty a => Maybe (AsName' a) -> Doc
as Maybe AsName
rn, ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i ]
                where
                    as :: Maybe (AsName' a) -> Doc
as Maybe (AsName' a)
Nothing  = Doc
forall a. Null a => a
empty
                    as (Just AsName' a
x) = Doc
"as" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty (AsName' a -> a
forall a. AsName' a -> a
asName AsName' a
x)
            UnquoteDecl Range
_ [Name]
xs Expr
t ->
              [Doc] -> Doc
sep [ Doc
"unquoteDecl" Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
            UnquoteDef Range
_ [Name]
xs Expr
t ->
              [Doc] -> Doc
sep [ Doc
"unquoteDef" Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs) Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
            Pragma Pragma
pr   -> [Doc] -> Doc
sep [ Doc
"{-#" Doc -> Doc -> Doc
<+> Pragma -> Doc
forall a. Pretty a => a -> Doc
pretty Pragma
pr, Doc
"#-}" ]
        where
            namedBlock :: String -> [a] -> Doc
namedBlock String
s [a]
ds =
                [Doc] -> Doc
sep [ String -> Doc
text String
s
                    , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
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
                    ]

pRecord :: Name -> Maybe (Ranged Induction) -> Maybe HasEta -> Maybe (Name, IsInstance) -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc
pRecord :: Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding]
tel TacticAttribute
me [Declaration]
cs =
  [Doc] -> Doc
sep [ [Doc] -> Doc
hsep  [ Doc
"record"
              , Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
              , [Doc] -> Doc
fcat ((LamBinding -> Doc) -> [LamBinding] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding]
tel)
              ]
      , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TacticAttribute -> Doc
forall a. Pretty a => Maybe a -> Doc
pType TacticAttribute
me
      ] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc]
pInd [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                          [Doc]
pEta [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                          [Doc]
pCon [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                          (Declaration -> Doc) -> [Declaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Doc
forall a. Pretty a => a -> Doc
pretty [Declaration]
cs)
  where pType :: Maybe a -> Doc
pType (Just a
e) = [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
$ String -> Doc
text (String -> Doc)
-> (Ranged Induction -> String) -> Ranged Induction -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Induction -> String
forall a. Show a => a -> String
show (Induction -> String)
-> (Ranged Induction -> Induction) -> Ranged Induction -> String
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 HasEta
eta Maybe HasEta -> (HasEta -> Doc) -> Maybe Doc
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
          HasEta
YesEta -> Doc
"eta-equality"
          HasEta
NoEta  -> Doc
"no-eta-equality"
        pCon :: [Doc]
pCon = Maybe Doc -> [Doc]
forall a. Maybe a -> [a]
maybeToList (Maybe Doc -> [Doc]) -> Maybe Doc -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Doc
"constructor" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty) (Name -> Doc)
-> ((Name, IsInstance) -> Name) -> (Name, IsInstance) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, IsInstance) -> Name
forall a b. (a, b) -> a
fst ((Name, IsInstance) -> Doc)
-> Maybe (Name, IsInstance) -> Maybe Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Name, IsInstance)
con

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

instance Pretty Pragma where
    pretty :: Pragma -> Doc
pretty (OptionsPragma Range
_ [String]
opts)  = [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String
"OPTIONS" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
opts
    pretty (BuiltinPragma Range
_ RString
b QName
x)   = [Doc] -> Doc
hsep [ Doc
"BUILTIN", String -> Doc
text (RString -> String
forall a. Ranged a -> a
rangedThing RString
b), QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x ]
    pretty (RewritePragma Range
_ Range
_ [QName]
xs)    =
      [Doc] -> Doc
hsep [ Doc
"REWRITE", [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (QName -> Doc) -> [QName] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Doc
forall a. Pretty a => a -> Doc
pretty [QName]
xs ]
    pretty (CompilePragma Range
_ RString
b QName
x String
e) =
      [Doc] -> Doc
hsep [ Doc
"COMPILE", String -> Doc
text (RString -> String
forall a. Ranged a -> a
rangedThing RString
b), QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, String -> Doc
text String
e ]
    pretty (ForeignPragma Range
_ RString
b String
s) =
      [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
"FOREIGN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RString -> String
forall a. Ranged a -> a
rangedThing RString
b) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text (String -> [String]
lines String
s)
    pretty (StaticPragma Range
_ QName
i) =
      [Doc] -> Doc
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
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
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"INLINE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
    pretty (InlinePragma Range
_ Bool
False QName
i) =
      [Doc] -> Doc
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
_) =
      [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"IMPOSSIBLE"]
    pretty (EtaPragma Range
_ QName
x) =
      [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
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 String
str) = [Doc] -> Doc
hsep [ Doc
"WARNING_ON_USAGE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
nm, String -> Doc
text String
str ]
    pretty (WarningOnImport Range
_ String
str)   = [Doc] -> Doc
hsep [ Doc
"WARNING_ON_IMPORT", String -> Doc
text String
str ]
    pretty (CatchallPragma Range
_) = Doc
"CATCHALL"
    pretty (DisplayPragma Range
_ Pattern
lhs Expr
rhs) = Doc
"DISPLAY" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [ Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
lhs Doc -> Doc -> Doc
<+> Doc
"=", Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
rhs ]
    pretty (NoPositivityCheckPragma Range
_) = Doc
"NO_POSITIVITY_CHECK"
    pretty (PolarityPragma Range
_ Name
q [Occurrence]
occs) =
      [Doc] -> Doc
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 Fixity where
    pretty :: Fixity -> Doc
pretty (Fixity Range
_ FixityLevel
Unrelated   Associativity
_)   = Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
    pretty (Fixity Range
_ (Related PrecedenceLevel
d) Associativity
ass) = Doc
s Doc -> Doc -> Doc
<+> String -> Doc
text (PrecedenceLevel -> String
toStringWithoutDotZero PrecedenceLevel
d)
      where
      s :: Doc
s = case Associativity
ass of
            Associativity
LeftAssoc  -> Doc
"infixl"
            Associativity
RightAssoc -> Doc
"infixr"
            Associativity
NonAssoc   -> Doc
"infix"

instance Pretty GenPart where
    pretty :: GenPart -> Doc
pretty (IdPart RString
x)   = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ RString -> String
forall a. Ranged a -> a
rangedThing RString
x
    pretty BindHole{}   = Doc
forall a. Underscore a => a
underscore
    pretty NormalHole{} = Doc
forall a. Underscore a => a
underscore
    pretty WildHole{}   = Doc
forall a. Underscore a => a
underscore

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

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

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

instance Pretty e => Pretty (Named_ e) where
  prettyPrec :: Int -> Named_ e -> Doc
prettyPrec Int
p (Named Maybe NamedName
nm e
e)
    | Just String
s <- Maybe NamedName -> Maybe String
forall a. LensNamed NamedName a => 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
sep [ String -> Doc
text String
s Doc -> Doc -> Doc
<+> Doc
"=", e -> Doc
forall a. Pretty a => a -> Doc
pretty e
e ]
    | Bool
otherwise               = Int -> e -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p e
e

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

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

    prOp :: [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
    prOp :: [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Doc, Maybe PositionInName)]
prOp [Name]
ms (NamePart
Hole : [NamePart]
xs) (NamedArg (MaybePlaceholder a)
e : [NamedArg (MaybePlaceholder a)]
es) =
      case NamedArg (MaybePlaceholder a) -> MaybePlaceholder a
forall a. NamedArg a -> a
namedArg NamedArg (MaybePlaceholder a)
e of
        Placeholder PositionInName
p   -> ([Name] -> Doc -> Doc
forall a. Pretty a => [a] -> Doc -> Doc
qual [Name]
ms (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ NamedArg (MaybePlaceholder a) -> Doc
forall a. Pretty a => a -> Doc
pretty NamedArg (MaybePlaceholder a)
e, PositionInName -> Maybe PositionInName
forall a. a -> Maybe a
Just PositionInName
p) (Doc, Maybe PositionInName)
-> [(Doc, Maybe PositionInName)] -> [(Doc, Maybe PositionInName)]
forall a. a -> [a] -> [a]
: [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Doc, Maybe PositionInName)]
prOp [] [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
        NoPlaceholder{} -> (NamedArg (MaybePlaceholder a) -> Doc
forall a. Pretty a => a -> Doc
pretty NamedArg (MaybePlaceholder a)
e, Maybe PositionInName
forall a. Maybe a
Nothing) (Doc, Maybe PositionInName)
-> [(Doc, Maybe PositionInName)] -> [(Doc, Maybe PositionInName)]
forall a. a -> [a] -> [a]
: [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Doc, Maybe PositionInName)]
prOp [Name]
ms [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
          -- Module qualifier needs to go on section holes (#3072)
    prOp [Name]
_  (NamePart
Hole : [NamePart]
_)  []       = [(Doc, Maybe PositionInName)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    prOp [Name]
ms (Id String
x : [NamePart]
xs) [NamedArg (MaybePlaceholder a)]
es       = ( [Name] -> Doc -> Doc
forall a. Pretty a => [a] -> Doc -> Doc
qual [Name]
ms (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope ([NamePart] -> Name) -> [NamePart] -> Name
forall a b. (a -> b) -> a -> b
$ [String -> NamePart
Id 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
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [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
sep [ Maybe Range -> Doc
forall p a. (IsString p, Null p) => Maybe a -> p
public (ImportDirective' a b -> Maybe Range
forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective' a b
i)
            , Using' a b -> Doc
forall a. Pretty a => a -> Doc
pretty (Using' a b -> Doc) -> Using' a b -> Doc
forall a b. (a -> b) -> a -> b
$ ImportDirective' a b -> Using' a b
forall n m. ImportDirective' n m -> Using' n m
using ImportDirective' a b
i
            , [ImportedName' a b] -> Doc
forall a. Pretty a => [a] -> Doc
prettyHiding ([ImportedName' a b] -> Doc) -> [ImportedName' a b] -> Doc
forall a b. (a -> b) -> a -> b
$ ImportDirective' a b -> [ImportedName' a b]
forall n m. ImportDirective' n m -> [ImportedName' 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 -> [Renaming' n m]
impRenaming ImportDirective' a b
i
            ]
        where
            public :: Maybe a -> p
public Just{}  = p
"public"
            public Maybe a
Nothing = p
forall a. Null a => a
empty

            prettyHiding :: [a] -> Doc
prettyHiding [] = Doc
forall a. Null a => a
empty
            prettyHiding [a]
xs = Doc
"hiding" Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [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
hsep [ Doc
"renaming"
                             , Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
";" ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
xs
                             ]

instance (Pretty a, Pretty b) => Pretty (Using' a b) where
    pretty :: Using' a b -> Doc
pretty Using' a b
UseEverything = Doc
forall a. Null a => a
empty
    pretty (Using [ImportedName' a b]
xs)    =
        Doc
"using" Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [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
hsep
      [ ImportedName' a b -> Doc
forall a. Pretty a => a -> Doc
pretty ImportedName' a b
from
      , Doc
"to"
      , Doc -> (Fixity -> Doc) -> Maybe Fixity -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty Fixity -> Doc
forall a. Pretty a => a -> Doc
pretty Maybe Fixity
mfx
      , case ImportedName' a b
to of
          ImportedName a
a   -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
          ImportedModule b
b -> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b   -- don't print "module" here
      ]

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