Agda.Utils.Pretty

Pretty printing functions.

Pretty class

class Pretty a where

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

prettyPrec :: Int -> a -> Doc

Instances

Pretty Bool

Methods

pretty :: Bool -> Doc

prettyPrec :: Int -> Bool -> Doc

Pretty Char

Methods

pretty :: Char -> Doc

prettyPrec :: Int -> Char -> Doc

Pretty Int

Methods

pretty :: Int -> Doc

prettyPrec :: Int -> Int -> Doc

Pretty Int32

Methods

pretty :: Int32 -> Doc

prettyPrec :: Int -> Int32 -> Doc

Pretty Integer

Methods

pretty :: Integer -> Doc

prettyPrec :: Int -> Integer -> Doc

Pretty String

Methods

pretty :: String -> Doc

prettyPrec :: Int -> String -> Doc

Pretty Doc

Methods

pretty :: Doc -> Doc

prettyPrec :: Int -> Doc -> Doc

Pretty AbsolutePath

Methods

pretty :: AbsolutePath -> Doc

prettyPrec :: Int -> AbsolutePath -> Doc

Pretty CPUTime

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

Methods

pretty :: CPUTime -> Doc

prettyPrec :: Int -> CPUTime -> Doc

Pretty Order

Methods

pretty :: Order -> Doc

prettyPrec :: Int -> Order -> Doc

Pretty CallMatrix

Methods

pretty :: CallMatrix -> Doc

prettyPrec :: Int -> CallMatrix -> Doc

Pretty IntervalWithoutFile

Methods

pretty :: IntervalWithoutFile -> Doc

prettyPrec :: Int -> IntervalWithoutFile -> Doc

Pretty PositionWithoutFile

Methods

pretty :: PositionWithoutFile -> Doc

prettyPrec :: Int -> PositionWithoutFile -> Doc

Pretty ParseWarning

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

Pretty ParseError

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

Pretty MetaId

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

Pretty TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc

prettyPrec :: Int -> TopLevelModuleName -> Doc

Pretty QName

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

Pretty NamePart

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

Pretty Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

Pretty AmbiguousQName

Methods

pretty :: AmbiguousQName -> Doc

prettyPrec :: Int -> AmbiguousQName -> Doc

Pretty ModuleName

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

Pretty QName

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

Pretty Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

Pretty Literal

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

Pretty Tel

Methods

pretty :: Tel -> Doc

prettyPrec :: Int -> Tel -> Doc

Pretty DeclarationException

Methods

pretty :: DeclarationException -> Doc

prettyPrec :: Int -> DeclarationException -> Doc

Pretty Phase

Methods

pretty :: Phase -> Doc

prettyPrec :: Int -> Phase -> Doc

Pretty DBPatVar

Methods

pretty :: DBPatVar -> Doc

prettyPrec :: Int -> DBPatVar -> Doc

Pretty Clause

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

Pretty LevelAtom

Methods

pretty :: LevelAtom -> Doc

prettyPrec :: Int -> LevelAtom -> Doc

Pretty PlusLevel

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

Pretty Level

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

Pretty Sort

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

Pretty Type

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

Pretty Elim

Methods

pretty :: Elim -> Doc

prettyPrec :: Int -> Elim -> Doc

Pretty Term

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

Pretty ScopeCopyInfo

Methods

pretty :: ScopeCopyInfo -> Doc

prettyPrec :: Int -> ScopeCopyInfo -> Doc

Pretty CompiledClauses

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

Pretty CallInfo

Methods

pretty :: CallInfo -> Doc

prettyPrec :: Int -> CallInfo -> Doc

Pretty Call

Methods

pretty :: Call -> Doc

prettyPrec :: Int -> Call -> Doc

Pretty NamedMeta

Methods

pretty :: NamedMeta -> Doc

prettyPrec :: Int -> NamedMeta -> Doc

Pretty Comparison

Methods

pretty :: Comparison -> Doc

prettyPrec :: Int -> Comparison -> Doc

Pretty Interface

Methods

pretty :: Interface -> Doc

prettyPrec :: Int -> Interface -> Doc

Pretty ProblemId

Methods

pretty :: ProblemId -> Doc

prettyPrec :: Int -> ProblemId -> Doc

Pretty AsBinding

Methods

pretty :: AsBinding -> Doc

prettyPrec :: Int -> AsBinding -> Doc

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).

Methods

pretty :: CallPath -> Doc

prettyPrec :: Int -> CallPath -> Doc

Pretty Cl

Methods

pretty :: Cl -> Doc

prettyPrec :: Int -> Cl -> Doc

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

Print benchmark as three-column table with totals.

Methods

pretty :: Benchmark a -> Doc

prettyPrec :: Int -> Benchmark a -> Doc

Pretty cinfo => Pretty (CMSet cinfo)

Methods

pretty :: CMSet cinfo -> Doc

prettyPrec :: Int -> CMSet cinfo -> Doc

Pretty cinfo => Pretty (CallMatrixAug cinfo)

Methods

pretty :: CallMatrixAug cinfo -> Doc

prettyPrec :: Int -> CallMatrixAug cinfo -> Doc

Pretty cinfo => Pretty (CallGraph cinfo)

Displays the recursion behaviour corresponding to a call graph.

Methods

pretty :: CallGraph cinfo -> Doc

prettyPrec :: Int -> CallGraph cinfo -> Doc

(Pretty a, HasRange a) => Pretty (PrintRange a)

Methods

pretty :: PrintRange a -> Doc

prettyPrec :: Int -> PrintRange a -> Doc

Pretty a => Pretty (Range' (Maybe a))

Methods

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

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

Pretty a => Pretty (Interval' (Maybe a))

Methods

pretty :: Interval' (Maybe a) -> Doc

prettyPrec :: Int -> Interval' (Maybe a) -> Doc

Pretty a => Pretty (Position' (Maybe a))

Methods

pretty :: Position' (Maybe a) -> Doc

prettyPrec :: Int -> Position' (Maybe a) -> Doc

Pretty a => Pretty (QNamed a)

Methods

pretty :: QNamed a -> Doc

prettyPrec :: Int -> QNamed a -> Doc

Pretty a => Pretty (Lisp a)

Methods

pretty :: Lisp a -> Doc

prettyPrec :: Int -> Lisp a -> Doc

Pretty a => Pretty (Substitution' a)

Methods

pretty :: Substitution' a -> Doc

prettyPrec :: Int -> Substitution' a -> Doc

Pretty a => Pretty (Pattern' a)

Methods

pretty :: Pattern' a -> Doc

prettyPrec :: Int -> Pattern' a -> Doc

Pretty a => Pretty (Tele (Dom a))

Methods

pretty :: Tele (Dom a) -> Doc

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

Pretty a => Pretty (Case a)

Methods

pretty :: Case a -> Doc

prettyPrec :: Int -> Case a -> Doc

Pretty a => Pretty (WithArity a)

Methods

pretty :: WithArity a -> Doc

prettyPrec :: Int -> WithArity a -> Doc

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)

Methods

pretty :: Matrix i b -> Doc

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

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

Methods

pretty :: OutputConstraint' a b -> Doc

prettyPrec :: Int -> OutputConstraint' a b -> Doc

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

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

Space separated list of pretty things.

Pretty instances

Doc utilities

pwords :: String -> [Doc]

fwords :: String -> Doc

mparens :: Bool -> Doc -> Doc

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

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

Handles strings with newlines properly (preserving indentation)

module Text.PrettyPrint