ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Unquote

9 types
1 class
25 values

PackageAgda-2.8.0.2
Exports35
LanguageHaskell2010
LicenceMIT
SourceUnquote.hs

valueagdaTermType :: TCM Type

valueagdaTypeType :: TCM Type

valueqNameType :: TCM Type

datadata Dirty

Dirty Clean

Instances1Eq

Eq DirtyDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote

typetype UnquoteState = (Dirty, TCState)

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

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

valueunpackUnquoteM

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

valuepackUnquoteM

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

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

valueliftU1

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

valueliftU2

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

valueinOriginalContext :: UnquoteM a -> UnquoteM a

valueisCon :: ConHead -> TCM (Maybe Term) -> UnquoteM Bool

valueisDef :: QName -> TCM (Maybe Term) -> UnquoteM Bool

valuereduceQuotedTerm :: Term -> UnquoteM Term

classclass Unquote a where

Methods

unquote :: Term -> UnquoteM a

Instances26Unquote, …

Unquote QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote BlockerDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote LiteralDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote ClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote PatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote SortDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote ErrorPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote IntegerDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote BoolDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote CharDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote DoubleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote Word64Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote TextDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote a => Unquote (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote a => Unquote (Dom a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote a => Unquote (Abs a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote a => Unquote [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
(Unquote a, Unquote b) => Unquote (a, b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote

valueunquoteN :: (HasCallStack, Unquote a) => Arg Term -> UnquoteM a

Unquote an Arg Term assuming the ArgInfo does not contain information. (This means, it should be visible, relevant, etc., like defaultArg).

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

valueensureDef :: QName -> UnquoteM QName

valueensureCon :: QName -> UnquoteM QName

valuepickName :: Type -> String

valueunquoteString :: Term -> UnquoteM String

valueunquoteNString :: Arg Term -> UnquoteM Text

datadata ErrorPart

Constructors

Instances2PrettyTCM, Unquote

PrettyTCM ErrorPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote ErrorPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote

valuerenderErrorParts :: [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.

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

valueevalTCM :: Term -> UnquoteM Term

Trusted executables

7 declarations

typetype ExeArg = Text

typetype StdIn = Text

typetype StdOut = Text

typetype StdErr = Text

valuerequireAllowExec :: TCM ()

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

valueexitCodeToNat :: ExitCode -> Nat

Convert an ExitCode to an Agda natural number.

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

Call a trusted executable with the given arguments and input.

Returns the exit code, stdout, and stderr.