Safe Haskell | None |
---|
- checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
- checkAlias :: Type -> Relevance -> Delayed -> DefInfo -> QName -> Expr -> TCM ()
- checkFunDef' :: Type -> Relevance -> Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
- trailingImplicits :: Type -> [Clause] -> TCM [Clause]
- dropNonHidden :: Nat -> [Dom (String, Type)] -> [Dom (String, Type)]
- splitTrailingImplicits :: Clause -> TCM (Patterns, Patterns)
- patchUpTrailingImplicits :: Patterns -> (Patterns, Patterns) -> Clause -> Clause
- insertPatterns :: [Pattern] -> RHS -> RHS
- data WithFunctionProblem
- checkClause :: Type -> Clause -> TCM Clause
- checkWithFunction :: WithFunctionProblem -> TCM ()
- checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a
- containsAbsurdPattern :: Pattern -> Bool
- actualConstructor :: QName -> TCM QName
Definitions by pattern matching
checkAlias :: Type -> Relevance -> Delayed -> DefInfo -> QName -> Expr -> TCM ()Source
Check a trivial definition of the form f = e
checkFunDef' :: Type -> Relevance -> Delayed -> DefInfo -> QName -> [Clause] -> TCM ()Source
Type check a definition by pattern matching. The third argument specifies whether the clauses are delayed or not.
trailingImplicits :: Type -> [Clause] -> TCM [Clause]Source
Ensure that all clauses have the same number of trailing implicits. Example:
test : Bool → {A B : Set} → Set test true {A} = A test false {B = B} = B
trailingImplicits
patches these clauses to
test : Bool → {A B : Set} → Set test true {A} {_} = A test false {_} {B = B} = B
such that the arity of the clauses of test
is uniform.
dropNonHidden :: Nat -> [Dom (String, Type)] -> [Dom (String, Type)]Source
dropNonHidden n tel
drops n
non-hidden domains from tel
,
including all hidden domains that come before the n
th non-hidden one.
splitTrailingImplicits :: Clause -> TCM (Patterns, Patterns)Source
splitTrailingImplicits c
returns the patterns of clause c
as pair (ps, ips)
where ips
are the trailing implicit patterns
and ps
is the rest.
patchUpTrailingImplicits :: Patterns -> (Patterns, Patterns) -> Clause -> ClauseSource
patchUpTrailingImplicits should (ps, is) c
takes a clause c
whose
patterns are split into (ps, is)
where is
are the trailing
implicit patterns and ps
the rest. is
has already been patched
with omitted implicit patterns (which can occur if named implicit patterns
are there originally). should
is an extension of is
.
The returned clause contains an extension of is
by new wildcards
to match should
.
insertPatterns :: [Pattern] -> RHS -> RHSSource
Insert some patterns in the in with-clauses LHS of the given RHS
checkWhere :: Nat -> [Declaration] -> TCM a -> TCM aSource
Type check a where clause. The first argument is the number of variables bound in the left hand side.
containsAbsurdPattern :: Pattern -> BoolSource
Check if a pattern contains an absurd pattern. For instance, suc ()
actualConstructor :: QName -> TCM QNameSource