ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Pretty

5 types
2 classes
40 values

PackageAgda-2.8.0.2
Exports47
LanguageHaskell2010
LicenceMIT
SourcePretty.hs

value($$) :: Applicative m => m Doc -> m Doc -> m Doc

value($+$) :: Applicative m => m Doc -> m Doc -> m Doc

value(<+>) :: Applicative m => m Doc -> m Doc -> m Doc

value(<?>) :: Applicative m => m Doc -> m Doc -> m Doc

valuebraces :: Functor m => m Doc -> m Doc

valuebrackets :: Functor m => m Doc -> m Doc

valuecolon :: Applicative m => m Doc

valuecomma :: Applicative m => m Doc

valuedbraces :: Functor m => m Doc -> m Doc

valuedoubleQuotes :: Functor m => m Doc -> m Doc

valueequals :: Applicative m => m Doc

valuefsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

valuefwords :: Applicative m => String -> m Doc

valuehang :: Applicative m => m Doc -> Int -> m Doc -> m Doc

valuehcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

valuehsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

valuemultiLineText :: Applicative m => String -> m Doc

valuenest :: Functor m => Int -> m Doc -> m Doc

valueparens :: Functor m => m Doc -> m Doc

valueparensNonEmpty :: Functor m => m Doc -> m Doc

valuepluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc

valuepretty :: (Applicative m, Pretty a) => a -> m Doc

valueprettyA

:: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m)
=> a
-> m Doc

valueprettyAs

:: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m)
=> a
-> m Doc

valueprettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

Comma-separated list in brackets.

valueprettyList_

:: (Applicative m, Semigroup (m Doc), Foldable t)
=> t (m Doc)
-> m Doc

prettyList without the brackets.

valueprettyR

:: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m)
=> r
-> m Doc

For unquote.

valueprettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc

Pretty print with a given context precedence

valueprettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc

valueprettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]

Proper pretty printing of patterns:

valuepshow :: (Applicative m, Show a) => a -> m Doc

valuepunctuate

:: (Applicative m, Semigroup (m Doc), Foldable t)
=> m Doc
-> t (m Doc)
-> [m Doc]

valuepwords :: Applicative m => String -> [m Doc]

valuequotes :: Functor m => m Doc -> m Doc

valuesep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

valuesequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]

sequenceAFoldable == sequenceA . Fold.toList

valuesuperscript :: Applicative m => Int -> m Doc

valuetext :: Applicative m => String -> m Doc

valuevcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

valuevsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

typetype Doc = Doc

typetype MonadPretty (m :: Type -> Type) = MonadAbsToCon m

newtypenewtype PrettyContext

Constructors

PrettyContext Context

Instances1PrettyTCM

PrettyTCM PrettyContextDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty

classclass PrettyTCM a where

Methods

prettyTCM :: MonadPretty m => a -> m Doc

Instances132PrettyTCM, …

PrettyTCM BaseComponentsDefined in Agda-2.8.0.2 · Agda.Mimer.Mimer
PrettyTCM ComponentDefined in Agda-2.8.0.2 · Agda.Mimer.Mimer
PrettyTCM MimerResultDefined in Agda-2.8.0.2 · Agda.Mimer.Mimer
PrettyTCM SearchOptionsDefined in Agda-2.8.0.2 · Agda.Mimer.Mimer
PrettyTCM ExprDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM PatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ProblemEqDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem · orphan
PrettyTCM TypedBindingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ErasedDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM InteractionIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ModalPolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NatDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM PolarityModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ProblemIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ImportedNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM LHSDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ConHeadDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM DBPatVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM DataOrRecord_Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Warning · orphan
PrettyTCM ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM EqualityViewDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM LevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM SortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TelescopeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM BlockerDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM LiteralDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM AbstractNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NamedClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM SplitPatVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.Coverage.Match
PrettyTCM SplitClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.Coverage · orphan
For debugging only.
PrettyTCM SplitTagDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM KeyDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM CallDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Call · orphan
PrettyTCM CallInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Call · orphan
PrettyTCM CandidateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM CheckpointIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM CompareAsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Constraint · orphan
PrettyTCM DisplayTermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ExecErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM GHCBackendErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM InteractionErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM IsForcedDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM JSBackendErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM MissingTypeSignatureInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM NLPSortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NLPTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NLPatDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NegativeUnificationDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM ProblemConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Constraint · orphan
PrettyTCM RewriteRuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM SplitErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM TCErrDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM TCWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Warning · orphan
PrettyTCM TypeCheckingProblemDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TypeErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM UnificationFailureDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM UnquoteErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors · orphan
PrettyTCM WarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty.Warning · orphan
PrettyTCM ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NamedMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NodeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
PrettyTCM OccurrenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM PrettyContextDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM ElimTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Records
PrettyTCM AbsurdPatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM AnnotationPatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM AsBindingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM DotPatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM LeftoverPatternsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM NoLeftInvDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
PrettyTCM UnifyStateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.Types
PrettyTCM UnifyStepDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.Types
PrettyTCM HypSizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
PrettyTCM SizeConstraintDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
Assumes we are in the right context.
PrettyTCM SizeMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Pretty · orphan
PrettyTCM ErrorPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
PrettyTCM PermutationDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM StringDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM BoolDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TextDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (QNamed Clause)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg String)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Bool)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Named_ Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Type' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Elim' DisplayTerm)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (LHSState a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM (Seq OccursWhere)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity · orphan
PrettyTCM a => PrettyTCM (WithHiding a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Blocked a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Pattern' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Masked a)Defined in Agda-2.8.0.2 · Agda.Termination.Monad
Print masked things in double parentheses.
PrettyTCM a => PrettyTCM (DiscrimTree a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Closure a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Judgement a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (MaybeReduced a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (List1 a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Set a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM a => PrettyTCM (Maybe a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM 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

classclass PrettyTCMWithNode a where

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.Pretty
PrettyTCMWithNode (Edge OccursWhere)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity

datadata WithNode n a

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.

Orphan instances

1 instance

Semigroup (TCM Doc)
This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).