Safe Haskell | None |
---|
Code which replaces pattern matching on record constructors with uses of projection functions.
Documentation
translateRecordPatterns :: Clause -> TCM ClauseSource
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.
translateSplitTree :: SplitTree -> TCM SplitTreeSource
Bottom-up procedure to record-pattern-translate split tree.
recordPatternToProjections :: Pattern -> TCM [Term -> Term]Source
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.