001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009:
010: package de.uka.ilkd.key.proof;
011:
012: import java.util.HashSet;
013: import java.util.regex.Matcher;
014: import java.util.regex.Pattern;
015:
016: import de.uka.ilkd.key.collection.ListOfString;
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.java.StatementBlock;
020: import de.uka.ilkd.key.java.visitor.LabelCollector;
021: import de.uka.ilkd.key.logic.Name;
022: import de.uka.ilkd.key.logic.NamespaceSet;
023: import de.uka.ilkd.key.logic.ProgramElementName;
024: import de.uka.ilkd.key.logic.Term;
025: import de.uka.ilkd.key.logic.op.SchemaVariable;
026: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
027: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
028: import de.uka.ilkd.key.rule.TacletApp;
029:
030: /**
031: * Proposes names for variables (except program variables).
032: */
033: public class VariableNameProposer implements InstantiationProposer {
034:
035: /**
036: * An instance of VariableNameProposer.
037: */
038: public static final VariableNameProposer DEFAULT = new VariableNameProposer();
039:
040: private static final String SKOLEMTERM_VARIABLE_NAME_POSTFIX = "_";
041: private static final String VARIABLE_NAME_PREFIX = "_var";
042: private static final String LABEL_NAME_PREFIX = "_label";
043:
044: private static final String GENERALNAMECOUNTER_PREFIX = "GenCnt";
045: private static final String SKOLEMTERMVARCOUNTER_PREFIX = "DepVarCnt";
046: private static final String VARCOUNTER_NAME = "VarCnt";
047: private static final String LABELCOUNTER_NAME = "LabelCnt";
048:
049: /**
050: * Returns an instantiation proposal for the schema variable var.
051: * Currently supports names for skolemterm SVs, variable SVs, and labels.
052: */
053: public String getProposal(TacletApp app, SchemaVariable var,
054: Services services, Node undoAnchor,
055: ListOfString previousProposals) {
056: if (var.isSkolemTermSV()) {
057: return getNameProposalForSkolemTermVariable(app, var,
058: services, undoAnchor, previousProposals);
059: } else if (var.isVariableSV()) {
060: return getNameProposalForVariableSV(app, var, services,
061: undoAnchor);
062: } else if (((SortedSchemaVariable) var).sort() == ProgramSVSort.LABEL) {
063: return getNameProposalForLabel(app, var, services,
064: undoAnchor, previousProposals);
065: } else {
066: return null;
067: }
068: }
069:
070: /**
071: * Generates a proposal for the instantiation of the given term
072: * schema variable, which is declared as skolem term SV.
073: */
074: private String getNameProposalForSkolemTermVariable(
075: TacletApp p_app, SchemaVariable p_var, Services services,
076: Node undoAnchor, ListOfString previousProposals) {
077: return getNameProposalForSkolemTermVariable(
078: createBaseNameProposalBasedOnCorrespondence(p_app,
079: p_var), services, undoAnchor, previousProposals);
080: }
081:
082: /**
083: * Find a name for the variable <code>p_var</code>, based on the result
084: * of <code>Taclet.getNameCorrespondent</code>
085: */
086: protected static String createBaseNameProposalBasedOnCorrespondence(
087: TacletApp p_app, SchemaVariable p_var) {
088: final String result;
089: final SchemaVariable v = p_app.taclet().getNameCorrespondent(
090: p_var);
091: if (v != null && p_app.instantiations().isInstantiated(v)) {
092:
093: final Object inst = p_app.instantiations()
094: .getInstantiation(v);
095:
096: if (inst instanceof Term) {
097: result = ((Term) inst).op().name().toString();
098: } else {
099: result = "" + inst;
100: }
101: } else {
102: // ... otherwise use the name of the SkolemTermSV
103: result = "" + p_var.name();
104: }
105:
106: // remove characters that should better not turn up in identifiers
107: // more or less a HACK
108: final Pattern pattern = Pattern.compile("[^_a-zA-Z0-9]");
109: final Matcher matcher = pattern.matcher(result);
110:
111: final Pattern doubledUnderScores = Pattern.compile("__");
112:
113: return doubledUnderScores.matcher(matcher.replaceAll("_"))
114: .replaceAll("");
115: }
116:
117: private String getNameProposalForSkolemTermVariable(String name,
118: Services services, Node undoAnchor,
119: ListOfString previousProposals) {
120:
121: final NamespaceSet nss = services.getNamespaces();
122: Name l_name;
123: final String basename = name + SKOLEMTERM_VARIABLE_NAME_POSTFIX;
124: do {
125: name = basename
126: + services.getCounter(
127: SKOLEMTERMVARCOUNTER_PREFIX + name)
128: .getCountPlusPlusWithParent(undoAnchor);
129: l_name = new Name(name);
130: } while (nss.lookup(l_name) != null
131: && !previousProposals.contains(name));
132:
133: return name;
134: }
135:
136: public String getNameProposal(String basename, Services services,
137: Node undoAnchor) {
138: final NamespaceSet nss = services.getNamespaces();
139: Name l_name;
140: String name = "";
141: do {
142: if (name.length() > 0) {
143: name = basename
144: + services.getCounter(
145: GENERALNAMECOUNTER_PREFIX + name)
146: .getCountPlusPlusWithParent(undoAnchor);
147: } else {
148: name = basename.length() > 0 ? basename : "gen";
149: }
150: l_name = new Name(name);
151: } while (nss.lookup(l_name) != null);
152:
153: return name;
154: }
155:
156: /**
157: * Generates a proposal for the instantiation of the given
158: * schema variable, which is a variable SV.
159: */
160: private String getNameProposalForVariableSV(TacletApp app,
161: SchemaVariable var, Services services, Node undoAnchor) {
162: return VARIABLE_NAME_PREFIX
163: + services.getCounter(VARCOUNTER_NAME)
164: .getCountPlusPlusWithParent(undoAnchor);
165: }
166:
167: /**
168: * Generates a proposal for the instantiation of the given
169: * schema variable, which is of sort label.
170: * @param previousProposals
171: */
172: private String getNameProposalForLabel(TacletApp app,
173: SchemaVariable var, Services services, Node undoAnchor,
174: ListOfString previousProposals) {
175:
176: ProgramElement contextProgram = app.matchConditions()
177: .getInstantiations().getContextInstantiation()
178: .contextProgram();
179:
180: if (contextProgram == null)
181: contextProgram = new StatementBlock();
182:
183: final LabelCollector lc = new LabelCollector(contextProgram,
184: new HashSet(10));
185:
186: lc.start();
187: String proposal;
188: do {
189: proposal = LABEL_NAME_PREFIX
190: + services.getCounter(LABELCOUNTER_NAME)
191: .getCountPlusPlusWithParent(undoAnchor);
192: } while (lc.contains(new ProgramElementName(proposal))
193: || previousProposals.contains(proposal));
194:
195: return proposal;
196: }
197: }
|