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:
011: package de.uka.ilkd.key.strategy.feature.instantiator;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
017: import de.uka.ilkd.key.logic.op.SchemaVariable;
018: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
019: import de.uka.ilkd.key.proof.Goal;
020: import de.uka.ilkd.key.rule.RuleApp;
021: import de.uka.ilkd.key.rule.TacletApp;
022: import de.uka.ilkd.key.strategy.LongRuleAppCost;
023: import de.uka.ilkd.key.strategy.RuleAppCost;
024: import de.uka.ilkd.key.strategy.feature.Feature;
025: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
026: import de.uka.ilkd.key.util.Debug;
027:
028: /**
029: * Feature representing a <code>ChoicePoint</code> for instantiating a schema
030: * variable of a taclet with the term that is returned by a
031: * <code>ProjectionToTerm</code>. This feature is useful in particular
032: * combined with <code>ForEachCP</code>. Although the feature formally is a
033: * choice point, it will always have exactly one branch
034: */
035: public class SVInstantiationCP implements Feature {
036:
037: private final BackTrackingManager manager;
038:
039: private final Name svToInstantiate;
040: private final ProjectionToTerm value;
041:
042: public static Feature create(Name svToInstantiate,
043: ProjectionToTerm value, BackTrackingManager manager) {
044: return new SVInstantiationCP(svToInstantiate, value, manager);
045: }
046:
047: private SVInstantiationCP(Name svToInstantiate,
048: ProjectionToTerm value, BackTrackingManager manager) {
049: this .svToInstantiate = svToInstantiate;
050: this .value = value;
051: this .manager = manager;
052: }
053:
054: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
055: Goal goal) {
056: manager.passChoicePoint(new CP(app, pos, goal), this );
057: return LongRuleAppCost.ZERO_COST;
058: }
059:
060: private SchemaVariable findSVWithName(TacletApp app) {
061: final SetOfSchemaVariable vars = app.uninstantiatedVars();
062: final IteratorOfSchemaVariable it = vars.iterator();
063: while (it.hasNext()) {
064: final SchemaVariable svt = it.next();
065: if (svt.name().equals(svToInstantiate))
066: return svt;
067: }
068:
069: Debug
070: .fail("Did not find schema variable "
071: + svToInstantiate
072: + " that I was supposed to instantiate\n"
073: + "(taclet "
074: + app.taclet().name()
075: + ")\n"
076: + "Either the name of the variable is wrong, or the variable\n"
077: + "has already been instantiated.");
078: return null;
079: }
080:
081: private class CP implements ChoicePoint {
082:
083: private final PosInOccurrence pos;
084: private final RuleApp app;
085: private final Goal goal;
086:
087: private CP(RuleApp app, PosInOccurrence pos, Goal goal) {
088: this .pos = pos;
089: this .app = app;
090: this .goal = goal;
091: }
092:
093: public IteratorOfCPBranch getBranches(RuleApp oldApp) {
094: if (!(oldApp instanceof TacletApp))
095: Debug
096: .fail("Instantiation feature is only applicable to "
097: + "taclet apps, but got " + oldApp);
098: final TacletApp tapp = (TacletApp) oldApp;
099:
100: final SchemaVariable sv = findSVWithName(tapp);
101: final Term instTerm = value.toTerm(app, pos, goal);
102:
103: final RuleApp newApp = tapp.addCheckedInstantiation(sv,
104: instTerm, goal.proof().getServices(), true);
105:
106: final CPBranch branch = new CPBranch() {
107: public void choose() {
108: }
109:
110: public RuleApp getRuleAppForBranch() {
111: return newApp;
112: }
113: };
114:
115: return SLListOfCPBranch.EMPTY_LIST.prepend(branch)
116: .iterator();
117: }
118:
119: }
120: }
|