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

Safe Haskell | None

Agda.TypeChecking.RecordPatterns

Description

Code which replaces pattern matching on record constructors with uses of projection functions.

Synopsis

- translateRecordPatterns :: Clause -> TCM Clause
- translateCompiledClauses :: CompiledClauses -> TCM CompiledClauses
- translateSplitTree :: SplitTree -> TCM SplitTree
- recordPatternToProjections :: Pattern -> TCM [Term -> Term]

# Documentation

translateRecordPatterns :: Clause -> TCM Clause

Replaces pattern matching on record constructors with uses of projection functions. Does not remove record constructor patterns which have sub-patterns containing non-record constructor or literal patterns.

If the input clause contains dot patterns inside record patterns, then the translation may yield clauses which are not type-correct. However, we believe that it is safe to use the output as input to `compileClauses`. Perhaps it would be better to perform record pattern translation on the compiled clauses instead, but the code below has already been implemented and seems to work.

translateCompiledClauses :: CompiledClauses -> TCM CompiledClauses

translateSplitTree :: SplitTree -> TCM SplitTree

Bottom-up procedure to record-pattern-translate split tree.

recordPatternToProjections :: Pattern -> TCM [Term -> Term]

Take a record pattern `p` and yield a list of projections corresponding to the pattern variables, from left to right.

E.g. for `(x , (y , z))` we return `[ fst, fst . snd, snd . snd ]`.

If it is not a record pattern, error `ShouldBeRecordPattern` is raised.