Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Free.Reduce

Description

Free variable check that reduces the subject to make certain variables not free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.

Synopsis

class (PrecomputeFreeVars a, Subst a) => ForceNotFree a
forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a)
data IsFree
- = MaybeFree MetaSet
- | NotFree

Documentation

class (PrecomputeFreeVars a, Subst a) => ForceNotFree a Source #

Minimal complete definition

forceNotFree'

Instances

Instances details

ForceNotFree PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel
ForceNotFree Level Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Level -> m Level
ForceNotFree Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort
ForceNotFree Type Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type
ForceNotFree Term Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Term -> m Term
ForceNotFree a => ForceNotFree [a] Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => [a] -> m [a]
(Reduce a, ForceNotFree a) => ForceNotFree (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Arg a -> m (Arg a)
(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)
(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a)
(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a)

forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a) Source #

Try to enforce a set of variables not occurring in a given type. Returns a possibly reduced version of the type and for each of the given variables whether it is either not free, or maybe free depending on some metavariables.

data IsFree Source #

A variable can either not occur (NotFree) or it does occur (MaybeFree). In the latter case, the occurrence may disappear depending on the instantiation of some set of metas.

Constructors

MaybeFree MetaSet
NotFree

Instances

Instances details

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