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.rule.soundness;
012:
013: import de.uka.ilkd.key.logic.Namespace;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
016: import de.uka.ilkd.key.logic.op.SchemaVariable;
017: import de.uka.ilkd.key.logic.op.SetAsListOfSchemaVariable;
018: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
019: import de.uka.ilkd.key.rule.ListOfTacletApp;
020: import de.uka.ilkd.key.rule.SLListOfTacletApp;
021: import de.uka.ilkd.key.rule.TacletApp;
022: import de.uka.ilkd.key.rule.inst.SVInstantiations;
023:
024: /**
025: * Immutable
026: */
027: public interface SkolemSet {
028:
029: SVInstantiations getInstantiations();
030:
031: Namespace getFunctions();
032:
033: Namespace getVariables();
034:
035: ListOfTacletApp getTaclets();
036:
037: SetOfSchemaVariable getMissing();
038:
039: Term getFormula();
040:
041: SVTypeInfos getSVTypeInfos();
042:
043: SVPartitioning getSVPartitioning();
044:
045: SkolemSet add(SVInstantiations p_inst);
046:
047: SkolemSet addFunctions(Namespace p_functions);
048:
049: SkolemSet addVariables(Namespace p_variables);
050:
051: SkolemSet addTaclets(ListOfTacletApp p_taclets);
052:
053: SkolemSet addMissing(IteratorOfSchemaVariable p_missing);
054:
055: SkolemSet setFormula(Term p_formula);
056:
057: SkolemSet setSVTypeInfos(SVTypeInfos p_infos);
058:
059: SkolemSet setSVPartitioning(SVPartitioning p_partitioning);
060:
061: static class DefaultSkolemSet implements SkolemSet {
062:
063: private SVInstantiations inst;
064: private Namespace functions;
065: private Namespace variables;
066: private ListOfTacletApp taclets;
067: private SetOfSchemaVariable miss;
068: private Term formula;
069: private SVTypeInfos svTypeInfos;
070: private SVPartitioning svPartitioning;
071:
072: private DefaultSkolemSet(SVInstantiations p_inst,
073: Namespace p_functions, Namespace p_variables,
074: ListOfTacletApp p_taclets, SetOfSchemaVariable p_miss,
075: Term p_formula, SVTypeInfos p_svTypeInfos,
076: SVPartitioning p_svPartitioning) {
077: inst = p_inst;
078: functions = p_functions;
079: variables = p_variables;
080: taclets = p_taclets;
081: miss = p_miss;
082: formula = p_formula;
083: svTypeInfos = p_svTypeInfos;
084: svPartitioning = p_svPartitioning;
085: }
086:
087: public DefaultSkolemSet(TacletApp p_app, Term p_formula) {
088: this (p_app.instantiations(), new Namespace(),
089: new Namespace(), SLListOfTacletApp.EMPTY_LIST,
090: p_app.uninstantiatedVars(), p_formula,
091: SVTypeInfos.EMPTY_SVTYPEINFOS, null);
092: }
093:
094: public SkolemSet addFunctions(Namespace p_functions) {
095: Namespace n = new Namespace(getFunctions());
096: n.add(p_functions);
097: return new DefaultSkolemSet(getInstantiations(), n,
098: getVariables(), getTaclets(), getMissing(),
099: getFormula(), getSVTypeInfos(), getSVPartitioning());
100: }
101:
102: public SkolemSet addVariables(Namespace p_variables) {
103: Namespace n = new Namespace(getVariables());
104: n.add(p_variables);
105: return new DefaultSkolemSet(getInstantiations(),
106: getFunctions(), n, getTaclets(), getMissing(),
107: getFormula(), getSVTypeInfos(), getSVPartitioning());
108: }
109:
110: public SkolemSet addTaclets(ListOfTacletApp p_taclets) {
111: return new DefaultSkolemSet(getInstantiations(),
112: getFunctions(), getVariables(), getTaclets()
113: .prepend(p_taclets), getMissing(),
114: getFormula(), getSVTypeInfos(), getSVPartitioning());
115: }
116:
117: public SkolemSet add(SVInstantiations p_inst) {
118: SetOfSchemaVariable m = SetAsListOfSchemaVariable.EMPTY_SET;
119: IteratorOfSchemaVariable it = getMissing().iterator();
120: SchemaVariable v;
121:
122: while (it.hasNext()) {
123: v = it.next();
124: if (!p_inst.isInstantiated(v))
125: m = m.add(v);
126: }
127:
128: return new DefaultSkolemSet(p_inst, getFunctions(),
129: getVariables(), getTaclets(), m, getFormula(),
130: getSVTypeInfos(), getSVPartitioning());
131: }
132:
133: public SkolemSet addMissing(IteratorOfSchemaVariable p_missing) {
134: SetOfSchemaVariable m = getMissing();
135: while (p_missing.hasNext())
136: m = m.add(p_missing.next());
137: return new DefaultSkolemSet(getInstantiations(),
138: getFunctions(), getVariables(), getTaclets(), m,
139: getFormula(), getSVTypeInfos(), getSVPartitioning());
140: }
141:
142: public SkolemSet setFormula(Term p_formula) {
143: return new DefaultSkolemSet(getInstantiations(),
144: getFunctions(), getVariables(), getTaclets(),
145: getMissing(), p_formula, getSVTypeInfos(),
146: getSVPartitioning());
147: }
148:
149: public SkolemSet setSVTypeInfos(SVTypeInfos p_infos) {
150: return new DefaultSkolemSet(getInstantiations(),
151: getFunctions(), getVariables(), getTaclets(),
152: getMissing(), getFormula(), p_infos,
153: getSVPartitioning());
154: }
155:
156: public SVInstantiations getInstantiations() {
157: return inst;
158: }
159:
160: public Namespace getFunctions() {
161: return functions;
162: }
163:
164: public Namespace getVariables() {
165: return variables;
166: }
167:
168: public ListOfTacletApp getTaclets() {
169: return taclets;
170: }
171:
172: public SetOfSchemaVariable getMissing() {
173: return miss;
174: }
175:
176: public Term getFormula() {
177: return formula;
178: }
179:
180: public SVTypeInfos getSVTypeInfos() {
181: return svTypeInfos;
182: }
183:
184: public SVPartitioning getSVPartitioning() {
185: return svPartitioning;
186: }
187:
188: public SkolemSet setSVPartitioning(SVPartitioning p_partitioning) {
189: return new DefaultSkolemSet(getInstantiations(),
190: getFunctions(), getVariables(), getTaclets(),
191: getMissing(), getFormula(), getSVTypeInfos(),
192: p_partitioning);
193: }
194:
195: }
196:
197: }
|