Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Pretty

Description

Pretty printing functions.

Synopsis

Documentation

class Pretty a where Source #

While Show is for rendering data in Haskell syntax, Pretty is for displaying data to the world, i.e., the user and the environment.

Atomic data has no inner document structure, so just implement pretty as pretty a = text $ ... a ....

Minimal complete definition

Nothing

Methods

pretty :: a -> Doc Source #

prettyPrec :: Int -> a -> Doc Source #

prettyList :: [a] -> Doc Source #

Instances

Instances details
Pretty Bool Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty Char Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty Int Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty Int32 Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty Integer Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty () Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: () -> Doc Source #

prettyPrec :: Int -> () -> Doc Source #

prettyList :: [()] -> Doc Source #

Pretty Doc Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty QOp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Name Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty QName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ModuleName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Literal Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Type Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ConDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty DataOrNew Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Decl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ImportSpec Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ImportDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ModulePragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Rigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty CPUTime Source #

Print CPU time in milli (10^-3) seconds.

Instance details

Defined in Agda.Utils.Time

Pretty IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Pretty PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Pretty GenPart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Access Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Cohesion Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Relevance Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Quantity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty NamedMeta Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Pretty ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Pretty AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Pretty Literal Source # 
Instance details

Defined in Agda.Syntax.Literal

Pretty TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Pretty

Pretty LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library

Pretty Label Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Pretty Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Pretty Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Tel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty NamedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Pretty Phase Source # 
Instance details

Defined in Agda.Benchmarking

Pretty ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty LocalVar Source #

We show shadowed variables as prefixed by a ".", as not in scope.

Instance details

Defined in Agda.Syntax.Scope.Base

Pretty ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty Order Source # 
Instance details

Defined in Agda.Termination.Order

Pretty CallMatrix Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Pretty DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Pretty DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Pretty DeclarationException Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Pretty NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions

Pretty LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library

Pretty CallInfo Source #

We only show the name of the callee.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Pretty OldSizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes

Pretty OldSizeExpr Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes

Pretty AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Pretty Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Pretty SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Pretty BlockingVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Pretty CallPath Source #

Only show intermediate nodes. (Drop last CallInfo).

Instance details

Defined in Agda.Termination.Monad

Pretty SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Pretty NamedRigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Pretty Cl Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause.Compile

Pretty HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

Pretty a => Pretty [a] Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: [a] -> Doc Source #

prettyPrec :: Int -> [a] -> Doc Source #

prettyList :: [[a]] -> Doc Source #

Pretty a => Pretty (Maybe a) Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty a => Pretty (NonEmpty a) Source # 
Instance details

Defined in Agda.Utils.Pretty

