| 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.
Synopsis
- modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
- initOccursCheck :: MetaVariable -> TCM ()
- defNeedsChecking :: QName -> TCM Bool
- tallyDef :: QName -> TCM ()
- data OccursExtra = OccursExtra {
- occUnfold :: UnfoldStrategy
- occVars :: VarMap
- occMeta :: MetaId
- occCxtSize :: Nat
- type OccursCtx = FreeEnv' () OccursExtra AllowedVar
- type OccursM = ReaderT OccursCtx TCM
- type AllowedVar = Modality -> All
- variableCheck :: VarMap -> Maybe Variable -> AllowedVar
- definitionCheck :: QName -> OccursM ()
- allowedVars :: OccursM (Nat -> Bool)
- data UnfoldStrategy
- defArgs :: OccursM a -> OccursM a
- unfoldB :: (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
- unfold :: (Instantiate t, Reduce t) => t -> OccursM t
- weakly :: OccursM a -> OccursM a
- strongly :: OccursM a -> OccursM a
- flexibly :: OccursM a -> OccursM a
- patternViolation' :: MonadTCM m => Int -> String -> m a
- abort :: TypeError -> OccursM a
- class Occurs t where
- occurs :: t -> OccursM t
- metaOccurs :: MetaId -> t -> TCM ()
- occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId -> VarMap -> a -> TCM a
- metaOccursQName :: MetaId -> QName -> TCM ()
- prune :: MonadMetaSolver m => MetaId -> Args -> (Nat -> Bool) -> m PruneResult
- hasBadRigid :: (MonadReduce m, HasConstInfo m, MonadAddContext m) => (Nat -> Bool) -> Term -> ExceptT () m Bool
- isNeutral :: HasConstInfo m => Blocked t -> QName -> Elims -> m Bool
- rigidVarsNotContainedIn :: (MonadReduce m, MonadAddContext m, MonadTCEnv m, MonadDebug m, AnyRigid a) => a -> (Nat -> Bool) -> m Bool
- class AnyRigid a where
- anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> a -> tcm Bool
- data PruneResult
- killArgs :: MonadMetaSolver m => [Bool] -> MetaId -> m PruneResult
- killedType :: MonadReduce m => [(Dom (ArgName, Type), Bool)] -> Type -> m ([Arg Bool], Type)
- reallyNotFreeIn :: MonadReduce m => IntSet -> Type -> m (IntSet, Type)
- performKill :: MonadMetaSolver m => [Arg Bool] -> MetaId -> Type -> m ()
MetaOccursCheck: going into definitions to exclude cyclic solutions
initOccursCheck :: MetaVariable -> TCM () Source #
Set the names of definitions to be looked at to the defs in the current mutual block.
OccursM monad and its services
data OccursExtra Source #
Extra environment for the occurs check. (Complements FreeEnv.)
Constructors
| OccursExtra | |
Fields
| |
type OccursCtx = FreeEnv' () OccursExtra AllowedVar Source #
Modality handling.
type AllowedVar = Modality -> All Source #
The passed modality is the one of the current context.
variableCheck :: VarMap -> Maybe Variable -> AllowedVar Source #
Check whether a free variable is allowed in the context as specified by the modality.
definitionCheck :: QName -> OccursM () Source #
Occurs check fails if a defined name is not available since it was declared in irrelevant or erased context.
allowedVars :: OccursM (Nat -> Bool) Source #
Construct a test whether a de Bruijn index is allowed or needs to be pruned.
Unfolding during occurs check.
data UnfoldStrategy Source #
Unfold definitions during occurs check? This effectively runs the occurs check on the normal form.
Instances
| Eq UnfoldStrategy Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs Methods (==) :: UnfoldStrategy -> UnfoldStrategy -> Bool # (/=) :: UnfoldStrategy -> UnfoldStrategy -> Bool # | |
| Show UnfoldStrategy Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs Methods showsPrec :: Int -> UnfoldStrategy -> ShowS # show :: UnfoldStrategy -> String # showList :: [UnfoldStrategy] -> ShowS # | |
Managing rigidiy during occurs check.
Error throwing during occurs check.
Implementation of the occurs check.
Extended occurs check.
Minimal complete definition
Nothing
Instances
| Occurs QName Source # | |
| Occurs Clause Source # | |
| Occurs LevelAtom Source # | |
| Occurs PlusLevel Source # | |
| Occurs Level Source # | |
| Occurs Sort Source # | |
| Occurs Type Source # | |
| Occurs Term Source # | |
| Occurs Defn Source # | |
| Occurs a => Occurs [a] Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs | |
| Occurs a => Occurs (Maybe a) Source # | |
| Occurs a => Occurs (Arg a) Source # | |
| (Occurs a, Subst t a) => Occurs (Abs a) Source # | |
| Occurs a => Occurs (Elim' a) Source # | |
| Occurs a => Occurs (Dom a) Source # | |
| (Occurs a, Occurs b) => Occurs (a, b) Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs | |
occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId -> VarMap -> a -> TCM a 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.
Pruning: getting rid of flexible occurrences.
Arguments
| :: MonadMetaSolver m | |
| => MetaId | Meta to prune. |
| -> Args | Arguments to meta variable. |
| -> (Nat -> Bool) | Test for allowed variable (de Bruijn index). |
| -> m 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.
Arguments
| :: (MonadReduce m, HasConstInfo m, MonadAddContext m) | |
| => (Nat -> Bool) | Test for allowed variable (de Bruijn index). |
| -> Term | Argument of meta variable. |
| -> ExceptT () m Bool | Exception if argument is matchable. |
hasBadRigid xs v = Just True iff one of the rigid variables in v is not in xs.
Actually we can only prune if a bad variable is in the head. See issue 458.
Or in a non-eliminateable position (see succeed/PruningNonMillerPattern).
hasBadRigid xs v = Nothing means that
we cannot prune at all as one of the meta args is matchable.
(See issue 1147.)
isNeutral :: HasConstInfo m => Blocked t -> QName -> Elims -> m Bool Source #
Check whether a term Def f es is finally stuck.
Currently, we give only a crude approximation.
rigidVarsNotContainedIn Source #
Arguments
| :: (MonadReduce m, MonadAddContext m, MonadTCEnv m, MonadDebug 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.
class AnyRigid a where Source #
Collect the *definitely* rigid variables in a monoid. We need to successively reduce the expression to do this.
Methods
anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> a -> tcm Bool Source #
Instances
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 :: MonadMetaSolver m => [Bool] -> MetaId -> m 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.
killedType :: MonadReduce m => [(Dom (ArgName, Type), Bool)] -> Type -> m ([Arg Bool], Type) Source #
killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')
(ignoring Dom). Let t' = (xs:as) -> b.
Invariant: k'i == True iff ki == True and pruning the ith argument from
type b is possible without creating unbound variables.
t' is type t after pruning all k'i==True.
reallyNotFreeIn :: MonadReduce m => IntSet -> Type -> m (IntSet, Type) Source #
Arguments
| :: MonadMetaSolver m | |
| => [Arg Bool] | Arguments to old meta var in left to right order
with |
| -> MetaId | The old meta var to receive pruning. |
| -> Type | The pruned type of the new meta var. |
| -> m () |
Instantiate a meta variable with a new one that only takes the arguments which are not pruneable.
Orphan instances
| IsVarSet () AllowedVar Source # | |
Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source # | |