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.proof.reuse;
012:
013: import java.util.List;
014:
015: import de.uka.ilkd.key.gui.KeYMediator;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.proof.Goal;
018: import de.uka.ilkd.key.rule.BuiltInRule;
019: import de.uka.ilkd.key.rule.BuiltInRuleApp;
020: import de.uka.ilkd.key.rule.RuleApp;
021:
022: public class ReuseUpdateSimplificationRule {
023:
024: private List reusePoints;
025: private KeYMediator medi;
026: private Constraint userC;
027:
028: public ReuseUpdateSimplificationRule(KeYMediator medi,
029: List reusePoints) {
030: this .medi = medi;
031: this .reusePoints = reusePoints;
032: userC = medi.getUserConstraint().getConstraint();
033: }
034:
035: public void applicableWhere(ReusePoint blank) {
036: Goal g = blank.target();
037: RuleApp templateApp = blank.getApp();
038:
039: IteratorOfConstrainedFormula formIter;
040:
041: final PosInOccurrence pio = templateApp.posInOccurrence();
042:
043: if (pio == null) {
044: final RuleApp tentativeApp = isApplicable(
045: (BuiltInRule) templateApp.rule(), blank.target(),
046: null);
047: if (tentativeApp != null) {
048: ReusePoint p = blank.initializeNoFind(tentativeApp,
049: medi);
050: if ((p != null)) { // RuleApp can be transferred // && goodEnough!
051: reusePoints.add(p);
052: }
053: }
054: return;
055: } else if (pio.isInAntec()) {
056: formIter = g.sequent().antecedent().iterator();
057: } else {
058: formIter = g.sequent().succedent().iterator();
059: }
060:
061: final boolean inAntec = pio.isInAntec();
062:
063: // but only if pos taclet
064: while (formIter.hasNext()) {
065: ConstrainedFormula cfma = formIter.next();
066: PosInOccurrence start = new PosInOccurrence(cfma,
067: PosInTerm.TOP_LEVEL, inAntec);
068: recMatch(start, cfma.formula(), (BuiltInRule) templateApp
069: .rule(), blank);
070: }
071: }
072:
073: private void recMatch(PosInOccurrence pos, Term t,
074: BuiltInRule rule, ReusePoint blank) {
075:
076: RuleApp tentativeApp = isApplicable(rule, blank.target(), pos);
077: if (tentativeApp != null) {
078: ReusePoint p = blank.initialize(pos, tentativeApp, medi);
079: if ((p != null)) { // RuleApp can be transferred // && goodEnough!
080: reusePoints.add(p);
081: }
082: }
083: // Succ- and Antec- are only applicable at top-level of formula
084: // if (!(rule instanceof RewriteTaclet)) return;
085: // does it make sense to do extra update simp on subformulas?
086: // let's suppose that it's not
087: /*
088: int i;
089: for (i=0; i<t.arity(); i++) {
090: recMatch(pos.down(i), t.sub(i), rule, blank);
091: }
092: */
093: }
094:
095: private RuleApp isApplicable(BuiltInRule rule, Goal g,
096: PosInOccurrence pos) {
097: if (!rule.isApplicable(g, pos, userC)) {
098: return null;
099: } else {
100: final RuleApp app = new BuiltInRuleApp(rule, pos, userC);
101: if (!g.proof().mgt().ruleApplicable(app, g)) {
102: return null;
103: }
104: return app;
105: }
106: }
107:
108: }
|