| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Reflection
Description
- data RConstructorDefn = RConstructor Name [RFunArg] Raw
- data RDataDefn = RDefineDatatype Name [RConstructorDefn]
- data RFunArg = RFunArg {}
- 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 |
Constructors
| RDefineDatatype Name [RConstructorDefn] |
data RFunClause a Source #
Constructors
| RMkFunClause a a | |
| RMkImpossibleClause a |
Instances
| Show a => Show (RFunClause a) Source # | |
Constructors
| RDefineFun Name [RFunClause a] |
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 #
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.
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 #
reflectFixity :: Fixity -> Raw Source #
reflectName :: Name -> Raw Source #
reflectNameType :: NameType -> Raw Source #
reflectRaw :: Raw -> Raw Source #
Lift a term into its Language.Reflection.Raw representation
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.
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.
reifyReportParts :: Term -> ElabD [ErrorReportPart] Source #
rFunArgToPArg :: RFunArg -> PArg Source #