Package: ImplicitDefinitionFinder

ImplicitDefinitionFinder

nameinstructionbranchcomplexitylinemethod
ImplicitDefinitionFinder(ITypeCheckerAssistantFactory)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAClassInvariantDefinition(AClassInvariantDefinition, Environment)
M: 0 C: 1
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
caseAEqualsDefinition(AEqualsDefinition, Environment)
M: 0 C: 1
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
caseAExplicitFunctionDefinition(AExplicitFunctionDefinition, Environment)
M: 0 C: 41
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
caseAExplicitOperationDefinition(AExplicitOperationDefinition, Environment)
M: 0 C: 47
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
caseAImplicitFunctionDefinition(AImplicitFunctionDefinition, Environment)
M: 0 C: 41
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
caseAImplicitOperationDefinition(AImplicitOperationDefinition, Environment)
M: 0 C: 41
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
caseAStateDefinition(AStateDefinition, Environment)
M: 0 C: 17
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
caseAThreadDefinition(AThreadDefinition, Environment)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
caseATypeDefinition(ATypeDefinition, Environment)
M: 0 C: 109
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 19
100%
M: 0 C: 1
100%
defaultPDefinition(PDefinition, Environment)
M: 0 C: 1
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
defaultSClassDefinition(SClassDefinition, Environment)
M: 79 C: 148
65%
M: 15 C: 25
63%
M: 11 C: 10
48%
M: 14 C: 32
70%
M: 0 C: 1
100%
findStateDefinition(Environment, INode)
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getInitDefinition(AStateDefinition)
M: 0 C: 59
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
getInvDefinition(AStateDefinition)
M: 0 C: 55
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
getInvDefinition(ATypeDefinition)
M: 0 C: 82
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 15
100%
M: 0 C: 1
100%
getPTypes(ATypeDefinition)
M: 0 C: 42
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
getRelDef(PRelation, ATypeDefinition, ILexNameToken)
M: 0 C: 63
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
getThreadDefinition(AThreadDefinition)
M: 0 C: 28
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
setMinMax(AOrdRelation, ATypeDefinition)
M: 0 C: 241
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 40
100%
M: 0 C: 1
100%

Coverage

