01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.gui;
12:
13: import org.apache.log4j.Logger;
14:
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.SchemaVariable;
17: import de.uka.ilkd.key.pp.AbbrevException;
18: import de.uka.ilkd.key.proof.ProofEvent;
19: import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
20: import de.uka.ilkd.key.rule.IteratorOfNewDependingOn;
21: import de.uka.ilkd.key.rule.RuleApp;
22: import de.uka.ilkd.key.rule.TacletApp;
23:
24: /**
25: * Listen for rule applications, add abbreviations of skolem functions
26: */
27: public class SkolemAbbreviator implements RuleAppListener {
28:
29: private KeYMediator mediator;
30:
31: public SkolemAbbreviator(KeYMediator p_mediator) {
32: mediator = p_mediator;
33:
34: mediator.addRuleAppListener(this );
35: }
36:
37: /** invoked when a rule has been applied */
38: public void ruleApplied(ProofEvent ev) {
39: RuleAppInfo rai = ev.getRuleAppInfo();
40:
41: if (rai == null)
42: return;
43:
44: RuleApp ruleApp = rai.getRuleApp();
45: if (ruleApp != null && ruleApp instanceof TacletApp) {
46: final TacletApp app = (TacletApp) ruleApp;
47: final IteratorOfNewDependingOn it = app.taclet()
48: .varsNewDependingOn();
49:
50: while (it.hasNext()) {
51: final SchemaVariable sv = it.next().first();
52: if (!sv.isSkolemTermSV())
53: continue;
54: final Term t = (Term) app.instantiations()
55: .getInstantiation(sv);
56:
57: assert t != null : "Instantiation missing, but should be there";
58:
59: if (t.op().arity() > 0)
60: addAbbreviation(t);
61: }
62: }
63: }
64:
65: private void addAbbreviation(Term p_t) {
66: try {
67: final String abbrev = p_t.op().name().toString();
68: mediator.getNotationInfo().getAbbrevMap().put(p_t, abbrev,
69: true);
70: } catch (AbbrevException e) {
71: final Logger logger = Logger
72: .getLogger(SkolemAbbreviator.class.getName());
73: logger.warn("Error occurred when trying to add "
74: + "abbreviation of skolem symbol:\n" + e);
75: }
76: }
77:
78: }
|