Agda.TypeChecking.Pretty

Wrappers for pretty printing combinators

type Doc = Doc

comma :: TCM Doc

colon :: TCM Doc

equals :: TCM Doc

pretty :: Pretty a => a -> TCM Doc

prettyA :: (Pretty c, ToConcrete a c) => a -> TCM Doc

prettyAs :: (Pretty c, ToConcrete a [c]) => a -> TCM Doc

text :: String -> TCM Doc

multiLineText :: String -> TCM Doc

pwords :: String -> [TCM Doc]

fwords :: String -> TCM Doc

sep :: [TCM Doc] -> TCM Doc

fsep :: [TCM Doc] -> TCM Doc

hsep :: [TCM Doc] -> TCM Doc

hcat :: [TCM Doc] -> TCM Doc

vcat :: [TCM Doc] -> TCM Doc

hang :: TCM Doc -> Int -> TCM Doc -> TCM Doc

($$) :: TCM Doc -> TCM Doc -> TCM Doc infixl 5

($+$) :: TCM Doc -> TCM Doc -> TCM Doc infixl 5

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

(<+>) :: TCM Doc -> TCM Doc -> TCM Doc infixl 6

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

nest :: Int -> TCM Doc -> TCM Doc

braces :: TCM Doc -> TCM Doc

dbraces :: TCM Doc -> TCM Doc

brackets :: TCM Doc -> TCM Doc

parens :: TCM Doc -> TCM Doc

pshow :: Show a => a -> TCM Doc

prettyList :: [TCM Doc] -> TCM Doc

Comma-separated list in brackets.

prettyList_ :: [TCM Doc] -> TCM Doc

prettyList without the brackets.

punctuate :: TCM Doc -> [TCM Doc] -> [TCM Doc]

The PrettyTCM class

class PrettyTCM a where

Methods

prettyTCM :: a -> TCM Doc

Instances

PrettyTCM Bool

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Bool -> TCM Doc

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Range -> TCM Doc

PrettyTCM Permutation

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Permutation -> TCM Doc

PrettyTCM MetaId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MetaId -> TCM Doc

PrettyTCM Nat

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Nat -> TCM Doc

PrettyTCM Relevance

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Relevance -> TCM Doc

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc

PrettyTCM ModuleName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ModuleName -> TCM Doc

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc

PrettyTCM Literal

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Literal -> TCM Doc

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Term -> TCM Doc

PrettyTCM Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Occurrence -> TCM Doc

PrettyTCM EqualityView

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: EqualityView -> TCM Doc

PrettyTCM DBPatVar

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: DBPatVar -> TCM Doc

PrettyTCM Clause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Clause -> TCM Doc

PrettyTCM Level

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Level -> TCM Doc

PrettyTCM Sort

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Sort -> TCM Doc

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Telescope -> TCM Doc

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type -> TCM Doc

PrettyTCM ArgName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ArgName -> TCM Doc

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim -> TCM Doc

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Term -> TCM Doc

PrettyTCM ConHead

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ConHead -> TCM Doc

PrettyTCM SplitTag

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: SplitTag -> TCM Doc

PrettyTCM ProblemEq

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: ProblemEq -> TCM Doc

PrettyTCM TypedBinding

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: TypedBinding -> TCM Doc

PrettyTCM Expr

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Expr -> TCM Doc

PrettyTCM TCErr

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: TCErr -> TCM Doc

PrettyTCM TypeError

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: TypeError -> TCM Doc

PrettyTCM UnificationFailure

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: UnificationFailure -> TCM Doc

PrettyTCM NegativeUnification

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: NegativeUnification -> TCM Doc

PrettyTCM SplitError

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: SplitError -> TCM Doc

PrettyTCM CallInfo

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: CallInfo -> TCM Doc

PrettyTCM TCWarning

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: TCWarning -> TCM Doc

PrettyTCM Warning

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: Warning -> TCM Doc

PrettyTCM Call

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: Call -> TCM Doc

PrettyTCM IsForced

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: IsForced -> TCM Doc

PrettyTCM Polarity

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Polarity -> TCM Doc

