Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Common.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 Phase Source # 
Instance details

Defined in Agda.Benchmarking

Pretty HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

Pretty CompilerBackend Source # 
Instance details

Defined in Agda.Interaction.Base

Pretty InterfaceFile Source # 
Instance details

Defined in Agda.Interaction.FindFile

Pretty SourceFile Source # 
Instance details

Defined in Agda.Interaction.FindFile

Pretty LibError' Source #

Pretty-print library management error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

Pretty LibParseError Source #

Print library file parse error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

Pretty LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Pretty LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Pretty OptionWarning Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Pretty AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Name -> Doc Source #

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

prettyList :: [Name] -> Doc Source #

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty Suffix Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty BuiltinId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Pretty PrimitiveId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Pretty Access Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Associativity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Cohesion Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Erased Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Modality Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty NotationPart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty OpaqueId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Q1Origin 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 Relevance Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc Source #

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

prettyList :: [Expr] -> Doc Source #

Pretty LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc Source #

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

prettyList :: [LHS] -> Doc Source #

Pretty LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc Source #

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

prettyList :: [RHS] -> Doc Source #

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Pretty DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Pretty DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Pretty DataRecOrFun Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Pretty NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc Source #

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

prettyList :: [Name] -> Doc Source #

Pretty NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty NamedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty Tel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc Source #

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

prettyList :: [Tel] -> Doc Source #

Pretty Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Pretty Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc Source #

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

prettyList :: [Sort] -> Doc Source #

Pretty Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc Source #

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

prettyList :: [Term] -> Doc Source #

Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc Source #

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

prettyList :: [Type] -> Doc Source #

Pretty Blocker Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

Pretty Literal Source # 
Instance details

Defined in Agda.Syntax.Literal

Pretty NewNotation Source # 
Instance details

Defined in Agda.Syntax.Notation

Pretty NotationKind Source # 
Instance details

Defined in Agda.Syntax.Notation

Pretty NotationSection Source # 
Instance details

Defined in Agda.Syntax.Notation

Pretty ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Pretty ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Pretty IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Pretty PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Pretty RangeFile Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Pretty AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty BindingSource 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 NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty FlatScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Flat

Pretty RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Pretty Compiled Source # 
Instance details

Defined in Agda.Compiler.Treeless.Pretty

Pretty TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Pretty

Pretty CallMatrix Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Pretty CallPath Source #

Only show intermediate nodes. (Drop last CallInfo).

Instance details

Defined in Agda.Termination.Monad

Pretty Order Source # 
Instance details

Defined in Agda.Termination.Order

Pretty CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Pretty Cl Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

pretty :: Cl -> Doc Source #

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

prettyList :: [Cl] -> Doc Source #

Pretty BlockingVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Pretty SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Pretty SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Pretty Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Call -> Doc Source #

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

prettyList :: [Call] -> Doc Source #

Pretty CallInfo Source #

We only show the name of the callee.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty ConstructorData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DataOrRecSigData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DatatypeData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Defn -> Doc Source #

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

prettyList :: [Defn] -> Doc Source #

Pretty DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty FunctionData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty MetaInstantiation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty NamedMeta Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty OpaqueBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty PrimitiveData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty PrimitiveSortData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty ProjectionLikenessMissing Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty RecordData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Pretty Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Item -> Doc Source #

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

prettyList :: [Item] -> Doc Source #

Pretty Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Node -> Doc Source #

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

prettyList :: [Node] -> Doc Source #

Pretty Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Pretty Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Lvl -> Doc Source #

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

prettyList :: [Lvl] -> Doc Source #

Pretty Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Nat -> Doc Source #

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

prettyList :: [Nat] -> Doc Source #

Pretty CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Pretty AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Pretty OldSizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes

Pretty OldSizeExpr Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes

Pretty NamedRigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Pretty SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Pretty Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Cmp -> Doc Source #

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

prettyList :: [Cmp] -> Doc Source #

Pretty Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Flex -> Doc Source #

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

prettyList :: [Flex] -> Doc Source #

Pretty Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Rigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Pretty Label Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Pretty Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Pretty CallSite Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Pretty AbsolutePath Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Pretty Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Alt -> Doc Source #

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

prettyList :: [Alt] -> Doc Source #

Pretty Binds 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

Methods

pretty :: Decl -> Doc Source #

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

prettyList :: [Decl] -> Doc Source #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Exp -> Doc Source #

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

