| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.MetaVars.Occurs
Description
The occurs check for unification. Does pruning on the fly.
When hitting a meta variable:
- Compute flex/rigid for its arguments.
- Compare to allowed variables.
- Mark arguments with rigid occurrences of disallowed variables for deletion.
- Attempt to delete marked arguments.
- We don't need to check for success, we can just continue occurs checking.
We also check modality usability for all bound variables; see issue 8570. In the example there, we elaborate a term as a type (using resourcing rules for types), but then solve a term metavariable with it. Hence, well-resourcing needs to be re-checked when we solve the metavariable.
Synopsis
- data PruneResult
- killArgs :: [Bool] -> MetaId -> TCM PruneResult
- occursCheck :: MetaId -> VarMap -> Term -> TCM Term
- prune :: MetaId -> Args -> (Nat -> Bool) -> TCM PruneResult
- rigidVarsNotContainedIn :: (PureTCM m, AnyRigid a) => a -> (Nat -> Bool) -> m Bool
Documentation
data PruneResult Source #
Constructors
| NothingToPrune | the kill list is empty or only |
| PrunedNothing | there is no possible kill (because of type dep.) |
| PrunedSomething | managed to kill some args in the list |
| PrunedEverything | all prescribed kills where performed |
Instances
| Eq PruneResult Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs | |
| Show PruneResult Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs Methods showsPrec :: Int -> PruneResult -> ShowS # show :: PruneResult -> String # showList :: [PruneResult] -> ShowS # | |
killArgs :: [Bool] -> MetaId -> TCM PruneResult Source #
killArgs [k1,...,kn] X prunes argument i from metavar X if ki==True.
Pruning is carried out whenever > 0 arguments can be pruned.
occursCheck :: MetaId -> VarMap -> Term -> TCM Term Source #
When assigning m xs := v, check that m does not occur in v
and that the free variables of v are contained in xs.
Arguments
| :: MetaId | Meta to prune. |
| -> Args | Arguments to meta variable. |
| -> (Nat -> Bool) | Test for allowed variable (de Bruijn index). |
| -> TCM PruneResult |
prune m' vs xs attempts to remove all arguments from vs whose
free variables are not contained in xs.
If successful, m' is solved by the new, pruned meta variable and we
return True else False.
Issue 1147:
If any of the meta args vs is matchable, e.g., is a constructor term,
we cannot prune, because the offending variables could be removed by
reduction for a suitable instantiation of the meta variable.
rigidVarsNotContainedIn Source #
Arguments
| :: (PureTCM m, AnyRigid a) | |
| => a | |
| -> (Nat -> Bool) | Test for allowed variable (de Bruijn index). |
| -> m Bool |
Check whether any of the variables (given as de Bruijn indices) occurs *definitely* in the term in a rigid position. Reduces the term successively to remove variables in dead subterms. This fixes issue 1386.