Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Rules.Def

Contents

- Definitions by pattern matching

Synopsis

- 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
  - = NoWithFunction
  - | WithFunction QName QName Telescope Telescope Telescope [Term] [Type] Type [Arg Pattern] Permutation Permutation [Clause]
- 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

checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()

checkAlias :: Type -> Relevance -> Delayed -> DefInfo -> QName -> Expr -> TCM ()

Check a trivial definition of the form `f = e`

checkFunDef' :: Type -> Relevance -> Delayed -> DefInfo -> QName -> [Clause] -> TCM ()

Type check a definition by pattern matching. The third argument specifies whether the clauses are delayed or not.

trailingImplicits :: Type -> [Clause] -> TCM [Clause]

Ensure that all clauses have the same number of trailing implicits. Example:

      test : Bool → {A B : Set} → Se  test true  {A}     = A
      test false {B = B} = B

`trailingImplicits` patches these clauses to

      test : Bool → {A B : Set} → Se  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)]

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

`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 -> Clause

`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 -> RHS

Insert some patterns in the in with-clauses LHS of the given RHS

data WithFunctionProblem

Constructors

NoWithFunction |
WithFunction QName QName Telescope Telescope Telescope [Term] [Type] Type [Arg Pattern] Permutation Permutation [Clause] |

checkClause :: Type -> Clause -> TCM Clause

Type check a function clause.

checkWithFunction :: WithFunctionProblem -> TCM ()

checkWhere :: Nat -> [Declaration] -> TCM a -> TCM a

Type check a where clause. The first argument is the number of variables bound in the left hand side.

containsAbsurdPattern :: Pattern -> Bool

Check if a pattern contains an absurd pattern. For instance, `suc ()`

actualConstructor :: QName -> TCM QName