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

Language | Haskell2010 |

A constructor argument is forced if it appears as pattern variable in an index of the target.

For instance `x`

is forced in `sing`

and `n`

is forced in `zero`

and `suc`

:

data Sing {a}{A : Set a} : A -> Set where sing : (x : A) -> Sing x data Fin : Nat -> Set where zero : (n : Nat) -> Fin (suc n) suc : (n : Nat) (i : Fin n) -> Fin (suc n)

At runtime, forced constructor arguments may be erased as they can be
recovered from dot patterns. For instance,
```
unsing : {A : Set} (x : A) -> Sing x -> A
unsing .x (sing x) = x
```

can become
```
unsing x sing = x
```

and
```
proj : (n : Nat) (i : Fin n) -> Nat
proj .(suc n) (zero n) = n
proj .(suc n) (suc n i) = n
```

becomes
```
proj (suc n) zero = n
proj (suc n) (suc i) = n
```

Forcing is a concept from pattern matching and thus builds on the concept of equality (I) used there (closed terms, extensional) which is different from the equality (II) used in conversion checking and the constraint solver (open terms, intensional).

Up to issue 1441 (Feb 2015), the forcing analysis here relied on the wrong equality (II), considering type constructors as injective. This is unsound for program extraction, but ok if forcing is only used to decide which arguments to skip during conversion checking.

From now on, forcing uses equality (I) and does not search for forced
variables under type constructors. This may lose some savings during
conversion checking. If this turns out to be a problem, the old
forcing could be brought back, using a new modality `Skip`

to indicate
that this is a relevant argument but still can be skipped during
conversion checking as it is forced by equality (II).

## Synopsis

- computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
- class ForcedVariables a where
- forcedVariables :: a -> [(Modality, Nat)]

- isForced :: IsForced -> Bool
- nextIsForced :: [IsForced] -> (IsForced, [IsForced])
- forcingTranslation :: [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
- forceTranslateTelescope :: Telescope -> [NamedArg DeBruijnPattern] -> TCM Telescope
- rebindForcedPattern :: [NamedArg DeBruijnPattern] -> DeBruijnPattern -> TCM [NamedArg DeBruijnPattern]
- rebinds :: DeBruijnPattern -> DeBruijnPattern -> Bool
- dotForcedPatterns :: [NamedArg DeBruijnPattern] -> TCM ([NamedArg DeBruijnPattern], Maybe [DeBruijnPattern])

# Documentation

computeForcingAnnotations :: QName -> Type -> TCM [IsForced] Source #

Given the type of a constructor (excluding the parameters),
decide which arguments are forced.
Precondition: the type is of the form `Γ → D vs`

and the `vs`

are in normal form.

class ForcedVariables a where Source #

Compute the pattern variables of a term or term-like thing.

Nothing

forcedVariables :: a -> [(Modality, Nat)] Source #

forcedVariables :: (ForcedVariables b, Foldable t, a ~ t b) => a -> [(Modality, Nat)] Source #

## Instances

ForcedVariables Term Source # | Assumes that the term is in normal form. |

Defined in Agda.TypeChecking.Forcing | |

ForcedVariables a => ForcedVariables [a] Source # | |

Defined in Agda.TypeChecking.Forcing forcedVariables :: [a] -> [(Modality, Nat)] Source # | |

ForcedVariables a => ForcedVariables (Arg a) Source # | |

Defined in Agda.TypeChecking.Forcing | |

ForcedVariables a => ForcedVariables (Elim' a) Source # | |

Defined in Agda.TypeChecking.Forcing |

# Forcing translation

forcingTranslation :: [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern] Source #

Move bindings for forced variables to unforced positions.

forceTranslateTelescope :: Telescope -> [NamedArg DeBruijnPattern] -> TCM Telescope Source #

Applies the forcing translation in order to update modalities of forced arguments in the telescope. This is used before checking a right-hand side in order to make sure all uses of forced arguments agree with the relevance of the position where the variable will ultimately be bound. Precondition: the telescope types the bound variables of the patterns.

rebindForcedPattern :: [NamedArg DeBruijnPattern] -> DeBruijnPattern -> TCM [NamedArg DeBruijnPattern] Source #

Rebind a forced pattern in a non-forced position. The forced pattern has
already been dotted by `dotForcedPatterns`

, so the remaining task is to
find a dot pattern in an unforced position that can be turned into a
proper match of the forced pattern.

For instance (with patterns prettified to ease readability):

rebindForcedPattern [.(suc n), cons .n x xs] n = [suc n, cons .n x xs]

rebinds :: DeBruijnPattern -> DeBruijnPattern -> Bool Source #

Check if the first pattern rebinds the second pattern. Almost equality, but allows the first pattern to have a variable where the second pattern has a dot pattern. Used to fix #3544.

dotForcedPatterns :: [NamedArg DeBruijnPattern] -> TCM ([NamedArg DeBruijnPattern], Maybe [DeBruijnPattern]) Source #

Dot all forced patterns and return a list of patterns that need to be undotted elsewhere. Patterns that need to be undotted are those that bind variables or does some actual (non-eta) matching.