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: * Created on 01.02.2005
11: *
12: * TODO To change the template for this generated file go to
13: * Window - Preferences - Java - Code Style - Code Templates
14: */
15: package de.uka.ilkd.key.logic;
16:
17: import de.uka.ilkd.key.logic.op.Function;
18: import de.uka.ilkd.key.logic.op.Operator;
19:
20: /**
21: *
22: */
23: public class TermCreationException extends RuntimeException {
24:
25: private String errorMessage;
26:
27: public TermCreationException(String errorMessage) {
28: super (errorMessage);
29: this .errorMessage = errorMessage;
30: }
31:
32: public TermCreationException(Operator op, Term failed) {
33:
34: Term[] subs = new Term[failed.arity()];
35: for (int i = 0; i < subs.length; i++) {
36: subs[i] = failed.sub(i);
37: }
38:
39: errorMessage = "Building a term failed. Normally there is an arity mismatch "
40: + "or one of the subterms' sorts "
41: + "is not compatible (e.g. like the \'2\' in \"true & 2\")\n"
42: + "The top level operator was "
43: + op
44: + "(Sort: "
45: + op.sort(subs)
46: + ")"
47: + (op instanceof Function ? "; its expected arg sorts were:\n"
48: + argsToString((Function) op)
49: : "\n")
50: + "The subterms were:\n"
51: + subsToString(subs);
52: }
53:
54: public String getMessage() {
55: return errorMessage;
56: }
57:
58: private String argsToString(Function f) {
59: StringBuffer sb = new StringBuffer();
60: for (int i = 0; i < f.arity(); i++) {
61: sb.append((i + 1) + ".) ");
62: sb.append("sort: " + f.argSort(i) + ", sort hash: "
63: + f.argSort(i).hashCode() + "\n");
64: }
65: return sb.toString();
66: }
67:
68: private String subsToString(Term[] subs) {
69: StringBuffer sb = new StringBuffer();
70: for (int i = 0; i < subs.length; i++) {
71: sb.append((i + 1) + ".) ");
72: sb.append(subs[i]);
73: sb.append("(sort: " + subs[i].sort() + ", sort hash: "
74: + subs[i].sort().hashCode() + ")\n");
75:
76: }
77: return sb.toString();
78: }
79:
80: public String toString() {
81: return errorMessage;
82: }
83: }
|