idris-0.9.20: Functional Programming Language with Dependent Types

Safe Haskell	None
Language	Haskell98

Idris.Reflection

Description

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

Synopsis

Documentation

data RErasure Source

Constructors

RErased
RNotErased

Instances

Show RErasure Source

data RPlicity Source

Constructors

RExplicit
RImplicit
RConstraint

Instances

Show RPlicity Source

data RFunArg Source

Constructors

RFunArg
Fields argName :: Name argTy :: Raw argPlicity :: RPlicity erasure :: RErasure

Instances

Show RFunArg Source

data RTyDecl Source

Constructors

RDeclare Name [RFunArg] Raw

Instances

Show RTyDecl Source

data RTyConArg Source

Constructors

RParameter RFunArg
RIndex RFunArg

Instances

Show RTyConArg Source

data RCtorArg Source

Constructors

RCtorParameter RFunArg
RCtorField RFunArg

Instances

Show RCtorArg Source

data RDatatype Source

Constructors

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

Instances

Show RDatatype Source

rArgOpts :: RErasure -> [ArgOpt] Source

rFunArgToPArg :: RFunArg -> PArg Source

data RFunClause Source

Constructors

RMkFunClause Raw Raw
RMkImpossibleClause Raw

Instances

Show RFunClause Source

data RFunDefn Source

Constructors

RDefineFun Name [RFunClause]

Instances

Show RFunDefn Source

reflm :: String -> Name Source

Prefix a name with the Language.Reflection namespace

tacN :: String -> Name Source

Prefix a name with the Language.Reflection.Elab namespace

reify :: IState -> Term -> ElabD PTactic Source

Reify tactics from their reflected representation

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

reifyBool :: Term -> ElabD Bool Source

reifyInt :: Term -> ElabD Int Source

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

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

reifyReportParts :: Term -> ElabD [ErrorReportPart] Source

reifyTT :: Term -> ElabD Term Source

Reify terms from their reflected representation

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

reifyUniverse :: Term -> ElabD Universe Source

reifyRaw :: Term -> ElabD Raw Source

Reify raw terms from their reflected representation

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

reifyTTName :: Term -> ElabD Name Source

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

reifyTTNamespace :: Term -> ElabD [String] Source

reifyTTNameType :: Term -> ElabD NameType Source

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

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

reifyTTConst :: Term -> ElabD Const Source

reifyTTConstApp :: Name -> Term -> ElabD Const Source

reifyArithTy :: Term -> ElabD ArithTy Source

reifyNativeTy :: Term -> ElabD NativeTy Source

reifyIntTy :: Term -> ElabD IntTy Source

reifyTTUExp :: Term -> ElabD UExp Source

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

Create a reflected call to a named function/constructor

reflect :: Term -> Raw Source

Lift a term into its Language.Reflection.TT representation

reflectRaw :: Raw -> Raw Source

Lift a term into its Language.Reflection.Raw representation

claimTy :: Name -> Raw -> ElabD Name Source

intToReflectedNat :: Int -> Raw Source

reflectFixity :: Fixity -> Raw Source

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

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 () Source

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

reflectUniverse :: Universe -> Raw Source

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

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

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

reflectNameType :: NameType -> Raw Source

reflectName :: Name -> Raw Source

reflectSpecialName :: SpecialName -> Raw Source

reflectNameQuotePattern :: Name -> ElabD () Source

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 Source

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

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

reflectConstant :: Const -> Raw Source

reflectUExp :: UExp -> Raw Source

reflectEnv :: Env -> Raw Source

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

reifyEnv :: Term -> ElabD Env Source

rawBool :: Bool -> Raw Source

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

rawNil :: Raw -> Raw Source

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

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

rawPairTy :: Raw -> Raw -> Raw Source

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

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

Idris tuples nest to the right

rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw Source

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

reflectErr :: Err -> Raw Source

reflectFC :: FC -> Raw Source

Reflect a file context

reifyFC :: Term -> ElabD FC Source

fromTTMaybe :: Term -> Maybe Term Source

reflErrName :: String -> Name Source

reifyReportPart :: Term -> Either Err ErrorReportPart Source

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 Source

reifyPlicity :: Term -> ElabD RPlicity Source

reifyRFunArg :: Term -> ElabD RFunArg Source

reifyTyDecl :: Term -> ElabD RTyDecl Source

reifyFunDefn :: Term -> ElabD RFunDefn Source

envTupleType :: Raw Source

reflectList :: Raw -> [Raw] -> Raw Source

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

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]) Source

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

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

reflectErasure :: RErasure -> Raw Source

reflectPlicity :: RPlicity -> Raw Source

reflectArg :: RFunArg -> Raw Source

reflectCtorArg :: RCtorArg -> Raw Source

reflectDatatype :: RDatatype -> Raw Source