Agda.TypeChecking.Unquote

Documentation

agdaTermType :: TCM Type

agdaTypeType :: TCM Type

qNameType :: TCM Type

data Dirty

Constructors

Dirty

Clean

Instances

Eq Dirty

type UnquoteState = (Dirty, TCState)

type UnquoteM = ReaderT Context (StateT UnquoteState (WriterT [QName] (ExceptionT 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]))

liftU :: TCM a -> UnquoteM a

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 Term -> UnquoteM Bool

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

reduceQuotedTerm :: Term -> UnquoteM Term

class Unquote a where

Methods

unquote :: Term -> UnquoteM a

Instances

Unquote Char

Unquote Double

Unquote Integer

Unquote Str

Unquote MetaId

Unquote ArgInfo

Unquote Relevance

Unquote Hiding

Unquote QName

Unquote Literal

Unquote Clause

Unquote Pattern

Unquote Sort

Unquote Term

Unquote Elim

Unquote ErrorPart

Unquote a => Unquote [a]

Unquote a => Unquote (Dom a)

Unquote a => Unquote (Arg a)

Unquote a => Unquote (Abs a)

unquoteH :: Unquote a => Arg Term -> UnquoteM a

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 String

data ErrorPart

Constructors

StrPart String

TermPart Term

NamePart QName

Instances

PrettyTCM ErrorPart

Unquote ErrorPart

getCurrentPath :: TCM AbsolutePath

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

evalTCM :: Term -> UnquoteM Term