clash-lib-1.8.1: Clash: a functional hardware description language - As a library

Copyright | (C) 2012-2016 University of Twente 2021 QBayLogic B.V.
License | BSD2 (see the file LICENSE)
Maintainer | QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

Clash.Core.FreeVars

Contents

- Free variable calculation
- occurrence check
- Internal

Description

Free variable calculations

Synopsis

- typeFreeVars :: Fold Type TyVar
- freeIds :: Fold Term Id
- freeLocalVars :: Fold Term (Var a)
- freeLocalIds :: Fold Term Id
- globalIds :: Fold Term Id
- termFreeTyVars :: Fold Term TyVar
- globalIdOccursIn :: Id -> Term -> Bool
- localVarsDoNotOccurIn :: [Var a] -> Term -> Bool
- countFreeOccurances :: Term -> VarEnv Int
- 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

typeFreeVars :: Fold Type TyVar Source #

Gives the free type-variables in a Type, implemented as a `Fold`

The `Fold` is closed over the types of its variables, so:

    foldMapOf typeFreeVars unitVarSet ((a:* -> k) Int) = {a, k}

freeIds :: Fold Term Id Source #

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

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.

termFreeTyVars :: Fold Term TyVar Source #

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

The `Fold` is closed over the types of variables, so:

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

# occurrence check

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

Check whether a local identifier occurs free in a term

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

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

countFreeOccurances :: Term -> VarEnv Int Source #

Get the free variables of an expression and count the number of occurrences

# Internal

typeFreeVars' Source #

Arguments

:: (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 `termFreeVars'`
-> (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://gitlab.haskell.org/ghc/ghc/-/commit/503514b94f8dc7bd9eab5392206649aee45f140b

termFreeVars' Source #

Arguments

:: (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://gitlab.haskell.org/ghc/ghc/-/commit/503514b94f8dc7bd9eab5392206649aee45f140b