Idris.Elab.Utils

Documentation

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)]

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 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]

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 :: (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

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 ()

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

displayWarnings :: EState -> Idris ()

propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

orderPats :: Term -> Term

Gather up all the outer PVars and Holes in an expression and reintroduce them in a canonical order

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