Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Unquote

Contents

- Trusted executables

Synopsis

- agdaTermType :: TCM Type
- agdaTypeType :: TCM Type
- qNameType :: TCM Type
- data Dirty
  - = Dirty
  - | Clean
- 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
  - unquote :: Term -> UnquoteM a
- unquoteN :: (HasCallStack, 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
  - = StrPart String
  - | TermPart Expr
  - | PattPart Pattern
  - | NamePart QName
- 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

# 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 Source # (/=) :: Dirty -> Dirty -> Bool 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 #

isCon :: ConHead -> TCM (Maybe Term) -> UnquoteM Bool Source #

isDef :: QName -> TCM (Maybe 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 Blocker Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Blocker 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 :: Term -> 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 :: (HasCallStack, Unquote a) => Arg Term -> UnquoteM a Source #

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

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 #

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

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.