public abstract class VariableNamer extends Object implements InstantiationProposer
Modifier and Type | Class and Description |
---|---|
private static class |
VariableNamer.AdapterOfIteratorOfNamed
adapter from IteratorOfNamed to IteratorOfProgramElementName
|
private static class |
VariableNamer.AdapterOfIteratorOfProgramVariable
adapter from IteratorOfProgramVariable to IteratorOfProgramElementName
|
protected static class |
VariableNamer.BasenameAndIndex
tuple of a basename and an index
|
private static class |
VariableNamer.CustomJavaASTWalker
a customized JavaASTWalker
|
protected static interface |
VariableNamer.Globals
internal representation for global variables
|
private static class |
VariableNamer.GlobalsAsListOfNamed
wrapper for global variables coming as a ListOfNamed
|
private static class |
VariableNamer.GlobalsAsSetOfProgramVariable
wrapper for global variables coming as a SetOfProgramVariable
|
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 String |
DEFAULT_BASENAME
default basename for variable name proposals
|
protected HashMap<ProgramVariable,ProgramVariable> |
map |
protected HashMap<ProgramVariable,ProgramVariable> |
renamingHistory |
protected Services |
services
pointer to services object
|
private static boolean |
suggestive_off
status of suggestive name proposing
|
private static 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(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 String |
getBaseNameProposal(Type type)
proposes a base name for a given sort
|
protected int |
getMaxCounterInGlobals(String basename,
VariableNamer.Globals globals)
returns the maximum counter value already associated with the passed
basename in the passed list of global variables, or -1
|
protected int |
getMaxCounterInProgram(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(String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<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
|
String |
getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<String> previousProposals)
proposes a unique name for the instantiation of a schema variable
|
HashMap<ProgramVariable,ProgramVariable> |
getRenamingMap() |
String |
getSuggestiveNameProposalForProgramVariable(SchemaVariable sv,
TacletApp app,
Services services,
ImmutableList<String> previousProposals) |
String |
getSuggestiveNameProposalForSchemaVariable(Expression e) |
ProgramElementName |
getTemporaryNameProposal(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(String name,
VariableNamer.Globals globals)
tells whether a name is unique in the passed list of global variables
|
protected boolean |
isUniqueInProgram(String name,
ProgramElement program,
PosInProgram posOfDeclaration)
tells whether a name is unique in the passed program
|
boolean |
isUniqueNameForSchemaVariable(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(String name) |
static ProgramElementName |
parseName(String name,
Comment[] comments) |
static ProgramElementName |
parseName(String name,
NameCreationInfo creationInfo) |
static ProgramElementName |
parseName(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 VariableNamer.Globals |
wrapGlobals(ImmutableList<Named> globals)
creates a Globals object for use with other internal methods
|
protected VariableNamer.Globals |
wrapGlobals(ImmutableSet<ProgramVariable> globals)
creates a Globals object for use with other internal methods
|
private static final String DEFAULT_BASENAME
private static final String TEMPCOUNTER_NAME
private static boolean suggestive_off
protected final Services services
protected final HashMap<ProgramVariable,ProgramVariable> map
protected HashMap<ProgramVariable,ProgramVariable> renamingHistory
public VariableNamer(Services services)
services
- pointer to services objectprotected VariableNamer.BasenameAndIndex getBasenameAndIndex(ProgramElementName name)
public HashMap<ProgramVariable,ProgramVariable> getRenamingMap()
private Term findProgramInTerm(Term term)
protected ProgramElement getProgramFromPIO(PosInOccurrence pio)
protected ProgramElementName createName(String basename, int index, NameCreationInfo creationInfo)
protected int getMaxCounterInGlobals(String basename, VariableNamer.Globals globals)
protected int getMaxCounterInProgram(String basename, ProgramElement program, PosInProgram posOfDeclaration)
protected boolean isUniqueInGlobals(String name, VariableNamer.Globals globals)
protected boolean isUniqueInProgram(String name, ProgramElement program, PosInProgram posOfDeclaration)
protected VariableNamer.Globals wrapGlobals(ImmutableList<Named> globals)
protected VariableNamer.Globals 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 String getBaseNameProposal(Type type)
protected ProgramElementName getNameProposalForSchemaVariable(String basename, SchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration, ImmutableList<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(String basename)
basename
- desired base name, or null to use defaultpublic String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ImmutableList<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(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(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(String name, NameCreationInfo creationInfo)
public static ProgramElementName parseName(String name, Comment[] comments)
public static ProgramElementName parseName(String name)
public static void setSuggestiveEnabled(boolean enabled)
public String getSuggestiveNameProposalForProgramVariable(SchemaVariable sv, TacletApp app, Services services, ImmutableList<String> previousProposals)
public String getSuggestiveNameProposalForSchemaVariable(Expression e)
private ProgramElement instantiateExpression(ProgramElement e, SVInstantiations svInst, Services services)