License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Reflection

Description

Synopsis

data RConstructorDefn = RConstructor Name [RFunArg] Raw
data RDataDefn = RDefineDatatype Name [RConstructorDefn]
data RFunArg = RFunArg {
- argName :: Name
- argTy :: Raw
- argPlicity :: RPlicity
- erasure :: RErasure
}
data RFunClause a
- = RMkFunClause a a
- | RMkImpossibleClause a
data RFunDefn a = RDefineFun Name [RFunClause a]
data RTyDecl = RDeclare Name [RFunArg] Raw
buildDatatypes :: IState -> Name -> [RDatatype]
buildFunDefns :: IState -> Name -> [RFunDefn Term]
envTupleType :: Raw
fromTTMaybe :: Term -> Maybe Term
getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
mkList :: Raw -> [Raw] -> Raw
rawList :: Raw -> [Raw] -> Raw
rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPairTy :: Raw -> Raw -> Raw
reflect :: Term -> Raw
reflectArg :: RFunArg -> Raw
reflectDatatype :: RDatatype -> Raw
reflectEnv :: Env -> Raw
reflectErr :: Err -> Raw
reflectFC :: FC -> Raw
reflectFixity :: Fixity -> Raw
reflectFunDefn :: RFunDefn Term -> Raw
reflectList :: Raw -> [Raw] -> Raw
reflectName :: Name -> Raw
reflectNameType :: NameType -> Raw
reflectRaw :: Raw -> Raw
reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectRawQuote :: [Name] -> Raw -> Raw
reflectTTQuote :: [Name] -> Term -> Raw
reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
reflm :: String -> Name
reify :: IState -> Term -> ElabD PTactic
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
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportParts :: Term -> ElabD [ErrorReportPart]
reifyTT :: Term -> ElabD Term
reifyTTName :: Term -> ElabD Name
reifyTyDecl :: Term -> ElabD RTyDecl
rFunArgToPArg :: RFunArg -> PArg
tacN :: String -> Name

Documentation

data RConstructorDefn Source #

Constructors

RConstructor Name [RFunArg] Raw

data RDataDefn Source #

Constructors

RDefineDatatype Name [RConstructorDefn]

data RFunArg Source #

Constructors

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

Instances

Show RFunArg Source #
Instance details Defined in Idris.Reflection Methods showsPrec :: Int -> RFunArg -> ShowS # show :: RFunArg -> String # showList :: [RFunArg] -> ShowS #

data RFunClause a Source #

Constructors

RMkFunClause a a
RMkImpossibleClause a

Instances

Show a => Show (RFunClause a) Source #
Instance details Defined in Idris.Reflection Methods showsPrec :: Int -> RFunClause a -> ShowS # show :: RFunClause a -> String # showList :: [RFunClause a] -> ShowS #

data RFunDefn a Source #

Constructors

RDefineFun Name [RFunClause a]

Instances

Show a => Show (RFunDefn a) Source #
Instance details Defined in Idris.Reflection Methods showsPrec :: Int -> RFunDefn a -> ShowS # show :: RFunDefn a -> String # showList :: [RFunDefn a] -> ShowS #

data RTyDecl Source #

Constructors

RDeclare Name [RFunArg] Raw

Instances

Show RTyDecl Source #
Instance details Defined in Idris.Reflection Methods showsPrec :: Int -> RTyDecl -> ShowS # show :: RTyDecl -> String # showList :: [RTyDecl] -> ShowS #

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

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

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

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

envTupleType :: Raw Source #

fromTTMaybe :: Term -> Maybe Term 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.

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

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

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

rawPairTy :: Raw -> Raw -> Raw Source #

reflect :: Term -> Raw Source #

Lift a term into its Language.Reflection.TT representation

reflectArg :: RFunArg -> Raw Source #

reflectDatatype :: RDatatype -> Raw Source #

reflectEnv :: Env -> Raw Source #

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

reflectErr :: Err -> Raw Source #

reflectFC :: FC -> Raw Source #

Reflect a file context

reflectFixity :: Fixity -> Raw Source #

reflectFunDefn :: RFunDefn Term -> Raw Source #

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

reflectName :: Name -> Raw Source #

reflectNameType :: NameType -> Raw Source #

reflectRaw :: Raw -> Raw Source #

Lift a term into its Language.Reflection.Raw representation

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

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

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

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

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.

reflm :: String -> Name Source #

Prefix a name with the Language.Reflection namespace

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

Reify tactics from their reflected representation

reifyBool :: Term -> ElabD Bool Source #

reifyEnv :: Term -> ElabD Env Source #

reifyFunDefn :: Term -> ElabD (RFunDefn Raw) Source #

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

reifyRDataDefn :: Term -> ElabD RDataDefn Source #

reifyRaw :: Term -> ElabD Raw Source #

Reify raw terms from their reflected representation

reifyReportPart :: Term -> Either Err ErrorReportPart Source #