Idris.Reflection

Documentation

data RConstructorDefn

Constructors

RConstructor Name [RFunArg] Raw

data RDataDefn

Constructors

RDefineDatatype Name [RConstructorDefn]

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

data RTyDecl

Constructors

RDeclare Name [RFunArg] Raw

Instances

Show RTyDecl

Methods

showsPrec :: Int -> RTyDecl -> ShowS

show :: RTyDecl -> String

showList :: [RTyDecl] -> ShowS

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

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

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

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

envTupleType :: Raw

fromTTMaybe :: Term -> Maybe Term

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.

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

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

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

rawPairTy :: Raw -> Raw -> Raw

reflect :: Term -> Raw

Lift a term into its Language.Reflection.TT representation

reflectArg :: RFunArg -> Raw

reflectDatatype :: RDatatype -> Raw

reflectEnv :: Env -> Raw

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

reflectErr :: Err -> Raw

reflectFC :: FC -> Raw

Reflect a file context

reflectFixity :: Fixity -> Raw

reflectFunDefn :: RFunDefn Term -> Raw

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

reflectName :: Name -> Raw

reflectNameType :: NameType -> Raw

reflectRaw :: Raw -> Raw

Lift a term into its Language.Reflection.Raw representation

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

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

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

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

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.

reflm :: String -> Name

Prefix a name with the Language.Reflection namespace

reify :: IState -> Term -> ElabD PTactic

Reify tactics from their reflected representation

reifyBool :: Term -> ElabD Bool

reifyEnv :: Term -> ElabD Env

reifyFunDefn :: Term -> ElabD (RFunDefn Raw)

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

reifyRDataDefn :: Term -> ElabD RDataDefn

reifyRaw :: Term -> ElabD Raw

Reify raw terms from their reflected representation

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.

reifyReportParts :: Term -> ElabD [ErrorReportPart]

reifyTT :: Term -> ElabD Term

Reify terms from their reflected representation

reifyTTName :: Term -> ElabD Name

reifyTyDecl :: Term -> ElabD RTyDecl

rFunArgToPArg :: RFunArg -> PArg

tacN :: String -> Name

Prefix a name with the Language.Reflection.Elab namespace