Map indexed by variables

Is the environment empty

Look up a value based on the variable

Lookup a value based on the variable

Errors out when the variable is not present

Lookup a value based on the unique of a variable

Empty map

Environment containing a single variable-value pair

Create an environment given a list of var-value pairs

Add a variable-value pair to the environment; overwrites the value if the variable already exists

Add a list of variable-value pairs; the values of existing keys will be overwritten

Add a variable-value pair to the environment; if the variable already exists, the two values are merged with the given function

Remove a variable-value pair from the environment

Remove a list of variable-value pairs from the environment

Get the (left-biased) union of two environments

Get the union of two environments, mapped values existing in both environments will be merged with the given function.

Apply a function to every element in the environment

Apply a function to every element in the environment; values for which the function returns Nothing are removed from the environment

Strict left-fold over an environment using both the unique of the the variable and the value

Does the variable exist in the environment

Does the variable not exist in the environment

Extract the elements

Set of variables

The empty set

The set of a single variable

Remove a variable from the set based on its Unique

Union two sets

Is the variable an element in the set

Is the variable not an element in the set

Create a set from a list of variables

Set of variables that is in scope at some point

The Int is a kind of hash-value used to generate new uniques. It should never be zero

See "Secrets of the Glasgow Haskell Compiler inliner" Section 3.2 for the motivation

The empty set

Look up a variable in the InScopeSet. This gives you the canonical version of the variable

Create a set of variables in scope

The empty set

Add a list of variables in scope

Union two sets of in scope variables

Is the variable in scope

Check whether an element exists in the set based on the Unique contained in that element

Is the variable not in scope

Is the set of variables in scope

Ensure that the Unique of a variable does not occur in the InScopeSet

Rename environment for e.g. alpha equivalence

When going under binders for e.g.

x -> e1  aeq y -> e2

We want to rename [x -> y] or [y -> x], but we have to pick a binder that is neither free in e1 nor e2 or we risk accidental capture.

So we must maintain:

1. A renaming for the left term
2. A renaming for the right term
3. A set of in scope variables

Create an empty renaming environment

Simultaneously go under the binder bL and binder bR, finds a new binder newTvB, and return an environment mapping [bL -> newB] and [bR -> newB]

Simultaneously go under the type-variable binder bTvL and type-variable binder bTvR, finds a new binder newTvB, and return an environment mapping [bTvL -> newB] and [bTvR -> newB]

Applies rnTmBndr to several variables: the two variable lists must be of equal length.

Applies rnTyBndr to several variables: the two variable lists must be of equal length.

Look up the renaming of an occurrence in the left term

Look up the renaming of an occurrence in the left term

Look up the renaming of an type-variable occurrence in the left term

Look up the renaming of an type-variable occurrence in the right term