Mikan
Safe HaskellNone
LanguageHaskell2010

Mikan.Interaction.Errors

Description

Diagnostics raised during interactive use.

Synopsis

Documentation

data InteractionError Source #

Errors raised in --interaction mode.

Constructors

CannotGive Expr

Failure of the give interactive tactic.

CannotRefine String

Failure of the refine interactive tactic.

CaseSplitError Doc

Failure of the makeCase interactive tactic.

ExpectedIdentifier Expr

Expected the given expression to be an identifier.

ExpectedApplication

Expected an argument of the form f e1 e2 .. en.

NoActionForInteractionPoint InteractionId

Interaction point has not been reached during type checking.

NoSuchInteractionPoint InteractionId

InteractionId does not resolve to an InteractionPoint.

UnexpectedWhere

where not allowed in hole.

Instances

Instances details
Diagnostic InteractionError Source # 
Instance details

Defined in Mikan.Interaction.Errors

Methods

diagnosticReason :: InteractionError -> DiagnosticReason Source #

diagnosticString :: InteractionError -> String Source #

toSomeDiagnostic :: InteractionError -> SomeDiagnostic Source #

fromSomeDiagnostic :: SomeDiagnostic -> Maybe InteractionError Source #

PrettyTCM InteractionError Source # 
Instance details

Defined in Mikan.Interaction.Errors

Methods

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

NFData InteractionError Source # 
Instance details

Defined in Mikan.Interaction.Errors

Methods

rnf :: InteractionError -> () #

Generic InteractionError Source # 
Instance details

Defined in Mikan.Interaction.Errors

Associated Types

type Rep InteractionError 
Instance details

Defined in Mikan.Interaction.Errors

type Rep InteractionError = D1 ('MetaData "InteractionError" "Mikan.Interaction.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (((C1 ('MetaCons "CannotGive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "CannotRefine" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "CaseSplitError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc)) :+: C1 ('MetaCons "ExpectedIdentifier" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "ExpectedApplication" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoActionForInteractionPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId))) :+: (C1 ('MetaCons "NoSuchInteractionPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "UnexpectedWhere" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: InteractionError -> Rep InteractionError x #

to :: Rep InteractionError x -> InteractionError #

Show InteractionError Source # 
Instance details

Defined in Mikan.Interaction.Errors

Methods

showsPrec :: Int -> InteractionError -> ShowS #

show :: InteractionError -> String #

showList :: [InteractionError] -> ShowS #

type Rep InteractionError Source # 
Instance details

Defined in Mikan.Interaction.Errors

type Rep InteractionError = D1 ('MetaData "InteractionError" "Mikan.Interaction.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (((C1 ('MetaCons "CannotGive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "CannotRefine" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "CaseSplitError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc)) :+: C1 ('MetaCons "ExpectedIdentifier" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "ExpectedApplication" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoActionForInteractionPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId))) :+: (C1 ('MetaCons "NoSuchInteractionPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "UnexpectedWhere" 'PrefixI 'False) (U1 :: Type -> Type))))