de.uka.ilkd.key.proof

Class VariableNameProposer

java.lang.Object

de.uka.ilkd.key.proof.VariableNameProposer

All Implemented Interfaces:

InstantiationProposer

public class VariableNameProposer
extends java.lang.Object
implements InstantiationProposer

Proposes names for variables (except program variables).

Field Summary

Fields

Modifier and Type	Field and Description
static VariableNameProposer	DEFAULT An instance of VariableNameProposer.
private static java.lang.String	GENERALNAMECOUNTER_PREFIX
private static java.lang.String	LABEL_NAME_PREFIX
private static java.lang.String	LABELCOUNTER_NAME
private static java.lang.String	SKOLEMTERM_VARIABLE_NAME_POSTFIX
private static java.lang.String	SKOLEMTERMVARCOUNTER_PREFIX

Constructor Summary

Constructors

Constructor and Description
VariableNameProposer()

Method Summary

Modifier and Type	Method and Description
protected static java.lang.String	createBaseNameProposalBasedOnCorrespondence(TacletApp p_app, SchemaVariable p_var, Services services) Find a name for the variable p_var, based on the result of Taclet.getNameCorrespondent
java.lang.String	getNameProposal(java.lang.String basename, Services services, Node undoAnchor)
private java.lang.String	getNameProposalForLabel(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ImmutableList<java.lang.String> previousProposals) Generates a proposal for the instantiation of the given schema variable, which is of sort label.
private java.lang.String	getNameProposalForSkolemTermVariable(java.lang.String name, Services services, Node undoAnchor, ImmutableList<java.lang.String> previousProposals)
private java.lang.String	getNameProposalForSkolemTermVariable(TacletApp p_app, SchemaVariable p_var, Services services, Node undoAnchor, ImmutableList<java.lang.String> previousProposals) Generates a proposal for the instantiation of the given term schema variable, which is declared as skolem term SV.
private java.lang.String	getNameProposalForVariableSV(TacletApp app, SchemaVariable var, TermServices services, ImmutableList<java.lang.String> previousProposals) Generates a proposal for the instantiation of the given schema variable, which is a variable SV.
Name	getNewName(Services services, Name baseName) Warning: this method is buggy.
java.lang.String	getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ImmutableList<java.lang.String> previousProposals) Returns an instantiation proposal for the schema variable var.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

DEFAULT

public static final VariableNameProposer DEFAULT

An instance of VariableNameProposer.

SKOLEMTERM_VARIABLE_NAME_POSTFIX

private static final java.lang.String SKOLEMTERM_VARIABLE_NAME_POSTFIX

See Also:

Constant Field Values

LABEL_NAME_PREFIX

private static final java.lang.String LABEL_NAME_PREFIX

See Also:

Constant Field Values

GENERALNAMECOUNTER_PREFIX

private static final java.lang.String GENERALNAMECOUNTER_PREFIX

See Also:

Constant Field Values

SKOLEMTERMVARCOUNTER_PREFIX

private static final java.lang.String SKOLEMTERMVARCOUNTER_PREFIX

See Also:

Constant Field Values

LABELCOUNTER_NAME

private static final java.lang.String LABELCOUNTER_NAME

See Also:

Constant Field Values

Constructor Detail

VariableNameProposer

public VariableNameProposer()

Method Detail

getProposal

public java.lang.String getProposal(TacletApp app,
                                    SchemaVariable var,
                                    Services services,
                                    Node undoAnchor,
                                    ImmutableList<java.lang.String> previousProposals)

Returns an instantiation proposal for the schema variable var. Currently supports names for skolemterm SVs, variable SVs, and labels.

Specified by:

getProposal in interface InstantiationProposer

Parameters:

app - the taclet app

var - the schema variable to be instantiated

services - pointer to services object

undoAnchor - node to be used as undo anchor

previousProposals - a list of other proposals which should be taken into account (e.g. for name uniqueness), or null

getNewName

public Name getNewName(Services services,
                       Name baseName)

Warning: this method is buggy. It causes problems with proof reloading. Use the method TermBuilder.newName instead.

getNameProposalForSkolemTermVariable

private java.lang.String getNameProposalForSkolemTermVariable(TacletApp p_app,
                                                              SchemaVariable p_var,
                                                              Services services,
                                                              Node undoAnchor,
                                                              ImmutableList<java.lang.String> previousProposals)

Generates a proposal for the instantiation of the given term schema variable, which is declared as skolem term SV.

createBaseNameProposalBasedOnCorrespondence

protected static java.lang.String createBaseNameProposalBasedOnCorrespondence(TacletApp p_app,
                                                                              SchemaVariable p_var,
                                                                              Services services)

Find a name for the variable p_var, based on the result of Taclet.getNameCorrespondent

getNameProposalForSkolemTermVariable

private java.lang.String getNameProposalForSkolemTermVariable(java.lang.String name,
                                                              Services services,
                                                              Node undoAnchor,
                                                              ImmutableList<java.lang.String> previousProposals)

getNameProposal

public java.lang.String getNameProposal(java.lang.String basename,
                                        Services services,
                                        Node undoAnchor)

getNameProposalForVariableSV

private java.lang.String getNameProposalForVariableSV(TacletApp app,
                                                      SchemaVariable var,
                                                      TermServices services,
                                                      ImmutableList<java.lang.String> previousProposals)

Generates a proposal for the instantiation of the given schema variable, which is a variable SV. The returned name is not necessarily globally unique, but that is not necessary for bound variables.

getNameProposalForLabel

private java.lang.String getNameProposalForLabel(TacletApp app,
                                                 SchemaVariable var,
                                                 Services services,
                                                 Node undoAnchor,
                                                 ImmutableList<java.lang.String> previousProposals)

Generates a proposal for the instantiation of the given schema variable, which is of sort label.

Parameters:

previousProposals -