Source Code Cross Referenced for DragNDropInstantiator.java in  » Testing » KeY » de » uka » ilkd » key » gui » nodeviews » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.gui.nodeviews 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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:        package de.uka.ilkd.key.gui.nodeviews;
010:
011:        import java.awt.Point;
012:        import java.awt.datatransfer.Transferable;
013:        import java.awt.datatransfer.UnsupportedFlavorException;
014:        import java.awt.dnd.DropTargetAdapter;
015:        import java.awt.dnd.DropTargetDragEvent;
016:        import java.awt.dnd.DropTargetDropEvent;
017:        import java.awt.event.ActionEvent;
018:        import java.awt.event.ActionListener;
019:        import java.io.IOException;
020:
021:        import javax.swing.JPopupMenu;
022:
023:        import de.uka.ilkd.key.gui.KeYMediator;
024:        import de.uka.ilkd.key.gui.configuration.ProofSettings;
025:        import de.uka.ilkd.key.java.Services;
026:        import de.uka.ilkd.key.logic.Constraint;
027:        import de.uka.ilkd.key.logic.PosInOccurrence;
028:        import de.uka.ilkd.key.logic.PosInTerm;
029:        import de.uka.ilkd.key.logic.Sequent;
030:        import de.uka.ilkd.key.logic.op.SchemaVariable;
031:        import de.uka.ilkd.key.pp.PosInSequent;
032:        import de.uka.ilkd.key.rule.*;
033:        import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
034:
035:        /**
036:         * <p>
037:         * The DragNDropInstantiator interpretes drag'n drop actions as taclet
038:         * instantiations. The behaviour is described below (excluding some
039:         * "optimisation" details)
040:         * </p>
041:         * <p>
042:         * Let "source" denote the formula/term which is dragged and dropped on another
043:         * term called "target". The DragNDropInstantiation of a taclet "t" is now
044:         * defined as follows:
045:         * <ol>
046:         * <li>t must have exactly one formula/term in the <tt>find</tt> part and
047:         * <tt>assumes</tt> sequent (in particular it must have an <tt>assumes</tt> -part)
048:         * </li>
049:         * <li>and
050:         * <ol>
051:         * <li>if t's goal descriptions do not contain any <tt>replacewith</tt> then
052:         * "source" is matched against the <tt>find</tt> part of the taclet and
053:         * "target" has to match the "if" part.</li>
054:         * <li>if t's goal descriptions contain at least <em>one</em> replacewith
055:         * then "target" is matched against the <tt>find</tt> part and "source"
056:         * against the <tt>assumes</tt> part</li>*
057:         * </ol>
058:         * or
059:         * <li>t must have a <tt>find</tt> part, no <tt>assumes</tt> and at least one
060:         * addrule. In this case source is merged against <tt>find</tt> part and
061:         * target has to be the complete sequent. Dropping on the sequent arrow is
062:         * interpreted as applying an addrule(treats hide rules)</li>
063:         * </ol>
064:         * The DragNDropInstantiator now determines all taclets, which have a valid
065:         * drag'n drop instantiation for a given (source, target) position pair. If
066:         * there is only one taclet with a valid dnd-instantiation this one is executed
067:         * otherwise the user is presented a list of possible taclets from which she/he
068:         * can select one.
069:         * </p>
070:         */
071:        public class DragNDropInstantiator extends DropTargetAdapter {
072:
073:            /** the sequentview where dnd has been initiated */
074:            private SequentView seqView;
075:
076:            DragNDropInstantiator(SequentView seqView) {
077:                this .seqView = seqView;
078:            }
079:
080:            public void drop(DropTargetDropEvent event) {
081:
082:                Point dropLocation = event.getLocation();
083:
084:                try {
085:                    Transferable transferable = event.getTransferable();
086:                    if (transferable
087:                            .isDataFlavorSupported(PosInSequentTransferable.POS_IN_SEQUENT_TRANSFER)) {
088:                        interpreteDragAndDropInstantiation(event, dropLocation,
089:                                transferable);
090:                    } else {
091:                        event.rejectDrop();
092:                    }
093:                } catch (IOException exception) {
094:                    // just reject drop do not bother the user
095:                    event.rejectDrop();
096:                } catch (UnsupportedFlavorException ufException) {
097:                    // just reject drop do not bother the user
098:                    event.rejectDrop();
099:                }
100:
101:                seqView.requestFocus();
102:            }
103:
104:            public void dragOver(DropTargetDragEvent dtde) {
105:                seqView.autoscroll(dtde.getLocation());
106:                seqView.paintHighlights(dtde.getLocation());
107:            }
108:
109:            /**
110:             * Interpretes the drag and drop gesture. Checks which taclets could be
111:             * meant by the drag'n drop and applies if the app can be uniquely
112:             * determined, otherwise a selection menu is presented to the user
113:             */
114:            private void interpreteDragAndDropInstantiation(
115:                    DropTargetDropEvent event, Point dropLocation,
116:                    Transferable transferable)
117:                    throws UnsupportedFlavorException, IOException {
118:
119:                final PosInSequent sourcePos = (PosInSequent) transferable
120:                        .getTransferData(PosInSequentTransferable.POS_IN_SEQUENT_TRANSFER);
121:
122:                final PosInSequent targetPos = seqView
123:                        .getPosInSequent(dropLocation);
124:
125:                if (targetPos == null || sourcePos == null
126:                        || sourcePos.isSequent()) {
127:                    event.rejectDrop();
128:                    return;
129:                }
130:
131:                final Services services = seqView.mediator().getServices();
132:
133:                ListOfPosTacletApp applicableApps = getAllApplicableApps(
134:                        sourcePos, targetPos, services);
135:
136:                if (applicableApps.isEmpty()
137:                        && !targetPos.isSequent()
138:                        && targetPos.getPosInOccurrence().posInTerm() != PosInTerm.TOP_LEVEL) {
139:                    // if no applicable taclet is found we relax the target position a bit
140:                    applicableApps = getAllApplicableApps(sourcePos,
141:                            PosInSequent.createCfmaPos(targetPos
142:                                    .getPosInOccurrence().up()), services);
143:                }
144:
145:                // in case of an equal source and target position the selection list is shown 
146:                // even if only one rule is applicable in order to avoid an accidently 
147:                // rule appliciation of replace_knwon_* rules and entering
148:                // the hell of non-confluence..       
149:                final boolean equalTargetPosition = sourcePos
150:                        .getPosInOccurrence().equals(
151:                                targetPos.getPosInOccurrence());
152:
153:                if (!equalTargetPosition && applicableApps.size() == 1) {
154:                    execute(applicableApps.head());
155:                } else if (applicableApps.size() >= 1) {
156:                    // open a pop up menu for user selection
157:                    SimpleTacletSelectionMenu menu = new SimpleTacletSelectionMenu(
158:                            applicableApps, seqView.mediator()
159:                                    .getNotationInfo(), new PopupListener());
160:
161:                    JPopupMenu pm = menu.getPopupMenu();
162:                    pm.show(seqView, (int) dropLocation.getX(),
163:                            (int) dropLocation.getY());
164:                } else {
165:                    // no rule applicable
166:                    event.rejectDrop();
167:                    return;
168:                }
169:                event.getDropTargetContext().dropComplete(true);
170:            }
171:
172:            /**
173:             * retrieves all drag'n drop instantiable taclet applications
174:             * @param sourcePos the PosInSequent where the drag started
175:             * @param targetPos the PosInSequent where the drop occured     
176:             * @param services theServices providing access to the program model  
177:             * @return all drag'n drop instantiable taclet applications
178:             */
179:            private ListOfPosTacletApp getAllApplicableApps(
180:                    final PosInSequent sourcePos, final PosInSequent targetPos,
181:                    final Services services) {
182:                final Sequent sequent = seqView.mediator().getSelectedGoal()
183:                        .sequent();
184:
185:                final Constraint userConstraint = seqView.mediator()
186:                        .getUserConstraint().getConstraint();
187:                ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
188:                if (targetPos.isSequent()) {
189:                    // collects all applicable taclets at the source position
190:                    // which have an addrule section
191:                    applicableApps = applicableApps
192:                            .prepend(completeIfInstantiations(
193:                                    getApplicableTaclets(
194:                                            sourcePos,
195:                                            TacletFilter.TACLET_WITH_NO_IF_FIND_AND_ADDRULE),
196:                                    sequent, targetPos.getPosInOccurrence(),
197:                                    userConstraint, services));
198:                } else {
199:                    if (ProofSettings.DEFAULT_SETTINGS.getGeneralSettings()
200:                            .isDndDirectionSensitive()) {
201:                        applicableApps = applicableApps
202:                                .prepend(getDirectionDependentApps(sourcePos,
203:                                        targetPos, services, sequent,
204:                                        userConstraint));
205:                    } else {
206:                        applicableApps = applicableApps
207:                                .prepend(getDirectionIndependentApps(sourcePos,
208:                                        targetPos, services, sequent,
209:                                        userConstraint));
210:                    }
211:                }
212:                return applicableApps;
213:            }
214:
215:            /**
216:             * returns all applicable apps respecting direction information in drag an drop 
217:             * @param sourcePos PosInSequent where the drag gesture started
218:             * @param targetPos PosInSequent where the drop action took place
219:             * @param services the Services
220:             * @param sequent the Sequent 
221:             * @param userConstraint the user Constraint 
222:             * @return  all applicable apps respecting direction information in drag an drop
223:             */
224:            private ListOfPosTacletApp getDirectionDependentApps(
225:                    final PosInSequent sourcePos, final PosInSequent targetPos,
226:                    final Services services, final Sequent sequent,
227:                    final Constraint userConstraint) {
228:
229:                ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
230:                // all applicable taclets where the drag source has been interpreted
231:                // as
232:                // the find part and the drop position as the one of the
233:                // in this case only taclets with no replacewith part are considered
234:                applicableApps = applicableApps
235:                        .prepend(completeIfInstantiations(
236:                                getApplicableTaclets(
237:                                        sourcePos,
238:                                        TacletFilter.TACLET_WITH_IF_FIND_AND_NO_REPLACEWITH),
239:                                sequent, targetPos.getPosInOccurrence(),
240:                                userConstraint, services));
241:
242:                // switch source and target interpretation
243:                // source is now the "If" instantiation and target the one of the
244:                // find part in this case only the taclets with at least one
245:                // replacewith part are considered
246:                applicableApps = applicableApps
247:                        .prepend(completeIfInstantiations(
248:                                getApplicableTaclets(
249:                                        targetPos,
250:                                        TacletFilter.TACLET_WITH_IF_FIND_AND_REPLACEWITH),
251:                                sequent, sourcePos.getPosInOccurrence(),
252:                                userConstraint, services));
253:
254:                // get those without an if sequent, in these we will try to apply this rule
255:                // if: * one sv instantiation is missing
256:                //     * the term dropped on is a legal instantiation for this sv
257:                applicableApps = applicableApps.prepend(completeInstantiations(
258:                        getApplicableTaclets(sourcePos,
259:                                TacletFilter.TACLET_WITH_NO_IF), targetPos
260:                                .getPosInOccurrence(), services));
261:
262:                return applicableApps;
263:            }
264:
265:            /**
266:             * returns all applicable apps without 
267:             * respecting direction information in drag an drop 
268:             * @param sourcePos PosInSequent where the drag gesture started
269:             * @param targetPos PosInSequent where the drop action took place
270:             * @param services the Services
271:             * @param sequent the Sequent 
272:             * @param userConstraint the user Constraint 
273:             * @return  all applicable apps respecting direction information in drag an drop
274:             */
275:            private ListOfPosTacletApp getDirectionIndependentApps(
276:                    PosInSequent sourcePos, PosInSequent targetPos,
277:                    final Services services, final Sequent sequent,
278:                    final Constraint userConstraint) {
279:
280:                ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
281:
282:                applicableApps = getDirectionDependentApps(sourcePos,
283:                        targetPos, services, sequent, userConstraint).prepend(
284:                        getDirectionDependentApps(targetPos, sourcePos,
285:                                services, sequent, userConstraint));
286:
287:                return applicableApps;
288:            }
289:
290:            /**
291:             * retrieves all taclets applicable on the given position and select those
292:             * that fulfill the given filter condition. The filter selects taclets
293:             * satisfying certain syntactic categories (for example, taclets with at
294:             * least one replacewith in their goal description or those without any
295:             * replacewith).
296:             * 
297:             * @param findPos
298:             *            the PosInSequent specifying the formula/term that has to be
299:             *            matched by the find part of a taclet
300:             * @param filter
301:             *            the TacletFilter specifying syntactic restrictions on the
302:             *            taclets to be returned
303:             * @return the list of taclets which match the term at the given position
304:             *         and satisfy the filter condition
305:             */
306:            private ListOfPosTacletApp getApplicableTaclets(
307:                    PosInSequent findPos, TacletFilter filter) {
308:
309:                if (findPos == null || findPos.isSequent()) {
310:                    return SLListOfPosTacletApp.EMPTY_LIST;
311:                }
312:
313:                ListOfTacletApp allTacletsAtFindPosition = SLListOfTacletApp.EMPTY_LIST;
314:
315:                final IteratorOfTacletApp it = seqView.mediator()
316:                        .getFindTaclet(findPos).iterator();
317:                // if in replaceWithMode only apps that contain at least one replacewith
318:                // are collected. Otherwise only those without a replacewith.
319:                while (it.hasNext()) {
320:                    final TacletApp app = it.next();
321:                    if (filter.satisfiesFilterCondition(app.taclet())) {
322:                        allTacletsAtFindPosition = allTacletsAtFindPosition
323:                                .prepend(app);
324:                    }
325:                }
326:
327:                return addPositionInformation(allTacletsAtFindPosition, findPos
328:                        .getPosInOccurrence());
329:            }
330:
331:            /**
332:             * the taclet applications is given the correct position information where
333:             * their "find" has been matched
334:             * 
335:             * @param tacletApps
336:             *            the ListOfTacletApp with taclet applications to be enriched by
337:             *            position information
338:             * @param findPos
339:             *            the PosInOccurrence against which the find part has been
340:             *            matched
341:             * @return the taclet apps as given in <tt>tacletApps</tt> but with
342:             *         position information
343:             */
344:            private ListOfPosTacletApp addPositionInformation(
345:                    ListOfTacletApp tacletApps, PosInOccurrence findPos) {
346:
347:                ListOfPosTacletApp applicableApps = SLListOfPosTacletApp.EMPTY_LIST;
348:                IteratorOfTacletApp it = tacletApps.iterator();
349:                while (it.hasNext()) {
350:                    TacletApp app = it.next();
351:                    if (app instanceof  NoPosTacletApp) {
352:                        app = PosTacletApp.createPosTacletApp((FindTaclet) app
353:                                .taclet(), app.matchConditions(), findPos);
354:                    }
355:                    applicableApps = applicableApps.prepend((PosTacletApp) app);
356:                }
357:                return applicableApps;
358:            }
359:
360:            /**
361:             * tries to complete the (partial) taclet instantantiation of the
362:             * applications given in <tt>apps</tt>. The resulting applications are
363:             * returned. The given apps must have either all an if part or none of them.
364:             * 
365:             * @param apps
366:             *            the ListOfPosTacletApp with all apps whose if sequent has to
367:             *            be matched against the formula specified by the pair
368:             *            <tt>seq</tt> and <tt>ifPIO</tt>
369:             * @param seq
370:             *            the Sequent to which the position information in <tt>ifPIO<tt>
371:             * is relative to
372:             * @param ifPIO the PosInOccurrence describing the position of the term to 
373:             * be matched against the if sequent of the taclets
374:             * @param userConstraint the Constraint describing user instantiations of
375:             * metavariables
376:             * @param services the Services 
377:             * @return the ListOfPosTacletApp that have been matched successfully
378:             */
379:            private ListOfPosTacletApp completeIfInstantiations(
380:                    ListOfPosTacletApp apps, Sequent seq,
381:                    PosInOccurrence ifPIO, Constraint userConstraint,
382:                    Services services) {
383:
384:                ListOfPosTacletApp result = SLListOfPosTacletApp.EMPTY_LIST;
385:
386:                final ListOfIfFormulaInstantiation ifFmlInst;
387:
388:                if (ifPIO == null || !ifPIO.isTopLevel()) {
389:                    // if formula have to be top level formulas
390:                    // TODO: should update prefix be allowed?
391:                    ifFmlInst = null;
392:                } else {
393:                    final IfFormulaInstSeq ifInst = new IfFormulaInstSeq(seq,
394:                            ifPIO.isInAntec(), ifPIO.constrainedFormula());
395:                    ifFmlInst = SLListOfIfFormulaInstantiation.EMPTY_LIST
396:                            .prepend(ifInst);
397:                }
398:
399:                final IteratorOfPosTacletApp it = apps.iterator();
400:                while (it.hasNext()) {
401:                    PosTacletApp app = it.next();
402:
403:                    final Sequent ifSequent = app.taclet().ifSequent();
404:                    if (ifSequent != null && !ifSequent.isEmpty()) {
405:                        if (ifSequent.size() != 1) {
406:                            // currently dnd is only supported for taclets with exact one formula
407:                            // in the if sequent
408:                            app = null;
409:                        } else if (ifFmlInst == null) {
410:                            // as either all taclets have an if sequent or none
411:                            // we can exit here
412:                            return SLListOfPosTacletApp.EMPTY_LIST;
413:                        } else {
414:                            // the right side is not checked in tacletapp
415:                            // not sure where to incorporate the check...
416:                            if (((IfFormulaInstSeq) ifFmlInst.head()).inAntec() == (ifSequent
417:                                    .succedent().size() == 0)) {
418:                                app = (PosTacletApp) app
419:                                        .setIfFormulaInstantiations(ifFmlInst,
420:                                                services, userConstraint);
421:                            }
422:                        }
423:                    }
424:                    if (app != null && app.complete()) {
425:                        //allow use of sufficientlyComplete here?
426:                        result = result.prepend(app);
427:                    }
428:                }
429:                return result;
430:            }
431:
432:            /**
433:             * tries to complete the (partial) taclet instantantiation of the
434:             * applications given in <tt>apps</tt>. The resulting applications are
435:             * returned. 
436:             * 
437:             * @param apps
438:             *            the ListOfPosTacletApp with all apps whose if sequent has to
439:             *            be matched against the formula specified by the pair
440:             *            <tt>seq</tt> and <tt>ifPIO</tt>
441:             * @param seq
442:             *            the Sequent to which the position information in <tt>ifPIO<tt>
443:             * is relative to
444:             * @param missingSVPIO the PosInOccurrence describing the position of the term an 
445:             * uninstantiated SV will be matched against 
446:             * @param userConstraint the Constraint describing user instantiations of
447:             * metavariables
448:             * @param services the Services 
449:             * @return the ListOfPosTacletApp that have been matched successfully
450:             */
451:            private ListOfPosTacletApp completeInstantiations(
452:                    ListOfPosTacletApp apps, PosInOccurrence missingSVPIO,
453:                    Services services) {
454:
455:                ListOfPosTacletApp result = SLListOfPosTacletApp.EMPTY_LIST;
456:                if (missingSVPIO == null) {
457:                    return SLListOfPosTacletApp.EMPTY_LIST;
458:                }
459:
460:                final IteratorOfPosTacletApp it = apps.iterator();
461:                while (it.hasNext()) {
462:                    PosTacletApp app = it.next();
463:
464:                    final SchemaVariable missingSV;
465:                    final Sequent ifSequent = app.taclet().ifSequent();
466:
467:                    if ((ifSequent != null && !ifSequent.isEmpty())
468:                            || app.uninstantiatedVars().size() != 1) {
469:                        continue;
470:                    } else {
471:                        missingSV = app.uninstantiatedVars().iterator().next();
472:                    }
473:                    try {
474:                        app = (PosTacletApp) app.addCheckedInstantiation(
475:                                missingSV, missingSVPIO.subTerm(), services,
476:                                true);
477:                    } catch (IllegalInstantiationException ie) {
478:                        app = null;
479:                    }
480:
481:                    if (app != null && app.sufficientlyComplete()) {
482:                        result = result.prepend(app);
483:                    }
484:                }
485:                return result;
486:            }
487:
488:            /**
489:             * applies the given app
490:             * 
491:             * @param app
492:             *            the PosTacletApp to be applied
493:             */
494:            private void execute(PosTacletApp app) {
495:                if (app == null) {
496:                    return;
497:                }
498:                final KeYMediator mediator = seqView.mediator();
499:                mediator.applyInteractive(app, mediator.getSelectedGoal());
500:            }
501:
502:            /**
503:             * This popup listener listens to the taclet app selection listener and
504:             * executes the selected app if necessary
505:             */
506:            private class PopupListener implements  ActionListener {
507:
508:                /*
509:                 * (non-Javadoc)
510:                 * 
511:                 * @see java.awt.event.ActionListener#actionPerformed(java.awt.event.ActionEvent)
512:                 */
513:                public void actionPerformed(ActionEvent e) {
514:                    if (e.getSource() instanceof  DefaultTacletMenuItem) {
515:                        final TacletMenuItem item = (TacletMenuItem) e
516:                                .getSource();
517:                        DragNDropInstantiator.this .execute((PosTacletApp) item
518:                                .connectedTo());
519:                    }
520:                }
521:            }
522:
523:            /**
524:             * This interface is impemented by filters selecting certain kinds of
525:             * taclets depending on their syntactic structure
526:             */
527:            protected interface TacletFilter {
528:
529:                /**
530:                 * This filter selects all Taclet which have an <tt>assumes</tt>,
531:                 * <tt>find</tt> and at least one <tt>replacewith</tt> part.
532:                 */
533:                TacletFilter TACLET_WITH_IF_FIND_AND_REPLACEWITH = new TacletWithIfFindAndReplacewith();
534:
535:                /**
536:                 * This filter selects all Taclet which have an <tt>assumes</tt>,
537:                 * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part.
538:                 */
539:                TacletFilter TACLET_WITH_IF_FIND_AND_NO_REPLACEWITH = new TacletWithIfFindAndNoReplacewith();
540:
541:                /**
542:                 * This filter selects all Taclet which have an <tt>assumes</tt>,
543:                 * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part.
544:                 */
545:                TacletFilter TACLET_WITH_NO_IF_FIND_AND_ADDRULE = new TacletWithNoIfFindAndAddrule();
546:
547:                /**
548:                 * This filter selects all Taclets which have no <tt>assumes</tt>,
549:                 * sequent but a <tt>find</tt>part.
550:                 */
551:                TacletFilter TACLET_WITH_NO_IF = new TacletWithNoIf();
552:
553:                /**
554:                 * checks if the taclet satisfies certain syntactic criterias
555:                 * 
556:                 * @param taclet
557:                 *            the Taclet to be tested
558:                 * @return true if filter condition is fulfilled
559:                 */
560:                boolean satisfiesFilterCondition(Taclet taclet);
561:
562:                /**
563:                 * This filter selects all Taclet which have an <tt>assumes</tt>,
564:                 * <tt>find</tt> and at least one <tt>replacewith</tt> part.
565:                 */
566:                class TacletWithIfFindAndReplacewith implements  TacletFilter {
567:
568:                    private TacletWithIfFindAndReplacewith() {
569:                    }
570:
571:                    /**
572:                     * tests if the given taclet consists of an <tt>assumes</tt>,
573:                     * <tt>find</tt> and <tt>replacewith</tt> part and returns true
574:                     * if the test is positive
575:                     */
576:                    public boolean satisfiesFilterCondition(Taclet taclet) {
577:                        return taclet.ifSequent() != null
578:                                && !taclet.ifSequent().isEmpty()
579:                                && taclet instanceof  FindTaclet
580:                                && taclet.hasReplaceWith();
581:                    }
582:                }
583:
584:                /**
585:                 * This filter selects all Taclet which have an <tt>assumes</tt>,
586:                 * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part.
587:                 */
588:                class TacletWithIfFindAndNoReplacewith implements  TacletFilter {
589:
590:                    private TacletWithIfFindAndNoReplacewith() {
591:                    }
592:
593:                    /**
594:                     * tests if the given taclet consists of an <tt>assumes</tt>,
595:                     * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part and
596:                     * returns true if the test is positive
597:                     */
598:                    public boolean satisfiesFilterCondition(Taclet taclet) {
599:                        return taclet.ifSequent() != null
600:                                && !taclet.ifSequent().isEmpty()
601:                                && taclet instanceof  FindTaclet
602:                                && !taclet.hasReplaceWith();
603:                    }
604:                }
605:
606:                /**
607:                 * This filter selects all Taclet which have no <tt>assumes</tt>, but a
608:                 * <tt>find</tt> and at least one <tt>addrule</tt> section.
609:                 */
610:                class TacletWithNoIfFindAndAddrule implements  TacletFilter {
611:
612:                    private TacletWithNoIfFindAndAddrule() {
613:                    }
614:
615:                    /**
616:                     * tests if the goal templates contain at least one addrule section
617:                     * 
618:                     * @param goalDescriptions
619:                     *            the ListOfTacletGoalTemplate to be looked through
620:                     * @return true if an addrule section has been found
621:                     */
622:                    private boolean goalTemplatesContainAddrules(
623:                            ListOfTacletGoalTemplate goalDescriptions) {
624:                        final IteratorOfTacletGoalTemplate it = goalDescriptions
625:                                .iterator();
626:                        while (it.hasNext()) {
627:                            final TacletGoalTemplate tgt = it.next();
628:                            if (tgt.rules().size() >= 1) {
629:                                return true;
630:                            }
631:                        }
632:
633:                        return false;
634:                    }
635:
636:                    /**
637:                     * tests if the given taclet consists of an <tt>assume</tt>,
638:                     * <tt>find</tt> and <em>no</em> <tt>replacewith</tt> part and
639:                     * returns true if the test is positive
640:                     */
641:                    public boolean satisfiesFilterCondition(Taclet taclet) {
642:                        // TODO: the null checks should be unneccessary
643:                        return (taclet.ifSequent() == null || taclet
644:                                .ifSequent().isEmpty())
645:                                && taclet instanceof  FindTaclet
646:                                && goalTemplatesContainAddrules(taclet
647:                                        .goalTemplates());
648:                    }
649:                }
650:
651:                /**
652:                 * This filter selects all Taclet which have no <tt>assume</tt>, but a
653:                 * <tt>find</tt>.
654:                 */
655:                class TacletWithNoIf implements  TacletFilter {
656:
657:                    private TacletWithNoIf() {
658:                    }
659:
660:                    /**
661:                     * checks if the taclet has a find part and no assumes sequent 
662:                     */
663:                    public boolean satisfiesFilterCondition(Taclet taclet) {
664:                        // TODO: the null checks should be unneccessary
665:                        final Sequent ifSequent = taclet.ifSequent();
666:                        return ((ifSequent == null || ifSequent.isEmpty()) && taclet instanceof  FindTaclet);
667:
668:                    }
669:
670:                }
671:
672:            }
673:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.