Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

Documentation

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

Minimal complete definition

forceNotFree'

Instances

Instances details
ForceNotFree Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Level -> m Level

ForceNotFree PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel

ForceNotFree Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Sort -> m Sort

ForceNotFree Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Term -> m Term

ForceNotFree Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Type -> m Type

(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 (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)

(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)

ForceNotFree a => ForceNotFree [a] Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => [a] -> m [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.

reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a)) Source #

Checks if the given term contains any free variables that are in the given set of variables, possibly reducing the term in the process. Returns `Right Nothing` if there are such variables, `Right (Just v')` if there are none (where v' is the possibly reduced version of the given term) or `Left b` if the problem is blocked on a meta.

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
Show IsFree Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

showsPrec :: Int -> IsFree -> ShowS

show :: IsFree -> String

showList :: [IsFree] -> ShowS

Eq IsFree Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

(==) :: IsFree -> IsFree -> Bool

(/=) :: IsFree -> IsFree -> Bool