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 Agda.TypeChecking.CompiledClause.Compile.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.