| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Unquote
Contents
Synopsis
- agdaTermType :: TCM Type
- agdaTypeType :: TCM Type
- qNameType :: TCM Type
- data Dirty
- 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 (Maybe Term) -> UnquoteM Bool
- isDef :: QName -> TCM (Maybe Term) -> UnquoteM Bool
- reduceQuotedTerm :: Term -> UnquoteM Term
- class Unquote a where
- 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
- renderErrorParts :: [ErrorPart] -> TCM Doc
- unquoteTCM :: Term -> Term -> UnquoteM Term
- evalTCM :: Term -> UnquoteM Term
- type ExeArg = Text
- type StdIn = Text
- type StdOut = Text
- type StdErr = Text
- requireAllowExec :: TCM ()
- exitCodeToNat :: ExitCode -> Nat
- tcExec :: ExeName -> [ExeArg] -> StdIn -> TCM Term
- raiseExeNotTrusted :: ExeName -> Map ExeName FilePath -> TCM a
- raiseExeNotFound :: ExeName -> FilePath -> TCM a
- raiseExeNotExecutable :: ExeName -> FilePath -> TCM a
Documentation
agdaTermType :: TCM Type Source #
agdaTypeType :: TCM Type Source #
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 #
class Unquote a where Source #
Instances
| Unquote QName Source # | |
| Unquote ArgInfo Source # | |
| Unquote Hiding Source # | |
| Unquote MetaId Source # | |
| Unquote Modality Source # | |
| Unquote Quantity Source # | |
| Unquote Relevance Source # | |
| Unquote Blocker Source # | |
| Unquote Literal Source # | |
| Unquote Clause Source # | |
| Unquote Elim Source # | |
| Unquote Pattern Source # | |
| Unquote Sort Source # | |
| Unquote Term Source # | |
| Unquote ErrorPart Source # | |
| Unquote Word64 Source # | |
| Unquote Text Source # | |
| Unquote Integer Source # | |
| Unquote Bool Source # | |
| Unquote Char Source # | |
| Unquote Double Source # | |
| Unquote a => Unquote (Arg a) Source # | |
| Unquote a => Unquote (Dom a) Source # | |
| Unquote a => Unquote (Abs a) Source # | |
| Unquote a => Unquote [a] Source # | |
| (Unquote a, Unquote b) => Unquote (a, b) Source # | |
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
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.