prettyList :: [Exp] -> Doc Source #

Pretty ImportDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ImportSpec Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Literal Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ModuleName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty ModulePragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Name Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Name -> Doc Source #

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

prettyList :: [Name] -> Doc Source #

Pretty Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Pat -> Doc Source #

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

prettyList :: [Pat] -> Doc Source #

Pretty QName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty QOp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QOp -> Doc Source #

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

prettyList :: [QOp] -> Doc Source #

Pretty Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Stmt -> Doc Source #

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

prettyList :: [Stmt] -> Doc Source #

Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Pretty Type Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Type -> Doc Source #

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

prettyList :: [Type] -> Doc Source #

Pretty CPUTime Source #

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

Instance details

Defined in Agda.Utils.Time

Pretty Constraint Source # 
Instance details

Defined in Agda.Utils.Warshall

Pretty Node Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: Node -> Doc Source #

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

prettyList :: [Node] -> Doc Source #

Pretty SizeExpr Source # 
Instance details

Defined in Agda.Utils.Warshall

Pretty Weight Source # 
Instance details

Defined in Agda.Utils.Warshall

Pretty Int32 Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Int32 -> Doc Source #

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

prettyList :: [Int32] -> Doc Source #

Pretty CallStack Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Pretty SrcLoc Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Pretty Word64 Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Word64 -> Doc Source #

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

prettyList :: [Word64] -> Doc Source #

Pretty IntSet Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: IntSet -> Doc Source #

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

prettyList :: [IntSet] -> Doc Source #

Pretty Text Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Text -> Doc Source #

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

prettyList :: [Text] -> Doc Source #

Pretty Integer Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Integer -> Doc Source #

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

prettyList :: [Integer] -> Doc Source #

Pretty () Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: () -> Doc Source #

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

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

Pretty Bool Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Bool -> Doc Source #

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

prettyList :: [Bool] -> Doc Source #

Pretty Char Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Char -> Doc Source #

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

prettyList :: [Char] -> Doc Source #

Pretty Double Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Double -> Doc Source #

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

prettyList :: [Double] -> Doc Source #

Pretty Int Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Int -> Doc Source #

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

