| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Unquote
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]))
- 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
- 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
- getCurrentPath :: TCM AbsolutePath
- unquoteTCM :: Term -> Term -> UnquoteM Term
- evalTCM :: Term -> UnquoteM Term
Documentation
agdaTermType :: TCM Type #
agdaTypeType :: TCM Type #
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 #
reduceQuotedTerm :: Term -> UnquoteM Term #
Minimal complete definition
Instances
| Unquote Bool # | |
| Unquote Char # | |
| Unquote Double # | |
| Unquote Integer # | |
| Unquote Word64 # | |
| Unquote Str # | |
| Unquote MetaId # | |
| Unquote ArgInfo # | |
| Unquote Relevance # | |
| Unquote Modality # | |
| Unquote Hiding # | |
| Unquote QName # | |
| Unquote Literal # | |
| Unquote Clause # | |
| Unquote Pattern # | |
| Unquote Sort # | |
| Unquote Term # | |
| Unquote Elim # | |
| Unquote ErrorPart # | |
| Unquote a => Unquote [a] # | |
Defined in Agda.TypeChecking.Unquote | |
| Unquote a => Unquote (Dom a) # | |
| Unquote a => Unquote (Arg a) # | |
| Unquote a => Unquote (Abs a) # | |
unquoteString :: Term -> UnquoteM String #