Idris.Reflection

Documentation

data RErasure

Constructors

RErased

RNotErased

Instances

Show RErasure

Methods

showsPrec :: Int -> RErasure -> ShowS

show :: RErasure -> String

showList :: [RErasure] -> ShowS

data RPlicity

Constructors

RExplicit

RImplicit

RConstraint

Instances

Show RPlicity

Methods

showsPrec :: Int -> RPlicity -> ShowS

show :: RPlicity -> String

showList :: [RPlicity] -> ShowS

data RFunArg

Constructors

RFunArg

Fields

• argName :: Name
• argTy :: Raw
• argPlicity :: RPlicity
• erasure :: RErasure

Instances

Show RFunArg

Methods

showsPrec :: Int -> RFunArg -> ShowS

show :: RFunArg -> String

showList :: [RFunArg] -> ShowS

data RTyDecl

Constructors

RDeclare Name [RFunArg] Raw

Instances

Show RTyDecl

Methods

showsPrec :: Int -> RTyDecl -> ShowS

show :: RTyDecl -> String

showList :: [RTyDecl] -> ShowS

data RTyConArg

Constructors

RParameter RFunArg

RIndex RFunArg

Instances

Show RTyConArg

Methods

showsPrec :: Int -> RTyConArg -> ShowS

show :: RTyConArg -> String

showList :: [RTyConArg] -> ShowS

data RCtorArg

Constructors

RCtorParameter RFunArg

RCtorField RFunArg

Instances

Show RCtorArg

Methods

showsPrec :: Int -> RCtorArg -> ShowS

show :: RCtorArg -> String

showList :: [RCtorArg] -> ShowS

data RDatatype

Constructors

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

Instances

Show RDatatype

Methods

showsPrec :: Int -> RDatatype -> ShowS

show :: RDatatype -> String

showList :: [RDatatype] -> ShowS

data RConstructorDefn

Constructors

RConstructor Name [RFunArg] Raw

data RDataDefn

Constructors

RDefineDatatype Name [RConstructorDefn]

rArgOpts :: RErasure -> [ArgOpt]

rFunArgToPArg :: RFunArg -> PArg

data RFunClause a

Constructors

RMkFunClause a a

RMkImpossibleClause a

Instances

Show a => Show (RFunClause a)

Methods

showsPrec :: Int -> RFunClause a -> ShowS

show :: RFunClause a -> String

showList :: [RFunClause a] -> ShowS

data RFunDefn a

Constructors

RDefineFun Name [RFunClause a]

Instances

Show a => Show (RFunDefn a)

Methods

showsPrec :: Int -> RFunDefn a -> ShowS

show :: RFunDefn a -> String

showList :: [RFunDefn a] -> ShowS

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

reifyFC :: Term -> ElabD FC

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

reifyRConstructorDefn :: Term -> ElabD RConstructorDefn

reifyRDataDefn :: Term -> ElabD RDataDefn

envTupleType :: Raw

reflectList :: Raw -> [Raw] -> 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])

buildFunDefns :: IState -> Name -> [RFunDefn Term]

Build the reflected function definition(s) that correspond(s) to a provided unqualifed name

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

reflectFunClause :: RFunClause Term -> Raw

reflectFunDefn :: RFunDefn Term -> Raw