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

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.Pretty

Contents

Description

Pretty printing functions.

Synopsis

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 # 
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 # 
Pretty IntervalWithoutFile # 
Pretty PositionWithoutFile # 
Pretty ParseWarning # 
Pretty ParseError # 
Pretty MetaId # 

Methods

pretty :: MetaId -> Doc #

prettyPrec :: Int -> MetaId -> Doc #

Pretty TopLevelModuleName # 
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 # 
Pretty ModuleName # 
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 # 
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 # 
Pretty PlusLevel # 
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 # 
Pretty CompiledClauses # 
Pretty CallInfo # 

Methods

pretty :: CallInfo -> Doc #

prettyPrec :: Int -> CallInfo -> Doc #

Pretty Call # 

Methods

pretty :: Call -> Doc #

prettyPrec :: Int -> Call -> Doc #

Pretty NamedMeta # 
Pretty Comparison # 
Pretty Interface # 
Pretty ProblemId # 
Pretty AsBinding # 
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) # 
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) # 

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] #

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)