Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.RecordPatterns

Description

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

Synopsis

Documentation

translateRecordPatterns :: Clause -> TCM Clause Source #

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.

translateSplitTree :: SplitTree -> TCM SplitTree Source #

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] 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.