Agda-2.6.2.1.20220320: 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 #

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

Unquote Text Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Integer Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Bool Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Char Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Double Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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 #

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

prettyErrorParts :: [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

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.