Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Unquote
- agdaTermType :: TCM Type
- agdaTypeType :: TCM Type
- qNameType :: TCM Type
- data 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
- 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] (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])) #
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 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) # | |
unquoteString :: Term -> UnquoteM String #