Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.RecordPatterns

Description

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

Synopsis

- translateCompiledClauses :: (HasConstInfo m, MonadChange m) => QName -> CompiledClauses -> m CompiledClauses
- translateSplitTree :: SplitTree -> TCM SplitTree
- recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
- recordRHSToCopatterns :: (MonadChange m, PureTCM m) => Clause -> m [Clause]

# Documentation

translateCompiledClauses :: (HasConstInfo m, MonadChange m) => QName -> CompiledClauses -> m CompiledClauses Source #

translateSplitTree :: SplitTree -> TCM SplitTree Source #

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 :: (MonadChange m, PureTCM m) => Clause -> m [Clause] Source #