ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Pretty
Synopsis
- value $$
- value $+$
- value <+>
- value <?>
- value braces
- value brackets
- value colon
- value comma
- value dbraces
- value doubleQuotes
- value equals
- value fsep
- value fwords
- value hang
- value hcat
- value hsep
- value multiLineText
- value nest
- value parens
- value parensNonEmpty
- value pluralS
- value pretty
- value prettyA
- value prettyAs
- value prettyList
- value prettyList_
- value prettyR
- value prettyTCMCtx
- value prettyTCMPatternList
- value prettyTCMPatterns
- value pshow
- value punctuate
- value pwords
- value quotes
- value sep
- value sequenceAFoldable
- value superscript
- value text
- value vcat
- value vsep
- type Doc
- type MonadPretty
- newtype PrettyContext
- class PrettyTCM
- class PrettyTCMWithNode
- data WithNode
- type MonadAbsToCon
- PackageAgda-2.8.0.2
- Exports47
- LanguageHaskell2010
- LicenceMIT
- SourcePretty.hs
Comma-separated list in brackets.
prettyList without the brackets.
For unquote.
Pretty print with a given context precedence
Proper pretty printing of patterns:
sequenceAFoldable == sequenceA . Fold.toListConstructors
Instances1PrettyTCM
PrettyTCM PrettyContextDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Methods
prettyTCM :: MonadPretty m => a -> m Doc
Instances132PrettyTCM, …
PrettyTCM BaseComponentsDefined in Agda-2.8.0.2 · Agda.Mimer.MimerPrettyTCM ComponentDefined in Agda-2.8.0.2 · Agda.Mimer.MimerPrettyTCM MimerResultDefined in Agda-2.8.0.2 · Agda.Mimer.MimerPrettyTCM SearchOptionsDefined in Agda-2.8.0.2 · Agda.Mimer.MimerPrettyTCM ExprDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM PatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ProblemEqDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem · orphanPrettyTCM TypedBindingDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ErasedDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM InteractionIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ModalPolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NatDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM PolarityModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ProblemIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ImportedNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM LHSDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ConHeadDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM DBPatVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM DataOrRecord_Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Warning · orphanPrettyTCM ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM EqualityViewDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM LevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM SortDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM TelescopeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM TypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM BlockerDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM LiteralDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM AbstractNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NamedClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM SplitPatVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.Coverage.MatchPrettyTCM SplitClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.Coverage · orphanFor debugging only.
PrettyTCM SplitTagDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM KeyDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM CallDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Call · orphanPrettyTCM CallInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Call · orphanPrettyTCM CandidateDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM CheckpointIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM CompareAsDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Constraint · orphanPrettyTCM DisplayTermDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ExecErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM GHCBackendErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM InteractionErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM IsForcedDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM JSBackendErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM MissingTypeSignatureInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM NLPSortDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NLPTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NLPatDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NegativeUnificationDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM ProblemConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Constraint · orphanPrettyTCM RewriteRuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM SplitErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM TCErrDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM TCWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Warning · orphanPrettyTCM TypeCheckingProblemDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM TypeErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM UnificationFailureDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM UnquoteErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphanPrettyTCM WarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Warning · orphanPrettyTCM ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NamedMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM NodeDefined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityPrettyTCM OccurrenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM PrettyContextDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM ElimTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.RecordsPrettyTCM AbsurdPatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.ProblemPrettyTCM AnnotationPatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.ProblemPrettyTCM AsBindingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.ProblemPrettyTCM DotPatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.ProblemPrettyTCM LeftoverPatternsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.ProblemPrettyTCM NoLeftInvDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.LeftInversePrettyTCM UnifyStateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.TypesPrettyTCM UnifyStepDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.TypesPrettyTCM HypSizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphanPrettyTCM SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphanAssumes we are in the right context.
PrettyTCM SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphanPrettyTCM ErrorPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquotePrettyTCM PermutationDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM StringDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM BoolDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM TextDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (QNamed Clause)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Arg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Arg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Arg Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Arg String)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Arg Bool)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (NamedArg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (NamedArg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Named_ Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Type' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Elim' DisplayTerm)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (LHSState a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.ProblemPrettyTCM (Seq OccursWhere)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity · orphanPrettyTCM a => PrettyTCM (WithHiding a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Blocked a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Pattern' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Masked a)Defined in Agda-2.8.0.2 · Agda.Termination.MonadPrint masked things in double parentheses.
PrettyTCM a => PrettyTCM (DiscrimTree a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Closure a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Judgement a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (MaybeReduced a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (List1 a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Set a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM (Maybe a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM a => PrettyTCM [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(PrettyTCM a, Subst a) => PrettyTCM (Abs a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(Pretty a, Pretty b) => PrettyTCM (OutputForm a b)Defined in Agda-2.8.0.2 · Agda.Interaction.BasicOps · orphan(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(PrettyTCM x, PrettyTCM a) => PrettyTCM (Boundary' x a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Pretty-print something paired with a (printable) node. | This intermediate typeclass exists to avoid UndecidableInstances.
Methods
prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
Instances2PrettyTCMWithNode
PrettyTCMWithNode OccurrenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCMWithNode (Edge OccursWhere)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
Pairing something with a node (for printing only).
Constructors
WithNode n a
type
type MonadAbsToCon (m :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))Preconditions to run the AbstractToConcrete translation.