Idris.Reflection

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

Documentation

data RErasure

Constructors

RErased

RNotErased

Instances

Show RErasure

data RPlicity

Constructors

RExplicit

RImplicit

RConstraint

Instances

Show RPlicity

data RFunArg

Constructors

RFunArg

Fields

argName :: Name

argTy :: Raw

argPlicity :: RPlicity

erasure :: RErasure

Instances

Show RFunArg

data RTyDecl

Constructors

RDeclare Name [RFunArg] Raw

Instances

Show RTyDecl

data RTyConArg

Constructors

RParameter RFunArg

RIndex RFunArg

Instances

Show RTyConArg

data RCtorArg

Constructors

RCtorParameter RFunArg

RCtorField RFunArg

Instances

Show RCtorArg

data RDatatype

Constructors

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

Instances

Show RDatatype

rArgOpts :: RErasure -> [ArgOpt]

rFunArgToPArg :: RFunArg -> 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

reifyBool :: Term -> ElabD Bool

reifyInt :: Term -> ElabD Int

reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)

reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]

reifyReportParts :: Term -> ElabD [ErrorReportPart]

reifyTT :: Term -> ElabD Term

Reify terms from their reflected representation

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

reifyUniverse :: Term -> ElabD Universe

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

claimTy :: Name -> Raw -> ElabD Name

intToReflectedNat :: Int -> Raw

reflectFixity :: Fixity -> Raw

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 ()) -> Raw -> [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)

reifyEnv :: Term -> ElabD Env

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

rawTripleTy :: Raw -> Raw -> Raw -> Raw

Idris tuples nest to the right

rawTriple :: (Raw, Raw, 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.

reifyErasure :: Term -> ElabD RErasure

reifyPlicity :: Term -> ElabD RPlicity

reifyRFunArg :: Term -> ElabD RFunArg

reifyTyDecl :: Term -> ElabD RTyDecl

reifyFunDefn :: Term -> ElabD RFunDefn

envTupleType :: Raw

getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)

Apply Idris's implicit info to get a signature. The [PArg] should come from a lookup in idris_implicits on IState.

unApplyRaw :: Raw -> (Raw, [Raw])

buildDatatypes :: IState -> Name -> [RDatatype]

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

reflectErasure :: RErasure -> Raw

reflectPlicity :: RPlicity -> Raw

reflectArg :: RFunArg -> Raw

reflectCtorArg :: RCtorArg -> Raw

reflectDatatype :: RDatatype -> Raw