idris-0.12.3: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell98

Idris.Elab.Utils

Description

 

Synopsis

Documentation

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.

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

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

orderPats :: Term -> Term Source #

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