Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Pretty

Contents

Orphan instances

Synopsis

($$) :: Applicative m => m Doc -> m Doc -> m Doc
($+$) :: Applicative m => m Doc -> m Doc -> m Doc
(<+>) :: Applicative m => m Doc -> m Doc -> m Doc
(<?>) :: Applicative m => m Doc -> m Doc -> m Doc
braces :: Functor m => m Doc -> m Doc
brackets :: Functor m => m Doc -> m Doc
colon :: Applicative m => m Doc
comma :: Applicative m => m Doc
dbraces :: Functor m => m Doc -> m Doc
defnToNameKind :: Defn -> NameKind
doubleQuotes :: Functor m => m Doc -> m Doc
equals :: Applicative m => m Doc
fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
fwords :: Applicative m => String -> m Doc
githubIssue :: Applicative m => Int -> m Doc
hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
hlArgument :: Functor m => m Doc -> m Doc
hlBound :: Functor m => m Doc -> m Doc
hlComment :: Functor m => m Doc -> m Doc
hlConstructor :: Functor m => Induction -> m Doc -> m Doc
hlDatatype :: Functor m => m Doc -> m Doc
hlField :: Functor m => m Doc -> m Doc
hlFunction :: Functor m => m Doc -> m Doc
hlGeneralizable :: Functor m => m Doc -> m Doc
hlHole :: Functor m => m Doc -> m Doc
hlKeyword :: Functor m => m Doc -> m Doc
hlMacro :: Functor m => m Doc -> m Doc
hlModule :: Functor m => m Doc -> m Doc
hlNumber :: Functor m => m Doc -> m Doc
hlPostulate :: Functor m => m Doc -> m Doc
hlPragma :: Functor m => m Doc -> m Doc
hlPrimitive :: Functor m => m Doc -> m Doc
hlPrimitiveType :: Functor m => m Doc -> m Doc
hlRecord :: Functor m => m Doc -> m Doc
hlString :: Functor m => m Doc -> m Doc
hlSymbol :: Functor m => m Doc -> m Doc
hsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
multiLineText :: Applicative m => String -> m Doc
nest :: Functor m => Int -> m Doc -> m Doc
parens :: Functor m => m Doc -> m Doc
parensNonEmpty :: Functor m => m Doc -> m Doc
pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc
pretty :: (Applicative m, Pretty a) => a -> m Doc
prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc
prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
pshow :: (Applicative m, Show a) => a -> m Doc
punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
pwords :: Applicative m => String -> [m Doc]
quotes :: Functor m => m Doc -> m Doc
sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]
superscript :: Applicative m => Int -> m Doc
text :: Applicative m => String -> m Doc
url :: Applicative m => String -> m Doc
vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
type Doc = Doc
type MonadPretty (m :: Type -> Type) = MonadAbsToCon m
newtype PrettyContext = PrettyContext Context
class PrettyTCM a where
- prettyTCM :: MonadPretty m => a -> m Doc
class PrettyTCMWithNode a where
- prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
data WithNode n a = WithNode n a
type MonadAbsToCon (m :: Type -> Type) = (MonadFileId m, MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

Documentation

($$) :: Applicative m => m Doc -> m Doc -> m Doc infixl 5 Source #

($+$) :: Applicative m => m Doc -> m Doc -> m Doc infixl 5 Source #

(<+>) :: Applicative m => m Doc -> m Doc -> m Doc infixl 6 Source #

(<?>) :: Applicative m => m Doc -> m Doc -> m Doc infixl 6 Source #

braces :: Functor m => m Doc -> m Doc Source #

brackets :: Functor m => m Doc -> m Doc Source #

colon :: Applicative m => m Doc Source #

comma :: Applicative m => m Doc Source #

dbraces :: Functor m => m Doc -> m Doc Source #

defnToNameKind :: Defn -> NameKind Source #

doubleQuotes :: Functor m => m Doc -> m Doc Source #

equals :: Applicative m => m Doc Source #

fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

fwords :: Applicative m => String -> m Doc Source #

githubIssue :: Applicative m => Int -> m Doc Source #

Link to an issue on the Agda bug tracker.

hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc Source #

hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

hlArgument :: Functor m => m Doc -> m Doc Source #

hlBound :: Functor m => m Doc -> m Doc Source #

hlComment :: Functor m => m Doc -> m Doc Source #

hlConstructor :: Functor m => Induction -> m Doc -> m Doc Source #

hlDatatype :: Functor m => m Doc -> m Doc Source #

hlField :: Functor m => m Doc -> m Doc Source #

hlFunction :: Functor m => m Doc -> m Doc Source #

hlGeneralizable :: Functor m => m Doc -> m Doc Source #

hlHole :: Functor m => m Doc -> m Doc Source #

hlKeyword :: Functor m => m Doc -> m Doc Source #

hlMacro :: Functor m => m Doc -> m Doc Source #

hlModule :: Functor m => m Doc -> m Doc Source #

hlNumber :: Functor m => m Doc -> m Doc Source #

hlPostulate :: Functor m => m Doc -> m Doc Source #

hlPragma :: Functor m => m Doc -> m Doc Source #

hlPrimitive :: Functor m => m Doc -> m Doc Source #

hlPrimitiveType :: Functor m => m Doc -> m Doc Source #

hlRecord :: Functor m => m Doc -> m Doc Source #

hlString :: Functor m => m Doc -> m Doc Source #

hlSymbol :: Functor m => m Doc -> m Doc Source #

hsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

multiLineText :: Applicative m => String -> m Doc Source #

nest :: Functor m => Int -> m Doc -> m Doc Source #

parens :: Functor m => m Doc -> m Doc Source #

parensNonEmpty :: Functor m => m Doc -> m Doc Source #

pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc Source #

pretty :: (Applicative m, Pretty a) => a -> m Doc Source #

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

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

prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

Comma-separated list in brackets.

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

prettyList without the brackets.

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

For unquote.

prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc Source #

Pretty print with a given context precedence

prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc Source #

prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc] Source #

