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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Pretty

Contents

- Wrappers for pretty printing combinators
- The PrettyTCM class

Synopsis

- 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
- ($+$) :: 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
- 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
- prettyList_ :: [TCM Doc] -> TCM Doc
- punctuate :: TCM Doc -> [TCM Doc] -> [TCM Doc]
- class PrettyTCM a where
  - prettyTCM :: a -> TCM Doc
- prettyTCMCtx :: PrettyTCM a => Precedence -> a -> TCM Doc
- newtype PrettyContext = PrettyContext Context
- prettyTCMPatterns :: [NamedArg DeBruijnPattern] -> TCM [Doc]
- prettyTCMPatternList :: [NamedArg DeBruijnPattern] -> TCM Doc
- data WithNode n a = WithNode n a

# Wrappers for pretty printing combinators

type Doc = Doc Source #

comma :: TCM Doc Source #

colon :: TCM Doc Source #

equals :: TCM 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 #

text :: String -> TCM Doc Source #

multiLineText :: String -> TCM Doc Source #

pwords :: String -> [TCM Doc] Source #

fwords :: String -> TCM Doc Source #

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

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

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

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

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

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

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

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

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

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

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

nest :: Int -> TCM Doc -> TCM Doc Source #

braces :: TCM Doc -> TCM Doc Source #

dbraces :: TCM Doc -> TCM Doc Source #

brackets :: TCM Doc -> TCM Doc Source #

parens :: TCM Doc -> TCM Doc Source #

pshow :: Show a => 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.

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

# The PrettyTCM class

class PrettyTCM a where Source #

Methods

prettyTCM :: a -> TCM Doc Source #

Instances

