Idris.Reflection

Code related to Idris's reflection system. This module contains quoters and unquoters along with some supporting datatypes.

Documentation

data RArg

Constructors

RExplicit

Fields

argName :: Name

argTy :: Raw

RImplicit

Fields

argName :: Name

argTy :: Raw

RConstraint

Fields

argName :: Name

argTy :: Raw

Instances

Show RArg

data RTyDecl

Constructors

RDeclare Name [RArg] Raw

Instances

Show RTyDecl

data RTyConArg

Constructors

RParameter

Fields

tcArgName :: Name

tcArgTy :: Raw

RIndex

Fields

tcArgName :: Name

tcArgTy :: Raw

Instances

Show RTyConArg

data RDatatype

Constructors

RDatatype Name [RTyConArg] Raw [(Name, Raw)]

Instances

Show RDatatype

rArgToPArg :: RArg -> PArg

data RFunClause

Constructors

RMkFunClause Raw Raw

RMkImpossibleClause Raw

Instances

Show RFunClause

data RFunDefn

Constructors

RDefineFun Name [RFunClause]

Instances

Show RFunDefn

reflm :: String -> Name

Prefix a name with the Language.Reflection namespace

tacN :: String -> Name

Prefix a name with the Language.Reflection.Elab namespace

reify :: IState -> Term -> ElabD PTactic

Reify tactics from their reflected representation

reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

reifyReportParts :: Term -> ElabD [ErrorReportPart]

reifyTT :: Term -> ElabD Term

Reify terms from their reflected representation

reifyTTApp :: Name -> [Term] -> ElabD Term

reifyRaw :: Term -> ElabD Raw

Reify raw terms from their reflected representation

reifyRawApp :: Name -> [Term] -> ElabD Raw

reifyTTName :: Term -> ElabD Name

reifyTTNameApp :: Name -> [Term] -> ElabD Name

reifyTTNamespace :: Term -> ElabD [String]

reifyTTNameType :: Term -> ElabD NameType

reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

reifyTTConst :: Term -> ElabD Const

reifyTTConstApp :: Name -> Term -> ElabD Const

reifyArithTy :: Term -> ElabD ArithTy

reifyNativeTy :: Term -> ElabD NativeTy

reifyIntTy :: Term -> ElabD IntTy

reifyTTUExp :: Term -> ElabD UExp

reflCall :: String -> [Raw] -> Raw

Create a reflected call to a named function/constructor

reflect :: Term -> Raw

Lift a term into its Language.Reflection.TT representation

reflectRaw :: Raw -> Raw

Lift a term into its Language.Reflection.Raw representation

claimTT :: Name -> ElabD Name

reflectTTQuotePattern :: [Name] -> Term -> ElabD ()

Convert a reflected term to a more suitable form for pattern-matching. In particular, the less-interesting bits are elaborated to _ patterns. This happens to NameTypes, universe levels, names that are bound but not used, and the type annotation field of the P constructor.

reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()

reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()

reflectUniverse :: Universe -> Raw

reflectTTQuote :: [Name] -> Term -> Raw

Create a reflected TT term, but leave refs to the provided name intact

reflectRawQuote :: [Name] -> Raw -> Raw

reflectNameType :: NameType -> Raw

reflectName :: Name -> Raw

reflectSpecialName :: SpecialName -> Raw

reflectNameQuotePattern :: Name -> ElabD ()

Elaborate a name to a pattern. This means that NS and UN will be intact. MNs corresponding to will care about the string but not the number. All others become _.

reflectBinder :: Binder Term -> Raw

reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

mkList :: Raw -> [Raw] -> Raw

reflectConstant :: Const -> Raw

reflectUExp :: UExp -> Raw

reflectEnv :: Env -> Raw

Reflect the environment of a proof into a List (TTName, Binder TT)

rawBool :: Bool -> Raw

Reflect an error into the internal datatype of Idris -- TODO

rawNil :: Raw -> Raw

rawCons :: Raw -> Raw -> Raw -> Raw

rawList :: Raw -> [Raw] -> Raw

rawPairTy :: Raw -> Raw -> Raw

rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

reflectCtxt :: [(Name, Type)] -> Raw

reflectErr :: Err -> Raw

reflectFC :: FC -> Raw

Reflect a file context

fromTTMaybe :: Term -> Maybe Term

reflErrName :: String -> Name

reifyReportPart :: Term -> Either Err ErrorReportPart

Attempt to reify a report part from TT to the internal representation. Not in Idris or ElabD monads because it should be usable from either.

reifyTyDecl :: Term -> ElabD RTyDecl

reifyFunDefn :: Term -> ElabD RFunDefn

envTupleType :: Raw

buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]

Build the reflected datatype definition(s) that correspond(s) to a provided unqualified name

reflectDatatype :: RDatatype -> Raw