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

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 #

Minimal complete definition

prettyTCM

Methods

prettyTCM :: a -> TCM Doc #

Instances
PrettyTCM Bool # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Bool -> TCM Doc #

PrettyTCM Range # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Range -> TCM Doc #

PrettyTCM Permutation # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Permutation -> TCM Doc #

PrettyTCM MetaId # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MetaId -> TCM Doc #

PrettyTCM Nat # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Nat -> TCM Doc #

PrettyTCM Relevance # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Relevance -> TCM Doc #

PrettyTCM QName # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc #

PrettyTCM Name # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc #

PrettyTCM ModuleName # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ModuleName -> TCM Doc #

PrettyTCM QName # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc #

PrettyTCM Name # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc #

PrettyTCM Literal # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Literal -> TCM Doc #

PrettyTCM Term # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Term -> TCM Doc #

PrettyTCM Occurrence # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Occurrence -> TCM Doc #

PrettyTCM OccursWhere # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: OccursWhere -> TCM Doc #

PrettyTCM EqualityView # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: EqualityView -> TCM Doc #

PrettyTCM DBPatVar # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: DBPatVar -> TCM Doc #

PrettyTCM Clause # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Clause -> TCM Doc #

PrettyTCM Level # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Level -> TCM Doc #

PrettyTCM Sort # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Sort -> TCM Doc #

PrettyTCM Telescope # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Telescope -> TCM Doc #

PrettyTCM Type # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type -> TCM Doc #

PrettyTCM ArgName # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ArgName -> TCM Doc #

PrettyTCM Elim # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim -> TCM Doc #

PrettyTCM Term # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Term -> TCM Doc #

PrettyTCM ConHead # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ConHead -> TCM Doc #

PrettyTCM ProblemEq # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: ProblemEq -> TCM Doc #

PrettyTCM TypedBinding # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: TypedBinding -> TCM Doc #

PrettyTCM Expr # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Expr -> TCM Doc #

PrettyTCM TCErr # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: TCErr -> TCM Doc #

PrettyTCM TypeError # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: TypeError -> TCM Doc #

PrettyTCM UnificationFailure # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: UnificationFailure -> TCM Doc #

PrettyTCM NegativeUnification # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: NegativeUnification -> TCM Doc #

PrettyTCM SplitError # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: SplitError -> TCM Doc #

PrettyTCM CallInfo # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: CallInfo -> TCM Doc #

PrettyTCM TCWarning # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: TCWarning -> TCM Doc #

PrettyTCM Warning # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: Warning -> TCM Doc #

PrettyTCM Call # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: Call -> TCM Doc #

PrettyTCM IsForced # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: IsForced -> TCM Doc #

PrettyTCM Polarity # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Polarity -> TCM Doc #

PrettyTCM RewriteRule # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: RewriteRule -> TCM Doc #

PrettyTCM NLPType # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NLPType -> TCM Doc #

PrettyTCM NLPat # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NLPat -> TCM Doc #

PrettyTCM DisplayTerm # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: DisplayTerm -> TCM Doc #

PrettyTCM TypeCheckingProblem # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: TypeCheckingProblem -> TCM Doc #

PrettyTCM Comparison # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Comparison -> TCM Doc #

PrettyTCM Constraint # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Constraint -> TCM Doc #

PrettyTCM ProblemConstraint # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ProblemConstraint -> TCM Doc #

PrettyTCM CheckpointId # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: CheckpointId -> TCM Doc #

PrettyTCM ProblemId # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ProblemId -> TCM Doc #

PrettyTCM NamedClause # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NamedClause -> TCM Doc #

PrettyTCM PrettyContext # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: PrettyContext -> TCM Doc #

PrettyTCM AbsurdPattern # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: AbsurdPattern -> TCM Doc #

PrettyTCM DotPattern # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: DotPattern -> TCM Doc #

PrettyTCM AsBinding # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: AsBinding -> TCM Doc #

PrettyTCM ElimType # 
Instance details

Defined in Agda.TypeChecking.Records

Methods

prettyTCM :: ElimType -> TCM Doc #

PrettyTCM Node # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: Node -> TCM Doc #

PrettyTCM SplitTag # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

prettyTCM :: SplitTag -> TCM Doc #

PrettyTCM SplitPatVar # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: SplitPatVar -> TCM Doc #

PrettyTCM ErrorPart # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

prettyTCM :: ErrorPart -> TCM Doc #

PrettyTCM HypSizeConstraint # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: HypSizeConstraint -> TCM Doc #

PrettyTCM SizeConstraint #

Assumes we are in the right context.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: SizeConstraint -> TCM Doc #

PrettyTCM SizeMeta # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: SizeMeta -> TCM Doc #

PrettyTCM SplitClause #

For debugging only.

Instance details

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: SplitClause -> TCM Doc #

PrettyTCM a => PrettyTCM [a] # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: [a] -> TCM Doc #

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Named_ a -> TCM Doc #

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Dom a -> TCM Doc #

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Arg a -> TCM Doc #

PrettyTCM a => PrettyTCM (WithHiding a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithHiding a -> TCM Doc #

PrettyTCM (QNamed Clause) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QNamed Clause -> TCM Doc #

(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Substitution' a -> TCM Doc #

PrettyTCM a => PrettyTCM (Pattern' a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Pattern' a -> TCM Doc #

PrettyTCM a => PrettyTCM (Blocked a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Blocked a -> TCM Doc #

PrettyTCM (Type' NLPat) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type' NLPat -> TCM Doc #

PrettyTCM (Elim' NLPat) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim' NLPat -> TCM Doc #

PrettyTCM (Elim' DisplayTerm) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim' DisplayTerm -> TCM Doc #

PrettyTCM a => PrettyTCM (MaybeReduced a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MaybeReduced a -> TCM Doc #

PrettyTCM a => PrettyTCM (Judgement a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Judgement a -> TCM Doc #

PrettyTCM a => PrettyTCM (Closure a) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Closure a -> TCM Doc #

PrettyTCM a => PrettyTCM (Masked a) #

Print masked things in double parentheses.

Instance details

Defined in Agda.Termination.Monad

Methods

prettyTCM :: Masked a -> TCM Doc #

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Map k v -> TCM Doc #

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Graph n e -> TCM Doc #

PrettyTCM n => PrettyTCM (WithNode n Occurrence) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithNode n Occurrence -> TCM Doc #

PrettyTCM n => PrettyTCM (WithNode n Edge) # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: WithNode n Edge -> TCM Doc #

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

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 # 
Instance details

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) # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: WithNode n Occurrence -> TCM Doc #

PrettyTCM n => PrettyTCM (WithNode n Edge) # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: WithNode n Edge -> TCM Doc #