PrettyTCM Bool Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Bool -> TCM Doc Source #
PrettyTCM Range Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Range -> TCM Doc Source #
PrettyTCM Permutation Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Permutation -> TCM Doc Source #
PrettyTCM MetaId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MetaId -> TCM Doc Source #
PrettyTCM Nat Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Nat -> TCM Doc Source #
PrettyTCM Relevance Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Relevance -> TCM Doc Source #
PrettyTCM QName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QName -> TCM Doc Source #
PrettyTCM Name Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Name -> TCM Doc Source #
PrettyTCM ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ModuleName -> TCM Doc Source #
PrettyTCM QName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QName -> TCM Doc Source #
PrettyTCM Name Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Name -> TCM Doc Source #
PrettyTCM Literal Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Literal -> TCM Doc Source #
PrettyTCM Term Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Term -> TCM Doc Source #
PrettyTCM Occurrence Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Occurrence -> TCM Doc Source #
PrettyTCM EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: EqualityView -> TCM Doc Source #
PrettyTCM DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: DBPatVar -> TCM Doc Source #
PrettyTCM Clause Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Clause -> TCM Doc Source #
PrettyTCM Level Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Level -> TCM Doc Source #
PrettyTCM Sort Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Sort -> TCM Doc Source #
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc Source #
PrettyTCM Type Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type -> TCM Doc Source #
PrettyTCM ArgName Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ArgName -> TCM Doc Source #
PrettyTCM Elim Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim -> TCM Doc Source #
PrettyTCM Term Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Term -> TCM Doc Source #
PrettyTCM ConHead Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ConHead -> TCM Doc Source #
PrettyTCM SplitTag Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: SplitTag -> TCM Doc Source #
PrettyTCM ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: ProblemEq -> TCM Doc Source #
PrettyTCM TypedBinding Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: TypedBinding -> TCM Doc Source #
PrettyTCM Expr Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Expr -> TCM Doc Source #
PrettyTCM TCErr Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TCErr -> TCM Doc Source #
PrettyTCM TypeError Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TypeError -> TCM Doc Source #
PrettyTCM UnificationFailure Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: UnificationFailure -> TCM Doc Source #
PrettyTCM NegativeUnification Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: NegativeUnification -> TCM Doc Source #
PrettyTCM SplitError Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: SplitError -> TCM Doc Source #
PrettyTCM CallInfo Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: CallInfo -> TCM Doc Source #
PrettyTCM TCWarning Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TCWarning -> TCM Doc Source #
PrettyTCM Warning Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: Warning -> TCM Doc Source #
PrettyTCM Call Source # |
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: Call -> TCM Doc Source #
PrettyTCM IsForced Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: IsForced -> TCM Doc Source #
PrettyTCM Polarity Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Polarity -> TCM Doc Source #
PrettyTCM RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: RewriteRule -> TCM Doc Source #
PrettyTCM NLPType Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NLPType -> TCM Doc Source #
PrettyTCM NLPat Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NLPat -> TCM Doc Source #
PrettyTCM DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: DisplayTerm -> TCM Doc Source #
PrettyTCM TypeCheckingProblem Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: TypeCheckingProblem -> TCM Doc Source #
PrettyTCM Comparison Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Comparison -> TCM Doc Source #
PrettyTCM Constraint Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Constraint -> TCM Doc Source #
PrettyTCM ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ProblemConstraint -> TCM Doc Source #
PrettyTCM CheckpointId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: CheckpointId -> TCM Doc Source #
PrettyTCM ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ProblemId -> TCM Doc Source #
PrettyTCM NamedClause Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NamedClause -> TCM Doc Source #
PrettyTCM PrettyContext Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: PrettyContext -> TCM Doc Source #
PrettyTCM AbsurdPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: AbsurdPattern -> TCM Doc Source #
PrettyTCM DotPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: DotPattern -> TCM Doc Source #
PrettyTCM AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: AsBinding -> TCM Doc Source #
PrettyTCM ElimType Source # |
Instance details Defined in Agda.TypeChecking.Records Methods prettyTCM :: ElimType -> TCM Doc Source #
PrettyTCM Node Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: Node -> TCM Doc Source #
PrettyTCM SplitPatVar Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods prettyTCM :: SplitPatVar -> TCM Doc Source #
PrettyTCM ErrorPart Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods prettyTCM :: ErrorPart -> TCM Doc Source #
PrettyTCM HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: HypSizeConstraint -> TCM Doc Source #
PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: SizeConstraint -> TCM Doc Source #
PrettyTCM SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: SizeMeta -> TCM Doc Source #
PrettyTCM SplitClause Source # | For debugging only.
Instance details Defined in Agda.TypeChecking.Coverage Methods prettyTCM :: SplitClause -> TCM Doc Source #
PrettyTCM a => PrettyTCM [a] Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: [a] -> TCM Doc Source #
PrettyTCM (Seq OccursWhere) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: Seq OccursWhere -> TCM Doc Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Named_ a -> TCM Doc Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Dom a -> TCM Doc Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Arg a -> TCM Doc Source #
PrettyTCM a => PrettyTCM (WithHiding a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: WithHiding a -> TCM Doc Source #
PrettyTCM (QNamed Clause) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QNamed Clause -> TCM Doc Source #
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Substitution' a -> TCM Doc Source #
PrettyTCM a => PrettyTCM (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Pattern' a -> TCM Doc Source #
PrettyTCM a => PrettyTCM (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Blocked a -> TCM Doc Source #
PrettyTCM (Type' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type' NLPat -> TCM Doc Source #
PrettyTCM (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' NLPat -> TCM Doc Source #
PrettyTCM (Elim' DisplayTerm) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' DisplayTerm -> TCM Doc Source #
PrettyTCM a => PrettyTCM (MaybeReduced a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MaybeReduced a -> TCM Doc Source #
PrettyTCM a => PrettyTCM (Judgement a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Judgement a -> TCM Doc Source #
PrettyTCM a => PrettyTCM (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Closure a -> TCM Doc Source #
PrettyTCM a => PrettyTCM (Masked a) Source # | Print masked things in double parentheses.
Instance details Defined in Agda.Termination.Monad Methods prettyTCM :: Masked a -> TCM Doc Source #
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: (a, b) -> TCM Doc Source #
(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Map k v -> TCM Doc Source #
(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Graph n e -> TCM Doc Source #
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: WithNode n Occurrence -> TCM Doc Source #
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: WithNode n (Edge OccursWhere) -> TCM Doc Source #
(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: (a, b, c) -> TCM Doc Source #

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

Pretty print with a given context precedence

newtype PrettyContext Source #

Constructors

PrettyContext Context |

Instances

PrettyTCM PrettyContext Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: PrettyContext -> TCM Doc Source #

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

Proper pretty printing of patterns:

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

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a |

Instances

PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: WithNode n Occurrence -> TCM Doc Source #
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: WithNode n (Edge OccursWhere) -> TCM Doc Source #