Package: RecursiveObligation

RecursiveObligation

nameinstructionbranchcomplexitylinemethod
RecursiveObligation(AExplicitFunctionDefinition, AApplyExp, IPOContextStack, IPogAssistantFactory)
M: 37 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
RecursiveObligation(AImplicitFunctionDefinition, AApplyExp, IPOContextStack, IPogAssistantFactory)
M: 37 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
RecursiveObligation(List, AApplyExp, IPOContextStack, IPogAssistantFactory)
M: 22 C: 69
76%
M: 2 C: 2
50%
M: 2 C: 1
33%
M: 3 C: 13
81%
M: 0 C: 1
100%
buildMeasureLeft(AExplicitFunctionDefinition, AApplyExp)
M: 0 C: 32
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
buildMeasureLeft(AImplicitFunctionDefinition, AApplyExp)
M: 33 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 5 C: 0
0%
M: 1 C: 0
0%
buildMeasureLeftParams(AApplyExp, List, PType, ILexNameToken, List)
M: 15 C: 70
82%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 4 C: 16
80%
M: 0 C: 1
100%
buildMeasureRight(AExplicitFunctionDefinition, AApplyExp)
M: 0 C: 9
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
buildMeasureRight(AImplicitFunctionDefinition, AApplyExp)
M: 9 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
buildMeasureRightParams(AApplyExp, ILexNameToken, PType)
M: 2 C: 85
98%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 1 C: 21
95%
M: 0 C: 1
100%
buildStructuralComparison(PExp, PExp, int)
M: 58 C: 6
9%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 11 C: 2
15%
M: 0 C: 1
100%
buildStructuralLessThan(PExp, PExp, int, int)
M: 75 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 15 C: 0
0%
M: 1 C: 0
0%
buildValueDef(PExp, String)
M: 30 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
getLex(AExplicitFunctionDefinition)
M: 8 C: 13
62%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 2 C: 5
71%
M: 0 C: 1
100%
getMeasureName(PDefinition)
M: 20 C: 18
47%
M: 5 C: 3
38%
M: 3 C: 2
40%
M: 6 C: 5
45%
M: 0 C: 1
100%
wrapName(ILexNameToken)
M: 0 C: 14
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
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.pog.obligation;
25:
26: import java.util.LinkedList;
27: import java.util.List;
28:
29: import org.overture.ast.analysis.AnalysisException;
30: import org.overture.ast.definitions.AExplicitFunctionDefinition;
31: import org.overture.ast.definitions.AImplicitFunctionDefinition;
32: import org.overture.ast.definitions.AValueDefinition;
33: import org.overture.ast.definitions.PDefinition;
34: import org.overture.ast.expressions.AApplyExp;
35: import org.overture.ast.expressions.AFieldNumberExp;
36: import org.overture.ast.expressions.AFuncInstatiationExp;
37: import org.overture.ast.expressions.AGreaterNumericBinaryExp;
38: import org.overture.ast.expressions.AIfExp;
39: import org.overture.ast.expressions.ALetDefExp;
40: import org.overture.ast.expressions.ANotEqualBinaryExp;
41: import org.overture.ast.expressions.AVariableExp;
42: import org.overture.ast.expressions.PExp;
43: import org.overture.ast.factory.AstExpressionFactory;
44: import org.overture.ast.intf.lex.ILexNameToken;
45: import org.overture.ast.lex.LexIntegerToken;
46: import org.overture.ast.lex.LexNameToken;
47: import org.overture.ast.patterns.AIdentifierPattern;
48: import org.overture.ast.patterns.APatternListTypePair;
49: import org.overture.ast.patterns.PPattern;
50: import org.overture.ast.types.AFunctionType;
51: import org.overture.ast.types.AProductType;
52: import org.overture.ast.types.PType;
53: import org.overture.pog.pub.IPOContextStack;
54: import org.overture.pog.pub.IPogAssistantFactory;
55: import org.overture.pog.pub.POType;
56:
57: public class RecursiveObligation extends ProofObligation
58: {
59:
60:         private static final long serialVersionUID = -6975984943449362262L;
61:
62:         private static final String LEFT_MEASURE_NAME = "LME";
63:         private static final String RIGHT_MEASURE_NAME = "RME";
64:
65:         public RecursiveObligation(AExplicitFunctionDefinition def,
66:                         AApplyExp apply, IPOContextStack ctxt, IPogAssistantFactory af)
67:                         throws AnalysisException
68:         {
69:                 super(apply, POType.RECURSIVE, ctxt, apply.getLocation(), af);
70:
71:                 PExp measureLeft_exp = buildMeasureLeft(def, apply);
72:                 PExp measureRight_exp = buildMeasureRight(def, apply);
73:
74:                 PExp lt_exp = buildStructuralComparison(measureLeft_exp, measureRight_exp, getLex(def.getMeasureDef()));
75:
76:                 stitch = lt_exp;
77:                 valuetree.setPredicate(ctxt.getPredWithContext(lt_exp));
78:         }
79:
80:         public RecursiveObligation(AImplicitFunctionDefinition def,
81:                         AApplyExp apply, IPOContextStack ctxt, IPogAssistantFactory af)
82:                         throws AnalysisException
83:         {
84:                 super(def, POType.RECURSIVE, ctxt, apply.getLocation(), af);
85:
86:                 PExp measureLeft_exp = buildMeasureLeft(def, apply);
87:                 PExp measureRight_exp = buildMeasureRight(def, apply);
88:
89:                 PExp lt_exp = buildStructuralComparison(measureLeft_exp, measureRight_exp, getLex(def.getMeasureDef()));
90:
91:                 stitch = lt_exp;
92:                 valuetree.setPredicate(ctxt.getPredWithContext(lt_exp));
93:         }
94:
95:         public RecursiveObligation(List<PDefinition> defs, AApplyExp apply, IPOContextStack ctxt, IPogAssistantFactory af)
96:                 throws AnalysisException
97:         {
98:                 super(defs.get(0), POType.RECURSIVE, ctxt, apply.getLocation(), af);
99:                 PExp measureLeft_exp = null;
100:                 PExp measureRight_exp = null;
101:                 AExplicitFunctionDefinition measureDef = null;
102:
103:•                if (defs.get(0) instanceof AExplicitFunctionDefinition)
104:                 {
105:                         measureLeft_exp = buildMeasureLeft((AExplicitFunctionDefinition)defs.get(0), apply);
106:                         measureDef = ((AExplicitFunctionDefinition)defs.get(0)).getMeasureDef();
107:                 }
108:                 else
109:                 {
110:                         measureLeft_exp = buildMeasureLeft((AImplicitFunctionDefinition)defs.get(0), apply);
111:                         measureDef = ((AImplicitFunctionDefinition)defs.get(0)).getMeasureDef();
112:                 }
113:
114:•                if (defs.get(1) instanceof AExplicitFunctionDefinition)
115:                 {
116:                         measureRight_exp = buildMeasureRight((AExplicitFunctionDefinition)defs.get(1), apply);
117:                 }
118:                 else
119:                 {
120:                         measureRight_exp = buildMeasureRight((AImplicitFunctionDefinition)defs.get(1), apply);
121:                 }
122:
123:                 PExp lt_exp = buildStructuralComparison(measureLeft_exp, measureRight_exp, getLex(measureDef));
124:
125:                 stitch = lt_exp;
126:                 valuetree.setPredicate(ctxt.getPredWithContext(lt_exp));
127:         }
128:
129:         private PExp buildMeasureLeft(AExplicitFunctionDefinition def,
130:                         AApplyExp apply) throws AnalysisException
131:         {
132:                 List<PPattern> paramPatterns = new LinkedList<PPattern>();
133:•                for (List<PPattern> list : def.getParamPatternList())
134:                 {
135:                         paramPatterns.addAll(list);
136:                 }
137:
138:                 return buildMeasureLeftParams(apply, def.getTypeParams(), def.getActualResult(), getMeasureName(def), paramPatterns);
139:         }
140:
141:         private PExp buildMeasureLeft(AImplicitFunctionDefinition def,
142:                         AApplyExp apply) throws AnalysisException
143:         {
144:                 List<PPattern> paramPatterns = new LinkedList<PPattern>();
145:•                for (APatternListTypePair pair : def.getParamPatterns())
146:                 {
147:                         paramPatterns.addAll(pair.getPatterns());
148:                 }
149:
150:                 return buildMeasureLeftParams(apply, def.getTypeParams(), def.getActualResult(), getMeasureName(def), paramPatterns);
151:         }
152:
153:         private PExp buildMeasureLeftParams(AApplyExp apply,
154:                         List<ILexNameToken> typeParams, PType actualResult,
155:                         ILexNameToken measure, List<PPattern> paramPatterns)
156:                         throws AnalysisException
157:         {
158:                 AApplyExp apply_exp = new AApplyExp();
159:
160:•                if (typeParams != null && !typeParams.isEmpty())
161:                 {
162:•                        if (apply.getRoot() instanceof AFuncInstatiationExp)
163:                         {
164:                                 AFuncInstatiationExp func_exp = (AFuncInstatiationExp) apply.getRoot().clone();
165:                                 func_exp.setFunction(wrapName(measure.clone()));
166:                                 apply_exp.setRoot(func_exp);
167:                         }
168:                         else
169:                         {
170:                                 AFuncInstatiationExp func_exp = new AFuncInstatiationExp();
171:                                 func_exp.setActualTypes(cloneListType(apply.getArgtypes()));        // Not sure about this?
172:                                 func_exp.setFunction(wrapName(measure.clone()));
173:                                 apply_exp.setRoot(func_exp);
174:                         }
175:                 }
176:                 else
177:                 {
178:                         apply_exp.setRoot(wrapName(measure.clone()));
179:                 }
180:
181:                 List<PExp> args = new LinkedList<PExp>();
182:
183:•                for (PPattern p : paramPatterns)
184:                 {
185:                         args.add(patternToExp(p.clone()));
186:                 }
187:
188:                 apply_exp.setType(actualResult.clone());
189:                 apply_exp.setArgs(args);
190:                 return apply_exp;
191:
192:         }
193:
194:         private PExp buildMeasureRight(AExplicitFunctionDefinition def,
195:                         AApplyExp apply)
196:         {
197:                 return buildMeasureRightParams(apply, getMeasureName(def), def.getActualResult());
198:         }
199:
200:         private PExp buildMeasureRight(AImplicitFunctionDefinition def,
201:                         AApplyExp apply)
202:         {
203:                 return buildMeasureRightParams(apply, getMeasureName(def), def.getActualResult());
204:         }
205:
206:         private PExp buildMeasureRightParams(AApplyExp apply,
207:                         ILexNameToken measure, PType actualResult)
208:         {
209:                 PExp start = null;
210:                 PExp root = apply.getRoot().clone();
211:
212:•                if (root instanceof AApplyExp)
213:                 {
214:                         AApplyExp aexp = (AApplyExp) root;
215:                         start = buildMeasureRightParams(aexp, measure, actualResult);
216:•                } else if (root instanceof AVariableExp)
217:                 {
218:                         start = wrapName(measure.clone());
219:•                } else if (root instanceof AFuncInstatiationExp)
220:                 {
221:                         AFuncInstatiationExp fie = (AFuncInstatiationExp) root;
222:                         AFuncInstatiationExp func_exp = new AFuncInstatiationExp();
223:                         func_exp.setActualTypes(cloneListType(fie.getActualTypes()));
224:                         func_exp.setFunction(wrapName(measure.clone()));
225:                         start = func_exp;
226:                 } else
227:                 {
228:                         start = root;
229:                 }
230:
231:                 List<PExp> arglist = new LinkedList<PExp>();
232:•                for (PExp arg : apply.getArgs())
233:                 {
234:                         arglist.add(arg.clone());
235:                 }
236:
237:                 AApplyExp apply_exp = getApplyExp(start, arglist);
238:                 apply_exp.setType(actualResult.clone());
239:
240:                 return apply_exp;
241:         }
242:
243:         private PExp buildStructuralComparison(PExp left_exp, PExp right_exp,
244:                         int measureLexical)
245:         {
246:•                if (measureLexical == 0)
247:                 // what about 1 measures? same as 0?
248:                 {
249:                         return AstExpressionFactory.newAGreaterNumericBinaryExp(left_exp, right_exp);
250:                 }
251:
252:                 ALetDefExp let_exp = new ALetDefExp();
253:
254:                 AValueDefinition left_def = buildValueDef(left_exp, LEFT_MEASURE_NAME);
255:                 AValueDefinition right_def = buildValueDef(right_exp, RIGHT_MEASURE_NAME);
256:
257:                 List<PDefinition> localDefs = new LinkedList<PDefinition>();
258:                 localDefs.add(left_def);
259:                 localDefs.add(right_def);
260:
261:                 let_exp.setLocalDefs(localDefs);
262:
263:                 // let left = [left expression], right=[right expression]
264:                 // in ...
265:
266:                 // we don't strictly need the let in
267:
268:                 AVariableExp leftName_exp = wrapName(new LexNameToken(null, LEFT_MEASURE_NAME, null));
269:                 AVariableExp rightName_exp = wrapName(new LexNameToken(null, RIGHT_MEASURE_NAME, null));
270:
271:                 // build the left < right structural comparison expression
272:                 let_exp.setExpression(buildStructuralLessThan(leftName_exp, rightName_exp, 1, measureLexical).clone());
273:
274:                 return let_exp;
275:         }
276:
277:         private PExp buildStructuralLessThan(PExp left_exp, PExp right_exp,
278:                         int tupleCounter, int recCounter)
279:         {
280:                 // left.i
281:                 AFieldNumberExp leftField_exp = new AFieldNumberExp();
282:                 leftField_exp.setTuple(left_exp.clone());
283:                 leftField_exp.setField(new LexIntegerToken(tupleCounter, null));
284:
285:                 // right.i
286:                 AFieldNumberExp rightField_exp = new AFieldNumberExp();
287:                 rightField_exp.setTuple(right_exp.clone());
288:                 rightField_exp.setField(new LexIntegerToken(tupleCounter, null));
289:
290:•                if (recCounter == 1)
291:                 {
292:                         // last one. don't chain further ifs
293:                         return AstExpressionFactory.newAGreaterNumericBinaryExp(leftField_exp, rightField_exp);
294:                 }
295:
296:                 // left.i <> right.i
297:                 ANotEqualBinaryExp notEquals_exp = AstExpressionFactory.newANotEqualBinaryExp(leftField_exp, rightField_exp);
298:
299:                 // if left.i <>right.i then left.i , right.i else [recurse]
300:                 AGreaterNumericBinaryExp gt_exp = AstExpressionFactory.newAGreaterNumericBinaryExp(leftField_exp.clone(), rightField_exp.clone());
301:                 AIfExp if_exp = new AIfExp();
302:                 if_exp.setTest(notEquals_exp);
303:                 if_exp.setThen(gt_exp);
304:
305:                 if_exp.setElse(buildStructuralLessThan(left_exp.clone(), right_exp.clone(), tupleCounter + 1, recCounter - 1));
306:
307:                 return if_exp;
308:         }
309:
310:         private AValueDefinition buildValueDef(PExp exp, String name)
311:         {
312:                 AValueDefinition valDef = new AValueDefinition();
313:                 valDef.setType(exp.getType().clone());
314:                 valDef.setExpression(exp.clone());
315:
316:                 AIdentifierPattern pattern = new AIdentifierPattern();
317:                 pattern.setName(new LexNameToken(null, name, null));
318:
319:                 valDef.setPattern(pattern);
320:
321:                 return valDef;
322:         }
323:
324:         private AVariableExp wrapName(ILexNameToken name)
325:         {
326:                 AVariableExp r = new AVariableExp();
327:                 r.setName(name.clone());
328:                 r.setOriginal(name.getFullName());
329:                 return r;
330:         }
331:         
332:         private int getLex(AExplicitFunctionDefinition mdef)
333:         {
334:•                if (mdef == null)
335:                 {
336:                         return 0;
337:                 }
338:
339:                 AFunctionType ftype = (AFunctionType) mdef.getType();
340:
341:•                if (ftype.getResult() instanceof AProductType)
342:                 {
343:                         AProductType type = (AProductType)ftype.getResult();
344:                         return type.getTypes().size();
345:                 }
346:                 else
347:                 {
348:                         return 0;
349:                 }
350:         }
351:         
352:         private ILexNameToken getMeasureName(PDefinition def)
353:         {
354:•                if (def instanceof AExplicitFunctionDefinition)
355:                 {
356:                         AExplicitFunctionDefinition edef = (AExplicitFunctionDefinition)def;
357:
358:•                        if (edef.getMeasureName() != null)
359:                         {
360:                                 return edef.getMeasureName();
361:                         }
362:                         else
363:                         {
364:                                 return edef.getName().getMeasureName(def.getLocation());
365:                         }
366:                 }
367:•                else if (def instanceof AImplicitFunctionDefinition)
368:                 {
369:                         AImplicitFunctionDefinition idef = (AImplicitFunctionDefinition)def;
370:
371:•                        if (idef.getMeasureName() != null)
372:                         {
373:                                 return idef.getMeasureName();
374:                         }
375:                         else
376:                         {
377:                                 return idef.getName().getMeasureName(def.getLocation());
378:                         }
379:                 }
380:                 else
381:                 {
382:                         return null;
383:                 }
384:         }
385: }