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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Pretty

Contents

Synopsis

Wrappers for pretty printing combinators

type Doc = Doc Source #

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

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

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

prettyList :: [TCM Doc] -> TCM Doc Source #

Comma-separated list in brackets.

prettyList_ :: [TCM Doc] -> TCM Doc Source #

prettyList without the brackets.

The PrettyTCM class

class PrettyTCM a where Source #

Minimal complete definition

prettyTCM

Methods

prettyTCM :: a -> TCM Doc Source #

Instances

PrettyTCM Bool Source # 

Methods

prettyTCM :: Bool -> TCM Doc Source #

PrettyTCM Range Source # 

Methods

prettyTCM :: Range -> TCM Doc Source #

PrettyTCM Permutation Source # 
PrettyTCM MetaId Source # 
PrettyTCM Nat Source # 

Methods

prettyTCM :: Nat -> TCM Doc Source #

PrettyTCM Relevance Source # 
PrettyTCM QName Source # 

Methods

prettyTCM :: QName -> TCM Doc Source #

PrettyTCM Name Source # 

Methods

prettyTCM :: Name -> TCM Doc Source #

PrettyTCM ModuleName Source # 
PrettyTCM QName Source # 

Methods

prettyTCM :: QName -> TCM Doc Source #

PrettyTCM Name Source # 

Methods

prettyTCM :: Name -> TCM Doc Source #

PrettyTCM Literal Source # 
PrettyTCM Term Source # 

Methods

prettyTCM :: Term -> TCM Doc Source #

PrettyTCM Occurrence Source # 
PrettyTCM EqualityView Source # 
PrettyTCM DBPatVar Source # 
PrettyTCM Clause Source # 
PrettyTCM Level Source # 

Methods

prettyTCM :: Level -> TCM Doc Source #

PrettyTCM Sort Source # 

Methods

prettyTCM :: Sort -> TCM Doc Source #

PrettyTCM Telescope Source # 
PrettyTCM Type Source # 

Methods

prettyTCM :: Type -> TCM Doc Source #

PrettyTCM ArgName Source # 
PrettyTCM Elim Source # 

Methods

prettyTCM :: Elim -> TCM Doc Source #

PrettyTCM Term Source # 

Methods

prettyTCM :: Term -> TCM Doc Source #

PrettyTCM ConHead Source # 
PrettyTCM TypedBinding Source # 
PrettyTCM Expr Source # 

Methods

prettyTCM :: Expr -> TCM Doc Source #

PrettyTCM CtxId Source # 

Methods

prettyTCM :: CtxId -> TCM Doc Source #

PrettyTCM Context Source # 
PrettyTCM ModuleParameters Source # 
PrettyTCM Polarity Source # 
PrettyTCM RewriteRule Source # 
PrettyTCM NLPType Source # 
PrettyTCM NLPat Source # 

Methods

prettyTCM :: NLPat -> TCM Doc Source #

PrettyTCM DisplayTerm Source # 
PrettyTCM TypeCheckingProblem Source # 
PrettyTCM Comparison Source # 
PrettyTCM Constraint Source # 
PrettyTCM ProblemConstraint Source # 
PrettyTCM ProblemId Source # 
PrettyTCM NamedClause Source # 
PrettyTCM PrettyContext Source # 
PrettyTCM AsBinding Source # 
PrettyTCM DotPatternInst Source # 
PrettyTCM ElimType Source # 
PrettyTCM Node Source # 

Methods

prettyTCM :: Node -> TCM Doc Source #

PrettyTCM ErrorPart Source # 
PrettyTCM HypSizeConstraint Source # 
PrettyTCM SizeConstraint Source #

Assumes we are in the right context.

PrettyTCM SizeMeta Source # 
PrettyTCM SplitClause Source #

For debugging only.

PrettyTCM a => PrettyTCM [a] Source # 

Methods

prettyTCM :: [a] -> TCM Doc Source #

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

Methods

prettyTCM :: Named_ a -> TCM Doc Source #

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

Methods

prettyTCM :: Dom a -> TCM Doc Source #

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

Methods

prettyTCM :: Arg a -> TCM Doc Source #

PrettyTCM a => PrettyTCM (WithHiding a) Source # 
PrettyTCM (QNamed Clause) Source # 
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # 
PrettyTCM a => PrettyTCM (Pattern' a) Source # 

Methods

prettyTCM :: Pattern' a -> TCM Doc Source #

PrettyTCM a => PrettyTCM (Blocked a) Source # 

Methods

prettyTCM :: Blocked a -> TCM Doc Source #

PrettyTCM (Type' NLPat) Source # 
PrettyTCM (Elim' NLPat) Source # 
PrettyTCM (Elim' DisplayTerm) Source # 
PrettyTCM a => PrettyTCM (MaybeReduced a) Source # 
PrettyTCM a => PrettyTCM (Judgement a) Source # 
PrettyTCM a => PrettyTCM (Closure a) Source # 

Methods

prettyTCM :: Closure a -> TCM Doc Source #

PrettyTCM a => PrettyTCM (Masked a) Source #

Print masked things in double parentheses.

Methods

prettyTCM :: Masked a -> TCM Doc Source #

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

Methods

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

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

Methods

prettyTCM :: Map k v -> TCM Doc Source #

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

Methods

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

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

Methods

prettyTCM :: Graph n n e -> TCM Doc Source #

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

Proper pretty printing of patterns:

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a