Package: DefinitionReader

DefinitionReader

nameinstructionbranchcomplexitylinemethod
DefinitionReader(LexTokenReader)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
accessSpecifier()
M: 1 C: 30
97%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 0 C: 3
100%
M: 0 C: 1
100%
newSection()
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
newSection(LexToken)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
readAccessSpecifier(boolean, boolean)
M: 64 C: 123
66%
M: 15 C: 20
57%
M: 12 C: 9
43%
M: 19 C: 41
68%
M: 0 C: 1
100%
readCoreTraceDefinition()
M: 19 C: 101
84%
M: 5 C: 9
64%
M: 4 C: 5
56%
M: 4 C: 23
85%
M: 0 C: 1
100%
readDefinitions()
M: 56 C: 124
69%
M: 9 C: 24
73%
M: 9 C: 13
59%
M: 18 C: 36
67%
M: 0 C: 1
100%
readEqualsDefinition()
M: 53 C: 122
70%
M: 7 C: 2
22%
M: 5 C: 1
17%
M: 13 C: 32
71%
M: 0 C: 1
100%
readExplicitFunctionDefinition(LexIdentifierToken, NameScope, List)
M: 46 C: 131
74%
M: 2 C: 16
89%
M: 2 C: 8
80%
M: 8 C: 31
79%
M: 0 C: 1
100%
readExplicitOperationDefinition(LexIdentifierToken)
M: 18 C: 90
83%
M: 2 C: 8
80%
M: 2 C: 4
67%
M: 2 C: 22
92%
M: 0 C: 1
100%
readExternal()
M: 4 C: 54
93%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 1 C: 12
92%
M: 0 C: 1
100%
readFunctionBody()
M: 17 C: 49
74%
M: 3 C: 4
57%
M: 2 C: 3
60%
M: 4 C: 12
75%
M: 0 C: 1
100%
readFunctionDefinition(NameScope)
M: 4 C: 45
92%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 10
91%
M: 0 C: 1
100%
readFunctions()
M: 0 C: 80
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 22
100%
M: 0 C: 1
100%
readImplicitFunctionDefinition(LexIdentifierToken, NameScope, List)
M: 28 C: 210
88%
M: 2 C: 20
91%
M: 2 C: 10
83%
M: 6 C: 48
89%
M: 0 C: 1
100%
readImplicitOperationDefinition(LexIdentifierToken)
M: 4 C: 164
98%
M: 1 C: 15
94%
M: 1 C: 8
89%
M: 1 C: 34
97%
M: 0 C: 1
100%
readInstanceVariableDefinition()
M: 0 C: 58
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
readInstanceVariables()
M: 7 C: 57
89%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 16
89%
M: 0 C: 1
100%
readLetBeStBinding()
M: 0 C: 41
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
readLetDefBinding()
M: 8 C: 50
86%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 2 C: 12
86%
M: 0 C: 1
100%
readLocalDefinition(NameScope)
M: 0 C: 54
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 17
100%
M: 0 C: 1
100%
readNamedTraceDefinition()
M: 0 C: 20
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
readOperationBody()
M: 17 C: 49
74%
M: 3 C: 4
57%
M: 2 C: 3
60%
M: 4 C: 12
75%
M: 0 C: 1
100%
readOperationDefinition()
M: 14 C: 38
73%
M: 3 C: 3
50%
M: 2 C: 2
50%
M: 3 C: 9
75%
M: 0 C: 1
100%
readOperations()
M: 5 C: 93
95%
M: 1 C: 11
92%
M: 1 C: 6
86%
M: 1 C: 22
96%
M: 0 C: 1
100%
readPermissionPredicateDefinition()
M: 6 C: 90
94%
M: 1 C: 6
86%
M: 1 C: 4
80%
M: 2 C: 21
91%
M: 0 C: 1
100%
readSpecification(ILexLocation, boolean)
M: 8 C: 129
94%
M: 2 C: 18
90%
M: 2 C: 9
82%
M: 2 C: 34
94%
M: 0 C: 1
100%
readStateDefinition()
M: 7 C: 127
95%
M: 2 C: 8
80%
M: 2 C: 4
67%
M: 1 C: 32
97%
M: 0 C: 1
100%
readSyncs()
M: 7 C: 52
88%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 15
88%
M: 0 C: 1
100%
readThreadDefinition()
M: 47 C: 57
55%
M: 4 C: 4
50%
M: 3 C: 2
40%
M: 11 C: 14
56%
M: 0 C: 1
100%
readTraceBinding()
M: 17 C: 40
70%
M: 2 C: 0
0%
M: 1 C: 1
50%
M: 4 C: 14
78%
M: 0 C: 1
100%
readTraceDefinition()
M: 0 C: 11
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
readTraceDefinitionList()
M: 0 C: 36
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
readTraceDefinitionTerm()
M: 0 C: 26
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
readTraceIdentifierList()
M: 11 C: 18
62%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 4
67%
M: 0 C: 1
100%
readTraceRepeat()
M: 39 C: 67
63%
M: 6 C: 6
50%
M: 6 C: 3
33%
M: 16 C: 18
53%
M: 0 C: 1
100%
readTraces()
M: 14 C: 53
79%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 3 C: 15
83%
M: 0 C: 1
100%
readTypeDefinition()
M: 53 C: 200
79%
M: 15 C: 22
59%
M: 12 C: 9
43%
M: 10 C: 55
85%
M: 0 C: 1
100%
readTypeParams()
M: 0 C: 56
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 13
100%
M: 0 C: 1
100%
readTypes()
M: 0 C: 72
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 20
100%
M: 0 C: 1
100%
readValueDefinition(NameScope)
M: 0 C: 31
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
readValues()
M: 7 C: 86
92%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 2 C: 22
92%
M: 0 C: 1
100%
static {...}
M: 0 C: 58
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
verifyName(String)
M: 14 C: 13
48%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 3 C: 4
57%
M: 0 C: 1
100%

