Copyright | (C) 2012-2016 University of Twente |
---|---|

License | BSD2 (see the file LICENSE) |

Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |

Safe Haskell | None |

Language | Haskell2010 |

Free variable calculations

## Synopsis

- typeFreeVars :: Fold Type TyVar
- termFreeVarsX :: Fold Term (Var a)
- freeIds :: Fold Term Id
- freeLocalVars :: Fold Term (Var a)
- freeLocalIds :: Fold Term Id
- globalIds :: Fold Term Id
- termFreeTyVars :: Fold Term TyVar
- tyFVsOfTypes :: Foldable f => f Type -> VarSet
- localFVsOfTerms :: Foldable f => f Term -> VarSet
- hasLocalFreeVars :: Term -> Bool
- noFreeVarsOfType :: Type -> Bool
- localIdOccursIn :: Id -> Term -> Bool
- globalIdOccursIn :: Id -> Term -> Bool
- localIdDoesNotOccurIn :: Id -> Term -> Bool
- localIdsDoNotOccurIn :: [Id] -> Term -> Bool
- localVarsDoNotOccurIn :: [Var a] -> Term -> Bool
- typeFreeVars' :: (Contravariant f, Applicative f) => (forall b. Var b -> Bool) -> IntSet -> (Var a -> f (Var a)) -> Type -> f Type
- termFreeVars' :: (Contravariant f, Applicative f) => (forall b. Var b -> Bool) -> (Var a -> f (Var a)) -> Term -> f Term

# Free variable calculation

termFreeVarsX :: Fold Term (Var a) Source #

Gives the free variables of a Term, implemented as a `Fold`

The `Fold`

is closed over the types of variables, so:

foldMapOf termFreeVars unitVarSet (case (x : (a:* -> k) Int)) of {}) = {x, a, k}

**NB** this collects both global and local IDs, and you almost **NEVER** want
to use this. Use one of the other FV calculations instead

freeLocalVars :: Fold Term (Var a) Source #

Calculate the *local* free variable of an expression: the free type
variables and the free identifiers that are not bound in the global
environment.

freeLocalIds :: Fold Term Id Source #

Calculate the *local* free identifiers of an expression: the free
identifiers that are not bound in the global environment.

globalIds :: Fold Term Id Source #

Calculate the *global* free identifiers of an expression: the free
identifiers that are bound in the global environment.

tyFVsOfTypes :: Foldable f => f Type -> VarSet Source #

Collect the free variables of a collection of type into a set

localFVsOfTerms :: Foldable f => f Term -> VarSet Source #

Collect the free variables of a collection of terms into a set

hasLocalFreeVars :: Term -> Bool Source #

Determines if term has any locally free variables. That is, the free type variables and the free identifiers that are not bound in the global scope.

# Fast

noFreeVarsOfType :: Type -> Bool Source #

Determine whether a type has no free type variables.

# occurrence check

localIdOccursIn :: Id -> Term -> Bool Source #

Check whether a local identifier occurs free in a term

globalIdOccursIn :: Id -> Term -> Bool Source #

Check whether a local identifier occurs free in a term

localIdDoesNotOccurIn :: Id -> Term -> Bool Source #

Check whether an identifier does not occur free in a term

localIdsDoNotOccurIn :: [Id] -> Term -> Bool Source #

Check whether a set of identifiers does not occur free in a term

localVarsDoNotOccurIn :: [Var a] -> Term -> Bool Source #

Check whether a set of variables does not occur free in a term

# Internal

:: (Contravariant f, Applicative f) | |

=> (forall b. Var b -> Bool) | Predicate telling whether a variable is interesting |

-> IntSet | Uniques of the variables in scope, used by |

-> (Var a -> f (Var a)) | |

-> Type | |

-> f Type |

Gives the "interesting" free variables in a Type, implemented as a `Fold`

The `Fold`

is closed over the types of variables, so:

foldMapOf (typeFreeVars' (const True) IntSet.empty) unitVarSet ((a:* -> k) Int) = {a, k}

Note [Closing over kind variables]

Consider the type

forall k . b -> k

where

b :: k -> Type

When we close over the free variables of `forall k . b -> k`

, i.e. `b`

, then
the `k`

in `b :: k -> Type`

is most definitely *not* the `k`

in
`forall k . b -> k`

. So when a type variable is free, i.e. not in the inScope
set, its kind variables also aren´t; so in order to prevent collisions due to
shadowing we close using an empty inScope set.

See also: https://git.haskell.org/ghc.git/commitdiff/503514b94f8dc7bd9eab5392206649aee45f140b

:: (Contravariant f, Applicative f) | |

=> (forall b. Var b -> Bool) | Predicate telling whether a variable is interesting |

-> (Var a -> f (Var a)) | |

-> Term | |

-> f Term |

Gives the "interesting" free variables in a Term, implemented as a `Fold`

The `Fold`

is closed over the types of variables, so:

foldMapOf (termFreeVars' (const True)) unitVarSet (case (x : (a:* -> k) Int)) of {}) = {x, a, k}

Note [Closing over type variables]

Consider the term

/\(k :: Type) -> \(b :: k) -> a

where

a :: k

When we close over the free variables of `/k -> (b :: k) -> (a :: k)`

, i.e.
`a`

, then the `k`

in `a :: k`

is most definitely *not* the `k`

in introduced
by the `/k ->`

. So when a term variable is free, i.e. not in the inScope
set, its type variables also aren´t; so in order to prevent collisions due to
shadowing we close using an empty inScope set.

See also: https://git.haskell.org/ghc.git/commitdiff/503514b94f8dc7bd9eab5392206649aee45f140b