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

prettyList :: [a] -> Doc

Instances

Pretty Bool

Methods

pretty :: Bool -> Doc

prettyPrec :: Int -> Bool -> Doc

prettyList :: [Bool] -> Doc

Pretty Char

Methods

pretty :: Char -> Doc

prettyPrec :: Int -> Char -> Doc

prettyList :: [Char] -> Doc

Pretty Int

Methods

pretty :: Int -> Doc

prettyPrec :: Int -> Int -> Doc

prettyList :: [Int] -> Doc

Pretty Int32

Methods

pretty :: Int32 -> Doc

prettyPrec :: Int -> Int32 -> Doc

prettyList :: [Int32] -> Doc

Pretty Integer

Methods

pretty :: Integer -> Doc

prettyPrec :: Int -> Integer -> Doc

prettyList :: [Integer] -> Doc

Pretty Doc

Methods

pretty :: Doc -> Doc

prettyPrec :: Int -> Doc -> Doc

prettyList :: [Doc] -> Doc

Pretty Polarity

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Pretty Cmp

Methods

pretty :: Cmp -> Doc

prettyPrec :: Int -> Cmp -> Doc

prettyList :: [Cmp] -> Doc

Pretty Flex

Methods

pretty :: Flex -> Doc

prettyPrec :: Int -> Flex -> Doc

prettyList :: [Flex] -> Doc

Pretty Rigid

Methods

pretty :: Rigid -> Doc

prettyPrec :: Int -> Rigid -> Doc

prettyList :: [Rigid] -> Doc

Pretty Offset

Methods

pretty :: Offset -> Doc

prettyPrec :: Int -> Offset -> Doc

prettyList :: [Offset] -> Doc

Pretty CPUTime

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

Methods

pretty :: CPUTime -> Doc

prettyPrec :: Int -> CPUTime -> Doc

prettyList :: [CPUTime] -> Doc

Pretty AbsolutePath

Methods

pretty :: AbsolutePath -> Doc

prettyPrec :: Int -> AbsolutePath -> Doc

prettyList :: [AbsolutePath] -> Doc

Pretty IntervalWithoutFile

Methods

pretty :: IntervalWithoutFile -> Doc

prettyPrec :: Int -> IntervalWithoutFile -> Doc

prettyList :: [IntervalWithoutFile] -> Doc

Pretty PositionWithoutFile

Methods

pretty :: PositionWithoutFile -> Doc

prettyPrec :: Int -> PositionWithoutFile -> Doc

prettyList :: [PositionWithoutFile] -> Doc

Pretty ParseWarning

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

prettyList :: [ParseWarning] -> Doc

Pretty ParseError

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

prettyList :: [ParseError] -> Doc

Pretty MetaId

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

prettyList :: [MetaId] -> Doc

Pretty Access

Methods

pretty :: Access -> Doc

prettyPrec :: Int -> Access -> Doc

prettyList :: [Access] -> Doc

Pretty TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc

prettyPrec :: Int -> TopLevelModuleName -> Doc

prettyList :: [TopLevelModuleName] -> Doc

Pretty QName

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty NamePart

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

prettyList :: [NamePart] -> Doc

Pretty Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty AmbiguousQName

Methods

pretty :: AmbiguousQName -> Doc

prettyPrec :: Int -> AmbiguousQName -> Doc

prettyList :: [AmbiguousQName] -> Doc

Pretty ModuleName

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

prettyList :: [ModuleName] -> Doc

Pretty QName

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty Literal

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

prettyList :: [Literal] -> Doc

Pretty Precedence

Methods

pretty :: Precedence -> Doc

prettyPrec :: Int -> Precedence -> Doc

prettyList :: [Precedence] -> Doc

Pretty Label

Methods

pretty :: Label -> Doc

prettyPrec :: Int -> Label -> Doc

prettyList :: [Label] -> Doc

Pretty Weight

Methods

pretty :: Weight -> Doc

prettyPrec :: Int -> Weight -> Doc

prettyList :: [Weight] -> Doc

Pretty Occurrence

Methods

pretty :: Occurrence -> Doc

prettyPrec :: Int -> Occurrence -> Doc

prettyList :: [Occurrence] -> Doc

Pretty Where

Methods

