Safe Haskell | None |
---|
- data ElabMode
- build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
- buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
- elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ()
- pruneAlt :: [PTerm] -> [PTerm]
- pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]
- findInstances :: IState -> Term -> [Name]
- trivial' :: IState -> ElabD ()
- proofSearch' :: IState -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> StateT (ElabState [PDecl]) TC ()
- resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
- resTC' :: (Eq a, Num a) => [TT Name] -> Bool -> a -> Term -> Name -> IState -> StateT (ElabState [PDecl]) TC ()
- collectDeferred :: Maybe Name -> Term -> State [(Name, (Int, Maybe Name, Type))] Term
- case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
- runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
- reflm :: String -> Name
- reify :: IState -> Term -> ElabD PTactic
- reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
- reifyTT :: Term -> ElabD Term
- reifyTTApp :: Name -> [Term] -> ElabD Term
- 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
- claimTT :: Name -> ElabD Name
- reflectQuotePattern :: [Name] -> Term -> ElabD ()
- reflectQuote :: [Name] -> Term -> Raw
- reflectNameType :: NameType -> Raw
- reflectName :: Name -> Raw
- reflectNameQuotePattern :: Name -> ElabD ()
- reflectBinder :: Binder Term -> Raw
- reflectBinderQuote :: [Name] -> Binder Term -> Raw
- mkList :: Raw -> [Raw] -> Raw
- reflectConstant :: Const -> Raw
- reflectUExp :: UExp -> Raw
- reflectEnv :: Env -> Raw
- 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
- reflectCtxt :: [(Name, Type)] -> Raw
- reflectErr :: Err -> Raw
- elaboratingArgErr :: [(Name, Name)] -> Err -> Err
- withErrorReflection :: Idris a -> Idris a
- fromTTMaybe :: Term -> Maybe Term
- reflErrName :: String -> Name
- reifyReportPart :: Term -> Either Err ErrorReportPart
- envTupleType :: Raw
- solveAll :: Elab' aux ()
Documentation
build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])Source
buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])Source
findInstances :: IState -> Term -> [Name]Source
proofSearch' :: IState -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> StateT (ElabState [PDecl]) TC ()Source
resTC' :: (Eq a, Num a) => [TT Name] -> Bool -> a -> Term -> Name -> IState -> StateT (ElabState [PDecl]) TC ()Source
Prefix a name with the Language.Reflection namespace
reifyTTName :: Term -> ElabD NameSource
reifyTTNamespace :: Term -> ElabD [String]Source
reifyTTConst :: Term -> ElabD ConstSource
reifyArithTy :: Term -> ElabD ArithTySource
reifyNativeTy :: Term -> ElabD NativeTySource
reifyIntTy :: Term -> ElabD IntTySource
reifyTTUExp :: Term -> ElabD UExpSource
reflectQuotePattern :: [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.
reflectQuote :: [Name] -> Term -> RawSource
Create a reflected term, but leave refs to the provided name intact
reflectNameType :: NameType -> RawSource
reflectName :: Name -> RawSource
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 _.
reflectBinder :: Binder Term -> RawSource
reflectConstant :: Const -> RawSource
reflectUExp :: UExp -> RawSource
reflectEnv :: Env -> RawSource
Reflect the environment of a proof into a List (TTName, Binder TT)
reflectCtxt :: [(Name, Type)] -> RawSource
reflectErr :: Err -> RawSource
withErrorReflection :: Idris a -> Idris aSource
fromTTMaybe :: Term -> Maybe TermSource
reflErrName :: String -> NameSource
reifyReportPart :: Term -> Either Err ErrorReportPartSource
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.