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.

translateCompiledClauses :: forall m. (HasConstInfo m, MonadChange m) => CompiledClauses -> m CompiledClauses

translateSplitTree :: SplitTree -> TCM SplitTree

Split tree annotated for record pattern translation. type RecordSplitTree = SplitTree' RecordSplitNode type RecordSplitTrees = SplitTrees' RecordSplitNode

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

recordPatternToProjections :: DeBruijnPattern -> 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.

recordRHSToCopatterns :: forall m. (MonadChange m, PureTCM m) => Clause -> m [Clause]