nominal-0.2.0.0: Binders and alpha-equivalence made easy

Safe HaskellSafe
LanguageHaskell2010

Nominal.ConcreteNames

Description

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.

This module exposes implementation details of the Nominal library, and should not normally be imported. Users of the library should only import the top-level module Nominal.

Synopsis

Documentation

type NameSuggestion = [String] Source #

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 Source #

The names to use if nothing else was specified.

to_subscript :: Char -> Char Source #

Convert a digit to a subscript.

isAlphaOrWild :: Char -> Bool Source #

Check if a character is a letter or underscore.

expand_default :: NameSuggestion -> [String] Source #

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

data NameGen Source #

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

default_namegen :: NameGen Source #

The default name generator.

rename_fresh :: Set String -> NameGen -> String Source #

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

combine_names :: NameGen -> NameGen -> NameGen Source #

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