Safe Haskell | None |
---|---|

Language | Haskell98 |

- data ProjectionView
- unProjView :: ProjectionView -> Term
- projView :: HasConstInfo m => Term -> m ProjectionView
- reduceProjectionLike :: Term -> TCM Term
- elimView :: Bool -> Term -> TCM Term
- eligibleForProjectionLike :: QName -> TCM Bool
- makeProjection :: QName -> TCM ()

# Documentation

data ProjectionView Source #

View for a `Def f (Apply a : es)`

where `isProjection f`

.
Used for projection-like `f`

s.

ProjectionView | A projection or projection-like function, applied to its principal argument |

- projViewProj :: QName
- projViewSelf :: Arg Term
- projViewSpine :: Elims
| |

LoneProjectionLike QName ArgInfo | Just a lone projection-like function, missing its principal argument (from which we could infer the parameters). |

NoProjection Term | Not a projection or projection-like thing. |

unProjView :: ProjectionView -> Term Source #

Semantics of `ProjectionView`

.

projView :: HasConstInfo m => Term -> m ProjectionView Source #

Top-level `ProjectionView`

(no reduction).

reduceProjectionLike :: Term -> TCM Term Source #

Reduce away top-level projection like functions. (Also reduces projections, but they should not be there, since Internal is in lambda- and projection-beta-normal form.)

elimView :: Bool -> Term -> TCM Term Source #

Turn prefix projection-like function application into postfix ones.
This does just one layer, such that the top spine contains
the projection-like functions as projections.
Used in `compareElims`

in `TypeChecking.Conversion`

and in Agda.TypeChecking.CheckInternal.

If the `Bool`

is `True`

, a lone projection like function will be
turned into a lambda-abstraction, expecting the principal argument.
If the `Bool`

is `False`

, it will be returned unaltered.

No precondition. Preserves constructorForm, since it really does only something on (applications of) projection-like functions.

eligibleForProjectionLike :: QName -> TCM Bool Source #

Which `Def`

types are eligible for the principle argument
of a projection-like function?

makeProjection :: QName -> TCM () Source #

Turn a definition into a projection if it looks like a projection.