PrettyTCM RewriteRule

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: RewriteRule -> TCM Doc

PrettyTCM NLPType

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NLPType -> TCM Doc

PrettyTCM NLPat

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NLPat -> TCM Doc

PrettyTCM DisplayTerm

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: DisplayTerm -> TCM Doc

PrettyTCM TypeCheckingProblem

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: TypeCheckingProblem -> TCM Doc

PrettyTCM Comparison

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Comparison -> TCM Doc

PrettyTCM Constraint

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Constraint -> TCM Doc

PrettyTCM ProblemConstraint

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ProblemConstraint -> TCM Doc

PrettyTCM CheckpointId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: CheckpointId -> TCM Doc

PrettyTCM ProblemId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ProblemId -> TCM Doc

PrettyTCM NamedClause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NamedClause -> TCM Doc

PrettyTCM PrettyContext

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: PrettyContext -> TCM Doc

PrettyTCM AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: AbsurdPattern -> TCM Doc

PrettyTCM DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: DotPattern -> TCM Doc

PrettyTCM AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: AsBinding -> TCM Doc

PrettyTCM ElimType

Defined in Agda.TypeChecking.Records

Methods

prettyTCM :: ElimType -> TCM Doc

PrettyTCM Node

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: Node -> TCM Doc

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: SplitPatVar -> TCM Doc

PrettyTCM ErrorPart

Defined in Agda.TypeChecking.Unquote

Methods

prettyTCM :: ErrorPart -> TCM Doc

PrettyTCM HypSizeConstraint

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: HypSizeConstraint -> TCM Doc

PrettyTCM SizeConstraint

Assumes we are in the right context.

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: SizeConstraint -> TCM Doc

PrettyTCM SizeMeta

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: SizeMeta -> TCM Doc

PrettyTCM SplitClause

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: SplitClause -> TCM Doc

PrettyTCM a => PrettyTCM [a]

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: [a] -> TCM Doc

PrettyTCM (Seq OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: Seq OccursWhere -> TCM Doc

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Named_ a -> TCM Doc

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Dom a -> TCM Doc

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Arg a -> TCM Doc

PrettyTCM a => PrettyTCM (WithHiding a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithHiding a -> TCM Doc

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QNamed Clause -> TCM Doc

(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Substitution' a -> TCM Doc

PrettyTCM a => PrettyTCM (Pattern' a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Pattern' a -> TCM Doc

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Blocked a -> TCM Doc

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type' NLPat -> TCM Doc

PrettyTCM (Elim' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim' NLPat -> TCM Doc

PrettyTCM (Elim' DisplayTerm)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim' DisplayTerm -> TCM Doc

PrettyTCM a => PrettyTCM (MaybeReduced a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MaybeReduced a -> TCM Doc

PrettyTCM a => PrettyTCM (Judgement a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Judgement a -> TCM Doc

PrettyTCM a => PrettyTCM (Closure a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Closure a -> TCM Doc

PrettyTCM a => PrettyTCM (Masked a)

Print masked things in double parentheses.

Defined in Agda.Termination.Monad

Methods

prettyTCM :: Masked a -> TCM Doc

(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: (a, b) -> TCM Doc

(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Map k v -> TCM Doc

(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Graph n e -> TCM Doc

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithNode n Occurrence -> TCM Doc

PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere))

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: WithNode n (Edge OccursWhere) -> TCM Doc

(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: (a, b, c) -> TCM Doc

prettyTCMCtx :: PrettyTCM a => Precedence -> a -> TCM Doc

Pretty print with a given context precedence

newtype PrettyContext

Constructors

PrettyContext Context

Instances

PrettyTCM PrettyContext

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: PrettyContext -> TCM Doc

prettyTCMPatterns :: [NamedArg DeBruijnPattern] -> TCM [Doc]

Proper pretty printing of patterns:

prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> TCM Doc

data WithNode n a

Pairing something with a node (for printing only).

Constructors

WithNode n a

Instances

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithNode n Occurrence -> TCM Doc

PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere))

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: WithNode n (Edge OccursWhere) -> TCM Doc