1: /*
2: * #%~
3: * The VDM Type Checker
4: * %%
5: * Copyright (C) 2008 - 2014 Overture
6: * %%
7: * This program is free software: you can redistribute it and/or modify
8: * it under the terms of the GNU General Public License as
9: * published by the Free Software Foundation, either version 3 of the
10: * License, or (at your option) any later version.
11: *
12: * This program is distributed in the hope that it will be useful,
13: * but WITHOUT ANY WARRANTY; without even the implied warranty of
14: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15: * GNU General Public License for more details.
16: *
17: * You should have received a copy of the GNU General Public
18: * License along with this program. If not, see
19: * <http://www.gnu.org/licenses/gpl-3.0.html>.
20: * #~%
21: */
22: package org.overture.typechecker.utilities;
23:
24: import org.overture.ast.analysis.AnalysisException;
25: import org.overture.ast.analysis.QuestionAdaptor;
26: import org.overture.ast.assistant.pattern.PTypeList;
27: import org.overture.ast.definitions.*;
28: import org.overture.ast.definitions.relations.AOrdRelation;
29: import org.overture.ast.definitions.relations.PRelation;
30: import org.overture.ast.expressions.*;
31: import org.overture.ast.factory.AstFactory;
32: import org.overture.ast.factory.AstFactoryTC;
33: import org.overture.ast.intf.lex.ILexLocation;
34: import org.overture.ast.intf.lex.ILexNameToken;
35: import org.overture.ast.lex.LexNameToken;
36: import org.overture.ast.lex.LexToken;
37: import org.overture.ast.lex.VDMToken;
38: import org.overture.ast.node.INode;
39: import org.overture.ast.patterns.PPattern;
40: import org.overture.ast.typechecker.NameScope;
41: import org.overture.ast.types.*;
42: import org.overture.typechecker.Environment;
43: import org.overture.typechecker.TypeCheckerErrors;
44: import org.overture.typechecker.assistant.ITypeCheckerAssistantFactory;
45:
46: import java.util.LinkedList;
47: import java.util.List;
48: import java.util.Vector;
49:
50: /**
51: * This class implements a way to find ImplicitDefinitions from nodes from the AST.
52: *
53: * @author kel
54: */
55: public class ImplicitDefinitionFinder extends QuestionAdaptor<Environment>
56: {
57:
58:         protected ITypeCheckerAssistantFactory af;
59:
60:         public ImplicitDefinitionFinder(ITypeCheckerAssistantFactory af)
61:         {
62:                 this.af = af;
63:         }
64:
65:         protected AStateDefinition findStateDefinition(Environment question,
66:                         INode node)
67:         {
68:                 return question.findStateDefinition();
69:         }
70:
71:         @Override
72:         public void defaultSClassDefinition(SClassDefinition node,
73:                         Environment question) throws AnalysisException
74:         {
75:                 // TODO: should I expand this even more?
76:•                if (node instanceof ASystemClassDefinition)
77:                 {
78:                         // af.createASystemClassDefinitionAssistant().implicitDefinitions((ASystemClassDefinition)node, question);
79:
80:                         af.createSClassDefinitionAssistant().implicitDefinitionsBase(node, question);
81:
82:•                        for (PDefinition d : node.getDefinitions())
83:                         {
84:•                                if (d instanceof AInstanceVariableDefinition)
85:                                 {
86:                                         AInstanceVariableDefinition iv = (AInstanceVariableDefinition) d;
87:
88:                                         PType ivType = af.createPDefinitionAssistant().getType(iv);
89:•                                        if (ivType instanceof AUnresolvedType
90:•                                                        && iv.getExpression() instanceof AUndefinedExp)
91:                                         {
92:                                                 AUnresolvedType ut = (AUnresolvedType) ivType;
93:
94:•                                                if (ut.getName().getFullName().equals("BUS"))
95:                                                 {
96:                                                         TypeCheckerErrors.warning(5014, "Uninitialized BUS ignored", d.getLocation(), d);
97:                                                 }
98:•                                        } else if (ivType instanceof AUnresolvedType
99:•                                                        && iv.getExpression() instanceof ANewExp)
100:                                         {
101:                                                 AUnresolvedType ut = (AUnresolvedType) ivType;
102:
103:•                                                if (ut.getName().getFullName().equals("CPU"))
104:                                                 {
105:                                                         ANewExp newExp = (ANewExp) iv.getExpression();
106:•                                                        PExp exp = newExp.getArgs().size() > 1 ? newExp.getArgs().get(1) : null;
107:                                                         double speed = 0;
108:•                                                        if (exp instanceof AIntLiteralExp)
109:                                                         {
110:                                                                 AIntLiteralExp frequencyExp = (AIntLiteralExp) newExp.getArgs().get(1);
111:                                                                 speed = frequencyExp.getValue().getValue();
112:•                                                        } else if (exp instanceof ARealLiteralExp)
113:                                                         {
114:                                                                 ARealLiteralExp frequencyExp = (ARealLiteralExp) newExp.getArgs().get(1);
115:                                                                 speed = frequencyExp.getValue().getValue();
116:                                                         }
117:
118:•                                                        if (speed == 0)
119:                                                         {
120:                                                                 TypeCheckerErrors.report(3305, "CPU frequency to slow: "
121:                                                                                 + speed + " Hz", d.getLocation(), d);
122:•                                                        } else if (speed > AstFactoryTC.CPU_MAX_FREQUENCY)
123:                                                         {
124:                                                                 TypeCheckerErrors.report(3306, "CPU frequency to fast: "
125:                                                                                 + speed + " Hz", d.getLocation(), d);
126:                                                         }
127:                                                 }
128:                                         }
129:•                                } else if (d instanceof AExplicitOperationDefinition)
130:                                 {
131:                                         AExplicitOperationDefinition edef = (AExplicitOperationDefinition) d;
132:
133:•                                        if (!edef.getName().getName().equals(node.getName().getName())
134:•                                                        || !edef.getParameterPatterns().isEmpty())
135:                                         {
136:                                                 TypeCheckerErrors.report(3285, "System class can only define a default constructor", d.getLocation(), d);
137:                                         }
138:•                                } else if (d instanceof AImplicitOperationDefinition)
139:                                 {
140:                                         AImplicitOperationDefinition idef = (AImplicitOperationDefinition) d;
141:
142:•                                        if (!d.getName().getName().equals(node.getName().getName()))
143:                                         {
144:                                                 TypeCheckerErrors.report(3285, "System class can only define a default constructor", d.getLocation(), d);
145:                                         }
146:
147:•                                        if (idef.getBody() == null)
148:                                         {
149:                                                 TypeCheckerErrors.report(3283, "System class constructor cannot be implicit", d.getLocation(), d);
150:                                         }
151:                                 } else
152:                                 {
153:                                         TypeCheckerErrors.report(3284, "System class can only define instance variables and a constructor", d.getLocation(), d);
154:                                 }
155:                         }
156:                 }
157:                 {
158:                         af.createSClassDefinitionAssistant().implicitDefinitionsBase(node, question);
159:                 }
160:         }
161:
162:         @Override
163:         public void caseAClassInvariantDefinition(AClassInvariantDefinition node,
164:                         Environment question) throws AnalysisException
165:         {
166:
167:         }
168:
169:         @Override
170:         public void caseAEqualsDefinition(AEqualsDefinition node,
171:                         Environment question) throws AnalysisException
172:         {
173:
174:         }
175:
176:         @Override
177:         public void caseAExplicitFunctionDefinition(
178:                         AExplicitFunctionDefinition node, Environment question)
179:                         throws AnalysisException
180:         {
181:•                if (node.getPrecondition() != null)
182:                 {
183:                         node.setPredef(af.createAExplicitFunctionDefinitionAssistant().getPreDefinition(node));
184:                         // PDefinitionAssistantTC.markUsed(d.getPredef());//ORIGINAL CODE
185:                         af.getUsedMarker().caseAExplicitFunctionDefinition(node.getPredef());
186:                 } else
187:                 {
188:                         node.setPredef(null);
189:                 }
190:
191:•                if (node.getPostcondition() != null)
192:                 {
193:                         node.setPostdef(af.createAExplicitFunctionDefinitionAssistant().getPostDefinition(node));
194:                         // PDefinitionAssistantTC.markUsed(d.getPostdef());//ORIGINAL CODE
195:                         af.getUsedMarker().caseAExplicitFunctionDefinition(node.getPostdef());
196:                 } else
197:                 {
198:                         node.setPostdef(null);
199:                 }
200:         }
201:
202:         @Override
203:         public void caseAExplicitOperationDefinition(
204:                         AExplicitOperationDefinition node, Environment question)
205:                         throws AnalysisException
206:         {
207:                 node.setState(findStateDefinition(question, node));
208:
209:•                if (node.getPrecondition() != null)
210:                 {
211:                         node.setPredef(af.createAExplicitOperationDefinitionAssistant(node.getLocation().getModule()).getPreDefinition(node, question));
212:                         af.createPDefinitionAssistant().markUsed(node.getPredef()); // ORIGINAL CODE
213:                 }
214:
215:•                if (node.getPostcondition() != null)
216:                 {
217:                         node.setPostdef(af.createAExplicitOperationDefinitionAssistant(node.getLocation().getModule()).getPostDefinition(node, question));
218:                         af.createPDefinitionAssistant().markUsed(node.getPostdef());
219:                 }
220:         }
221:
222:         @Override
223:         public void caseAImplicitFunctionDefinition(
224:                         AImplicitFunctionDefinition node, Environment question)
225:                         throws AnalysisException
226:         {
227:
228:•                if (node.getPrecondition() != null)
229:                 {
230:                         node.setPredef(af.createAImplicitFunctionDefinitionAssistant().getPreDefinition(node));
231:                         af.createPDefinitionAssistant().markUsed(node.getPredef());
232:                         // af.createPDefinitionAssistant().markUsed(node.getPredef());
233:                 } else
234:                 {
235:                         node.setPredef(null);
236:                 }
237:
238:•                if (node.getPostcondition() != null)
239:                 {
240:                         node.setPostdef(af.createAImplicitFunctionDefinitionAssistant().getPostDefinition(node));
241:                         af.createPDefinitionAssistant().markUsed(node.getPostdef());
242:                 } else
243:                 {
244:                         node.setPostdef(null);
245:                 }
246:         }
247:
248:         @Override
249:         public void caseAImplicitOperationDefinition(
250:                         AImplicitOperationDefinition node, Environment question)
251:                         throws AnalysisException
252:         {
253:                 node.setState(findStateDefinition(question, node));
254:
255:•                if (node.getPrecondition() != null)
256:                 {
257:                         node.setPredef(af.createAImplicitOperationDefinitionAssistant().getPreDefinition(node, question));
258:                         af.createPDefinitionAssistant().markUsed(node.getPredef());
259:                 }
260:
261:•                if (node.getPostcondition() != null)
262:                 {
263:                         node.setPostdef(af.createAImplicitOperationDefinitionAssistant().getPostDefinition(node, question));
264:                         af.createPDefinitionAssistant().markUsed(node.getPostdef());
265:                 }
266:         }
267:
268:         @Override
269:         public void caseAStateDefinition(AStateDefinition node, Environment question)
270:                         throws AnalysisException
271:         {
272:•                if (node.getInvPattern() != null)
273:                 {
274:                         node.setInvdef(getInvDefinition(node));
275:                 }
276:
277:•                if (node.getInitPattern() != null)
278:                 {
279:                         node.setInitdef(getInitDefinition(node));
280:                 }
281:         }
282:
283:         @Override
284:         public void caseAThreadDefinition(AThreadDefinition node,
285:                         Environment question) throws AnalysisException
286:         {
287:                 // ORIGINAL CODE FROM ASSISTANT
288:                 // node.setOperationDef(AThreadDefinitionAssistantTC.getThreadDefinition(node));
289:                 // Mine non static call of the code.
290:                 node.setOperationDef(getThreadDefinition(node));
291:         }
292:
293:         @Override
294:         public void caseATypeDefinition(ATypeDefinition node, Environment question)
295:                         throws AnalysisException
296:         {
297:•                if (node.getInvPattern() != null)
298:                 {
299:                         // node.setInvdef(getInvDefinition(d)); //Original code from Assistant.
300:                         node.setInvdef(getInvDefinition(node));
301:                         node.getInvType().setInvDef(node.getInvdef());
302:                 } else
303:                 {
304:                         node.setInvdef(null);
305:                 }
306:
307:•                if (node.getOrdRelation() != null) {
308:                         node.getOrdRelation().setRelDef(getRelDef(node.getOrdRelation(),node,node.getName().getOrdName(node.getLocation().clone())));
309:                         node.getInvType().setOrdDef(node.getOrdRelation().getRelDef());
310:                         setMinMax(node.getOrdRelation(),node);
311:                 }
312:
313:•                if (node.getEqRelation() != null) {
314:                         node.getEqRelation().setRelDef(getRelDef(node.getEqRelation(),node,node.getName().getEqName(node.getLocation().clone())));
315:                         node.getInvType().setEqDef(node.getEqRelation().getRelDef());
316:                 }
317:
318:•                if (node.getInvType() instanceof ANamedInvariantType)
319:                 {
320:                         ANamedInvariantType ntype = (ANamedInvariantType) node.getInvType();
321:                         node.getComposeDefinitions().clear();
322:
323:•                        for (PType compose : af.createPTypeAssistant().getComposeTypes(ntype.getType()))
324:                         {
325:                                 ARecordInvariantType rtype = (ARecordInvariantType) compose;
326:                                 node.getComposeDefinitions().add(AstFactory.newATypeDefinition(rtype.getName(), rtype, null, null));
327:                         }
328:                 }
329:         }
330:
331:         @Override
332:         public void defaultPDefinition(PDefinition node, Environment question)
333:                         throws AnalysisException
334:         {
335:                 return;
336:         }
337:         
338:         public AExplicitFunctionDefinition getInitDefinition(AStateDefinition d)
339:         {
340:                 ILexLocation loc = d.getInitPattern().getLocation();
341:                 List<PPattern> params = new Vector<PPattern>();
342:                 params.add(d.getInitPattern().clone());
343:
344:                 List<List<PPattern>> parameters = new Vector<List<PPattern>>();
345:                 parameters.add(params);
346:
347:                 PTypeList ptypes = new PTypeList();
348:                 ptypes.add(AstFactory.newAUnresolvedType(d.getName()));
349:                 AFunctionType ftype = AstFactory.newAFunctionType(loc, false, ptypes, AstFactory.newABooleanBasicType(loc));
350:
351:                 PExp body = AstFactory.newAStateInitExp(d);
352:
353:                 AExplicitFunctionDefinition def = AstFactory.newAExplicitFunctionDefinition(d.getName().getInitName(loc), NameScope.GLOBAL, null, ftype, parameters, body, null, null, false, null);
354:
355:                 return def;
356:         }
357:
358:         public AExplicitFunctionDefinition getInvDefinition(AStateDefinition d)
359:         {
360:
361:                 ILexLocation loc = d.getInvPattern().getLocation();
362:                 List<PPattern> params = new Vector<PPattern>();
363:                 params.add(d.getInvPattern().clone());
364:
365:                 List<List<PPattern>> parameters = new Vector<List<PPattern>>();
366:                 parameters.add(params);
367:
368:                 PTypeList ptypes = new PTypeList();
369:                 ptypes.add(AstFactory.newAUnresolvedType(d.getName()));
370:                 AFunctionType ftype = AstFactory.newAFunctionType(loc, false, ptypes, AstFactory.newABooleanBasicType(loc));
371:
372:                 return AstFactory.newAExplicitFunctionDefinition(d.getName().getInvName(loc), NameScope.GLOBAL, null, ftype, parameters, d.getInvExpression(), null, null, true, null);
373:         }
374:
375:         private AExplicitFunctionDefinition getRelDef(PRelation node, ATypeDefinition typedef, ILexNameToken fname) {
376:                 ILexLocation loc = node.getLhsPattern().getLocation();
377:
378:                 List<PPattern> params = new Vector<PPattern>();
379:                 params.add(node.getLhsPattern().clone());
380:                 params.add(node.getRhsPattern().clone());
381:                 List<List<PPattern>> parameters = new Vector<List<PPattern>>();
382:                 parameters.add(params);
383:
384:                 PTypeList ptypes = getPTypes(typedef);
385:
386:                 AFunctionType ftype = AstFactory.newAFunctionType(loc, false, ptypes, AstFactory.newABooleanBasicType(loc));
387:                 AExplicitFunctionDefinition def = AstFactory.newAExplicitFunctionDefinition(fname, NameScope.GLOBAL, null, ftype, parameters,
388:                                 node.getRelExp(), null, null, false, null);
389:
390:                 def.setAccess(typedef.getAccess().clone()); // Same as type's
391:                 def.setClassDefinition(typedef.getClassDefinition());
392:
393:                 return def;
394:         }
395:
396:         private PTypeList getPTypes(ATypeDefinition typedef) {
397:                 PTypeList ptypes = new PTypeList();
398:•                if (typedef.getInvType() instanceof ARecordInvariantType)
399:                 {
400:                         // Records are inv_R: R +> bool
401:                         AUnresolvedType uType= AstFactory.newAUnresolvedType(typedef.getName().clone());
402:                         ptypes.add(uType.clone());
403:                         ptypes.add(uType.clone());
404:                 } else
405:                 {
406:                         // Named types are inv_T: x +> bool, for T = x
407:                         ANamedInvariantType nt = (ANamedInvariantType) typedef.getInvType();
408:                         ptypes.add(nt.getType().clone());
409:                         ptypes.add(nt.getType().clone());
410:                 }
411:                 return ptypes;
412:         }
413:
414:         private void setMinMax(AOrdRelation ordRelation, ATypeDefinition typeDef) {
415:                 ILexLocation loc = ordRelation.getRelDef().getLocation().clone();
416:                 String module = typeDef.getName().getModule();
417:
418:                 PExp left = AstFactoryTC.newAVariableExp(new LexNameToken(module, "x", loc.clone()));
419:                 PExp right = AstFactoryTC.newAVariableExp(new LexNameToken(module, "y", loc.clone()));
420:
421:                 List<PPattern> params = new LinkedList<>();
422:                 params.add(AstFactory.newAIdentifierPattern(new LexNameToken(module, "x", loc.clone())));
423:                 params.add(AstFactory.newAIdentifierPattern(new LexNameToken(module, "y", loc.clone())));
424:                 List<List<PPattern>> parameters = new Vector<List<PPattern>>();
425:                 parameters.add(params);
426:
427:                 AIfExp maxBody = AstFactoryTC.newAIfExp(loc.clone(),
428:                                 AstFactoryTC.newALessEqualNumericBinaryExp(left.clone(), new LexToken(loc.clone(), VDMToken.LE), right.clone()),
429:                                 right.clone(),
430:                                 new LinkedList<>(),
431:                                 left.clone());
432:
433:                 // PTypeList ptypes = getPTypes(typeDef);
434:                 PTypeList ptypes = new PTypeList();
435:                 ptypes.add(AstFactory.newAUnresolvedType(typeDef.getName()));
436:                 ptypes.add(AstFactory.newAUnresolvedType(typeDef.getName()));
437:
438:
439:                 AFunctionType ftype = AstFactory.newAFunctionType(loc.clone(), false, ptypes, AstFactory.newAUnresolvedType(typeDef.getName()));
440:                 AExplicitFunctionDefinition maxD = AstFactory.newAExplicitFunctionDefinition(typeDef.getName().getMaxName(loc), NameScope.GLOBAL, null, ftype, parameters,
441:                                 maxBody, null, null, true, null);
442:                 maxD.setAccess(typeDef.getAccess().clone()); // Same as type's
443:                 maxD.setClassDefinition(typeDef.getClassDefinition());
444:                 ordRelation.setMaxDef(maxD);
445:
446:                 AIfExp minBody = AstFactoryTC.newAIfExp(loc.clone(),
447:                                 AstFactoryTC.newALessEqualNumericBinaryExp(left.clone(), new LexToken(loc.clone(), VDMToken.LE), right.clone()),
448:                                 left.clone(),
449:                                 new LinkedList<>(),
450:                                 right.clone());
451:
452:                 // ptypes = getPTypes(typeDef);
453:                 ptypes = new PTypeList();
454:                 ptypes.add(AstFactory.newAUnresolvedType(typeDef.getName()));
455:                 ptypes.add(AstFactory.newAUnresolvedType(typeDef.getName()));
456:
457:                 List<PPattern> temp = new LinkedList<>();
458:•                for (PPattern a : parameters.get(0)) {
459:                         temp.add(a.clone());
460:                 }
461:                 List<List<PPattern>> parameters2 = new LinkedList<>();
462:                 parameters2.add((temp));
463:                 ftype = AstFactory.newAFunctionType(loc.clone(), false, ptypes, AstFactory.newAUnresolvedType(typeDef.getName()));
464:
465:                 AExplicitFunctionDefinition minD = AstFactory.newAExplicitFunctionDefinition(typeDef.getName().getMinName(loc), NameScope.GLOBAL, null, ftype, parameters2,
466:                                 minBody, null, null, true, null);
467:                 minD.setAccess(typeDef.getAccess().clone()); // Same as type's
468:                 minD.setClassDefinition(typeDef.getClassDefinition());
469:                 ordRelation.setMinDef(minD);
470:         }
471:
472:         public AExplicitFunctionDefinition getInvDefinition(ATypeDefinition d)
473:         {
474:
475:                 ILexLocation loc = d.getInvPattern().getLocation();
476:                 List<PPattern> params = new Vector<PPattern>();
477:                 params.add(d.getInvPattern().clone());
478:
479:                 List<List<PPattern>> parameters = new Vector<List<PPattern>>();
480:                 parameters.add(params);
481:
482:                 PTypeList ptypes = new PTypeList();
483:
484:•                if (d.getInvType() instanceof ARecordInvariantType)
485:                 {
486:                         // Records are inv_R: R +> bool
487:                         ptypes.add(AstFactory.newAUnresolvedType(d.getName().clone()));
488:                 } else
489:                 {
490:                         // Named types are inv_T: x +> bool, for T = x
491:                         ANamedInvariantType nt = (ANamedInvariantType) d.getInvType();
492:                         ptypes.add(nt.getType().clone());
493:                 }
494:
495:                 AFunctionType ftype = AstFactory.newAFunctionType(loc, false, ptypes, AstFactory.newABooleanBasicType(loc));
496:
497:                 AExplicitFunctionDefinition def = AstFactory.newAExplicitFunctionDefinition(d.getName().getInvName(loc), NameScope.GLOBAL, null, ftype, parameters, d.getInvExpression(), null, null, true, null);
498:
499:                 def.setAccess(d.getAccess().clone()); // Same as type's
500:                 def.setClassDefinition(d.getClassDefinition());
501:
502:                 return def;
503:         }
504:
505:         public AExplicitOperationDefinition getThreadDefinition(AThreadDefinition d)
506:         {
507:
508:                 AOperationType type = AstFactory.newAOperationType(d.getLocation()); // () ==> ()
509:
510:                 AExplicitOperationDefinition def = AstFactory.newAExplicitOperationDefinition(d.getOperationName(), type, new Vector<PPattern>(), null, null, d.getStatement().clone());
511:
512:                 def.setAccess(d.getAccess().clone());
513:                 def.setClassDefinition(d.getClassDefinition());
514:                 return def;
515:         }
516:
517: }