Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.MetaVars.Occurs

Contents

- MetaOccursCheck: going into definitions to exclude cyclic solutions
- OccursM monad and its services
  - Modality handling.
  - Unfolding during occurs check.
  - Managing rigidiy during occurs check.
  - Error throwing during occurs check.
- Implementation of the occurs check.
- Pruning: getting rid of flexible occurrences.
- Orphan instances

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
  - occMeta :: MetaId
  - occVars :: VarMap
  - occRHS :: Term
  - occCxtSize :: Nat
  }
- type OccursCtx = FreeEnv' () OccursExtra AllowedVar
- type OccursM = ReaderT OccursCtx TCM
- type AllowedVar = Modality -> All
- variableCheck :: VarMap -> Maybe Variable -> AllowedVar
- definitionCheck :: QName -> OccursM ()
- metaCheck :: MetaId -> OccursM MetaId
- allowedVars :: OccursM (Nat -> Bool)
- data UnfoldStrategy
  - = YesUnfold
  - | NoUnfold
- defArgs :: OccursM a -> OccursM a
- conArgs :: Elims -> 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 => Blocker -> Int -> String -> m a
- abort :: Blocker -> TypeError -> OccursM a
- class Occurs t where
  - occurs :: t -> OccursM t
  - metaOccurs :: MetaId -> t -> TCM ()
- occurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t
- metaOccurs2 :: (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
- metaOccurs3 :: (Occurs a, Occurs b, Occurs c) => MetaId -> a -> b -> c -> TCM ()
- occursCheck :: MetaId -> VarMap -> Term -> TCM Term
- metaOccursQName :: MetaId -> QName -> TCM ()
- prune :: (PureTCM m, MonadMetaSolver m) => MetaId -> Args -> (Nat -> Bool) -> m PruneResult
- hasBadRigid :: forall (m :: Type -> Type). PureTCM m => (Nat -> Bool) -> Term -> ExceptT () m Bool
- isNeutral :: HasConstInfo m => Blocked t -> QName -> Elims -> m Bool
- rigidVarsNotContainedIn :: (PureTCM m, AnyRigid a) => a -> (Nat -> Bool) -> m Bool
- class AnyRigid a where
  - anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> a -> tcm Bool
- data PruneResult
  - = NothingToPrune
  - | PrunedNothing
  - | PrunedSomething
  - | PrunedEverything
- killArgs :: MonadMetaSolver m => [Bool] -> MetaId -> m PruneResult
- killedType :: MonadReduce m => [(Dom (ArgName, Type), Bool)] -> Type -> m ([Arg Bool], Type)
- reallyNotFreeIn :: MonadReduce m => VarSet -> Type -> m (VarSet, Type)
- performKill :: MonadMetaSolver m => [Arg Bool] -> MetaId -> Type -> m ()

# MetaOccursCheck: going into definitions to exclude cyclic solutions

modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM () Source #

initOccursCheck :: MetaVariable -> TCM () Source #

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

defNeedsChecking :: QName -> TCM Bool Source #

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

tallyDef :: QName -> TCM () Source #

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

# OccursM monad and its services

data OccursExtra Source #

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

Constructors

OccursExtra |

Fields

- occUnfold :: UnfoldStrategy
- occMeta :: MetaId

  The meta `m` we want to solve.

- occVars :: VarMap

  The allowed variables `xs` with their variance.

- occRHS :: Term

  The proposed solution `v` for the meta (`m xs := v`).

- occCxtSize :: Nat

  The size of the typing context upon invocation.

type OccursCtx = FreeEnv' () OccursExtra AllowedVar Source #

type OccursM = ReaderT OccursCtx TCM 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.

metaCheck :: MetaId -> OccursM MetaId Source #

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.

Constructors

YesUnfold |
NoUnfold |

#### Instances

Instances details

Show UnfoldStrategy Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods showsPrec :: Int -> UnfoldStrategy -> ShowS Source # show :: UnfoldStrategy -> String Source # showList :: [UnfoldStrategy] -> ShowS Source #
Eq UnfoldStrategy Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods (==) :: UnfoldStrategy -> UnfoldStrategy -> Bool Source # (/=) :: UnfoldStrategy -> UnfoldStrategy -> Bool Source #

defArgs :: OccursM a -> OccursM a Source #

conArgs :: Elims -> OccursM a -> OccursM a Source #

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.

unfoldB :: (Instantiate t, Reduce t) => t -> OccursM (Blocked t) Source #

unfold :: (Instantiate t, Reduce t) => t -> OccursM t Source #

## Managing rigidiy during occurs check.

weakly :: OccursM a -> OccursM a Source #

Leave the strongly rigid position.

strongly :: OccursM a -> OccursM a Source #

flexibly :: OccursM a -> OccursM a Source #

## Error throwing during occurs check.

patternViolation' :: MonadTCM m => Blocker -> Int -> String -> m a Source #

abort :: Blocker -> TypeError -> OccursM a Source #

# Implementation of the occurs check.

class Occurs t where Source #

Extended occurs check.

Minimal complete definition

occurs

Methods

occurs :: t -> OccursM t Source #

metaOccurs :: MetaId -> t -> TCM () Source #

default metaOccurs :: forall (f :: Type -> Type) a. (Foldable f, Occurs a, f a ~ t) => MetaId -> t -> TCM () Source #

#### Instances

Instances details

Occurs QName Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: QName -> OccursM QName Source # metaOccurs :: MetaId -> QName -> TCM () Source #
Occurs Clause Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Clause -> OccursM Clause Source # metaOccurs :: MetaId -> Clause -> TCM () Source #
Occurs Elims Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Elims -> OccursM Elims Source # metaOccurs :: MetaId -> Elims -> TCM () Source #
Occurs Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Level -> OccursM Level Source # metaOccurs :: MetaId -> Level -> TCM () Source #
Occurs PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: PlusLevel -> OccursM PlusLevel Source # metaOccurs :: MetaId -> PlusLevel -> TCM () Source #
Occurs Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Sort -> OccursM Sort Source # metaOccurs :: MetaId -> Sort -> TCM () Source #
Occurs Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Term -> OccursM Term Source # metaOccurs :: MetaId -> Term -> TCM () Source #
Occurs Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Type -> OccursM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
Occurs Defn Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Defn -> OccursM Defn Source # metaOccurs :: MetaId -> Defn -> TCM () Source #
Occurs a => Occurs (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Arg a -> OccursM (Arg a) Source # metaOccurs :: MetaId -> Arg a -> TCM () Source #
Occurs (Abs Term) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Term -> OccursM (Abs Term) Source # metaOccurs :: MetaId -> Abs Term -> TCM () Source #
Occurs (Abs Type) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Type -> OccursM (Abs Type) Source # metaOccurs :: MetaId -> Abs Type -> TCM () Source #
Occurs a => Occurs (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Dom a -> OccursM (Dom a) Source # metaOccurs :: MetaId -> Dom a -> TCM () Source #

occurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t Source #

metaOccurs2 :: (Occurs a, Occurs b) => MetaId -> a -> b -> TCM () Source #

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

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`.

metaOccursQName :: MetaId -> QName -> TCM () Source #

# Pruning: getting rid of flexible occurrences.

prune Source #

Arguments

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

hasBadRigid Source #

Arguments

:: forall (m :: Type -> Type). 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.)

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

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

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 :: PureTCM tcm => (Nat -> tcm Bool) -> a -> tcm Bool Source #

#### Instances

Instances details

AnyRigid Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Level -> tcm Bool Source #
AnyRigid PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> PlusLevel -> tcm Bool Source #
AnyRigid Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Sort -> tcm Bool Source #
AnyRigid Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Term -> tcm Bool Source #
AnyRigid Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Type -> tcm Bool Source #
AnyRigid a => AnyRigid (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Arg a -> tcm Bool Source #
(Subst a, AnyRigid a) => AnyRigid (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Abs a -> tcm Bool Source #
AnyRigid a => AnyRigid (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Dom a -> tcm Bool Source #
AnyRigid a => AnyRigid (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Elim' a -> tcm Bool Source #
AnyRigid a => AnyRigid [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> [a] -> tcm Bool Source #
(AnyRigid a, AnyRigid b) => AnyRigid (a, b) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> (a, b) -> tcm Bool Source #

data PruneResult Source #

Constructors

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

Instances details

Show PruneResult Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods showsPrec :: Int -> PruneResult -> ShowS Source # show :: PruneResult -> String Source # showList :: [PruneResult] -> ShowS Source #
Eq PruneResult Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods (==) :: PruneResult -> PruneResult -> Bool Source # (/=) :: PruneResult -> PruneResult -> Bool Source #

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 `i`th argument from type `b` is possible without creating unbound variables. `t'` is type `t` after pruning all `k'i==True`.

reallyNotFreeIn :: MonadReduce m => VarSet -> Type -> m (VarSet, Type) Source #

performKill Source #

Arguments

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

IsVarSet () AllowedVar Source # |
Instance details Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source #