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.rule.soundness;
12:
13: import de.uka.ilkd.key.logic.op.SchemaVariable;
14:
15: /**
16: * Immutable
17: */
18: public class SVTypeInfos {
19:
20: public static final SVTypeInfos EMPTY_SVTYPEINFOS = new SVTypeInfos(
21: SLListOfSVTypeInfo.EMPTY_LIST);
22:
23: private ListOfSVTypeInfo infos;
24:
25: private SVTypeInfos(ListOfSVTypeInfo p_infos) {
26: infos = p_infos;
27: }
28:
29: public SVTypeInfos addInfo(SVTypeInfo p) {
30: SVTypeInfo old = getInfo(p.getSV());
31:
32: if (old != null) {
33: if (old.equals(p))
34: return this ;
35: else
36: throw new InvalidPrefixException(
37: "Invalid types given for schema variable (perhaps TODO)");
38: }
39:
40: return new SVTypeInfos(infos.prepend(p));
41: }
42:
43: public SVTypeInfo getInfo(SchemaVariable p) {
44: IteratorOfSVTypeInfo it = infos.iterator();
45: SVTypeInfo info;
46:
47: while (it.hasNext()) {
48: info = it.next();
49: if (info.getSV() == p)
50: return info;
51: }
52:
53: return null;
54: }
55:
56: public String toString() {
57: return "" + infos;
58: }
59: }
|