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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
010: // and Chalmers University of Technology, Sweden
011: //
012: //The KeY system is protected by the GNU General Public License.
013: //See LICENSE.TXT for details.
014: //
015:
016: package de.uka.ilkd.key.rule.export;
017:
018: import java.util.*;
019:
020: import de.uka.ilkd.key.logic.IteratorOfNamed;
021: import de.uka.ilkd.key.logic.Named;
022: import de.uka.ilkd.key.logic.Namespace;
023: import de.uka.ilkd.key.logic.NamespaceSet;
024: import de.uka.ilkd.key.logic.sort.Sort;
025: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
026: import de.uka.ilkd.key.proof.RuleSource;
027: import de.uka.ilkd.key.proof.init.*;
028: import de.uka.ilkd.key.rule.*;
029:
030: public class TacletLoader {
031:
032: private boolean loadStandardRules = true;
033:
034: //private static InitConfig BASE_CONFIG = null;
035:
036: private InitConfig initConfig;
037: private HashSet alreadyParsed;
038:
039: // key: String
040: // value: SetOfTaclet
041: private HashMap file2taclets;
042:
043: public TacletLoader() {
044: initConfig = new InitConfig();
045: alreadyParsed = new HashSet();
046:
047: file2taclets = new HashMap();
048: }
049:
050: private void printlnIndented(int level, String msg) {
051: for (int n = 0; n < level * 2; n++) {
052: System.out.print(' ');
053: }
054: System.out.println(msg);
055: }
056:
057: private void setUpSorts(InitConfig initConfig) {
058: IteratorOfNamed it = initConfig.sortNS().allElements()
059: .iterator();
060: while (it.hasNext()) {
061: Sort sort = (Sort) it.next();
062: if (sort instanceof SortDefiningSymbols) {
063: ((SortDefiningSymbols) sort).addDefinedSymbols(
064: initConfig.funcNS(), initConfig.sortNS());
065: }
066: }
067: }
068:
069: private void loadIncludes(Includes in, int level, String filename)
070: throws ProofInputException {
071: if (in.getIncludes().isEmpty())
072: return;
073:
074: printlnIndented(level, filename + ": loading includes");
075:
076: final Iterator it = in.getIncludes().iterator();
077:
078: while (it.hasNext()) {
079: final String name = (String) it.next();
080:
081: loadFile(name, in.get(name), level + 1);
082: }
083: }
084:
085: private void loadLDTIncludes(Includes in, int level, String filename)
086: throws ProofInputException {
087: if (in.getLDTIncludes().isEmpty())
088: return;
089:
090: printlnIndented(level, filename + ": loading LDTs");
091:
092: KeYFile[] keyFile = new KeYFile[in.getLDTIncludes().size()];
093: Iterator it = in.getLDTIncludes().iterator();
094: int i = 0;
095: if (initConfig == null) {
096: initConfig = new InitConfig();
097: }
098: while (it.hasNext()) {
099: final String name = (String) it.next();
100: keyFile[i] = new KeYFile(name, in.get(name), null);
101: keyFile[i].setInitConfig(initConfig);
102: Includes includes = keyFile[i].readIncludes();
103: loadIncludes(includes, level + 1, name);
104: i++;
105: }
106:
107: final ModStrategy mod = ModStrategy.NO_VARS;
108:
109: for (i = 0; i < keyFile.length; i++) {
110: keyFile[i].readSorts(mod);
111: }
112: for (i = 0; i < keyFile.length; i++) {
113: keyFile[i].readFuncAndPred(mod);
114: }
115: for (i = 0; i < keyFile.length; i++) {
116:
117: final String name = keyFile[i].name();
118:
119: printlnIndented(level + 1, name + ": loading taclets");
120: initConfig.setTaclets(SetAsListOfTaclet.EMPTY_SET);
121: keyFile[i].readRulesAndProblem(mod);
122: file2taclets.put(name, initConfig.getTaclets());
123:
124: alreadyParsed.add(name);
125: }
126: }
127:
128: private void loadFile(String filename, RuleSource ruleSource,
129: int level) throws ProofInputException {
130: if (alreadyParsed.add(filename)) {
131: KeYFile file = new KeYFile(filename, ruleSource, null);
132: file.setInitConfig(initConfig);
133:
134: Includes includes = file.readIncludes();
135:
136: if (!includes.getLDTIncludes().isEmpty()) {
137: loadLDTIncludes(includes, level, filename);
138: }
139:
140: if (!includes.getIncludes().isEmpty()) {
141: loadIncludes(includes, level, filename);
142: }
143:
144: printlnIndented(level, filename + ": loading taclets");
145: initConfig.setTaclets(SetAsListOfTaclet.EMPTY_SET);
146:
147: setUpSorts(initConfig);
148: file.read(ModStrategy.NO_VARS);
149: file2taclets.put(filename, initConfig.getTaclets());
150: } else {
151: printlnIndented(level, filename + ": already loaded");
152: }
153: }
154:
155: public void loadFile(String filename) throws ProofInputException {
156: if (filename.endsWith(".key")) {
157: final String name = filename.substring(0,
158: filename.length() - 4);
159: if (alreadyParsed.contains(name)) {
160: return;
161: }
162: }
163: if (!alreadyParsed.contains(filename)) {
164: RuleSource ruleSource = RuleSource.initRuleFile(filename);
165: loadFile(filename, ruleSource, 0);
166: }
167: }
168:
169: public ListOfTaclet loadRules(String filename) {
170: ListOfTaclet result = null;
171:
172: try {
173: System.out.println("Loading " + filename);
174: loadFile(filename);
175:
176: //dumpInitConfig(initConfig);
177:
178: //initConfig.setTaclets(SetAsListOfTaclet.EMPTY_SET);
179:
180: System.out.println("Loading rules for " + filename);
181: //file.readRulesAndProblem(ModStrategy.NO_VARS_FUNCS);
182:
183: //dumpInitConfig(initConfig);
184:
185: result = SLListOfTaclet.EMPTY_LIST;
186:
187: final IteratorOfTaclet it = ((SetOfTaclet) file2taclets
188: .get(filename)).iterator();
189:
190: while (it.hasNext()) {
191: final Taclet taclet = it.next();
192: result = result.prepend(taclet);
193: }
194: } catch (ProofInputException e) {
195: System.err.println(e);
196: }
197:
198: return result;
199: }
200:
201: public void setLoadStandardRules(boolean flag) {
202: loadStandardRules = flag;
203: }
204:
205: public boolean getLoadStandardRules() {
206: return loadStandardRules;
207: }
208:
209: public void addAllLoadedRules(RuleExportModel model) {
210:
211: final Iterator it = file2taclets.entrySet().iterator();
212: while (it.hasNext()) {
213: final Map.Entry entry = (Map.Entry) it.next();
214: final String filename = (String) entry.getKey();
215: final SetOfTaclet tacletSet = (SetOfTaclet) entry
216: .getValue();
217: final IteratorOfTaclet it2 = tacletSet.iterator();
218: while (it2.hasNext()) {
219: final Taclet t = it2.next();
220: model.addTaclet(t, filename);
221: }
222: }
223: }
224:
225: /** Dump namespace set from InitConfig (for debugging). */
226: public static void dumpInitConfig(InitConfig initConfig) {
227: dumpNamespaceSet(initConfig.namespaces(), "InitConfig");
228: }
229:
230: /** Dump namespace set (for debugging). */
231: public static void dumpNamespaceSet(NamespaceSet nss) {
232: dumpNamespaceSet(nss, "NamespaceSet");
233: }
234:
235: /** Dump namespace set with given name in delimiters (for debugging). */
236: public static void dumpNamespaceSet(NamespaceSet nss, String name) {
237: System.out.println("---- " + name + " ----");
238: dumpNamespace(nss.ruleSets(), "rule sets");
239: dumpNamespace(nss.choices(), "choices");
240: dumpNamespace(nss.sorts(), "sorts");
241: dumpNamespace(nss.functions(), "functions");
242: System.out.println("---- End of " + name + " ----");
243: }
244:
245: /** Dump namespace with given name (for debugging). */
246: private static void dumpNamespace(Namespace ns, String name) {
247: Named elements[] = ns.elements().toArray();
248: Arrays.sort(elements, new Comparator() {
249: public int compare(Object a, Object b) {
250: return ((Named) a).name().compareTo(((Named) b).name());
251: }
252: });
253:
254: System.out.println("-- " + name + " --");
255:
256: for (int n = 0; n < elements.length; n++) {
257: System.out.println(elements[n].name());
258: }
259: }
260:
261: }
|