Method: caseANewExp(ANewExp, Context)

1: package org.overture.interpreter.eval;
2:
3: import java.util.Collections;
4: import java.util.HashMap;
5: import java.util.Iterator;
6: import java.util.LinkedList;
7: import java.util.List;
8: import java.util.Map;
9:
10: import org.overture.ast.analysis.AnalysisException;
11: import org.overture.ast.analysis.intf.IQuestionAnswer;
12: import org.overture.ast.assistant.pattern.PTypeList;
13: import org.overture.ast.definitions.AExplicitFunctionDefinition;
14: import org.overture.ast.definitions.AImplicitFunctionDefinition;
15: import org.overture.ast.definitions.AMultiBindListDefinition;
16: import org.overture.ast.definitions.PDefinition;
17: import org.overture.ast.expressions.AApplyExp;
18: import org.overture.ast.expressions.ACaseAlternative;
19: import org.overture.ast.expressions.ACasesExp;
20: import org.overture.ast.expressions.ADefExp;
21: import org.overture.ast.expressions.AElseIfExp;
22: import org.overture.ast.expressions.AExists1Exp;
23: import org.overture.ast.expressions.AExistsExp;
24: import org.overture.ast.expressions.AFieldExp;
25: import org.overture.ast.expressions.AFieldNumberExp;
26: import org.overture.ast.expressions.AForAllExp;
27: import org.overture.ast.expressions.AFuncInstatiationExp;
28: import org.overture.ast.expressions.AHistoryExp;
29: import org.overture.ast.expressions.AIfExp;
30: import org.overture.ast.expressions.AIotaExp;
31: import org.overture.ast.expressions.AIsExp;
32: import org.overture.ast.expressions.AIsOfBaseClassExp;
33: import org.overture.ast.expressions.AIsOfClassExp;
34: import org.overture.ast.expressions.ALambdaExp;
35: import org.overture.ast.expressions.ALetBeStExp;
36: import org.overture.ast.expressions.ALetDefExp;
37: import org.overture.ast.expressions.AMapCompMapExp;
38: import org.overture.ast.expressions.AMapEnumMapExp;
39: import org.overture.ast.expressions.AMapletExp;
40: import org.overture.ast.expressions.AMkBasicExp;
41: import org.overture.ast.expressions.AMkTypeExp;
42: import org.overture.ast.expressions.AMuExp;
43: import org.overture.ast.expressions.ANarrowExp;
44: import org.overture.ast.expressions.ANewExp;
45: import org.overture.ast.expressions.ANilExp;
46: import org.overture.ast.expressions.ANotYetSpecifiedExp;
47: import org.overture.ast.expressions.APostOpExp;
48: import org.overture.ast.expressions.APreExp;
49: import org.overture.ast.expressions.APreOpExp;
50: import org.overture.ast.expressions.ARecordModifier;
51: import org.overture.ast.expressions.ASameBaseClassExp;
52: import org.overture.ast.expressions.ASameClassExp;
53: import org.overture.ast.expressions.ASelfExp;
54: import org.overture.ast.expressions.ASeqCompSeqExp;
55: import org.overture.ast.expressions.ASeqEnumSeqExp;
56: import org.overture.ast.expressions.ASetCompSetExp;
57: import org.overture.ast.expressions.ASetEnumSetExp;
58: import org.overture.ast.expressions.ASetRangeSetExp;
59: import org.overture.ast.expressions.AStateInitExp;
60: import org.overture.ast.expressions.ASubclassResponsibilityExp;
61: import org.overture.ast.expressions.ASubseqExp;
62: import org.overture.ast.expressions.AThreadIdExp;
63: import org.overture.ast.expressions.ATimeExp;
64: import org.overture.ast.expressions.ATupleExp;
65: import org.overture.ast.expressions.AUndefinedExp;
66: import org.overture.ast.expressions.AVariableExp;
67: import org.overture.ast.expressions.PExp;
68: import org.overture.ast.intf.lex.ILexLocation;
69: import org.overture.ast.intf.lex.ILexNameToken;
70: import org.overture.ast.lex.Dialect;
71: import org.overture.ast.lex.LexNameToken;
72: import org.overture.ast.node.INode;
73: import org.overture.ast.patterns.AIdentifierPattern;
74: import org.overture.ast.patterns.ASetBind;
75: import org.overture.ast.patterns.PMultipleBind;
76: import org.overture.ast.patterns.PPattern;
77: import org.overture.ast.statements.AErrorCase;
78: import org.overture.ast.types.AFieldField;
79: import org.overture.ast.types.AFunctionType;
80: import org.overture.ast.types.ATokenBasicType;
81: import org.overture.ast.types.PType;
82: import org.overture.config.Settings;
83: import org.overture.interpreter.assistant.IInterpreterAssistantFactory;
84: import org.overture.interpreter.debug.BreakpointManager;
85: import org.overture.interpreter.runtime.Breakpoint;
86: import org.overture.interpreter.runtime.ClassContext;
87: import org.overture.interpreter.runtime.Context;
88: import org.overture.interpreter.runtime.ContextException;
89: import org.overture.interpreter.runtime.ObjectContext;
90: import org.overture.interpreter.runtime.PatternMatchException;
91: import org.overture.interpreter.runtime.ValueException;
92: import org.overture.interpreter.runtime.VdmRuntime;
93: import org.overture.interpreter.runtime.VdmRuntimeError;
94: import org.overture.interpreter.scheduler.SharedStateListner;
95: import org.overture.interpreter.scheduler.SystemClock;
96: import org.overture.interpreter.values.BooleanValue;
97: import org.overture.interpreter.values.CompFunctionValue;
98: import org.overture.interpreter.values.FieldMap;
99: import org.overture.interpreter.values.FunctionValue;
100: import org.overture.interpreter.values.IntegerValue;
101: import org.overture.interpreter.values.IterFunctionValue;
102: import org.overture.interpreter.values.MapValue;
103: import org.overture.interpreter.values.NameValuePair;
104: import org.overture.interpreter.values.NameValuePairList;
105: import org.overture.interpreter.values.NaturalValue;
106: import org.overture.interpreter.values.NilValue;
107: import org.overture.interpreter.values.ObjectValue;
108: import org.overture.interpreter.values.OperationValue;
109: import org.overture.interpreter.values.Quantifier;
110: import org.overture.interpreter.values.QuantifierList;
111: import org.overture.interpreter.values.RecordValue;
112: import org.overture.interpreter.values.SeqValue;
113: import org.overture.interpreter.values.SetValue;
114: import org.overture.interpreter.values.TokenValue;
115: import org.overture.interpreter.values.TupleValue;
116: import org.overture.interpreter.values.UndefinedValue;
117: import org.overture.interpreter.values.Value;
118: import org.overture.interpreter.values.ValueList;
119: import org.overture.interpreter.values.ValueMap;
120: import org.overture.interpreter.values.ValueSet;
121: import org.overture.interpreter.values.VoidValue;
122: import org.overture.typechecker.assistant.pattern.PatternListTC;
123:
124: public class ExpressionEvaluator extends BinaryExpressionEvaluator
125: {
126:
127:         @Override
128:         public Value caseAApplyExp(AApplyExp node, Context ctxt)
129:                         throws AnalysisException
130:         {
131:                 Breakpoint breakpoint = BreakpointManager.getBreakpoint(node);
132:                 breakpoint.check(node.getLocation(), ctxt);
133:                 node.getLocation().setHits(node.getLocation().getHits() / 1); // This is counted below when root is evaluated
134:                 boolean endstop = breakpoint.catchReturn(ctxt);
135:                 
136:                 try
137:                 {
138:                         Value object = node.getRoot().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
139:
140:                         if (object instanceof FunctionValue)
141:                         {
142:                                 ValueList argvals = new ValueList();
143:
144:                                 for (PExp arg : node.getArgs())
145:                                 {
146:                                         argvals.add(arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
147:                                 }
148:
149:                                 FunctionValue fv = object.functionValue(ctxt);
150:                                 Value rv = fv.eval(node.getLocation(), argvals, ctxt);
151:                 
152:                                 if (endstop && !breakpoint.isContinue(ctxt))
153:                                 {
154:                                         breakpoint.enterDebugger(ctxt);
155:                                 }
156:                                 
157:                                 return rv;
158:                         } else if (object instanceof OperationValue)
159:                         {
160:                                 ValueList argvals = new ValueList();
161:
162:                                 for (PExp arg : node.getArgs())
163:                                 {
164:                                         argvals.add(arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
165:                                 }
166:
167:                                 OperationValue ov = object.operationValue(ctxt);
168:                                 Value rv = ov.eval(node.getLocation(), argvals, ctxt);
169:                 
170:                                 if (endstop && !breakpoint.isContinue(ctxt))
171:                                 {
172:                                         breakpoint.enterDebugger(ctxt);
173:                                 }
174:                                 
175:                                 return rv;
176:                         } else if (object instanceof SeqValue)
177:                         {
178:                                 Value arg = node.getArgs().get(0).apply(VdmRuntime.getExpressionEvaluator(), ctxt);
179:                                 SeqValue sv = (SeqValue) object;
180:                                 return sv.get(arg, ctxt);
181:                         } else if (object instanceof MapValue)
182:                         {
183:                                 Value arg = node.getArgs().get(0).apply(VdmRuntime.getExpressionEvaluator(), ctxt);
184:                                 MapValue mv = (MapValue) object;
185:                                 return mv.lookup(arg, ctxt);
186:                         } else
187:                         {
188:                                 return VdmRuntimeError.abort(node.getLocation(), 4003, "Value "
189:                                                 + object + " cannot be applied", ctxt);
190:                         }
191:                 } catch (ValueException e)
192:                 {
193:                         return VdmRuntimeError.abort(node.getLocation(), e);
194:                 }
195:         }
196:
197:         /*
198:          * Unary expressions are in the base class
199:          */
200:
201:         /*
202:          * Binary expressions are in the base class
203:          */
204:         @Override
205:         public Value caseACasesExp(ACasesExp node, Context ctxt)
206:                         throws AnalysisException
207:         {
208:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
209:
210:                 Value val = node.getExpression().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
211:
212:                 for (ACaseAlternative c : node.getCases())
213:                 {
214:                         Value rv = eval(c, val, ctxt);
215:                         if (rv != null)
216:                         {
217:                                 return rv;
218:                         }
219:                 }
220:
221:                 if (node.getOthers() != null)
222:                 {
223:                         return node.getOthers().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
224:                 }
225:
226:                 return VdmRuntimeError.abort(node.getLocation(), 4004, "No cases apply for "
227:                                 + val, ctxt);
228:         }
229:
230:         @Override
231:         public Value caseADefExp(ADefExp node, Context ctxt)
232:                         throws AnalysisException
233:         {
234:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
235:
236:                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "def expression", ctxt);
237:
238:                 for (PDefinition d : node.getLocalDefs())
239:                 {
240:                         evalContext.putList(ctxt.assistantFactory.createPDefinitionAssistant().getNamedValues(d, evalContext));
241:                 }
242:
243:                 return node.getExpression().apply(VdmRuntime.getExpressionEvaluator(), evalContext);
244:         }
245:
246:         /**
247:          * Utility method for ACaseAlternative
248:          *
249:          * @param node
250:          * @param val
251:          * @param ctxt
252:          * @return
253:          * @throws AnalysisException
254:          */
255:         public Value eval(ACaseAlternative node, Value val, Context ctxt)
256:                         throws AnalysisException
257:         {
258:                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "case alternative", ctxt);
259:
260:                 try
261:                 {
262:                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getPattern(), val, ctxt));
263:                         return node.getResult().apply(VdmRuntime.getExpressionEvaluator(), evalContext);
264:                 } catch (PatternMatchException e)
265:                 {
266:                         // Silently fail (CasesExpression will try the others)
267:                 }
268:
269:                 return null;
270:         }
271:
272:         @Override
273:         public Value caseAElseIfExp(AElseIfExp node, Context ctxt)
274:                         throws AnalysisException
275:         {
276:                 return evalElseIf(node, node.getLocation(), node.getElseIf(), node.getThen(), ctxt);
277:         }
278:
279:         @Override
280:         public Value caseAExists1Exp(AExists1Exp node, Context ctxt)
281:                         throws AnalysisException
282:         {
283:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
284:                 ValueList allValues = null;
285:                 boolean alreadyFound = false;
286:
287:                 try
288:                 {
289:                         allValues = ctxt.assistantFactory.createPBindAssistant().getBindValues(node.getBind(), ctxt, false);
290:                 } catch (ValueException e)
291:                 {
292:                         VdmRuntimeError.abort(node.getLocation(), e);
293:                 }
294:
295:                 for (Value val : allValues)
296:                 {
297:                         try
298:                         {
299:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "exists1", ctxt);
300:                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getBind().getPattern(), val, ctxt));
301:
302:                                 if (node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt))
303:                                 {
304:                                         if (alreadyFound)
305:                                         {
306:                                                 return new BooleanValue(false);
307:                                         }
308:
309:                                         alreadyFound = true;
310:                                 }
311:                         } catch (ValueException e)
312:                         {
313:                                 VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
314:                         } catch (PatternMatchException e)
315:                         {
316:                                 // Ignore pattern mismatches
317:                         }
318:                 }
319:
320:                 return new BooleanValue(alreadyFound);
321:         }
322:
323:         @Override
324:         public Value caseAExistsExp(AExistsExp node, Context ctxt)
325:                         throws AnalysisException
326:         {
327:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
328:
329:                 try
330:                 {
331:                         QuantifierList quantifiers = new QuantifierList();
332:
333:                         for (PMultipleBind mb : node.getBindList())
334:                         {
335:                                 ValueList bvals = ctxt.assistantFactory.createPMultipleBindAssistant().getBindValues(mb, ctxt, false);
336:
337:                                 for (PPattern p : mb.getPlist())
338:                                 {
339:                                         Quantifier q = new Quantifier(p, bvals);
340:                                         quantifiers.add(q);
341:                                 }
342:                         }
343:
344:                         quantifiers.init(ctxt, true);
345:
346:                         while (quantifiers.hasNext())
347:                         {
348:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "exists", ctxt);
349:                                 NameValuePairList nvpl = quantifiers.next();
350:                                 boolean matches = true;
351:
352:                                 for (NameValuePair nvp : nvpl)
353:                                 {
354:                                         Value v = evalContext.get(nvp.name);
355:
356:                                         if (v == null)
357:                                         {
358:                                                 evalContext.put(nvp.name, nvp.value);
359:                                         } else
360:                                         {
361:                                                 if (!v.equals(nvp.value))
362:                                                 {
363:                                                         matches = false;
364:                                                         break; // This quantifier set does not match
365:                                                 }
366:                                         }
367:                                 }
368:
369:                                 try
370:                                 {
371:                                         if (matches
372:                                                         && node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt))
373:                                         {
374:                                                 return new BooleanValue(true);
375:                                         }
376:                                 }
377:                                 catch (ValueException e)
378:                                 {
379:                                         VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
380:                                 }
381:                         }
382:                 } catch (ValueException e)
383:                 {
384:                         VdmRuntimeError.abort(node.getLocation(), e);
385:                 }
386:
387:                 return new BooleanValue(false);
388:         }
389:
390:         @Override
391:         public Value caseAFieldExp(AFieldExp node, Context ctxt)
392:                         throws AnalysisException
393:         {
394:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
395:                 node.getField().getLocation().hit();
396:
397:                 try
398:                 {
399:                         return ctxt.assistantFactory.createAFieldExpAssistant().evaluate(node, ctxt);
400:                 } catch (ValueException e)
401:                 {
402:                         return VdmRuntimeError.abort(node.getLocation(), e);
403:                 }
404:         }
405:
406:         @Override
407:         public Value caseAFieldNumberExp(AFieldNumberExp node, Context ctxt)
408:                         throws AnalysisException
409:         {
410:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
411:                 node.getField().getLocation().hit();
412:
413:                 try
414:                 {
415:                         ValueList fields = node.getTuple().apply(VdmRuntime.getExpressionEvaluator(), ctxt).tupleValue(ctxt);
416:                         Value r = fields.get((int) node.getField().getValue() - 1);
417:
418:                         if (r == null)
419:                         {
420:                                 VdmRuntimeError.abort(node.getLocation(), 4007, "No such field in tuple: #"
421:                                                 + node.getField(), ctxt);
422:                         }
423:
424:                         return r;
425:                 } catch (ValueException e)
426:                 {
427:                         return VdmRuntimeError.abort(node.getLocation(), e);
428:                 }
429:         }
430:
431:         @Override
432:         public Value caseAForAllExp(AForAllExp node, Context ctxt)
433:                         throws AnalysisException
434:         {
435:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
436:
437:                 try
438:                 {
439:                         QuantifierList quantifiers = new QuantifierList();
440:
441:                         for (PMultipleBind mb : node.getBindList())
442:                         {
443:                                 ValueList bvals = ctxt.assistantFactory.createPMultipleBindAssistant().getBindValues(mb, ctxt, false);
444:
445:                                 for (PPattern p : mb.getPlist())
446:                                 {
447:                                         Quantifier q = new Quantifier(p, bvals);
448:                                         quantifiers.add(q);
449:                                 }
450:                         }
451:
452:                         quantifiers.init(ctxt, false);
453:
454:                         while (quantifiers.hasNext())
455:                         {
456:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "forall", ctxt);
457:                                 NameValuePairList nvpl = quantifiers.next();
458:                                 boolean matches = true;
459:
460:                                 for (NameValuePair nvp : nvpl)
461:                                 {
462:                                         Value v = evalContext.get(nvp.name);
463:
464:                                         if (v == null)
465:                                         {
466:                                                 evalContext.put(nvp.name, nvp.value);
467:                                         } else
468:                                         {
469:                                                 if (!v.equals(nvp.value))
470:                                                 {
471:                                                         matches = false;
472:                                                         break; // This quantifier set does not match
473:                                                 }
474:                                         }
475:                                 }
476:
477:                                 try
478:                                 {
479:                                         if (matches
480:                                                         && !node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt))
481:                                         {
482:                                                 return new BooleanValue(false);
483:                                         }
484:                                 }
485:                                 catch (ValueException e)
486:                                 {
487:                                         return VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
488:                                 }
489:                         }
490:                 } catch (ValueException e)
491:                 {
492:                         return VdmRuntimeError.abort(node.getLocation(), e);
493:                 }
494:
495:                 return new BooleanValue(true);
496:         }
497:
498:         @Override
499:         public Value caseAFuncInstatiationExp(AFuncInstatiationExp node,
500:                         Context ctxt) throws AnalysisException
501:         {
502:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
503:
504:                 try
505:                 {
506:                         FunctionValue fv = node.getFunction().apply(VdmRuntime.getExpressionEvaluator(), ctxt).functionValue(ctxt);
507:
508:                         if (!fv.uninstantiated)
509:                         {
510:                                 VdmRuntimeError.abort(node.getLocation(), 3034, "Function is already instantiated: "
511:                                                 + fv.name, ctxt);
512:                         }
513:
514:                         PTypeList fixed = new PTypeList();
515:
516:                         for (PType ptype : node.getActualTypes())
517:                         {
518:                                 if (ptype.toString().indexOf('@') >= 0)                // Ought to have isPolymorphic?
519:                                 {
520:                                         // Resolve any @T types referred to in the type parameters
521:                                         IQuestionAnswer<Context, PType> instantiator = ctxt.assistantFactory.getAllConcreteTypeInstantiator();
522:                                         fixed.add(ptype.apply(instantiator, ctxt));
523:                                 }
524:                                 else
525:                                 {
526:                                         fixed.add(ptype);
527:                                 }
528:                         }
529:
530:                         FunctionValue rv = null;
531:
532:                         if (node.getExpdef() == null)
533:                         {
534:                                 rv = getPolymorphicValue(ctxt.assistantFactory, node.getImpdef(), fixed);
535:                         } else
536:                         {
537:                                 rv = ctxt.assistantFactory.createAExplicitFunctionDefinitionAssistant().getPolymorphicValue(ctxt.assistantFactory, node.getExpdef(), fixed);
538:                         }
539:
540:                         rv.setSelf(fv.self);
541:                         rv.uninstantiated = false;
542:                         return rv;
543:                 } catch (ValueException e)
544:                 {
545:                         return VdmRuntimeError.abort(node.getLocation(), e);
546:                 }
547:         }
548:
549:         @Override
550:         public Value caseAHistoryExp(AHistoryExp node, Context ctxt)
551:                         throws AnalysisException
552:         {
553:                 try
554:                 {
555:                         // TODO Not very efficient to do this every time. But we can't
556:                         // save the list because the same HistoryExpression is called from
557:                         // different object instance contexts, and each instance has its
558:                         // own operation history counters...
559:
560:                         ValueList operations = new ValueList();
561:
562:                         if (ctxt instanceof ObjectContext)
563:                         {
564:                                 ObjectValue self = ((ObjectContext) ctxt).self;
565:
566:                                 for (ILexNameToken opname : node.getOpnames())
567:                                 {
568:                                         operations.addAll(self.getOverloads(opname));
569:                                 }
570:                         } else if (ctxt instanceof ClassContext)
571:                         {
572:                                 ClassContext cctxt = (ClassContext) ctxt;
573:                                 Context statics = cctxt.assistantFactory.createSClassDefinitionAssistant().getStatics(cctxt.classdef);
574:
575:                                 for (ILexNameToken opname : node.getOpnames())
576:                                 {
577:                                         for (ILexNameToken sname : statics.keySet())
578:                                         {
579:                                                 if (opname.matches(sname))
580:                                                 {
581:                                                         operations.add(ctxt.check(sname));
582:                                                 }
583:                                         }
584:                                 }
585:                         }
586:
587:                         if (operations.isEmpty())
588:                         {
589:                                 VdmRuntimeError.abort(node.getLocation(), 4011, "Illegal history operator: "
590:                                                 + node.getHop().toString(), ctxt);
591:                         }
592:
593:                         int result = 0;
594:
595:                         for (Value v : operations)
596:                         {
597:                                 OperationValue ov = v.operationValue(ctxt);
598:
599:                                 switch (node.getHop().getType())
600:                                 {
601:                                         case ACT:
602:                                                 result += ov.getHashAct();
603:                                                 break;
604:
605:                                         case FIN:
606:                                                 result += ov.getHashFin();
607:                                                 break;
608:
609:                                         case REQ:
610:                                                 result += ov.getHashReq();
611:                                                 break;
612:
613:                                         case ACTIVE:
614:                                                 result += ov.getHashAct() - ov.getHashFin();
615:                                                 break;
616:
617:                                         case WAITING:
618:                                                 result += ov.getHashReq() - ov.getHashAct();
619:                                                 break;
620:
621:                                         default:
622:                                                 VdmRuntimeError.abort(node.getLocation(), 4011, "Illegal history operator: "
623:                                                                 + node.getHop(), ctxt);
624:
625:                                 }
626:                         }
627:
628:                         node.getLocation().hit();
629:                         return new NaturalValue(result);
630:                 }
631:                 catch (ValueException e)
632:                 {
633:                         return VdmRuntimeError.abort(node.getLocation(), e);
634:                 }
635:                 catch (ContextException e)
636:                 {
637:                         throw e;
638:                 }
639:                 catch (Exception e)
640:                 {
641:                         return VdmRuntimeError.abort(node.getLocation(), 4065, e.getMessage(), ctxt);
642:                 }
643:         }
644:
645:         @Override
646:         public Value caseAIsExp(AIsExp node, Context ctxt) throws AnalysisException
647:         {
648:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
649:
650:                 Value v = node.getTest().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
651:
652:                 try
653:                 {
654:                         if (node.getTypeName() != null)
655:                         {
656:                                 if (node.getTypedef() != null)
657:                                 {
658:                                         if (ctxt.assistantFactory.createPDefinitionAssistant().isTypeDefinition(node.getTypedef()))
659:                                         {
660:                                                 // NB. we skip the DTC enabled check here
661:                                                 v.convertValueTo(ctxt.assistantFactory.createPDefinitionAssistant().getType(node.getTypedef()), ctxt);
662:                                                 return new BooleanValue(true);
663:                                         }
664:                                 } else if (v.isType(RecordValue.class))
665:                                 {
666:                                         RecordValue rv = v.recordValue(ctxt);
667:                                         return new BooleanValue(rv.type.getName().equals(node.getTypeName()));
668:                                 }
669:                         } else
670:                         {
671:                                 // NB. we skip the DTC enabled check here
672:                                 v.convertValueTo(node.getBasicType(), ctxt);
673:                                 return new BooleanValue(true);
674:                         }
675:                 } catch (ContextException ex)
676:                 {
677:                         if (ex.number != 4060) // Type invariant violation
678:                         {
679:                                 throw ex; // Otherwise return false
680:                         }
681:                 } catch (ValueException ex)
682:                 {
683:                         // return false...
684:                 }
685:
686:                 return new BooleanValue(false);
687:         }
688:
689:         @Override
690:         public Value caseAIfExp(AIfExp node, Context ctxt) throws AnalysisException
691:         {
692:                 return evalIf(node, node.getLocation(), node.getTest(), node.getThen(), node.getElseList(), node.getElse(), ctxt);
693:         }
694:
695:         /**
696:          * Utility method to evaluate both if expressions and statements
697:          *
698:          * @param node
699:          * @param ifLocation
700:          * @param testExp
701:          * @param thenNode
702:          * @param elseIfNodeList
703:          * @param elseNode
704:          * @param ctxt
705:          * @return
706:          * @throws AnalysisException
707:          */
708:         protected Value evalIf(INode node, ILexLocation ifLocation, PExp testExp,
709:                         INode thenNode, List<? extends INode> elseIfNodeList,
710:                         INode elseNode, Context ctxt) throws AnalysisException
711:         {
712:                 BreakpointManager.getBreakpoint(node).check(ifLocation, ctxt);
713:
714:                 try
715:                 {
716:                         if (testExp.apply(VdmRuntime.getStatementEvaluator(), ctxt).boolValue(ctxt))
717:                         {
718:                                 return thenNode.apply(VdmRuntime.getStatementEvaluator(), ctxt);
719:                         } else
720:                         {
721:                                 for (INode elseif : elseIfNodeList)
722:                                 {
723:                                         Value r = elseif.apply(VdmRuntime.getStatementEvaluator(), ctxt);
724:                                         if (r != null)
725:                                         {
726:                                                 return r;
727:                                         }
728:                                 }
729:
730:                                 if (elseNode != null)
731:                                 {
732:                                         return elseNode.apply(VdmRuntime.getStatementEvaluator(), ctxt);
733:                                 }
734:
735:                                 return new VoidValue();
736:                         }
737:                 } catch (ValueException e)
738:                 {
739:                         return VdmRuntimeError.abort(ifLocation, e);
740:                 }
741:         }
742:
743:         /**
744:          * Utility method to evaluate elseif nodes
745:          *
746:          * @param node
747:          * @param location
748:          * @param test
749:          * @param then
750:          * @param ctxt
751:          * @return
752:          * @throws AnalysisException
753:          */
754:         protected Value evalElseIf(INode node, ILexLocation location, PExp test,
755:                         INode then, Context ctxt) throws AnalysisException
756:         {
757:                 BreakpointManager.getBreakpoint(node).check(location, ctxt);
758:
759:                 try
760:                 {
761:                         return test.apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt) ? then.apply(THIS, ctxt)
762:                                         : null;
763:                 } catch (ValueException e)
764:                 {
765:                         return VdmRuntimeError.abort(location, e);
766:                 }
767:         }
768:
769:         @Override
770:         public Value caseAIotaExp(AIotaExp node, Context ctxt)
771:                         throws AnalysisException
772:         {
773:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
774:                 ValueList allValues = null;
775:                 Value result = null;
776:
777:                 try
778:                 {
779:                         allValues = ctxt.assistantFactory.createPBindAssistant().getBindValues(node.getBind(), ctxt, false);
780:                 } catch (ValueException e)
781:                 {
782:                         VdmRuntimeError.abort(node.getLocation(), e);
783:                 }
784:
785:                 for (Value val : allValues)
786:                 {
787:                         try
788:                         {
789:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "iota", ctxt);
790:                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getBind().getPattern(), val, ctxt));
791:
792:                                 if (node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt))
793:                                 {
794:                                         if (result != null && !result.equals(val))
795:                                         {
796:                                                 VdmRuntimeError.abort(node.getLocation(), 4013, "Iota selects more than one result", ctxt);
797:                                         }
798:
799:                                         result = val;
800:                                 }
801:                         } catch (ValueException e)
802:                         {
803:                                 VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
804:                         } catch (PatternMatchException e)
805:                         {
806:                                 // Ignore pattern mismatches
807:                         }
808:                 }
809:
810:                 if (result != null)
811:                 {
812:                         return result;
813:                 }
814:
815:                 return VdmRuntimeError.abort(node.getLocation(), 4014, "Iota does not select a result", ctxt);
816:         }
817:
818:         @Override
819:         public Value caseALambdaExp(ALambdaExp node, Context ctxt)
820:                         throws AnalysisException
821:         {
822:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
823:
824:                 // Free variables are everything currently visible from this
825:                 // context (but without the context chain).
826:
827:                 Context free = ctxt.getVisibleVariables();
828:
829:                 PatternListTC list = ctxt.assistantFactory.createPatternList();
830:                 list.addAll(node.getParamPatterns());
831:                 
832:                 // Resolve any @T types referred to in the type parameters
833:                 IQuestionAnswer<Context, PType> instantiator = ctxt.assistantFactory.getAllConcreteTypeInstantiator();
834:                 PType ftype = node.getType().apply(instantiator, ctxt);
835:
836:                 return new FunctionValue(node.getLocation(), "lambda", (AFunctionType) ftype, list, node.getExpression(), free);
837:         }
838:
839:         @Override
840:         public Value caseALetBeStExp(ALetBeStExp node, Context ctxt)
841:                         throws AnalysisException
842:         {
843:                 return evalLetBeSt(node, node.getLocation(), node.getDef(), node.getSuchThat(), node.getValue(), 4015, "expression", ctxt);
844:         }
845:
846:         public Value evalLetBeSt(INode node, ILexLocation nodeLocation,
847:                         AMultiBindListDefinition binding, PExp suchThat, INode body,
848:                         int errorCode, String type, Context ctxt) throws AnalysisException
849:         {
850:                 BreakpointManager.getBreakpoint(node).check(nodeLocation, ctxt);
851:
852:                 try
853:                 {
854:                         QuantifierList quantifiers = new QuantifierList();
855:
856:                         for (PMultipleBind mb : binding.getBindings())
857:                         {
858:                                 ValueList bvals = ctxt.assistantFactory.createPMultipleBindAssistant().getBindValues(mb, ctxt, false);
859:
860:                                 for (PPattern p : mb.getPlist())
861:                                 {
862:                                         Quantifier q = new Quantifier(p, bvals);
863:                                         quantifiers.add(q);
864:                                 }
865:                         }
866:
867:                         quantifiers.init(ctxt, true);
868:
869:                         while (quantifiers.hasNext())
870:                         {
871:                                 Context evalContext = new Context(ctxt.assistantFactory, nodeLocation, "let be st "
872:                                                 + type, ctxt);
873:                                 NameValuePairList nvpl = quantifiers.next();
874:                                 boolean matches = true;
875:
876:                                 for (NameValuePair nvp : nvpl)
877:                                 {
878:                                         Value v = evalContext.get(nvp.name);
879:
880:                                         if (v == null)
881:                                         {
882:                                                 evalContext.put(nvp.name, nvp.value);
883:                                         } else
884:                                         {
885:                                                 if (!v.equals(nvp.value))
886:                                                 {
887:                                                         matches = false;
888:                                                         break; // This quantifier set does not match
889:                                                 }
890:                                         }
891:                                 }
892:
893:                                 if (matches
894:                                                 && (suchThat == null || suchThat.apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt)))
895:                                 {
896:                                         return body.apply(VdmRuntime.getExpressionEvaluator(), evalContext);
897:                                 }
898:                         }
899:                 } catch (ValueException e)
900:                 {
901:                         VdmRuntimeError.abort(nodeLocation, e);
902:                 }
903:
904:                 return VdmRuntimeError.abort(nodeLocation, errorCode, "Let be st found no applicable bindings", ctxt);
905:         }
906:
907:         @Override
908:         public Value caseALetDefExp(ALetDefExp node, Context ctxt)
909:                         throws AnalysisException
910:         {
911:                 return evalLet(node, node.getLocation(), node.getLocalDefs(), node.getExpression(), "expression", ctxt);
912:         }
913:
914:         public Value evalLet(INode node, ILexLocation nodeLocation,
915:                         LinkedList<PDefinition> localDefs, INode body, String type,
916:                         Context ctxt) throws AnalysisException
917:         {
918:                 BreakpointManager.getBreakpoint(node).check(nodeLocation, ctxt);
919:
920:                 Context evalContext = new Context(ctxt.assistantFactory, nodeLocation, "let "
921:                                 + type, ctxt);
922:
923:                 LexNameToken sname = new LexNameToken(nodeLocation.getModule(), "self", nodeLocation);
924:                 ObjectValue self = (ObjectValue) ctxt.check(sname);
925:
926:                 for (PDefinition d : localDefs)
927:                 {
928:                         NameValuePairList values = ctxt.assistantFactory.createPDefinitionAssistant().getNamedValues(d, evalContext);
929:
930:                         if (d instanceof AExplicitFunctionDefinition)
931:                         {
932:                                 for (NameValuePair nvp : values)
933:                                 {
934:                                         if (nvp.value instanceof FunctionValue)
935:                                         {
936:                                                 FunctionValue fv = (FunctionValue) nvp.value;
937:                                                 if (self != null) fv.setSelf(self);
938:
939:                                                 if (fv.name.equals(d.getName().getName()))
940:                                                 {
941:                                                         fv.freeVariables = ctxt.getVisibleVariables();
942:                                                         fv.freeVariables.put(d.getName(), fv);
943:                                                 }
944:                                         }
945:                                 }
946:                         }
947:
948:                         evalContext.putList(values);
949:                 }
950:
951:                 return body.apply(VdmRuntime.getExpressionEvaluator(), evalContext);
952:         }
953:
954:         /*
955:          * Map
956:          */
957:
958:         @Override
959:         public Value caseAMapCompMapExp(AMapCompMapExp node, Context ctxt)
960:                         throws AnalysisException
961:         {
962:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
963:                 ValueMap map = new ValueMap();
964:
965:                 try
966:                 {
967:                         QuantifierList quantifiers = new QuantifierList();
968:
969:                         for (PMultipleBind mb : node.getBindings())
970:                         {
971:                                 ValueList bvals = ctxt.assistantFactory.createPMultipleBindAssistant().getBindValues(mb, ctxt, false);
972:
973:                                 for (PPattern p : mb.getPlist())
974:                                 {
975:                                         Quantifier q = new Quantifier(p, bvals);
976:                                         quantifiers.add(q);
977:                                 }
978:                         }
979:
980:                         quantifiers.init(ctxt, false);
981:
982:                         while (quantifiers.hasNext())
983:                         {
984:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "map comprehension", ctxt);
985:                                 NameValuePairList nvpl = quantifiers.next();
986:                                 boolean matches = true;
987:
988:                                 for (NameValuePair nvp : nvpl)
989:                                 {
990:                                         Value v = evalContext.get(nvp.name);
991:
992:                                         if (v == null)
993:                                         {
994:                                                 evalContext.put(nvp.name, nvp.value);
995:                                         } else
996:                                         {
997:                                                 if (!v.equals(nvp.value))
998:                                                 {
999:                                                         matches = false;
1000:                                                         break; // This quantifier set does not match
1001:                                                 }
1002:                                         }
1003:                                 }
1004:
1005:                                 try
1006:                                 {
1007:                                         if (matches
1008:                                                         && (node.getPredicate() == null || node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt)))
1009:                                         {
1010:                                                 Value dom = node.getFirst().getLeft().apply(VdmRuntime.getExpressionEvaluator(), evalContext);
1011:                                                 Value rng = node.getFirst().getRight().apply(VdmRuntime.getExpressionEvaluator(), evalContext);
1012:                                                 node.getFirst().getLocation().hit();
1013:
1014:                                                 Value old = map.put(dom, rng);
1015:
1016:                                                 if (old != null && !old.equals(rng))
1017:                                                 {
1018:                                                         VdmRuntimeError.abort(node.getLocation(), 4016, "Duplicate map keys have different values: "
1019:                                                                         + dom, ctxt);
1020:                                                 }
1021:                                         }
1022:                                 }
1023:                                 catch (ValueException e)
1024:                                 {
1025:                                         return VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
1026:                                 }
1027:                         }
1028:                 } catch (ValueException e)
1029:                 {
1030:                         return VdmRuntimeError.abort(node.getLocation(), e);
1031:                 }
1032:
1033:                 return new MapValue(map);
1034:         }
1035:
1036:         @Override
1037:         public Value caseAMapEnumMapExp(AMapEnumMapExp node, Context ctxt)
1038:                         throws AnalysisException
1039:         {
1040:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1041:
1042:                 ValueMap map = new ValueMap();
1043:
1044:                 for (AMapletExp e : node.getMembers())
1045:                 {
1046:                         Value l = e.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1047:                         Value r = e.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1048:                         e.getLocation().hit();
1049:                         Value old = map.put(l, r);
1050:
1051:                         if (old != null && !old.equals(r))
1052:                         {
1053:                                 VdmRuntimeError.abort(node.getLocation(), 4017, "Duplicate map keys have different values: "
1054:                                                 + l, ctxt);
1055:                         }
1056:                 }
1057:
1058:                 return new MapValue(map);
1059:         }
1060:
1061:         /*
1062:          * Map end
1063:          */
1064:
1065:         @Override
1066:         public Value caseAMapletExp(AMapletExp node, Context ctxt)
1067:                         throws AnalysisException
1068:         {
1069:                 // Not used
1070:                 return null;
1071:         }
1072:
1073:         @Override
1074:         public Value caseAMkBasicExp(AMkBasicExp node, Context ctxt)
1075:                         throws AnalysisException
1076:         {
1077:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1078:
1079:                 Value v = node.getArg().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1080:
1081:                 if (node.getType() instanceof ATokenBasicType)
1082:                 {
1083:                         return new TokenValue(v);
1084:                 } else
1085:                 {
1086:                         try
1087:                         {
1088:                                 v = v.convertTo(node.getType(), ctxt);
1089:                         } catch (ValueException e)
1090:                         {
1091:                                 VdmRuntimeError.abort(node.getLocation(), 4022, "mk_ type argument is not "
1092:                                                 + node.getType(), ctxt);
1093:                         }
1094:                 }
1095:
1096:                 return v;
1097:         }
1098:
1099:         @Override
1100:         public Value caseAMkTypeExp(AMkTypeExp node, Context ctxt)
1101:                         throws AnalysisException
1102:         {
1103:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1104:
1105:                 ValueList argvals = new ValueList();
1106:
1107:                 for (PExp e : node.getArgs())
1108:                 {
1109:                         argvals.add(e.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1110:                 }
1111:
1112:                 try
1113:                 {
1114:                         return new RecordValue(node.getRecordType(), argvals, ctxt);
1115:                 } catch (ValueException e)
1116:                 {
1117:                         return VdmRuntimeError.abort(node.getLocation(), e);
1118:                 }
1119:         }
1120:
1121:         @Override
1122:         public Value caseAMuExp(AMuExp node, Context ctxt) throws AnalysisException
1123:         {
1124:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1125:
1126:                 try
1127:                 {
1128:                         RecordValue r = node.getRecord().apply(VdmRuntime.getExpressionEvaluator(), ctxt).recordValue(ctxt);
1129:                         FieldMap fields = new FieldMap(r.fieldmap);
1130:
1131:                         for (ARecordModifier rm : node.getModifiers())
1132:                         {
1133:                                 AFieldField f = ctxt.assistantFactory.createARecordInvariantTypeAssistant().findField(r.type, rm.getTag().getName());
1134:
1135:                                 if (f == null)
1136:                                 {
1137:                                         VdmRuntimeError.abort(node.getLocation(), 4023, "Mu type conflict? No field tag "
1138:                                                         + rm.getTag().getName(), ctxt);
1139:                                 } else
1140:                                 {
1141:                                         fields.add(rm.getTag().getName(), rm.getValue().apply(VdmRuntime.getExpressionEvaluator(), ctxt), !f.getEqualityAbstraction());
1142:                                 }
1143:                         }
1144:
1145:                         return new RecordValue(r.type, fields, ctxt);
1146:                 } catch (ValueException e)
1147:                 {
1148:                         return VdmRuntimeError.abort(node.getLocation(), e);
1149:                 }
1150:         }
1151:
1152:         @Override
1153:         public Value caseANarrowExp(ANarrowExp node, Context ctxt)
1154:                         throws AnalysisException
1155:         {
1156:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1157:
1158:                 Value v = node.getTest().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1159:
1160:                 try
1161:                 {
1162:
1163:                         if (node.getTypeName() != null)
1164:                         {
1165:
1166:                                 if (ctxt.assistantFactory.createPDefinitionAssistant().isTypeDefinition(node.getTypedef()))
1167:                                 {
1168:                                         // NB. we skip the DTC enabled check here
1169:                                         v = v.convertValueTo(ctxt.assistantFactory.createPDefinitionAssistant().getType(node.getTypedef()), ctxt);
1170:                                 } else if (v.isType(RecordValue.class))
1171:                                 {
1172:                                         v = v.recordValue(ctxt);
1173:                                 }
1174:                         } else
1175:                         {
1176:                                 // NB. we skip the DTC enabled check here
1177:                                 v = v.convertValueTo(node.getBasicType(), ctxt);
1178:                         }
1179:                 } catch (ValueException ex)
1180:                 {
1181:                         VdmRuntimeError.abort(node.getLocation(), ex);
1182:                 }
1183:
1184:                 return v;
1185:         }
1186:
1187:         @Override
1188:         public Value caseANewExp(ANewExp node, Context ctxt)
1189:                         throws AnalysisException
1190:         {
1191:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1192:                 node.getClassName().getLocation().hit();
1193:
1194:                 try
1195:                 {
1196:                         ValueList argvals = new ValueList();
1197:
1198:•                        for (PExp arg : node.getArgs())
1199:                         {
1200:                                 argvals.add(arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1201:                         }
1202:
1203:                         ObjectValue objval = ctxt.assistantFactory.createSClassDefinitionAssistant().newInstance(node.getClassdef(), node.getCtorDefinition(), argvals, ctxt);
1204:
1205:•                        if (objval.invlistener != null)
1206:                         {
1207:                                 // Check the initial values of the object's fields
1208:                                 objval.invlistener.doInvariantChecks = true;
1209:                                 objval.invlistener.changedValue(node.getLocation(), objval, ctxt);
1210:                         }
1211:
1212:                         return objval;
1213:                 } catch (ValueException e)
1214:                 {
1215:                         return VdmRuntimeError.abort(node.getLocation(), e);
1216:                 }
1217:         }
1218:
1219:         @Override
1220:         public Value caseANilExp(ANilExp node, Context ctxt)
1221:                         throws AnalysisException
1222:         {
1223:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1224:
1225:                 return new NilValue();
1226:         }
1227:
1228:         @Override
1229:         public Value caseANotYetSpecifiedExp(ANotYetSpecifiedExp node, Context ctxt)
1230:                         throws AnalysisException
1231:         {
1232:                 return evalANotYetSpecified(node, node.getLocation(), 4024, "expression", ctxt);
1233:         }
1234:
1235:         protected Value evalANotYetSpecified(INode node, ILexLocation location,
1236:                         int abortNumber, String type, Context ctxt)
1237:                         throws AnalysisException
1238:         {
1239:                 BreakpointManager.getBreakpoint(node).check(location, ctxt);
1240:
1241:                 return VdmRuntimeError.abort(location, abortNumber, "'not yet specified' "
1242:                                 + type + " reached", ctxt);
1243:         }
1244:
1245:         @Override
1246:         public Value caseAPostOpExp(APostOpExp node, Context ctxt)
1247:                         throws AnalysisException
1248:         {
1249:                 // No break check here, as we want to start in the expression
1250:
1251:                 // The postcondition function arguments are the function args, the
1252:                 // result, the old/new state (if any). These all exist in ctxt.
1253:                 // We find the Sigma record and expand its contents to give additional
1254:                 // values in ctxt for each field. Ditto with Sigma~.
1255:
1256:                 try
1257:                 {
1258:                         if (node.getState() != null)
1259:                         {
1260:                                 RecordValue sigma = ctxt.lookup(node.getState().getName()).recordValue(ctxt);
1261:
1262:                                 for (AFieldField field : node.getState().getFields())
1263:                                 {
1264:                                         ctxt.put(field.getTagname(), sigma.fieldmap.get(field.getTag()));
1265:                                 }
1266:
1267:                                 RecordValue oldsigma = ctxt.lookup(node.getState().getName().getOldName()).recordValue(ctxt);
1268:
1269:                                 for (AFieldField field : node.getState().getFields())
1270:                                 {
1271:                                         ctxt.put(field.getTagname().getOldName(), oldsigma.fieldmap.get(field.getTag()));
1272:                                 }
1273:                         } else if (ctxt instanceof ObjectContext)
1274:                         {
1275:                                 ObjectContext octxt = (ObjectContext) ctxt;
1276:                                 ILexNameToken selfname = node.getOpname().getSelfName();
1277:                                 ILexNameToken oldselfname = selfname.getOldName();
1278:
1279:                                 ObjectValue self = octxt.lookup(selfname).objectValue(ctxt);
1280:                                 ValueMap oldvalues = octxt.lookup(oldselfname).mapValue(ctxt);
1281:
1282:                                 // If the opname was defined in a superclass of "self", we have
1283:                                 // to discover the subobject to populate its state variables.
1284:
1285:                                 ObjectValue subself = ctxt.assistantFactory.createAPostOpExpAssistant().findObject(node, node.getOpname().getModule(), self);
1286:
1287:                                 if (self.superobjects.size() == 0)
1288:                                 {
1289:                                         subself = self;
1290:                                 }
1291:
1292:                                 if (subself == null)
1293:                                 {
1294:                                         VdmRuntimeError.abort(node.getLocation(), 4026, "Cannot create post_op environment", ctxt);
1295:                                 }
1296:
1297:                                 // Create an object context using the "self" passed in, rather
1298:                                 // than the self that we're being called from, assuming they
1299:                                 // are different.
1300:
1301:                                 if (subself != octxt.self)
1302:                                 {
1303:                                         ObjectContext selfctxt = new ObjectContext(ctxt.assistantFactory, ctxt.location, "postcondition's object", ctxt, subself);
1304:
1305:                                         selfctxt.putAll(ctxt); // To add "RESULT" and args.
1306:                                         ctxt = selfctxt;
1307:                                 }
1308:
1309:                                 ctxt.assistantFactory.createAPostOpExpAssistant().populate(node, ctxt, subself.type.getName().getName(), oldvalues); // To
1310:                                                                                                                                                                                                                                                                                 // add
1311:                                                                                                                                                                                                                                                                                 // old
1312:                                                                                                                                                                                                                                                                                 // "~"
1313:                                 // values
1314:                         } else if (ctxt instanceof ClassContext)
1315:                         {
1316:                                 ILexNameToken selfname = node.getOpname().getSelfName();
1317:                                 ILexNameToken oldselfname = selfname.getOldName();
1318:                                 ValueMap oldvalues = ctxt.lookup(oldselfname).mapValue(ctxt);
1319:                                 ctxt.assistantFactory.createAPostOpExpAssistant().populate(node, ctxt, node.getOpname().getModule(), oldvalues);
1320:                         }
1321:
1322:                         // If there are errs clauses, and there is a precondition defined, then
1323:                         // we evaluate that as well as the postcondition.
1324:
1325:                         boolean result = (node.getErrors().isEmpty()
1326:                                         || node.getPreexpression() == null || node.getPreexpression().apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt))
1327:                                         && node.getPostexpression().apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt);
1328:
1329:                         node.setErrorLocation(node.getLocation());// FIXME not good
1330:
1331:                         if (node.getErrors() != null)
1332:                         {
1333:                                 for (AErrorCase err : node.getErrors())
1334:                                 {
1335:                                         boolean left = err.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt);
1336:                                         boolean right = err.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt);
1337:
1338:                                         if (left && !right)
1339:                                         {
1340:                                                 node.setErrorLocation(err.getLeft().getLocation());// FIXME not good
1341:                                         }
1342:
1343:                                         result = result || left && right;
1344:                                 }
1345:                         }
1346:
1347:                         return new BooleanValue(result);
1348:                 } catch (ValueException e)
1349:                 {
1350:                         return VdmRuntimeError.abort(node.getLocation(), e);
1351:                 }
1352:         }
1353:
1354:         @Override
1355:         public Value caseAPreExp(APreExp node, Context ctxt)
1356:                         throws AnalysisException
1357:         {
1358:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1359:
1360:                 Value fv = node.getFunction().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1361:
1362:                 if (fv instanceof FunctionValue)
1363:                 {
1364:                         FunctionValue tfv = (FunctionValue) fv;
1365:
1366:                         while (true)
1367:                         {
1368:                                 if (tfv instanceof CompFunctionValue)
1369:                                 {
1370:                                         tfv = ((CompFunctionValue) tfv).ff1;
1371:                                         continue;
1372:                                 }
1373:
1374:                                 if (tfv instanceof IterFunctionValue)
1375:                                 {
1376:                                         tfv = ((IterFunctionValue) tfv).function;
1377:                                         continue;
1378:                                 }
1379:
1380:                                 break;
1381:                         }
1382:
1383:                         FunctionValue pref = tfv.precondition;
1384:
1385:                         if (pref == null)
1386:                         {
1387:                                 return new BooleanValue(true);
1388:                         }
1389:
1390:                         if (pref.type.getParameters().size() <= node.getArgs().size())
1391:                         {
1392:                                 try
1393:                                 {
1394:                                         ValueList argvals = new ValueList();
1395:                                         Iterator<PExp> aiter = node.getArgs().iterator();
1396:
1397:                                         for (@SuppressWarnings("unused")
1398:                                         PType t : pref.type.getParameters())
1399:                                         {
1400:                                                 argvals.add(aiter.next().apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1401:                                         }
1402:
1403:                                         return pref.eval(node.getLocation(), argvals, ctxt);
1404:                                 } catch (ValueException e)
1405:                                 {
1406:                                         VdmRuntimeError.abort(node.getLocation(), e);
1407:                                 }
1408:                         }
1409:
1410:                         // else true, below.
1411:                 }
1412:
1413:                 return new BooleanValue(true);
1414:         }
1415:
1416:         @Override
1417:         public Value caseAPreOpExp(APreOpExp node, Context ctxt)
1418:                         throws AnalysisException
1419:         {
1420:                 try
1421:                 {
1422:                         BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1423:
1424:                         // The precondition function arguments are the function args,
1425:                         // plus the state (if any). These all exist in ctxt. We find the
1426:                         // Sigma record and expand its contents to give additional
1427:                         // values in ctxt for each field.
1428:
1429:                         if (node.getState() != null)
1430:                         {
1431:                                 try
1432:                                 {
1433:                                         RecordValue sigma = ctxt.lookup(node.getState().getName()).recordValue(ctxt);
1434:
1435:                                         for (AFieldField field : node.getState().getFields())
1436:                                         {
1437:                                                 ctxt.put(field.getTagname(), sigma.fieldmap.get(field.getTag()));
1438:                                         }
1439:                                 } catch (ValueException e)
1440:                                 {
1441:                                         VdmRuntimeError.abort(node.getLocation(), e);
1442:                                 }
1443:                         } else if (ctxt instanceof ObjectContext)
1444:                         {
1445:                                 ObjectContext octxt = (ObjectContext) ctxt;
1446:                                 ILexNameToken selfname = node.getOpname().getSelfName();
1447:                                 ObjectValue self = octxt.lookup(selfname).objectValue(ctxt);
1448:
1449:                                 // Create an object context using the "self" passed in, rather
1450:                                 // than the self that we're being called from.
1451:
1452:                                 ObjectContext selfctxt = new ObjectContext(ctxt.assistantFactory, ctxt.location, "precondition's object", ctxt, self);
1453:
1454:                                 selfctxt.putAll(ctxt); // To add "RESULT" and args.
1455:                                 ctxt = selfctxt;
1456:                         }
1457:
1458:                         boolean result = node.getExpression().apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt);
1459:
1460:                         if (node.getErrors() != null)
1461:                         {
1462:                                 for (AErrorCase err : node.getErrors())
1463:                                 {
1464:                                         result = result
1465:                                                         || err.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).boolValue(ctxt);
1466:                                 }
1467:                         }
1468:
1469:                         return new BooleanValue(result);
1470:                 } catch (ValueException e)
1471:                 {
1472:                         return VdmRuntimeError.abort(node.getLocation(), e);
1473:                 }
1474:         }
1475:
1476:         @Override
1477:         public Value caseASameBaseClassExp(ASameBaseClassExp node, Context ctxt)
1478:                         throws AnalysisException
1479:         {
1480:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1481:
1482:                 try
1483:                 {
1484:                         Value l = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1485:                         Value r = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1486:
1487:                         if (!l.isType(ObjectValue.class) || !r.isType(ObjectValue.class))
1488:                         {
1489:                                 return new BooleanValue(false);
1490:                         }
1491:
1492:                         ObjectValue lv = l.objectValue(ctxt);
1493:                         ObjectValue rv = r.objectValue(ctxt);
1494:
1495:                         PTypeList lbases = lv.getBaseTypes();
1496:                         PTypeList rbases = rv.getBaseTypes();
1497:
1498:                         for (PType ltype : lbases)
1499:                         {
1500:                                 if (rbases.contains(ltype))
1501:                                 {
1502:                                         return new BooleanValue(true);
1503:                                 }
1504:                         }
1505:
1506:                         return new BooleanValue(false);
1507:                 } catch (ValueException e)
1508:                 {
1509:                         return VdmRuntimeError.abort(node.getLocation(), e);
1510:                 }
1511:         }
1512:
1513:         @Override
1514:         public Value caseASameClassExp(ASameClassExp node, Context ctxt)
1515:                         throws AnalysisException
1516:         {
1517:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1518:
1519:                 try
1520:                 {
1521:                         Value l = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1522:                         Value r = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1523:
1524:                         if (!l.isType(ObjectValue.class) || !r.isType(ObjectValue.class))
1525:                         {
1526:                                 return new BooleanValue(false);
1527:                         }
1528:
1529:                         ObjectValue lv = l.objectValue(ctxt);
1530:                         ObjectValue rv = r.objectValue(ctxt);
1531:
1532:                         return new BooleanValue(lv.type.equals(rv.type));
1533:                 } catch (ValueException e)
1534:                 {
1535:                         return VdmRuntimeError.abort(node.getLocation(), e);
1536:                 }
1537:         }
1538:
1539:         /*
1540:          * Seq
1541:          */
1542:
1543:         @Override
1544:         public Value caseASeqCompSeqExp(ASeqCompSeqExp node, Context ctxt)
1545:                         throws AnalysisException
1546:         {
1547:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1548:
1549:                 if (node.getBind() instanceof ASetBind)
1550:                 {
1551:                         return evalSetBind(node, ctxt);
1552:                 }
1553:                 else
1554:                 {
1555:                         return evalSeqBind(node, ctxt);
1556:                 }
1557:         }
1558:         
1559:         private Value evalSeqBind(ASeqCompSeqExp node, Context ctxt) throws AnalysisException
1560:         {
1561:                 ValueList allValues = ctxt.assistantFactory.createPBindAssistant().getBindValues(node.getBind(), ctxt, false);
1562:                 ValueList seq = new ValueList();        // Bind variable values
1563:
1564:                 for (Value val: allValues)
1565:                 {
1566:                         try
1567:                         {
1568:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "seq comprehension", ctxt);
1569:                                 NameValuePairList nvpl = ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getBind().getPattern(), val, ctxt);
1570:
1571:                                 evalContext.putList(nvpl);
1572:
1573:                                 if (node.getPredicate() == null
1574:                                         || node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt))
1575:                                 {
1576:                                         Value out = node.getFirst().apply(VdmRuntime.getExpressionEvaluator(), evalContext);
1577:                                         seq.add(out);
1578:                                 }
1579:                         }
1580:                         catch (ValueException e)
1581:                         {
1582:                                 VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
1583:                         }
1584:                         catch (PatternMatchException e)
1585:                         {
1586:                                 // Ignore mismatches
1587:                         }
1588:                 }
1589:
1590:                 return new SeqValue(seq);
1591:         }
1592:
1593:         private Value evalSetBind(ASeqCompSeqExp node, Context ctxt) throws AnalysisException
1594:         {
1595:                 ValueList allValues = ctxt.assistantFactory.createPBindAssistant().getBindValues(node.getBind(), ctxt, false);
1596:                 ValueSet seq = new ValueSet(); // Bind variable values
1597:                 ValueMap map = new ValueMap(); // Map bind values to output values
1598:                 int count = 0;
1599:
1600:                 for (Value val : allValues)
1601:                 {
1602:                         try
1603:                         {
1604:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "seq comprehension", ctxt);
1605:                                 NameValuePairList nvpl = ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getBind().getPattern(), val, ctxt);
1606:                                 Value sortOn = nvpl.isEmpty() ? new NaturalValue(count++) : nvpl.get(0).value;
1607:
1608:                                 if (map.get(sortOn) == null)
1609:                                 {
1610:                                         if (nvpl.size() > 1 || !sortOn.isOrdered())
1611:                                         {
1612:                                                 VdmRuntimeError.abort(node.getLocation(), 4029, "Sequence comprehension bindings must be one ordered value", ctxt);
1613:                                         }
1614:
1615:                                         evalContext.putList(nvpl);
1616:
1617:                                         if (node.getPredicate() == null
1618:                                                         || node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt))
1619:                                         {
1620:                                                 Value out = node.getFirst().apply(VdmRuntime.getExpressionEvaluator(), evalContext);
1621:                                                 seq.add(sortOn);
1622:                                                 map.put(sortOn, out);
1623:                                         }
1624:                                 }
1625:                         }
1626:                         catch (ValueException e)
1627:                         {
1628:                                 VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
1629:                         }
1630:                         catch (PatternMatchException e)
1631:                         {
1632:                                 // Ignore mismatches
1633:                         }
1634:                         catch (ContextException e)
1635:                         {
1636:                                 throw e;
1637:                         }
1638:                         catch (Exception e)
1639:                         {
1640:                                 // Ignore NaturalValue exception
1641:                         }
1642:                 }
1643:
1644:                 Collections.sort(seq); // Using compareTo
1645:                 ValueList sorted = new ValueList();
1646:
1647:                 for (Value bv : seq)
1648:                 {
1649:                         sorted.add(map.get(bv));
1650:                 }
1651:
1652:                 return new SeqValue(sorted);
1653:         }
1654:
1655:         @Override
1656:         public Value caseASeqEnumSeqExp(ASeqEnumSeqExp node, Context ctxt)
1657:                         throws AnalysisException
1658:         {
1659:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1660:
1661:                 ValueList values = new ValueList();
1662:
1663:                 for (PExp e : node.getMembers())
1664:                 {
1665:                         values.add(e.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1666:                 }
1667:
1668:                 return new SeqValue(values);
1669:         }
1670:
1671:         /*
1672:          * seq end
1673:          */
1674:
1675:         /*
1676:          * (non-Javadoc) Set start
1677:          * @see
1678:          * org.overture.ast.analysis.QuestionAnswerAdaptor#caseAStateInitExp(org.overture.ast.expressions.AStateInitExp,
1679:          * java.lang.Object)
1680:          */
1681:         @Override
1682:         public Value caseASetEnumSetExp(ASetEnumSetExp node, Context ctxt)
1683:                         throws AnalysisException
1684:         {
1685:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1686:
1687:                 ValueSet values = new ValueSet();
1688:
1689:                 for (PExp e : node.getMembers())
1690:                 {
1691:                         values.add(e.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1692:                 }
1693:
1694:                 return new SetValue(values);
1695:         }
1696:
1697:         @Override
1698:         public Value caseASetCompSetExp(ASetCompSetExp node, Context ctxt)
1699:                         throws AnalysisException
1700:         {
1701:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1702:                 ValueSet set = new ValueSet();
1703:
1704:                 try
1705:                 {
1706:                         QuantifierList quantifiers = new QuantifierList();
1707:
1708:                         for (PMultipleBind mb : node.getBindings())
1709:                         {
1710:                                 ValueList bvals = ctxt.assistantFactory.createPMultipleBindAssistant().getBindValues(mb, ctxt, false);
1711:
1712:                                 for (PPattern p : mb.getPlist())
1713:                                 {
1714:                                         Quantifier q = new Quantifier(p, bvals);
1715:                                         quantifiers.add(q);
1716:                                 }
1717:                         }
1718:
1719:                         quantifiers.init(ctxt, false);
1720:
1721:                         while (quantifiers.hasNext())
1722:                         {
1723:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "set comprehension", ctxt);
1724:                                 NameValuePairList nvpl = quantifiers.next();
1725:                                 boolean matches = true;
1726:
1727:                                 for (NameValuePair nvp : nvpl)
1728:                                 {
1729:                                         Value v = evalContext.get(nvp.name);
1730:
1731:                                         if (v == null)
1732:                                         {
1733:                                                 evalContext.put(nvp.name, nvp.value);
1734:                                         } else
1735:                                         {
1736:                                                 if (!v.equals(nvp.value))
1737:                                                 {
1738:                                                         matches = false;
1739:                                                         break; // This quantifier set does not match
1740:                                                 }
1741:                                         }
1742:                                 }
1743:
1744:                                 try
1745:                                 {
1746:                                         if (matches
1747:                                                         && (node.getPredicate() == null || node.getPredicate().apply(VdmRuntime.getExpressionEvaluator(), evalContext).boolValue(ctxt)))
1748:                                         {
1749:                                                 set.add(node.getFirst().apply(VdmRuntime.getExpressionEvaluator(), evalContext));
1750:                                         }
1751:                                 }
1752:                                 catch (ValueException e)
1753:                                 {
1754:                                         return VdmRuntimeError.abort(node.getPredicate().getLocation(), e);
1755:                                 }
1756:                         }
1757:
1758:                         return new SetValue(set);
1759:                 }
1760:                 catch (ValueException e)
1761:                 {
1762:                         return VdmRuntimeError.abort(node.getLocation(), e);
1763:                 }
1764:         }
1765:
1766:         @Override
1767:         public Value caseASetRangeSetExp(ASetRangeSetExp node, Context ctxt)
1768:                         throws AnalysisException
1769:         {
1770:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1771:
1772:                 try
1773:                 {
1774:                         long from = (long) Math.ceil(node.getFirst().apply(VdmRuntime.getExpressionEvaluator(), ctxt).realValue(ctxt));
1775:                         long to = (long) Math.floor(node.getLast().apply(VdmRuntime.getExpressionEvaluator(), ctxt).realValue(ctxt));
1776:                         ValueSet set = new ValueSet();
1777:
1778:                         for (long i = from; i <= to; i++)
1779:                         {
1780:                                 set.addNoCheck(new IntegerValue(i));
1781:                         }
1782:
1783:                         return new SetValue(set);
1784:                 } catch (ValueException e)
1785:                 {
1786:                         return VdmRuntimeError.abort(node.getLocation(), e);
1787:                 }
1788:         }
1789:
1790:         @Override
1791:         public Value caseAStateInitExp(AStateInitExp node, Context ctxt)
1792:                         throws AnalysisException
1793:         {
1794:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1795:
1796:                 try
1797:                 {
1798:                         FunctionValue invariant = VdmRuntime.getNodeState(node.getState()).invfunc;
1799:
1800:                         // Note, the function just checks whether the argument passed would
1801:                         // violate the state invariant (if any). It doesn't initialize the
1802:                         // state itself. This is done in State.initialize().
1803:
1804:                         if (invariant != null)
1805:                         {
1806:                                 AIdentifierPattern argp = (AIdentifierPattern) node.getState().getInitPattern();
1807:                                 RecordValue rv = (RecordValue) ctxt.lookup(argp.getName());
1808:                                 return invariant.eval(node.getLocation(), rv, ctxt);
1809:                         }
1810:
1811:                         return new BooleanValue(true);
1812:                 } catch (ValueException e)
1813:                 {
1814:                         return VdmRuntimeError.abort(node.getLocation(), e);
1815:                 }
1816:         }
1817:
1818:         @Override
1819:         public Value caseASubclassResponsibilityExp(
1820:                         ASubclassResponsibilityExp node, Context ctxt)
1821:                         throws AnalysisException
1822:         {
1823:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1824:                 return VdmRuntimeError.abort(node.getLocation(), 4032, "'is subclass responsibility' expression reached", ctxt);
1825:         }
1826:
1827:         @Override
1828:         public Value caseASubseqExp(ASubseqExp node, Context ctxt)
1829:                         throws AnalysisException
1830:         {
1831:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1832:
1833:                 try
1834:                 {
1835:                         ValueList list = node.getSeq().apply(VdmRuntime.getExpressionEvaluator(), ctxt).seqValue(ctxt);
1836:                         double fr = node.getFrom().apply(VdmRuntime.getExpressionEvaluator(), ctxt).realValue(ctxt);
1837:                         double tr = node.getTo().apply(VdmRuntime.getExpressionEvaluator(), ctxt).realValue(ctxt);
1838:                         int fi = (int) Math.ceil(fr);
1839:                         int ti = (int) Math.floor(tr);
1840:
1841:                         if (fi < 1)
1842:                         {
1843:                                 fi = 1;
1844:                         }
1845:
1846:                         if (ti > list.size())
1847:                         {
1848:                                 ti = list.size();
1849:                         }
1850:
1851:                         ValueList result = new ValueList();
1852:
1853:                         if (fi <= ti)
1854:                         {
1855:                                 result.addAll(list.subList(fi - 1, ti));
1856:                         }
1857:
1858:                         return new SeqValue(result);
1859:                 } catch (ValueException e)
1860:                 {
1861:                         return VdmRuntimeError.abort(node.getLocation(), e);
1862:                 }
1863:         }
1864:
1865:         @Override
1866:         public Value caseAThreadIdExp(AThreadIdExp node, Context ctxt)
1867:                         throws AnalysisException
1868:         {
1869:                 try
1870:                 {
1871:                         node.getLocation().hit();
1872:                         return new NaturalValue(ctxt.threadState.threadId);
1873:                 } catch (Exception e)
1874:                 {
1875:                         return VdmRuntimeError.abort(node.getLocation(), 4065, e.getMessage(), ctxt);
1876:                 }
1877:         }
1878:
1879:         @Override
1880:         public Value caseATimeExp(ATimeExp node, Context ctxt)
1881:                         throws AnalysisException
1882:         {
1883:                 node.getLocation().hit();
1884:
1885:                 try
1886:                 {
1887:                         return new NaturalValue(SystemClock.getWallTime());
1888:                 } catch (Exception e)
1889:                 {
1890:                         return VdmRuntimeError.abort(node.getLocation(), 4145, "Time: "
1891:                                         + e.getMessage(), ctxt);
1892:                 }
1893:         }
1894:
1895:         @Override
1896:         public Value caseATupleExp(ATupleExp node, Context ctxt)
1897:                         throws AnalysisException
1898:         {
1899:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1900:
1901:                 ValueList argvals = new ValueList();
1902:
1903:                 for (PExp arg : node.getArgs())
1904:                 {
1905:                         argvals.add(arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1906:                 }
1907:
1908:                 return new TupleValue(argvals);
1909:         }
1910:
1911:         @Override
1912:         public Value caseAUndefinedExp(AUndefinedExp node, Context ctxt)
1913:                         throws AnalysisException
1914:         {
1915:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1916:
1917:                 return new UndefinedValue();
1918:         }
1919:
1920:         @Override
1921:         public Value caseAVariableExp(AVariableExp node, Context ctxt)
1922:                         throws AnalysisException
1923:         {
1924:                 // Experimental hood added for DESTECS
1925:                 if (Settings.dialect == Dialect.VDM_RT)
1926:                 {
1927:                         SharedStateListner.beforeVariableReadDuration(node);
1928:                 }
1929:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1930:                 return ctxt.lookup(node.getName());
1931:         }
1932:
1933:         @Override
1934:         public Value caseASelfExp(ASelfExp node, Context ctxt)
1935:                         throws AnalysisException
1936:         {
1937:                 node.getLocation().hit();
1938:                 return ctxt.lookup(node.getName());
1939:         }
1940:
1941:         @Override
1942:         public Value caseAIsOfBaseClassExp(AIsOfBaseClassExp node, Context ctxt)
1943:                         throws AnalysisException
1944:         {
1945:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1946:                 node.getBaseClass().getLocation().hit();
1947:
1948:                 try
1949:                 {
1950:                         Value v = node.getExp().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
1951:
1952:                         if (!(v instanceof ObjectValue))
1953:                         {
1954:                                 return new BooleanValue(false);
1955:                         }
1956:
1957:                         ObjectValue ov = v.objectValue(ctxt);
1958:                         return new BooleanValue(search(node, ov));
1959:                 } catch (ValueException e)
1960:                 {
1961:                         return VdmRuntimeError.abort(node.getLocation(), e);
1962:                 }
1963:         }
1964:
1965:         @Override
1966:         public Value caseAIsOfClassExp(AIsOfClassExp node, Context ctxt)
1967:                         throws AnalysisException
1968:         {
1969:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1970:                 node.getClassName().getLocation().hit();
1971:
1972:                 try
1973:                 {
1974:                         Value v = node.getExp().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
1975:
1976:                         if (!(v instanceof ObjectValue))
1977:                         {
1978:                                 return new BooleanValue(false);
1979:                         }
1980:
1981:                         ObjectValue ov = v.objectValue(ctxt);
1982:                         return new BooleanValue(isOfClass(ov, node.getClassName().getName()));
1983:                 } catch (ValueException e)
1984:                 {
1985:                         return VdmRuntimeError.abort(node.getLocation(), e);
1986:                 }
1987:         }
1988:         
1989:         public FunctionValue getPolymorphicValue(IInterpreterAssistantFactory af,
1990:                         AImplicitFunctionDefinition impdef, PTypeList actualTypes)
1991:         {
1992:
1993:                 Map<List<PType>, FunctionValue> polyfuncs = VdmRuntime.getNodeState(impdef).polyfuncs;
1994:
1995:                 if (polyfuncs == null)
1996:                 {
1997:                         polyfuncs = new HashMap<List<PType>, FunctionValue>();
1998:                 } else
1999:                 {
2000:                         // We always return the same function value for a polymorph
2001:                         // with a given set of types. This is so that the one function
2002:                         // value can record measure counts for recursive polymorphic
2003:                         // functions.
2004:
2005:                         FunctionValue rv = polyfuncs.get(actualTypes);
2006:
2007:                         if (rv != null)
2008:                         {
2009:                                 return rv;
2010:                         }
2011:                 }
2012:
2013:                 FunctionValue prefv = null;
2014:                 FunctionValue postfv = null;
2015:
2016:                 if (impdef.getPredef() != null)
2017:                 {
2018:                         prefv = af.createAExplicitFunctionDefinitionAssistant().getPolymorphicValue(af, impdef.getPredef(), actualTypes);
2019:                 } else
2020:                 {
2021:                         prefv = null;
2022:                 }
2023:
2024:                 if (impdef.getPostdef() != null)
2025:                 {
2026:                         postfv = af.createAExplicitFunctionDefinitionAssistant().getPolymorphicValue(af, impdef.getPostdef(), actualTypes);
2027:                 } else
2028:                 {
2029:                         postfv = null;
2030:                 }
2031:
2032:                 FunctionValue rv = new FunctionValue(af, impdef, actualTypes, prefv, postfv, null);
2033:
2034:                 polyfuncs.put(actualTypes, rv);
2035:                 return rv;
2036:         }
2037:         
2038:         public boolean search(AIsOfBaseClassExp node, ObjectValue from)
2039:         {
2040:                 if (from.type.getName().getName().equals(node.getBaseClass().getName())
2041:                                 && from.superobjects.isEmpty())
2042:                 {
2043:                         return true;
2044:                 }
2045:
2046:                 for (ObjectValue svalue : from.superobjects)
2047:                 {
2048:                         if (search(node, svalue))
2049:                         {
2050:                                 return true;
2051:                         }
2052:                 }
2053:
2054:                 return false;
2055:         }
2056:         
2057:         public boolean isOfClass(ObjectValue obj, String name)
2058:         {
2059:                 if (obj.type.getName().getName().equals(name))
2060:                 {
2061:                         return true;
2062:                 } else
2063:                 {
2064:                         for (ObjectValue objval : obj.superobjects)
2065:                         {
2066:                                 if (isOfClass(objval, name))
2067:                                 {
2068:                                         return true;
2069:                                 }
2070:                         }
2071:                 }
2072:
2073:                 return false;
2074:         }
2075: }