Agda.TypeChecking.RecordPatterns

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

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.