{-# OPTIONS_GHC -fno-warn-orphans #-}
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)
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
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
UnicodeOk -> SpecialCharacters :: (Doc -> Doc)
-> Doc -> Doc -> Doc -> Doc -> Doc -> Doc -> SpecialCharacters
SpecialCharacters { _dbraces :: Doc -> Doc
_dbraces = (("\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
<> " \x2984"))
, _lambda :: Doc
_lambda = "\x03bb"
, _arrow :: Doc
_arrow = "\x2192"
, _forallQ :: Doc
_forallQ = "\x2200"
, _leftIdiomBrkt :: Doc
_leftIdiomBrkt = "\x2987"
, _rightIdiomBrkt :: Doc
_rightIdiomBrkt = "\x2988"
, _emptyIdiomBrkt :: Doc
_emptyIdiomBrkt = "\x2987\x2988"
}
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 = "\\"
, _arrow :: Doc
_arrow = "->"
, _forallQ :: Doc
_forallQ = "forall"
, _leftIdiomBrkt :: Doc
_leftIdiomBrkt = "(|"
, _rightIdiomBrkt :: Doc
_rightIdiomBrkt = "|)"
, _emptyIdiomBrkt :: Doc
_emptyIdiomBrkt = "(|)"
}
braces' :: Doc -> Doc
braces' :: Doc -> Doc
braces' d :: 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) ((String -> Doc) -> Doc) -> (String -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \ s :: 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))
where
spaceIfDash :: Char -> p
spaceIfDash '-' = " "
spaceIfDash _ = p
forall a. Null a => a
empty
dbraces :: Doc -> Doc
dbraces :: Doc -> Doc
dbraces = SpecialCharacters -> Doc -> Doc
_dbraces SpecialCharacters
specialCharacters
forallQ :: Doc
forallQ :: Doc
forallQ = SpecialCharacters -> Doc
_forallQ SpecialCharacters
specialCharacters
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
bracesAndSemicolons :: [Doc] -> Doc
bracesAndSemicolons :: [Doc] -> Doc
bracesAndSemicolons [] = "{}"
bracesAndSemicolons (d :: Doc
d : ds :: [Doc]
ds) =
[Doc] -> Doc
sep (["{" 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]
ds [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ["}"])
arrow, lambda :: Doc
arrow :: Doc
arrow = SpecialCharacters -> Doc
_arrow SpecialCharacters
specialCharacters
lambda :: Doc
lambda = SpecialCharacters -> Doc
_lambda SpecialCharacters
specialCharacters
prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding :: a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding a :: a
a parens :: Doc -> Doc
parens =
case a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding a
a of
Hidden -> Doc -> Doc
braces'
Instance{} -> Doc -> Doc
dbraces
NotHidden -> Doc -> Doc
parens
prettyRelevance :: LensRelevance a => a -> Doc -> Doc
prettyRelevance :: a -> Doc -> Doc
prettyRelevance a :: a
a d :: Doc
d =
if Doc -> String
render Doc
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_" 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
a d :: Doc
d =
if Doc -> String
render Doc
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_" 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
a d :: Doc
d =
if Doc -> String
render Doc
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_" 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' Nothing d :: Doc
d = Doc
d
prettyTactic' (Just t :: Expr
t) d :: Doc
d = "@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (Doc -> Doc
parens ("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
a, b :: 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 n :: Name
n _) = Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n
instance Pretty a => Pretty (WithHiding a) where
pretty :: WithHiding a -> Doc
pretty w :: 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 Relevant = Doc
forall a. Null a => a
empty
pretty Irrelevant = "."
pretty NonStrict = ".."
instance Pretty Q0Origin where
pretty :: Q0Origin -> Doc
pretty = \case
Q0Inferred -> Doc
forall a. Null a => a
empty
Q0{} -> "@0"
Q0Erased{} -> "@erased"
instance Pretty Q1Origin where
pretty :: Q1Origin -> Doc
pretty = \case
Q1Inferred -> Doc
forall a. Null a => a
empty
Q1{} -> "@1"
Q1Linear{} -> "@linear"
instance Pretty QωOrigin where
pretty :: QωOrigin -> Doc
pretty = \case
QωInferred -> Doc
forall a. Null a => a
empty
Qω{} -> "@ω"
QωPlenty{} -> "@plenty"
instance Pretty Quantity where
pretty :: Quantity -> Doc
pretty = \case
Quantity0 o :: 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) "@0" Doc -> Doc
forall a. a -> a
id
Quantity1 o :: 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) "@1" Doc -> Doc
forall a. a -> a
id
Quantityω o :: QωOrigin
o -> QωOrigin -> Doc
forall a. Pretty a => a -> Doc
pretty QωOrigin
o
instance Pretty Cohesion where
pretty :: Cohesion -> Doc
pretty Flat = "@♭"
pretty Continuous = Doc
forall a. Monoid a => a
mempty
pretty Squash = "@⊤"
instance Pretty (OpApp Expr) where
pretty :: OpApp Expr -> Doc
pretty (Ordinary e :: Expr
e) = Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
pretty (SyntaxBindingLambda r :: Range
r bs :: [LamBinding' (TypedBinding' Expr)]
bs e :: Expr
e) = Expr -> Doc
forall a. Pretty a => a -> Doc
pretty (Range -> [LamBinding' (TypedBinding' Expr)] -> Expr -> Expr
Lam Range
r [LamBinding' (TypedBinding' Expr)]
bs Expr
e)
instance Pretty a => Pretty (MaybePlaceholder a) where
pretty :: MaybePlaceholder a -> Doc
pretty Placeholder{} = "_"
pretty (NoPlaceholder _ e :: a
e) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e
instance Pretty Expr where
pretty :: Expr -> Doc
pretty e :: Expr
e =
case Expr
e of
Ident x :: QName
x -> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
Lit l :: Literal
l -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
QuestionMark _ n :: Maybe Int
n -> "?" 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 _ n :: 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 _ _ _ ->
case Expr -> AppView
appView Expr
e of
AppView e1 :: Expr
e1 args :: [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
RawApp _ es :: [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 _ q :: QName
q _ es :: [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 _ e :: Expr
e es :: [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) -> (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 _ e :: 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 _ e :: 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 _ bs :: [LamBinding' (TypedBinding' Expr)]
bs (AbsurdLam _ h :: Hiding
h) -> Doc
lambda Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
bs) Doc -> Doc -> Doc
<+> Hiding -> Doc
forall p. IsString p => Hiding -> p
absurd Hiding
h
Lam _ bs :: [LamBinding' (TypedBinding' Expr)]
bs e :: Expr
e ->
[Doc] -> Doc
sep [ Doc
lambda Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
bs) Doc -> Doc -> Doc
<+> Doc
arrow
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
]
AbsurdLam _ h :: Hiding
h -> Doc
lambda Doc -> Doc -> Doc
<+> Hiding -> Doc
forall p. IsString p => Hiding -> p
absurd Hiding
h
ExtendedLam _ pes :: [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 _ e1 :: Arg Expr
e1 e2 :: 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 tel :: [TypedBinding' Expr]
tel e :: Expr
e ->
[Doc] -> Doc
sep [ Tel -> Doc
forall a. Pretty a => a -> Doc
pretty ([TypedBinding' Expr] -> Tel
Tel ([TypedBinding' Expr] -> Tel) -> [TypedBinding' Expr] -> Tel
forall a b. (a -> b) -> a -> b
$ [TypedBinding' Expr] -> [TypedBinding' Expr]
smashTel [TypedBinding' Expr]
tel) Doc -> Doc -> Doc
<+> Doc
arrow
, Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
]
Set _ -> "Set"
Prop _ -> "Prop"
SetN _ n :: Integer
n -> "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 _ n :: Integer
n -> "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 _ ds :: [Declaration]
ds me :: TacticAttribute
me ->
[Doc] -> Doc
sep [ "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 (\ e :: Expr
e -> "in" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e) TacticAttribute
me
]
Paren _ e :: 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 _ es :: [Expr]
es ->
case [Expr]
es of
[] -> Doc
emptyIdiomBrkt
[e :: Expr
e] -> Doc
leftIdiomBrkt Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e Doc -> Doc -> Doc
<+> Doc
rightIdiomBrkt
e :: Expr
e:es :: [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) -> (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 _ ss :: [DoStmt]
ss -> "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 _ x :: Name
x e :: 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
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
Dot _ e :: Expr
e -> "." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
DoubleDot _ e :: Expr
e -> ".." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
Absurd _ -> "()"
Rec _ xs :: RecordAssignments
xs -> [Doc] -> Doc
sep ["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 _ e :: Expr
e xs :: [FieldAssignment]
xs ->
[Doc] -> Doc
sep ["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 [] -> "()"
ETel tel :: [TypedBinding' Expr]
tel -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TypedBinding' Expr -> Doc) -> [TypedBinding' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding' Expr]
tel
Quote _ -> "quote"
QuoteTerm _ -> "quoteTerm"
Unquote _ -> "unquote"
Tactic _ t :: Expr
t -> "tactic" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t
DontCare e :: Expr
e -> "." 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 _ a :: Expr
a b :: Expr
b -> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
a Doc -> Doc -> Doc
<+> "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
b
Ellipsis _ -> "..."
Generalized e :: Expr
e -> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
where
absurd :: Hiding -> p
absurd NotHidden = "()"
absurd Instance{} = "{{}}"
absurd Hidden = "{}"
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 x :: Name
x e :: a
e) = [Doc] -> Doc
sep [ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> "=" , Int -> Doc -> Doc
nest 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 m :: QName
m es :: [Expr]
es i :: 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
lhs rhs :: RHS' Expr
rhs wh :: WhereClause' [Declaration]
wh _) =
[Doc] -> Doc
sep [ LHS -> Doc
forall a. Pretty a => a -> Doc
pretty LHS
lhs
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ RHS' Expr -> Doc
forall a. Pretty a => RHS' a -> Doc
pretty' RHS' Expr
rhs
] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (WhereClause' [Declaration] -> Doc
forall a. Pretty a => a -> Doc
pretty WhereClause' [Declaration]
wh)
where
pretty' :: RHS' a -> Doc
pretty' (RHS e :: a
e) = Doc
arrow Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e
pretty' 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 x :: NamedArg Binder
x
| NamedArg Binder -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Binder
x = Maybe String
forall a. Maybe a
Nothing
| Just l :: 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 mpat :: Maybe Pattern
mpat n :: a
n) = let d :: Doc
d = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
n in case Maybe Pattern
mpat of
Nothing -> Doc
d
Just pat :: Pattern
pat -> Doc
d 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 withH :: Bool
withH x :: NamedArg Binder
x) = Doc -> Doc
prH (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
if | Just l :: String
l <- NamedArg Binder -> Maybe String
isLabeled NamedArg Binder
x -> String -> Doc
text String
l 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
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' (TypedBinding' Expr) -> Doc
pretty (DomainFree x :: NamedArg Binder
x) = NamedBinding -> Doc
forall a. Pretty a => a -> Doc
pretty (Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
True NamedArg Binder
x)
pretty (DomainFull b :: TypedBinding' Expr
b) = TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty TypedBinding' Expr
b
instance Pretty TypedBinding where
pretty :: TypedBinding' Expr -> Doc
pretty (TLet _ ds :: [Declaration]
ds) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "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 _ xs :: [NamedArg Binder]
xs (Underscore _ 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 _ xs :: [NamedArg Binder]
xs e :: 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
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e ]
| ys :: [NamedArg Binder]
ys@(y :: NamedArg Binder
y : _) <- [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
xs ]
where
groupBinds :: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [] = []
groupBinds (x :: NamedArg Binder
x : xs :: [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 (ys :: [NamedArg Binder]
ys, zs :: [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 x :: a
x y :: 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 tel :: [TypedBinding' Expr]
tel)
| (TypedBinding' Expr -> Bool) -> [TypedBinding' Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypedBinding' Expr -> Bool
isMeta [TypedBinding' Expr]
tel = Doc
forallQ Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((TypedBinding' Expr -> Doc) -> [TypedBinding' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding' Expr]
tel)
| Bool
otherwise = [Doc] -> Doc
fsep ((TypedBinding' Expr -> Doc) -> [TypedBinding' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding' Expr]
tel)
where
isMeta :: TypedBinding' Expr -> Bool
isMeta (TBind _ _ (Underscore _ Nothing)) = Bool
True
isMeta _ = Bool
False
smashTel :: Telescope -> Telescope
smashTel :: [TypedBinding' Expr] -> [TypedBinding' Expr]
smashTel (TBind r :: Range
r xs :: [NamedArg Binder]
xs e :: Expr
e :
TBind _ ys :: [NamedArg Binder]
ys e' :: Expr
e' : tel :: [TypedBinding' Expr]
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' Expr] -> [TypedBinding' Expr]
smashTel (Range -> [NamedArg Binder] -> Expr -> TypedBinding' Expr
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' Expr -> [TypedBinding' Expr] -> [TypedBinding' Expr]
forall a. a -> [a] -> [a]
: [TypedBinding' Expr]
tel)
smashTel (b :: TypedBinding' Expr
b : tel :: [TypedBinding' Expr]
tel) = TypedBinding' Expr
b TypedBinding' Expr -> [TypedBinding' Expr] -> [TypedBinding' Expr]
forall a. a -> [a] -> [a]
: [TypedBinding' Expr] -> [TypedBinding' Expr]
smashTel [TypedBinding' Expr]
tel
smashTel [] = []
instance Pretty RHS where
pretty :: RHS' Expr -> Doc
pretty (RHS e :: Expr
e) = "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
pretty AbsurdRHS = Doc
forall a. Null a => a
empty
instance Pretty WhereClause where
pretty :: WhereClause' [Declaration] -> Doc
pretty NoWhere = Doc
forall a. Null a => a
empty
pretty (AnyWhere [Module _ x :: QName
x [] ds :: [Declaration]
ds]) | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName (QName -> Name
unqualify QName
x)
= [Doc] -> Doc
vcat [ "where", Int -> Doc -> Doc
nest 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 ds :: [Declaration]
ds) = [Doc] -> Doc
vcat [ "where", Int -> Doc -> Doc
nest 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 m :: Name
m a :: Access
a ds :: [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) ("private" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:)
[ "module", Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
m, "where" ]
, Int -> Doc -> Doc
nest 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 p :: Pattern
p eqs :: [RewriteEqn]
eqs es :: [WithHiding Expr]
es ell :: ExpandedEllipsis
ell) = [Doc] -> Doc
sep
[ Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
, Int -> Doc -> Doc
nest 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 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
prefixedThings "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 f :: QName
f ps :: [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 d :: QName
d ps :: [NamedArg Pattern]
ps lhscore :: NamedArg LHSCore
lhscore ps' :: [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 h :: LHSCore
h wps :: [Pattern]
wps ps :: [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) -> (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 _ bs :: [TypedBinding' Expr]
bs e :: Expr
e) = [Doc] -> Doc
fsep ((TypedBinding' Expr -> Doc) -> [TypedBinding' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding' Expr]
bs) Doc -> Doc -> Doc
<+> "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
pretty (RecordModuleInstance _ rec :: QName
rec) = "=" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
rec Doc -> Doc -> Doc
<+> "{{...}}"
instance Pretty DoStmt where
pretty :: DoStmt -> Doc
pretty (DoBind _ p :: Pattern
p e :: Expr
e cs :: [LamClause]
cs) =
((Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p 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 cs :: [a]
cs = "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 e :: Expr
e) = Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
pretty (DoLet _ ds :: [Declaration]
ds) = "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 d :: Declaration
d =
case Declaration
d of
TypeSig i :: ArgInfo
i tac :: TacticAttribute
tac x :: Name
x e :: 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
<+> ":"
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
]
FieldSig inst :: IsInstance
inst tac :: TacticAttribute
tac x :: Name
x (Arg i :: ArgInfo
i e :: 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 _) d :: Doc
d = [Doc] -> Doc
sep [ "instance", Int -> Doc -> Doc
nest 2 Doc
d ]
mkInst NotInstanceDef d :: Doc
d = Doc
d
mkOverlap :: a -> Doc -> Doc
mkOverlap i :: a
i d :: Doc
d | a -> Bool
forall a. LensHiding a => a -> Bool
isOverlappable a
i = "overlap" Doc -> Doc -> Doc
<+> Doc
d
| Bool
otherwise = Doc
d
Field _ fs :: [Declaration]
fs ->
[Doc] -> Doc
sep [ "field"
, Int -> Doc -> Doc
nest 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
lhs rhs :: RHS' Expr
rhs wh :: WhereClause' [Declaration]
wh _ ->
[Doc] -> Doc
sep [ LHS -> Doc
forall a. Pretty a => a -> Doc
pretty LHS
lhs
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ RHS' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty RHS' Expr
rhs
] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (WhereClause' [Declaration] -> Doc
forall a. Pretty a => a -> Doc
pretty WhereClause' [Declaration]
wh)
DataSig _ x :: Name
x tel :: [LamBinding' (TypedBinding' Expr)]
tel e :: Expr
e ->
[Doc] -> Doc
sep [ [Doc] -> Doc
hsep [ "data"
, Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
, [Doc] -> Doc
fcat ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
tel)
]
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
[ ":"
, Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
]
]
Data _ x :: Name
x tel :: [LamBinding' (TypedBinding' Expr)]
tel e :: Expr
e cs :: [Declaration]
cs ->
[Doc] -> Doc
sep [ [Doc] -> Doc
hsep [ "data"
, Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
, [Doc] -> Doc
fcat ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
tel)
]
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
[ ":"
, Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
, "where"
]
] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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 _ x :: Name
x tel :: [LamBinding' (TypedBinding' Expr)]
tel cs :: [Declaration]
cs ->
[Doc] -> Doc
sep [ [Doc] -> Doc
hsep [ "data"
, Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
, [Doc] -> Doc
fcat ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
tel)
]
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "where"
] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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 _ x :: Name
x tel :: [LamBinding' (TypedBinding' Expr)]
tel e :: Expr
e ->
[Doc] -> Doc
sep [ [Doc] -> Doc
hsep [ "record"
, Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
, [Doc] -> Doc
fcat ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
tel)
]
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
[ ":"
, Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
]
]
Record _ x :: Name
x ind :: Maybe (Ranged Induction)
ind eta :: Maybe HasEta
eta con :: Maybe (Name, IsInstance)
con tel :: [LamBinding' (TypedBinding' Expr)]
tel e :: Expr
e cs :: [Declaration]
cs ->
Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding' (TypedBinding' Expr)]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding' (TypedBinding' Expr)]
tel (Expr -> TacticAttribute
forall a. a -> Maybe a
Just Expr
e) [Declaration]
cs
RecordDef _ x :: Name
x ind :: Maybe (Ranged Induction)
ind eta :: Maybe HasEta
eta con :: Maybe (Name, IsInstance)
con tel :: [LamBinding' (TypedBinding' Expr)]
tel cs :: [Declaration]
cs ->
Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding' (TypedBinding' Expr)]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord Name
x Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
con [LamBinding' (TypedBinding' Expr)]
tel TacticAttribute
forall a. Maybe a
Nothing [Declaration]
cs
Infix f :: Fixity
f xs :: [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 n :: Name
n xs :: Notation
xs -> "syntax" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
<+> "..."
PatternSyn _ n :: Name
n as :: [Arg Name]
as p :: Pattern
p -> "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
<+> Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
Mutual _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "mutual" [Declaration]
ds
Abstract _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "abstract" [Declaration]
ds
Private _ _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "private" [Declaration]
ds
InstanceB _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "instance" [Declaration]
ds
Macro _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "macro" [Declaration]
ds
Postulate _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "postulate" [Declaration]
ds
Primitive _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "primitive" [Declaration]
ds
Generalize _ ds :: [Declaration]
ds -> String -> [Declaration] -> Doc
forall a. Pretty a => String -> [a] -> Doc
namedBlock "variable" [Declaration]
ds
Module _ x :: QName
x tel :: [TypedBinding' Expr]
tel ds :: [Declaration]
ds ->
[Doc] -> Doc
hsep [ "module"
, QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
, [Doc] -> Doc
fcat ((TypedBinding' Expr -> Doc) -> [TypedBinding' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding' Expr]
tel)
, "where"
] Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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 _ x :: Name
x (SectionApp _ [] e :: Expr
e) DoOpen i :: 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 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 4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i
]
ModuleMacro _ x :: Name
x (SectionApp _ tel :: [TypedBinding' Expr]
tel e :: Expr
e) open :: OpenShortHand
open i :: ImportDirective
i ->
[Doc] -> Doc
sep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open 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' Expr -> Doc) -> [TypedBinding' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [TypedBinding' Expr]
tel)
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "=" 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 _ x :: Name
x (RecordModuleInstance _ rec :: QName
rec) open :: OpenShortHand
open i :: ImportDirective
i ->
[Doc] -> Doc
sep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open Doc -> Doc -> Doc
<+> "module" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "=" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
rec Doc -> Doc -> Doc
<+> "{{...}}"
]
Open _ x :: QName
x i :: ImportDirective
i -> [Doc] -> Doc
hsep [ "open", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x, ImportDirective -> Doc
forall a. Pretty a => a -> Doc
pretty ImportDirective
i ]
Import _ x :: QName
x rn :: Maybe AsName
rn open :: OpenShortHand
open i :: ImportDirective
i ->
[Doc] -> Doc
hsep [ OpenShortHand -> Doc
forall a. Pretty a => a -> Doc
pretty OpenShortHand
open, "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 Nothing = Doc
forall a. Null a => a
empty
as (Just x :: AsName' a
x) = "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 _ xs :: [Name]
xs t :: Expr
t ->
[Doc] -> Doc
sep [ "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
<+> "=", Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
UnquoteDef _ xs :: [Name]
xs t :: Expr
t ->
[Doc] -> Doc
sep [ "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
<+> "=", Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
t ]
Pragma pr :: Pragma
pr -> [Doc] -> Doc
sep [ "{-#" Doc -> Doc -> Doc
<+> Pragma -> Doc
forall a. Pretty a => a -> Doc
pretty Pragma
pr, "#-}" ]
where
namedBlock :: String -> [a] -> Doc
namedBlock s :: String
s ds :: [a]
ds =
[Doc] -> Doc
sep [ String -> Doc
text String
s
, Int -> Doc -> Doc
nest 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' (TypedBinding' Expr)]
-> TacticAttribute
-> [Declaration]
-> Doc
pRecord x :: Name
x ind :: Maybe (Ranged Induction)
ind eta :: Maybe HasEta
eta con :: Maybe (Name, IsInstance)
con tel :: [LamBinding' (TypedBinding' Expr)]
tel me :: TacticAttribute
me cs :: [Declaration]
cs =
[Doc] -> Doc
sep [ [Doc] -> Doc
hsep [ "record"
, Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
, [Doc] -> Doc
fcat ((LamBinding' (TypedBinding' Expr) -> Doc)
-> [LamBinding' (TypedBinding' Expr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map LamBinding' (TypedBinding' Expr) -> Doc
forall a. Pretty a => a -> Doc
pretty [LamBinding' (TypedBinding' Expr)]
tel)
]
, Int -> Doc -> Doc
nest 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 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 e :: a
e) = [Doc] -> Doc
hsep
[ ":"
, a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e
, "where"
]
pType Nothing =
"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
YesEta -> "eta-equality"
NoEta -> "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
$ (("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 DoOpen = "open"
pretty DontOpen = Doc
forall a. Null a => a
empty
instance Pretty Pragma where
pretty :: Pragma -> Doc
pretty (OptionsPragma _ opts :: [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
$ "OPTIONS" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
opts
pretty (BuiltinPragma _ b :: RString
b x :: QName
x) = [Doc] -> Doc
hsep [ "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 _ _ xs :: [QName]
xs) =
[Doc] -> Doc
hsep [ "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 _ b :: RString
b x :: QName
x e :: String
e) =
[Doc] -> Doc
hsep [ "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 _ b :: RString
b s :: String
s) =
[Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text ("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 _ i :: QName
i) =
[Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["STATIC", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
pretty (InjectivePragma _ i :: QName
i) =
[Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["INJECTIVE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
pretty (InlinePragma _ True i :: QName
i) =
[Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["INLINE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
pretty (InlinePragma _ False i :: QName
i) =
[Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["NOINLINE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
i]
pretty (ImpossiblePragma _) =
[Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["IMPOSSIBLE"]
pretty (EtaPragma _ x :: QName
x) =
[Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["ETA", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x]
pretty (TerminationCheckPragma _ tc :: TerminationCheck Name
tc) =
case TerminationCheck Name
tc of
TerminationCheck -> Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
NoTerminationCheck -> "NO_TERMINATION_CHECK"
NonTerminating -> "NON_TERMINATING"
Terminating -> "TERMINATING"
TerminationMeasure _ x :: Name
x -> [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ["MEASURE", Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x]
pretty (NoCoverageCheckPragma _) = "NON_COVERING"
pretty (WarningOnUsage _ nm :: QName
nm str :: String
str) = [Doc] -> Doc
hsep [ "WARNING_ON_USAGE", QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
nm, String -> Doc
text String
str ]
pretty (WarningOnImport _ str :: String
str) = [Doc] -> Doc
hsep [ "WARNING_ON_IMPORT", String -> Doc
text String
str ]
pretty (CatchallPragma _) = "CATCHALL"
pretty (DisplayPragma _ lhs :: Pattern
lhs rhs :: Expr
rhs) = "DISPLAY" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [ Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
lhs Doc -> Doc -> Doc
<+> "=", Int -> Doc -> Doc
nest 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 _) = "NO_POSITIVITY_CHECK"
pretty (PolarityPragma _ q :: Name
q occs :: [Occurrence]
occs) =
[Doc] -> Doc
hsep ("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 _) = "NO_UNIVERSE_CHECK"
instance Pretty Fixity where
pretty :: Fixity -> Doc
pretty (Fixity _ Unrelated _) = Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
pretty (Fixity _ (Related d :: PrecedenceLevel
d) ass :: Associativity
ass) = Doc
s Doc -> Doc -> Doc
<+> String -> Doc
text (PrecedenceLevel -> String
toStringWithoutDotZero PrecedenceLevel
d)
where
s :: Doc
s = case Associativity
ass of
LeftAssoc -> "infixl"
RightAssoc -> "infixr"
NonAssoc -> "infix"
instance Pretty GenPart where
pretty :: GenPart -> Doc
pretty (IdPart x :: 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' fix :: Fixity
fix nota :: Notation
nota _)
| 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 = "syntax" Doc -> Doc -> Doc
<+> Notation -> Doc
forall a. Pretty a => a -> Doc
pretty Notation
nota
instance Pretty a => Pretty (Arg a) where
prettyPrec :: Int -> Arg a -> Doc
prettyPrec p :: Int
p (Arg ai :: ArgInfo
ai e :: 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 = 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 p :: Int
p (Named nm :: Maybe NamedName
nm e :: e
e)
| Just s :: 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
> 0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ String -> Doc
text String
s 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 x :: QName
x -> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
AppP p1 :: Pattern
p1 p2 :: NamedArg Pattern
p2 -> [Doc] -> Doc
sep [ Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p1, Int -> Doc -> Doc
nest 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 _ ps :: [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 _ q :: QName
q _ ps :: [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 _ p :: 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 _ p :: 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 _ p :: 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 _ -> Doc
forall a. Underscore a => a
underscore
AsP _ x :: Name
x p :: 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
forall a. Semigroup a => a -> a -> a
<> Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
DotP _ p :: Expr
p -> "." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
p
AbsurdP _ -> "()"
LitP l :: Literal
l -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
QuoteP _ -> "quote"
RecP _ fs :: [FieldAssignment' Pattern]
fs -> [Doc] -> Doc
sep [ "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 _ es :: [(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, "=", Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e2]) | (e1 :: Expr
e1,e2 :: Expr
e2) <- [(Expr, Expr)]
es ]
EllipsisP _ -> "..."
WithP _ p :: Pattern
p -> "|" 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 q :: QName
q es :: [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 :: [Name]
ms = [Name] -> [Name]
forall a. [a] -> [a]
init (QName -> [Name]
qnameParts QName
q)
xs :: [NamePart]
xs = case QName -> Name
unqualify QName
q of
Name _ _ xs :: [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 ms :: [Name]
ms (Hole : xs :: [NamePart]
xs) (e :: NamedArg (MaybePlaceholder a)
e : es :: [NamedArg (MaybePlaceholder a)]
es) =
case NamedArg (MaybePlaceholder a) -> MaybePlaceholder a
forall a. NamedArg a -> a
namedArg NamedArg (MaybePlaceholder a)
e of
Placeholder p :: 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
prOp _ (Hole : _) [] = [(Doc, Maybe PositionInName)]
forall a. HasCallStack => a
__IMPOSSIBLE__
prOp ms :: [Name]
ms (Id x :: String
x : xs :: [NamePart]
xs) es :: [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
prOp _ [] es :: [NamedArg (MaybePlaceholder a)]
es = (NamedArg (MaybePlaceholder a) -> (Doc, Maybe PositionInName))
-> [NamedArg (MaybePlaceholder a)] -> [(Doc, Maybe PositionInName)]
forall a b. (a -> b) -> [a] -> [b]
map (\e :: 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 ms :: [a]
ms doc :: Doc
doc = [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate "." ([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]
merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
merge before :: [Doc]
before [] = [Doc] -> [Doc]
forall a. [a] -> [a]
reverse [Doc]
before
merge before :: [Doc]
before ((d :: Doc
d, Nothing) : after :: [(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 before :: [Doc]
before ((d :: Doc
d, Just Beginning) : after :: [(Doc, Maybe PositionInName)]
after) = [Doc] -> Doc -> [(Doc, Maybe PositionInName)] -> [Doc]
mergeRight [Doc]
before Doc
d [(Doc, Maybe PositionInName)]
after
merge before :: [Doc]
before ((d :: Doc
d, Just End) : after :: [(Doc, Maybe PositionInName)]
after) = case Doc -> [Doc] -> (Doc, [Doc])
forall a. Semigroup a => a -> [a] -> (a, [a])
mergeLeft Doc
d [Doc]
before of
(d :: Doc
d, bs :: [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 before :: [Doc]
before ((d :: Doc
d, Just Middle) : after :: [(Doc, Maybe PositionInName)]
after) = case Doc -> [Doc] -> (Doc, [Doc])
forall a. Semigroup a => a -> [a] -> (a, [a])
mergeLeft Doc
d [Doc]
before of
(d :: Doc
d, bs :: [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 before :: [Doc]
before d :: Doc
d after :: [(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]
a :: Doc
a : as :: [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 d :: a
d before :: [a]
before = case [a]
before of
[] -> (a
d, [])
b :: a
b : bs :: [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 i :: 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{} = "public"
public Nothing = p
forall a. Null a => a
empty
prettyHiding :: [a] -> Doc
prettyHiding [] = Doc
forall a. Null a => a
empty
prettyHiding xs :: [a]
xs = "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]
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 xs :: [a]
xs = [Doc] -> Doc
hsep [ "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]
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 UseEverything = Doc
forall a. Null a => a
empty
pretty (Using xs :: [ImportedName' a b]
xs) =
"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]
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 from :: ImportedName' a b
from to :: ImportedName' a b
to mfx :: Maybe Fixity
mfx _r :: Range
_r) = [Doc] -> Doc
hsep
[ ImportedName' a b -> Doc
forall a. Pretty a => a -> Doc
pretty ImportedName' a b
from
, "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 -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
ImportedModule b :: b
b -> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b
]
instance (Pretty a, Pretty b) => Pretty (ImportedName' a b) where
pretty :: ImportedName' a b -> Doc
pretty (ImportedName a :: a
a) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
pretty (ImportedModule b :: b
b) = "module" Doc -> Doc -> Doc
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b