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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.MetaVars.Occurs

Contents

- Getting rid of flexible occurrences

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 OccursCtx
  - = Flex
  - | Rigid
  - | StronglyRigid
  - | Irrel
- data UnfoldStrategy
  - = YesUnfold
  - | NoUnfold
- defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
- unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
- weakly :: OccursCtx -> OccursCtx
- strongly :: OccursCtx -> OccursCtx
- patternViolation' :: Int -> String -> TCM a
- abort :: OccursCtx -> TypeError -> TCM a
- type Vars = ([Nat], [Nat], [Nat])
- goIrrelevant :: Vars -> Vars
- goNonStrict :: Vars -> Vars
- allowedVar :: Nat -> Vars -> Bool
- takeRelevant :: Vars -> [Nat]
- takeAll :: Vars -> [Nat]
- liftUnderAbs :: Vars -> Vars
- class Occurs t where
  - occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t
  - metaOccurs :: MetaId -> t -> TCM ()
- occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId -> Vars -> a -> TCM a
- metaOccursQName :: MetaId -> QName -> TCM ()
- prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
- hasBadRigid :: [Nat] -> Term -> ExceptT () TCM Bool
- isNeutral :: MonadTCM tcm => Blocked t -> QName -> Elims -> tcm Bool
- rigidVarsNotContainedIn :: (MonadTCM tcm, FoldRigid a) => a -> [Nat] -> tcm Bool
- class FoldRigid a where
  - foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> a -> TCM m
- data PruneResult
  - = NothingToPrune
  - | PrunedNothing
  - | PrunedSomething
  - | PrunedEverything
- killArgs :: [Bool] -> MetaId -> TCM PruneResult
- killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> TCM ([Arg Bool], Type)
- reallyNotFreeIn :: IntSet -> Type -> TCM (IntSet, Type)
- performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()

# Documentation

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.

data OccursCtx Source #

Constructors

Flex | We are in arguments of a meta.
Rigid | We are not in arguments of a meta but a bound var.
StronglyRigid | We are at the start or in the arguments of a constructor.
Irrel | We are in an irrelevant argument.

Instances

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

data UnfoldStrategy Source #

Constructors

YesUnfold |
NoUnfold |

Instances

Eq UnfoldStrategy Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods (==) :: UnfoldStrategy -> UnfoldStrategy -> Bool Source # (/=) :: UnfoldStrategy -> UnfoldStrategy -> Bool Source #
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 #

defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx Source #

unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term) Source #

weakly :: OccursCtx -> OccursCtx Source #

Leave the strongly rigid position.

strongly :: OccursCtx -> OccursCtx Source #

patternViolation' :: Int -> String -> TCM a Source #

abort :: OccursCtx -> TypeError -> TCM a Source #

type Vars = ([Nat], [Nat], [Nat]) Source #

Distinguish relevant, irrelevant and nonstrict variables in occurs check.

goIrrelevant :: Vars -> Vars Source #

goNonStrict :: Vars -> Vars Source #

allowedVar :: Nat -> Vars -> Bool Source #

takeRelevant :: Vars -> [Nat] Source #

takeAll :: Vars -> [Nat] Source #

liftUnderAbs :: Vars -> Vars Source #

class Occurs t where Source #

Extended occurs check.

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t Source #

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

Instances

Occurs QName Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> QName -> TCM QName Source # metaOccurs :: MetaId -> QName -> TCM () Source #
Occurs Clause Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Clause -> TCM Clause Source # metaOccurs :: MetaId -> Clause -> TCM () Source #
Occurs LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> LevelAtom -> TCM LevelAtom Source # metaOccurs :: MetaId -> LevelAtom -> TCM () Source #
Occurs PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> PlusLevel -> TCM PlusLevel Source # metaOccurs :: MetaId -> PlusLevel -> TCM () Source #
Occurs Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Level -> TCM Level Source # metaOccurs :: MetaId -> Level -> TCM () Source #
Occurs Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Sort -> TCM Sort Source # metaOccurs :: MetaId -> Sort -> TCM () Source #
Occurs Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
Occurs Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Term -> TCM Term Source # metaOccurs :: MetaId -> Term -> TCM () Source #
Occurs Defn Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Defn -> TCM Defn Source # metaOccurs :: MetaId -> Defn -> TCM () Source #
Occurs a => Occurs [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> [a] -> TCM [a] Source # metaOccurs :: MetaId -> [a] -> TCM () Source #
Occurs a => Occurs (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Maybe a -> TCM (Maybe a) Source # metaOccurs :: MetaId -> Maybe a -> TCM () Source #
Occurs a => Occurs (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Dom a -> TCM (Dom a) Source # metaOccurs :: MetaId -> Dom a -> TCM () Source #
Occurs a => Occurs (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Arg a -> TCM (Arg a) Source # metaOccurs :: MetaId -> Arg a -> TCM () Source #
(Occurs a, Subst t a) => Occurs (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Abs a -> TCM (Abs a) Source # metaOccurs :: MetaId -> Abs a -> TCM () Source #
Occurs a => Occurs (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Elim' a -> TCM (Elim' a) Source # metaOccurs :: MetaId -> Elim' a -> TCM () Source #
(Occurs a, Occurs b) => Occurs (a, b) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> (a, b) -> TCM (a, b) Source # metaOccurs :: MetaId -> (a, b) -> TCM () Source #

occursCheck :: (Occurs a, InstantiateFull a, PrettyTCM a) => MetaId -> Vars -> 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`.

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

# Getting rid of flexible occurrences

prune :: MetaId -> Args -> [Nat] -> TCM PruneResult Source #

`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 :: [Nat] -> Term -> ExceptT () TCM Bool Source #

`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 :: MonadTCM tcm => Blocked t -> QName -> Elims -> tcm Bool Source #

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

rigidVarsNotContainedIn :: (MonadTCM tcm, FoldRigid a) => a -> [Nat] -> tcm Bool Source #

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 FoldRigid a where Source #

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

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> a -> TCM m Source #

Instances

FoldRigid LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m Source #
FoldRigid PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m Source #
FoldRigid Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Level -> TCM m Source #
FoldRigid Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Sort -> TCM m Source #
FoldRigid Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m Source #
FoldRigid Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Term -> TCM m Source #
FoldRigid a => FoldRigid [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> [a] -> TCM m Source #
FoldRigid a => FoldRigid (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Dom a -> TCM m Source #
FoldRigid a => FoldRigid (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Arg a -> TCM m Source #
(Subst t a, FoldRigid a) => FoldRigid (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Abs a -> TCM m Source #
FoldRigid a => FoldRigid (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Elim' a -> TCM m Source #
(FoldRigid a, FoldRigid b) => FoldRigid (a, b) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> (a, b) -> TCM m 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

Eq PruneResult Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods (==) :: PruneResult -> PruneResult -> Bool Source # (/=) :: PruneResult -> PruneResult -> Bool Source #
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 #

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.

killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> TCM ([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 :: IntSet -> Type -> TCM (IntSet, Type) Source #

performKill Source #

Arguments

:: [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.
-> TCM () |

Instantiate a meta variable with a new one that only takes the arguments which are not pruneable.