ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.MetaVars.Occurs

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.

6 types
2 classes
30 values

PackageAgda-2.7.0.1
Exports38
LanguageHaskell2010
LicenceMIT
SourceOccurs.hs

MetaOccursCheck: going into definitions to exclude cyclic solutions

4 declarations

valuemodifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()

valueinitOccursCheck :: MetaVariable -> TCM ()

Set the names of definitions to be looked at to the defs in the current mutual block.

valuedefNeedsChecking :: QName -> TCM Bool

Is a def in the list of stuff to be checked?

valuetallyDef :: QName -> TCM ()

Remove a def from the list of defs to be looked at.

OccursM monad and its services

3 declarations

datadata OccursExtra

Extra environment for the occurs check. (Complements FreeEnv.)

Constructors

OccursExtra
- occUnfold :: UnfoldStrategy
- occVars :: VarMap
  The allowed variables with their variance.
- occMeta :: MetaId
  The meta we want to solve.
- occCxtSize :: Nat
  The size of the typing context upon invocation.

typetype OccursCtx = FreeEnv' () OccursExtra AllowedVar

typetype OccursM = ReaderT OccursCtx TCM

Modality handling.

typetype AllowedVar = Modality -> All

The passed modality is the one of the current context.

valuevariableCheck :: VarMap -> Maybe Variable -> AllowedVar

Check whether a free variable is allowed in the context as specified by the modality.

valuedefinitionCheck :: QName -> OccursM ()

Occurs check fails if a defined name is not available since it was declared in irrelevant or erased context.

valuemetaCheck :: MetaId -> OccursM MetaId

valueallowedVars :: OccursM (Nat -> Bool)

Construct a test whether a de Bruijn index is allowed or needs to be pruned.

Unfolding during occurs check.

datadata UnfoldStrategy

Unfold definitions during occurs check? This effectively runs the occurs check on the normal form.

YesUnfold NoUnfold

Instances2Eq, Show

Eq UnfoldStrategyDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Show UnfoldStrategyDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs

valuedefArgs :: OccursM a -> OccursM a

valueconArgs :: Elims -> OccursM a -> OccursM a

For a path constructor `c : ... -> Path D a b`, we have that e.g. `c es i0` reduces to a. So we have to consider its arguments as flexible when we do not actually unfold.

valueunfoldB :: (Instantiate t, Reduce t) => t -> OccursM (Blocked t)

valueunfold :: (Instantiate t, Reduce t) => t -> OccursM t

Managing rigidiy during occurs check.

valueweakly :: OccursM a -> OccursM a

Leave the strongly rigid position.

valuestrongly :: OccursM a -> OccursM a

valueflexibly :: OccursM a -> OccursM a

Error throwing during occurs check.

valuepatternViolation' :: MonadTCM m => Blocker -> Int -> String -> m a

valueabort :: Blocker -> TypeError -> OccursM a

Implementation of the occurs check.

6 declarations

classclass Occurs t where

Extended occurs check.

Methods

occurs :: t -> OccursM t
metaOccurs :: MetaId -> t -> TCM ()

Instances13Occurs, …

Occurs QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs ClauseDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs DefnDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs (Abs Term)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs (Abs Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs a => Occurs (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Occurs a => Occurs (Dom a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs

valueoccurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t

valuemetaOccurs2 :: (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()

valuemetaOccurs3

:: (Occurs a, Occurs b, Occurs c)
=> MetaId
-> a
-> b
-> c
-> TCM ()

valueoccursCheck :: MetaId -> VarMap -> Term -> TCM Term

When assigning m xs := v, check that m does not occur in v and that the free variables of v are contained in xs.

valuemetaOccursQName :: MetaId -> QName -> TCM ()

Pruning: getting rid of flexible occurrences.

10 declarations

valueprune

:: (PureTCM m, 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.

valuehasBadRigid

:: PureTCM 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.)

valueisNeutral :: HasConstInfo m => Blocked t -> QName -> Elims -> m Bool

Check whether a term Def f es is finally stuck. Currently, we give only a crude approximation.

valuerigidVarsNotContainedIn

:: (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.

classclass AnyRigid a where

Collect the *definitely* rigid variables in a monoid. We need to successively reduce the expression to do this.

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> a -> tcm Bool

Instances11AnyRigid, …

AnyRigid LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid a => AnyRigid (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid a => AnyRigid (Dom a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid a => AnyRigid (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AnyRigid a => AnyRigid [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
(Subst a, AnyRigid a) => AnyRigid (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
(AnyRigid a, AnyRigid b) => AnyRigid (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs

datadata PruneResult

Constructors

NothingToPrune
the kill list is empty or only Falses
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

Instances2Eq, Show

Eq PruneResultDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
Show PruneResultDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs

valuekillArgs :: MonadMetaSolver m => [Bool] -> MetaId -> m PruneResult

killArgs [k1,...,kn] X prunes argument i from metavar X if ki==True. Pruning is carried out whenever > 0 arguments can be pruned.

valuekilledType

:: MonadReduce m
=> [(Dom (ArgName, Type), Bool)]
-> Type
-> m ([Arg Bool], Type)

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.

valuereallyNotFreeIn :: MonadReduce m => IntSet -> Type -> m (IntSet, Type)

valueperformKill

:: MonadMetaSolver m
=> [Arg Bool]
Arguments to old meta var in left to right order with Bool indicating whether they can be pruned.
-> 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

1 instance

IsVarSet () AllowedVar