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.java.Services;
017: import de.uka.ilkd.key.logic.*;
018: import de.uka.ilkd.key.proof.Goal;
019: import de.uka.ilkd.key.proof.init.InitConfig;
020: import de.uka.ilkd.key.rule.*;
021:
022: public class ReuseFindTaclet {
023:
024: private List reusePoints;
025: private KeYMediator medi;
026: private Services services;
027: private Constraint userC;
028: private InitConfig iconfig;
029:
030: public ReuseFindTaclet(KeYMediator medi, List reusePoints) {
031: this .medi = medi;
032: this .reusePoints = reusePoints;
033: services = medi.getServices();
034: userC = medi.getUserConstraint().getConstraint();
035: iconfig = medi.getProof().env().getInitConfig();
036: }
037:
038: public void applicableWhere(ReusePoint blank) {
039: Goal g = blank.target();
040: RuleApp templateApp = blank.getApp();
041:
042: final boolean inAntec = templateApp.posInOccurrence()
043: .isInAntec();
044:
045: final IteratorOfConstrainedFormula formIter;
046:
047: if (inAntec) {
048: formIter = g.sequent().antecedent().iterator();
049: } else {
050: formIter = g.sequent().succedent().iterator();
051: }
052:
053: Rule rule = iconfig.lookupActiveTaclet(templateApp.rule()
054: .name());
055: if (rule == null) { // goal local rule
056: rule = g.indexOfTaclets().lookup(templateApp.rule().name())
057: .rule();
058: blank.setGoalLocal(true);
059: }
060:
061: // but only if pos taclet
062: while (formIter.hasNext()) {
063: final ConstrainedFormula cfma = formIter.next();
064: final PosInOccurrence start = new PosInOccurrence(cfma,
065: PosInTerm.TOP_LEVEL, inAntec);
066: recMatch(start, cfma.formula(), rule, blank);
067: }
068: }
069:
070: private void recMatch(PosInOccurrence pos, Term t, Rule rule,
071: ReusePoint blank) {
072:
073: final TacletApp tentativeApp = isApplicable(rule, pos, t);
074: if (tentativeApp != null) {
075: checkIfInstsAndRecord(blank, pos, tentativeApp);
076: }
077: // Succ- and Antec- are only applicable at top-level of formula
078: if (!(rule instanceof RewriteTaclet))
079: return;
080: for (int i = 0, arity = t.arity(); i < arity; i++) {
081: recMatch(pos.down(i), t.sub(i), rule, blank);
082: }
083: }
084:
085: private void checkIfInstsAndRecord(ReusePoint blank,
086: PosInOccurrence pos, TacletApp tentativeApp) {
087:
088: final ListOfTacletApp ifCandidates;
089: if (!tentativeApp.ifInstsComplete()) {
090: ifCandidates = tentativeApp.findIfFormulaInstantiations(
091: blank.target().sequent(), services, userC);
092: } else {
093: ifCandidates = SLListOfTacletApp.EMPTY_LIST
094: .prepend(tentativeApp);
095: }
096:
097: final IteratorOfTacletApp it = ifCandidates.iterator();
098: while (it.hasNext()) {
099: final ReusePoint p = blank.initialize(pos, it.next(), medi);
100: if ((p != null)) { // RuleApp can be transferred // && goodEnough!
101: reusePoints.add(p);
102: }
103: }
104: }
105:
106: private TacletApp isApplicable(Rule rule, PosInOccurrence pos,
107: Term t) {
108: if (rule instanceof FindTaclet) {
109: //this is copied from TermTacletAppIndex :-/
110: Constraint c = pos.constrainedFormula().constraint();
111: if (pos.termBelowMetavariable() != null) {
112: c = c.unify(pos.constrainedFormula().formula().subAt(
113: pos.posInTerm()), pos.termBelowMetavariable(),
114: services);
115: if (!c.isSatisfiable())
116: return null;
117: }
118:
119: NoPosTacletApp app = NoPosTacletApp
120: .createNoPosTacletApp((FindTaclet) rule);
121: app = app.matchFind(pos, c, services, userC, t);
122: if (app == null)
123: return null;
124:
125: return app.setPosInOccurrence(pos);
126:
127: } else
128: throw new RuntimeException(
129: "Not a FindTaclet: Re-Use Failed " + rule);
130:
131: }
132:
133: }
|