Coverage

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.parser.syntax;
25:
26: import java.util.Arrays;
27: import java.util.List;
28: import java.util.Vector;
29:
30: import org.overture.ast.annotations.PAnnotation;
31: import org.overture.ast.definitions.AAssignmentDefinition;
32: import org.overture.ast.definitions.AEqualsDefinition;
33: import org.overture.ast.definitions.AImplicitOperationDefinition;
34: import org.overture.ast.definitions.AInstanceVariableDefinition;
35: import org.overture.ast.definitions.APrivateAccess;
36: import org.overture.ast.definitions.AProtectedAccess;
37: import org.overture.ast.definitions.APublicAccess;
38: import org.overture.ast.definitions.AStateDefinition;
39: import org.overture.ast.definitions.ATypeDefinition;
40: import org.overture.ast.definitions.AValueDefinition;
41: import org.overture.ast.definitions.PAccess;
42: import org.overture.ast.definitions.PDefinition;
43: import org.overture.ast.definitions.relations.AEqRelation;
44: import org.overture.ast.definitions.relations.AOrdRelation;
45: import org.overture.ast.definitions.traces.ATraceDefinitionTerm;
46: import org.overture.ast.definitions.traces.PTraceCoreDefinition;
47: import org.overture.ast.definitions.traces.PTraceDefinition;
48: import org.overture.ast.expressions.AEqualsBinaryExp;
49: import org.overture.ast.expressions.PExp;
50: import org.overture.ast.factory.AstFactory;
51: import org.overture.ast.intf.lex.ILexCommentList;
52: import org.overture.ast.intf.lex.ILexLocation;
53: import org.overture.ast.intf.lex.ILexNameToken;
54: import org.overture.ast.intf.lex.ILexToken;
55: import org.overture.ast.lex.Dialect;
56: import org.overture.ast.lex.LexIdentifierToken;
57: import org.overture.ast.lex.LexIntegerToken;
58: import org.overture.ast.lex.LexLocation;
59: import org.overture.ast.lex.LexNameList;
60: import org.overture.ast.lex.LexNameToken;
61: import org.overture.ast.lex.LexToken;
62: import org.overture.ast.lex.VDMToken;
63: import org.overture.ast.node.tokens.TStatic;
64: import org.overture.ast.patterns.APatternListTypePair;
65: import org.overture.ast.patterns.APatternTypePair;
66: import org.overture.ast.patterns.ASeqBind;
67: import org.overture.ast.patterns.ASetBind;
68: import org.overture.ast.patterns.ATypeBind;
69: import org.overture.ast.patterns.PMultipleBind;
70: import org.overture.ast.patterns.PPattern;
71: import org.overture.ast.statements.ACallObjectStm;
72: import org.overture.ast.statements.ACallStm;
73: import org.overture.ast.statements.AErrorCase;
74: import org.overture.ast.statements.AExternalClause;
75: import org.overture.ast.statements.ASpecificationStm;
76: import org.overture.ast.statements.PStm;
77: import org.overture.ast.typechecker.NameScope;
78: import org.overture.ast.types.AAccessSpecifierAccessSpecifier;
79: import org.overture.ast.types.AFieldField;
80: import org.overture.ast.types.AFunctionType;
81: import org.overture.ast.types.ANamedInvariantType;
82: import org.overture.ast.types.AOperationType;
83: import org.overture.ast.types.AUnresolvedType;
84: import org.overture.ast.types.PType;
85: import org.overture.ast.types.SInvariantType;
86: import org.overture.config.Release;
87: import org.overture.config.Settings;
88: import org.overture.parser.config.Properties;
89: import org.overture.parser.lex.LexException;
90: import org.overture.parser.lex.LexTokenReader;
91: import org.overture.parser.messages.LocatedException;
92:
93: /**
94: * A syntax analyser to parse definitions.
95: */
96:
97: public class DefinitionReader extends SyntaxReader
98: {
99:
100:         public DefinitionReader(LexTokenReader reader)
101:         {
102:                 super(reader);
103:         }
104:
105:         private static VDMToken[] sectionArray = { VDMToken.TYPES,
106:                         VDMToken.FUNCTIONS, VDMToken.STATE, VDMToken.VALUES,
107:                         VDMToken.OPERATIONS, VDMToken.INSTANCE, VDMToken.THREAD,
108:                         VDMToken.SYNC, VDMToken.TRACES, VDMToken.END, VDMToken.EOF };
109:
110:         private static VDMToken[] afterArray = { VDMToken.SEMICOLON };
111:
112:         private static List<VDMToken> sectionList = Arrays.asList(sectionArray);
113:
114:         private boolean newSection() throws LexException
115:         {
116:                 return newSection(lastToken());
117:         }
118:
119:         public static boolean newSection(LexToken tok)
120:         {
121:                 return sectionList.contains(tok.type);
122:         }
123:         
124:         
125:         private boolean accessSpecifier() throws LexException
126:         {
127:                 LexToken tok = lastToken();
128:                 
129:•                return tok.is(VDMToken.PUBLIC) || tok.is(VDMToken.PRIVATE) || tok.is(VDMToken.PROTECTED) ||
130:•                         tok.is(VDMToken.PURE) || tok.is(VDMToken.STATIC)|| tok.is(VDMToken.ASYNC);
131:         }
132:
133:         public List<PDefinition> readDefinitions() throws ParserException,
134:                         LexException
135:         {
136:                 List<PDefinition> list = new Vector<PDefinition>();
137:                 boolean threadDone = false;
138:
139:•                while (lastToken().isNot(VDMToken.EOF)
140:•                                && lastToken().isNot(VDMToken.END))
141:                 {
142:•                        switch (lastToken().type)
143:                         {
144:                                 case TYPES:
145:                                         list.addAll(readTypes());
146:                                         break;
147:
148:                                 case FUNCTIONS:
149:                                         list.addAll(readFunctions());
150:                                         break;
151:
152:                                 case STATE:
153:•                                        if (dialect != Dialect.VDM_SL)
154:                                         {
155:                                                 throwMessage(2277, "Can't have state in VDM++");
156:                                         }
157:
158:                                         try
159:                                         {
160:                                                 nextToken();
161:                                                 list.add(readStateDefinition());
162:
163:•                                                if (!newSection())
164:                                                 {
165:                                                         checkFor(VDMToken.SEMICOLON, 2080, "Missing ';' after state definition");
166:                                                 }
167:                                         } catch (LocatedException e)
168:                                         {
169:                                                 report(e, afterArray, sectionArray);
170:                                         }
171:                                         break;
172:
173:                                 case VALUES:
174:                                         list.addAll(readValues());
175:                                         break;
176:
177:                                 case OPERATIONS:
178:                                         list.addAll(readOperations());
179:                                         break;
180:
181:                                 case INSTANCE:
182:•                                        if (dialect == Dialect.VDM_SL)
183:                                         {
184:                                                 throwMessage(2009, "Can't have instance variables in VDM-SL");
185:                                         }
186:
187:                                         list.addAll(readInstanceVariables());
188:                                         break;
189:
190:                                 case TRACES:
191:•                                        if (dialect == Dialect.VDM_SL
192:                                                         && Settings.release != Release.VDM_10)
193:                                         {
194:                                                 throwMessage(2262, "Can't have traces in VDM-SL classic");
195:                                         }
196:
197:                                         list.addAll(readTraces());
198:                                         break;
199:
200:                                 case THREAD:
201:•                                        if (dialect == Dialect.VDM_SL)
202:                                         {
203:                                                 throwMessage(2010, "Can't have a thread clause in VDM-SL");
204:                                         }
205:
206:•                                        if (!threadDone)
207:                                         {
208:                                                 threadDone = true;
209:                                         } else
210:                                         {
211:                                                 throwMessage(2011, "Only one thread clause permitted per class");
212:                                         }
213:
214:                                         try
215:                                         {
216:                                                 nextToken();
217:                                                 list.add(readThreadDefinition());
218:
219:•                                                if (!newSection())
220:                                                 {
221:                                                         checkFor(VDMToken.SEMICOLON, 2085, "Missing ';' after thread definition");
222:                                                 }
223:                                         } catch (LocatedException e)
224:                                         {
225:                                                 report(e, afterArray, sectionArray);
226:                                         }
227:                                         break;
228:
229:                                 case SYNC:
230:•                                        if (dialect == Dialect.VDM_SL)
231:                                         {
232:                                                 throwMessage(2012, "Can't have a sync clause in VDM-SL");
233:                                         }
234:
235:                                         list.addAll(readSyncs());
236:                                         break;
237:
238:                                 case EOF:
239:                                         break;
240:
241:                                 default:
242:                                         try
243:                                         {
244:                                                 throwMessage(2013, "Expected 'operations', 'state', 'functions', 'types' or 'values'");
245:                                         } catch (LocatedException e)
246:                                         {
247:                                                 report(e, afterArray, sectionArray);
248:                                         }
249:                         }
250:                 }
251:
252:                 return list;
253:         }
254:
255:         private AAccessSpecifierAccessSpecifier readAccessSpecifier(boolean asyncOK, boolean pureOK)
256:                         throws LexException, ParserException
257:         {
258:•                if (dialect == Dialect.VDM_SL)
259:                 {
260:•                        if (lastToken().is(VDMToken.PURE))
261:                         {
262:•                                if (Settings.release == Release.CLASSIC)
263:                                 {
264:                                         throwMessage(2325, "Pure operations are not available in classic");
265:                                 }
266:                                 
267:•                                if (pureOK)
268:                                 {
269:                                         nextToken();
270:                                         return AstFactory.newAAccessSpecifierAccessSpecifier(new APrivateAccess(), false, false, true);
271:                                 }
272:                                 else
273:                                 {
274:                                         throwMessage(2324, "Pure only permitted for operations");
275:                                 }
276:                         }
277:                         else
278:                         {
279:                                 return AstFactory.getDefaultAccessSpecifier();
280:                         }
281:                 }
282:
283:                 // Defaults
284:                 // boolean isStatic = false;
285:                 // boolean isAsync = false;
286:                 boolean isStatic = false;
287:                 boolean isAsync = false;
288:                 boolean isPure = false;
289:                 // VDMToken access = VDMToken.PRIVATE;
290:                 PAccess access = new APrivateAccess();
291:
292:                 // Keyword counts
293:                 int numStatic = 0;
294:                 int numAsync = 0;
295:                 int numPure = 0;
296:                 int numAccess = 0;
297:
298:                 boolean more = true;
299:
300:•                while (more)
301:                 {
302:•                        switch (lastToken().type)
303:                         {
304:                                 case ASYNC:
305:•                                        if (asyncOK)
306:                                         {
307:•                                                if (++numAsync > 1)
308:                                                 {
309:                                                         throwMessage(2329, "Duplicate async keyword");
310:                                                 }
311:                                                 
312:                                                 isAsync = true;
313:                                                 nextToken();
314:                                         }
315:                                         else
316:                                         {
317:                                                 throwMessage(2278, "Async only permitted for operations");
318:                                                 more = false;
319:                                         }
320:                                         break;
321:
322:                                 case STATIC:
323:•                                        if (++numStatic > 1)
324:                                         {
325:                                                 throwMessage(2329, "Duplicate static keyword");
326:                                         }
327:                                         
328:                                         isStatic = true;
329:                                         nextToken();
330:                                         break;
331:
332:                                 case PUBLIC:
333:•                                        if (++numAccess > 1)
334:                                         {
335:                                                 throwMessage(2329, "Duplicate access specifier keyword");
336:                                         }
337:
338:                                         access = new APublicAccess();
339:                                         nextToken();
340:                                         break;
341:                                         
342:                                 case PRIVATE:
343:•                                        if (++numAccess > 1)
344:                                         {
345:                                                 throwMessage(2329, "Duplicate access specifier keyword");
346:                                         }
347:
348:                                         access = new APrivateAccess();
349:                                         nextToken();
350:                                         break;
351:                                         
352:                                 case PROTECTED:
353:•                                        if (++numAccess > 1)
354:                                         {
355:                                                 throwMessage(2329, "Duplicate access specifier keyword");
356:                                         }
357:
358:                                         access = new AProtectedAccess();
359:                                         nextToken();
360:                                         break;
361:                                         
362:                                 case PURE:
363:•                                        if (Settings.release == Release.CLASSIC)
364:                                         {
365:                                                 throwMessage(2325, "Pure operations are not available in classic");
366:                                         }
367:
368:•                                        if (pureOK)
369:                                         {
370:•                                                if (++numPure > 1)
371:                                                 {
372:                                                         throwMessage(2329, "Duplicate pure keyword");
373:                                                 }
374:                                                 
375:                                                 isPure = true;
376:                                                 nextToken();
377:                                         }
378:                                         else
379:                                         {
380:                                                 throwMessage(2324, "Pure only permitted for operations");
381:                                         }
382:                                         break;
383:
384:                                 default:
385:                                         more = false;
386:                                         break;
387:                         }
388:                 }
389:
390:                 return AstFactory.newAAccessSpecifierAccessSpecifier(access, isStatic, isAsync, isPure);
391:         }
392:
393:         public ATypeDefinition readTypeDefinition() throws ParserException,
394:                         LexException
395:         {
396:                 LexIdentifierToken id = readIdToken("Expecting new type identifier");
397:                 TypeReader tr = getTypeReader();
398:                 SInvariantType invtype = null;
399:
400:•                switch (lastToken().type)
401:                 {
402:                         case EQUALS:
403:                                 nextToken();
404:                                 PType type = tr.readType();
405:                                 ANamedInvariantType nt = AstFactory.newANamedInvariantType(idToName(id), type);
406:
407:•                                if (type instanceof AUnresolvedType
408:•                                                && ((AUnresolvedType) type).getName().equals(idToName(id)))
409:                                 {
410:                                         throwMessage(2014, "Recursive type declaration");
411:                                 }
412:
413:                                 invtype = nt;
414:                                 break;
415:
416:                         case COLONCOLON:
417:                                 nextToken();
418:                                 invtype = AstFactory.newARecordInvariantType(idToName(id), tr.readFieldList());
419:                                 break;
420:
421:                         default:
422:                                 throwMessage(2015, "Expecting =<type> or ::<field list>");
423:                 }
424:
425:                 PPattern invPattern = null;
426:                 PExp invExpression = null;
427:                 
428:                 PPattern eqPattern1 = null;
429:                 PPattern eqPattern2 = null;
430:                 PExp eqExpression = null;
431:                 AEqRelation eqRel = null;
432:                 
433:                 PPattern ordPattern1 = null;
434:                 PPattern ordPattern2 = null;
435:                 PExp ordExpression = null;
436:                 AOrdRelation ordRel = null;
437:
438:•                while (lastToken().is(VDMToken.INV) || lastToken().is(VDMToken.EQ) || lastToken().is(VDMToken.ORD))
439:                 {
440:•                 switch (lastToken().type)
441:                 {
442:                         case INV:
443:•                                 if (invPattern != null)
444:                                 {
445:                                         throwMessage(2332, "Duplicate inv clause");
446:                                 }
447:                                 
448:•                                 if (Settings.strict && (eqPattern1 != null || ordPattern1 != null))
449:                                 {
450:                                         warning(5026, "Strict: Order should be inv, eq, ord", lastToken().location);
451:                                 }
452:
453:                                 nextToken();
454:                         invPattern = getPatternReader().readPattern();
455:                         checkFor(VDMToken.EQUALSEQUALS, 2087, "Expecting '==' after pattern in invariant");
456:                         invExpression = getExpressionReader().readExpression();
457:                         break;
458:                         
459:                         case EQ:
460:•                                 if (Settings.release == Release.CLASSIC)
461:                                 {
462:                                         throwMessage(2333, "Type eq/ord clauses not available in classic");
463:                                 }
464:
465:•                                 if (eqPattern1 != null)
466:                                 {
467:                                         throwMessage(2332, "Duplicate eq clause");
468:                                 }
469:
470:•                                 if (Settings.strict && ordPattern1 != null)
471:                                 {
472:                                         warning(5026, "Strict: order should be inv, eq, ord", lastToken().location);
473:                                 }
474:                                 
475:                         nextToken();
476:                         eqPattern1 = getPatternReader().readPattern();
477:                         checkFor(VDMToken.EQUALS, 2087, "Expecting '=' between patterns in eq clause");
478:                         eqPattern2 = getPatternReader().readPattern();
479:                         checkFor(VDMToken.EQUALSEQUALS, 2087, "Expecting '==' after patterns in eq clause");
480:                         eqExpression = getExpressionReader().readExpression();
481:                         eqRel = AstFactory.newAEqRelation(eqPattern1, eqPattern2, eqExpression);
482:                                 break;
483:                                 
484:                         case ORD:
485:•                                 if (Settings.release == Release.CLASSIC)
486:                                 {
487:                                         throwMessage(2333, "Type eq/ord clauses not available in classic");
488:                                 }
489:
490:•                                 if (ordPattern1 != null)
491:                                 {
492:                                         throwMessage(2332, "Duplicate ord clause");
493:                                 }
494:                                 
495:                         nextToken();
496:                         ordPattern1 = getPatternReader().readPattern();
497:                         checkFor(VDMToken.LT, 2087, "Expecting '<' between patterns in ord clause");
498:                         ordPattern2 = getPatternReader().readPattern();
499:                         checkFor(VDMToken.EQUALSEQUALS, 2087, "Expecting '==' after patterns in ord clause");
500:                         ordExpression = getExpressionReader().readExpression();
501:                         ordRel = AstFactory.newAOrdRelation(ordPattern1, ordPattern2, ordExpression);
502:                                 break;
503:
504:                         default:
505:                                 throwMessage(2331, "Expecting inv, eq or ord clause");
506:                 }
507:                 }
508:                 
509:                 return AstFactory.newATypeDefinition(idToName(id), invtype, invPattern, invExpression, eqRel, ordRel);
510:         }
511:
512:         private List<PDefinition> readTypes() throws LexException, ParserException
513:         {
514:                 checkFor(VDMToken.TYPES, 2013, "Expected 'types'");
515:                 List<PDefinition> list = new Vector<PDefinition>();
516:
517:•                while (!newSection())
518:                 {
519:                         try
520:                         {
521:                                 ILexCommentList comments = getComments();
522:                                 List<PAnnotation> annotations = readAnnotations(comments);
523:                                 beforeAnnotations(this, annotations);
524:                                 AAccessSpecifierAccessSpecifier access = readAccessSpecifier(false, false);
525:                                 access.setStatic(new TStatic());
526:                                 ATypeDefinition def = readTypeDefinition();
527:                                 afterAnnotations(this, annotations, def);
528:                                 def.setAnnotations(annotations);
529:                                 def.setComments(comments);
530:
531:                                 // Force all type defs (invs) to be static
532:                                 def.setAccess(access);
533:                                 list.add(def);
534:
535:•                                if (!newSection())
536:                                 {
537:                                         checkFor(VDMToken.SEMICOLON, 2078, "Missing ';' after type definition");
538:                                 }
539:                         } catch (LocatedException e)
540:                         {
541:                                 report(e, afterArray, sectionArray);
542:                         }
543:                 }
544:
545:                 return list;
546:         }
547:
548:         private List<PDefinition> readValues() throws LexException, ParserException
549:         {
550:                 checkFor(VDMToken.VALUES, 2013, "Expected 'values'");
551:                 List<PDefinition> list = new Vector<PDefinition>();
552:
553:•                while (!newSection())
554:                 {
555:                         try
556:                         {
557:                                 ILexCommentList comments = getComments();
558:                                 List<PAnnotation> annotations = readAnnotations(comments);
559:                                 beforeAnnotations(this, annotations);
560:                                 AAccessSpecifierAccessSpecifier access = readAccessSpecifier(false, false);
561:                                 access.setStatic(new TStatic());
562:                                 PDefinition def = readValueDefinition(NameScope.GLOBAL);
563:                                 afterAnnotations(this, annotations, def);
564:                                 def.setAnnotations(annotations);
565:                                 def.setComments(comments);
566:
567:                                 // Force all values to be static
568:                                 def.setAccess(access);
569:
570:•                                if (def instanceof AValueDefinition)
571:                                 {
572:•                                        for (PDefinition pDefinition : ((AValueDefinition) def).getDefs())
573:                                         {
574:                                                 pDefinition.setAccess(access.clone());
575:                                         }
576:                                 }
577:
578:                                 list.add(def);
579:
580:•                                if (!newSection())
581:                                 {
582:                                         checkFor(VDMToken.SEMICOLON, 2081, "Missing ';' after value definition");
583:                                 }
584:                         } catch (LocatedException e)
585:                         {
586:                                 report(e, afterArray, sectionArray);
587:                         }
588:                 }
589:
590:                 return list;
591:         }
592:
593:         private List<PDefinition> readFunctions() throws LexException,
594:                         ParserException
595:         {
596:                 checkFor(VDMToken.FUNCTIONS, 2013, "Expected 'functions'");
597:                 List<PDefinition> list = new Vector<PDefinition>();
598:
599:•                while (!newSection())
600:                 {
601:                         try
602:                         {
603:                                 ILexCommentList comments = getComments();
604:                                 List<PAnnotation> annotations = readAnnotations(comments);
605:                                 beforeAnnotations(this, annotations);
606:                                 AAccessSpecifierAccessSpecifier access = readAccessSpecifier(false, false);
607:                                 PDefinition def = readFunctionDefinition(NameScope.GLOBAL);
608:                                 afterAnnotations(this, annotations, def);
609:                                 def.setAnnotations(annotations);
610:                                 def.setComments(comments);
611:
612:•                                if (Settings.release == Release.VDM_10)
613:                                 {
614:                                         // Force all functions to be static for VDM-10
615:                                         access.setStatic(new TStatic());
616:                                         def.setAccess(access);
617:                                 } else
618:                                 {
619:                                         def.setAccess(access);
620:                                 }
621:
622:                                 list.add(def);
623:
624:•                                if (!newSection())
625:                                 {
626:                                         checkFor(VDMToken.SEMICOLON, 2079, "Missing ';' after function definition");
627:                                 }
628:                         } catch (LocatedException e)
629:                         {
630:                                 report(e, afterArray, sectionArray);
631:                         }
632:                 }
633:
634:                 return list;
635:         }
636:
637:         public List<PDefinition> readOperations() throws LexException,
638:                         ParserException
639:         {
640:                 checkFor(VDMToken.OPERATIONS, 2013, "Expected 'operations'");
641:                 List<PDefinition> list = new Vector<PDefinition>();
642:
643:•                while (!newSection())
644:                 {
645:                         try
646:                         {
647:                                 ILexCommentList comments = getComments();
648:                                 List<PAnnotation> annotations = readAnnotations(comments);
649:                                 beforeAnnotations(this, annotations);
650:•                                AAccessSpecifierAccessSpecifier access = readAccessSpecifier(dialect == Dialect.VDM_RT, true);
651:                                 PDefinition def = readOperationDefinition();
652:                                 afterAnnotations(this, annotations, def);
653:                                 def.setAnnotations(annotations);
654:                                 def.setComments(comments);
655:                                 def.setAccess(access);
656:                                 ((AOperationType)def.getType()).setPure(access.getPure());
657:                                 list.add(def);
658:
659:•                                if (!newSection())
660:                                 {
661:                                         LexToken end = lastToken();
662:                                         checkFor(VDMToken.SEMICOLON, 2082, "Missing ';' after operation definition");
663:                                         
664:•                                        if (lastToken().isNot(VDMToken.IDENTIFIER) && !newSection() && !accessSpecifier())
665:                                         {
666:                                                 throwMessage(2082, "Semi-colon is not allowed here", end);
667:                                         }
668:                                 }
669:                         } catch (LocatedException e)
670:                         {
671:                                 report(e, afterArray, sectionArray);
672:                         }
673:                 }
674:
675:                 return list;
676:         }
677:
678:         public List<PDefinition> readInstanceVariables() throws LexException,
679:                         ParserException
680:         {
681:                 checkFor(VDMToken.INSTANCE, 2083, "Expected 'instance variables'");
682:                 checkFor(VDMToken.VARIABLES, 2083, "Expecting 'instance variables'");
683:                 List<PDefinition> list = new Vector<PDefinition>();
684:
685:•                while (!newSection())
686:                 {
687:                         try
688:                         {
689:                                 ILexCommentList comments = getComments();
690:                                 List<PAnnotation> annotations = readAnnotations(comments);
691:                                 beforeAnnotations(this, annotations);
692:                                 PDefinition def = readInstanceVariableDefinition();
693:                                 afterAnnotations(this, annotations, def);
694:                                 def.setAnnotations(annotations);
695:                                 def.setComments(comments);
696:                                 list.add(def);
697:
698:•                                if (!newSection())
699:                                 {
700:                                         checkFor(VDMToken.SEMICOLON, 2084, "Missing ';' after instance variable definition");
701:                                 }
702:                         } catch (LocatedException e)
703:                         {
704:                                 report(e, afterArray, sectionArray);
705:                         }
706:                 }
707:
708:                 return list;
709:         }
710:
711:         private List<PDefinition> readTraces() throws LexException, ParserException
712:         {
713:                 checkFor(VDMToken.TRACES, 2013, "Expected 'traces'");
714:                 List<PDefinition> list = new Vector<PDefinition>();
715:
716:•                while (!newSection())
717:                 {
718:                         try
719:                         {
720:                                 ILexCommentList comments = getComments();
721:                                 List<PAnnotation> annotations = readAnnotations(comments);
722:                                 beforeAnnotations(this, annotations);
723:                                 PDefinition def = readNamedTraceDefinition();
724:                                 afterAnnotations(this, annotations, def);
725:                                 def.setAnnotations(annotations);
726:                                 def.setComments(comments);
727:                                 list.add(def);
728:
729:•                                if (!newSection())
730:                                 {
731:•                                        if (ignore(VDMToken.SEMICOLON) && Settings.strict)
732:                                         {
733:                                                 warning(5028, "Strict: expecting semi-colon between traces", lastToken().location);
734:                                         }
735:                                 }
736:                         } catch (LocatedException e)
737:                         {
738:                                 report(e, afterArray, sectionArray);
739:                         }
740:                 }
741:
742:                 return list;
743:         }
744:
745:         private List<PDefinition> readSyncs() throws LexException, ParserException
746:         {
747:                 checkFor(VDMToken.SYNC, 2013, "Expected 'sync'");
748:                 List<PDefinition> list = new Vector<PDefinition>();
749:
750:•                while (!newSection())
751:                 {
752:                         try
753:                         {
754:                                 ILexCommentList comments = getComments();
755:                                 List<PAnnotation> annotations = readAnnotations(comments);
756:                                 beforeAnnotations(this, annotations);
757:                                 PDefinition def = readPermissionPredicateDefinition();
758:                                 afterAnnotations(this, annotations, def);
759:                                 def.setAnnotations(annotations);
760:                                 def.setComments(comments);
761:                                 list.add(def);
762:
763:•                                if (!newSection())
764:                                 {
765:                                         checkFor(VDMToken.SEMICOLON, 2086, "Missing ';' after sync definition");
766:                                 }
767:                         } catch (LocatedException e)
768:                         {
769:                                 report(e, afterArray, sectionArray);
770:                         }
771:                 }
772:
773:                 return list;
774:         }
775:
776:         public LexNameList readTypeParams() throws LexException, ParserException
777:         {
778:                 LexNameList typeParams = null;
779:
780:•                if (lastToken().is(VDMToken.SEQ_OPEN))
781:                 {
782:                         typeParams = new LexNameList();
783:                         nextToken();
784:                         checkFor(VDMToken.AT, 2088, "Expecting '@' before type parameter");
785:                         LexIdentifierToken tid = readIdToken("Expecting '@identifier' in type parameter list");
786:                         typeParams.add(idToName(tid));
787:
788:•                        while (ignore(VDMToken.COMMA))
789:                         {
790:                                 checkFor(VDMToken.AT, 2089, "Expecting '@' before type parameter");
791:                                 tid = readIdToken("Expecting '@identifier' in type parameter list");
792:                                 typeParams.add(idToName(tid));
793:                         }
794:
795:                         checkFor(VDMToken.SEQ_CLOSE, 2090, "Expecting ']' after type parameters");
796:                 }
797:
798:                 return typeParams;
799:         }
800:         
801:         private void verifyName(String name) throws ParserException, LexException
802:         {
803:•                if (name.startsWith("mk_"))
804:                 {
805:                         throwMessage(2016, "Name cannot start with 'mk_'");
806:                 }
807:•                else if (name.equals("mu"))
808:                 {
809:                         throwMessage(2016, "Name cannot be 'mu' (reserved)");
810:                 }
811:•                else if (name.equals("narrow_"))
812:                 {
813:                         throwMessage(2016, "Name cannot be 'narrow_' (reserved)");
814:                 }
815:         }
816:
817:         private PDefinition readFunctionDefinition(NameScope scope)
818:                         throws ParserException, LexException
819:         {
820:                 PDefinition def = null;
821:                 LexIdentifierToken funcName = readIdToken("Expecting new function identifier");
822:                 verifyName(funcName.getName());
823:
824:                 LexNameList typeParams = readTypeParams();
825:
826:•                if (lastToken().is(VDMToken.COLON))
827:                 {
828:                         def = readExplicitFunctionDefinition(funcName, scope, typeParams);
829:•                } else if (lastToken().is(VDMToken.BRA))
830:                 {
831:                         def = readImplicitFunctionDefinition(funcName, scope, typeParams);
832:                 } else
833:                 {
834:                         throwMessage(2017, "Expecting ':' or '(' after name in function definition");
835:                 }
836:
837:                 LexLocation.addSpan(idToName(funcName), lastToken());
838:                 return def;
839:         }
840:
841:         private PDefinition readExplicitFunctionDefinition(
842:                         LexIdentifierToken funcName, NameScope scope,
843:                         List<ILexNameToken> typeParams) throws ParserException,
844:                         LexException
845:         {
846:                 // Explicit function definition, like "f: int->bool f(x) == true"
847:
848:                 nextToken();
849:                 PType t = getTypeReader().readType();
850:
851:•                if (!(t instanceof AFunctionType))
852:                 {
853:                         throwMessage(2018, "Function type is not a -> or +> function");
854:                 }
855:
856:                 AFunctionType type = (AFunctionType) t;
857:
858:                 LexIdentifierToken name = readIdToken("Expecting identifier after function type in definition");
859:
860:•                if (!name.equals(funcName))
861:                 {
862:                         throwMessage(2019, "Expecting identifier " + funcName.getName()
863:                                         + " after type in definition");
864:                 }
865:
866:•                if (lastToken().isNot(VDMToken.BRA))
867:                 {
868:                         throwMessage(2020, "Expecting '(' after function name");
869:                 }
870:
871:                 List<List<PPattern>> parameters = new Vector<List<PPattern>>();
872:
873:•                while (lastToken().is(VDMToken.BRA))
874:                 {
875:•                        if (nextToken().isNot(VDMToken.KET))
876:                         {
877:                                 parameters.add(getPatternReader().readPatternList());
878:                                 checkFor(VDMToken.KET, 2091, "Expecting ')' after function parameters");
879:                         } else
880:                         {
881:                                 parameters.add(new Vector<PPattern>()); // empty "()"
882:                                 nextToken();
883:                         }
884:                 }
885:
886:                 checkFor(VDMToken.EQUALSEQUALS, 2092, "Expecting '==' after parameters");
887:                 ExpressionReader expr = getExpressionReader();
888:                 PExp body = readFunctionBody();
889:                 PExp precondition = null;
890:                 PExp postcondition = null;
891:                 PExp measure = null;
892:
893:•                if (lastToken().is(VDMToken.PRE))
894:                 {
895:                         nextToken();
896:                         precondition = expr.readExpression();
897:                 }
898:
899:•                if (lastToken().is(VDMToken.POST))
900:                 {
901:                         nextToken();
902:                         postcondition = expr.readExpression();
903:                 }
904:
905:•                if (lastToken().is(VDMToken.MEASURE))
906:                 {
907:                         nextToken();
908:
909:•                        if (lastToken().is(VDMToken.IS))
910:                         {
911:                                 nextToken();
912:                                 checkFor(VDMToken.NOT, 2125, "Expecting 'is not yet specified'");
913:                                 checkFor(VDMToken.YET, 2125, "Expecting 'is not yet specified'");
914:                                 checkFor(VDMToken.SPECIFIED, 2126, "Expecting 'is not yet specified'");
915:                                 measure = AstFactory.newANotYetSpecifiedExp(lastToken().location);
916:                         }
917:                         else
918:                         {
919:                                 measure = expr.readExpression();
920:                         }
921:                 }
922:
923:                 return AstFactory.newAExplicitFunctionDefinition(idToName(funcName), scope, typeParams, type, parameters, body, precondition, postcondition, false, measure);
924:         }
925:
926:         private PDefinition readImplicitFunctionDefinition(
927:                         LexIdentifierToken funcName, NameScope scope,
928:                         List<ILexNameToken> typeParams) throws ParserException,
929:                         LexException
930:         {
931:                 // Implicit, like g(x: int) y: bool pre exp post exp
932:
933:                 nextToken();
934:
935:                 PatternReader pr = getPatternReader();
936:                 TypeReader tr = getTypeReader();
937:                 List<APatternListTypePair> parameterPatterns = new Vector<APatternListTypePair>();
938:
939:•                if (lastToken().isNot(VDMToken.KET))
940:                 {
941:                         List<PPattern> pl = pr.readPatternList();
942:                         checkFor(VDMToken.COLON, 2093, "Missing colon after pattern/type parameter");
943:                         parameterPatterns.add(AstFactory.newAPatternListTypePair(pl, tr.readType()));
944:
945:•                        while (ignore(VDMToken.COMMA))
946:                         {
947:                                 pl = pr.readPatternList();
948:                                 checkFor(VDMToken.COLON, 2093, "Missing colon after pattern/type parameter");
949:                                 parameterPatterns.add(AstFactory.newAPatternListTypePair(pl, tr.readType()));
950:                         }
951:                 }
952:
953:                 checkFor(VDMToken.KET, 2124, "Expecting ')' after parameters");
954:
955:                 LexToken firstResult = lastToken();
956:                 List<PPattern> resultNames = new Vector<PPattern>();
957:                 List<PType> resultTypes = new Vector<PType>();
958:
959:                 do
960:                 {
961:                         LexIdentifierToken rname = readIdToken("Expecting result identifier");
962:                         resultNames.add(AstFactory.newAIdentifierPattern(idToName(rname)));
963:                         checkFor(VDMToken.COLON, 2094, "Missing colon in identifier/type return value");
964:                         resultTypes.add(tr.readType());
965:•                } while (ignore(VDMToken.COMMA));
966:
967:•                if (lastToken().is(VDMToken.IDENTIFIER))
968:                 {
969:                         throwMessage(2261, "Missing comma between return types?");
970:                 }
971:
972:                 APatternTypePair resultPattern = null;
973:
974:•                if (resultNames.size() > 1)
975:                 {
976:                         resultPattern = AstFactory.newAPatternTypePair(AstFactory.newATuplePattern(firstResult.location, resultNames), AstFactory.newAProductType(firstResult.location, resultTypes));
977:                 } else
978:                 {
979:                         resultPattern = AstFactory.newAPatternTypePair(resultNames.get(0), resultTypes.get(0));
980:                 }
981:
982:                 ExpressionReader expr = getExpressionReader();
983:                 PExp body = null;
984:                 PExp precondition = null;
985:                 PExp postcondition = null;
986:                 PExp measure = null;
987:
988:•                if (lastToken().is(VDMToken.EQUALSEQUALS)) // extended implicit function
989:                 {
990:                         nextToken();
991:                         body = readFunctionBody();
992:                 }
993:
994:•                if (lastToken().is(VDMToken.PRE))
995:                 {
996:                         nextToken();
997:                         precondition = expr.readExpression();
998:                 }
999:
1000:•                if (body == null) // Mandatory for standard implicit functions
1001:                 {
1002:                         checkFor(VDMToken.POST, 2095, "Implicit function must have post condition");
1003:                         postcondition = expr.readExpression();
1004:                 } else
1005:                 {
1006:•                        if (lastToken().is(VDMToken.POST))
1007:                         {
1008:                                 nextToken();
1009:                                 postcondition = expr.readExpression();
1010:                         }
1011:                 }
1012:
1013:•                if (lastToken().is(VDMToken.MEASURE))
1014:                 {
1015:                         nextToken();
1016:•                        if (lastToken().is(VDMToken.IS))
1017:                         {
1018:                                 nextToken();
1019:                                 checkFor(VDMToken.NOT, 2125, "Expecting 'is not yet specified'");
1020:                                 checkFor(VDMToken.YET, 2125, "Expecting 'is not yet specified'");
1021:                                 checkFor(VDMToken.SPECIFIED, 2126, "Expecting 'is not yet specified'");
1022:                                 measure = AstFactory.newANotYetSpecifiedExp(lastToken().location);
1023:                         }
1024:                         else
1025:                         {
1026:                                 measure = expr.readExpression();
1027:                         }
1028:                 }
1029:
1030:                 return AstFactory.newAImplicitFunctionDefinition(idToName(funcName), scope, typeParams, parameterPatterns, resultPattern, body, precondition, postcondition, measure);
1031:
1032:         }
1033:
1034:         public PDefinition readLocalDefinition(NameScope scope)
1035:                         throws ParserException, LexException
1036:         {
1037:                 ParserException funcDefError = null;
1038:
1039:                 try
1040:                 {
1041:                         reader.push();
1042:                         PDefinition def = readFunctionDefinition(scope);
1043:                         reader.unpush();
1044:                         return def;
1045:                 } catch (ParserException e) // Not a function then...
1046:                 {
1047:                         e.adjustDepth(reader.getTokensRead());
1048:                         reader.pop();
1049:                         funcDefError = e;
1050:                 }
1051:
1052:                 try
1053:                 {
1054:                         reader.push();
1055:                         PDefinition def = readValueDefinition(scope);
1056:                         reader.unpush();
1057:                         return def;
1058:                 } catch (ParserException e)
1059:                 {
1060:                         e.adjustDepth(reader.getTokensRead());
1061:                         reader.pop();
1062:•                        throw e.deeperThan(funcDefError) ? e : funcDefError;
1063:                 }
1064:         }
1065:
1066:         public PDefinition readValueDefinition(NameScope scope)
1067:                         throws ParserException, LexException
1068:         {
1069:                 // Should be <pattern>[:<type>]=<expression>
1070:
1071:                 PPattern p = getPatternReader().readPattern();
1072:                 PType type = null;
1073:
1074:•                if (lastToken().is(VDMToken.COLON))
1075:                 {
1076:                         nextToken();
1077:                         type = getTypeReader().readType();
1078:                 }
1079:
1080:                 checkFor(VDMToken.EQUALS, 2096, "Expecting <pattern>[:<type>]=<exp>");
1081:
1082:                 return AstFactory.newAValueDefinition(p, scope, type, getExpressionReader().readExpression());
1083:         }
1084:
1085:         private PDefinition readStateDefinition() throws ParserException,
1086:                         LexException
1087:         {
1088:                 ILexCommentList comments = getComments();
1089:                 List<PAnnotation> annotations = readAnnotations(comments);
1090:                 beforeAnnotations(this, annotations);
1091:                 LexIdentifierToken name = readIdToken("Expecting identifier after 'state' definition");
1092:                 checkFor(VDMToken.OF, 2097, "Expecting 'of' after state name");
1093:                 List<AFieldField> fieldList = getTypeReader().readFieldList();
1094:
1095:                 PExp invExpression = null;
1096:                 PExp initExpression = null;
1097:                 PPattern invPattern = null;
1098:                 PPattern initPattern = null;
1099:
1100:•                if (lastToken().is(VDMToken.INV))
1101:                 {
1102:                         nextToken();
1103:                         invPattern = getPatternReader().readPattern();
1104:                         checkFor(VDMToken.EQUALSEQUALS, 2098, "Expecting '==' after pattern in invariant");
1105:                         invExpression = getExpressionReader().readExpression();
1106:                 }
1107:
1108:•                if (lastToken().is(VDMToken.INIT))
1109:                 {
1110:                         nextToken();
1111:                         initPattern = getPatternReader().readPattern();
1112:                         checkFor(VDMToken.EQUALSEQUALS, 2099, "Expecting '==' after pattern in initializer");
1113:                         initExpression = getExpressionReader().readExpression();
1114:                 }
1115:
1116:                 // Be forgiving about the inv/init order
1117:•                if (lastToken().is(VDMToken.INV) && invExpression == null)
1118:                 {
1119:•                        if (Settings.strict)
1120:                         {
1121:                                 warning(5027, "Strict: order should be inv, init", lastToken().location);
1122:                         }
1123:                         
1124:                         nextToken();
1125:                         invPattern = getPatternReader().readPattern();
1126:                         checkFor(VDMToken.EQUALSEQUALS, 2098, "Expecting '==' after pattern in invariant");
1127:                         invExpression = getExpressionReader().readExpression();
1128:                 }
1129:
1130:                 checkFor(VDMToken.END, 2100, "Expecting 'end' after state definition");
1131:
1132:                 AStateDefinition def = AstFactory.newAStateDefinition(idToName(name), fieldList, invPattern, invExpression, initPattern, initExpression);
1133:                 afterAnnotations(this, annotations, def);
1134:                 def.setAnnotations(annotations);
1135:                 def.setComments(comments);
1136:                 return def;
1137:         }
1138:
1139:         private PDefinition readOperationDefinition() throws ParserException,
1140:                         LexException
1141:         {
1142:                 PDefinition def = null;
1143:                 LexIdentifierToken opName = readIdToken("Expecting new operation identifier");
1144:                 verifyName(opName.getName());
1145:
1146:•                if (lastToken().is(VDMToken.COLON))
1147:                 {
1148:                         def = readExplicitOperationDefinition(opName);
1149:•                } else if (lastToken().is(VDMToken.BRA))
1150:                 {
1151:                         def = readImplicitOperationDefinition(opName);
1152:•                } else if (lastToken().is(VDMToken.SEQ_OPEN))
1153:                 {
1154:                         throwMessage(2059, "Operations cannot have [@T] type parameters");
1155:                 } else
1156:                 {
1157:                         throwMessage(2021, "Expecting ':' or '(' after name in operation definition");
1158:                 }
1159:
1160:                 LexLocation.addSpan(idToName(opName), lastToken());
1161:                 return def;
1162:         }
1163:
1164:         private PDefinition readExplicitOperationDefinition(
1165:                         LexIdentifierToken opName) throws ParserException, LexException
1166:         {
1167:                 // Like "f: int ==> bool f(x) == <statement>"
1168:
1169:                 nextToken();
1170:                 AOperationType type = getTypeReader().readOperationType();
1171:
1172:                 LexIdentifierToken name = readIdToken("Expecting operation identifier after type in definition");
1173:
1174:•                if (!name.equals(opName))
1175:                 {
1176:                         throwMessage(2022, "Expecting name " + opName.getName()
1177:                                         + " after type in definition");
1178:                 }
1179:
1180:•                if (lastToken().isNot(VDMToken.BRA))
1181:                 {
1182:                         throwMessage(2023, "Expecting '(' after operation name");
1183:                 }
1184:
1185:                 List<PPattern> parameters = null;
1186:
1187:•                if (nextToken().isNot(VDMToken.KET))
1188:                 {
1189:                         parameters = getPatternReader().readPatternList();
1190:                         checkFor(VDMToken.KET, 2101, "Expecting ')' after operation parameters");
1191:                 } else
1192:                 {
1193:                         parameters = new Vector<PPattern>(); // empty "()"
1194:                         nextToken();
1195:                 }
1196:
1197:                 checkFor(VDMToken.EQUALSEQUALS, 2102, "Expecting '==' after parameters");
1198:                 PStm body = readOperationBody();
1199:                 PExp precondition = null;
1200:                 PExp postcondition = null;
1201:
1202:•                if (lastToken().is(VDMToken.PRE))
1203:                 {
1204:                         nextToken();
1205:                         precondition = getExpressionReader().readExpression();
1206:                 }
1207:
1208:•                if (lastToken().is(VDMToken.POST))
1209:                 {
1210:                         nextToken();
1211:                         postcondition = getExpressionReader().readExpression();
1212:                 }
1213:
1214:                 return AstFactory.newAExplicitOperationDefinition(idToName(opName), type, parameters, precondition, postcondition, body);
1215:         }
1216:
1217:         private PDefinition readImplicitOperationDefinition(
1218:                         LexIdentifierToken opName) throws ParserException, LexException
1219:         {
1220:                 // Like g(x: int) [y: bool]? ext rd fred[:int] pre exp post exp
1221:
1222:                 nextToken();
1223:                 PatternReader pr = getPatternReader();
1224:                 TypeReader tr = getTypeReader();
1225:                 List<APatternListTypePair> parameterPatterns = new Vector<APatternListTypePair>();
1226:
1227:•                if (lastToken().isNot(VDMToken.KET))
1228:                 {
1229:                         List<PPattern> pl = pr.readPatternList();
1230:                         checkFor(VDMToken.COLON, 2103, "Missing colon after pattern/type parameter");
1231:                         parameterPatterns.add(AstFactory.newAPatternListTypePair(pl, tr.readType()));
1232:
1233:•                        while (ignore(VDMToken.COMMA))
1234:                         {
1235:                                 pl = pr.readPatternList();
1236:                                 checkFor(VDMToken.COLON, 2103, "Missing colon after pattern/type parameter");
1237:                                 parameterPatterns.add(AstFactory.newAPatternListTypePair(pl, tr.readType()));
1238:                         }
1239:                 }
1240:
1241:                 checkFor(VDMToken.KET, 2124, "Expecting ')' after args");
1242:
1243:                 LexToken firstResult = lastToken();
1244:                 APatternTypePair resultPattern = null;
1245:
1246:•                if (firstResult.is(VDMToken.IDENTIFIER))
1247:                 {
1248:                         List<PPattern> resultNames = new Vector<PPattern>();
1249:                         List<PType> resultTypes = new Vector<PType>();
1250:
1251:                         do
1252:                         {
1253:                                 LexIdentifierToken rname = readIdToken("Expecting result identifier");
1254:                                 resultNames.add(AstFactory.newAIdentifierPattern(idToName(rname)));
1255:                                 checkFor(VDMToken.COLON, 2104, "Missing colon in identifier/type return value");
1256:                                 resultTypes.add(tr.readType());
1257:•                        } while (ignore(VDMToken.COMMA));
1258:
1259:•                        if (lastToken().is(VDMToken.IDENTIFIER))
1260:                         {
1261:                                 throwMessage(2261, "Missing comma between return types?");
1262:                         }
1263:
1264:•                        if (resultNames.size() > 1)
1265:                         {
1266:                                 resultPattern = AstFactory.newAPatternTypePair(AstFactory.newATuplePattern(firstResult.location, resultNames), AstFactory.newAProductType(firstResult.location, resultTypes));
1267:                         } else
1268:                         {
1269:                                 resultPattern = AstFactory.newAPatternTypePair(resultNames.get(0), resultTypes.get(0));
1270:                         }
1271:                 }
1272:
1273:                 PStm body = null;
1274:
1275:•                if (lastToken().is(VDMToken.EQUALSEQUALS)) // extended implicit operation
1276:                 {
1277:                         nextToken();
1278:                         body = readOperationBody();
1279:                 }
1280:
1281:•                ASpecificationStm spec = readSpecification(opName.location, body == null);
1282:
1283:                 AImplicitOperationDefinition def = AstFactory.newAImplicitOperationDefinition(idToName(opName), parameterPatterns, resultPattern, body, spec);
1284:
1285:                 return def;
1286:         }
1287:
1288:         public ASpecificationStm readSpecification(ILexLocation location,
1289:                         boolean postMandatory) throws ParserException, LexException
1290:         {
1291:                 List<AExternalClause> externals = null;
1292:
1293:•                if (lastToken().is(VDMToken.EXTERNAL))
1294:                 {
1295:                         externals = new Vector<AExternalClause>();
1296:                         nextToken();
1297:
1298:•                        while (lastToken().is(VDMToken.READ)
1299:•                                        || lastToken().is(VDMToken.WRITE))
1300:                         {
1301:                                 externals.add(readExternal());
1302:                         }
1303:
1304:•                        if (externals.isEmpty())
1305:                         {
1306:                                 throwMessage(2024, "Expecting external declarations after 'ext'");
1307:                         }
1308:                 }
1309:
1310:                 ExpressionReader expr = getExpressionReader();
1311:                 PExp precondition = null;
1312:                 PExp postcondition = null;
1313:
1314:•                if (lastToken().is(VDMToken.PRE))
1315:                 {
1316:                         nextToken();
1317:                         precondition = expr.readExpression();
1318:                 }
1319:
1320:•                if (postMandatory) // Mandatory for standard implicit operations
1321:                 {
1322:                         checkFor(VDMToken.POST, 2105, "Implicit operation must define a post condition");
1323:                         postcondition = expr.readExpression();
1324:                 } else
1325:                 {
1326:•                        if (lastToken().is(VDMToken.POST))
1327:                         {
1328:                                 nextToken();
1329:                                 postcondition = expr.readExpression();
1330:                         }
1331:                 }
1332:
1333:                 List<AErrorCase> errors = null;
1334:
1335:•                if (lastToken().is(VDMToken.ERRS))
1336:                 {
1337:                         errors = new Vector<AErrorCase>();
1338:                         nextToken();
1339:
1340:•                        while (lastToken() instanceof LexIdentifierToken)
1341:                         {
1342:                                 LexIdentifierToken name = readIdToken("Expecting error identifier");
1343:                                 checkFor(VDMToken.COLON, 2106, "Expecting ':' after name in errs clause");
1344:                                 PExp left = expr.readExpression();
1345:                                 checkFor(VDMToken.ARROW, 2107, "Expecting '->' in errs clause");
1346:                                 PExp right = expr.readExpression();
1347:                                 errors.add(AstFactory.newAErrorCase(name, left, right));
1348:                         }
1349:
1350:•                        if (errors.isEmpty())
1351:                         {
1352:                                 throwMessage(2025, "Expecting <name>: exp->exp in errs clause");
1353:                         }
1354:                 }
1355:
1356:                 return AstFactory.newASpecificationStm(location, externals, precondition, postcondition, errors);
1357:         }
1358:
1359:         private AExternalClause readExternal() throws ParserException, LexException
1360:         {
1361:                 LexToken mode = lastToken();
1362:
1363:•                if (mode.isNot(VDMToken.READ) && mode.isNot(VDMToken.WRITE))
1364:                 {
1365:                         throwMessage(2026, "Expecting 'rd' or 'wr' after 'ext'");
1366:                 }
1367:
1368:                 LexNameList names = new LexNameList();
1369:                 nextToken();
1370:                 names.add(readNameToken("Expecting name in external clause"));
1371:
1372:•                while (ignore(VDMToken.COMMA))
1373:                 {
1374:                         names.add(readNameToken("Expecting name in external clause"));
1375:                 }
1376:
1377:                 PType type = null;
1378:
1379:•                if (lastToken().is(VDMToken.COLON))
1380:                 {
1381:                         nextToken();
1382:                         type = getTypeReader().readType();
1383:                 }
1384:
1385:                 return AstFactory.newAExternalClause(mode, names, type);
1386:
1387:         }
1388:
1389:         public AEqualsDefinition readEqualsDefinition() throws ParserException,
1390:                         LexException
1391:         {
1392:                 // The grammar here says the form of the definition should be
1393:                 // "def" <patternBind>=<expression> "in" <expression>, but since
1394:                 // a set bind is "s in set S" that naively parses as
1395:                 // "s in set (S = <expression>)". Talking to PGL, we have to
1396:                 // make a special parse here. It is one of these forms:
1397:                 //
1398:                 // "def" <pattern> "=" <expression> "in" ...
1399:                 // "def" <type bind> "=" <expression> "in" ...
1400:                 // "def" <pattern> "in set" <equals-expression> "in" ...
1401:                 // "def" <pattern> "in seq" <equals-expression> "in" ...
1402:                 //
1403:                 // and the "=" is unpicked from the left and right of the equals
1404:                 // expression in the last two cases.
1405:
1406:                 ILexLocation location = lastToken().location;
1407:                 ParserException equalsDefError = null;
1408:
1409:                 try
1410:                 // "def" <pattern> "=" <expression> "in" ...
1411:                 {
1412:                         reader.push();
1413:                         PPattern pattern = getPatternReader().readPattern();
1414:                         checkFor(VDMToken.EQUALS, 2108, "Expecting <pattern>=<exp>");
1415:                         PExp test = getExpressionReader().readExpression();
1416:                         reader.unpush();
1417:                         return AstFactory.newAEqualsDefinition(location, pattern, test);
1418:                 } catch (ParserException e)
1419:                 {
1420:                         e.adjustDepth(reader.getTokensRead());
1421:                         reader.pop();
1422:                         equalsDefError = e;
1423:                 }
1424:
1425:                 try
1426:                 // "def" <type bind> "=" <expression> "in" ...
1427:                 {
1428:                         reader.push();
1429:                         ATypeBind typebind = getBindReader().readTypeBind();
1430:                         checkFor(VDMToken.EQUALS, 2109, "Expecting <type bind>=<exp>");
1431:                         PExp test = getExpressionReader().readExpression();
1432:                         reader.unpush();
1433:                         return AstFactory.newAEqualsDefinition(location, typebind, test);
1434:                 } catch (ParserException e)
1435:                 {
1436:                         e.adjustDepth(reader.getTokensRead());
1437:                         reader.pop();
1438:•                        equalsDefError = e.deeperThan(equalsDefError) ? e : equalsDefError;
1439:                 }
1440:
1441:                 try
1442:                 {
1443:                         reader.push();
1444:                         PPattern pattern = getPatternReader().readPattern();
1445:                         checkFor(VDMToken.IN, 2110, "Expecting <pattern> in set|seq <exp>");
1446:                         AEqualsBinaryExp test = null;
1447:                         
1448:•                        switch (lastToken().type)
1449:                         {
1450:                         case SET:                // "def" <pattern> "in set" <equals-expression> "in" ...
1451:                                 nextToken();
1452:                                 test = getExpressionReader().readDefEqualsExpression();
1453:                                 ASetBind setbind = AstFactory.newASetBind(pattern, test.getLeft());
1454:                                 reader.unpush();
1455:                                 return AstFactory.newAEqualsDefinition(location, setbind, test.getRight());
1456:
1457:                         case SEQ:                // "def" <pattern> "in seq" <equals-expression> "in" ...
1458:•                                if (Settings.release == Release.CLASSIC)
1459:                                 {
1460:                                         throwMessage(2328, "Sequence binds are not available in classic");
1461:                                 }
1462:
1463:                                 nextToken();
1464:                                 test = getExpressionReader().readDefEqualsExpression();
1465:                                 ASeqBind seqbind = AstFactory.newASeqBind(pattern, test.getLeft());
1466:                                 reader.unpush();
1467:                                 return AstFactory.newAEqualsDefinition(location, seqbind, test.getRight());
1468:
1469:                         default:
1470:                                 throwMessage(2111, "Expecting <pattern> in set|seq <exp>");
1471:                                 return null;
1472:                         }
1473:                         
1474:                 }
1475:                 catch (ParserException e)
1476:                 {
1477:                         e.adjustDepth(reader.getTokensRead());
1478:                         reader.pop();
1479:•                        throw e.deeperThan(equalsDefError) ? e : equalsDefError;
1480:                 }
1481:         }
1482:
1483:         private PDefinition readInstanceVariableDefinition()
1484:                         throws ParserException, LexException
1485:         {
1486:                 LexToken token = lastToken();
1487:
1488:•                if (token.is(VDMToken.INV))
1489:                 {
1490:                         nextToken();
1491:                         PExp exp = getExpressionReader().readExpression();
1492:                         String str = getCurrentModule();
1493:                         LexNameToken className = new LexNameToken(str, str, token.location);
1494:                         return AstFactory.newAClassInvariantDefinition(className.getInvName(token.location), exp);
1495:                 } else
1496:                 {
1497:                         AAccessSpecifierAccessSpecifier access = readAccessSpecifier(false, false);
1498:                         AAssignmentDefinition def = getStatementReader().readAssignmentDefinition();
1499:                         AInstanceVariableDefinition ivd = AstFactory.newAInstanceVariableDefinition(def.getName(), def.getType(), def.getExpression());
1500:                         def.getType().parent(ivd);// the type of ivd is graph but we trough away the assignment
1501:                         ivd.setAccess(access);
1502:                         return ivd;
1503:                 }
1504:         }
1505:
1506:         private PDefinition readThreadDefinition() throws LexException,
1507:                         ParserException
1508:         {
1509:                 LexToken token = lastToken();
1510:
1511:•                if (token.is(VDMToken.PERIODIC))
1512:                 {
1513:•                        if (dialect != Dialect.VDM_RT)
1514:                         {
1515:                                 throwMessage(2316, "Periodic threads only available in VDM-RT");
1516:                         }
1517:
1518:                         nextToken();
1519:                         checkFor(VDMToken.BRA, 2112, "Expecting '(' after periodic");
1520:                         List<PExp> args = getExpressionReader().readExpressionList();
1521:                         checkFor(VDMToken.KET, 2113, "Expecting ')' after periodic arguments");
1522:                         checkFor(VDMToken.BRA, 2114, "Expecting '(' after periodic(...)");
1523:                         LexNameToken name = readNameToken("Expecting (name) after periodic(...)");
1524:                         checkFor(VDMToken.KET, 2115, "Expecting (name) after periodic(...)");
1525:                         // PStm statement = AstFactory.newAPeriodicStm(token.location, name, args);
1526:                         return AstFactory.newPeriodicAThreadDefinition(name, args);
1527:•                } else if (token.is(VDMToken.SPORADIC))
1528:                 {
1529:•                        if (dialect != Dialect.VDM_RT)
1530:                         {
1531:                                 throwMessage(2317, "Sporadic threads only available in VDM-RT");
1532:                         }
1533:
1534:                         nextToken();
1535:                         checkFor(VDMToken.BRA, 2312, "Expecting '(' after sporadic");
1536:                         List<PExp> args = getExpressionReader().readExpressionList();
1537:                         checkFor(VDMToken.KET, 2313, "Expecting ')' after sporadic arguments");
1538:                         checkFor(VDMToken.BRA, 2314, "Expecting '(' after sporadic(...)");
1539:                         LexNameToken name = readNameToken("Expecting (name) after sporadic(...)");
1540:                         checkFor(VDMToken.KET, 2315, "Expecting (name) after sporadic(...)");
1541:                         return AstFactory.newSporadicAThreadDefinition(name, args);
1542:                 } else
1543:                 {
1544:                         PStm stmt = getStatementReader().readStatement();
1545:                         return AstFactory.newAThreadDefinition(stmt);
1546:                 }
1547:         }
1548:
1549:         private PDefinition readPermissionPredicateDefinition()
1550:                         throws LexException, ParserException
1551:         {
1552:                 LexToken token = lastToken();
1553:
1554:•                switch (token.type)
1555:                 {
1556:                         case PER:
1557:                                 nextToken();
1558:                                 LexNameToken name = readNameToken("Expecting name after 'per'");
1559:                                 checkFor(VDMToken.IMPLIES, 2116, "Expecting <name> => <exp>");
1560:                                 PExp exp = getExpressionReader().readPerExpression();
1561:                                 return AstFactory.newAPerSyncDefinition(token.location, name, exp);
1562:
1563:                         case MUTEX:
1564:                                 nextToken();
1565:                                 checkFor(VDMToken.BRA, 2117, "Expecting '(' after mutex");
1566:                                 LexNameList opnames = new LexNameList();
1567:
1568:•                                switch (lastToken().type)
1569:                                 {
1570:                                         case ALL:
1571:                                                 nextToken();
1572:                                                 checkFor(VDMToken.KET, 2118, "Expecting ')' after 'all'");
1573:                                                 break;
1574:
1575:                                         default:
1576:                                                 LexNameToken op = readNameToken("Expecting a name");
1577:                                                 opnames.add(op);
1578:
1579:•                                                while (ignore(VDMToken.COMMA))
1580:                                                 {
1581:                                                         op = readNameToken("Expecting a name");
1582:                                                         opnames.add(op);
1583:                                                 }
1584:
1585:                                                 checkFor(VDMToken.KET, 2119, "Expecting ')'");
1586:                                                 break;
1587:                                 }
1588:
1589:                                 return AstFactory.newAMutexSyncDefinition(token.location, opnames);
1590:
1591:                         default:
1592:                                 throwMessage(2028, "Expecting 'per' or 'mutex'");
1593:                                 return null;
1594:                 }
1595:         }
1596:
1597:         private PDefinition readNamedTraceDefinition() throws ParserException,
1598:                         LexException
1599:         {
1600:                 ILexLocation start = lastToken().location;
1601:                 List<String> names = readTraceIdentifierList();
1602:                 checkFor(VDMToken.COLON, 2264, "Expecting ':' after trace name(s)");
1603:                 List<ATraceDefinitionTerm> traces = readTraceDefinitionList();
1604:
1605:                 return AstFactory.newANamedTraceDefinition(start, names, traces);
1606:         }
1607:
1608:         private List<String> readTraceIdentifierList() throws ParserException,
1609:                         LexException
1610:         {
1611:                 List<String> names = new Vector<String>();
1612:                 names.add(readIdToken("Expecting trace identifier").getName());
1613:
1614:•                while (lastToken().is(VDMToken.DIVIDE))
1615:                 {
1616:                         nextToken();
1617:                         names.add(readIdToken("Expecting trace identifier").getName());
1618:                 }
1619:
1620:                 return names;
1621:         }
1622:
1623:         private List<ATraceDefinitionTerm> readTraceDefinitionList()
1624:                         throws LexException, ParserException
1625:         {
1626:                 List<ATraceDefinitionTerm> list = new Vector<ATraceDefinitionTerm>();
1627:                 list.add(readTraceDefinitionTerm());
1628:
1629:•                while (lastToken().is(VDMToken.SEMICOLON))
1630:                 {
1631:                         try
1632:                         {
1633:                                 reader.push();
1634:                                 nextToken();
1635:                                 list.add(readTraceDefinitionTerm());
1636:                                 reader.unpush();
1637:                         } catch (ParserException e)
1638:                         {
1639:                                 reader.pop();
1640:                                 break;
1641:                         }
1642:                 }
1643:
1644:                 return list;
1645:         }
1646:
1647:         private ATraceDefinitionTerm readTraceDefinitionTerm() throws LexException,
1648:                         ParserException
1649:         {
1650:                 List<PTraceDefinition> term = new Vector<PTraceDefinition>();
1651:                 term.add(readTraceDefinition());
1652:
1653:•                while (lastToken().is(VDMToken.PIPE))
1654:                 {
1655:                         nextToken();
1656:                         term.add(readTraceDefinition());
1657:                 }
1658:
1659:                 return AstFactory.newATraceDefinitionTerm(term);
1660:         }
1661:
1662:         private PTraceDefinition readTraceDefinition() throws LexException,
1663:                         ParserException
1664:         {
1665:•                if (lastToken().is(VDMToken.LET))
1666:                 {
1667:                         return readTraceBinding();
1668:                 } else
1669:                 {
1670:                         return readTraceRepeat();
1671:                 }
1672:         }
1673:
1674:         private PTraceDefinition readTraceRepeat() throws ParserException,
1675:                         LexException
1676:         {
1677:                 PTraceCoreDefinition core = readCoreTraceDefinition();
1678:
1679:                 long from = 1;
1680:                 long to = 1;
1681:                 LexToken token = lastToken();
1682:
1683:•                switch (token.type)
1684:                 {
1685:                         case TIMES:
1686:                                 from = 0;
1687:                                 to = Properties.traces_max_repeats;
1688:                                 nextToken();
1689:                                 break;
1690:
1691:                         case PLUS:
1692:                                 from = 1;
1693:                                 to = Properties.traces_max_repeats;
1694:                                 nextToken();
1695:                                 break;
1696:
1697:                         case QMARK:
1698:                                 from = 0;
1699:                                 to = 1;
1700:                                 nextToken();
1701:                                 break;
1702:
1703:                         case SET_OPEN:
1704:•                                if (nextToken().isNot(VDMToken.NUMBER))
1705:                                 {
1706:                                         throwMessage(2266, "Expecting '{n}' or '{n1, n2}' after trace definition");
1707:                                 }
1708:
1709:                                 LexIntegerToken lit = (LexIntegerToken) lastToken();
1710:                                 from = lit.value;
1711:                                 to = lit.value;
1712:
1713:•                                switch (nextToken().type)
1714:                                 {
1715:                                         case COMMA:
1716:•                                                if (nextToken().isNot(VDMToken.NUMBER))
1717:                                                 {
1718:                                                         throwMessage(2265, "Expecting '{n1, n2}' after trace definition");
1719:                                                 }
1720:
1721:                                                 lit = (LexIntegerToken) readToken();
1722:                                                 to = lit.value;
1723:                                                 checkFor(VDMToken.SET_CLOSE, 2265, "Expecting '{n1, n2}' after trace definition");
1724:                                                 break;
1725:
1726:                                         case SET_CLOSE:
1727:                                                 nextToken();
1728:                                                 break;
1729:
1730:                                         default:
1731:                                                 throwMessage(2266, "Expecting '{n}' or '{n1, n2}' after trace definition");
1732:                                 }
1733:                                 break;
1734:                         default:
1735:                                 break;
1736:                 }
1737:
1738:                 return AstFactory.newARepeatTraceDefinition(token.location, core, from, to);
1739:         }
1740:
1741:         private PTraceDefinition readTraceBinding() throws ParserException,
1742:                         LexException
1743:         {
1744:                 checkFor(VDMToken.LET, 2230, "Expecting 'let'");
1745:                 ParserException letDefError = null;
1746:
1747:                 try
1748:                 {
1749:                         reader.push();
1750:                         PTraceDefinition def = readLetDefBinding();
1751:                         reader.unpush();
1752:                         return def;
1753:                 } catch (ParserException e)
1754:                 {
1755:                         e.adjustDepth(reader.getTokensRead());
1756:                         reader.pop();
1757:                         letDefError = e;
1758:                 }
1759:
1760:                 try
1761:                 {
1762:                         reader.push();
1763:                         PTraceDefinition def = readLetBeStBinding();
1764:                         reader.unpush();
1765:                         return def;
1766:                 } catch (ParserException e)
1767:                 {
1768:                         e.adjustDepth(reader.getTokensRead());
1769:                         reader.pop();
1770:•                        throw e.deeperThan(letDefError) ? e : letDefError;
1771:                 }
1772:         }
1773:
1774:         private PTraceDefinition readLetDefBinding() throws ParserException,
1775:                         LexException
1776:         {
1777:                 List<AValueDefinition> localDefs = new Vector<AValueDefinition>();
1778:                 LexToken start = lastToken();
1779:
1780:                 PDefinition def = readLocalDefinition(NameScope.LOCAL);
1781:
1782:•                if (!(def instanceof AValueDefinition))
1783:                 {
1784:                         throwMessage(2270, "Only value definitions allowed in traces");
1785:                 }
1786:
1787:                 localDefs.add((AValueDefinition) def);
1788:
1789:•                while (ignore(VDMToken.COMMA))
1790:                 {
1791:                         def = readLocalDefinition(NameScope.LOCAL);
1792:
1793:•                        if (!(def instanceof AValueDefinition))
1794:                         {
1795:                                 throwMessage(2270, "Only value definitions allowed in traces");
1796:                         }
1797:
1798:                         localDefs.add((AValueDefinition) def);
1799:                 }
1800:
1801:                 checkFor(VDMToken.IN, 2231, "Expecting 'in' after local definitions");
1802:                 PTraceDefinition body = readTraceDefinition();
1803:
1804:                 return AstFactory.newALetDefBindingTraceDefinition(start.location, localDefs, body);
1805:         }
1806:
1807:         private PTraceDefinition readLetBeStBinding() throws ParserException,
1808:                         LexException
1809:         {
1810:                 LexToken start = lastToken();
1811:                 PMultipleBind bind = getBindReader().readMultipleBind();
1812:                 PExp stexp = null;
1813:
1814:•                if (lastToken().is(VDMToken.BE))
1815:                 {
1816:                         nextToken();
1817:                         checkFor(VDMToken.ST, 2232, "Expecting 'st' after 'be' in let statement");
1818:                         stexp = getExpressionReader().readExpression();
1819:                 }
1820:
1821:                 checkFor(VDMToken.IN, 2233, "Expecting 'in' after bind in let statement");
1822:                 PTraceDefinition body = readTraceDefinition();
1823:
1824:                 return AstFactory.newALetBeStBindingTraceDefinition(start.location, bind, stexp, body);
1825:         }
1826:
1827:         private PTraceCoreDefinition readCoreTraceDefinition()
1828:                         throws ParserException, LexException
1829:         {
1830:                 LexToken token = lastToken();
1831:
1832:•                switch (token.type)
1833:                 {
1834:                         case IDENTIFIER:
1835:                         case NAME:
1836:                         case SELF:
1837:                                 StatementReader sr = getStatementReader();
1838:                                 PStm stmt = sr.readCallStatement();
1839:
1840:•                                if (!(stmt instanceof ACallStm)
1841:                                                 && !(stmt instanceof ACallObjectStm))
1842:                                 {
1843:                                         throwMessage(2267, "Expecting 'obj.op(args)' or 'op(args)'", token);
1844:                                 }
1845:
1846:                                 return AstFactory.newAApplyExpressionTraceCoreDefinition(stmt, getCurrentModule());
1847:
1848:                         case BRA:
1849:                                 nextToken();
1850:                                 List<ATraceDefinitionTerm> list = readTraceDefinitionList();
1851:                                 ILexLocation semi = lastToken().location;
1852:                                 
1853:•                                if (ignore(VDMToken.SEMICOLON) && Settings.strict)
1854:                                 {
1855:                                         warning(5029, "Strict: unexpected trailing semi-colon", semi);
1856:                                 }
1857:                                 
1858:                                 checkFor(VDMToken.KET, 2269, "Expecting '(trace definitions)'");
1859:                                 return AstFactory.newABracketedExpressionTraceCoreDefinition(token.location, list);
1860:
1861:                         case PIPEPIPE:
1862:                                 nextToken();
1863:                                 checkFor(VDMToken.BRA, 2292, "Expecting '|| (...)'");
1864:                                 List<PTraceDefinition> defs = new Vector<PTraceDefinition>();
1865:                                 defs.add(readTraceDefinition());
1866:                                 checkFor(VDMToken.COMMA, 2293, "Expecting '|| (a, b {,...})'");
1867:                                 defs.add(readTraceDefinition());
1868:
1869:•                                while (lastToken().is(VDMToken.COMMA))
1870:                                 {
1871:                                         nextToken();
1872:                                         defs.add(readTraceDefinition());
1873:                                 }
1874:
1875:                                 checkFor(VDMToken.KET, 2294, "Expecting ')' ending || clause");
1876:                                 return AstFactory.newAConcurrentExpressionTraceCoreDefinition(token.location, defs);
1877:
1878:                         default:
1879:                                 throwMessage(2267, "Expecting 'obj.op(args)' or 'op(args)'", token);
1880:                                 return null;
1881:                 }
1882:         }
1883:
1884:         private PExp readFunctionBody() throws LexException, ParserException
1885:         {
1886:                 ILexToken token = lastToken();
1887:
1888:•                if (token.is(VDMToken.IS))
1889:                 {
1890:•                        switch (nextToken().type)
1891:                         {
1892:                                 case NOT:
1893:                                         nextToken();
1894:                                         checkFor(VDMToken.YET, 2125, "Expecting 'is not yet specified'");
1895:                                         checkFor(VDMToken.SPECIFIED, 2126, "Expecting 'is not yet specified'");
1896:                                         return AstFactory.newANotYetSpecifiedExp(token.getLocation());
1897:
1898:                                 case SUBCLASS:
1899:                                         nextToken();
1900:                                         checkFor(VDMToken.RESPONSIBILITY, 2127, "Expecting 'is subclass responsibility'");
1901:                                         return AstFactory.newASubclassResponsibilityExp(token.getLocation());
1902:
1903:                                 default:
1904:•                                        if (dialect == Dialect.VDM_PP)
1905:                                         {
1906:                                                 throwMessage(2033, "Expecting 'is not yet specified' or 'is subclass responsibility'", token);
1907:                                         } else
1908:                                         {
1909:                                                 throwMessage(2033, "Expecting 'is not yet specified'", token);
1910:                                         }
1911:                                         return null;
1912:                         }
1913:                 } else
1914:                 {
1915:                         ExpressionReader expr = getExpressionReader();
1916:                         return expr.readExpression();
1917:                 }
1918:         }
1919:
1920:         private PStm readOperationBody() throws LexException, ParserException
1921:         {
1922:                 ILexToken token = lastToken();
1923:
1924:•                if (token.is(VDMToken.IS))
1925:                 {
1926:•                        switch (nextToken().type)
1927:                         {
1928:                                 case NOT:
1929:                                         nextToken();
1930:                                         checkFor(VDMToken.YET, 2187, "Expecting 'is not yet specified");
1931:                                         checkFor(VDMToken.SPECIFIED, 2188, "Expecting 'is not yet specified");
1932:                                         return AstFactory.newANotYetSpecifiedStm(token.getLocation());
1933:
1934:                                 case SUBCLASS:
1935:                                         nextToken();
1936:                                         checkFor(VDMToken.RESPONSIBILITY, 2189, "Expecting 'is subclass responsibility'");
1937:                                         return AstFactory.newASubclassResponsibilityStm(token.getLocation());
1938:
1939:                                 default:
1940:•                                        if (dialect == Dialect.VDM_PP)
1941:                                         {
1942:                                                 throwMessage(2062, "Expecting 'is not yet specified' or 'is subclass responsibility'", token);
1943:                                         } else
1944:                                         {
1945:                                                 throwMessage(2062, "Expecting 'is not yet specified'", token);
1946:                                         }
1947:                                         return null;
1948:                         }
1949:                 } else
1950:                 {
1951:                         StatementReader stmt = getStatementReader();
1952:                         return stmt.readStatement();
1953:                 }
1954:         }
1955: }