pretty :: Where -> Doc

prettyPrec :: Int -> Where -> Doc

prettyList :: [Where] -> Doc

Pretty OccursWhere

Methods

pretty :: OccursWhere -> Doc

prettyPrec :: Int -> OccursWhere -> Doc

prettyList :: [OccursWhere] -> Doc

Pretty Tel

Methods

pretty :: Tel -> Doc

prettyPrec :: Int -> Tel -> Doc

prettyList :: [Tel] -> Doc

Pretty Phase

Methods

pretty :: Phase -> Doc

prettyPrec :: Int -> Phase -> Doc

prettyList :: [Phase] -> Doc

Pretty AbstractModule

Methods

pretty :: AbstractModule -> Doc

prettyPrec :: Int -> AbstractModule -> Doc

prettyList :: [AbstractModule] -> Doc

Pretty AbstractName

Methods

pretty :: AbstractName -> Doc

prettyPrec :: Int -> AbstractName -> Doc

prettyList :: [AbstractName] -> Doc

Pretty NameSpace

Methods

pretty :: NameSpace -> Doc

prettyPrec :: Int -> NameSpace -> Doc

prettyList :: [NameSpace] -> Doc

Pretty LocalVar

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

Methods

pretty :: LocalVar -> Doc

prettyPrec :: Int -> LocalVar -> Doc

prettyList :: [LocalVar] -> Doc

Pretty ScopeInfo

Methods

pretty :: ScopeInfo -> Doc

prettyPrec :: Int -> ScopeInfo -> Doc

prettyList :: [ScopeInfo] -> Doc

Pretty NameSpaceId

Methods

pretty :: NameSpaceId -> Doc

prettyPrec :: Int -> NameSpaceId -> Doc

prettyList :: [NameSpaceId] -> Doc

Pretty Scope

Methods

pretty :: Scope -> Doc

prettyPrec :: Int -> Scope -> Doc

prettyList :: [Scope] -> Doc

Pretty Order

Methods

pretty :: Order -> Doc

prettyPrec :: Int -> Order -> Doc

prettyList :: [Order] -> Doc

Pretty CallMatrix

Methods

pretty :: CallMatrix -> Doc

prettyPrec :: Int -> CallMatrix -> Doc

prettyList :: [CallMatrix] -> Doc

Pretty DBPatVar

Methods

pretty :: DBPatVar -> Doc

prettyPrec :: Int -> DBPatVar -> Doc

prettyList :: [DBPatVar] -> Doc

Pretty Clause

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

prettyList :: [Clause] -> Doc

Pretty LevelAtom

Methods

pretty :: LevelAtom -> Doc

prettyPrec :: Int -> LevelAtom -> Doc

prettyList :: [LevelAtom] -> Doc

Pretty PlusLevel

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

Pretty Level

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

Pretty Sort

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

Pretty Type

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty Term

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

prettyList :: [Term] -> Doc

Pretty ConHead

Methods

pretty :: ConHead -> Doc

prettyPrec :: Int -> ConHead -> Doc

prettyList :: [ConHead] -> Doc

Pretty CompiledClauses

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

Pretty ScopeCopyInfo

Methods

pretty :: ScopeCopyInfo -> Doc

prettyPrec :: Int -> ScopeCopyInfo -> Doc

prettyList :: [ScopeCopyInfo] -> Doc

Pretty DeclarationWarning

Methods

pretty :: DeclarationWarning -> Doc

prettyPrec :: Int -> DeclarationWarning -> Doc

prettyList :: [DeclarationWarning] -> Doc

Pretty DeclarationException

Methods

pretty :: DeclarationException -> Doc

prettyPrec :: Int -> DeclarationException -> Doc

prettyList :: [DeclarationException] -> Doc

Pretty CallInfo

We only show the name of the callee.

Methods

pretty :: CallInfo -> Doc

prettyPrec :: Int -> CallInfo -> Doc

prettyList :: [CallInfo] -> Doc

Pretty Call

Methods

pretty :: Call -> Doc

prettyPrec :: Int -> Call -> Doc

prettyList :: [Call] -> Doc

Pretty TermHead

Methods

pretty :: TermHead -> Doc

prettyPrec :: Int -> TermHead -> Doc

