Nominal.ConcreteNames

This module provides a way to generate infinitely many distinct concrete variable names from a list of name suggestions.

Since bound atoms must sometimes be renamed, we need a way to generate suitable concrete names. This should be configurable on a per-atom basis, with a fallback default behavior for each atom type.

A name suggestion is a list of possible names. The first useable name from the list is chosen. If the list is finite and contains no useable names, then we will generate more names by appending numerical subscripts. A client can override this default behavior by specifying an infinite list of name suggestions.

An empty list of name suggestions counts as no suggestion, in which case a default will be used.

When merging two atoms (see merge), we concatenate their name suggestions. In particular, if one name has a user-specified suggestion and the other one does not, we always use the user-specified one.

Documentation

type NameSuggestion = [String]

A name suggestion is a list of possible names. When an atom must be renamed, the first useable name from the list is chosen. If the list is finite and contains no useable names, then additional names will be generated by appending numerical subscripts. To override this behavior, redefine expand_names for the given AtomKind instance, or specify an infinite list of names.

default_names :: NameSuggestion

The names to use if nothing else was specified.

to_subscript :: Char -> Char

Convert a digit to a subscript.

isAlphaOrWild :: Char -> Bool

Check if a character is a letter or underscore.

expand_default :: NameSuggestion -> [String]

Generate an infinite list of possible names from a (possibly finite) list of suggestions.

data NameGen

A name generator consists of a (possibly finite) list of name suggestions and an expander, which is a function for generating more names.

Constructors

NameGen NameSuggestion (NameSuggestion -> [String])

default_namegen :: NameGen

The default name generator.

rename_fresh :: Set String -> NameGen -> String

Compute a string that is not in the given set, and whose name is based on the supplied suggestions.

combine_names :: NameGen -> NameGen -> NameGen

Merge two name suggestions. Essentially this appends them, but we try to avoid duplication. We use the left expander.