| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
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.
- type NameSuggestion = [String]
- default_names :: NameSuggestion
- to_subscript :: Char -> Char
- isAlphaOrWild :: Char -> Bool
- expand_default :: NameSuggestion -> [String]
- data NameGen = NameGen NameSuggestion (NameSuggestion -> [String])
- default_namegen :: NameGen
- rename_fresh :: Set String -> NameGen -> String
- combine_names :: NameGen -> NameGen -> NameGen
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.
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 Source #
The default name generator.