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

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.Pretty

Contents

- Orphan instances

Description

Pretty printing functions.

Synopsis

- class Pretty a where
  - pretty :: a -> Doc
  - prettyPrec :: Int -> a -> Doc
  - prettyList :: [a] -> Doc
- prettyShow :: Pretty a => a -> String
- pwords :: String -> [Doc]
- fwords :: String -> Doc
- prettyList_ :: Pretty a => [a] -> Doc
- mparens :: Bool -> Doc -> Doc
- align :: Int -> [(String, Doc)] -> Doc
- multiLineText :: String -> Doc
- (<?>) :: Doc -> Doc -> Doc
- pshow :: Show a => a -> Doc
- fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc -> a
- renderStyle :: Style -> Doc -> String
- render :: Doc -> String
- fsep :: [Doc] -> Doc
- fcat :: [Doc] -> Doc
- cat :: [Doc] -> Doc
- sep :: [Doc] -> Doc
- (<+>) :: Doc -> Doc -> Doc
- (<>) :: Doc -> Doc -> Doc
- ($+$) :: Doc -> Doc -> Doc
- ($$) :: Doc -> Doc -> Doc
- punctuate :: Doc -> [Doc] -> [Doc]
- hang :: Doc -> Int -> Doc -> Doc
- nest :: Int -> Doc -> Doc
- vcat :: [Doc] -> Doc
- hsep :: [Doc] -> Doc
- hcat :: [Doc] -> Doc
- braces :: Doc -> Doc
- brackets :: Doc -> Doc
- parens :: Doc -> Doc
- doubleQuotes :: Doc -> Doc
- quotes :: Doc -> Doc
- rational :: Rational -> Doc
- double :: Double -> Doc
- float :: Float -> Doc
- integer :: Integer -> Doc
- int :: Int -> Doc
- rbrace :: Doc
- lbrace :: Doc
- rbrack :: Doc
- lbrack :: Doc
- rparen :: Doc
- lparen :: Doc
- equals :: Doc
- space :: Doc
- colon :: Doc
- comma :: Doc
- semi :: Doc
- isEmpty :: Doc -> Bool
- zeroWidthText :: String -> Doc
- sizedText :: Int -> String -> Doc
- ptext :: String -> Doc
- text :: String -> Doc
- char :: Char -> Doc
- data Doc
- style :: Style
- pattern Chr :: !Char -> TextDetails
- pattern PStr :: String -> TextDetails
- data Style = Style {
  - mode :: Mode
  - lineLength :: Int
  - ribbonsPerLine :: Float
  }
- data Mode
  - = PageMode
  - | ZigZagMode
  - | LeftMode
  - | OneLineMode

# 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