prettyList :: [TermHead] -> Doc

Pretty Defn

Methods

pretty :: Defn -> Doc

prettyPrec :: Int -> Defn -> Doc

prettyList :: [Defn] -> Doc

Pretty Polarity

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Pretty Definition

Methods

pretty :: Definition -> Doc

prettyPrec :: Int -> Definition -> Doc

prettyList :: [Definition] -> Doc

Pretty DisplayTerm

Methods

pretty :: DisplayTerm -> Doc

prettyPrec :: Int -> DisplayTerm -> Doc

prettyList :: [DisplayTerm] -> Doc

Pretty Section

Methods

pretty :: Section -> Doc

prettyPrec :: Int -> Section -> Doc

prettyList :: [Section] -> Doc

Pretty NamedMeta

Methods

pretty :: NamedMeta -> Doc

prettyPrec :: Int -> NamedMeta -> Doc

prettyList :: [NamedMeta] -> Doc

Pretty CompareDirection

Methods

pretty :: CompareDirection -> Doc

prettyPrec :: Int -> CompareDirection -> Doc

prettyList :: [CompareDirection] -> Doc

Pretty Comparison

Methods

pretty :: Comparison -> Doc

prettyPrec :: Int -> Comparison -> Doc

prettyList :: [Comparison] -> Doc

Pretty Interface

Methods

pretty :: Interface -> Doc

prettyPrec :: Int -> Interface -> Doc

prettyList :: [Interface] -> Doc

Pretty ProblemId

Methods

pretty :: ProblemId -> Doc

prettyPrec :: Int -> ProblemId -> Doc

prettyList :: [ProblemId] -> Doc

Pretty ResolvedName

Methods

pretty :: ResolvedName -> Doc

prettyPrec :: Int -> ResolvedName -> Doc

prettyList :: [ResolvedName] -> Doc

Pretty AsBinding

Methods

pretty :: AsBinding -> Doc

prettyPrec :: Int -> AsBinding -> Doc

prettyList :: [AsBinding] -> Doc

Pretty BlockingVar

Methods

pretty :: BlockingVar -> Doc

prettyPrec :: Int -> BlockingVar -> Doc

prettyList :: [BlockingVar] -> Doc

Pretty Node

Methods

pretty :: Node -> Doc

prettyPrec :: Int -> Node -> Doc

prettyList :: [Node] -> Doc

Pretty SizeMeta

Methods

pretty :: SizeMeta -> Doc

prettyPrec :: Int -> SizeMeta -> Doc

prettyList :: [SizeMeta] -> Doc

Pretty NamedRigid

Methods

pretty :: NamedRigid -> Doc

prettyPrec :: Int -> NamedRigid -> Doc

prettyList :: [NamedRigid] -> Doc

Pretty Cl

Methods

pretty :: Cl -> Doc

prettyPrec :: Int -> Cl -> Doc

prettyList :: [Cl] -> Doc

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).

Methods

pretty :: CallPath -> Doc

prettyPrec :: Int -> CallPath -> Doc

prettyList :: [CallPath] -> Doc

Pretty a => Pretty [a]

Methods

pretty :: [a] -> Doc

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

prettyList :: [[a]] -> Doc

Pretty a => Pretty (Maybe a)

Methods

pretty :: Maybe a -> Doc

prettyPrec :: Int -> Maybe a -> Doc

prettyList :: [Maybe a] -> Doc

Pretty flex => Pretty (PolarityAssignment flex)

Methods

pretty :: PolarityAssignment flex -> Doc

prettyPrec :: Int -> PolarityAssignment flex -> Doc

prettyList :: [PolarityAssignment flex] -> Doc

Pretty a => Pretty (Lisp a)

Methods

pretty :: Lisp a -> Doc

prettyPrec :: Int -> Lisp a -> Doc

prettyList :: [Lisp a] -> 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

prettyList :: [Benchmark a] -> Doc

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

Methods

pretty :: PrintRange a -> Doc

prettyPrec :: Int -> PrintRange a -> Doc

prettyList :: [PrintRange a] -> Doc

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

Methods

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

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