Pretty flex => Pretty (PolarityAssignment flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty a => Pretty (Lisp a) Source # 
Instance details

Defined in Agda.Interaction.EmacsCommand

Methods

pretty :: Lisp a -> Doc Source #

prettyPrec :: Int -> Lisp a -> Doc Source #

prettyList :: [Lisp a] -> Doc Source #

(Ord a, Pretty a) => Pretty (Benchmark a) Source #

Print benchmark as three-column table with totals.

Instance details

Defined in Agda.Utils.Benchmark

(Pretty a, HasRange a) => Pretty (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Pretty a => Pretty (Range' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

Pretty a => Pretty (Interval' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

Pretty a => Pretty (Position' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

Pretty a => Pretty (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty e => Pretty (Named_ e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Arg a -> Doc Source #

prettyPrec :: Int -> Arg a -> Doc Source #

prettyList :: [Arg a] -> Doc Source #

Pretty a => Pretty (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty a => Pretty (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (QNamed a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty a => Pretty (SplitTreeLabel a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Pretty a => Pretty (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Pretty cinfo => Pretty (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CMSet cinfo -> Doc Source #

prettyPrec :: Int -> CMSet cinfo -> Doc Source #

prettyList :: [CMSet cinfo] -> Doc Source #

Pretty cinfo => Pretty (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Pretty cinfo => Pretty (CallGraph cinfo) Source #

Displays the recursion behaviour corresponding to a call graph.

Instance details

Defined in Agda.Termination.CallGraph

Methods

pretty :: CallGraph cinfo -> Doc Source #

prettyPrec :: Int -> CallGraph cinfo -> Doc Source #

prettyList :: [CallGraph cinfo] -> Doc Source #

Pretty a => Pretty (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty a => Pretty (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty a => Pretty (Tele (Dom a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc Source #

prettyPrec :: Int -> Tele (Dom a) -> Doc Source #

prettyList :: [Tele (Dom a)] -> Doc Source #

Pretty tm => Pretty (Elim' tm) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Elim' tm -> Doc Source #

prettyPrec :: Int -> Elim' tm -> Doc Source #

prettyList :: [Elim' tm] -> Doc Source #

Pretty a => Pretty (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: Case a -> Doc Source #

prettyPrec :: Int -> Case a -> Doc Source #

prettyList :: [Case a] -> Doc Source #

Pretty a => Pretty (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Pretty c => Pretty (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(Pretty a, Pretty b) => Pretty (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Either a b -> Doc Source #

prettyPrec :: Int -> Either a b -> Doc Source #

prettyList :: [Either a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (a, b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: (a, b) -> Doc Source #

prettyPrec :: Int -> (a, b) -> Doc Source #

prettyList :: [(a, b)] -> Doc Source #

(Pretty r, Pretty f) => Pretty (Solution r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

(Pretty r, Pretty f) => Pretty (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

(Pretty r, Pretty f) => Pretty (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(Pretty a, Pretty b) => Pretty (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Using' a b -> Doc Source #

prettyPrec :: Int -> Using' a b -> Doc Source #

prettyList :: [Using' a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

(Pretty n, Pretty e) => Pretty (Edge n e) Source # 
Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: Edge n e -> Doc Source #

prettyPrec :: Int -> Edge n e -> Doc Source #

prettyList :: [Edge n e] -> Doc Source #

(Ord n, Pretty n, Pretty e) => Pretty (Graph n e) Source # 
Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: Graph n e -> Doc Source #

prettyPrec :: Int -> Graph n e -> Doc Source #

prettyList :: [Graph n e] -> Doc Source #

(Pretty rigid, Pretty flex) => Pretty (Node rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Node rigid flex -> Doc Source #

prettyPrec :: Int -> Node rigid flex -> Doc Source #

prettyList :: [Node rigid flex] -> Doc Source #

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source # 
Instance details

Defined in Agda.Termination.SparseMatrix

Methods

pretty :: Matrix i b -> Doc Source #

prettyPrec :: Int -> Matrix i b -> Doc Source #

prettyList :: [Matrix i b] -> Doc Source #

(Pretty t, Pretty e) => Pretty (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc Source #

prettyPrec :: Int -> Dom' t e -> Doc Source #

prettyList :: [Dom' t e] -> Doc Source #

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(Pretty a, Pretty b) => Pretty (OutputForm a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(Pretty p, Pretty e) => Pretty (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: RewriteEqn' qn p e -> Doc Source #

prettyPrec :: Int -> RewriteEqn' qn p e -> Doc Source #

prettyList :: [RewriteEqn' qn p e] -> Doc Source #

prettyShow :: Pretty a => a -> String Source #

Use instead of show when printing to world.

prettyList_ :: Pretty a => [a] -> Doc Source #

Comma separated list, without the brackets.

mparens :: Bool -> Doc -> Doc Source #

Apply parens to Doc if boolean is true.

align :: Int -> [(String, Doc)] -> Doc Source #

align max rows lays out the elements of rows in two columns, with the second components aligned. The alignment column of the second components is at most max characters to the right of the left-most column.

Precondition: max > 0.

multiLineText :: String -> Doc Source #

Handles strings with newlines properly (preserving indentation)

(<?>) :: Doc -> Doc -> Doc infixl 6 Source #

a ? b = hang a 2 b

pshow :: Show a => a -> Doc Source #

pshow = text . pretty

singPlural :: Sized a => a -> c -> c -> c Source #

prefixedThings :: Doc -> [Doc] -> Doc Source #

Used for with-like telescopes

fullRender #

Arguments

:: Mode

Rendering mode.

-> Int

Line length.

-> Float

Ribbons per line.

-> (TextDetails -> a -> a)

What to do with text.

-> a

What to do at the end.

-> Doc

The document.

-> a

Result.

The general rendering interface. Please refer to the Style and Mode types for a description of rendering mode, line length and ribbons.

renderStyle :: Style -> Doc -> String #

Render the Doc to a String using the given Style.

render :: Doc -> String #

Render the Doc to a String using the default Style (see style).

fsep :: [Doc] -> Doc #

"Paragraph fill" version of sep.

fcat :: [Doc] -> Doc #

"Paragraph fill" version of cat.

cat :: [Doc] -> Doc #

Either hcat or vcat.

sep :: [Doc] -> Doc #

Either hsep or vcat.

(<+>) :: Doc -> Doc -> Doc infixl 6 #

Beside, separated by space, unless one of the arguments is empty. <+> is associative, with identity empty.

($+$) :: Doc -> Doc -> Doc infixl 5 #

Above, with no overlapping. $+$ is associative, with identity empty.

($$) :: Doc -> Doc -> Doc infixl 5 #

Above, except that if the last line of the first argument stops at least one position before the first line of the second begins, these two lines are overlapped. For example:

   text "hi" $$ nest 5 (text "there")

lays out as

   hi   there

rather than

   hi
        there

$$ is associative, with identity empty, and also satisfies

  • (x $$ y) <> z = x $$ (y <> z), if y non-empty.

punctuate :: Doc -> [Doc] -> [Doc] #

punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]

hang :: Doc -> Int -> Doc -> Doc #

hang d1 n d2 = sep [d1, nest n d2]

nest :: Int -> Doc -> Doc #

Nest (or indent) a document by a given number of positions (which may also be negative). nest satisfies the laws:

The side condition on the last law is needed because empty is a left identity for <>.

vcat :: [Doc] -> Doc #

List version of $$.

hsep :: [Doc] -> Doc #

List version of <+>.

hcat :: [Doc] -> Doc #

List version of <>.

braces #

Arguments

:: Doc 
-> Doc

Wrap document in {...}

brackets #

Arguments

:: Doc 
-> Doc

Wrap document in [...]

parens #

Arguments

:: Doc 
-> Doc

Wrap document in (...)

doubleQuotes #

Arguments

:: Doc 
-> Doc

Wrap document in "..."

quotes #

Arguments

:: Doc 
-> Doc

Wrap document in '...'

rational #

Arguments

:: Rational 
-> Doc
rational n = text (show n)

double #

Arguments

:: Double 
-> Doc
double n = text (show n)

float #

Arguments

:: Float 
-> Doc
float n = text (show n)

integer #

Arguments

:: Integer 
-> Doc
integer n = text (show n)

int #

Arguments

:: Int 
-> Doc
int n = text (show n)

rbrace #

Arguments

:: Doc

A '}' character

lbrace #

Arguments

:: Doc

A '{' character

rbrack #

Arguments

:: Doc

A ']' character

lbrack #

Arguments

:: Doc

A '[' character

rparen #

Arguments

:: Doc

A ')' character

lparen #

Arguments

:: Doc

A '(' character

equals #

Arguments

:: Doc

A '=' character

space #

Arguments

:: Doc

A space character

colon #

Arguments

:: Doc

A : character

comma #

Arguments

:: Doc

A ',' character

semi #

Arguments

:: Doc

A ';' character

isEmpty :: Doc -> Bool #

Returns True if the document is empty

zeroWidthText :: String -> Doc #

Some text, but without any width. Use for non-printing text such as a HTML or Latex tags

sizedText :: Int -> String -> Doc #

Some text with any width. (text s = sizedText (length s) s)

ptext :: String -> Doc #

Same as text. Used to be used for Bytestrings.

text :: String -> Doc #

A document of height 1 containing a literal string. text satisfies the following laws:

The side condition on the last law is necessary because text "" has height 1, while empty has no height.

char :: Char -> Doc #

A document of height and width 1, containing a literal character.

data Doc #

The abstract type of documents. A Doc represents a set of layouts. A Doc with no occurrences of Union or NoDoc represents just one layout.

Instances

Instances details
Eq Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

(==) :: Doc -> Doc -> Bool #

(/=) :: Doc -> Doc -> Bool #

Data Doc Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc #

toConstr :: Doc -> Constr #

dataTypeOf :: Doc -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) #

gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r #

gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc #

Show Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

showsPrec :: Int -> Doc -> ShowS #

show :: Doc -> String #

showList :: [Doc] -> ShowS #

IsString Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

fromString :: String -> Doc #

Generic Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Associated Types

type Rep Doc :: Type -> Type #

Methods

from :: Doc -> Rep Doc x #

to :: Rep Doc x -> Doc #

Semigroup Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

(<>) :: Doc -> Doc -> Doc #

sconcat :: NonEmpty Doc -> Doc #

stimes :: Integral b => b -> Doc -> Doc #

Monoid Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

mempty :: Doc #

mappend :: Doc -> Doc -> Doc #

mconcat :: [Doc] -> Doc #

NFData Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

rnf :: Doc -> () #

Null Doc Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Doc Source #

null :: Doc -> Bool Source #

Pretty Doc Source # 
Instance details

Defined in Agda.Utils.Pretty

Underscore Doc Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

TraceS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #

ReportS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #

ToJSON Doc 
Instance details

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value

toEncoding :: Doc -> Encoding

toJSONList :: [Doc] -> Value

toEncodingList :: [Doc] -> Encoding

EncodeTCM Doc Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value Source #

Semigroup (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc #

stimes :: Integral b => b -> TCM Doc -> TCM Doc #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

TraceS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

ReportS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

Monad m => Null (PureConversionT m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Applicative m => Semigroup (ReaderT s m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: ReaderT s m Doc -> ReaderT s m Doc -> ReaderT s m Doc #

sconcat :: NonEmpty (ReaderT s m Doc) -> ReaderT s m Doc #

stimes :: Integral b => b -> ReaderT s m Doc -> ReaderT s m Doc #

Monad m => Semigroup (StateT s m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: StateT s m Doc -> StateT s m Doc -> StateT s m Doc #

sconcat :: NonEmpty (StateT s m Doc) -> StateT s m Doc #

stimes :: Integral b => b -> StateT s m Doc -> StateT s m Doc #

type Rep Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

type Rep Doc = D1 ('MetaData "Doc" "Text.PrettyPrint.HughesPJ" "pretty-1.1.3.6" 'True) (C1 ('MetaCons "Doc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Doc ()))))

style :: Style #

The default style (mode=PageMode, lineLength=100, ribbonsPerLine=1.5).

pattern Chr :: !Char -> TextDetails #

A single Char fragment

pattern PStr :: String -> TextDetails #

Used to represent a Fast String fragment but now deprecated and identical to the Str constructor.

data Style #

A rendering style. Allows us to specify constraints to choose among the many different rendering options.

Constructors

Style 

Fields

  • mode :: Mode

    The rendering mode.

  • lineLength :: Int

    Maximum length of a line, in characters.

  • ribbonsPerLine :: Float

    Ratio of line length to ribbon length. A ribbon refers to the characters on a line excluding indentation. So a lineLength of 100, with a ribbonsPerLine of 2.0 would only allow up to 50 characters of ribbon to be displayed on a line, while allowing it to be indented up to 50 characters.

Instances

Instances details
Eq Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(==) :: Style -> Style -> Bool #

(/=) :: Style -> Style -> Bool #

Show Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Style -> ShowS #

show :: Style -> String #

showList :: [Style] -> ShowS #

Generic Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

type Rep Style :: Type -> Type #

Methods

from :: Style -> Rep Style x #

to :: Rep Style x -> Style #

type Rep Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

type Rep Style = D1 ('MetaData "Style" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) (C1 ('MetaCons "Style" 'PrefixI 'True) (S1 ('MetaSel ('Just "mode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Mode) :*: (S1 ('MetaSel ('Just "lineLength") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "ribbonsPerLine") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Float))))

data Mode #

Rendering mode.

Constructors

PageMode

Normal rendering (lineLength and ribbonsPerLine respected').

ZigZagMode

With zig-zag cuts.

LeftMode

No indentation, infinitely long lines (lineLength ignored), but explicit new lines, i.e., text "one" $$ text "two", are respected.

OneLineMode

All on one line, lineLength ignored and explicit new lines ($$) are turned into spaces.

Instances

Instances details
Eq Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(==) :: Mode -> Mode -> Bool #

(/=) :: Mode -> Mode -> Bool #

Show Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Mode -> ShowS #

show :: Mode -> String #

showList :: [Mode] -> ShowS #

Generic Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

type Rep Mode :: Type -> Type #

Methods

from :: Mode -> Rep Mode x #

to :: Rep Mode x -> Mode #

type Rep Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

type Rep Mode = D1 ('MetaData "Mode" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) ((C1 ('MetaCons "PageMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ZigZagMode" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LeftMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OneLineMode" 'PrefixI 'False) (U1 :: Type -> Type)))

(<>) :: Semigroup a => a -> a -> a infixr 6 #

An associative operation.

>>> [1,2,3] <> [4,5,6]
[1,2,3,4,5,6]

Orphan instances

Data Doc Source # 
Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc #

toConstr :: Doc -> Constr #

dataTypeOf :: Doc -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) #

gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r #

gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc #