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: /** this class is used to parse in Taclet from a file that are used by tests */package de.uka.ilkd.key.rule;
012:
013: import java.io.File;
014: import java.io.StringReader;
015:
016: import de.uka.ilkd.key.java.JavaInfo;
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.java.Recoder2KeY;
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.logic.*;
021: import de.uka.ilkd.key.logic.op.Function;
022: import de.uka.ilkd.key.logic.op.SchemaVariable;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.parser.KeYLexer;
025: import de.uka.ilkd.key.parser.KeYParser;
026: import de.uka.ilkd.key.parser.ParserMode;
027: import de.uka.ilkd.key.pp.AbbrevMap;
028: import de.uka.ilkd.key.proof.ProofAggregate;
029: import de.uka.ilkd.key.proof.RuleSource;
030: import de.uka.ilkd.key.proof.TacletIndex;
031: import de.uka.ilkd.key.proof.init.*;
032:
033: public class TacletForTests {
034:
035: private TacletForTests() {
036: }
037:
038: public static final String testRules = System
039: .getProperty("key.home")
040: + File.separator
041: + "examples"
042: + File.separator
043: + "_testcase" + File.separator + "testrules.key";
044: public static String standardFile = testRules;
045:
046: public static AbbrevMap scm = new AbbrevMap();
047:
048: public static NamespaceSet nss = new NamespaceSet();
049: public static TacletIndex rules = null;
050: public static Services services;
051: public static File lastFile = null;
052:
053: public static Profile profile = new JUnitTestProfile() {
054: //we do not want normal standard rules, but ruleSetsDeclarations is needed for string library (HACK)
055: public RuleCollection getStandardRules() {
056: return new RuleCollection(RuleSource
057: .initRuleFile("ruleSetsDeclarations.key"),
058: SLListOfBuiltInRule.EMPTY_LIST);
059: }
060: };
061:
062: public static void clear() {
063: lastFile = null;
064: services = null;
065: rules = null;
066: nss = new NamespaceSet();
067: }
068:
069: public static void parse(File file) {
070: try {
071: if (!file.equals(lastFile)) {
072: EnvInput envInput = new KeYFileForTests("Test", file);
073: ProblemInitializer pi = new ProblemInitializer(profile);
074: InitConfig ic = pi.prepare(envInput);
075: nss = ic.namespaces();
076: rules = ic.createTacletIndex();
077: services = ic.getServices();
078: lastFile = file;
079: }
080: } catch (Exception e) {
081: System.err.println("Exception occurred while parsing "
082: + file + "\n");
083: e.printStackTrace();
084: System.exit(-1);
085: }
086: }
087:
088: public static Services services() {
089: if (services == null)
090: parse();
091: return services;
092: }
093:
094: public static JavaInfo javaInfo() {
095: return services().getJavaInfo();
096: }
097:
098: public static JavaInfo getJavaInfo() {
099: return javaInfo();
100: }
101:
102: public static void setStandardFile(String filename) {
103: standardFile = filename;
104: }
105:
106: public static ProofAggregate problems() {
107: return null;
108: }
109:
110: public static void parse(String filename) {
111: parse(new File(filename));
112: }
113:
114: public static void parse() {
115: parse(standardFile);
116: }
117:
118: public static NoPosTacletApp getTaclet(String name) {
119: return rules.lookup(new Name(name));
120: }
121:
122: public static AbbrevMap getAbbrevs() {
123: return scm;
124: }
125:
126: public static Namespace getSorts() {
127: return nss.sorts();
128: }
129:
130: public static TacletIndex getRules() {
131: return rules;
132: }
133:
134: public static Namespace getHeuristics() {
135: return nss.ruleSets();
136: }
137:
138: public static Namespace getFunctions() {
139: return nss.functions();
140: }
141:
142: public static Namespace getVariables() {
143: return nss.variables();
144: }
145:
146: public static Namespace getProgramVariables() {
147: return nss.programVariables();
148: }
149:
150: public static NamespaceSet getNamespaces() {
151: return nss;
152: }
153:
154: public static Function funcLookup(String name) {
155: return (Function) getFunctions().lookup(new Name(name));
156: }
157:
158: public static SchemaVariable svLookup(String name) {
159: return (SchemaVariable) getVariables().lookup(new Name(name));
160: }
161:
162: public static Sort sortLookup(String name) {
163: return (Sort) getSorts().lookup(new Name(name));
164: }
165:
166: public static Term parseTerm(String termstr, Services services) {
167: if (termstr.equals(""))
168: return null;
169: try {
170: StringReader br = new StringReader(termstr);
171: KeYParser parser = new KeYParser(ParserMode.TERM,
172: new KeYLexer(br, null), "No file. "
173: + "TacletForTests.parseTerm(" + termstr
174: + ")", TermFactory.DEFAULT,
175: new Recoder2KeY(services, nss), services, nss,
176: TacletForTests.getAbbrevs());
177: return parser.term();
178: } catch (Exception e) {
179: System.err.println("Exception during parsing!");
180: e.printStackTrace();
181: System.exit(-1);
182: return null;
183: }
184:
185: }
186:
187: public static Term parseTerm(String termstr, NamespaceSet set) {
188: if (termstr.equals(""))
189: return null;
190: try {
191: StringReader br = new StringReader(termstr);
192: KeYParser parser = new KeYParser(ParserMode.TERM,
193: new KeYLexer(br, null), "No file. "
194: + "TacletForTests.parseTerm(" + termstr
195: + ")", TermFactory.DEFAULT,
196: new Recoder2KeY(services(), set), services(), set,
197: new AbbrevMap());
198: return parser.term();
199: } catch (Exception e) {
200: System.err.println("Exception during parsing!");
201: e.printStackTrace();
202: return null;
203: }
204:
205: }
206:
207: public static Term parseTerm(String termstr) {
208: return parseTerm(termstr, services());
209: }
210:
211: public static ProgramElement parsePrg(String prgString) {
212: Recoder2KeY r2k = new Recoder2KeY(services(),
213: new NamespaceSet());
214: return r2k.readBlockWithEmptyContext(prgString).program();
215: }
216: }
|