Agda-2.5.1.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell98

Agda.Utils.Pretty

Contents

Description

Pretty printing functions.

Synopsis

Pretty class

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 ....

Methods

pretty :: a -> Doc Source #

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

Instances

Pretty Bool Source # 
Pretty Char Source # 
Pretty Int Source # 

Methods

pretty :: Int -> Doc Source #

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

Pretty Int32 Source # 
Pretty Integer Source # 
Pretty String Source # 
Pretty Doc Source # 

Methods

pretty :: Doc -> Doc Source #

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

Pretty AbsolutePath Source # 
Pretty CPUTime Source #

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

Pretty Phase Source # 
Pretty Order Source # 
Pretty CallMatrix Source # 
Pretty IntervalWithoutFile Source # 
Pretty PositionWithoutFile Source # 
Pretty MetaId Source # 
Pretty TopLevelModuleName Source # 
Pretty QName Source # 
Pretty NamePart Source # 
Pretty Name Source # 
Pretty AmbiguousQName Source # 
Pretty ModuleName Source # 
Pretty QName Source # 
Pretty Name Source # 
Pretty Literal Source # 
Pretty Tel Source # 

Methods

pretty :: Tel -> Doc Source #

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

Pretty DeclarationException Source # 
Pretty ParseError Source # 
Pretty Substitution Source # 
Pretty LevelAtom Source # 
Pretty PlusLevel Source # 
Pretty Level Source # 
Pretty Sort Source # 
Pretty Type Source # 
Pretty Elim Source # 
Pretty Term Source # 
Pretty CompiledClauses Source # 
Pretty CallInfo Source # 
Pretty Call Source # 
Pretty NamedMeta Source # 
Pretty Comparison Source # 
Pretty Interface Source # 
Pretty ProblemId Source # 
Pretty CallPath Source #

Only show intermediate nodes. (Drop last CallInfo).

Pretty Cl Source # 

Methods

pretty :: Cl -> Doc Source #

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

Pretty a => Pretty (Lisp a) Source # 

Methods

pretty :: Lisp a -> Doc Source #

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

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

Print benchmark as two-column table with totals.

Pretty cinfo => Pretty (CMSet cinfo) Source # 

Methods

pretty :: CMSet cinfo -> Doc Source #

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

Pretty cinfo => Pretty (CallMatrixAug cinfo) Source # 
Pretty cinfo => Pretty (CallGraph cinfo) Source #

Displays the recursion behaviour corresponding to a call graph.

Methods

pretty :: CallGraph cinfo -> Doc Source #

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

(Pretty a, HasRange a) => Pretty (PrintRange a) Source # 
Pretty a => Pretty (Range' (Maybe a)) Source # 

Methods

pretty :: Range' (Maybe a) -> Doc Source #

prettyPrec :: Int -> Range' (Maybe a) -> Doc Source #

Pretty a => Pretty (Interval' (Maybe a)) Source # 
Pretty a => Pretty (Position' (Maybe a)) Source # 
Pretty a => Pretty (QNamed a) Source # 

Methods

pretty :: QNamed a -> Doc Source #

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

Pretty a => Pretty (Pattern' a) Source # 
Pretty a => Pretty (ClauseBodyF a) Source # 
Pretty a => Pretty (Case a) Source # 

Methods

pretty :: Case a -> Doc Source #

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

Pretty a => Pretty (WithArity a) Source # 
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source # 

Methods

pretty :: Matrix i b -> Doc Source #

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

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

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

Use instead of show when printing to world.

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

Space separated list of pretty things.

Pretty instances

Doc utilities

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.