Safe Haskell | None |
---|---|
Language | Haskell98 |
- 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' :: (Num a, Eq 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' :: (Num a, Eq a) => [TT Name] -> Bool -> a -> Term -> Name -> IState -> StateT (ElabState [PDecl]) TC () Source
reflm :: String -> Name Source
Prefix a name with the Language.Reflection namespace
reifyTTName :: Term -> ElabD Name Source
reifyTTNamespace :: Term -> ElabD [String] Source
reifyTTNameType :: Term -> ElabD NameType Source
reifyTTConst :: Term -> ElabD Const Source
reifyArithTy :: Term -> ElabD ArithTy Source
reifyNativeTy :: Term -> ElabD NativeTy Source
reifyIntTy :: Term -> ElabD IntTy Source
reifyTTUExp :: Term -> ElabD UExp Source
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 -> Raw Source
Create a reflected term, but leave refs to the provided name intact
reflectNameType :: NameType -> Raw Source
reflectName :: Name -> 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 _.
reflectBinder :: Binder Term -> Raw Source
reflectConstant :: Const -> Raw Source
reflectUExp :: UExp -> Raw Source
reflectEnv :: Env -> Raw Source
Reflect the environment of a proof into a List (TTName, Binder TT)
reflectCtxt :: [(Name, Type)] -> Raw Source
reflectErr :: Err -> Raw Source
withErrorReflection :: Idris a -> Idris a Source
fromTTMaybe :: Term -> Maybe Term 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.