public abstract class VariableNamer extends java.lang.Object implements InstantiationProposer
Modifier and Type | Class and Description |
---|---|
protected static class |
VariableNamer.BasenameAndIndex
tuple of a basename and an index
|
private static class |
VariableNamer.CustomJavaASTWalker
a customized JavaASTWalker
|
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
private static class |
VariableNamer.PermIndProgramElementName
regular indexed ProgramElementName
|
private static class |
VariableNamer.TempIndProgramElementName
temporary indexed ProgramElementName
|
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
DEFAULT_BASENAME
default basename for variable name proposals
|
protected java.util.HashMap<ProgramVariable,ProgramVariable> |
map |
protected java.util.HashMap<ProgramVariable,ProgramVariable> |
renamingHistory |
protected Services |
services
pointer to services object
|
private static boolean |
suggestive_off
status of suggestive name proposing
|
private static java.lang.String |
TEMPCOUNTER_NAME
name of the counter object used for temporary name proposals
|
Constructor and Description |
---|
VariableNamer(Services services) |
Modifier and Type | Method and Description |
---|---|
protected ProgramElementName |
createName(java.lang.String basename,
int index,
NameCreationInfo creationInfo)
creates a ProgramElementName object to be used for permanent names
|
private Term |
findProgramInTerm(Term term)
returns the subterm containing a java block, or null
(helper for getProgramFromPIO())
|
static Name |
getBasename(Name name) |
protected VariableNamer.BasenameAndIndex |
getBasenameAndIndex(ProgramElementName name)
determines the passed ProgramElementName's basename and index (ignoring
temporary indices)
|
private java.lang.String |
getBaseNameProposal(Type type)
proposes a base name for a given sort
|
protected int |
getMaxCounterInGlobals(java.lang.String basename,
java.lang.Iterable<ProgramElementName> globals)
returns the maximum counter value already associated with the passed
basename in the passed list of global variables, or -1
|
protected int |
getMaxCounterInProgram(java.lang.String basename,
ProgramElement program,
PosInProgram posOfDeclaration)
returns the maximum counter value already associated with the passed
basename in the passed program (ignoring temporary counters), or -1
|
protected ProgramElementName |
getNameProposalForSchemaVariable(java.lang.String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
|
protected ProgramElement |
getProgramFromPIO(PosInOccurrence pio)
returns the program contained in a PosInOccurrence
|
java.lang.String |
getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
|
java.util.HashMap<ProgramVariable,ProgramVariable> |
getRenamingMap() |
java.lang.String |
getSuggestiveNameProposalForProgramVariable(SchemaVariable sv,
TacletApp app,
Services services,
ImmutableList<java.lang.String> previousProposals) |
java.lang.String |
getSuggestiveNameProposalForSchemaVariable(Expression e) |
ProgramElementName |
getTemporaryNameProposal(java.lang.String basename)
proposes a unique name; intended for use in places where the information
required by getProposal() is not available
|
private ProgramElement |
instantiateExpression(ProgramElement e,
SVInstantiations svInst,
Services services) |
protected boolean |
isUniqueInGlobals(java.lang.String name,
java.lang.Iterable<ProgramElementName> globals)
tells whether a name is unique in the passed list of global variables
|
protected boolean |
isUniqueInProgram(java.lang.String name,
ProgramElement program,
PosInProgram posOfDeclaration)
tells whether a name is unique in the passed program
|
boolean |
isUniqueNameForSchemaVariable(java.lang.String name,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration)
tells whether a name for instantiating a schema variable is unique
within its scope
|
static ProgramElementName |
parseName(java.lang.String name) |
static ProgramElementName |
parseName(java.lang.String name,
Comment[] comments) |
static ProgramElementName |
parseName(java.lang.String name,
NameCreationInfo creationInfo) |
static ProgramElementName |
parseName(java.lang.String name,
NameCreationInfo creationInfo,
Comment[] comments)
parses the passed string and creates a suitable program element name
(this does *not* make the name unique - if that is necessary, use either
getTemporaryNameProposal() or getProposal())
|
abstract ProgramVariable |
rename(ProgramVariable var,
Goal goal,
PosInOccurrence posOfFind)
intended to be called when symbolically executing a variable declaration;
resolves any naming conflicts between the new variable and other global
variables by renaming the new variable and / or other variables
|
static void |
setSuggestiveEnabled(boolean enabled) |
protected java.lang.Iterable<ProgramElementName> |
wrapGlobals(ImmutableList<? extends Named> globals)
creates a Globals object for use with other internal methods
|
protected java.lang.Iterable<ProgramElementName> |
wrapGlobals(ImmutableSet<ProgramVariable> globals)
creates a Globals object for use with other internal methods
|
private static final java.lang.String DEFAULT_BASENAME
private static final java.lang.String TEMPCOUNTER_NAME
private static boolean suggestive_off
protected final Services services
protected final java.util.HashMap<ProgramVariable,ProgramVariable> map
protected java.util.HashMap<ProgramVariable,ProgramVariable> renamingHistory
public VariableNamer(Services services)
services
- pointer to services objectprotected VariableNamer.BasenameAndIndex getBasenameAndIndex(ProgramElementName name)
public java.util.HashMap<ProgramVariable,ProgramVariable> getRenamingMap()
private Term findProgramInTerm(Term term)
protected ProgramElement getProgramFromPIO(PosInOccurrence pio)
protected ProgramElementName createName(java.lang.String basename, int index, NameCreationInfo creationInfo)
protected int getMaxCounterInGlobals(java.lang.String basename, java.lang.Iterable<ProgramElementName> globals)
protected int getMaxCounterInProgram(java.lang.String basename, ProgramElement program, PosInProgram posOfDeclaration)
protected boolean isUniqueInGlobals(java.lang.String name, java.lang.Iterable<ProgramElementName> globals)
protected boolean isUniqueInProgram(java.lang.String name, ProgramElement program, PosInProgram posOfDeclaration)
protected java.lang.Iterable<ProgramElementName> wrapGlobals(ImmutableList<? extends Named> globals)
protected java.lang.Iterable<ProgramElementName> wrapGlobals(ImmutableSet<ProgramVariable> globals)
public abstract ProgramVariable rename(ProgramVariable var, Goal goal, PosInOccurrence posOfFind)
var
- the new program variablegoal
- the goalposOfFind
- the PosInOccurrence of the currently executed programprivate java.lang.String getBaseNameProposal(Type type)
protected ProgramElementName getNameProposalForSchemaVariable(java.lang.String basename, SchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration, ImmutableList<java.lang.String> previousProposals)
basename
- desired base name, or null to use defaultsv
- the schema variableposOfFind
- the PosInOccurrence containing the name's target programposOfDeclaration
- the PosInProgram where the name will be declared
(or null to just be pessimistic about the scope)previousProposals
- list of names which should be considered taken,
or nullpublic ProgramElementName getTemporaryNameProposal(java.lang.String basename)
basename
- desired base name, or null to use defaultpublic java.lang.String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ImmutableList<java.lang.String> previousProposals)
getProposal
in interface InstantiationProposer
app
- the taclet appvar
- the schema variable to be instantiatedservices
- not usedundoAnchor
- not usedpreviousProposals
- list of names which should be considered taken,
or nullpublic boolean isUniqueNameForSchemaVariable(java.lang.String name, SchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration)
name
- the name to be checkedsv
- the schema variableposOfFind
- the PosInOccurrence of the name's target programposOfDeclaration
- the PosInProgram where the name will be declaredpublic static ProgramElementName parseName(java.lang.String name, NameCreationInfo creationInfo, Comment[] comments)
name
- the name as a stringcreationInfo
- optional name creation info the name should carrycomments
- any comments the name should carrypublic static ProgramElementName parseName(java.lang.String name, NameCreationInfo creationInfo)
public static ProgramElementName parseName(java.lang.String name, Comment[] comments)
public static ProgramElementName parseName(java.lang.String name)
public static void setSuggestiveEnabled(boolean enabled)
public java.lang.String getSuggestiveNameProposalForProgramVariable(SchemaVariable sv, TacletApp app, Services services, ImmutableList<java.lang.String> previousProposals)
public java.lang.String getSuggestiveNameProposalForSchemaVariable(Expression e)
private ProgramElement instantiateExpression(ProgramElement e, SVInstantiations svInst, Services services)