Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Atd.Unique_name
SourceFunctions to translate an identifier into one that's not reserved or already taken.
When necessary, identifiers are modified by adding prefixes or suffixes that are compatible with Python syntax.
Important terminology:
The general goal in practice is to minimize the differences between source and destination identifiers.
Things a user might want to do:
create
function.translate
function.The mutable container holding all translation data.
val init :
reserved_identifiers:string list ->
reserved_prefixes:string list ->
safe_prefix:string ->
t
Initialize the translation tables by specifying the set of identifiers already reserved in the destination space.
reserved_identifiers
are forbidden identifiers, i.e. we guarantee that a translation will never return one of these. safe_prefix
is a prefix that will be added to an identifier that matches one of the reserved prefixes (reserved_prefixes
).
Reserve a new identifier in the source space. If the given name is already an identifier in the source space, a new identifier is created by appending an alphanumeric suffix and returned.
Repeated calls of this function on the same input will produce a different output each time.
Translate an identifier from the source space to the destination space.
This registers the translation of a name if it's not already registered. The translation is a name in the destination space that is not reserved for other uses.
Repeated calls of this function on the same input will produce the same output as the previous times.
Return whether a name exists in the source space. If it exists, return its translation to the destination space.
Return whether a name exists in the destination space. If it exists, return its translation to the source space.