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-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof;
019:
020: import java.io.StringReader;
021: import java.util.Vector;
022:
023: import javax.swing.table.AbstractTableModel;
024:
025: import de.uka.ilkd.key.collection.ListOfString;
026: import de.uka.ilkd.key.collection.SLListOfString;
027: import de.uka.ilkd.key.java.*;
028: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
029: import de.uka.ilkd.key.logic.*;
030: import de.uka.ilkd.key.logic.op.*;
031: import de.uka.ilkd.key.logic.sort.ArraySort;
032: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
033: import de.uka.ilkd.key.logic.sort.Sort;
034: import de.uka.ilkd.key.parser.*;
035: import de.uka.ilkd.key.parser.Location;
036: import de.uka.ilkd.key.pp.AbbrevMap;
037: import de.uka.ilkd.key.rule.NewVarcond;
038: import de.uka.ilkd.key.rule.TacletApp;
039: import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
040: import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
041: import de.uka.ilkd.key.rule.inst.RigidnessException;
042: import de.uka.ilkd.key.rule.inst.SortException;
043:
044: public class TacletInstantiationsTableModel extends AbstractTableModel {
045:
046: /** the instantiations entries */
047: private Vector entries;
048: /** the related rule application */
049: private final TacletApp originalApp;
050: /** the integer defines the row until which no editing is possible */
051: private int noEditRow;
052: /** universal namespace of variables, minimum for input in a row */
053: private NamespaceSet nss;
054: /** the java service object */
055: private Services services;
056: /** the abbreviationmap */
057: private AbbrevMap scm;
058: /** the current goal */
059: private Goal goal;
060: /** variable namer */
061: private VariableNamer varNamer;
062: /** proposers to ask when instantiating a schema variable */
063: private InstantiationProposerCollection instantiationProposers;
064:
065: /** create new data model for tree
066: * @param app the TacletApp where to get the necessary entries
067: */
068: public TacletInstantiationsTableModel(TacletApp app,
069: Services services, NamespaceSet nss, AbbrevMap scm,
070: Goal goal) {
071: this .originalApp = app;
072:
073: this .nss = nss;
074: this .services = services;
075: this .scm = scm;
076: this .goal = goal;
077: this .varNamer = services.getVariableNamer();
078:
079: instantiationProposers = new InstantiationProposerCollection();
080: instantiationProposers.add(LoopInvariantProposer.DEFAULT);
081: instantiationProposers.add(varNamer);
082: instantiationProposers.add(VariableNameProposer.DEFAULT);
083:
084: entries = createEntryArray(app);
085: }
086:
087: /**
088: * returns the set of namespaces
089: */
090: public NamespaceSet namespaces() {
091: return nss;
092: }
093:
094: /** creates a Vector with the row entries of the table
095: */
096: private Vector createEntryArray(TacletApp tacletApp) {
097: Vector rowVec = new Vector();
098: IteratorOfSchemaVariable it = tacletApp.instantiations()
099: .svIterator();
100: int count = 0;
101:
102: while (it.hasNext()) {
103: SchemaVariable sv = it.next();
104: Object[] column = new Object[2];
105: column[0] = sv;
106: column[1] = ProofSaver.printAnything(tacletApp
107: .instantiations().getInstantiation(sv), services);
108: rowVec.add(column);
109: count++;
110: }
111:
112: noEditRow = count - 1;
113:
114: IteratorOfSchemaVariable varIt = tacletApp.uninstantiatedVars()
115: .iterator();
116: ListOfString proposals = SLListOfString.EMPTY_LIST;
117:
118: while (varIt.hasNext()) {
119: Object[] column = new Object[2];
120: SchemaVariable var = varIt.next();
121:
122: if (!tacletApp.taclet().getIfFindVariables().contains(var)) {
123: column[0] = var;
124:
125: // create an appropriate and unique proposal for the name ...
126: String proposal = instantiationProposers.getProposal(
127: tacletApp, var, services, goal.node(),
128: proposals);
129:
130: if (proposal != null) {
131: // A proposal is available ...
132: column[1] = proposal;
133: proposals = proposals.append(proposal);
134: }
135:
136: rowVec.add(column);
137: }
138: }
139:
140: return rowVec;
141: }
142:
143: /** adds an instantiation of a schemavariable */
144: public void addInstantiationEntry(int row, Term instantiation) {
145: ((Object[]) entries.get(row))[1] = instantiation;
146: }
147:
148: /** return the rule application which is the table models base
149: * @return the Ruleapp
150: */
151: public TacletApp application() {
152: return originalApp;
153: }
154:
155: /** number of colums
156: * @return number of colums
157: */
158: public int getColumnCount() {
159: return 2;
160: }
161:
162: /** number of rows
163: * @return number of rows
164: */
165: public int getRowCount() {
166: return entries.size();
167: }
168:
169: /** returns true iff an instantiation is missing
170: * @return true iff an instantiation is missing
171: */
172: public boolean isCellEditable(int rowIndex, int columnIndex) {
173: return (rowIndex > noEditRow) && (columnIndex > 0);
174: }
175:
176: /** parses the given string that represents the term (or formula)
177: * using the given variable namespace and the default namespaces
178: * for functions and sorts
179: * @param s the String to parse
180: * @param sort the expected sort
181: * @param varNS the variable namespace
182: */
183: public Term parseTerm(String s, Namespace varNS)
184: throws ParserException {
185: NamespaceSet copy = nss.copy();
186: copy.setVariables(varNS);
187: Term term = TermParserFactory.createInstance().parse(
188: new StringReader(s), null, services, copy, scm);
189: return term;
190: }
191:
192: /**
193: * Parse the declaration of an identifier (i.e. the declaration of
194: * a variable or skolem function)
195: */
196: public IdDeclaration parseIdDeclaration(String s)
197: throws ParserException {
198: try {
199: KeYParser parser = new KeYParser(ParserMode.DECLARATION,
200: new KeYLexer(new StringReader(s), services
201: .getExceptionHandler()), "", services, // should not be needed
202: nss);
203: return parser.id_declaration();
204: } catch (antlr.RecognitionException re) {
205: throw new ParserException(re.getMessage(), new Location(re
206: .getFilename(), re.getLine(), re.getColumn()));
207: } catch (antlr.TokenStreamException tse) {
208: throw new ParserException(tse.getMessage(), null);
209: }
210: }
211:
212: /**
213: * throws an exception iff no input in indicated row, and no
214: * metavariable instantiation is possible
215: *
216: */
217:
218: private void checkNeededInputAvailable(int irow)
219: throws MissingInstantiationException {
220:
221: final int icol = 1;
222:
223: if ((getValueAt(irow, icol) == null || ((String) getValueAt(
224: irow, icol)).length() == 0)
225: && !originalApp.sufficientlyComplete()
226: && !originalApp
227: .canUseMVAPriori((SchemaVariable) getValueAt(
228: irow, 0))) {
229: throw new MissingInstantiationException(""
230: + getValueAt(irow, 0), irow, 0, false);
231: }
232: }
233:
234: /**
235: * @return true iff this row is not empty (i.e. a string of data
236: * is available)
237: */
238: private boolean isInputAvailable(int irow) {
239: if (((SchemaVariable) getValueAt(irow, 0)).isListSV())
240: return true;
241: return getValueAt(irow, 1) != null
242: && ((String) getValueAt(irow, 1)).length() != 0;
243: }
244:
245: private SetOfLocationDescriptor parseLocationList(int irow)
246: throws ParserException {
247: String instantiation = (String) getValueAt(irow, 1);
248: if (instantiation == null) {
249: instantiation = "";
250: }
251: SetOfLocationDescriptor result = null;
252: try {
253: result = (new KeYParser(ParserMode.TERM, new KeYLexer(
254: new StringReader(instantiation), services
255: .getExceptionHandler()), null,
256: TermFactory.DEFAULT, null, services, nss, scm))
257: .location_list();
258: } catch (antlr.RecognitionException re) {
259: throw new ParserException(re.getMessage(), new Location(re
260: .getFilename(), re.getLine(), re.getColumn()));
261: } catch (antlr.TokenStreamException tse) {
262: throw new ParserException(tse.getMessage(), null);
263: }
264: return result;
265: }
266:
267: /**
268: * parses the indicated row and returns a Term corresponding to the
269: * entry in the row
270: *
271: * @param irow the row to be parsed
272: * @return the parsed term
273: */
274: private Term parseRow(int irow, Namespace varNS)
275: throws SVInstantiationParserException,
276: MissingInstantiationException {
277:
278: String instantiation = (String) getValueAt(irow, 1);
279:
280: if (instantiation == null || "".equals(instantiation)) {
281: throw new MissingInstantiationException("", irow, 0, false);
282: }
283:
284: try {
285: return parseTerm(instantiation, varNS);
286: } catch (ParserException pe) {
287: Location loc = pe.getLocation();
288: if (loc != null) {
289: throw new SVInstantiationParserException(
290: instantiation,
291: irow + (loc.getLine() <= 0 ? 0 : loc.getLine()),
292: loc.getColumn(), pe.getMessage(), false);
293: } else {
294: throw new SVInstantiationParserException(instantiation,
295: irow, -1, pe.getMessage(), false);
296: }
297: }
298: }
299:
300: /**
301: * parses the indicated row and returns a identifier declaration
302: * corresponding to the entry in the row
303: *
304: * @param irow the row to be parsed
305: * @return the parsed declaration
306: */
307: private IdDeclaration parseIdDeclaration(int irow)
308: throws SVInstantiationParserException,
309: MissingInstantiationException {
310:
311: String instantiation = (String) getValueAt(irow, 1);
312:
313: if (instantiation == null || "".equals(instantiation)) {
314: throw new MissingInstantiationException("", irow, 0, false);
315: }
316:
317: try {
318: return parseIdDeclaration(instantiation);
319: } catch (ParserException pe) {
320: Location loc = pe.getLocation();
321: if (loc != null) {
322: throw new SVInstantiationParserException(
323: instantiation,
324: irow + (loc.getLine() <= 0 ? 0 : loc.getLine()),
325: loc.getColumn(), pe.getMessage(), false);
326: } else {
327: throw new SVInstantiationParserException(instantiation,
328: irow, -1, pe.getMessage(), false);
329: }
330: }
331: }
332:
333: public static ProgramElement getProgramElement(TacletApp app,
334: String instantiation, SchemaVariable sv, Services services) {
335: Sort svSort = ((SortedSchemaVariable) sv).sort();
336: if (svSort == ProgramSVSort.LABEL) {
337: return VariableNamer.parseName(instantiation);
338: } else if (svSort == ProgramSVSort.VARIABLE) {
339: NewVarcond nvc = app.taclet().varDeclaredNew(sv);
340: if (nvc != null) {
341: KeYJavaType kjt;
342: Object o = nvc.getSortDefiningObject();
343: JavaInfo javaInfo = services.getJavaInfo();
344: if (o instanceof SchemaVariable) {
345: final TypeConverter tc = services
346: .getTypeConverter();
347: final SchemaVariable peerSV = (SchemaVariable) o;
348: final Object peerInst = app.instantiations()
349: .getInstantiation(peerSV);
350: Expression peerInstExpr;
351: if (peerInst instanceof Term) {
352: peerInstExpr = tc
353: .convertToProgramElement((Term) peerInst);
354: } else {
355: peerInstExpr = (Expression) peerInst;
356: }
357: kjt = tc.getKeYJavaType(peerInstExpr, app
358: .instantiations().getContextInstantiation()
359: .activeStatementContext());
360: if (nvc.isDefinedByElementSort()) {
361: Sort s = kjt.getSort();
362: if (s instanceof ArraySort)
363: s = ((ArraySort) s).elementSort();
364: kjt = javaInfo.getKeYJavaType(s);
365: }
366: } else {
367: kjt = javaInfo.getKeYJavaType((Sort) o);
368: }
369: return new LocationVariable(VariableNamer
370: .parseName(instantiation), kjt);
371: }
372: }
373: return null;
374: }
375:
376: /**
377: * parses the indicated row and returns the ProgramElement
378: * corresponding to the entry in the row
379: * @param irow the row to be parsed
380: * @return the parsed term
381: */
382: private ProgramElement parseRow(int irow)
383: throws SVInstantiationParserException {
384:
385: String instantiation = (String) getValueAt(irow, 1);
386: SortedSchemaVariable sv = (SortedSchemaVariable) getValueAt(
387: irow, 0);
388:
389: if (!varNamer.isUniqueNameForSchemaVariable(instantiation, sv,
390: originalApp.posInOccurrence(), originalApp
391: .instantiations().getContextInstantiation()
392: .prefix())) {
393: throw new SVInstantiationParserException(instantiation,
394: irow, 0, "Name is already in use.", false);
395: }
396:
397: ContextInstantiationEntry contextInstantiation = originalApp
398: .instantiations().getContextInstantiation();
399:
400: final PosInProgram prefix;
401: if (contextInstantiation == null) {
402: prefix = PosInProgram.TOP;
403: } else {
404: prefix = contextInstantiation.prefix();
405: }
406:
407: if (!varNamer.isUniqueNameForSchemaVariable(instantiation, sv,
408: originalApp.posInOccurrence(), prefix)) {
409: throw new SVInstantiationParserException(instantiation,
410: irow, 0, "Name is already in use.", false);
411: }
412:
413: ProgramElement pe = getProgramElement(originalApp,
414: instantiation, sv, services);
415: if (pe == null) {
416: throw new SVInstantiationParserException(
417: instantiation,
418: irow,
419: -1,
420: "Unexpected sort: "
421: + sv.sort()
422: + "."
423: + "Label SV or a program variable SV expected"
424: + " declared as new.", false);
425: }
426: return pe;
427: }
428:
429: /**
430: * creates new rule app with all inserted instantiations in the variable
431: * instantiations table
432: * @throws SVInstantiationException if the instantiation is incorrect
433: */
434: public TacletApp createTacletAppFromVarInsts()
435: throws SVInstantiationException {
436:
437: final TermBuilder tb = TermBuilder.DF;
438: TacletApp result = originalApp;
439: SchemaVariable sv = null;
440: Sort sort = null;
441: int irow = 0;
442:
443: try {
444:
445: for (irow = noEditRow + 1; irow < entries.size(); irow++) {
446: checkNeededInputAvailable(irow);
447: sv = (SchemaVariable) getValueAt(irow, 0);
448: sort = null;
449: if (sv.isVariableSV() || sv.isSkolemTermSV()) {
450: IdDeclaration idd = parseIdDeclaration(irow);
451: sort = idd.getSort();
452: if (sort == null) {
453: try {
454: sort = result.getRealSort(sv, services);
455: } catch (SortException e) {
456: throw new MissingSortException("" + sv,
457: irow, 0);
458: }
459: }
460:
461: if (sv.isVariableSV()) {
462: LogicVariable lv = new LogicVariable(new Name(
463: idd.getName()), sort);
464: result = result.addCheckedInstantiation(sv, tb
465: .var(lv), services, true);
466: } else {
467: // sv.isSkolemTermSV ()
468:
469: Named n = namespaces().lookupLogicSymbol(
470: new Name(idd.getName()));
471: if (n == null) {
472: result = result.createSkolemConstant(idd
473: .getName(), sv, sort, true);
474: } else {
475: throw new SVInstantiationParserException(
476: idd.getName(), irow, 1,
477: "Name already in use.", false);
478: }
479: }
480: } else if (sv.isProgramSV()) {
481: final ProgramElement pe = parseRow(irow);
482: result = result.addCheckedInstantiation(sv, pe,
483: services, true);
484: }
485: }
486: SchemaVariable problemVarSV = result.varSVNameConflict();
487:
488: if (problemVarSV != null) {
489: throw new SVInstantiationParserException("",
490: getSVRow(problemVarSV), 0,
491: "Ambiguous instantiation of schema variable "
492: + problemVarSV, false);
493: }
494:
495: for (irow = noEditRow + 1; irow < entries.size(); irow++) {
496:
497: if (!isInputAvailable(irow))
498: continue;
499:
500: sv = (SchemaVariable) getValueAt(irow, 0);
501:
502: if (result.isDependingOnModifiesSV(sv)
503: || sv.isVariableSV() || sv.isSkolemTermSV()
504: || result.instantiations().isInstantiated(sv))
505: continue;
506:
507: sort = null;
508:
509: if (sv.isProgramSV()) {
510: final ProgramElement pe = parseRow(irow);
511: result = result.addCheckedInstantiation(sv, pe,
512: services, true);
513: } else if (sv.isListSV()) {
514: try {
515: SetOfLocationDescriptor s = parseLocationList(irow);
516: result = result.addInstantiation(sv, s
517: .toArray(), true);
518: } catch (ParserException pe) {
519: Location loc = pe.getLocation();
520: if (loc != null) {
521: throw new SVInstantiationParserException(
522: (String) getValueAt(irow, 1), irow
523: + (loc.getLine() <= 0 ? 0
524: : loc.getLine()),
525: loc.getColumn(), pe.getMessage(),
526: false);
527: } else {
528: throw new SVInstantiationParserException(
529: (String) getValueAt(irow, 1), irow,
530: -1, pe.getMessage(), false);
531: }
532: }
533: } else if (sv.isNameSV()) {
534: result = result.addInstantiation(sv, tb.tt(), true);
535: } else {
536: if (!result.isDependingOnModifiesSV(sv)
537: && isInputAvailable(irow)) {
538: final Namespace extVarNS = result
539: .extendVarNamespaceForSV(nss
540: .variables(), sv);
541:
542: final Term instance = parseRow(irow, extVarNS);
543: sort = instance.sort();
544:
545: try {
546: result = result.addCheckedInstantiation(sv,
547: instance, services, true);
548: } catch (RigidnessException e) {
549: throw new SVRigidnessException("" + sv,
550: irow, 0);
551: } catch (IllegalInstantiationException iae) {
552: throw new SVInstantiationParserException(
553: (String) getValueAt(irow, 1), irow,
554: -1, iae.getMessage(), false);
555: }
556: }
557: }
558: }
559: } catch (SortException e) {
560: throw new SortMismatchException("" + sv, sort, irow, 0);
561: }
562:
563: return result;
564:
565: }
566:
567: /** sets the Value of the cell */
568: public void setValueAt(Object instantiation, int rowIndex,
569: int columnIndex) {
570: ((Object[]) entries.get(rowIndex))[columnIndex] = instantiation;
571: }
572:
573: /** get value at the specified row and col
574: * @return the value
575: */
576: public Object getValueAt(int row, int col) {
577: return ((Object[]) entries.get(row))[col];
578: }
579:
580: /** returns the index of the row the given Schemavariable stands
581: *@return the index of the row the given Schemavariable stands (-1
582: * if not found)
583: */
584: public int getSVRow(SchemaVariable sv) {
585: for (int i = 0; i < entries.size(); i++) {
586: if (getValueAt(i, 0).equals(sv)) {
587: return i;
588: }
589: }
590: return -1;
591: }
592:
593: public static String getNameProposalForMetavariable(Goal goal,
594: TacletApp p_app, SchemaVariable p_var) {
595: String s = VariableNameProposer
596: .createBaseNameProposalBasedOnCorrespondence(p_app,
597: p_var).toUpperCase();
598: s += "_" + MetavariableDeliverer.mv_Counter(s, goal);
599: return s;
600: }
601:
602: }
|