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

Agda.TypeChecking.Unquote

Synopsis

Documentation

agdaTermType :: TCM Type Source #

agdaTypeType :: TCM Type Source #

qNameType :: TCM Type Source #

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 UnquoteState = (Dirty, TCState) Source #

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

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

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

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

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

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

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

inOriginalContext :: UnquoteM a -> UnquoteM a Source #

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

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

reduceQuotedTerm :: Term -> UnquoteM Term 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

Methods

unquote :: Term -> UnquoteM QName Source #

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ArgInfo Source #

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Hiding Source #

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId Source #

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Modality Source #

Unquote Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Quantity Source #

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Relevance Source #

Unquote Literal Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Literal Source #

Unquote Clause Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Clause Source #

Unquote Elim Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Elim Source #

Unquote Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Pattern Source #

Unquote Sort Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Sort Source #

Unquote Term Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term0 -> UnquoteM Term Source #

Unquote ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ErrorPart Source #

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 #

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

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

ensureDef :: QName -> UnquoteM QName Source #

ensureCon :: QName -> UnquoteM QName Source #

pickName :: Type -> String Source #

unquoteString :: Term -> UnquoteM String Source #

unquoteNString :: Arg Term -> UnquoteM Text Source #

data ErrorPart Source #

Constructors

StrPart String 
TermPart Expr 
PattPart Pattern 
NamePart QName 

Instances

Instances details
PrettyTCM ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

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

Unquote ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ErrorPart Source #

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

evalTCM :: Term -> UnquoteM Term Source #

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 #

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