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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Common.Pretty

Description

Pretty printing functions.

Synopsis

- class Pretty a where
  - pretty :: a -> Doc
  - prettyPrec :: Int -> a -> Doc
  - prettyList :: [a] -> Doc
- (<?>) :: Doc -> Doc -> Doc
- comma :: Doc
- colon :: Doc
- parens :: Doc -> Doc
- align :: Int -> [(String, Doc)] -> Doc
- hcat :: Foldable t => t Doc -> Doc
- hsep :: Foldable t => t Doc -> Doc
- vcat :: Foldable t => t Doc -> Doc
- vsep :: [Doc] -> Doc
- dot :: Doc
- space :: Doc
- semi :: Doc
- brackets :: Doc -> Doc
- braces :: Doc -> Doc
- type Doc = Doc Aspects
- equals :: Doc
- lparen :: Doc
- rparen :: Doc
- lbrack :: Doc
- rbrack :: Doc
- lbrace :: Doc
- rbrace :: Doc
- quotes :: Doc -> Doc
- doubleQuotes :: Doc -> Doc
- punctuate :: Foldable t => Doc -> t Doc -> [Doc]
- sep :: Foldable t => t Doc -> Doc
- fsep :: Foldable t => t Doc -> Doc
- prettyShow :: Pretty a => a -> String
- prettyList_ :: Pretty a => [a] -> Doc
- singPlural :: Sized a => a -> c -> c -> c
- pshow :: Show a => a -> Doc
- pluralS :: Sized a => a -> Doc -> Doc
- prettySet :: Pretty a => [a] -> Doc
- prettyMap :: (Pretty k, Pretty v) => [(k, v)] -> Doc
- prettyLineColumn :: Position' a -> Doc
- pwords :: String -> [Doc]
- fwords :: String -> Doc
- hsepWith :: Doc -> Doc -> Doc -> Doc
- prettyAssign :: (Pretty k, Pretty v) => (k, v) -> Doc
- hlSymbol :: Doc -> Doc
- mparens :: Bool -> Doc -> Doc
- parensNonEmpty :: Doc -> Doc
- textNonEmpty :: String -> Doc
- multiLineText :: String -> Doc
- prefixedThings :: Doc -> [Doc] -> Doc
- annotateAspect :: Aspect -> Doc -> Doc
- hlComment :: Doc -> Doc
- hlKeyword :: Doc -> Doc
- hlString :: Doc -> Doc
- hlNumber :: Doc -> Doc
- hlHole :: Doc -> Doc
- hlPrimitiveType :: Doc -> Doc
- hlPragma :: Doc -> Doc
- text :: String -> Doc a
- int :: Int -> Doc a
- integer :: Integer -> Doc a
- float :: Float -> Doc a
- double :: Double -> Doc a
- char :: Char -> Doc a
- (<+>) :: Doc a -> Doc a -> Doc a
- isEmpty :: Doc a -> Bool
- style :: Style
- render :: Doc a -> String
- data Mode
  - = PageMode
  - | ZigZagMode
  - | LeftMode
  - | OneLineMode
- data Span a = Span {
  - spanStart :: !Int
  - spanLength :: !Int
  - spanAnnotation :: a
  }
- data Style = Style {
  - mode :: Mode
  - lineLength :: Int
  - ribbonsPerLine :: Float
  }
- pattern Chr :: !Char -> TextDetails
- pattern PStr :: String -> TextDetails
- annotate :: a -> Doc a -> Doc a
- ptext :: String -> Doc a
- sizedText :: Int -> String -> Doc a
- zeroWidthText :: String -> Doc a
- rational :: Rational -> Doc a
- nest :: Int -> Doc a -> Doc a
- hang :: Doc a -> Int -> Doc a -> Doc a
- ($$) :: Doc a -> Doc a -> Doc a
- ($+$) :: Doc a -> Doc a -> Doc a
- cat :: [Doc a] -> Doc a
- fcat :: [Doc a] -> Doc a
- renderStyle :: Style -> Doc a -> String
- fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc b -> a
- fullRenderAnn :: Mode -> Int -> Float -> (AnnotDetails b -> a -> a) -> a -> Doc b -> a
- renderSpans :: Doc ann -> (String, [Span ann])
- (<>) :: Semigroup a => a -> a -> a

