Agda.TypeChecking.Unquote

Documentation

agdaTermType :: TCM Type

agdaTypeType :: TCM Type

qNameType :: TCM Type

data Dirty

Constructors

Dirty

Clean

Instances

Eq Dirty

Defined in Agda.TypeChecking.Unquote

Methods

(==) :: Dirty -> Dirty -> Bool

(/=) :: Dirty -> Dirty -> Bool

type UnquoteState = (Dirty, TCState)

type UnquoteM = ReaderT Context (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))

type UnquoteRes a = Either UnquoteError ((a, UnquoteState), [QName])

unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)

packUnquoteM :: (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a

runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName]))

liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b

liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)) -> UnquoteM a -> UnquoteM b -> UnquoteM c

inOriginalContext :: UnquoteM a -> UnquoteM a

isCon :: ConHead -> TCM Term -> UnquoteM Bool

isDef :: QName -> TCM Term -> UnquoteM Bool

reduceQuotedTerm :: Term -> UnquoteM Term

class Unquote a where

Methods

unquote :: Term -> UnquoteM a

Instances

Unquote QName

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM QName

Unquote ArgInfo

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ArgInfo

Unquote Hiding

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Hiding

Unquote MetaId

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId

Unquote Modality

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Modality

Unquote Quantity

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Quantity

Unquote Relevance

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Relevance

Unquote Blocker

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Blocker

Unquote Literal

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Literal

Unquote Clause

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Clause

Unquote Elim

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Elim

Unquote Pattern

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Pattern

Unquote Sort

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Sort

Unquote Term

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term0 -> UnquoteM Term

Unquote ErrorPart

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ErrorPart

Unquote Word64

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Word64

Unquote Text

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Text

Unquote Integer

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Integer

Unquote Bool

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Bool

Unquote Char

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Char

Unquote Double

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Double

Unquote a => Unquote (Arg a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Arg a)

Unquote a => Unquote (Dom a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a)

Unquote a => Unquote (Abs a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Abs a)

Unquote a => Unquote [a]

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM [a]

(Unquote a, Unquote b) => Unquote (a, b)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (a, b)

unquoteN :: Unquote a => Arg Term -> UnquoteM a

choice :: Monad m => [(m Bool, m a)] -> m a -> m a

ensureDef :: QName -> UnquoteM QName

ensureCon :: QName -> UnquoteM QName

pickName :: Type -> String

unquoteString :: Term -> UnquoteM String

unquoteNString :: Arg Term -> UnquoteM Text

data ErrorPart

Constructors

StrPart String

TermPart Expr

PattPart Pattern

NamePart QName

Instances

PrettyTCM ErrorPart

Defined in Agda.TypeChecking.Unquote

Methods

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

Unquote ErrorPart

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ErrorPart

renderErrorParts :: [ErrorPart] -> TCM Doc

We do a little bit of work here to make it possible to generate nice layout for multi-line error messages. Specifically we split the parts into lines (indicated by n in a string part) and vcat all the lines.

unquoteTCM :: Term -> Term -> UnquoteM Term

Argument should be a term of type Term → TCM A for some A. Returns the resulting term of type A. The second argument is the term for the hole, which will typically be a metavariable. This is passed to the computation (quoted).

evalTCM :: Term -> UnquoteM Term

Trusted executables

type ExeArg = Text

type StdIn = Text

type StdOut = Text

type StdErr = Text

requireAllowExec :: TCM ()

Raise an error if the --allow-exec option was not specified.

exitCodeToNat :: ExitCode -> Nat

Convert an ExitCode to an Agda natural number.

tcExec :: ExeName -> [ExeArg] -> StdIn -> TCM Term

Call a trusted executable with the given arguments and input.

Returns the exit code, stdout, and stderr.

raiseExeNotTrusted :: ExeName -> Map ExeName FilePath -> TCM a

Raise an error if the trusted executable cannot be found.

raiseExeNotFound :: ExeName -> FilePath -> TCM a

raiseExeNotExecutable :: ExeName -> FilePath -> TCM a