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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Pretty

Contents

Synopsis

Wrappers for pretty printing combinators

type Doc = 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

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

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

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

nest :: Int -> TCM Doc -> 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 
PrettyTCM Name 
PrettyTCM Range 
PrettyTCM Nat 
PrettyTCM Relevance 
PrettyTCM QName 
PrettyTCM Name 
PrettyTCM ModuleName 
PrettyTCM QName 
PrettyTCM Literal 
PrettyTCM Expr 
PrettyTCM Permutation 
PrettyTCM DeBruijnPattern 
PrettyTCM Pattern 
PrettyTCM ClauseBody 
PrettyTCM Clause 
PrettyTCM MetaId 
PrettyTCM Level 
PrettyTCM Sort 
PrettyTCM Telescope 
PrettyTCM Type 
PrettyTCM Elim 
PrettyTCM Term 
PrettyTCM ConHead 
PrettyTCM Context 
PrettyTCM RewriteRule 
PrettyTCM NLPat 
PrettyTCM DisplayTerm 
PrettyTCM TypeCheckingProblem 
PrettyTCM Comparison 
PrettyTCM Constraint 
PrettyTCM ProblemConstraint 
PrettyTCM ProblemId 
PrettyTCM NamedClause 
PrettyTCM PrettyContext 
PrettyTCM AsBinding 
PrettyTCM DotPatternInst 
PrettyTCM DeBruijnPat 
PrettyTCM Node 
PrettyTCM OccursWhere 
PrettyTCM HypSizeConstraint 
PrettyTCM SizeConstraint

Assumes we are in the right context.

PrettyTCM SizeMeta 
PrettyTCM SplitClause

For debugging only.

PrettyTCM a => PrettyTCM [a] 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) 
PrettyTCM a => PrettyTCM (WithHiding a) 
PrettyTCM a => PrettyTCM (Blocked a) 
PrettyTCM (Elim' NLPat) 
PrettyTCM (Elim' DisplayTerm) 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) 
PrettyTCM a => PrettyTCM (MaybeReduced a) 
PrettyTCM a => PrettyTCM (Judgement a) 
PrettyTCM a => PrettyTCM (Closure a) 
PrettyTCM a => PrettyTCM (Masked a)

Print masked things in double parentheses.

PrettyTCM a => PrettyTCM (HomHet a) 
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) 
PrettyTCM n => PrettyTCM (WithNode n Occurrence) 
PrettyTCM n => PrettyTCM (WithNode n Edge) 
(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) 

showPat' :: (a -> TCM Doc) -> Pattern' a -> TCM Doc

Show a pattern, given a method how to show pattern variables.