| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Idris.Elab.Utils
- recheckC :: FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)
- recheckC_borrowing :: Bool -> [Name] -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)
- iderr :: Name -> Err -> Err
- checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] -> Idris [(Name, (Int, Maybe Name, Type))]
- checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] -> Idris [(Name, (Int, Maybe Name, Type))]
- inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]
- inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
- elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()
- checkInferred :: FC -> PTerm -> PTerm -> Idris ()
- inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
- checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
- decorateid :: (Name -> Name) -> PDecl' PTerm -> PDecl' PTerm
- pbinds :: IState -> Term -> ElabD ()
- pbty :: TT n -> TT n -> TT n
- getPBtys :: TT t -> [(t, TT t)]
- psolve :: TT t -> StateT (ElabState aux) TC ()
- pvars :: IState -> TT Name -> [(Name, PTerm)]
- getFixedInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name]
- getFlexInType :: IState -> [Name] -> [Name] -> TT Name -> [Name]
- getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
- paramNames :: Eq t => [TT t] -> [t] -> [Int] -> [t]
- getUniqueUsed :: Context -> Term -> [Name]
- getStaticNames :: IState -> Term -> [Name]
- getStatics :: [Name] -> Term -> [Bool]
- mkStatic :: [Name] -> PDecl -> PDecl
- mkStaticTy :: [Name] -> PTerm -> PTerm
Documentation
recheckC :: FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type) Source
recheckC_borrowing :: Bool -> [Name] -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type) Source
checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] -> Idris [(Name, (Int, Maybe Name, Type))] Source
checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] -> Idris [(Name, (Int, Maybe Name, Type))] Source
inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)] Source
Get the list of (index, name) of inaccessible arguments from an elaborated type
inaccessibleArgs :: Int -> PTerm -> [(Int, Name)] Source
Get the list of (index, name) of inaccessible arguments from the type.
checkInferred :: FC -> PTerm -> PTerm -> Idris () Source
Check that the result of type checking matches what the programmer wrote (i.e. - if we inferred any arguments that the user provided, make sure they are the same!)
inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool Source
Return whether inferred term is different from given term (as above, but return a Bool)
checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris () Source
Check a PTerm against documentation and ensure that every documented argument actually exists. This must be run _after_ implicits have been found, or it will give spurious errors.
getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name] Source
Treat a name as a parameter if it appears in parameter positions in types, and never in a non-parameter position in a (non-param) argument type.
paramNames :: Eq t => [TT t] -> [t] -> [Int] -> [t] Source
getUniqueUsed :: Context -> Term -> [Name] Source
getStaticNames :: IState -> Term -> [Name] Source
getStatics :: [Name] -> Term -> [Bool] Source
mkStaticTy :: [Name] -> PTerm -> PTerm Source