| Copyright | License : BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell98 |
Idris.Reflection
Description
- data RErasure
- data RPlicity
- data RFunArg = RFunArg {}
- data RTyDecl = RDeclare Name [RFunArg] Raw
- data RTyConArg
- data RCtorArg
- data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)]
- data RConstructorDefn = RConstructor Name [RFunArg] Raw
- data RDataDefn = RDefineDatatype Name [RConstructorDefn]
- rArgOpts :: RErasure -> [ArgOpt]
- rFunArgToPArg :: RFunArg -> PArg
- data RFunClause a
- = RMkFunClause a a
- | RMkImpossibleClause a
- data RFunDefn a = RDefineFun Name [RFunClause a]
- reflm :: String -> Name
- tacN :: String -> Name
- reify :: IState -> Term -> ElabD PTactic
- 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
- reifyTTApp :: Name -> [Term] -> ElabD Term
- reifyUniverse :: Term -> ElabD Universe
- reifyRaw :: Term -> ElabD Raw
- 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
- reflect :: Term -> Raw
- reflectRaw :: Raw -> Raw
- claimTy :: Name -> Raw -> ElabD Name
- intToReflectedNat :: Int -> Raw
- reflectFixity :: Fixity -> Raw
- reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
- reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
- reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
- reflectUniverse :: Universe -> Raw
- reflectTTQuote :: [Name] -> Term -> Raw
- reflectRawQuote :: [Name] -> Raw -> Raw
- reflectNameType :: NameType -> Raw
- reflectName :: Name -> Raw
- reflectSpecialName :: SpecialName -> Raw
- reflectNameQuotePattern :: Name -> ElabD ()
- 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
- reifyEnv :: Term -> ElabD Env
- rawBool :: Bool -> Raw
- 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
- rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
- reflectCtxt :: [(Name, Type)] -> Raw
- reflectErr :: Err -> Raw
- reflectFC :: FC -> Raw
- reifyFC :: Term -> ElabD FC
- fromTTMaybe :: Term -> Maybe Term
- reflErrName :: String -> Name
- reifyReportPart :: Term -> Either Err ErrorReportPart
- 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)
- unApplyRaw :: Raw -> (Raw, [Raw])
- buildFunDefns :: IState -> Name -> [RFunDefn Term]
- buildDatatypes :: IState -> Name -> [RDatatype]
- reflectErasure :: RErasure -> Raw
- reflectPlicity :: RPlicity -> Raw
- reflectArg :: RFunArg -> Raw
- reflectCtorArg :: RCtorArg -> Raw
- reflectDatatype :: RDatatype -> Raw
- reflectFunClause :: RFunClause Term -> Raw
- reflectFunDefn :: RFunDefn Term -> Raw
Documentation
Constructors
| RParameter RFunArg | |
| RIndex RFunArg |
Constructors
| RCtorParameter RFunArg | |
| RCtorField RFunArg |
data RConstructorDefn Source #
Constructors
| RConstructor Name [RFunArg] Raw |
Constructors
| RDefineDatatype Name [RConstructorDefn] |
rFunArgToPArg :: RFunArg -> PArg Source #
data RFunClause a Source #
Constructors
| RMkFunClause a a | |
| RMkImpossibleClause a |
Instances
| Show a => Show (RFunClause a) Source # | |
Constructors
| RDefineFun Name [RFunClause a] |
reifyReportParts :: Term -> ElabD [ErrorReportPart] Source #
reflectRaw :: Raw -> Raw Source #
Lift a term into its Language.Reflection.Raw representation
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.
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
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 _.
reflectConstant :: Const -> Raw Source #
reflectUExp :: UExp -> Raw Source #
reflectEnv :: Env -> Raw Source #
Reflect the environment of a proof into a List (TTName, Binder TT)
reflectErr :: Err -> Raw 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.
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.
buildFunDefns :: IState -> Name -> [RFunDefn Term] Source #
Build the reflected function definition(s) that correspond(s) to a provided unqualifed name
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 #
reflectFunClause :: RFunClause Term -> Raw Source #