Safe Haskell | None |
---|---|
Language | Haskell98 |
- checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
- isAlias :: [Clause] -> Type -> Maybe (Expr, MetaId)
- checkAlias :: Type -> ArgInfo -> Delayed -> DefInfo -> QName -> Expr -> TCM ()
- checkFunDef' :: Type -> ArgInfo -> Delayed -> Maybe (Int, Int) -> Maybe QName -> DefInfo -> QName -> [Clause] -> TCM ()
- useTerPragma :: Definition -> TCM Definition
- insertPatterns :: [Pattern] -> RHS -> RHS
- data WithFunctionProblem
- = NoWithFunction
- | WithFunction {
- wfParentName :: QName
- wfName :: QName
- wfParentTel :: Telescope
- wfBeforeTel :: Telescope
- wfAfterTel :: Telescope
- wfExprs :: [Term]
- wfExprTypes :: [Type]
- wfRHSType :: Type
- wfParentPats :: [NamedArg Pattern]
- wfPermSplit :: Permutation
- wfPermParent :: Permutation
- wfPermFinal :: Permutation
- wfClauses :: [Clause]
- checkClause :: Type -> SpineClause -> TCM Clause
- checkWithFunction :: WithFunctionProblem -> TCM ()
- checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a
- containsAbsurdPattern :: Pattern -> Bool
Definitions by pattern matching
isAlias :: [Clause] -> Type -> Maybe (Expr, MetaId) Source
A single clause without arguments and without type signature is an alias.
checkAlias :: Type -> ArgInfo -> Delayed -> DefInfo -> QName -> Expr -> TCM () Source
Check a trivial definition of the form f = e
:: Type | the type we expect the function to have |
-> ArgInfo | is it irrelevant (for instance) |
-> Delayed | are the clauses delayed (not unfolded willy-nilly) |
-> Maybe (Int, Int) | does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args) |
-> Maybe QName | is it a with function (if so, what's the name of the parent function) |
-> DefInfo | range info |
-> QName | the name of the function |
-> [Clause] | the clauses to check |
-> TCM () |
Type check a definition by pattern matching.
useTerPragma :: Definition -> TCM Definition Source
Set funTerminates
according to termination info in TCEnv
,
which comes from a possible termination pragma.
insertPatterns :: [Pattern] -> RHS -> RHS Source
Insert some patterns in the in with-clauses LHS of the given RHS
data WithFunctionProblem Source
Parameters for creating a with
-function.
NoWithFunction | |
WithFunction | |
|
checkClause :: Type -> SpineClause -> TCM Clause Source
Type check a function clause.
checkWithFunction :: WithFunctionProblem -> TCM () Source
checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a Source
Type check a where clause. The first argument is the number of variables bound in the left hand side.
containsAbsurdPattern :: Pattern -> Bool Source
Check if a pattern contains an absurd pattern. For instance, suc ()