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: package de.uka.ilkd.key.proof.init;
011:
012: import de.uka.ilkd.key.gui.Main;
013: import de.uka.ilkd.key.gui.configuration.LibrariesSettings;
014: import de.uka.ilkd.key.logic.Choice;
015: import de.uka.ilkd.key.logic.IteratorOfNamed;
016: import de.uka.ilkd.key.logic.Name;
017: import de.uka.ilkd.key.logic.Namespace;
018: import de.uka.ilkd.key.logic.ldt.BooleanLDT;
019: import de.uka.ilkd.key.logic.ldt.ByteLDT;
020: import de.uka.ilkd.key.logic.ldt.CharLDT;
021: import de.uka.ilkd.key.logic.ldt.IntLDT;
022: import de.uka.ilkd.key.logic.ldt.IntegerDomainLDT;
023: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
024: import de.uka.ilkd.key.logic.ldt.ListOfLDT;
025: import de.uka.ilkd.key.logic.ldt.LongLDT;
026: import de.uka.ilkd.key.logic.ldt.SLListOfLDT;
027: import de.uka.ilkd.key.logic.ldt.ShortLDT;
028:
029: /** Represents the LDT .key files as a whole. Special treatment of these
030: * files is necessary because their parts need to be read in a special
031: * order, namely first all sort declarations then all function and predicate
032: * declarations and third the rules. This procedure makes it possible to
033: * use all declared sorts in all rules.
034: */
035: public class LDTInput implements EnvInput {
036: private static final String NAME = "language data types";
037:
038: private final KeYFile[] keyFiles;
039: private final Main main;
040:
041: private InitConfig initConfig = null;
042:
043: /** creates a representation of the LDT files to be used as input
044: * to the KeY prover.
045: * @param keyFiles an array containing the LDT .key files
046: * @param main the main class used to report the progress of reading
047: */
048: public LDTInput(KeYFile[] keyFiles, Main main) {
049: this .keyFiles = keyFiles;
050: this .main = main;
051: }
052:
053: public String name() {
054: return NAME;
055: }
056:
057: public int getNumberOfChars() {
058: int sum = 0;
059: for (int i = 0; i < keyFiles.length; i++) {
060: sum = sum + keyFiles[i].getNumberOfChars();
061: }
062: return sum;
063: }
064:
065: public void setInitConfig(InitConfig conf) {
066: this .initConfig = conf;
067: for (int i = 0; i < keyFiles.length; i++) {
068: keyFiles[i].setInitConfig(conf);
069: }
070: }
071:
072: public Includes readIncludes() throws ProofInputException {
073: Includes result = new Includes();
074: for (int i = 0; i < keyFiles.length; i++) {
075: result.putAll(keyFiles[i].readIncludes());
076: }
077: return result;
078: }
079:
080: public LibrariesSettings readLibrariesSettings()
081: throws ProofInputException {
082: return new LibrariesSettings();
083: }
084:
085: public String readJavaPath() throws ProofInputException {
086: return "";
087: }
088:
089: /** reads all LDTs, i.e., all associated .key files with respect to
090: * the given modification strategy. Reading is done in a special order: first
091: * all sort declarations then all function and predicate declarations and
092: * third the rules. This procedure makes it possible to use all declared
093: * sorts in all rules, e.g.
094: */
095: public void read(ModStrategy mod) throws ProofInputException {
096: if (initConfig == null) {
097: throw new IllegalStateException(
098: "LDTInput: InitConfig not set.");
099: }
100: for (int i = 0; i < keyFiles.length; i++) {
101: keyFiles[i].readSorts(mod);
102: }
103: for (int i = 0; i < keyFiles.length; i++) {
104: keyFiles[i].readFuncAndPred(mod);
105: }
106: for (int i = 0; i < keyFiles.length; i++) {
107: if (main != null) {
108: main.setStatusLine("Reading " + keyFiles[i].name(),
109: keyFiles[i].getNumberOfChars());
110: }
111: keyFiles[i].readRulesAndProblem(mod);
112: }
113:
114: //create LDTs
115: Namespace sorts = initConfig.sortNS();
116: Namespace functions = new Namespace(initConfig.funcNS());
117: IteratorOfNamed it = initConfig.choiceNS().allElements()
118: .iterator();
119: while (it.hasNext()) {
120: Choice c = (Choice) it.next();
121: functions.add(c.funcNS());
122: }
123: ListOfLDT ldts = SLListOfLDT.EMPTY_LIST.prepend(
124: new ByteLDT(sorts, functions)).prepend(
125: new ShortLDT(sorts, functions)).prepend(
126: new IntLDT(sorts, functions)).prepend(
127: new LongLDT(sorts, functions)).prepend(
128: new CharLDT(sorts, functions)).prepend(
129: new IntegerLDT(sorts, functions)).prepend(
130: new IntegerDomainLDT(sorts, functions)).prepend(
131: new BooleanLDT(sorts, functions));
132: initConfig.getServices().getTypeConverter().init(ldts);
133: }
134:
135: public boolean equals(Object o) {
136: if (!(o instanceof LDTInput)) {
137: return false;
138: }
139:
140: LDTInput li = (LDTInput) o;
141: if (keyFiles.length != li.keyFiles.length) {
142: return false;
143: }
144:
145: for (int i = 0; i < keyFiles.length; i++) {
146: boolean found = false;
147: for (int j = 0; j < keyFiles.length; j++) {
148: if (li.keyFiles[j].equals(keyFiles[i])) {
149: found = true;
150: break;
151: }
152: }
153: if (!found) {
154: return false;
155: }
156: }
157:
158: return true;
159: }
160:
161: public int hashCode() {
162: int result = 0;
163: for (int i = 0; i < keyFiles.length; i++) {
164: result += keyFiles[i].hashCode();
165: }
166: return result;
167: }
168: }
|