Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Unquote

Synopsis

Documentation

data Dirty Source #

Constructors

Dirty 
Clean 

Instances

Instances details
Eq Dirty Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

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

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

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

class Unquote a where Source #

Methods

unquote :: Term -> UnquoteM a Source #

Instances

Instances details
Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Blocker Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Literal Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Clause Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Elim Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Sort Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Term Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Word64 Source #

Unquote Text Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Text Source #

Unquote Integer Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Integer Source #

Unquote Bool Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Bool Source #

Unquote Char Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Char Source #

Unquote Double Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Double Source #

Unquote a => Unquote (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Arg a) Source #

Unquote a => Unquote (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a) Source #

Unquote a => Unquote (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Abs a) Source #

Unquote a => Unquote [a] Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM [a] Source #

(Unquote a, Unquote b) => Unquote (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

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

pickName :: Type -> String Source #

data ErrorPart Source #

Instances

Instances details
PrettyTCM ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

renderErrorParts :: [ErrorPart] -> TCM Doc Source #

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

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).

Trusted executables

type ExeArg = Text Source #

type StdIn = Text Source #

type StdOut = Text Source #

type StdErr = Text Source #

requireAllowExec :: TCM () Source #

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

exitCodeToNat :: ExitCode -> Nat Source #

Convert an ExitCode to an Agda natural number.

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

Call a trusted executable with the given arguments and input.

Returns the exit code, stdout, and stderr.

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

Raise an error if the trusted executable cannot be found.

raiseExeNotFound :: ExeName -> FilePath -> TCM a Source #