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

Safe HaskellNone
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
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
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 Integer Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Integer Source #

Unquote Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Word64 Source #

Unquote Str Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Str Source #

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId Source #

Unquote ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ArgInfo Source #

Unquote Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Relevance Source #

Unquote Modality Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Modality Source #

Unquote Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Hiding Source #

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM QName 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 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 Elim Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Elim Source #

Unquote ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM ErrorPart Source #

Unquote a => Unquote [a] Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM [a] 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 #

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 String Source #

data ErrorPart Source #

Constructors

StrPart String 
TermPart Expr 
NamePart QName 
Instances
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 #

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 #