Pretty Bool Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Bool -> Doc Source # prettyPrec :: Int -> Bool -> Doc Source # prettyList :: [Bool] -> Doc Source #
Pretty Char Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Char -> Doc Source # prettyPrec :: Int -> Char -> Doc Source # prettyList :: [Char] -> Doc Source #
Pretty Int Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Int -> Doc Source # prettyPrec :: Int -> Int -> Doc Source # prettyList :: [Int] -> Doc Source #
Pretty Int32 Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Int32 -> Doc Source # prettyPrec :: Int -> Int32 -> Doc Source # prettyList :: [Int32] -> Doc Source #
Pretty Integer Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Integer -> Doc Source # prettyPrec :: Int -> Integer -> Doc Source # prettyList :: [Integer] -> Doc Source #
Pretty () Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: () -> Doc Source # prettyPrec :: Int -> () -> Doc Source # prettyList :: [()] -> Doc Source #
Pretty Doc Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Doc -> Doc Source # prettyPrec :: Int -> Doc -> Doc Source # prettyList :: [Doc] -> Doc Source #
Pretty TyVarBind Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: TyVarBind -> Doc Source # prettyPrec :: Int -> TyVarBind -> Doc Source # prettyList :: [TyVarBind] -> Doc Source #
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 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 QName Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
Pretty ModuleName Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source #
Pretty Literal Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Literal -> Doc Source # prettyPrec :: Int -> Literal -> Doc Source # prettyList :: [Literal] -> Doc Source #
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 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 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 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 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 Match Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Match -> Doc Source # prettyPrec :: Int -> Match -> Doc Source # prettyList :: [Match] -> Doc Source #
Pretty Binds Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Binds -> Doc Source # prettyPrec :: Int -> Binds -> Doc Source # prettyList :: [Binds] -> Doc Source #
Pretty Strictness Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Strictness -> Doc Source # prettyPrec :: Int -> Strictness -> Doc Source # prettyList :: [Strictness] -> Doc Source #
Pretty ConDecl Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ConDecl -> Doc Source # prettyPrec :: Int -> ConDecl -> Doc Source # prettyList :: [ConDecl] -> Doc Source #
Pretty DataOrNew Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: DataOrNew -> Doc Source # prettyPrec :: Int -> DataOrNew -> Doc Source # prettyList :: [DataOrNew] -> Doc Source #
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 ImportSpec Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ImportSpec -> Doc Source # prettyPrec :: Int -> ImportSpec -> Doc Source # prettyList :: [ImportSpec] -> Doc Source #
Pretty ImportDecl Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ImportDecl -> Doc Source # prettyPrec :: Int -> ImportDecl -> Doc Source # prettyList :: [ImportDecl] -> Doc Source #
Pretty ModulePragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ModulePragma -> Doc Source # prettyPrec :: Int -> ModulePragma -> Doc Source # prettyList :: [ModulePragma] -> Doc Source #
Pretty Module Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Module -> Doc Source # prettyPrec :: Int -> Module -> Doc Source # prettyList :: [Module] -> Doc Source #
Pretty Polarity Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Polarity -> Doc Source # prettyPrec :: Int -> Polarity -> Doc Source # prettyList :: [Polarity] -> Doc Source #
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 Rigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Rigid -> Doc Source # prettyPrec :: Int -> Rigid -> Doc Source # prettyList :: [Rigid] -> Doc Source #
Pretty Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Offset -> Doc Source # prettyPrec :: Int -> Offset -> Doc Source # prettyList :: [Offset] -> Doc Source #
Pretty CPUTime Source # | Print CPU time in milli (10^-3) seconds.
Instance details Defined in Agda.Utils.Time Methods pretty :: CPUTime -> Doc Source # prettyPrec :: Int -> CPUTime -> Doc Source # prettyList :: [CPUTime] -> Doc Source #
Pretty LibWarning' Source # |
Instance details Defined in Agda.Interaction.Library Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source #
Pretty AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> Doc Source #
Pretty IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: IntervalWithoutFile -> Doc Source # prettyPrec :: Int -> IntervalWithoutFile -> Doc Source # prettyList :: [IntervalWithoutFile] -> Doc Source #
Pretty PositionWithoutFile Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: PositionWithoutFile -> Doc Source # prettyPrec :: Int -> PositionWithoutFile -> Doc Source # prettyList :: [PositionWithoutFile] -> Doc Source #
Pretty Fixity' Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity' -> Doc Source # prettyPrec :: Int -> Fixity' -> Doc Source # prettyList :: [Fixity'] -> Doc Source #
Pretty InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source #
Pretty MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: MetaId -> Doc Source # prettyPrec :: Int -> MetaId -> Doc Source # prettyList :: [MetaId] -> Doc Source #
Pretty NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: NameId -> Doc Source # prettyPrec :: Int -> NameId -> Doc Source # prettyList :: [NameId] -> Doc Source #
Pretty Access Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Access -> Doc Source # prettyPrec :: Int -> Access -> Doc Source # prettyList :: [Access] -> Doc Source #
Pretty Relevance Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Relevance -> Doc Source # prettyPrec :: Int -> Relevance -> Doc Source # prettyList :: [Relevance] -> Doc Source #
Pretty Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Hiding -> Doc Source # prettyPrec :: Int -> Hiding -> Doc Source # prettyList :: [Hiding] -> Doc Source #
Pretty Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Induction -> Doc Source # prettyPrec :: Int -> Induction -> Doc Source # prettyList :: [Induction] -> Doc Source #
Pretty FileType Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: FileType -> Doc Source # prettyPrec :: Int -> FileType -> Doc Source # prettyList :: [FileType] -> Doc Source #
Pretty ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source #
Pretty ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source #
Pretty GenPart Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: GenPart -> Doc Source # prettyPrec :: Int -> GenPart -> Doc Source # prettyList :: [GenPart] -> Doc Source #
Pretty TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
Pretty QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
Pretty NamePart Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods pretty :: NamePart -> Doc Source # prettyPrec :: Int -> NamePart -> Doc Source # prettyList :: [NamePart] -> Doc Source #
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 AmbiguousQName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: AmbiguousQName -> Doc Source # prettyPrec :: Int -> AmbiguousQName -> Doc Source # prettyList :: [AmbiguousQName] -> Doc Source #
Pretty ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source #
Pretty QName Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
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 Literal Source # |
Instance details Defined in Agda.Syntax.Literal Methods pretty :: Literal -> Doc Source # prettyPrec :: Int -> Literal -> Doc Source # prettyList :: [Literal] -> Doc Source #
Pretty TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Pretty Methods pretty :: TTerm -> Doc Source # prettyPrec :: Int -> TTerm -> Doc Source # prettyList :: [TTerm] -> Doc Source #
Pretty Precedence Source # |
Instance details Defined in Agda.Syntax.Fixity Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> Doc Source #
Pretty Fixity Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity -> Doc Source # prettyPrec :: Int -> Fixity -> Doc Source # prettyList :: [Fixity] -> Doc Source #
Pretty Label Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods pretty :: Label -> Doc Source # prettyPrec :: Int -> Label -> Doc Source # prettyList :: [Label] -> Doc Source #
Pretty Weight Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods pretty :: Weight -> Doc Source # prettyPrec :: Int -> Weight -> Doc Source # prettyList :: [Weight] -> Doc Source #
Pretty Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: Occurrence -> Doc Source # prettyPrec :: Int -> Occurrence -> Doc Source # prettyList :: [Occurrence] -> Doc Source #
Pretty Where Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: Where -> Doc Source # prettyPrec :: Int -> Where -> Doc Source # prettyList :: [Where] -> Doc Source #
Pretty OccursWhere Source # |
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods pretty :: OccursWhere -> Doc Source # prettyPrec :: Int -> OccursWhere -> Doc Source # prettyList :: [OccursWhere] -> Doc Source #
Pretty Pragma Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pragma -> Doc Source # prettyPrec :: Int -> Pragma -> Doc Source # prettyList :: [Pragma] -> Doc Source #
Pretty OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source #
Pretty ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleApplication -> Doc Source # prettyPrec :: Int -> ModuleApplication -> Doc Source # prettyList :: [ModuleApplication] -> Doc Source #
Pretty Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source #
Pretty LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamClause -> Doc Source # prettyPrec :: Int -> LamClause -> Doc Source # prettyList :: [LamClause] -> Doc Source #
Pretty WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source #
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 LHSCore Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LHSCore -> Doc Source # prettyPrec :: Int -> LHSCore -> Doc Source # prettyList :: [LHSCore] -> 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 TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source #
Pretty BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: BoundName -> Doc Source # prettyPrec :: Int -> BoundName -> Doc Source # prettyList :: [BoundName] -> Doc Source #
Pretty LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
Pretty DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: DoStmt -> Doc Source # prettyPrec :: Int -> DoStmt -> Doc Source # prettyList :: [DoStmt] -> Doc Source #
Pretty Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pattern -> Doc Source # prettyPrec :: Int -> Pattern -> Doc Source # prettyList :: [Pattern] -> Doc Source #
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 ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleAssignment -> Doc Source # prettyPrec :: Int -> ModuleAssignment -> Doc Source # prettyList :: [ModuleAssignment] -> Doc Source #
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 NamedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: NamedBinding -> Doc Source # prettyPrec :: Int -> NamedBinding -> Doc Source # prettyList :: [NamedBinding] -> Doc Source #
Pretty Phase Source # |
Instance details Defined in Agda.Benchmarking Methods pretty :: Phase -> Doc Source # prettyPrec :: Int -> Phase -> Doc Source # prettyList :: [Phase] -> Doc Source #
Pretty ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ResolvedName -> Doc Source # prettyPrec :: Int -> ResolvedName -> Doc Source # prettyList :: [ResolvedName] -> Doc Source #
Pretty AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractModule -> Doc Source # prettyPrec :: Int -> AbstractModule -> Doc Source # prettyList :: [AbstractModule] -> Doc Source #
Pretty AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractName -> Doc Source # prettyPrec :: Int -> AbstractName -> Doc Source # prettyList :: [AbstractName] -> Doc Source #
Pretty NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpace -> Doc Source # prettyPrec :: Int -> NameSpace -> Doc Source # prettyList :: [NameSpace] -> Doc Source #
Pretty LocalVar Source # | We show shadowed variables as prefixed by a ".", as not in scope.
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: LocalVar -> Doc Source # prettyPrec :: Int -> LocalVar -> Doc Source # prettyList :: [LocalVar] -> Doc Source #
Pretty ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ScopeInfo -> Doc Source # prettyPrec :: Int -> ScopeInfo -> Doc Source # prettyList :: [ScopeInfo] -> Doc Source #
Pretty NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpaceId -> Doc Source # prettyPrec :: Int -> NameSpaceId -> Doc Source # prettyList :: [NameSpaceId] -> Doc Source #
Pretty Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: Scope -> Doc Source # prettyPrec :: Int -> Scope -> Doc Source # prettyList :: [Scope] -> Doc Source #
Pretty Order Source # |
Instance details Defined in Agda.Termination.Order Methods pretty :: Order -> Doc Source # prettyPrec :: Int -> Order -> Doc Source # prettyList :: [Order] -> Doc Source #
Pretty CallMatrix Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods pretty :: CallMatrix -> Doc Source # prettyPrec :: Int -> CallMatrix -> Doc Source # prettyList :: [CallMatrix] -> Doc Source #
Pretty DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: DBPatVar -> Doc Source # prettyPrec :: Int -> DBPatVar -> Doc Source # prettyList :: [DBPatVar] -> Doc Source #
Pretty Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Clause -> Doc Source # prettyPrec :: Int -> Clause -> Doc Source # prettyList :: [Clause] -> Doc Source #
Pretty LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: LevelAtom -> Doc Source # prettyPrec :: Int -> LevelAtom -> Doc Source # prettyList :: [LevelAtom] -> Doc Source #
Pretty PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: PlusLevel -> Doc Source # prettyPrec :: Int -> PlusLevel -> Doc Source # prettyList :: [PlusLevel] -> Doc Source #
Pretty Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Level -> Doc Source # prettyPrec :: Int -> Level -> Doc Source # prettyList :: [Level] -> Doc Source #
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 Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source # prettyList :: [Type] -> 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 ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: ConHead -> Doc Source # prettyPrec :: Int -> ConHead -> Doc Source # prettyList :: [ConHead] -> Doc Source #
Pretty SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods pretty :: SplitTag -> Doc Source # prettyPrec :: Int -> SplitTag -> Doc Source # prettyList :: [SplitTag] -> Doc Source #
Pretty CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
Pretty ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
Pretty DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods pretty :: DeclarationWarning -> Doc Source # prettyPrec :: Int -> DeclarationWarning -> Doc Source # prettyList :: [DeclarationWarning] -> Doc Source #
Pretty DeclarationException Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods pretty :: DeclarationException -> Doc Source # prettyPrec :: Int -> DeclarationException -> Doc Source # prettyList :: [DeclarationException] -> Doc Source #
Pretty NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions Methods pretty :: NiceDeclaration -> Doc Source # prettyPrec :: Int -> NiceDeclaration -> Doc Source # prettyList :: [NiceDeclaration] -> Doc Source #
Pretty LibWarning Source # |
Instance details Defined in Agda.Interaction.Library Methods pretty :: LibWarning -> Doc Source # prettyPrec :: Int -> LibWarning -> Doc Source # prettyList :: [LibWarning] -> Doc Source #
Pretty CallInfo Source # | We only `show` the name of the callee.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CallInfo -> Doc Source # prettyPrec :: Int -> CallInfo -> Doc Source # prettyList :: [CallInfo] -> Doc Source #
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 TermHead Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: TermHead -> Doc Source # prettyPrec :: Int -> TermHead -> Doc Source # prettyList :: [TermHead] -> Doc Source #
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 Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Polarity -> Doc Source # prettyPrec :: Int -> Polarity -> Doc Source # prettyList :: [Polarity] -> Doc Source #
Pretty Definition Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Definition -> Doc Source # prettyPrec :: Int -> Definition -> Doc Source # prettyList :: [Definition] -> Doc Source #
Pretty DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: DisplayTerm -> Doc Source # prettyPrec :: Int -> DisplayTerm -> Doc Source # prettyList :: [DisplayTerm] -> Doc Source #
Pretty Section Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Section -> Doc Source # prettyPrec :: Int -> Section -> Doc Source # prettyList :: [Section] -> Doc Source #
Pretty NamedMeta Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: NamedMeta -> Doc Source # prettyPrec :: Int -> NamedMeta -> Doc Source # prettyList :: [NamedMeta] -> Doc Source #
Pretty CompareDirection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CompareDirection -> Doc Source # prettyPrec :: Int -> CompareDirection -> Doc Source # prettyList :: [CompareDirection] -> Doc Source #
Pretty Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source #
Pretty Interface Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Interface -> Doc Source # prettyPrec :: Int -> Interface -> Doc Source # prettyList :: [Interface] -> Doc Source #
Pretty CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CheckpointId -> Doc Source # prettyPrec :: Int -> CheckpointId -> Doc Source # prettyList :: [CheckpointId] -> Doc Source #
Pretty ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ProblemId -> Doc Source # prettyPrec :: Int -> ProblemId -> Doc Source # prettyList :: [ProblemId] -> Doc Source #
Pretty DeepSizeView Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods pretty :: DeepSizeView -> Doc Source # prettyPrec :: Int -> DeepSizeView -> Doc Source # prettyList :: [DeepSizeView] -> Doc Source #
Pretty OldSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods pretty :: OldSizeConstraint -> Doc Source # prettyPrec :: Int -> OldSizeConstraint -> Doc Source # prettyList :: [OldSizeConstraint] -> Doc Source #
Pretty OldSizeExpr Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes Methods pretty :: OldSizeExpr -> Doc Source # prettyPrec :: Int -> OldSizeExpr -> Doc Source # prettyList :: [OldSizeExpr] -> Doc Source #
Pretty AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods pretty :: AsBinding -> Doc Source # prettyPrec :: Int -> AsBinding -> Doc Source # prettyList :: [AsBinding] -> 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 BlockingVar Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods pretty :: BlockingVar -> Doc Source # prettyPrec :: Int -> BlockingVar -> Doc Source # prettyList :: [BlockingVar] -> Doc Source #
Pretty SplitPatVar Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods pretty :: SplitPatVar -> Doc Source # prettyPrec :: Int -> SplitPatVar -> Doc Source # prettyList :: [SplitPatVar] -> Doc Source #
Pretty CallPath Source # | Only show intermediate nodes. (Drop last `CallInfo`).
Instance details Defined in Agda.Termination.Monad Methods pretty :: CallPath -> Doc Source # prettyPrec :: Int -> CallPath -> Doc Source # prettyList :: [CallPath] -> Doc Source #
Pretty SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods pretty :: SizeMeta -> Doc Source # prettyPrec :: Int -> SizeMeta -> Doc Source # prettyList :: [SizeMeta] -> Doc Source #
Pretty NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods pretty :: NamedRigid -> Doc Source # prettyPrec :: Int -> NamedRigid -> Doc Source # prettyList :: [NamedRigid] -> Doc Source #
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 HaskellPragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods pretty :: HaskellPragma -> Doc Source # prettyPrec :: Int -> HaskellPragma -> Doc Source # prettyList :: [HaskellPragma] -> Doc Source #
Pretty a => Pretty [a] Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: [a] -> Doc Source # prettyPrec :: Int -> [a] -> Doc Source # prettyList :: [[a]] -> Doc Source #
Pretty a => Pretty (Maybe a) Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Maybe a -> Doc Source # prettyPrec :: Int -> Maybe a -> Doc Source # prettyList :: [Maybe a] -> Doc Source #
Pretty a => Pretty (NonemptyList a) Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: NonemptyList a -> Doc Source # prettyPrec :: Int -> NonemptyList a -> Doc Source # prettyList :: [NonemptyList a] -> Doc Source #
Pretty flex => Pretty (PolarityAssignment flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: PolarityAssignment flex -> Doc Source # prettyPrec :: Int -> PolarityAssignment flex -> Doc Source # prettyList :: [PolarityAssignment flex] -> 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 #
(Ord a, Pretty a) => Pretty (Benchmark a) Source # | Print benchmark as three-column table with totals.
Instance details Defined in Agda.Utils.Benchmark Methods pretty :: Benchmark a -> Doc Source # prettyPrec :: Int -> Benchmark a -> Doc Source # prettyList :: [Benchmark a] -> Doc Source #
(Pretty a, HasRange a) => Pretty (PrintRange a) Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: PrintRange a -> Doc Source # prettyPrec :: Int -> PrintRange a -> Doc Source # prettyList :: [PrintRange a] -> Doc Source #
Pretty a => Pretty (Range' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Position Methods pretty :: Range' (Maybe a) -> Doc Source # prettyPrec :: Int -> Range' (Maybe a) -> Doc Source # prettyList :: [Range' (Maybe a)] -> Doc Source #
Pretty a => Pretty (Interval' (Maybe a)) Source # |
Instance details Defined in Agda.Syntax.Position 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.Position Methods pretty :: Position' (Maybe a) -> Doc Source # prettyPrec :: Int -> Position' (Maybe a) -> Doc Source # prettyList :: [Position' (Maybe a)] -> Doc Source #
Pretty a => Pretty (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: MaybePlaceholder a -> Doc Source # prettyPrec :: Int -> MaybePlaceholder a -> Doc Source # prettyList :: [MaybePlaceholder a] -> Doc Source #
Pretty a => Pretty (Ranged a) Source # |
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 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 (Dom a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Dom a -> Doc Source # prettyPrec :: Int -> Dom a -> Doc Source # prettyList :: [Dom 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 (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding 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 (ThingWithFixity Name) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
Pretty a => Pretty (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: FieldAssignment' a -> Doc Source # prettyPrec :: Int -> FieldAssignment' a -> Doc Source # prettyList :: [FieldAssignment' a] -> Doc Source #
Pretty (OpApp Expr) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpApp Expr -> Doc Source # prettyPrec :: Int -> OpApp Expr -> Doc Source # prettyList :: [OpApp Expr] -> 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 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 a => Pretty (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source #
Pretty a => Pretty (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Pattern' a -> Doc Source # prettyPrec :: Int -> Pattern' a -> Doc Source # prettyList :: [Pattern' a] -> Doc Source #
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 tm => Pretty (Elim' tm) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Elim' tm -> Doc Source # prettyPrec :: Int -> Elim' tm -> Doc Source # prettyList :: [Elim' tm] -> Doc Source #
Pretty a => Pretty (SplitTreeLabel a) Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods pretty :: SplitTreeLabel a -> Doc Source # prettyPrec :: Int -> SplitTreeLabel a -> Doc Source # prettyList :: [SplitTreeLabel a] -> Doc Source #
Pretty a => Pretty (SplitTree' a) Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitTree Methods pretty :: SplitTree' a -> Doc Source # prettyPrec :: Int -> SplitTree' a -> Doc Source # prettyList :: [SplitTree' a] -> 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 Methods pretty :: WithArity a -> Doc Source # prettyPrec :: Int -> WithArity a -> Doc Source # prettyList :: [WithArity a] -> 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 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 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 r, Pretty f) => Pretty (Constraint' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Constraint' r f -> Doc Source # prettyPrec :: Int -> Constraint' r f -> Doc Source # prettyList :: [Constraint' r f] -> Doc Source #
(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 a, Pretty b) => Pretty (ImportedName' a b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ImportedName' a b -> Doc Source # prettyPrec :: Int -> ImportedName' a b -> Doc Source # prettyList :: [ImportedName' 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 a, Pretty b) => Pretty (ImportDirective' a b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ImportDirective' a b -> Doc Source # prettyPrec :: Int -> ImportDirective' a b -> Doc Source # prettyList :: [ImportDirective' a b] -> 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 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 #
(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 a, Pretty b) => Pretty (OutputConstraint' a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint' a b -> Doc Source # prettyPrec :: Int -> OutputConstraint' a b -> Doc Source # prettyList :: [OutputConstraint' a b] -> Doc Source #
(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint a b -> Doc Source # prettyPrec :: Int -> OutputConstraint a b -> Doc Source # prettyList :: [OutputConstraint a b] -> Doc Source #
(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 #

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

Use instead of `show` when printing to world.

pwords :: String -> [Doc] Source #

fwords :: String -> Doc Source #

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

Comma separated list, without the brackets.

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

Apply `parens` to `Doc` if boolean is true.

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

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

    pshow = text . pretty

fullRender Source #

Arguments

:: Mode | Rendering mode.
-> Int | Line length.
-> Float | Ribbons per line.
-> (TextDetails -> a -> a) | What to do with text.
-> a | What to do at the end.
-> Doc | The document.
-> a | Result.

The general rendering interface. Please refer to the `Style` and `Mode` types for a description of rendering mode, line length and ribbons.

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

Render the `Doc` to a String using the given `Style`.

render :: Doc -> String Source #

Render the `Doc` to a String using the default `Style` (see `style`).

fsep :: [Doc] -> Doc Source #

"Paragraph fill" version of `sep`.

fcat :: [Doc] -> Doc Source #

"Paragraph fill" version of `cat`.

cat :: [Doc] -> Doc Source #

Either `hcat` or `vcat`.

sep :: [Doc] -> Doc Source #

Either `hsep` or `vcat`.

(<+>) :: Doc -> Doc -> Doc infixl 6 Source #

Beside, separated by space, unless one of the arguments is `empty`. `<+>` is associative, with identity `empty`.

(<>) :: Doc -> Doc -> Doc infixl 6 Source #

Beside. `<>` is associative, with identity `empty`.

($+$) :: Doc -> Doc -> Doc infixl 5 Source #

Above, with no overlapping. `$+$` is associative, with identity `empty`.

($$) :: Doc -> Doc -> Doc infixl 5 Source #

Above, except that if the last line of the first argument stops at least one position before the first line of the second begins, these two lines are overlapped. For example:

       text "hi" $$ nest 5 (text "there")

lays out as

       hi   there

rather than

       hi
            there

`$$` is associative, with identity `empty`, and also satisfies

- `(x `$$` y) `<>` z = x `$$` (y `<>` z)`, if `y` non-empty.

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

    punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]

hang :: Doc -> Int -> Doc -> Doc Source #

    hang d1 n d2 = sep [d1, nest n d2]

nest :: Int -> Doc -> Doc Source #

Nest (or indent) a document by a given number of positions (which may also be negative). `nest` satisfies the laws:

-     nest 0 x = x

-     nest k (nest k' x) = nest (k+k') x

-     nest k (x <> y) = nest k x <> nest k y

-     nest k (x $$ y) = nest k x $$ nest k y

-     nest k empty = empty

- `x `<>` `nest` k y = x `<>` y`, if `x` non-empty

The side condition on the last law is needed because `empty` is a left identity for `<>`.

vcat :: [Doc] -> Doc Source #

List version of `$$`.

hsep :: [Doc] -> Doc Source #

List version of `<+>`.

hcat :: [Doc] -> Doc Source #

List version of `<>`.

braces Source #

Arguments

:: Doc |
-> Doc | Wrap document in `{...}`

brackets Source #

Arguments

:: Doc |
-> Doc | Wrap document in `[...]`

parens Source #

Arguments

:: Doc |
-> Doc | Wrap document in `(...)`

doubleQuotes Source #

Arguments

:: Doc |
-> Doc | Wrap document in `"..."`

quotes Source #

Arguments

:: Doc |
-> Doc | Wrap document in `'...'`

rational Source #

Arguments

:: Rational |

-> Doc

    rational n = text (show n)

double Source #

Arguments

:: Double |

-> Doc

    double n = text (show n)

float Source #

Arguments

:: Float |

-> Doc

    float n = text (show n)

integer Source #

Arguments

:: Integer |

-> Doc

    integer n = text (show n)

int Source #

Arguments

:: Int |

-> Doc

    int n = text (show n)

rbrace Source #

Arguments

:: Doc | A '}' character

lbrace Source #

Arguments

:: Doc | A '{' character

rbrack Source #

Arguments

:: Doc | A ']' character

lbrack Source #

Arguments

:: Doc | A '[' character

rparen Source #

Arguments

:: Doc | A ')' character

lparen Source #

Arguments

:: Doc | A '(' character

equals Source #

Arguments

:: Doc | A '=' character

space Source #

Arguments

:: Doc | A space character

colon Source #

Arguments

:: Doc | A `:` character

comma Source #

Arguments

:: Doc | A ',' character

semi Source #

Arguments

:: Doc | A ';' character

isEmpty :: Doc -> Bool Source #

Returns `True` if the document is empty

zeroWidthText :: String -> Doc Source #

Some text, but without any width. Use for non-printing text such as a HTML or Latex tags

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

Some text with any width. (`text s = sizedText (length s) s`)

ptext :: String -> Doc Source #

Same as `text`. Used to be used for Bytestrings.

text :: String -> Doc Source #

A document of height 1 containing a literal string. `text` satisfies the following laws:

-     text s <> text t = text (s++t)

- ``text` "" `<>` x = x`, if `x` non-empty

The side condition on the last law is necessary because ``text` ""` has height 1, while `empty` has no height.

char :: Char -> Doc Source #

A document of height and width 1, containing a literal character.

data Doc Source #

The abstract type of documents. A Doc represents a set of layouts. A Doc with no occurrences of Union or NoDoc represents just one layout.

Instances

Eq Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (==) :: Doc -> Doc -> Bool Source # (/=) :: Doc -> Doc -> Bool Source #
Data Doc Source # |

Instance details

Defined in Agda.Utils.Pretty

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc Source #

toConstr :: Doc -> Constr Source #

dataTypeOf :: Doc -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) Source #

gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source #

Show Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods showsPrec :: Int -> Doc -> ShowS Source # show :: Doc -> String Source # showList :: [Doc] -> ShowS Source #
IsString Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods fromString :: String -> Doc Source #
Generic Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Associated Types type Rep Doc :: Type -> Type Source # Methods from :: Doc -> Rep Doc x Source # to :: Rep Doc x -> Doc Source #
Semigroup Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (<>) :: Doc -> Doc -> Doc Source # sconcat :: NonEmpty Doc -> Doc Source # stimes :: Integral b => b -> Doc -> Doc Source #
Monoid Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods mempty :: Doc Source # mappend :: Doc -> Doc -> Doc Source # mconcat :: [Doc] -> Doc Source #
NFData Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods rnf :: Doc -> () Source #
Null Doc Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: Doc Source # null :: Doc -> Bool Source #
Pretty Doc Source # |
Instance details Defined in Agda.Utils.Pretty Methods pretty :: Doc -> Doc Source # prettyPrec :: Int -> Doc -> Doc Source # prettyList :: [Doc] -> Doc Source #
Underscore Doc Source # |
Instance details Defined in Agda.Syntax.Common Methods underscore :: Doc Source # isUnderscore :: Doc -> Bool Source #
EmbPrj Doc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Int32 Source # icod_ :: Doc -> S Int32 Source # value :: Int32 -> R Doc Source #
Null (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc Source # null :: TCM Doc -> Bool Source #
type Rep Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ type Rep Doc = D1 (MetaData "Doc" "Text.PrettyPrint.HughesPJ" "pretty-1.1.3.6" True) (C1 (MetaCons "Doc" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Doc ()))))

style :: Style Source #

The default style (`mode=PageMode, lineLength=100, ribbonsPerLine=1.5`).

pattern Chr :: !Char -> TextDetails Source #

A single Char fragment

pattern PStr :: String -> TextDetails Source #

Used to represent a Fast String fragment but now deprecated and identical to the Str constructor.

data Style Source #

A rendering style. Allows us to specify constraints to choose among the many different rendering options.

Constructors

Style |

Fields

- mode :: Mode

  The rendering mode.

- lineLength :: Int

  Maximum length of a line, in characters.

- ribbonsPerLine :: Float

  Ratio of line length to ribbon length. A ribbon refers to the characters on a line excluding indentation. So a `lineLength` of 100, with a `ribbonsPerLine` of `2.0` would only allow up to 50 characters of ribbon to be displayed on a line, while allowing it to be indented up to 50 characters.

Instances

Eq Style |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Style -> Style -> Bool Source # (/=) :: Style -> Style -> Bool Source #
Show Style |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods showsPrec :: Int -> Style -> ShowS Source # show :: Style -> String Source # showList :: [Style] -> ShowS Source #
Generic Style |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Associated Types type Rep Style :: Type -> Type Source # Methods from :: Style -> Rep Style x Source # to :: Rep Style x -> Style Source #
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 Mode Source #

Rendering mode.

Constructors

PageMode | Normal rendering (`lineLength` and `ribbonsPerLine` respected').
ZigZagMode | With zig-zag cuts.
LeftMode | No indentation, infinitely long lines (`lineLength` ignored), but explicit new lines, i.e., `text "one" $$ text "two"`, are respected.
OneLineMode | All on one line, `lineLength` ignored and explicit new lines (`$$`) are turned into spaces.

Instances

Eq Mode |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Mode -> Mode -> Bool Source # (/=) :: Mode -> Mode -> Bool Source #
Show Mode |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods showsPrec :: Int -> Mode -> ShowS Source # show :: Mode -> String Source # showList :: [Mode] -> ShowS Source #
Generic Mode |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Associated Types type Rep Mode :: Type -> Type Source # Methods from :: Mode -> Rep Mode x Source # to :: Rep Mode x -> Mode Source #
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)))

# Orphan instances

Data Doc Source # |

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc Source #

toConstr :: Doc -> Constr Source #

dataTypeOf :: Doc -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) Source #

gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source #