Proper pretty printing of patterns:

pshow :: (Applicative m, Show a) => a -> m Doc Source #

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

pwords :: Applicative m => String -> [m Doc] Source #

quotes :: Functor m => m Doc -> m Doc Source #

sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a] Source #

sequenceAFoldable == sequenceA . Fold.toList

superscript :: Applicative m => Int -> m Doc Source #

text :: Applicative m => String -> m Doc Source #

url :: Applicative m => String -> m Doc Source #

vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

type Doc = Doc Source #

type MonadPretty (m :: Type -> Type) = MonadAbsToCon m Source #

newtype PrettyContext Source #

Constructors

PrettyContext Context

Instances

Instances details

PrettyTCM PrettyContext Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PrettyContext -> m Doc Source #

class PrettyTCM a where Source #

Methods

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

Instances

Instances details

PrettyTCM InteractionError Source #
Instance details Defined in Mikan.Interaction.Errors Methods prettyTCM :: MonadPretty m => InteractionError -> m Doc Source #
PrettyTCM BaseComponents Source #
Instance details Defined in Mikan.Mimer.Types Methods prettyTCM :: MonadPretty m => BaseComponents -> m Doc Source #
PrettyTCM Component Source #
Instance details Defined in Mikan.Mimer.Types Methods prettyTCM :: MonadPretty m => Component -> m Doc Source #
PrettyTCM MimerResult Source #
Instance details Defined in Mikan.Mimer.Types Methods prettyTCM :: MonadPretty m => MimerResult -> m Doc Source #
PrettyTCM SearchOptions Source #
Instance details Defined in Mikan.Mimer.Types Methods prettyTCM :: MonadPretty m => SearchOptions -> m Doc Source #
PrettyTCM Expr Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
PrettyTCM Pattern Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern -> m Doc Source #
PrettyTCM ProblemEq Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
PrettyTCM TypedBinding Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source #
PrettyTCM AbstractName Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => AbstractName -> m Doc Source #
PrettyTCM ConHead Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ConHead -> m Doc Source #
PrettyTCM ModuleName Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ModuleName -> m Doc Source #
PrettyTCM Name Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Name -> m Doc Source #
PrettyTCM QName Source #	Automatically highlights the resulting document with the correct name kind.
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QName -> m Doc Source #
PrettyTCM DataOrRecord_ Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => DataOrRecord_ -> m Doc Source #
PrettyTCM InteractionId Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => InteractionId -> m Doc Source #
PrettyTCM MetaId Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaId -> m Doc Source #
PrettyTCM Nat Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Nat -> m Doc Source #
PrettyTCM ProblemId Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemId -> m Doc Source #
PrettyTCM ImportedName Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ImportedName -> m Doc Source #
PrettyTCM LHS Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => LHS -> m Doc Source #
PrettyTCM DeclarationException' Source #
Instance details Defined in Mikan.TypeChecking.Monad.Diagnostic Methods prettyTCM :: MonadPretty m => DeclarationException' -> m Doc Source #
PrettyTCM DeclarationWarning Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => DeclarationWarning -> m Doc Source #
PrettyTCM Name Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Name -> m Doc Source #
PrettyTCM QName Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QName -> m Doc Source #
PrettyTCM Blocker Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocker -> m Doc Source #
PrettyTCM Clause Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Clause -> m Doc Source #
PrettyTCM DBPatVar Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => DBPatVar -> m Doc Source #
PrettyTCM Telescope Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
PrettyTCM Teletype Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Teletype -> m Doc Source #
PrettyTCM Elim Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim -> m Doc Source #
PrettyTCM Level Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Level -> m Doc Source #
PrettyTCM Sort Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Sort -> m Doc Source #
PrettyTCM Term Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Term -> m Doc Source #
PrettyTCM Type Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type -> m Doc Source #
PrettyTCM Literal Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Literal -> m Doc Source #
PrettyTCM Range Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Range -> m Doc Source #
PrettyTCM IgnoredRecordDeclaration Source #
Instance details Defined in Mikan.Syntax.Scope.Errors Methods prettyTCM :: MonadPretty m => IgnoredRecordDeclaration -> m Doc Source #
PrettyTCM PatternSynonymError Source #
Instance details Defined in Mikan.Syntax.Scope.Errors Methods prettyTCM :: MonadPretty m => PatternSynonymError -> m Doc Source #
PrettyTCM TopLevelModuleName Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #
PrettyTCM NamedClause Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source #
PrettyTCM CallMatrix Source #
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => CallMatrix -> m Doc Source #
PrettyTCM CallPath Source #	Show all nodes.
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => CallPath -> m Doc Source #
PrettyTCM NoConstraintsError Source #
Instance details Defined in Mikan.TypeChecking.Constraints Methods prettyTCM :: MonadPretty m => NoConstraintsError -> m Doc Source #
PrettyTCM ConversionError Source #
Instance details Defined in Mikan.TypeChecking.Conversion.Errors Methods prettyTCM :: MonadPretty m => ConversionError -> m Doc Source #
PrettyTCM ConversionZipper Source #
Instance details Defined in Mikan.TypeChecking.Conversion.Errors Methods prettyTCM :: MonadPretty m => ConversionZipper -> m Doc Source #
PrettyTCM FailedCompareAs Source #
Instance details Defined in Mikan.TypeChecking.Conversion.Errors Methods prettyTCM :: MonadPretty m => FailedCompareAs -> m Doc Source #
PrettyTCM SplitError Source #
Instance details Defined in Mikan.TypeChecking.Coverage.Errors Methods prettyTCM :: MonadPretty m => SplitError -> m Doc Source #
PrettyTCM UnificationFailure Source #
Instance details Defined in Mikan.TypeChecking.Coverage.Errors Methods prettyTCM :: MonadPretty m => UnificationFailure -> m Doc Source #
PrettyTCM WrongProjectionName Source #
Instance details Defined in Mikan.TypeChecking.Coverage.Errors Methods prettyTCM :: MonadPretty m => WrongProjectionName -> m Doc Source #
PrettyTCM SplitClause Source #	For debugging only.
Instance details Defined in Mikan.TypeChecking.Coverage Methods prettyTCM :: MonadPretty m => SplitClause -> m Doc Source #
PrettyTCM SplitPatVar Source #
Instance details Defined in Mikan.TypeChecking.Coverage.SplitPattern Methods prettyTCM :: MonadPretty m => SplitPatVar -> m Doc Source #
PrettyTCM SplitTag Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => SplitTag -> m Doc Source #
PrettyTCM Key Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Key -> m Doc Source #
PrettyTCM DeferredError Source #
Instance details Defined in Mikan.TypeChecking.Errors.Deferred Methods prettyTCM :: MonadPretty m => DeferredError -> m Doc Source #
PrettyTCM MetaSet Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaSet -> m Doc Source #
PrettyTCM InstanceSearchError Source #
Instance details Defined in Mikan.TypeChecking.InstanceArguments.Errors Methods prettyTCM :: MonadPretty m => InstanceSearchError -> m Doc Source #
PrettyTCM Call Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Call Methods prettyTCM :: MonadPretty m => Call -> m Doc Source #
PrettyTCM CallInfo Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Call Methods prettyTCM :: MonadPretty m => CallInfo -> m Doc Source #
PrettyTCM Candidate Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Candidate -> m Doc Source #
PrettyTCM CheckpointId Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => CheckpointId -> m Doc Source #
PrettyTCM CompareAs Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => CompareAs -> m Doc Source #
PrettyTCM Constraint Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Constraint Methods prettyTCM :: MonadPretty m => Constraint -> m Doc Source #
PrettyTCM DisplayTerm Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => DisplayTerm -> m Doc Source #
PrettyTCM IsForced Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => IsForced -> m Doc Source #
PrettyTCM MissingTypeSignatureInfo Source #
Instance details Defined in Mikan.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => MissingTypeSignatureInfo -> m Doc Source #
PrettyTCM NegativeUnification Source #
Instance details Defined in Mikan.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => NegativeUnification -> m Doc Source #
PrettyTCM ProblemConstraint Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Constraint Methods prettyTCM :: MonadPretty m => ProblemConstraint -> m Doc Source #
PrettyTCM TCErr Source #
Instance details Defined in Mikan.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => TCErr -> m Doc Source #
PrettyTCM TypeCheckingProblem Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypeCheckingProblem -> m Doc Source #
PrettyTCM TypeError Source #
Instance details Defined in Mikan.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => TypeError -> m Doc Source #
PrettyTCM UnsolvedWarning Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => UnsolvedWarning -> m Doc Source #
PrettyTCM Warning Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => Warning -> m Doc Source #
PrettyTCM Comparison Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source #
PrettyTCM Context Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Context -> m Doc Source #
PrettyTCM ContextEntry Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source #
PrettyTCM NamedMeta Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedMeta -> m Doc Source #
PrettyTCM Polarity Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Polarity -> m Doc Source #
PrettyTCM TopLevelModuleNameWithSourceFile Source #
Instance details Defined in Mikan.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => TopLevelModuleNameWithSourceFile -> m Doc Source #
PrettyTCM EqualityView Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => EqualityView -> m Doc Source #
PrettyTCM EncodedDiagnostic Source #
Instance details Defined in Mikan.TypeChecking.Monad.Diagnostic Methods prettyTCM :: MonadPretty m => EncodedDiagnostic -> m Doc Source #
PrettyTCM SomeDiagnostic Source #
Instance details Defined in Mikan.TypeChecking.Monad.Diagnostic Methods prettyTCM :: MonadPretty m => SomeDiagnostic -> m Doc Source #
PrettyTCM Node Source #
Instance details Defined in Mikan.TypeChecking.Positivity Methods prettyTCM :: MonadPretty m => Node -> m Doc Source #
PrettyTCM Occurrence Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Occurrence -> m Doc Source #
PrettyTCM PrettyContext Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PrettyContext -> m Doc Source #
PrettyTCM ElimType Source #
Instance details Defined in Mikan.TypeChecking.Records Methods prettyTCM :: MonadPretty m => ElimType -> m Doc Source #
PrettyTCM UnboundParameters Source #
Instance details Defined in Mikan.TypeChecking.Rules.Data Methods prettyTCM :: MonadPretty m => UnboundParameters -> m Doc Source #
PrettyTCM AbsurdPattern Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc Source #
PrettyTCM AnnotationPattern Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc Source #
PrettyTCM AsBinding Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AsBinding -> m Doc Source #
PrettyTCM DotPattern Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => DotPattern -> m Doc Source #
PrettyTCM LeftoverPatterns Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc Source #
PrettyTCM DigestedUnifyStep Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => DigestedUnifyStep -> m Doc Source #
PrettyTCM NoLeftInv Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => NoLeftInv -> m Doc Source #
PrettyTCM UnifyState Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Unify.Types Methods prettyTCM :: MonadPretty m => UnifyState -> m Doc Source #
PrettyTCM UnifyStep Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Unify.Types Methods prettyTCM :: MonadPretty m => UnifyStep -> m Doc Source #
PrettyTCM ErrorPart Source #
Instance details Defined in Mikan.TypeChecking.Unquote Methods prettyTCM :: MonadPretty m => ErrorPart -> m Doc Source #
PrettyTCM ExecError Source #
Instance details Defined in Mikan.TypeChecking.Unquote.Errors Methods prettyTCM :: MonadPretty m => ExecError -> m Doc Source #
PrettyTCM UnquoteError Source #
Instance details Defined in Mikan.TypeChecking.Unquote.Errors Methods prettyTCM :: MonadPretty m => UnquoteError -> m Doc Source #
PrettyTCM Permutation Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Permutation -> m Doc Source #
PrettyTCM VarSet Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => VarSet -> m Doc Source #
PrettyTCM ShortText Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ShortText -> m Doc Source #
PrettyTCM String Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => String -> m Doc Source #
PrettyTCM Bool Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Bool -> m Doc Source #
PrettyTCM (QNamed Clause) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #
PrettyTCM (Arg Expr) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #
PrettyTCM (Arg Term) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Term -> m Doc Source #
PrettyTCM (Arg Type) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Type -> m Doc Source #
PrettyTCM (Arg ShortText) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg ShortText -> m Doc Source #
PrettyTCM (Arg Bool) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Bool -> m Doc Source #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
PrettyTCM (NamedArg Term) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
PrettyTCM (Named_ Term) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ Term -> m Doc Source #
PrettyTCM a => PrettyTCM (WithHiding a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => WithHiding a -> m Doc Source #
(PrettyTCM a, Subst a) => PrettyTCM (Abs a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Abs a -> m Doc Source #
PrettyTCM (Elim' DisplayTerm) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc Source #
PrettyTCM a => PrettyTCM (Pattern' a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern' a -> m Doc Source #
PrettyTCM a => PrettyTCM (Blocked a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocked a -> m Doc Source #
PrettyTCM (Dom Type) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom Type -> m Doc Source #
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #
PrettyTCM cinfo => PrettyTCM (Call cinfo) Source #
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => Call cinfo -> m Doc Source #
PrettyTCM cinfo => PrettyTCM (CallGraph cinfo) Source #
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => CallGraph cinfo -> m Doc Source #
PrettyTCM cinfo => PrettyTCM (CMSet cinfo) Source #
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => CMSet cinfo -> m Doc Source #
PrettyTCM cinfo => PrettyTCM (CallMatrixAug cinfo) Source #
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => CallMatrixAug cinfo -> m Doc Source #
PrettyTCM a => PrettyTCM (DiscrimTree a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => DiscrimTree a -> m Doc Source #
PrettyTCM a => PrettyTCM (FlexRig' a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => FlexRig' a -> m Doc Source #
PrettyTCM a => PrettyTCM (VarMap' a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => VarMap' a -> m Doc Source #
PrettyTCM a => PrettyTCM (VarOcc' a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => VarOcc' a -> m Doc Source #
PrettyTCM a => PrettyTCM (Closure a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Closure a -> m Doc Source #
PrettyTCM a => PrettyTCM (Judgement a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Judgement a -> m Doc Source #
PrettyTCM a => PrettyTCM (MaybeReduced a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MaybeReduced a -> m Doc Source #
PrettyTCM (TCWarning' a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => TCWarning' a -> m Doc Source #
PrettyTCM (LHSState a) Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LHSState a -> m Doc Source #
PrettyTCM a => PrettyTCM (List1 a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => List1 a -> m Doc Source #
PrettyTCM (Seq OccursWhere) Source #
Instance details Defined in Mikan.TypeChecking.Positivity Methods prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source #
PrettyTCM a => PrettyTCM (Set a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Set a -> m Doc Source #
PrettyTCM a => PrettyTCM (Maybe a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Maybe a -> m Doc Source #
PrettyTCM a => PrettyTCM [a] Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => [a] -> m Doc Source #
(Pretty a, Pretty b) => PrettyTCM (OutputForm a b) Source #
Instance details Defined in Mikan.Interaction.BasicOps Methods prettyTCM :: MonadPretty m => OutputForm a b -> m Doc Source #
(PrettyTCM x, PrettyTCM a) => PrettyTCM (Boundary' x a) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Boundary' x a -> m Doc Source #
(PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Graph n e -> m Doc Source #
(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Map k v -> m Doc Source #
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => (a, b) -> m Doc Source #
(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => (a, b, c) -> m Doc Source #

class PrettyTCMWithNode a where Source #

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 Source #

Instances

Instances details

PrettyTCMWithNode Occurrence Source #
Instance details Defined in Mikan.TypeChecking.Pretty Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n Occurrence -> m Doc Source #
PrettyTCMWithNode (Edge OccursWhere) Source #
Instance details Defined in Mikan.TypeChecking.Positivity.OccurrenceAnalysis Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source #
Pretty a => PrettyTCMWithNode (Edge a) Source #
Instance details Defined in Mikan.TypeChecking.Positivity Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge a) -> m Doc Source #

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a

type MonadAbsToCon (m :: Type -> Type) = (MonadFileId m, MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc)) Source #

Preconditions to run the AbstractToConcrete translation.

Orphan instances

Semigroup (TCM Doc) Source #	This instance is more specific than a generic instance `Semigroup a => Semigroup (TCM a)`.
Instance details Methods (<>) :: TCM Doc -> TCM Doc -> TCM Doc # sconcat :: NonEmpty (TCM Doc) -> TCM Doc # stimes :: Integral b => b -> TCM Doc -> TCM Doc #