Mikan
Safe HaskellNone
LanguageHaskell2010

Mikan.TypeChecking.Unquote.Errors

Description

Diagnostics related to execution of metaprograms.

Synopsis

Documentation

data UnquoteError Source #

An error raised during execution of a metaprogram.

Constructors

BlockedOnMeta TCState Blocker 
CannotDeclareHiddenFunction QName

Attempt to unquoteDecl with Hiding other than NotHidden.

CommitAfterDef 
ConInsteadOfDef QName String String 
DefineDataNotData QName 
DefInsteadOfCon QName String String 
EscapingVariable (Closure Term)

Given meta-program produces unbound variable under extendContext.

FreshNameWhileElaborating 
MissingDeclaration QName 
MissingDefinition QName 
NakedUnquote 
NonCanonical String Term 
PatLamWithoutClauses Term 
StaleMeta TopLevelModuleName MetaId

Attempt to unquote a serialized meta.

TooManyParameters Nat Expr

Attempt to shave of Nat many parameters from function type Expr.

UnboundName QName 

Instances

Instances details
Diagnostic UnquoteError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

diagnosticReason :: UnquoteError -> DiagnosticReason Source #

diagnosticString :: UnquoteError -> String Source #

toSomeDiagnostic :: UnquoteError -> SomeDiagnostic Source #

fromSomeDiagnostic :: SomeDiagnostic -> Maybe UnquoteError Source #

PrettyTCM UnquoteError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

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

NFData UnquoteError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

rnf :: UnquoteError -> () #

Generic UnquoteError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Associated Types

type Rep UnquoteError 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

type Rep UnquoteError = D1 ('MetaData "UnquoteError" "Mikan.TypeChecking.Unquote.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((((C1 ('MetaCons "BlockedOnMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCState) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Blocker)) :+: C1 ('MetaCons "CannotDeclareHiddenFunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "CommitAfterDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConInsteadOfDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))) :+: ((C1 ('MetaCons "DefineDataNotData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "DefInsteadOfCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "EscapingVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Closure Term))) :+: C1 ('MetaCons "FreshNameWhileElaborating" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "MissingDeclaration" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "NakedUnquote" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonCanonical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))) :+: ((C1 ('MetaCons "PatLamWithoutClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "StaleMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId))) :+: (C1 ('MetaCons "TooManyParameters" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "UnboundName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))))

Methods

from :: UnquoteError -> Rep UnquoteError x #

to :: Rep UnquoteError x -> UnquoteError #

Show UnquoteError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

showsPrec :: Int -> UnquoteError -> ShowS #

show :: UnquoteError -> String #

showList :: [UnquoteError] -> ShowS #

type Rep UnquoteError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

type Rep UnquoteError = D1 ('MetaData "UnquoteError" "Mikan.TypeChecking.Unquote.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((((C1 ('MetaCons "BlockedOnMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCState) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Blocker)) :+: C1 ('MetaCons "CannotDeclareHiddenFunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "CommitAfterDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConInsteadOfDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))) :+: ((C1 ('MetaCons "DefineDataNotData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "DefInsteadOfCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "EscapingVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Closure Term))) :+: C1 ('MetaCons "FreshNameWhileElaborating" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "MissingDeclaration" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "NakedUnquote" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonCanonical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))) :+: ((C1 ('MetaCons "PatLamWithoutClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "StaleMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId))) :+: (C1 ('MetaCons "TooManyParameters" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "UnboundName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))))

data ExecError Source #

Error when trying to call an external executable during reflection.

Constructors

ExeNotTrusted ExeName ExeMap

The given executable is not listed as trusted.

ExeNotFound ExeName FilePath

The given executable could not be found under the given path.

ExeNotExecutable ExeName FilePath

The given file path does not have executable permissions.

Instances

Instances details
Diagnostic ExecError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

diagnosticReason :: ExecError -> DiagnosticReason Source #

diagnosticString :: ExecError -> String Source #

toSomeDiagnostic :: ExecError -> SomeDiagnostic Source #

fromSomeDiagnostic :: SomeDiagnostic -> Maybe ExecError Source #

PrettyTCM ExecError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

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

NFData ExecError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

rnf :: ExecError -> () #

Generic ExecError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Associated Types

type Rep ExecError 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

type Rep ExecError = D1 ('MetaData "ExecError" "Mikan.TypeChecking.Unquote.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ExeNotTrusted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeMap)) :+: (C1 ('MetaCons "ExeNotFound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: C1 ('MetaCons "ExeNotExecutable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath))))

Methods

from :: ExecError -> Rep ExecError x #

to :: Rep ExecError x -> ExecError #

Show ExecError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

Methods

showsPrec :: Int -> ExecError -> ShowS #

show :: ExecError -> String #

showList :: [ExecError] -> ShowS #

type Rep ExecError Source # 
Instance details

Defined in Mikan.TypeChecking.Unquote.Errors

type Rep ExecError = D1 ('MetaData "ExecError" "Mikan.TypeChecking.Unquote.Errors" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ExeNotTrusted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeMap)) :+: (C1 ('MetaCons "ExeNotFound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: C1 ('MetaCons "ExeNotExecutable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExeName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath))))