Idris.Elab.Utils

Documentation

recheckC :: FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)

recheckC_borrowing :: Bool -> Bool -> [Name] -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)

checkDeprecated :: FC -> Name -> Idris ()

iderr :: Name -> Err -> Err

checkDef :: FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

Get the list of (index, name) of inaccessible arguments from an elaborated type

inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

Get the list of (index, name) of inaccessible arguments from the type.

elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

checkInferred :: FC -> PTerm -> PTerm -> Idris ()

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

Return whether inferred term is different from given term (as above, but return a Bool)

checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()

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.

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 :: Foldable t => IState -> [Name] -> t Name -> TT Name -> [Name]

getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]

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.

getTCinj :: IState -> TT Name -> [Name]

getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]

paramNames :: (Eq t, Foldable t1) => [TT t] -> t1 t -> [Int] -> [t]

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

Arguments

:: Name

the name of the family that we are finding parameters for

-> [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, which appear exactly once in the return type of a constructor First, find all applications of the constructor, then check over them for repeated arguments

setDetaggable :: Name -> Idris ()

Mark a name as detaggable in the global state (should be called for type and constructor names of single-constructor datatypes)