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: * visitor for <t> execPostOrder </t> of
013: * {@link de.uka.ilkd.key.logic.Term}. Called with that method
014: * on a term, the visitor builds a new term replacing SchemaVariables with their
015: * instantiations that are given as a SVInstantiations object.
016: */package de.uka.ilkd.key.rule;
017:
018: import java.util.*;
019:
020: import de.uka.ilkd.key.java.*;
021: import de.uka.ilkd.key.java.reference.ExecutionContext;
022: import de.uka.ilkd.key.java.visitor.ProgramContextAdder;
023: import de.uka.ilkd.key.java.visitor.ProgramReplaceVisitor;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.ArraySort;
027: import de.uka.ilkd.key.logic.sort.GenericSort;
028: import de.uka.ilkd.key.logic.sort.Sort;
029: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
030: import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
031: import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
032: import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
033: import de.uka.ilkd.key.rule.inst.SVInstantiations;
034: import de.uka.ilkd.key.util.Debug;
035:
036: public class SyntacticalReplaceVisitor extends Visitor {
037:
038: private final SVInstantiations svInst;
039: private final Constraint metavariableInst;
040: private MapFromSchemaVariableToTerm newInstantiations = MapAsListFromSchemaVariableToTerm.EMPTY_MAP;
041: private final boolean forceSVInst;
042: private final Name svInstBasename;
043: private Services services;
044: private Term computedResult = null;
045: private TypeConverter typeConverter = null;
046: private final boolean allowPartialReplacement;
047: private final boolean resolveSubsts;
048:
049: /**
050: * the stack contains the subterms that will be added in the next step of
051: * execPostOrder in Term in order to build the new term. A boolean value
052: * between or under the subterms on the stack indicate that a term using
053: * these subterms should build a new term instead of using the old one,
054: * because one of its subterms has been built, too.
055: */
056: private final Stack subStack; //of Term (and Boolean)
057: private final TermFactory tf = TermFactory.DEFAULT;
058: private final Boolean newMarker = new Boolean(true);
059:
060: /** used to indicate if variables have changed */
061: private final BooleanContainer varsChanged = new BooleanContainer();
062:
063: /** an empty array for resourse optimisation*/
064: private static final QuantifiableVariable[] EMPTY_QUANTIFIABLE_VARS = new QuantifiableVariable[0];
065:
066: /**
067: * @param forceSVInst iff true instantiate uninstantiated SVs by
068: * creating new metavariables or new bound logicvariables
069: */
070: public SyntacticalReplaceVisitor(Services services,
071: SVInstantiations svInst, Constraint metavariableInst,
072: boolean forceSVInst,
073:
074: Name svInstBasename, boolean allowPartialReplacement,
075: boolean resolveSubsts) {
076: this .services = services;
077: this .svInst = svInst;
078: this .metavariableInst = metavariableInst;
079: this .forceSVInst = forceSVInst;
080: this .svInstBasename = svInstBasename;
081: this .allowPartialReplacement = allowPartialReplacement;
082: this .resolveSubsts = resolveSubsts;
083: subStack = new Stack(); // of Term
084: }
085:
086: public SyntacticalReplaceVisitor(Services services,
087: SVInstantiations svInst, Constraint metavariableInst,
088: boolean forceSVInst, Name svInstBasename) {
089: this (services, svInst, metavariableInst, forceSVInst,
090: svInstBasename, false, true);
091: }
092:
093: public SyntacticalReplaceVisitor(Services services,
094: SVInstantiations svInst) {
095: this (services, svInst, Constraint.BOTTOM, false, null, false,
096: true);
097: }
098:
099: public SyntacticalReplaceVisitor(Services services,
100: Constraint metavariableInst) {
101: this (services, SVInstantiations.EMPTY_SVINSTANTIATIONS,
102: metavariableInst, false, null, false, true);
103: }
104:
105: public SyntacticalReplaceVisitor(Services services,
106: SVInstantiations svInst, Constraint metavariableInst) {
107: this (services, svInst, metavariableInst, false, null, false,
108: true);
109: }
110:
111: public SyntacticalReplaceVisitor(Constraint metavariableInst) {
112: this (null, metavariableInst);
113: }
114:
115: private JavaProgramElement addContext(StatementBlock pe) {
116: final ContextInstantiationEntry cie = svInst
117: .getContextInstantiation();
118: if (cie == null) {
119: throw new IllegalStateException("Context should also "
120: + "be instantiated");
121: }
122:
123: if (cie.prefix() != null) {
124: return ProgramContextAdder.INSTANCE.start(
125: (JavaNonTerminalProgramElement) cie
126: .contextProgram(), pe,
127: (ContextStatementBlockInstantiation) cie
128: .getInstantiation());
129: }
130:
131: return pe;
132: }
133:
134: private Services getServices() {
135: if (services == null)
136: services = new Services();
137: return services;
138: }
139:
140: private TypeConverter getTypeConverter() {
141: if (typeConverter == null)
142: typeConverter = getServices().getTypeConverter();
143: return typeConverter;
144: }
145:
146: private JavaBlock replacePrg(SVInstantiations svInst, JavaBlock jb) {
147: if (svInst == SVInstantiations.EMPTY_SVINSTANTIATIONS) {
148: return jb;
149: }
150: ProgramReplaceVisitor trans;
151: ProgramElement result = null;
152:
153: if (jb.program() instanceof ContextStatementBlock) {
154: trans = new ProgramReplaceVisitor(new StatementBlock(
155: ((ContextStatementBlock) jb.program()).getBody()), // TODO
156: getServices(), svInst, allowPartialReplacement);
157: trans.start();
158: result = addContext((StatementBlock) trans.result());
159: } else {
160: trans = new ProgramReplaceVisitor(jb.program(),
161: getServices(), svInst, allowPartialReplacement);
162: trans.start();
163: result = trans.result();
164: }
165: return (result == jb.program()) ? jb : JavaBlock
166: .createJavaBlock((StatementBlock) result);
167: }
168:
169: private Term[] neededSubs(int n) {
170: boolean newTerm = false;
171: Term[] result = new Term[n];
172: for (int i = n - 1; i >= 0; i--) {
173: Object top = subStack.pop();
174: if (top == newMarker) {
175: newTerm = true;
176: top = subStack.pop();
177: }
178: result[i] = (Term) top;
179: }
180: if (newTerm
181: && (subStack.empty() || subStack.peek() != newMarker)) {
182: subStack.push(newMarker);
183: }
184: return result;
185: }
186:
187: /**
188: * Pop the top-most <code>n</code> objects from the subterm stack,
189: * together with possibly interleaving newmarkers, store everything in
190: * <code>store</code>. The top element of the stack will be the last
191: * element of list <code>store</code>
192: */
193: private void popN(int n, LinkedList store) {
194: for (int i = 0; i < n; i++) {
195: store.addFirst(subStack.pop());
196: if (subStack.peek() == newMarker) {
197: store.addFirst(subStack.pop());
198: }
199: }
200: }
201:
202: /**
203: * Push the given objects on the subterm stack, in the order in which they
204: * are returned by the method <code>iterator</code>
205: */
206: private void push(Collection store) {
207: final Iterator it = store.iterator();
208: while (it.hasNext())
209: subStack.push(it.next());
210: }
211:
212: private void pushNew(Object t) {
213: if (subStack.empty() || subStack.peek() != newMarker) {
214: subStack.push(newMarker);
215: }
216: subStack.push(t);
217: }
218:
219: private void pushNewAt(Object[] t, int posFromTop) {
220:
221: final LinkedList store = new LinkedList();
222: popN(posFromTop, store);
223:
224: for (int i = 0; i < t.length; i++) {
225: pushNew(t[i]);
226: }
227:
228: push(store);
229: }
230:
231: private void replaceAt(Object[] t, int posFromTop, int length) {
232:
233: final LinkedList store = new LinkedList();
234: popN(posFromTop, store);
235:
236: // remove
237: popN(length, new LinkedList());
238:
239: // add new
240: for (int i = 0; i < t.length; i++) {
241: pushNew(t[i]);
242: }
243:
244: push(store);
245: }
246:
247: private Term[] peek(int pos, int length) {
248:
249: final Term[] result = new Term[length];
250:
251: final LinkedList store = new LinkedList();
252: popN(pos + length, store);
253:
254: final Iterator it = store.iterator();
255: for (int i = 0; i < length; i++) {
256: Object o = it.next();
257: if (o == newMarker)
258: o = it.next();
259: result[i] = (Term) o;
260: }
261:
262: push(store);
263:
264: return result;
265: }
266:
267: private Term toTerm(Object o) {
268: if (o instanceof Term) {
269: final Term t = (Term) o;
270: if (t.metaVars().size() != 0
271: && !metavariableInst.isBottom()) {
272: // use the visitor recursively for replacing metavariables that
273: // might occur in the term (if possible)
274: final SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
275: metavariableInst);
276: t.execPostOrder(srv);
277: return srv.getTerm();
278: }
279: return t;
280: } else if (o instanceof ProgramElement) {
281: ExecutionContext ec = (svInst.getContextInstantiation() == null) ? null
282: : svInst.getContextInstantiation()
283: .activeStatementContext();
284: return getTypeConverter().convertToLogicElement(
285: (ProgramElement) o, ec);
286: }
287: de.uka.ilkd.key.util.Debug
288: .fail("Wrong instantiation in SRVisitor");
289: return null;
290: }
291:
292: private void updateLocation(Location loc, Term location,
293: int positionInStack, int oldLocationArity, boolean replace) {
294: final Term[] newSubterms = new Term[loc.arity()];
295: for (int j = 0; j < newSubterms.length; j++) {
296: newSubterms[j] = location.sub(j);
297: }
298: if (replace) {
299: replaceAt(newSubterms, positionInStack, oldLocationArity);
300: } else {
301: pushNewAt(newSubterms, positionInStack);
302: }
303: }
304:
305: private IUpdateOperator instantiateUpdateOperator(IUpdateOperator op) {
306: final Location[] newOps = new Location[op.locationCount()];
307: final int locCount = op.locationCount();
308: boolean changed = false;
309: for (int i = 0; i < locCount; i++) {
310: final Location originalOp = op.location(i);
311: if (originalOp instanceof SchemaVariable) {
312: final Object inst = svInst
313: .getInstantiation((SchemaVariable) originalOp);
314: if (!(inst instanceof Operator)) {
315: if (inst == null) {
316: // we have only a partial instantiation
317: // continue with schema
318: newOps[i] = originalOp;
319: } else {
320: final int posInStack = op.arity()
321: - op.locationSubtermsEnd(i);
322: Term instantiation = toTerm(inst);
323: newOps[i] = (Location) instantiation.op();
324: updateLocation(newOps[i], instantiation,
325: posInStack, 0, false);
326: }
327: } else {
328: newOps[i] = (Location) inst;
329: }
330: } else if (originalOp instanceof MetaOperator) {
331: final MetaOperator mop = (MetaOperator) originalOp;
332: final int posInStack = op.arity()
333: - op.locationSubtermsEnd(i);
334:
335: final Term computedLocation = mop.calculate(tf
336: .createMetaTerm(mop, peek(posInStack, mop
337: .arity())), svInst, getServices());
338: newOps[i] = (Location) computedLocation.op();
339:
340: updateLocation(newOps[i], computedLocation, posInStack,
341: mop.arity(), true);
342: } else {
343: if (originalOp instanceof ArrayOp) {
344: final int posInStack = op.arity()
345: - op.locationSubtermsEnd(i);
346: newOps[i] = (Location) instantiateArrayOperator(
347: (ArrayOp) originalOp, posInStack);
348: } else {
349: newOps[i] = (Location) instantiateOperator(originalOp);
350: }
351: }
352: changed = (changed || (newOps[i] != originalOp));
353: }
354:
355: if (!changed)
356: return op;
357:
358: return op.replaceLocations(newOps);
359: }
360:
361: private AttributeOp instantiateAttributeOperator(AttributeOp op) {
362: if (op.attribute() instanceof SchemaVariable) {
363: final IProgramVariable attribute = (ProgramVariable) svInst
364: .getInstantiation((SchemaVariable) op.attribute());
365: if (attribute == null) {
366: // illegal inst. exception required for matchMV to fail
367: throw new IllegalInstantiationException(
368: "No instantiation found for " + op);
369: }
370:
371: if (op instanceof ShadowedOperator) {
372: op = ShadowAttributeOp.getShadowAttributeOp(attribute);
373: } else {
374: op = AttributeOp.getAttributeOp(attribute);
375: }
376: }
377: return op;
378: }
379:
380: private ArrayOp instantiateArrayOperator(ArrayOp op, int pos) {
381: final Sort sortDependingOn = op.getSortDependingOn();
382: final Sort s;
383: if (sortDependingOn == null) {
384: s = peek(pos, op.arity())[0].sort();
385: } else if (sortDependingOn instanceof GenericSort) {
386: s = svInst.getGenericSortInstantiations().getInstantiation(
387: (GenericSort) sortDependingOn);
388: } else {
389: return op;
390: }
391: assert s instanceof ArraySort : "Expected array sort but is "
392: + s;
393: return op instanceof ShadowedOperator ? ShadowArrayOp
394: .getShadowArrayOp(s) : ArrayOp.getArrayOp(s);
395:
396: }
397:
398: private Operator instantiateOperatorSV(OperatorSV op) {
399: Operator newOp = (Operator) svInst.getInstantiation(op);
400: Debug.assertTrue(newOp != null, "No instantiation found for "
401: + op);
402: return newOp;
403: }
404:
405: private Operator instantiateOperator(Operator op) {
406: if (op instanceof OperatorSV) {
407: return instantiateOperatorSV((OperatorSV) op);
408: } else if (op instanceof AttributeOp) {
409: return instantiateAttributeOperator((AttributeOp) op);
410: } else if (op instanceof ArrayOp) {
411: return instantiateArrayOperator((ArrayOp) op, 0);
412: } else if (op instanceof SortDependingSymbol) {
413: return handleSortDependingSymbol(op);
414: } else if (op instanceof IUpdateOperator) {
415: return instantiateUpdateOperator((IUpdateOperator) op);
416: } else if (op instanceof NRFunctionWithExplicitDependencies) {
417: return instantiateNRFunctionWithExplicitDependencies((NRFunctionWithExplicitDependencies) op);
418: } else if (op instanceof SortedSchemaVariable
419: && ((SortedSchemaVariable) op).isListSV()) {
420: return op;
421: } else if (op instanceof SortedSchemaVariable) {
422: return (Operator) svInst
423: .getInstantiation((SchemaVariable) op);
424: }
425: return op;
426: }
427:
428: /**
429: * @param dependencies
430: * @return
431: */
432: private Operator instantiateNRFunctionWithExplicitDependencies(
433: NRFunctionWithExplicitDependencies nrFunc) {
434: final Location[] locs = new Location[nrFunc.dependencies()
435: .size()];
436: final ArrayOfLocation patternDeps = nrFunc.dependencies();
437: boolean instantiationNecessary = false;
438: for (int i = 0; i < locs.length; i++) {
439: Location loc = patternDeps.getLocation(i);
440: if (loc instanceof SchemaVariable) {
441: Object o = svInst
442: .getInstantiation((SchemaVariable) loc);
443: if (o instanceof Term) {
444: loc = (Location) ((Term) o).op();
445: } else {
446: Debug.assertTrue(o instanceof Location);
447: loc = (Location) o;
448: }
449: instantiationNecessary = true;
450: }
451: locs[i] = loc;
452: }
453:
454: if (!instantiationNecessary)
455: return nrFunc;
456:
457: // HACK
458: String name = nrFunc.name().toString();
459: name = name.substring(0, name.indexOf("[") + 1);
460: for (int i = 0; i < locs.length; i++) {
461: name += locs[i].name();
462: name += ";";
463: }
464: name += "]";
465: return NRFunctionWithExplicitDependencies.getSymbol(new Name(
466: name), new ArrayOfLocation(locs));
467: }
468:
469: private ArrayOfQuantifiableVariable[] instantiateBoundVariables(
470: Term visited) {
471: boolean containsBoundVars = false;
472: ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[visited
473: .arity()];
474:
475: for (int i = 0, arity = visited.arity(); i < arity; i++) {
476: final ArrayOfQuantifiableVariable vBoundVars = visited
477: .varsBoundHere(i);
478:
479: final QuantifiableVariable[] newVars = (vBoundVars.size() > 0) ? new QuantifiableVariable[vBoundVars
480: .size()]
481: : EMPTY_QUANTIFIABLE_VARS;
482:
483: for (int j = 0, size = vBoundVars.size(); j < size; j++) {
484: containsBoundVars = true;
485: QuantifiableVariable boundVar = vBoundVars
486: .getQuantifiableVariable(j);
487: if (boundVar instanceof SchemaVariable) {
488: final SortedSchemaVariable boundSchemaVariable = (SortedSchemaVariable) boundVar;
489: if (svInst.isInstantiated(boundSchemaVariable)) {
490: boundVar = ((QuantifiableVariable) ((Term) svInst
491: .getInstantiation(boundSchemaVariable))
492: .op());
493: } else {
494: if (forceSVInst) {
495: boundVar = createTemporaryLV(boundSchemaVariable);
496: } else {
497: // this case may happen for PO generation of
498: // taclets
499: boundVar = boundSchemaVariable;
500: }
501: }
502: varsChanged.setVal(true);
503: }
504: newVars[j] = boundVar;
505: }
506: boundVars[i] = varsChanged.val() ? new ArrayOfQuantifiableVariable(
507: newVars)
508: : vBoundVars;
509: }
510:
511: if (!containsBoundVars) {
512: boundVars = null;
513: }
514: return boundVars;
515: }
516:
517: public void visit(Term visited) {
518: // Sort equality has to be ensured before calling this method
519: final Operator visitedOp = visited.op();
520: if (visitedOp instanceof SortedSchemaVariable
521: && svInst.isInstantiated((SchemaVariable) visitedOp)
522: && (!((SchemaVariable) visitedOp).isListSV())) {
523: pushNew(toTerm(svInst
524: .getInstantiation((SchemaVariable) visitedOp)));
525: } else if (forceSVInst
526: && visitedOp instanceof SortedSchemaVariable
527: && ((SchemaVariable) visitedOp).isTermSV()
528: && instantiateWithMV(visited)) {
529: // then we are done ...
530: } else if ((visitedOp instanceof Metavariable)
531: && metavariableInst
532: .getInstantiation((Metavariable) visitedOp) != visitedOp) {
533: pushNew(metavariableInst
534: .getInstantiation((Metavariable) visitedOp));
535: } else if (visitedOp instanceof ExpressionOperator) {
536: ExpressionOperator exprOp = (ExpressionOperator) visitedOp;
537: pushNew(exprOp.resolveExpression(svInst, getServices()));
538: } else {
539:
540: Operator newOp = instantiateOperator(visitedOp);
541:
542: if (newOp == null) {
543: // only partial instantiation information available
544: // use original op
545: newOp = visitedOp;
546: }
547:
548: boolean operatorInst = (newOp != visitedOp);
549:
550: // instantiation of java block
551: boolean jblockChanged = false;
552: JavaBlock jb = visited.javaBlock();
553:
554: if (jb != JavaBlock.EMPTY_JAVABLOCK) {
555: jb = replacePrg(svInst, jb);
556: if (jb != visited.javaBlock()) {
557: jblockChanged = true;
558: }
559: }
560:
561: // instantiate bound variables
562: varsChanged.setVal(false); // reset variable change flag
563: final ArrayOfQuantifiableVariable[] boundVars = instantiateBoundVariables(visited);
564:
565: Term[] neededsubs = neededSubs(newOp.arity());
566: if (varsChanged.val()
567: || jblockChanged
568: || operatorInst
569: || (!subStack.empty() && subStack.peek() == newMarker)) {
570: pushNew(resolveSubst(tf.createTerm(newOp, neededsubs,
571: boundVars, jb)));
572: } else {
573: final Term t = resolveSubst(visited);
574: if (t == visited)
575: subStack.push(t);
576: else
577: pushNew(t);
578: }
579: }
580: }
581:
582: /**
583: * @param boundSchemaVariable
584: * @return
585: */
586: private LogicVariable createTemporaryLV(
587: SortedSchemaVariable boundSchemaVariable) {
588: final Term t = newInstantiations.get(boundSchemaVariable);
589: if (t != null)
590: return (LogicVariable) t.op();
591:
592: final Sort realSort = svInst.getGenericSortInstantiations()
593: .getRealSort(boundSchemaVariable.sort(), getServices());
594: final LogicVariable v = new LogicVariable(new Name("TempLV"),
595: realSort);
596:
597: newInstantiations = newInstantiations.put(boundSchemaVariable,
598: tf.createVariableTerm(v));
599: return v;
600: }
601:
602: private Operator handleSortDependingSymbol(Operator op) {
603: final SortDependingSymbol depOp = (SortDependingSymbol) op;
604: final Sort depSort = depOp.getSortDependingOn();
605:
606: final SortDefiningSymbols realDepSort = (SortDefiningSymbols) svInst
607: .getGenericSortInstantiations().getRealSort(depSort,
608: getServices());
609:
610: final Operator res = (Operator) depOp
611: .getInstanceFor(realDepSort);
612: Debug.assertFalse(res == null,
613: "Did not find instance of symbol " + op + " for sort "
614: + realDepSort);
615: return res;
616: }
617:
618: private Term resolveSubst(Term t) {
619: if (resolveSubsts && t.op() instanceof SubstOp)
620: return ((SubstOp) t.op()).apply(t);
621: return t;
622: }
623:
624: /**
625: * PRECONDITION: visited.op() instanceof SchemaVariable &&
626: * ((SchemaVariable)visited.op()).isTermSV ()
627: * Instantiate the given TermSV with a new metavariable
628: * @return true iff the instantiation succeeded
629: */
630: private boolean instantiateWithMV(Term visited) {
631: if (newInstantiations == null)
632: return false;
633:
634: final SchemaVariable sv = (SchemaVariable) visited.op();
635:
636: Term t = newInstantiations.get(sv);
637:
638: if (t == null) {
639: final Sort realSort = svInst.getGenericSortInstantiations()
640: .getRealSort(visited.sort(), getServices());
641: final Metavariable mv = MetavariableDeliverer
642: .createNewMatchVariable(svInstBasename.toString(),
643: realSort, getServices());
644:
645: if (mv == null) {
646: newInstantiations = null;
647: return false;
648: } else {
649: t = tf.createFunctionTerm(mv);
650: newInstantiations = newInstantiations.put(sv, t);
651: }
652: }
653:
654: pushNew(t);
655: return true;
656: }
657:
658: /**
659: * delivers the new built term
660: */
661: public Term getTerm() {
662: if (computedResult == null) {
663: Object o = null;
664: do {
665: o = subStack.pop();
666: } while (o == newMarker);
667: Term t = (Term) o;
668: // CollisionDeletingSubstitutionTermApplier substVisit
669: // = new CollisionDeletingSubstitutionTermApplier();
670: // t.execPostOrder(substVisit);
671: // t=substVisit.getTerm();
672: computedResult = t;
673: }
674: return computedResult;
675: }
676:
677: public SVInstantiations getSVInstantiations() {
678: return svInst;
679: }
680:
681: /**
682: * @return introduced metavariables for instantiation of schema
683: * variables, or null if some schema variables could not be
684: * instantiated
685: */
686: public MapFromSchemaVariableToTerm getNewInstantiations() {
687: return newInstantiations;
688: }
689:
690: /**
691: * this method is called in execPreOrder and execPostOrder in class Term
692: * when leaving the subtree rooted in the term subtreeRoot.
693: * Default implementation is to do nothing. Subclasses can
694: * override this method
695: * when the visitor behaviour depends on informations bound to subtrees.
696: * @param subtreeRoot root of the subtree which the visitor leaves.
697: */
698: public void subtreeLeft(Term subtreeRoot) {
699: if (subtreeRoot.op() instanceof MetaOperator) {
700: MetaOperator mop = (MetaOperator) subtreeRoot.op();
701: pushNew(mop.calculate((Term) subStack.pop(), svInst,
702: getServices()));
703: }
704: }
705:
706: }
|