# 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

pretty | prettyPrec

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 Methods pretty :: Phase -> Doc Source # prettyPrec :: Int -> Phase -> Doc Source # prettyList :: [Phase] -> 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 CompilerBackend Source # |
Instance details Defined in Agda.Interaction.Base Methods pretty :: CompilerBackend -> Doc Source # prettyPrec :: Int -> CompilerBackend -> Doc Source # prettyList :: [CompilerBackend] -> Doc Source #
Pretty InterfaceFile Source # |
Instance details Defined in Agda.Interaction.FindFile Methods pretty :: InterfaceFile -> Doc Source # prettyPrec :: Int -> InterfaceFile -> Doc Source # prettyList :: [InterfaceFile] -> Doc Source #
Pretty LibError' Source # | Pretty-print library management error without position info.
Instance details Defined in Agda.Interaction.Library.Base Methods pretty :: LibError' -> Doc Source # prettyPrec :: Int -> LibError' -> Doc Source # prettyList :: [LibError'] -> Doc Source #
Pretty LibName Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods pretty :: LibName -> Doc Source # prettyPrec :: Int -> LibName -> Doc Source # prettyList :: [LibName] -> Doc Source #
Pretty LibParseError Source # | Print library file parse error without position info.
Instance details Defined in Agda.Interaction.Library.Base Methods pretty :: LibParseError -> Doc Source # prettyPrec :: Int -> LibParseError -> Doc Source # prettyList :: [LibParseError] -> Doc Source #
Pretty LibWarning Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning -> Doc Source # prettyPrec :: Int -> LibWarning -> Doc Source # prettyList :: [LibWarning] -> Doc Source #
Pretty LibWarning' Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods pretty :: LibWarning' -> Doc Source # prettyPrec :: Int -> LibWarning' -> Doc Source # prettyList :: [LibWarning'] -> Doc Source #
Pretty OptionWarning Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods pretty :: OptionWarning -> Doc Source # prettyPrec :: Int -> OptionWarning -> Doc Source # prettyList :: [OptionWarning] -> Doc Source #
Pretty HintMode Source # |
Instance details Defined in Agda.Mimer.Options Methods pretty :: HintMode -> Doc Source # prettyPrec :: Int -> HintMode -> Doc Source # prettyList :: [HintMode] -> 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 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 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 Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
Pretty Suffix Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: Suffix -> Doc Source # prettyPrec :: Int -> Suffix -> Doc Source # prettyList :: [Suffix] -> Doc Source #
Pretty BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods pretty :: BuiltinId -> Doc Source # prettyPrec :: Int -> BuiltinId -> Doc Source # prettyList :: [BuiltinId] -> Doc Source #
Pretty PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods pretty :: PrimitiveId -> Doc Source # prettyPrec :: Int -> PrimitiveId -> Doc Source # prettyList :: [PrimitiveId] -> 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 Associativity Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source #
Pretty Cohesion Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Cohesion -> Doc Source # prettyPrec :: Int -> Cohesion -> Doc Source # prettyList :: [Cohesion] -> Doc Source #
Pretty ConstructorOrPatternSynonym Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: ConstructorOrPatternSynonym -> Doc Source # prettyPrec :: Int -> ConstructorOrPatternSynonym -> Doc Source # prettyList :: [ConstructorOrPatternSynonym] -> Doc Source #
Pretty Erased Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Erased -> Doc Source # prettyPrec :: Int -> Erased -> Doc Source # prettyList :: [Erased] -> 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 Fixity Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Fixity -> Doc Source # prettyPrec :: Int -> Fixity -> Doc Source # prettyList :: [Fixity] -> 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 FixityLevel Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: FixityLevel -> Doc Source # prettyPrec :: Int -> FixityLevel -> Doc Source # prettyList :: [FixityLevel] -> 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 InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source #
Pretty Lock Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Lock -> Doc Source # prettyPrec :: Int -> Lock -> Doc Source # prettyList :: [Lock] -> 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 ModalPolarity Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: ModalPolarity -> Doc Source # prettyPrec :: Int -> ModalPolarity -> Doc Source # prettyList :: [ModalPolarity] -> Doc Source #
Pretty Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Modality -> Doc Source # prettyPrec :: Int -> Modality -> Doc Source # prettyList :: [Modality] -> 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 NotationPart Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> Doc Source #
Pretty OpaqueId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: OpaqueId -> Doc Source # prettyPrec :: Int -> OpaqueId -> Doc Source # prettyList :: [OpaqueId] -> Doc Source #
Pretty OriginIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: OriginIrrelevant -> Doc Source # prettyPrec :: Int -> OriginIrrelevant -> Doc Source # prettyList :: [OriginIrrelevant] -> Doc Source #
Pretty OriginRelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: OriginRelevant -> Doc Source # prettyPrec :: Int -> OriginRelevant -> Doc Source # prettyList :: [OriginRelevant] -> Doc Source #
Pretty OriginShapeIrrelevant Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: OriginShapeIrrelevant -> Doc Source # prettyPrec :: Int -> OriginShapeIrrelevant -> Doc Source # prettyList :: [OriginShapeIrrelevant] -> Doc Source #
Pretty OverlapMode Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: OverlapMode -> Doc Source # prettyPrec :: Int -> OverlapMode -> Doc Source # prettyList :: [OverlapMode] -> Doc Source #
Pretty PolarityModality Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: PolarityModality -> Doc Source # prettyPrec :: Int -> PolarityModality -> Doc Source # prettyList :: [PolarityModality] -> Doc Source #
Pretty ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: ProblemId -> Doc Source # prettyPrec :: Int -> ProblemId -> Doc Source # prettyList :: [ProblemId] -> Doc Source #
Pretty Q0Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Q0Origin -> Doc Source # prettyPrec :: Int -> Q0Origin -> Doc Source # prettyList :: [Q0Origin] -> Doc Source #
Pretty Q1Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Q1Origin -> Doc Source # prettyPrec :: Int -> Q1Origin -> Doc Source # prettyList :: [Q1Origin] -> Doc Source #
Pretty Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Quantity -> Doc Source # prettyPrec :: Int -> Quantity -> Doc Source # prettyList :: [Quantity] -> Doc Source #
Pretty QωOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: QωOrigin -> Doc Source # prettyPrec :: Int -> QωOrigin -> Doc Source # prettyList :: [QωOrigin] -> Doc Source #
Pretty Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Relevance -> Doc Source # prettyPrec :: Int -> Relevance -> Doc Source # prettyList :: [Relevance] -> 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 KwRange Source # |
Instance details Defined in Agda.Syntax.Common.KeywordRange Methods pretty :: KwRange -> Doc Source # prettyPrec :: Int -> KwRange -> Doc Source # prettyList :: [KwRange] -> 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 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 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 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 Methods pretty :: LHSCore -> Doc Source # prettyPrec :: Int -> LHSCore -> Doc Source # prettyList :: [LHSCore] -> 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 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 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 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 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 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 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 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 RecordDirective Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RecordDirective -> Doc Source # prettyPrec :: Int -> RecordDirective -> Doc Source # prettyList :: [RecordDirective] -> 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 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 DeclarationException' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: DeclarationException' -> Doc Source # prettyPrec :: Int -> DeclarationException' -> Doc Source # prettyList :: [DeclarationException'] -> Doc Source #
Pretty DeclarationWarning Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: DeclarationWarning -> Doc Source # prettyPrec :: Int -> DeclarationWarning -> Doc Source # prettyList :: [DeclarationWarning] -> Doc Source #
Pretty DeclarationWarning' Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: DeclarationWarning' -> Doc Source # prettyPrec :: Int -> DeclarationWarning' -> Doc Source # prettyList :: [DeclarationWarning'] -> Doc Source #
Pretty OpenOrImport Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Errors Methods pretty :: OpenOrImport -> Doc Source # prettyPrec :: Int -> OpenOrImport -> Doc Source # prettyList :: [OpenOrImport] -> Doc Source #
Pretty DataRecOrFun Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: DataRecOrFun -> Doc Source # prettyPrec :: Int -> DataRecOrFun -> Doc Source # prettyList :: [DataRecOrFun] -> Doc Source #
Pretty NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: NiceDeclaration -> Doc Source # prettyPrec :: Int -> NiceDeclaration -> Doc Source # prettyList :: [NiceDeclaration] -> 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 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 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 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 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 Methods pretty :: Precedence -> Doc Source # prettyPrec :: Int -> Precedence -> Doc Source # prettyList :: [Precedence] -> 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 ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: ConHead -> Doc Source # prettyPrec :: Int -> ConHead -> Doc Source # prettyList :: [ConHead] -> 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 Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Level -> Doc Source # prettyPrec :: Int -> Level -> Doc Source # prettyList :: [Level] -> 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 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 Methods pretty :: Blocker -> Doc Source # prettyPrec :: Int -> Blocker -> Doc Source # prettyList :: [Blocker] -> 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 NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NewNotation -> Doc Source # prettyPrec :: Int -> NewNotation -> Doc Source # prettyList :: [NewNotation] -> Doc Source #
Pretty NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NotationKind -> Doc Source # prettyPrec :: Int -> NotationKind -> Doc Source # prettyList :: [NotationKind] -> Doc Source #
Pretty NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NotationSection -> Doc Source # prettyPrec :: Int -> NotationSection -> Doc Source # prettyList :: [NotationSection] -> 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 ParseWarning Source # | Does not include printing of the range.
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source #
Pretty IntervalWithoutFile Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: IntervalWithoutFile -> Doc Source # prettyPrec :: Int -> IntervalWithoutFile -> Doc Source # prettyList :: [IntervalWithoutFile] -> Doc Source #
Pretty PositionWithoutFile Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: PositionWithoutFile -> Doc Source # prettyPrec :: Int -> PositionWithoutFile -> Doc Source # prettyList :: [PositionWithoutFile] -> Doc Source #
Pretty RangeFile Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: RangeFile -> Doc Source # prettyPrec :: Int -> RangeFile -> Doc Source # prettyList :: [RangeFile] -> 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 BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: BindingSource -> Doc Source # prettyPrec :: Int -> BindingSource -> Doc Source # prettyList :: [BindingSource] -> 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 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 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 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 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 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 FlatScope Source # |
Instance details Defined in Agda.Syntax.Scope.Flat Methods pretty :: FlatScope -> Doc Source # prettyPrec :: Int -> FlatScope -> Doc Source # prettyList :: [FlatScope] -> Doc Source #
Pretty RawTopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods pretty :: RawTopLevelModuleName -> Doc Source # prettyPrec :: Int -> RawTopLevelModuleName -> Doc Source # prettyList :: [RawTopLevelModuleName] -> Doc Source #
Pretty TopLevelModuleName Source # |
Instance details Defined in Agda.Syntax.TopLevelModuleName Methods pretty :: TopLevelModuleName -> Doc Source # prettyPrec :: Int -> TopLevelModuleName -> Doc Source # prettyList :: [TopLevelModuleName] -> Doc Source #
Pretty Compiled Source # |
Instance details Defined in Agda.Compiler.Treeless.Pretty Methods pretty :: Compiled -> Doc Source # prettyPrec :: Int -> Compiled -> Doc Source # prettyList :: [Compiled] -> 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 CallMatrix Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods pretty :: CallMatrix -> Doc Source # prettyPrec :: Int -> CallMatrix -> Doc Source # prettyList :: [CallMatrix] -> 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 Order Source # |
Instance details Defined in Agda.Termination.Order Methods pretty :: Order -> Doc Source # prettyPrec :: Int -> Order -> Doc Source # prettyList :: [Order] -> 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 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 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 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 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 Methods pretty :: CallInfo -> Doc Source # prettyPrec :: Int -> CallInfo -> Doc Source # prettyList :: [CallInfo] -> 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 CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CompareAs -> Doc Source # prettyPrec :: Int -> CompareAs -> Doc Source # prettyList :: [CompareAs] -> 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 ConstructorData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ConstructorData -> Doc Source # prettyPrec :: Int -> ConstructorData -> Doc Source # prettyList :: [ConstructorData] -> Doc Source #
Pretty DataOrRecSigData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: DataOrRecSigData -> Doc Source # prettyPrec :: Int -> DataOrRecSigData -> Doc Source # prettyList :: [DataOrRecSigData] -> Doc Source #
Pretty DatatypeData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: DatatypeData -> Doc Source # prettyPrec :: Int -> DatatypeData -> Doc Source # prettyList :: [DatatypeData] -> 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 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 Methods pretty :: DisplayForm -> Doc Source # prettyPrec :: Int -> DisplayForm -> Doc Source # prettyList :: [DisplayForm] -> 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 FunctionData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: FunctionData -> Doc Source # prettyPrec :: Int -> FunctionData -> Doc Source # prettyList :: [FunctionData] -> 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 MetaInstantiation Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: MetaInstantiation -> Doc Source # prettyPrec :: Int -> MetaInstantiation -> Doc Source # prettyList :: [MetaInstantiation] -> Doc Source #
Pretty MutualId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: MutualId -> Doc Source # prettyPrec :: Int -> MutualId -> Doc Source # prettyList :: [MutualId] -> Doc Source #
Pretty OpaqueBlock Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: OpaqueBlock -> Doc Source # prettyPrec :: Int -> OpaqueBlock -> Doc Source # prettyList :: [OpaqueBlock] -> Doc Source #
Pretty PrimitiveData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: PrimitiveData -> Doc Source # prettyPrec :: Int -> PrimitiveData -> Doc Source # prettyList :: [PrimitiveData] -> Doc Source #
Pretty PrimitiveSortData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: PrimitiveSortData -> Doc Source # prettyPrec :: Int -> PrimitiveSortData -> Doc Source # prettyList :: [PrimitiveSortData] -> Doc Source #
Pretty ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ProjLams -> Doc Source # prettyPrec :: Int -> ProjLams -> Doc Source # prettyList :: [ProjLams] -> Doc Source #
Pretty Projection Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Projection -> Doc Source # prettyPrec :: Int -> Projection -> Doc Source # prettyList :: [Projection] -> Doc Source #
Pretty ProjectionLikenessMissing Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ProjectionLikenessMissing -> Doc Source # prettyPrec :: Int -> ProjectionLikenessMissing -> Doc Source # prettyList :: [ProjectionLikenessMissing] -> Doc Source #
Pretty RecordData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: RecordData -> Doc Source # prettyPrec :: Int -> RecordData -> Doc Source # prettyList :: [RecordData] -> 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 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 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 ModuleToSource Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ModuleToSource -> Doc Source # prettyPrec :: Int -> ModuleToSource -> Doc Source # prettyList :: [ModuleToSource] -> 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 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 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 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 Methods pretty :: Occurrence -> Doc Source # prettyPrec :: Int -> Occurrence -> Doc Source # prettyList :: [Occurrence] -> 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 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 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 Methods pretty :: CType -> Doc Source # prettyPrec :: Int -> CType -> Doc Source # prettyList :: [CType] -> 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 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 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 NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: NamedRigid -> Doc Source # prettyPrec :: Int -> NamedRigid -> Doc Source # prettyList :: [NamedRigid] -> 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 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 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 SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: SizeMeta -> Doc Source # prettyPrec :: Int -> SizeMeta -> Doc Source # prettyList :: [SizeMeta] -> 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 CallSite Source # |
Instance details Defined in Agda.Utils.CallStack.Pretty Methods pretty :: CallSite -> Doc Source # prettyPrec :: Int -> CallSite -> Doc Source # prettyList :: [CallSite] -> Doc Source #
Pretty AbsolutePath Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> 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 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 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 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 Methods pretty :: ImportDecl -> Doc Source # prettyPrec :: Int -> ImportDecl -> Doc Source # prettyList :: [ImportDecl] -> 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 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 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 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 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 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 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 Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> 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 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 Methods pretty :: Strictness -> Doc Source # prettyPrec :: Int -> Strictness -> Doc Source # prettyList :: [Strictness] -> 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 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 Methods pretty :: CPUTime -> Doc Source # prettyPrec :: Int -> CPUTime -> Doc Source # prettyList :: [CPUTime] -> 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 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 Methods pretty :: CallStack -> Doc Source # prettyPrec :: Int -> CallStack -> Doc Source # prettyList :: [CallStack] -> Doc Source #
Pretty SrcLoc Source # |
Instance details Defined in Agda.Utils.CallStack.Pretty Methods pretty :: SrcLoc -> Doc Source # prettyPrec :: Int -> SrcLoc -> Doc Source # prettyList :: [SrcLoc] -> Doc Source #
Pretty Word32 Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: Word32 -> Doc Source # prettyPrec :: Int -> Word32 -> Doc Source # prettyList :: [Word32] -> Doc Source #
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 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.Common 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 Methods pretty :: MaybePlaceholder a -> Doc Source # prettyPrec :: Int -> MaybePlaceholder a -> Doc Source # prettyList :: [MaybePlaceholder a] -> Doc Source #
Pretty e => Pretty (Named_ e) Source # |
Instance details Defined in Agda.Syntax.Common 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.Common Methods pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding a] -> Doc Source #
Pretty a => Pretty (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: WithOrigin a -> Doc Source # prettyPrec :: Int -> WithOrigin a -> Doc Source # prettyList :: [WithOrigin a] -> Doc Source #
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 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 a => Pretty (TacticAttribute' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TacticAttribute' a -> Doc Source # prettyPrec :: Int -> TacticAttribute' a -> Doc Source # prettyList :: [TacticAttribute' 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 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 Methods pretty :: Pattern' a -> Doc Source # prettyPrec :: Int -> Pattern' a -> Doc Source # prettyList :: [Pattern' a] -> 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 (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 Methods pretty :: NotBlocked' t -> Doc Source # prettyPrec :: Int -> NotBlocked' t -> Doc Source # prettyList :: [NotBlocked' t] -> Doc Source #
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 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.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 Methods pretty :: WithArity a -> Doc Source # prettyPrec :: Int -> WithArity a -> Doc Source # prettyList :: [WithArity 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 (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 c => Pretty (FunctionInverse' c) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: FunctionInverse' c -> Doc Source # prettyPrec :: Int -> FunctionInverse' c -> Doc Source # prettyList :: [FunctionInverse' c] -> Doc Source #
Pretty a => Pretty (Judgement a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Judgement a -> Doc Source # prettyPrec :: Int -> Judgement a -> Doc Source # prettyList :: [Judgement a] -> Doc Source #
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 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 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 #
(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 n => Pretty (WithUniqueInt n) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods pretty :: WithUniqueInt n -> Doc Source # prettyPrec :: Int -> WithUniqueInt n -> Doc Source # prettyList :: [WithUniqueInt n] -> Doc Source #
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 -> Doc Source # prettyPrec :: Int -> Doc a -> Doc Source # prettyList :: [Doc a] -> Doc 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 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 #
(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: ImportDirective' a b -> Doc Source # prettyPrec :: Int -> ImportDirective' a b -> Doc Source # prettyList :: [ImportDirective' a b] -> Doc Source #
(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # |
Instance details Defined in Agda.Syntax.Common 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 (Renaming' a b) Source # |
Instance details Defined in Agda.Syntax.Common 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.Common 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 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 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 x, Pretty a) => Pretty (Boundary' x a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods pretty :: Boundary' x a -> Doc Source # prettyPrec :: Int -> Boundary' x a -> Doc Source # prettyList :: [Boundary' x a] -> 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 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 (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.Common.Pretty Methods pretty :: (a, b) -> Doc Source # prettyPrec :: Int -> (a, b) -> Doc Source # prettyList :: [(a, b)] -> 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 #

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

    a ? b = hang a 2 b

comma :: Doc Source #

colon :: Doc Source #

parens Source #

Arguments

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

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

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

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

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

vsep :: [Doc] -> Doc Source #

dot :: Doc Source #

space :: Doc Source #

semi :: Doc Source #

brackets Source #

Arguments

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

braces Source #

Arguments

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

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.

equals :: Doc Source #

lparen :: Doc Source #

rparen :: Doc Source #

lbrack :: Doc Source #

rbrack :: Doc Source #

lbrace :: Doc Source #

rbrace :: Doc Source #

quotes Source #

Arguments

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

doubleQuotes Source #

Arguments

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

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

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

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

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

Use instead of `show` when printing to world.

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

pluralS :: Sized a => a -> Doc -> Doc Source #

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

Pretty print a set.

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

Pretty print an association list.

prettyLineColumn :: Position' a -> Doc Source #

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.

hlSymbol :: Doc -> Doc Source #

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

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

parensNonEmpty :: Doc -> Doc Source #

Only wrap in parens if not `empty`

textNonEmpty :: String -> Doc Source #

Return `empty` for empty strings.

multiLineText :: String -> Doc Source #

Handles strings with newlines properly (preserving indentation)

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.

hlComment :: Doc -> Doc Source #

hlKeyword :: Doc -> Doc Source #

hlString :: Doc -> Doc Source #

hlNumber :: Doc -> Doc Source #

hlHole :: Doc -> Doc Source #

hlPrimitiveType :: Doc -> Doc Source #

hlPragma :: Doc -> Doc Source #

text :: String -> Doc a 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.

int Source #

Arguments

:: Int |

-> Doc a

    int n = text (show n)

integer Source #

Arguments

:: Integer |

-> Doc a

    integer n = text (show n)

float Source #

Arguments

:: Float |

-> Doc a

    float n = text (show n)

double Source #

Arguments

:: Double |

-> Doc a

    double n = text (show n)

char :: Char -> Doc a Source #

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

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

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

isEmpty :: Doc a -> Bool Source #

Returns `True` if the document is empty

style :: Style Source #

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

render :: Doc a -> String Source #

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

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

Instances details

Generic Mode |

Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

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-inplace" '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)))

Methods

from :: Mode -> Rep Mode x Source #

to :: Rep Mode x -> Mode 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 #
Eq Mode |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Mode -> Mode -> Bool Source # (/=) :: Mode -> Mode -> Bool 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-inplace" '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 Span a Source #

A `Span` represents the result of an annotation after a `Doc` has been rendered, capturing where the annotation now starts and ends in the rendered output.

Constructors

Span |

Fields

- spanStart :: !Int
- spanLength :: !Int
- spanAnnotation :: a

#### Instances

Instances details

Functor Span |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods fmap :: (a -> b) -> Span a -> Span b Source # (<$) :: a -> Span b -> Span a Source #
Show a => Show (Span a) |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods showsPrec :: Int -> Span a -> ShowS Source # show :: Span a -> String Source # showList :: [Span a] -> ShowS Source #
Eq a => Eq (Span a) |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Span a -> Span a -> Bool Source # (/=) :: Span a -> Span a -> Bool Source #

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

Instances details

Generic Style |

Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

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-inplace" '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))))

Methods

from :: Style -> Rep Style x Source #

to :: Rep Style x -> Style 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 #
Eq Style |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (==) :: Style -> Style -> Bool Source # (/=) :: Style -> Style -> Bool 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-inplace" '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))))

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.

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

Attach an annotation to a document.

ptext :: String -> Doc a Source #

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

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

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

zeroWidthText :: String -> Doc a Source #

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

rational Source #

Arguments

:: Rational |

-> Doc a

    rational n = text (show n)

nest :: Int -> Doc a -> Doc a 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 z <> 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 `<>`.

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

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

($$) :: Doc a -> Doc a -> Doc a 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.

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

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

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

Either `hcat` or `vcat`.

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

"Paragraph fill" version of `cat`.

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

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

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

fullRenderAnn Source #

Arguments

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

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

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

Render an annotated `Doc` to a String and list of annotations (see `Span`) using the default `Style` (see `style`).

(<>) :: Semigroup a => a -> a -> a infixr 6 Source #

An associative operation.

#### Examples

Expand

    >>> [1,2,3] <> [4,5,6]
    [1,2,3,4,5,6]

    >>> Just [1, 2, 3] <> Just [4, 5, 6]
    Just [1,2,3,4,5,6]

    >>> putStr "Hello, " <> putStrLn "World!"
    Hello, World!