Module Finitize

A module to convert an infinite type to a finite type by constraining it to a finite set of values.

The result of instantiating this module exposes a Type class that is the finite version of the infinite input type, e.g. Finitize<MyInfiniteType, myConstraint/1>::Type.

Example usage:

// Given a predicate to constrain an infinite type, such as `string`:
predicate functionName(string s) { exists(Function f | f.getName() = s) }

// Use that infinite type without a `bindingset` by applying the constraint:
predicate upperCaseFunctionName(Finitize<string, functionName/1>::Type str) {
  result = str.toUpperCase()
}

Note that this module cannot strip bindingset[this] from the members of the given infinite type without knowing the names and signatures. This isn’t usually a problem, but can prevent the use of some parameterized modules. This module does strip the bindingset[this] from the toString() method since that member has a known signature.