prettyList :: [Range' (Maybe a)] -> Doc

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

Methods

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

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

prettyList :: [Interval' (Maybe a)] -> Doc

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

Methods

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

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

prettyList :: [Position' (Maybe a)] -> Doc

Pretty a => Pretty (QNamed a)

Methods

pretty :: QNamed a -> Doc

prettyPrec :: Int -> QNamed a -> Doc

prettyList :: [QNamed a] -> Doc

Pretty cinfo => Pretty (CMSet cinfo)

Methods

pretty :: CMSet cinfo -> Doc

prettyPrec :: Int -> CMSet cinfo -> Doc

prettyList :: [CMSet cinfo] -> Doc

Pretty cinfo => Pretty (CallMatrixAug cinfo)

Methods

pretty :: CallMatrixAug cinfo -> Doc

prettyPrec :: Int -> CallMatrixAug cinfo -> Doc

prettyList :: [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

prettyList :: [CallGraph cinfo] -> Doc

Pretty a => Pretty (Substitution' a)

Methods

pretty :: Substitution' a -> Doc

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

prettyList :: [Substitution' a] -> Doc

Pretty a => Pretty (Pattern' a)

Methods

pretty :: Pattern' a -> Doc

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

prettyList :: [Pattern' a] -> Doc

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

Methods

pretty :: Tele (Dom a) -> Doc

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

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

Pretty tm => Pretty (Elim' tm)

Methods

pretty :: Elim' tm -> Doc

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

prettyList :: [Elim' tm] -> Doc

Pretty a => Pretty (SplitTreeLabel a)

Methods

pretty :: SplitTreeLabel a -> Doc

prettyPrec :: Int -> SplitTreeLabel a -> Doc

prettyList :: [SplitTreeLabel a] -> Doc

Pretty a => Pretty (SplitTree' a)

Methods

pretty :: SplitTree' a -> Doc

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

prettyList :: [SplitTree' a] -> Doc

Pretty a => Pretty (Case a)

Methods

pretty :: Case a -> Doc

prettyPrec :: Int -> Case a -> Doc

prettyList :: [Case a] -> Doc

Pretty a => Pretty (WithArity a)

Methods

pretty :: WithArity a -> Doc

prettyPrec :: Int -> WithArity a -> Doc

prettyList :: [WithArity a] -> Doc

(Pretty r, Pretty f) => Pretty (Solution r f)

Methods

pretty :: Solution r f -> Doc

prettyPrec :: Int -> Solution r f -> Doc

prettyList :: [Solution r f] -> Doc

(Pretty r, Pretty f) => Pretty (Constraint' r f)

Methods

pretty :: Constraint' r f -> Doc

prettyPrec :: Int -> Constraint' r f -> Doc

prettyList :: [Constraint' r f] -> Doc

(Pretty r, Pretty f) => Pretty (SizeExpr' r f)

Methods

pretty :: SizeExpr' r f -> Doc

prettyPrec :: Int -> SizeExpr' r f -> Doc

prettyList :: [SizeExpr' r f] -> Doc

(Pretty rigid, Pretty flex) => Pretty (Node rigid flex)

Methods

pretty :: Node rigid flex -> Doc

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

prettyList :: [Node rigid flex] -> Doc

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

Methods

pretty :: Matrix i b -> Doc

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

prettyList :: [Matrix i b] -> Doc

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

Methods

pretty :: OutputConstraint' a b -> Doc

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

prettyList :: [OutputConstraint' a b] -> Doc

(Pretty s, Pretty t, Pretty e) => Pretty (Edge s t e)

Methods

pretty :: Edge s t e -> Doc

prettyPrec :: Int -> Edge s t e -> Doc

prettyList :: [Edge s t e] -> Doc

(Pretty s, Pretty t, Pretty e) => Pretty (Graph s t e)

Methods

pretty :: Graph s t e -> Doc

prettyPrec :: Int -> Graph s t e -> Doc

prettyList :: [Graph s t e] -> Doc

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

Pretty instances

Doc utilities

pwords :: String -> [Doc]

fwords :: String -> Doc

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

Comma separated list, without the brackets.

mparens :: Bool -> Doc -> Doc

Apply parens to Doc if boolean is true.

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)

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

a ? b = hang a 2 b

pshow :: Show a => a -> Doc

pshow = text . pretty

module Text.PrettyPrint

Orphan instances

Data Doc

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 :: (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