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;
012:
013: import java.io.FileOutputStream;
014: import java.io.IOException;
015: import java.io.PrintStream;
016: import java.util.Vector;
017:
018: import de.uka.ilkd.key.gui.KeYMediator;
019: import de.uka.ilkd.key.gui.Main;
020: import de.uka.ilkd.key.gui.configuration.ProofSettings;
021: import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent;
022: import de.uka.ilkd.key.java.ProgramElement;
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.EntryOfSchemaVariableAndInstantiationEntry;
026: import de.uka.ilkd.key.logic.op.IteratorOfEntryOfSchemaVariableAndInstantiationEntry;
027: import de.uka.ilkd.key.logic.op.SchemaVariable;
028: import de.uka.ilkd.key.pp.LogicPrinter;
029: import de.uka.ilkd.key.pp.NotationInfo;
030: import de.uka.ilkd.key.pp.PresentationFeatures;
031: import de.uka.ilkd.key.pp.ProgramPrinter;
032: import de.uka.ilkd.key.rule.*;
033: import de.uka.ilkd.key.rule.inst.*;
034:
035: /**
036: * Saves a proof and provides useful methods for pretty printing
037: * terms or programs.
038: */
039: public class ProofSaver {
040:
041: protected Main main;
042: protected KeYMediator mediator;
043: protected String filename;
044: protected Proof proof;
045: LogicPrinter printer;
046:
047: private ProofSaver() {
048: }
049:
050: public ProofSaver(Main main, String filename) {
051: this .main = main;
052: this .mediator = main.mediator();
053: this .filename = filename;
054: this .proof = mediator.getSelectedProof();
055: }
056:
057: public StringBuffer writeLog(Proof p) {
058: StringBuffer logstr = new StringBuffer();
059: //Advance the Logentries
060: if (p.userLog == null)
061: p.userLog = new Vector();
062: if (p.keyVersionLog == null)
063: p.keyVersionLog = new Vector();
064: p.userLog.add(System.getProperty("user.name"));
065: p.keyVersionLog.add(Main.getInstance().getPrcsVersion());
066: int s = p.userLog.size();
067: for (int i = 0; i < s; i++) {
068: logstr.append("(keyLog \"" + i + "\" (keyUser \""
069: + p.userLog.elementAt(i) + "\" ) (keyVersion \""
070: + p.keyVersionLog.elementAt(i) + "\"))\n");
071: }
072: return logstr;
073: }
074:
075: public String writeSettings(ProofSettings ps) {
076: return new String("\\settings {\n\"" + ps.settingsToString()
077: + "\"\n}\n");
078: }
079:
080: public String save() {
081: String errorMsg = null;
082: FileOutputStream fos = null;
083: PrintStream ps = null;
084:
085: try {
086: fos = new FileOutputStream(filename);
087: ps = new PrintStream(fos);
088:
089: Sequent problemSeq = proof.root().sequent();
090: printer = createLogicPrinter(proof.getServices(), false);
091:
092: ps.println(writeSettings(proof.getSettings()));
093: ps.print(proof.header());
094: ps.println("\\problem {");
095: printer.printSemisequent(problemSeq.succedent());
096: ps.println(printer.result());
097: ps.println("}\n");
098: // ps.println(mediator.sort_ns());
099: ps.println("\\proof {");
100: ps.println(writeLog(proof));
101: ps.println(node2Proof(proof.root()));
102: ps.println("}");
103:
104: } catch (IOException ioe) {
105: errorMsg = "Could not save \n" + filename + ".\n";
106: errorMsg += ioe.toString();
107: } catch (NullPointerException npe) {
108: errorMsg = "Could not save \n" + filename + "\n";
109: errorMsg += "No proof present?";
110: npe.printStackTrace();
111: } catch (Exception e) {
112: errorMsg = e.toString();
113: e.printStackTrace();
114: } finally {
115: try {
116: if (fos != null)
117: fos.close();
118: } catch (IOException ioe) {
119: mediator
120: .notify(new GeneralFailureEvent(ioe.toString()));
121: }
122: }
123: return errorMsg; // null if success
124: }
125:
126: private void printSingleNode(Node node, String prefix,
127: StringBuffer tree) {
128:
129: RuleApp appliedRuleApp = node.getAppliedRuleApp();
130: if (appliedRuleApp == null && (proof.getGoal(node) != null)) { // open goal
131: tree.append(prefix);
132: tree.append("(opengoal \"");
133: LogicPrinter logicPrinter = createLogicPrinter(proof
134: .getServices(), false);
135:
136: logicPrinter.printSequent(node.sequent());
137: // WATCHOUT Woj: replaceAll... is necessary for the newly introduced backslash
138: // notation in the parser
139: tree.append(printer.result().toString().replace('\n', ' ')
140: .replaceAll("\\\\", "\\\\\\\\"));
141: tree.append("\")\n");
142: return;
143: }
144:
145: if (appliedRuleApp instanceof TacletApp) {
146: tree.append(prefix);
147: tree.append("(rule \"");
148: tree.append(appliedRuleApp.rule().name());
149: tree.append("\"");
150: tree.append(posInOccurrence2Proof(node.sequent(),
151: appliedRuleApp.posInOccurrence()));
152: tree.append(getInteresting(((TacletApp) appliedRuleApp)
153: .instantiations()));
154: ListOfIfFormulaInstantiation l = ((TacletApp) appliedRuleApp)
155: .ifFormulaInstantiations();
156: if (l != null)
157: tree.append(ifFormulaInsts(node, l));
158: tree.append("");
159: userInteraction2Proof(node, tree);
160: tree.append(")\n");
161: }
162:
163: if (appliedRuleApp instanceof BuiltInRuleApp) {
164: tree.append(prefix);
165: tree.append("(builtin \"");
166: tree.append(appliedRuleApp.rule().name().toString());
167: tree.append("\"");
168: tree.append(posInOccurrence2Proof(node.sequent(),
169: appliedRuleApp.posInOccurrence()));
170: if (appliedRuleApp instanceof MethodContractRuleApp) {
171: tree.append(" (contract \"");
172: tree.append(((MethodContractRuleApp) appliedRuleApp)
173: .getMethodContract().getName());
174: tree.append("\")");
175: }
176: tree.append(")\n");
177: }
178: }
179:
180: private StringBuffer collectProof(Node node, String prefix,
181: StringBuffer tree) {
182:
183: printSingleNode(node, prefix, tree);
184: IteratorOfNode childrenIt = null;
185:
186: while (node.childrenCount() == 1) {
187: childrenIt = node.childrenIterator();
188: node = childrenIt.next();
189: printSingleNode(node, prefix, tree);
190: }
191:
192: if (node.childrenCount() == 0)
193: return tree;
194:
195: childrenIt = node.childrenIterator();
196:
197: while (childrenIt.hasNext()) {
198: Node child = childrenIt.next();
199: tree.append(prefix);
200: tree.append("(branch \" "
201: + child.getNodeInfo().getBranchLabel().replaceAll(
202: "\\\\", "\\\\\\\\") + "\"\n");
203: collectProof(child, prefix + " ", tree);
204: tree.append(prefix + ")\n");
205: }
206:
207: return tree;
208: }
209:
210: private void userInteraction2Proof(Node node, StringBuffer tree) {
211: if (node.getNodeInfo().getInteractiveRuleApplication())
212: tree.append(" (userinteraction)");
213: }
214:
215: public String node2Proof(Node node) {
216: StringBuffer tree = new StringBuffer();
217: String s = "(branch \"dummy ID\"\n"
218: + collectProof(node, "", tree) + ")\n";
219: return s;
220: }
221:
222: public String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos) {
223: if (pos == null)
224: return "";
225: return " (formula \""
226: + seq.formulaNumberInSequent(pos.isInAntec(), pos
227: .constrainedFormula()) + "\")"
228: + posInTerm2Proof(pos.posInTerm());
229: }
230:
231: public String posInTerm2Proof(PosInTerm pos) {
232: if (pos == PosInTerm.TOP_LEVEL)
233: return "";
234: String s = " (term \"";
235: String list = pos.integerList(pos.reverseIterator()); // cheaper to read in
236: s = s + list.substring(1, list.length() - 1); // chop off "[" and "]"
237: s = s + "\")";
238: return s;
239: }
240:
241: public String getInteresting(SVInstantiations inst) {
242: //System.err.println(inst);
243: String s = "";
244: IteratorOfEntryOfSchemaVariableAndInstantiationEntry pairIt = inst
245: .interesting().entryIterator();
246:
247: while (pairIt.hasNext()) {
248: EntryOfSchemaVariableAndInstantiationEntry pair = pairIt
249: .next();
250: SchemaVariable var = pair.key();
251: s += " (inst \"" + var.name() + "=";
252: Object value = pair.value();
253: if (value instanceof TermInstantiation) {
254: s += printTerm(((TermInstantiation) value).getTerm(),
255: proof.getServices());
256: } else if (value instanceof ProgramInstantiation) {
257: ProgramElement pe = ((ProgramInstantiation) value)
258: .getProgramElement();
259: s += printProgramElement(pe);
260: } else if (value instanceof NameInstantiationEntry) {
261: s += ((NameInstantiationEntry) value)
262: .getInstantiation();
263: } else if (value instanceof ListInstantiation) {
264: ListOfObject l = (ListOfObject) ((ListInstantiation) value)
265: .getInstantiation();
266: s += printListInstantiation(l, proof.getServices());
267: } else
268: throw new RuntimeException("Saving failed.\n"
269: + "FIXME: Unhandled instantiation type: "
270: + value.getClass());
271: s += "\")";
272: }
273: // WATCHOUT: Woj: again, quote backslashes
274: s = s.replaceAll("\\\\", "\\\\\\\\");
275: return s;
276: }
277:
278: public static String printListInstantiation(ListOfObject l,
279: Services serv) {
280: final StringBuffer sb = new StringBuffer("{");
281: final IteratorOfObject it = l.iterator();
282: while (it.hasNext()) {
283: final Object next = it.next();
284: if (next instanceof LocationDescriptor) {
285: sb.append(printLocationDescriptor(
286: (LocationDescriptor) next, serv));
287: } else {
288: throw new RuntimeException("Unexpected entry in "
289: + "ListInstantiation");
290: }
291: if (it.hasNext())
292: sb.append(",");
293: }
294: sb.append("}");
295: return sb.toString();
296: }
297:
298: public String ifFormulaInsts(Node node,
299: ListOfIfFormulaInstantiation l) {
300: String s = "";
301: IteratorOfIfFormulaInstantiation it = l.iterator();
302: while (it.hasNext()) {
303: IfFormulaInstantiation iff = it.next();
304: if (iff instanceof IfFormulaInstSeq) {
305: ConstrainedFormula f = iff.getConstrainedFormula();
306: s += " (ifseqformula \""
307: + node.sequent().formulaNumberInSequent(
308: ((IfFormulaInstSeq) iff).inAntec(), f)
309: + "\")";
310: } else if (iff instanceof IfFormulaInstDirect) {
311: throw new RuntimeException(
312: "IfFormulaInstDirect not yet supported");
313: } else
314: throw new RuntimeException(
315: "Unknown If-Seq-Formula type");
316: }
317: return s;
318: }
319:
320: public static String printProgramElement(ProgramElement pe) {
321: java.io.StringWriter sw = new java.io.StringWriter();
322: ProgramPrinter prgPrinter = new ProgramPrinter(sw);
323: try {
324: pe.prettyPrint(prgPrinter);
325: } catch (IOException ioe) {
326: System.err.println(ioe);
327: }
328: return sw.toString();
329: }
330:
331: public static StringBuffer printTerm(Term t, Services serv) {
332: return printTerm(t, serv, false);
333: }
334:
335: public static StringBuffer printTerm(Term t, Services serv,
336: boolean shortAttrNotation) {
337: StringBuffer result;
338: LogicPrinter logicPrinter = createLogicPrinter(serv,
339: shortAttrNotation);
340: try {
341: logicPrinter.printTerm(t);
342: } catch (IOException ioe) {
343: System.err.println(ioe);
344: }
345: result = logicPrinter.result();
346: if (result.charAt(result.length() - 1) == '\n')
347: result.deleteCharAt(result.length() - 1);
348: return result;
349: }
350:
351: public static StringBuffer printLocationDescriptor(
352: LocationDescriptor loc, Services serv) {
353: StringBuffer result;
354: LogicPrinter logicPrinter = createLogicPrinter(serv, false);
355: try {
356: logicPrinter.printLocationDescriptor(loc);
357: } catch (IOException ioe) {
358: System.err.println(ioe);
359: }
360: result = logicPrinter.result();
361: if (result.charAt(result.length() - 1) == '\n')
362: result.deleteCharAt(result.length() - 1);
363: return result;
364: }
365:
366: public static String printAnything(Object val, Services services) {
367: if (val instanceof ProgramElement) {
368: return printProgramElement((ProgramElement) val);
369: } else if (val instanceof Term) {
370: return printTerm((Term) val, services, true).toString();
371: } else if (val == null) {
372: return null;
373: } else {
374: System.err.println("Don't know how to prettyprint "
375: + val.getClass());
376: // try to String by chance
377: return val.toString();
378: }
379: }
380:
381: private static LogicPrinter createLogicPrinter(Services serv,
382: boolean shortAttrNotation) {
383:
384: NotationInfo ni = NotationInfo.createInstance();
385: LogicPrinter p = null;
386:
387: if (serv != null) {
388: PresentationFeatures.modifyNotationInfo(ni, serv
389: .getNamespaces().functions());
390: }
391: p = new LogicPrinter(new ProgramPrinter(null), ni,
392: (shortAttrNotation ? serv : null), true);
393: return p;
394: }
395:
396: }
|