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: //
012:
013: // This file is partially taken from the RECODER library, which is protected by
014: // the LGPL, and modified.
015:
016: package de.uka.ilkd.key.java.recoderext;
017:
018: import java.io.IOException;
019: import java.io.Reader;
020:
021: import recoder.ParserException;
022: import recoder.convenience.TreeWalker;
023: import recoder.java.*;
024: import recoder.java.SourceElement.Position;
025: import recoder.java.declaration.*;
026: import recoder.java.reference.MethodReference;
027: import recoder.java.reference.TypeReference;
028: import recoder.list.CommentArrayList;
029: import recoder.list.CommentMutableList;
030: import recoder.list.StatementMutableList;
031: import de.uka.ilkd.key.parser.proofjava.ParseException;
032: import de.uka.ilkd.key.parser.proofjava.ProofJavaParser;
033:
034: public class ProofJavaProgramFactory extends JavaProgramFactory {
035:
036: /**
037: Protected constructor - use {@link #getInstance} instead.
038: */
039: protected ProofJavaProgramFactory() {
040: }
041:
042: /**
043: The singleton instance of the program factory.
044: */
045: private static ProofJavaProgramFactory theFactory = new ProofJavaProgramFactory();
046:
047: /**
048: Returns the single instance of this class.
049: */
050: public static JavaProgramFactory getInstance() {
051: return theFactory;
052: }
053:
054: /**
055: For internal reuse and synchronization.
056: */
057: private static ProofJavaParser parser = new ProofJavaParser(
058: System.in);
059:
060: private static final Position ZERO_POSITION = new Position(0, 0);
061:
062: private static void attachComment(Comment c, ProgramElement pe) {
063: ProgramElement dest = pe;
064: if (!c.isPrefixed()) {
065: NonTerminalProgramElement ppe = dest.getASTParent();
066: int i = 0;
067: if (ppe != null) {
068: for (; ppe.getChildAt(i) != dest; i++) {
069: }
070: }
071: if (i == 0) { // before syntactical parent
072: c.setPrefixed(true);
073: } else {
074: dest = ppe.getChildAt(i - 1);
075: while (dest instanceof NonTerminalProgramElement) {
076: ppe = (NonTerminalProgramElement) dest;
077: i = ppe.getChildCount();
078: if (i == 0) {
079: break;
080: }
081: dest = ppe.getChildAt(i - 1);
082: }
083: }
084: }
085: if (c instanceof SingleLineComment && c.isPrefixed()) {
086: Position p = dest.getFirstElement().getRelativePosition();
087: if (p.getLine() < 1) {
088: p.setLine(1);
089: dest.getFirstElement().setRelativePosition(p);
090: }
091: }
092: CommentMutableList cml = dest.getComments();
093: if (cml == null) {
094: dest.setComments(cml = new CommentArrayList());
095: }
096: cml.add(c);
097: }
098:
099: /**
100: Perform post work on the created element. Creates parent links
101: and assigns comments.
102: */
103: private static void postWork(ProgramElement pe) {
104: CommentMutableList comments = ProofJavaParser.getComments();
105: int commentIndex = 0;
106: int commentCount = comments.size();
107: Position cpos = ZERO_POSITION;
108: Comment current = null;
109: if (commentIndex < commentCount) {
110: current = comments.getComment(commentIndex);
111: cpos = current.getFirstElement().getStartPosition();
112: }
113: TreeWalker tw = new TreeWalker(pe);
114: while (tw.next()) {
115: pe = tw.getProgramElement();
116: if (pe instanceof NonTerminalProgramElement) {
117: ((NonTerminalProgramElement) pe).makeParentRoleValid();
118: }
119: if (pe.getFirstElement() != null) {
120: Position pos = pe.getFirstElement().getStartPosition();
121: while ((commentIndex < commentCount)
122: && pos.compareTo(cpos) > 0) {
123: current.setPrefixed(true);
124: attachComment(current, pe);
125: commentIndex += 1;
126: if (commentIndex < commentCount) {
127: current = comments.getComment(commentIndex);
128: cpos = current.getFirstElement()
129: .getStartPosition();
130: }
131: }
132: }
133: }
134: if (commentIndex < commentCount) {
135: while (pe.getASTParent() != null) {
136: pe = pe.getASTParent();
137: }
138: CommentMutableList cml = pe.getComments();
139: if (cml == null) {
140: pe.setComments(cml = new CommentArrayList());
141: }
142: do {
143: current = comments.getComment(commentIndex);
144: current.setPrefixed(false);
145: cml.add(current);
146: commentIndex += 1;
147: } while (commentIndex < commentCount);
148: }
149: }
150:
151: /**
152: Parse a {@link CompilationUnit} from the given reader.
153: */
154: public CompilationUnit parseCompilationUnit(Reader in)
155: throws IOException, ParserException {
156: synchronized (parser) {
157: try {
158: ProofJavaParser.initialize(in);
159: CompilationUnit res = ProofJavaParser.CompilationUnit();
160: postWork(res);
161: return res;
162: } catch (ParseException e) {
163: throw (ParserException) (new ParserException())
164: .initCause(e);
165: }
166: }
167: }
168:
169: /**
170: Parse a {@link TypeDeclaration} from the given reader.
171: */
172: public TypeDeclaration parseTypeDeclaration(Reader in)
173: throws IOException, ParserException {
174: synchronized (parser) {
175: try {
176: ProofJavaParser.initialize(in);
177: TypeDeclaration res = ProofJavaParser.TypeDeclaration();
178: postWork(res);
179: return res;
180: } catch (ParseException e) {
181: throw (ParserException) (new ParserException())
182: .initCause(e);
183: }
184:
185: }
186: }
187:
188: /**
189: Parse a {@link FieldDeclaration} from the given reader.
190: */
191: public FieldDeclaration parseFieldDeclaration(Reader in)
192: throws IOException, ParserException {
193: synchronized (parser) {
194: try {
195: ProofJavaParser.initialize(in);
196: FieldDeclaration res = ProofJavaParser
197: .FieldDeclaration();
198: postWork(res);
199: return res;
200: } catch (ParseException e) {
201: throw (ParserException) (new ParserException())
202: .initCause(e);
203: }
204:
205: }
206: }
207:
208: /**
209: Parse a {@link MethodDeclaration} from the given reader.
210: */
211: public MethodDeclaration parseMethodDeclaration(Reader in)
212: throws IOException, ParserException {
213: synchronized (parser) {
214: try {
215: ProofJavaParser.initialize(in);
216: MethodDeclaration res = ProofJavaParser
217: .MethodDeclaration();
218: postWork(res);
219: return res;
220: } catch (ParseException e) {
221: throw (ParserException) (new ParserException())
222: .initCause(e);
223: }
224:
225: }
226: }
227:
228: /**
229: Parse a {@link MemberDeclaration} from the given reader.
230: */
231: public MemberDeclaration parseMemberDeclaration(Reader in)
232: throws IOException, ParserException {
233: synchronized (parser) {
234: try {
235: ProofJavaParser.initialize(in);
236: MemberDeclaration res = ProofJavaParser
237: .ClassBodyDeclaration();
238: postWork(res);
239: return res;
240: } catch (ParseException e) {
241: throw (ParserException) (new ParserException())
242: .initCause(e);
243: }
244:
245: }
246: }
247:
248: /**
249: Parse a {@link ParameterDeclaration} from the given reader.
250: */
251: public ParameterDeclaration parseParameterDeclaration(Reader in)
252: throws IOException, ParserException {
253: synchronized (parser) {
254: try {
255: ProofJavaParser.initialize(in);
256: ParameterDeclaration res = ProofJavaParser
257: .FormalParameter();
258: postWork(res);
259: return res;
260: } catch (ParseException e) {
261: throw (ParserException) (new ParserException())
262: .initCause(e);
263: }
264:
265: }
266: }
267:
268: /**
269: Parse a {@link ConstructorDeclaration} from the given reader.
270: */
271: public ConstructorDeclaration parseConstructorDeclaration(Reader in)
272: throws IOException, ParserException {
273: synchronized (parser) {
274: try {
275: ProofJavaParser.initialize(in);
276: ConstructorDeclaration res = ProofJavaParser
277: .ConstructorDeclaration();
278: postWork(res);
279: return res;
280: } catch (ParseException e) {
281: throw (ParserException) (new ParserException())
282: .initCause(e);
283: }
284:
285: }
286: }
287:
288: /**
289: Parse a {@link TypeReference} from the given reader.
290: */
291: public TypeReference parseTypeReference(Reader in)
292: throws IOException, ParserException {
293: synchronized (parser) {
294: try {
295: ProofJavaParser.initialize(in);
296: TypeReference res = ProofJavaParser.ResultType();
297: postWork(res);
298: return res;
299: } catch (ParseException e) {
300: throw (ParserException) (new ParserException())
301: .initCause(e);
302: }
303:
304: }
305: }
306:
307: /**
308: Parse an {@link Expression} from the given reader.
309: */
310: public Expression parseExpression(Reader in) throws IOException,
311: ParserException {
312: synchronized (parser) {
313: try {
314: ProofJavaParser.initialize(in);
315: Expression res = ProofJavaParser.Expression();
316: postWork(res);
317: return res;
318: } catch (ParseException e) {
319: throw (ParserException) (new ParserException())
320: .initCause(e);
321: }
322:
323: }
324: }
325:
326: /**
327: Parse some {@link Statement}s from the given reader.
328: */
329: public StatementMutableList parseStatements(Reader in)
330: throws IOException, ParserException {
331: synchronized (parser) {
332: try {
333: ProofJavaParser.initialize(in);
334: StatementMutableList res = ProofJavaParser
335: .GeneralizedStatements();
336: for (int i = 0; i < res.size(); i += 1) {
337: postWork(res.getStatement(i));
338: }
339: return res;
340: } catch (ParseException e) {
341: throw (ParserException) (new ParserException())
342: .initCause(e);
343: }
344:
345: }
346: }
347:
348: /**
349: * Parse a {@link StatementBlock} from the given string.
350: */
351: public StatementBlock parseStatementBlock(Reader in)
352: throws IOException, ParserException {
353: synchronized (parser) {
354: try {
355: ProofJavaParser.initialize(in);
356: StatementBlock res = ProofJavaParser.StartBlock();
357: postWork(res);
358: return res;
359: } catch (ParseException e) {
360: throw (ParserException) (new ParserException())
361: .initCause(e);
362: }
363:
364: }
365: }
366:
367: /**
368: * Create a {@link PassiveExpression}.
369: */
370: public PassiveExpression createPassiveExpression(Expression e) {
371: return new PassiveExpression(e);
372: }
373:
374: /**
375: * Create a {@link PassiveExpression}.
376: */
377: public PassiveExpression createPassiveExpression() {
378: return new PassiveExpression();
379: }
380:
381: /**
382: * Create a {@link MethodCallStatement}.
383: */
384: public MethodCallStatement createMethodCallStatement(
385: Expression resVar, ExecutionContext ec, StatementBlock block) {
386: return new MethodCallStatement(resVar, ec, block);
387: }
388:
389: /**
390: * Create a {@link MethodBodyStatement}.
391: */
392: public MethodBodyStatement createMethodBodyStatement(
393: TypeReference bodySource, Expression resVar,
394: MethodReference methRef) {
395: return new MethodBodyStatement(bodySource, resVar, methRef);
396: }
397:
398: /**
399: * Create a {@link CatchAllStatement}.
400: */
401: public Statement createCatchAllStatement(ParameterDeclaration decl,
402: StatementBlock body) {
403: return new CatchAllStatement(decl, body);
404: }
405:
406: /**
407: * Create an {@link ImplicitIdentifier}.
408: */
409: public ImplicitIdentifier createImplicitIdentifier(String text) {
410: return new ImplicitIdentifier(text);
411: }
412:
413: public Identifier createIdentifier(String text) {
414: return new ExtendedIdentifier(text);
415: }
416:
417: }
|