idris-0.10: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Utils

Synopsis

Documentation

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

checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> [(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.

pbty :: TT n -> TT n -> TT n Source

getPBtys :: TT t -> [(t, TT t)] Source

psolve :: TT t -> StateT (ElabState aux) TC () Source

getFixedInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name] Source

getFlexInType :: Foldable t => IState -> [Name] -> t Name -> TT Name -> [Name] Source

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, Foldable t1) => [TT t] -> t1 t -> [Int] -> [t] Source