| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Elab.Utils
Description
Synopsis
- recheckC :: String -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)
- recheckC_borrowing :: Bool -> Bool -> [Name] -> String -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)
- checkDeprecated :: FC -> Name -> Idris ()
- checkFragile :: FC -> Name -> Idris ()
- iderr :: Name -> Err -> Err
- checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
- checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
- 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 a -> [(a, TT a)]
- psolve :: TT n -> StateT (ElabState aux) TC ()
- pvars :: IState -> TT Name -> [(Name, PTerm)]
- getFixedInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name]
- getFlexInType :: Foldable t => IState -> [Name] -> t Name -> TT Name -> [Name]
- getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
- getTCinj :: IState -> TT Name -> [Name]
- getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
- paramNames :: (Foldable t, Eq a) => [TT a] -> t a -> [Int] -> [a]
- getLinearUsed :: Context -> Term -> [Name]
- getUniqueUsed :: Context -> Term -> [Name]
- getStaticNames :: IState -> Term -> [Name]
- getStatics :: [Name] -> Term -> [Bool]
- mkStatic :: [Name] -> PDecl -> PDecl
- mkStaticTy :: [Name] -> PTerm -> PTerm
- checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()
- findParams :: Name -> Type -> [Type] -> [Int]
- setDetaggable :: Name -> Idris ()
- displayWarnings :: EState -> Idris ()
- propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
- orderPats :: Term -> Term
- liftPats :: Term -> Term
- isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool
- hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool
- findLinear :: RigCount -> IState -> [Name] -> Term -> [(Name, RigCount)]
- setLinear :: [(Name, RigCount)] -> Term -> Term
- linearArg :: Type -> Bool
- pruneByType :: Bool -> Env -> Term -> Type -> IState -> [PTerm] -> [PTerm]
- isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
Documentation
recheckC :: String -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type) Source #
recheckC_borrowing :: Bool -> Bool -> [Name] -> String -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type) Source #
checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))] Source #
checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))] 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.
checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris () Source #
Arguments
| :: Name | the name of the family that we are finding parameters for |
| -> Type | the type of the type constructor (normalised already) |
| -> [Type] | the declared constructor types |
| -> [Int] |
Find the type constructor arguments that are parameters, given a list of constructor types.
Parameters are names which are unchanged across the structure. They appear at least once in every constructor type, always appear in the same argument position(s), and nothing else ever appears in those argument positions.
setDetaggable :: Name -> Idris () Source #
Mark a name as detaggable in the global state (should be called for type and constructor names of single-constructor datatypes)
displayWarnings :: EState -> Idris () Source #