| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.RecordPatterns
Description
Code which replaces pattern matching on record constructors with uses of projection functions.
Synopsis
- translateRecordPatterns :: Clause -> TCM Clause
- translateCompiledClauses :: forall m. (HasConstInfo m, MonadChange m) => CompiledClauses -> m CompiledClauses
- translateSplitTree :: SplitTree -> TCM SplitTree
- recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
- recordRHSToCopatterns :: forall m. (MonadChange m, PureTCM m) => Clause -> m [Clause]
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.
translateCompiledClauses :: forall m. (HasConstInfo m, MonadChange m) => CompiledClauses -> m CompiledClauses Source #
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.
recordRHSToCopatterns :: forall m. (MonadChange m, PureTCM m) => Clause -> m [Clause] Source #