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.mgt;
012:
013: import java.util.*;
014:
015: import javax.swing.JOptionPane;
016:
017: import org.apache.log4j.Logger;
018:
019: import de.uka.ilkd.key.gui.KeYMediator;
020: import de.uka.ilkd.key.gui.Main;
021: import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent;
022: import de.uka.ilkd.key.proof.*;
023: import de.uka.ilkd.key.proof.reuse.ReuseFrontend;
024:
025: public class GlobalProofMgt {
026:
027: private static final GlobalProofMgt INSTANCE = new GlobalProofMgt();
028:
029: private Map envKeyToEnv = new HashMap();
030:
031: private KeYMediator mediator;
032:
033: private Logger mgtLogger = Logger.getLogger("key.proof.mgt");
034:
035: public static GlobalProofMgt getInstance() {
036: return INSTANCE;
037: }
038:
039: public void setMediator(KeYMediator m) {
040: mediator = m;
041: }
042:
043: public ProofEnvironment getProofEnvironment(JavaModel jmodel,
044: RuleConfig ruleConfig, boolean askUser) {
045: if (jmodel == null) {
046: return null;
047: }
048: List setOfEnv = (List) envKeyToEnv.get(new EnvKey(jmodel,
049: ruleConfig));
050: if (setOfEnv == null || setOfEnv.size() == 0) {
051: return null;
052: } else if (!askUser && setOfEnv.size() > 0) {
053: return (ProofEnvironment) setOfEnv.get(0);
054: } else {
055: Object[] choice = new Object[setOfEnv.size() + 1];
056: System.arraycopy(setOfEnv.toArray(), 0, choice, 1, setOfEnv
057: .size());
058: choice[0] = "Open in new environment";
059: Object o = (JOptionPane
060: .showInputDialog(
061: mediator.mainFrame(),
062: "Java model and rule sets are suitable "
063: + "to already existing environment(s). \n"
064: + "Please select one or choose to open the problem "
065: + "in a new environment.\n"
066: + "Attention: Unless you open the problem in a "
067: + "new environment,\n"
068: + "sort, function, and rule declarations are ignored.",
069: "Proof Environment",
070: JOptionPane.QUESTION_MESSAGE, null, choice,
071: null));
072: if (o instanceof ProofEnvironment) {
073: return (ProofEnvironment) o;
074: } else {
075: return null;
076: }
077: }
078: }
079:
080: public void registerProofEnvironment(ProofEnvironment env) {
081: EnvKey envKey = new EnvKey(env.getJavaModel(), env
082: .getRuleConfig());
083: List listOfEnv = (List) envKeyToEnv.get(envKey);
084: if (listOfEnv == null) {
085: listOfEnv = new LinkedList();
086: envKeyToEnv.put(envKey, listOfEnv);
087: }
088: listOfEnv.add(env);
089: env.setNumber(listOfEnv.size());
090: }
091:
092: public void tryReuse(ProofAggregate plist) {
093: int size = plist.size();
094: for (int i = 0; i < size; i++) {
095: tryReuse(plist.getProofs()[i]);
096: }
097: }
098:
099: public void tryReuse(Proof proof) {
100: Proof[] prevs = lookupPrevious(proof);
101: if (prevs.length > 0 && !Main.testStandalone) {
102: String[] prevNames = new String[prevs.length];
103: for (int i = 0; i < prevNames.length; i++) {
104: prevNames[i] = "From " + prevs[i].env().description();
105: }
106: String pname = (String) JOptionPane
107: .showInputDialog(
108: mediator.mainFrame(),
109: "Found previous proofs for this PO in "
110: + proof.env().description()
111: + "\n"
112: + "Mark up for re-use? (previous marks will be lost)",
113: "Re-Use", JOptionPane.QUESTION_MESSAGE,
114: null, prevNames, null);
115:
116: if (pname != null) {
117: int i = 0;
118: while (!pname.equals(prevNames[i]))
119: i++;
120: tryReuse(proof, prevs[i]);
121: }
122: }
123: }
124:
125: public void tryReuse(Proof proof, Proof prev) {
126: String error = null;
127: CvsRunner cvs = new CvsRunner();
128: String diff;
129: Node.clearReuseCandidates();
130: ReuseFrontend f = new ReuseFrontend(mediator);
131: if (!proof.getJavaModel().isEmpty()) {
132: try {
133: diff = cvs.cvsDiff(proof.getJavaModel().getCVSModule(), //XXX: check equality
134: prev.getJavaModel().getModelTag(), proof
135: .getJavaModel().getModelTag());
136: error = f.markup(prev, diff);
137: } catch (CvsException cvse) {
138: mgtLogger
139: .error("Diffing models in CVS failed: " + cvse);
140: }
141: } else
142: f.markRoot(prev);
143:
144: if (error != null) {
145: mediator.notify(new GeneralFailureEvent(error));
146: }
147: }
148:
149: private Proof[] lookupPrevious(Proof p) {
150: List result = new LinkedList();
151: Iterator it = envKeyToEnv.values().iterator();
152: while (it.hasNext()) {
153: List envList = (List) it.next();
154: Iterator envIt = envList.iterator();
155: while (envIt.hasNext()) {
156: ProofEnvironment env = (ProofEnvironment) envIt.next();
157: Iterator proofListIt = env.getProofs().iterator();
158: while (proofListIt.hasNext()) {
159: ProofAggregate pl = (ProofAggregate) proofListIt
160: .next();
161: Proof[] proofs = pl.getProofs();
162: for (int i = 0; i < proofs.length; i++) {
163: if (p != proofs[i]
164: && p.mgt().proofSimilarTo(proofs[i])) {
165: result.add(proofs[i]);
166: }
167: }
168: }
169: }
170: }
171: return (Proof[]) result.toArray(new Proof[0]);
172: }
173:
174: public void removeEnv(ProofEnvironment env) {
175: Set entries = envKeyToEnv.entrySet();
176: Iterator it = entries.iterator();
177: while (it.hasNext()) {
178: Map.Entry entry = (Map.Entry) it.next();
179: List l = (List) entry.getValue();
180: Iterator listIt = l.iterator();
181: while (listIt.hasNext()) {
182: if (listIt.next().equals(env))
183: listIt.remove();
184: }
185: }
186: }
187:
188: static class EnvKey {
189: private JavaModel jModel;
190: private RuleConfig ruleConfig;
191: private int number;
192:
193: public EnvKey(JavaModel jModel, RuleConfig ruleConfig,
194: int number) {
195: this .jModel = jModel;
196: this .ruleConfig = ruleConfig;
197: this .number = number;
198: }
199:
200: public EnvKey(JavaModel jModel, RuleConfig ruleConfig) {
201: this (jModel, ruleConfig, 0);
202: }
203:
204: public JavaModel getJavaModel() {
205: return jModel;
206: }
207:
208: public RuleConfig getRuleConfig() {
209: return ruleConfig;
210: }
211:
212: public int getNumber() {
213: return number;
214: }
215:
216: public boolean equals(Object o) {
217: if (!(o instanceof EnvKey))
218: return false;
219: EnvKey e = (EnvKey) o;
220: return e.getJavaModel().equals(getJavaModel())
221: && e.getRuleConfig().equals(getRuleConfig());
222: }
223:
224: public int hashCode() {
225: int result = 17;
226: result = 37 * result + getJavaModel().hashCode();
227: result = 37 * result + getRuleConfig().hashCode();
228: return result;
229: }
230: }
231:
232: }
|