Agda-2.5.2: 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 #

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 #

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

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

($+$) :: TCM Doc -> 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 #

Minimal complete definition

prettyTCM

Methods

prettyTCM :: a -> TCM Doc #

Instances

PrettyTCM Bool # 

Methods

prettyTCM :: Bool -> TCM Doc #

PrettyTCM Range # 

Methods

prettyTCM :: Range -> TCM Doc #

PrettyTCM Permutation # 
PrettyTCM MetaId # 

Methods

prettyTCM :: MetaId -> TCM Doc #

PrettyTCM Nat # 

Methods

prettyTCM :: Nat -> TCM Doc #

PrettyTCM Relevance # 

Methods

prettyTCM :: Relevance -> TCM Doc #

PrettyTCM QName # 

Methods

prettyTCM :: QName -> TCM Doc #

PrettyTCM Name # 

Methods

prettyTCM :: Name -> TCM Doc #

PrettyTCM ModuleName # 
PrettyTCM QName # 

Methods

prettyTCM :: QName -> TCM Doc #

PrettyTCM Name # 

Methods

prettyTCM :: Name -> TCM Doc #

PrettyTCM Literal # 

Methods

prettyTCM :: Literal -> TCM Doc #

PrettyTCM Term # 

Methods

prettyTCM :: Term -> TCM Doc #

PrettyTCM Occurrence # 
PrettyTCM EqualityView # 
PrettyTCM DBPatVar # 

Methods

prettyTCM :: DBPatVar -> TCM Doc #

PrettyTCM Clause # 

Methods

prettyTCM :: Clause -> TCM Doc #

PrettyTCM Level # 

Methods

prettyTCM :: Level -> TCM Doc #

PrettyTCM Sort # 

Methods

prettyTCM :: Sort -> TCM Doc #

PrettyTCM Telescope # 

Methods

prettyTCM :: Telescope -> TCM Doc #

PrettyTCM Type # 

Methods

prettyTCM :: Type -> TCM Doc #

PrettyTCM ArgName # 

Methods

prettyTCM :: ArgName -> TCM Doc #

PrettyTCM Elim # 

Methods

prettyTCM :: Elim -> TCM Doc #

PrettyTCM Term # 

Methods

prettyTCM :: Term -> TCM Doc #

PrettyTCM ConHead # 

Methods

prettyTCM :: ConHead -> TCM Doc #

PrettyTCM TypedBinding # 
PrettyTCM Expr # 

Methods

prettyTCM :: Expr -> TCM Doc #

PrettyTCM CtxId # 

Methods

prettyTCM :: CtxId -> TCM Doc #

PrettyTCM Context # 

Methods

prettyTCM :: Context -> TCM Doc #

PrettyTCM ModuleParameters # 
PrettyTCM Polarity # 

Methods

prettyTCM :: Polarity -> TCM Doc #

PrettyTCM RewriteRule # 
PrettyTCM NLPType # 

Methods

prettyTCM :: NLPType -> TCM Doc #

PrettyTCM NLPat # 

Methods

prettyTCM :: NLPat -> TCM Doc #

PrettyTCM DisplayTerm # 
PrettyTCM TypeCheckingProblem # 
PrettyTCM Comparison # 
PrettyTCM Constraint # 
PrettyTCM ProblemConstraint # 
PrettyTCM ProblemId # 

Methods

prettyTCM :: ProblemId -> TCM Doc #

PrettyTCM NamedClause # 
PrettyTCM PrettyContext # 
PrettyTCM AsBinding # 

Methods

prettyTCM :: AsBinding -> TCM Doc #

PrettyTCM DotPatternInst # 
PrettyTCM DeBruijnPat # 
PrettyTCM Node # 

Methods

prettyTCM :: Node -> TCM Doc #

PrettyTCM SplitClause #

For debugging only.

PrettyTCM HypSizeConstraint # 
PrettyTCM SizeConstraint #

Assumes we are in the right context.

PrettyTCM SizeMeta # 

Methods

prettyTCM :: SizeMeta -> TCM Doc #

PrettyTCM ErrorPart # 

Methods

prettyTCM :: ErrorPart -> TCM Doc #

PrettyTCM a => PrettyTCM [a] # 

Methods

prettyTCM :: [a] -> TCM Doc #

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

Methods

prettyTCM :: Named_ a -> TCM Doc #

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

Methods

prettyTCM :: Dom a -> TCM Doc #

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

Methods

prettyTCM :: Arg a -> TCM Doc #

PrettyTCM a => PrettyTCM (WithHiding a) # 

Methods

prettyTCM :: WithHiding a -> TCM Doc #

PrettyTCM (QNamed Clause) # 
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) # 
PrettyTCM a => PrettyTCM (Pattern' a) # 

Methods

prettyTCM :: Pattern' a -> TCM Doc #

PrettyTCM a => PrettyTCM (Blocked a) # 

Methods

prettyTCM :: Blocked a -> TCM Doc #

PrettyTCM (Type' NLPat) # 

Methods

prettyTCM :: Type' NLPat -> TCM Doc #

PrettyTCM (Elim' NLPat) # 

Methods

prettyTCM :: Elim' NLPat -> TCM Doc #

PrettyTCM (Elim' DisplayTerm) # 
PrettyTCM a => PrettyTCM (MaybeReduced a) # 

Methods

prettyTCM :: MaybeReduced a -> TCM Doc #

PrettyTCM a => PrettyTCM (Judgement a) # 

Methods

prettyTCM :: Judgement a -> TCM Doc #

PrettyTCM a => PrettyTCM (Closure a) # 

Methods

prettyTCM :: Closure a -> TCM Doc #

PrettyTCM a => PrettyTCM (Masked a) #

Print masked things in double parentheses.

Methods

prettyTCM :: Masked a -> TCM Doc #

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

Methods

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

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

Methods

prettyTCM :: Map k v -> TCM Doc #

PrettyTCM n => PrettyTCM (WithNode n Occurrence) # 
PrettyTCM n => PrettyTCM (WithNode n Edge) # 

Methods

prettyTCM :: WithNode n Edge -> TCM Doc #

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

Methods

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

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

Methods

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

prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> TCM Doc #

Proper pretty printing of patterns:

data WithNode n a #

Pairing something with a node (for printing only).

Constructors

WithNode n a