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.logic;
012:
013: public class NamespaceSet {
014:
015: private Namespace varNS = new Namespace();
016: private Namespace progVarNS = new Namespace();
017: private Namespace funcNS = new Namespace();
018: private Namespace ruleSetNS = new Namespace();
019: private Namespace sortNS = new Namespace();
020: private Namespace choiceNS = new Namespace();
021:
022: public NamespaceSet() {
023: }
024:
025: public NamespaceSet(Namespace varNS, Namespace funcNS,
026: Namespace sortNS, Namespace ruleSetNS, Namespace choiceNS,
027: Namespace programVarNS) {
028: this .varNS = varNS;
029: this .progVarNS = programVarNS;
030: this .funcNS = funcNS;
031: this .sortNS = sortNS;
032: this .ruleSetNS = ruleSetNS;
033: this .choiceNS = choiceNS;
034: }
035:
036: public Namespace variables() {
037: return varNS;
038: }
039:
040: public void setVariables(Namespace varNS) {
041: this .varNS = varNS;
042: }
043:
044: public Namespace programVariables() {
045: return progVarNS;
046: }
047:
048: public void setProgramVariables(Namespace progVarNS) {
049: this .progVarNS = progVarNS;
050: }
051:
052: public Namespace functions() {
053: return funcNS;
054: }
055:
056: public void setFunctions(Namespace funcNS) {
057: this .funcNS = funcNS;
058: }
059:
060: public Namespace ruleSets() {
061: return ruleSetNS;
062: }
063:
064: public void setRuleSets(Namespace ruleSetNS) {
065: this .ruleSetNS = ruleSetNS;
066: }
067:
068: public Namespace sorts() {
069: return sortNS;
070: }
071:
072: public void setSorts(Namespace sortNS) {
073: this .sortNS = sortNS;
074: }
075:
076: public Namespace choices() {
077: return choiceNS;
078: }
079:
080: public void setChoices(Namespace choiceNS) {
081: this .choiceNS = choiceNS;
082: }
083:
084: public void add(NamespaceSet ns) {
085: variables().add(ns.variables());
086: programVariables().add(ns.programVariables());
087: sorts().add(ns.sorts());
088: ruleSets().add(ns.ruleSets());
089: functions().add(ns.functions());
090: choices().add(ns.choices());
091: }
092:
093: public NamespaceSet copy() {
094: NamespaceSet c = new NamespaceSet();
095: c.setSorts(sorts().copy());
096: c.setRuleSets(ruleSets().copy());
097: c.setFunctions(functions().copy());
098: c.setVariables(variables().copy());
099: c.setProgramVariables(programVariables().copy());
100: c.setChoices(choices().copy());
101: return c;
102: }
103:
104: /**
105: * starts the protocol of all contained namespaces
106: */
107: public void startProtocol() {
108: variables().startProtocol();
109: programVariables().startProtocol();
110: sorts().startProtocol();
111: ruleSets().startProtocol();
112: functions().startProtocol();
113: choices().startProtocol();
114: }
115:
116: /**
117: * returns all namespaces in an array
118: */
119: private Namespace[] asArray() {
120: return new Namespace[] { variables(), programVariables(),
121: sorts(), ruleSets(), functions(), choices() };
122: }
123:
124: /**
125: * returns all namespaces with symbols that may occur
126: * in a real sequent (this means all namespaces without
127: * variables, choices and ruleSets)
128: */
129: private Namespace[] logicAsArray() {
130: return new Namespace[] { programVariables(), sorts(),
131: functions() };
132: }
133:
134: /**
135: * adds the protocolled names of the given NamespaceSet to this one
136: */
137: public void addProtocolled(NamespaceSet nss) {
138: final Namespace[] myNames = asArray();
139: final Namespace[] otherNames = nss.asArray();
140: for (int i = 0; i < myNames.length; i++) {
141: final IteratorOfNamed it = otherNames[i].getProtocolled();
142: while (it.hasNext()) {
143: myNames[i].add(it.next());
144: }
145: }
146: }
147:
148: /**
149: * looks up if the given name is found in one of the namespaces
150: * and returns the named object or null if no object with the same name
151: * has been found
152: */
153: public Named lookup(Name name) {
154: final Namespace[] spaces = asArray();
155: return lookup(name, spaces);
156: }
157:
158: /**
159: * looks up for the symbol in the namespaces sort, functions and
160: * programVariables
161: * @param name the Name to look up
162: * @return the element of the given name or null
163: */
164: public Named lookupLogicSymbol(Name name) {
165: return lookup(name, logicAsArray());
166: }
167:
168: /**
169: * @param name
170: * @param spaces
171: * @return
172: */
173: private Named lookup(Name name, final Namespace[] spaces) {
174: for (int i = 0; i < spaces.length; i++) {
175: final Named n = spaces[i].lookup(name);
176: if (n != null)
177: return n;
178: }
179: return null;
180: }
181:
182: public String toString() {
183: return "Sorts: " + sorts() + "\n" + "Functions: " + functions()
184: + "\n" + "Variables: " + variables() + "\n"
185: + "ProgramVariables: " + programVariables() + "\n"
186: + "Heuristics: " + ruleSets() + "\n"
187: + "Taclet Options: " + choices() + "\n";
188: }
189:
190: }
|