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

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)
- reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))
- data IsFree
  - = MaybeFree MetaSet
  - | NotFree

# 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 Source # show :: IsFree -> String Source # showList :: [IsFree] -> ShowS Source #
Eq IsFree Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods (==) :: IsFree -> IsFree -> Bool Source # (/=) :: IsFree -> IsFree -> Bool Source #