Method: TypeCompatibilityObligation(AExplicitFunctionDefinition, PType, PType, IPOContextStack, IPogAssistantFactory)

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.pog.obligation;
25:
26: import java.util.ArrayList;
27: import java.util.Iterator;
28: import java.util.List;
29: import java.util.Vector;
30:
31: import org.overture.ast.analysis.AnalysisException;
32: import org.overture.ast.definitions.AExplicitFunctionDefinition;
33: import org.overture.ast.definitions.AExplicitOperationDefinition;
34: import org.overture.ast.definitions.AImplicitFunctionDefinition;
35: import org.overture.ast.definitions.AImplicitOperationDefinition;
36: import org.overture.ast.expressions.ABooleanConstExp;
37: import org.overture.ast.expressions.ACharLiteralExp;
38: import org.overture.ast.expressions.AGreaterEqualNumericBinaryExp;
39: import org.overture.ast.expressions.AGreaterNumericBinaryExp;
40: import org.overture.ast.expressions.AIsExp;
41: import org.overture.ast.expressions.ALenUnaryExp;
42: import org.overture.ast.expressions.ALessEqualNumericBinaryExp;
43: import org.overture.ast.expressions.AMapEnumMapExp;
44: import org.overture.ast.expressions.AMapletExp;
45: import org.overture.ast.expressions.AMkTypeExp;
46: import org.overture.ast.expressions.ANotEqualBinaryExp;
47: import org.overture.ast.expressions.ANotYetSpecifiedExp;
48: import org.overture.ast.expressions.ASeqEnumSeqExp;
49: import org.overture.ast.expressions.ASetEnumSetExp;
50: import org.overture.ast.expressions.ASetRangeSetExp;
51: import org.overture.ast.expressions.ASubclassResponsibilityExp;
52: import org.overture.ast.expressions.ASubseqExp;
53: import org.overture.ast.expressions.ATupleExp;
54: import org.overture.ast.expressions.AVariableExp;
55: import org.overture.ast.expressions.PExp;
56: import org.overture.ast.factory.AstFactory;
57: import org.overture.ast.intf.lex.ILexLocation;
58: import org.overture.ast.lex.LexKeywordToken;
59: import org.overture.ast.lex.LexNameToken;
60: import org.overture.ast.lex.VDMToken;
61: import org.overture.ast.node.INode;
62: import org.overture.ast.patterns.AIdentifierPattern;
63: import org.overture.ast.patterns.APatternListTypePair;
64: import org.overture.ast.patterns.ATuplePattern;
65: import org.overture.ast.patterns.PPattern;
66: import org.overture.ast.types.ABooleanBasicType;
67: import org.overture.ast.types.ACharBasicType;
68: import org.overture.ast.types.AFieldField;
69: import org.overture.ast.types.ANamedInvariantType;
70: import org.overture.ast.types.ANatNumericBasicType;
71: import org.overture.ast.types.ANatOneNumericBasicType;
72: import org.overture.ast.types.AOperationType;
73: import org.overture.ast.types.AProductType;
74: import org.overture.ast.types.ARecordInvariantType;
75: import org.overture.ast.types.ASeq1SeqType;
76: import org.overture.ast.types.ASet1SetType;
77: import org.overture.ast.types.SSetType;
78: import org.overture.ast.types.AUnionType;
79: import org.overture.ast.types.PType;
80: import org.overture.ast.types.SBasicType;
81: import org.overture.ast.types.SInvariantType;
82: import org.overture.ast.types.SMapType;
83: import org.overture.ast.types.SNumericBasicType;
84: import org.overture.ast.types.SSeqType;
85: import org.overture.ast.util.PTypeSet;
86: import org.overture.pog.pub.IPOContextStack;
87: import org.overture.pog.pub.IPogAssistantFactory;
88: import org.overture.pog.pub.POType;
89:
90: public class TypeCompatibilityObligation extends ProofObligation
91: {
92:         private static final long serialVersionUID = 1108478780469068741L;
93:
94:         public final IPogAssistantFactory assistantFactory;
95:
96:         /**
97:          * Factory Method since we need to return null STOs (which should be discarded
98:          *
99:          * @param exp
100:          * The expression to be checked
101:          * @param etype
102:          * The expected type
103:          * @param atype
104:          * The actual type
105:          * @param ctxt
106:          * Context Information
107:          * @param assistantFactory
108:          * @return
109:          * @throws AnalysisException
110:          */
111:         public static TypeCompatibilityObligation newInstance(PExp exp,
112:                         PType etype, PType atype, IPOContextStack ctxt,
113:                         IPogAssistantFactory assistantFactory) throws AnalysisException
114:         {
115:
116:                 TypeCompatibilityObligation sto = new TypeCompatibilityObligation(exp, etype, atype, ctxt, assistantFactory);
117:                 if (sto.getValueTree() != null)
118:                 {
119:                         return sto;
120:                 }
121:
122:                 return null;
123:         }
124:
125:         public static TypeCompatibilityObligation newInstance(
126:                         AExplicitFunctionDefinition func, PType etype, PType atype,
127:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
128:                         throws AnalysisException
129:         {
130:                 TypeCompatibilityObligation sto = new TypeCompatibilityObligation(func, etype, atype, ctxt, assistantFactory);
131:                 if (sto.getValueTree() != null)
132:                 {
133:                         return sto;
134:                 }
135:
136:                 return null;
137:         }
138:
139:         public static TypeCompatibilityObligation newInstance(
140:                         AImplicitFunctionDefinition func, PType etype, PType atype,
141:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
142:                         throws AnalysisException
143:         {
144:                 TypeCompatibilityObligation sto = new TypeCompatibilityObligation(func, etype, atype, ctxt, assistantFactory);
145:                 if (sto.getValueTree() != null)
146:                 {
147:                         return sto;
148:                 }
149:
150:                 return null;
151:         }
152:
153:         public static TypeCompatibilityObligation newInstance(
154:                         AExplicitOperationDefinition def, PType actualResult,
155:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
156:                         throws AnalysisException
157:         {
158:                 TypeCompatibilityObligation sto = new TypeCompatibilityObligation(def, actualResult, ctxt, assistantFactory);
159:                 if (sto.getValueTree() != null)
160:                 {
161:                         return sto;
162:                 }
163:
164:                 return null;
165:         }
166:
167:         public static TypeCompatibilityObligation newInstance(
168:                         AImplicitOperationDefinition def, PType actualResult,
169:                         IPOContextStack ctxt, IPogAssistantFactory af)
170:                         throws AnalysisException
171:         {
172:                 TypeCompatibilityObligation sto = new TypeCompatibilityObligation(def, actualResult, ctxt, af);
173:                 if (sto.getValueTree() != null)
174:                 {
175:                         return sto;
176:                 }
177:
178:                 return null;
179:         }
180:
181:         /**
182:          * Help Constructor for the COMPASS Subtype POs <br>
183:          * <b> Do not use this constructor directly! </b> Use one of the factory methods instead
184:          *
185:          * @param root
186:          * The root node generating the PO
187:          * @param loc
188:          * The location of the root node
189:          * @param resultexp
190:          * The PExp identifying the result to be testes for subtyping
191:          * @param deftype
192:          * The declared type
193:          * @param actualtype
194:          * The actual type
195:          * @param ctxt
196:          * Context Information
197:          * @throws AnalysisException
198:          */
199:         protected TypeCompatibilityObligation(INode root, ILexLocation loc,
200:                         PExp resultexp, PType deftype, PType actualtype,
201:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
202:                         throws AnalysisException
203:         {
204:                 super(root, POType.TYPE_COMP, ctxt, loc, assistantFactory);
205:                 this.assistantFactory = assistantFactory;
206:                 stitch = oneType(false, resultexp, deftype, actualtype);
207:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
208:         }
209:
210:         private TypeCompatibilityObligation(PExp exp, PType etype, PType atype,
211:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
212:                         throws AnalysisException
213:         {
214:                 super(exp, POType.TYPE_COMP, ctxt, exp.getLocation(), assistantFactory);
215:                 this.assistantFactory = assistantFactory;
216:                 // valuetree.setContext(ctxt.getContextNodeList());
217:                 PExp onetype_exp = oneType(false, exp.clone(), etype.clone(), atype.clone());
218:
219:                 if (onetype_exp == null)
220:                 {
221:                         valuetree = null;
222:                 } else
223:                 {
224:                         stitch = onetype_exp;
225:                         valuetree.setPredicate(ctxt.getPredWithContext(onetype_exp));
226:                 }
227:         }
228:
229:         private TypeCompatibilityObligation(AExplicitFunctionDefinition func,
230:                         PType etype, PType atype, IPOContextStack ctxt,
231:                         IPogAssistantFactory assistantFactory) throws AnalysisException
232:         {
233:                 super(func, POType.TYPE_COMP, ctxt, func.getLocation(), assistantFactory);
234:                 this.assistantFactory = assistantFactory;
235:                 PExp body = null;
236:
237:•                if (func.getBody() instanceof ANotYetSpecifiedExp
238:•                                || func.getBody() instanceof ASubclassResponsibilityExp)
239:                 {
240:                         // We have to say "f(a)" because we have no body
241:                         PExp root = AstFactory.newAVariableExp(func.getName());
242:                         List<PExp> args = new ArrayList<PExp>();
243:
244:•                        for (PPattern p : func.getParamPatternList().get(0))
245:                         {
246:                                 args.add(patternToExp(p));
247:                         }
248:
249:                         body = AstFactory.newAApplyExp(root, args);
250:                 } else
251:                 {
252:                         body = func.getBody().clone();
253:                 }
254:
255:                 stitch = oneType(false, body, etype.clone(), atype.clone());
256:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
257:         }
258:
259:         private TypeCompatibilityObligation(AImplicitFunctionDefinition func,
260:                         PType etype, PType atype, IPOContextStack ctxt,
261:                         IPogAssistantFactory assistantFactory) throws AnalysisException
262:         {
263:                 super(func, POType.TYPE_COMP, ctxt, func.getLocation(), assistantFactory);
264:                 this.assistantFactory = assistantFactory;
265:                 PExp body = null;
266:
267:                 if (func.getBody() instanceof ANotYetSpecifiedExp
268:                                 || func.getBody() instanceof ASubclassResponsibilityExp)
269:                 {
270:                         // We have to say "f(a)" because we have no body
271:                         PExp root = AstFactory.newAVariableExp(func.getName());
272:                         List<PExp> args = new ArrayList<PExp>();
273:
274:                         for (APatternListTypePair pltp : func.getParamPatterns())
275:                         {
276:                                 for (PPattern p : pltp.getPatterns())
277:                                 {
278:                                         args.add(patternToExp(p));
279:                                 }
280:                         }
281:
282:                         body = AstFactory.newAApplyExp(root, args);
283:                 } else
284:                 {
285:                         body = func.getBody().clone();
286:                 }
287:
288:                 stitch = oneType(false, body, etype.clone(), atype.clone());
289:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
290:         }
291:
292:         private TypeCompatibilityObligation(AExplicitOperationDefinition def,
293:                         PType actualResult, IPOContextStack ctxt,
294:                         IPogAssistantFactory assistantFactory) throws AnalysisException
295:         {
296:                 super(def, POType.TYPE_COMP, ctxt, def.getLocation(), assistantFactory);
297:                 this.assistantFactory = assistantFactory;
298:
299:                 AVariableExp result = AstFactory.newAVariableExp(new LexNameToken(def.getName().getModule(), "RESULT", def.getLocation()));
300:
301:                 stitch = oneType(false, result, ((AOperationType) def.getType()).getResult().clone(), actualResult.clone());
302:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
303:         }
304:
305:         private TypeCompatibilityObligation(AImplicitOperationDefinition def,
306:                         PType actualResult, IPOContextStack ctxt,
307:                         IPogAssistantFactory assistantFactory) throws AnalysisException
308:         {
309:                 super(def, POType.TYPE_COMP, ctxt, def.getLocation(), assistantFactory);
310:                 this.assistantFactory = assistantFactory;
311:                 PExp result = null;
312:
313:                 if (def.getResult().getPattern() instanceof AIdentifierPattern)
314:                 {
315:                         AIdentifierPattern ip = (AIdentifierPattern) def.getResult().getPattern();
316:                         result = AstFactory.newAVariableExp(ip.getName());
317:                 } else
318:                 {
319:                         ATuplePattern tp = (ATuplePattern) def.getResult().getPattern();
320:                         List<PExp> args = new ArrayList<PExp>();
321:
322:                         for (PPattern p : tp.getPlist())
323:                         {
324:                                 AIdentifierPattern ip = (AIdentifierPattern) p;
325:                                 args.add(AstFactory.newAVariableExp(ip.getName()));
326:                         }
327:
328:                         result = AstFactory.newATupleExp(def.getLocation(), args);
329:                 }
330:
331:                 stitch = oneType(false, result, ((AOperationType) def.getType()).getResult().clone(), actualResult.clone());
332:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
333:         }
334:
335:         private PExp oneType(boolean rec, PExp exp, PType etype, PType atype)
336:         {
337:                 if (atype != null && rec)
338:                 {
339:                         if (assistantFactory.getTypeComparator().isSubType(atype, etype))
340:                         {
341:                                 return null; // Means a sub-comparison is OK without PO checks
342:                         }
343:                 }
344:
345:                 if (exp.getType() != null && etype != null && rec)
346:                 {
347:                         if (assistantFactory.getTypeComparator().isSubType(exp.getType(), etype))
348:                         {
349:                                 return null; // Means a sub-comparison is OK without PO checks
350:                         }
351:                 }
352:
353:                 PExp po = null;
354:                 etype = assistantFactory.createPTypeAssistant().deBracket(etype);
355:
356:                 if (etype instanceof AUnionType)
357:                 {
358:                         AUnionType ut = (AUnionType) etype;
359:                         PTypeSet possibles = new PTypeSet(assistantFactory);
360:
361:                         for (PType pos : ut.getTypes())
362:                         {
363:                                 if (atype == null
364:                                                 || assistantFactory.getTypeComparator().compatible(pos, atype))
365:                                 {
366:                                         possibles.add(pos);
367:                                 }
368:                         }
369:
370:                         po = null;
371:
372:                         for (PType poss : possibles)
373:                         {
374:                                 PExp s = oneType(true, exp, poss, null);
375:                                 PExp e = addIs(exp, poss);
376:
377:                                 if (s != null && !(s instanceof AIsExp))
378:                                 {
379:                                         e = makeAnd(e, s);
380:                                 }
381:
382:                                 po = makeOr(po, e);
383:                         }
384:                 } else if (etype instanceof SInvariantType)
385:                 {
386:                         SInvariantType et = (SInvariantType) etype;
387:                         po = null;
388:
389:                         if (et.getInvDef() != null)
390:                         {
391:                                 AVariableExp root = getVarExp(et.getInvDef().getName());
392:                                 root.setType(et.getInvDef().getType().clone());
393:                                 // This needs to be put back if/when we change the inv_R
394:                                 // signature to take
395:                                 // the record fields as arguments, rather than one R value.
396:                                 //
397:                                 // if (exp instanceof MkTypeExpression)
398:                                 // {
399:                                 // MkTypeExpression mk = (MkTypeExpression)exp;
400:                                 // sb.append(Utils.listToString(mk.args));
401:                                 // }
402:                                 // else
403:                                 // {
404:                                 // ab.append(exp);
405:                                 // }
406:
407:                                 po = getApplyExp(root, exp);
408:                                 po.setType(new ABooleanBasicType());
409:                         }
410:
411:                         if (etype instanceof ANamedInvariantType)
412:                         {
413:                                 ANamedInvariantType nt = (ANamedInvariantType) etype;
414:
415:                                 if (atype instanceof ANamedInvariantType)
416:                                 {
417:                                         atype = ((ANamedInvariantType) atype).getType();
418:                                 } else
419:                                 {
420:                                         atype = null;
421:                                 }
422:
423:                                 PExp s = oneType(true, exp, nt.getType(), atype);
424:
425:                                 if (s != null)
426:                                 {
427:                                         po = makeAnd(po, s);
428:                                 }
429:                         } else if (etype instanceof ARecordInvariantType)
430:                         {
431:                                 if (exp instanceof AMkTypeExp)
432:                                 {
433:                                         ARecordInvariantType rt = (ARecordInvariantType) etype;
434:                                         AMkTypeExp mk = (AMkTypeExp) exp;
435:
436:                                         if (rt.getFields().size() == mk.getArgs().size())
437:                                         {
438:                                                 Iterator<AFieldField> fit = rt.getFields().iterator();
439:                                                 Iterator<PType> ait = mk.getArgTypes().iterator();
440:
441:                                                 for (PExp e : mk.getArgs())
442:                                                 {
443:                                                         PExp s = oneType(true, e.clone(), fit.next().getType(), ait.next());
444:
445:                                                         if (s != null)
446:                                                         {
447:                                                                 po = makeAnd(po, s);
448:                                                         }
449:                                                 }
450:                                         }
451:                                 } else
452:                                 {
453:                                         po = makeAnd(po, addIs(exp, etype));
454:                                 }
455:                         } else
456:                         {
457:                                 po = makeAnd(po, addIs(exp, etype));
458:                         }
459:                 } else if (etype instanceof SSeqType)
460:                 {
461:                         po = null;
462:
463:                         if (etype instanceof ASeq1SeqType)
464:                         {
465:                                 ANotEqualBinaryExp ne = new ANotEqualBinaryExp();
466:                                 ne.setLeft(exp);
467:                                 ne.setOp(new LexKeywordToken(VDMToken.NE, exp.getLocation()));
468:                                 ASeqEnumSeqExp empty = new ASeqEnumSeqExp();
469:                                 empty.setMembers(new Vector<PExp>());
470:                                 ne.setRight(empty);
471:                                 
472:                                 po = ne;
473:                         }
474:
475:                         if (exp instanceof ASeqEnumSeqExp)
476:                         {
477:                                 SSeqType stype = (SSeqType) etype;
478:                                 ASeqEnumSeqExp seq = (ASeqEnumSeqExp) exp;
479:                                 Iterator<PType> it = seq.getTypes().iterator();
480:
481:                                 for (PExp m : seq.getMembers())
482:                                 {
483:                                         PExp s = oneType(true, m.clone(), stype.getSeqof().clone(), it.next().clone());
484:
485:                                         if (s != null)
486:                                         {
487:                                                 po = makeAnd(po, s);
488:                                         }
489:                                 }
490:                         } else if (exp instanceof ASubseqExp)
491:                         {
492:                                 ASubseqExp subseq = (ASubseqExp) exp;
493:                                 PType itype = AstFactory.newANatOneNumericBasicType(exp.getLocation());
494:                                 PExp s = oneType(true, subseq.getFrom().clone(), itype, subseq.getFtype());
495:
496:                                 if (s != null)
497:                                 {
498:                                         po = makeAnd(po, s);
499:                                 }
500:
501:                                 s = oneType(true, subseq.getTo().clone(), itype, subseq.getTtype());
502:
503:                                 if (s != null)
504:                                 {
505:                                         po = makeAnd(po, s);
506:                                 }
507:
508:                                 ALessEqualNumericBinaryExp le = new ALessEqualNumericBinaryExp();
509:                                 le.setLeft(subseq.getTo().clone());
510:                                 ALenUnaryExp len = new ALenUnaryExp();
511:                                 len.setExp(subseq.getSeq().clone());
512:                                 le.setRight(len);
513:                                 po = makeAnd(po, le);
514:
515:                                 po = makeAnd(po, addIs(exp, etype)); // Like set range does
516:                         } else
517:                         {
518:                                 po = addIs(exp, etype); // remove any "x <> []"
519:                         }
520:                 } else if (etype instanceof SMapType)
521:                 {
522:                         if (exp instanceof AMapEnumMapExp)
523:                         {
524:                                 SMapType mtype = (SMapType) etype;
525:                                 AMapEnumMapExp seq = (AMapEnumMapExp) exp;
526:                                 Iterator<PType> dit = seq.getDomTypes().iterator();
527:                                 Iterator<PType> rit = seq.getRngTypes().iterator();
528:                                 po = null;
529:
530:                                 for (AMapletExp m : seq.getMembers())
531:                                 {
532:                                         PExp s = oneType(true, m.getLeft(), mtype.getFrom(), dit.next());
533:
534:                                         if (s != null)
535:                                         {
536:                                                 po = makeAnd(po, s);
537:                                         }
538:
539:                                         s = oneType(true, m.getRight(), mtype.getTo(), rit.next());
540:
541:                                         if (s != null)
542:                                         {
543:                                                 po = makeAnd(po, s);
544:                                         }
545:                                 }
546:                         } else
547:                         {
548:                                 po = addIs(exp, etype);
549:                         }
550:                 } else if (etype instanceof SSetType)
551:                 {
552:                         po = null;
553:
554:                         if (etype instanceof ASet1SetType)
555:                         {
556:                                 ANotEqualBinaryExp ne = new ANotEqualBinaryExp();
557:                                 ne.setLeft(exp);
558:                                 ne.setOp(new LexKeywordToken(VDMToken.NE, exp.getLocation()));
559:                                 ASetEnumSetExp empty = new ASetEnumSetExp();
560:                                 empty.setMembers(new Vector<PExp>());
561:                                 ne.setRight(empty);
562:                                 
563:                                 po = ne;
564:                 }
565:
566:                         if (exp instanceof ASetEnumSetExp)
567:                         {
568:                                 SSetType stype = (SSetType) etype;
569:                                 ASetEnumSetExp set = (ASetEnumSetExp) exp;
570:                                 Iterator<PType> it = set.getTypes().iterator();
571:
572:                                 for (PExp m : set.getMembers())
573:                                 {
574:                                         PExp s = oneType(true, m.clone(), stype.getSetof(), it.next().clone());
575:
576:                                         if (s != null)
577:                                         {
578:                                                 po = makeAnd(po, s);
579:                                         }
580:                                 }
581:                         } else if (exp instanceof ASetRangeSetExp)
582:                         {
583:                                 SSetType stype = (SSetType) etype;
584:                                 ASetRangeSetExp range = (ASetRangeSetExp) exp;
585:                                 PType itype = AstFactory.newAIntNumericBasicType(exp.getLocation());
586:
587:                                 PExp s = oneType(true, range.getFirst(), itype, range.getFtype());
588:
589:                                 if (s != null)
590:                                 {
591:                                         po = makeAnd(po, s);
592:                                 }
593:
594:                                 s = oneType(true, range.getFirst(), stype.getSetof(), range.getFtype());
595:
596:                                 if (s != null)
597:                                 {
598:                                         po = makeAnd(po, s);
599:                                 }
600:
601:                                 s = oneType(true, range.getLast(), itype, range.getLtype());
602:
603:                                 if (s != null)
604:                                 {
605:                                         po = makeAnd(po, s);
606:                                 }
607:
608:                                 s = oneType(true, range.getLast(), stype.getSetof(), range.getLtype());
609:
610:                                 if (s != null)
611:                                 {
612:                                         po = makeAnd(po, s);
613:                                 }
614:                         }
615:
616:                         po = makeAnd(po, addIs(exp, etype));
617:                 } else if (etype instanceof AProductType)
618:                 {
619:                         if (exp instanceof ATupleExp)
620:                         {
621:                                 AProductType pt = (AProductType) etype;
622:                                 ATupleExp te = (ATupleExp) exp;
623:                                 Iterator<PType> eit = pt.getTypes().iterator();
624:                                 Iterator<PType> ait = te.getTypes().iterator();
625:                                 po = null;
626:
627:                                 for (PExp e : te.getArgs())
628:                                 {
629:                                         PExp s = oneType(true, e.clone(), eit.next(), ait.next());
630:
631:                                         if (s != null)
632:                                         {
633:                                                 po = makeAnd(po, s);
634:                                         }
635:                                 }
636:                         } else
637:                         {
638:                                 po = addIs(exp, etype);
639:                         }
640:                 } else if (etype instanceof SBasicType)
641:                 {
642:                         if (etype instanceof SNumericBasicType)
643:                         {
644:                                 SNumericBasicType ent = (SNumericBasicType) etype;
645:
646:                                 if (atype instanceof SNumericBasicType)
647:                                 {
648:                                         SNumericBasicType ant = (SNumericBasicType) atype;
649:
650:                                         if (assistantFactory.createSNumericBasicTypeAssistant().getWeight(ant) > assistantFactory.createSNumericBasicTypeAssistant().getWeight(ent))
651:                                         {
652:                                                 boolean isWhole = assistantFactory.createSNumericBasicTypeAssistant().getWeight(ant) < 3;
653:
654:                                                 if (isWhole && ent instanceof ANatOneNumericBasicType)
655:                                                 {
656:                                                         AGreaterNumericBinaryExp gt = new AGreaterNumericBinaryExp();
657:                                                         gt.setLeft(exp);
658:                                                         gt.setOp(new LexKeywordToken(VDMToken.GT, exp.getLocation()));
659:                                                         gt.setRight(getIntLiteral(0));
660:                                                         po = gt;
661:                                                 } else if (isWhole
662:                                                                 && ent instanceof ANatNumericBasicType)
663:                                                 {
664:                                                         AGreaterEqualNumericBinaryExp ge = new AGreaterEqualNumericBinaryExp();
665:                                                         ge.setLeft(exp);
666:                                                         ge.setOp(new LexKeywordToken(VDMToken.GE, exp.getLocation()));
667:                                                         ge.setRight(getIntLiteral(0));
668:                                                         po = ge;
669:                                                 } else
670:                                                 {
671:                                                         AIsExp isExp = new AIsExp();
672:                                                         isExp.setBasicType(ent);
673:                                                         isExp.setType(new ABooleanBasicType());
674:                                                         isExp.setTest(exp);
675:                                                         po = isExp;
676:                                                 }
677:                                         }
678:                                 } else
679:                                 {
680:                                         AIsExp isExp = new AIsExp();
681:                                         isExp.setBasicType(ent);
682:                                         isExp.setType(new ABooleanBasicType());
683:                                         isExp.setTest(exp);
684:                                         po = isExp;
685:                                 }
686:                         } else if (etype instanceof ABooleanBasicType)
687:                         {
688:                                 if (!(exp instanceof ABooleanConstExp))
689:                                 {
690:                                         po = addIs(exp, etype);
691:                                 }
692:                         } else if (etype instanceof ACharBasicType)
693:                         {
694:                                 if (!(exp instanceof ACharLiteralExp))
695:                                 {
696:                                         po = addIs(exp, etype);
697:                                 }
698:                         } else
699:                         {
700:                                 po = addIs(exp, etype);
701:                         }
702:                 } else
703:                 {
704:                         po = addIs(exp, etype);
705:                 }
706:
707:                 return po;
708:         }
709:
710:         /**
711:          * Just produce one is_(<expression>, <type>) node.
712:          */
713:         private PExp addIs(PExp exp, PType type)
714:         {
715:                 AIsExp isExp = new AIsExp();
716:                 isExp.setBasicType(type);
717:                 isExp.setType(new ABooleanBasicType());
718:                 isExp.setTest(exp.clone());
719:                 return isExp;
720:         }
721: }