prettyList :: [Int] -> Doc Source #

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 #

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

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QNamed a -> Doc Source #

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

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

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 (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

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

prettyList :: [Named_ e] -> Doc Source #

Pretty a => Pretty (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Ranged a -> Doc Source #

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

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

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

Defined in Agda.Syntax.Concrete.Pretty

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

Defined in Agda.Syntax.Common

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Binder' a -> Doc Source #

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

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

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 (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Pretty t => Pretty (Abs t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc Source #

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

prettyList :: [Abs t] -> Doc Source #

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc Source #

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

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

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

Defined in Agda.Syntax.Internal

Pretty a => Pretty (Substitution' 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 t => Pretty (NotBlocked' t) Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

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

Defined in Agda.Syntax.Internal.Elim

Methods

pretty :: Elim' tm -> Doc Source #

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

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

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

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

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

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

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

Defined in Agda.Syntax.Common.Pretty

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

Defined in Agda.Syntax.Common.Pretty

Methods

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

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

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

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

Methods

pretty :: CallMatrixAug cinfo -> Doc Source #

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

prettyList :: [CallMatrixAug cinfo] -> 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 a => Pretty (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

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

Defined in Agda.TypeChecking.Coverage.SplitTree

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Interaction.BasicOps

Methods

pretty :: IPFace' c -> Doc Source #

prettyPrec :: Int -> IPFace' c -> Doc Source #

prettyList :: [IPFace' c] -> Doc Source #

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Open a -> Doc Source #

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

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

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

Defined in Agda.TypeChecking.SizedTypes.Syntax

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

Print benchmark as three-column table with totals.

Instance details

Defined in Agda.Utils.Benchmark

Pretty n => Pretty (WithUniqueInt n) Source # 
Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

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

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: List1 a -> Doc Source #

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: IntMap a -> Doc Source #

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Set a -> Doc Source #

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

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

a ~ Aspects => Pretty (Doc a) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Doc a -> Doc0 Source #

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Maybe a -> Doc Source #

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: [a] -> Doc Source #

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

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

Methods

pretty :: OutputForm a b -> Doc Source #

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

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

(Pretty a, Pretty b) => Pretty (ImportDirective' 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 (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

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

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

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

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

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

Methods

pretty :: SizeExpr' r f -> Doc Source #

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

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

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

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Solution r f -> Doc Source #

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

prettyList :: [Solution r f] -> 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 #

(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 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 k, Pretty v) => Pretty (Map k v) Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Map k v -> Doc Source #

prettyPrec :: Int -> Map k v -> Doc Source #

prettyList :: [Map k v] -> 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 a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: LegendMatrix a b c -> Doc Source #

prettyPrec :: Int -> LegendMatrix a b c -> Doc Source #

prettyList :: [LegendMatrix a b c] -> Doc Source #

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

Defined in Agda.Syntax.Common

Methods

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

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

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

type Doc = Doc Aspects Source #

The type of documents. We use documents annotated by Aspects to record syntactic highlighting information that is generated during pretty-printing.

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

Use instead of show when printing to world.

sep :: Foldable t => t Doc -> Doc Source #

fsep :: Foldable t => t Doc -> Doc Source #

hsep :: Foldable t => t Doc -> Doc Source #

hcat :: Foldable t => t Doc -> Doc Source #

vcat :: Foldable t => t Doc -> Doc Source #

punctuate :: Foldable t => Doc -> t Doc -> [Doc] Source #

parens Source #

Arguments

:: Doc 
-> Doc

Wrap document in (...)

brackets Source #

Arguments

:: Doc 
-> Doc

Wrap document in [...]

braces Source #

Arguments

:: Doc 
-> Doc

Wrap document in {...}

quotes Source #

Arguments

:: Doc 
-> Doc

Wrap document in '...'

doubleQuotes Source #

Arguments

:: Doc 
-> Doc

Wrap document in "..."

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

Comma separated list, without the brackets.

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

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

pshow = text . show

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

Pretty print a set.

prettyMap :: (Pretty k, Pretty v) => [(k, v)] -> Doc Source #

Pretty print an association list.

pwords :: String -> [Doc] Source #

fwords :: String -> Doc Source #

hsepWith :: Doc -> Doc -> Doc -> Doc Source #

Separate, but only if both separees are not null.

prettyAssign :: (Pretty k, Pretty v) => (k, v) -> Doc Source #

Pretty print a single association.

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

Apply parens to Doc if boolean is true.

parensNonEmpty :: Doc -> Doc Source #

Only wrap in parens if not empty

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

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

Used for with-like telescopes

annotateAspect :: Aspect -> Doc -> Doc Source #

Attach a simple Aspect, rather than a full set of Aspects, to a document.

data Mode #

Instances

Instances details
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

Show Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Mode -> ShowS

show :: Mode -> String

showList :: [Mode] -> ShowS

Eq Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

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

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

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

data Style #

Constructors

Style 

Fields

Instances

Instances details
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

Show Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Style -> ShowS

show :: Style -> String

showList :: [Style] -> ShowS

Eq Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

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

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

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 Span a #

Constructors

Span 

Fields

Instances

Instances details
Functor Span 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

fmap :: (a -> b) -> Span a -> Span b

(<$) :: a -> Span b -> Span a #

Show a => Show (Span a) 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Span a -> ShowS

show :: Span a -> String

showList :: [Span a] -> ShowS

Eq a => Eq (Span a) 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(==) :: Span a -> Span a -> Bool

(/=) :: Span a -> Span a -> Bool

pattern Chr :: !Char -> TextDetails #

pattern PStr :: String -> TextDetails #

text :: String -> Doc a #

render :: Doc a -> String #

char :: Char -> Doc a #

integer :: Integer -> Doc a #

isEmpty :: Doc a -> Bool #

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

cat :: [Doc a] -> Doc a #

($$) :: Doc a -> Doc a -> Doc a #

annotate :: a -> Doc a -> Doc a #

($+$) :: Doc a -> Doc a -> Doc a #

nest :: Int -> Doc a -> Doc a #

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

double :: Double -> Doc a #

fcat :: [Doc a] -> Doc a #

float :: Float -> Doc a #

fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc b -> a #

fullRenderAnn :: Mode -> Int -> Float -> (AnnotDetails b -> a -> a) -> a -> Doc b -> a #

int :: Int -> Doc a #

ptext :: String -> Doc a #

rational :: Rational -> Doc a #

renderSpans :: Doc ann -> (String, [Span ann]) #

renderStyle :: Style -> Doc a -> String #

sizedText :: Int -> String -> Doc a #

zeroWidthText :: String -> Doc a #

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