Package: OrderedObligation

OrderedObligation

nameinstructionbranchcomplexitylinemethod
OrderedObligation(SBinaryExp, List, IPOContextStack, IPogAssistantFactory)
M: 0 C: 27
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
makeIsType(PExp, PExp, PType)
M: 0 C: 18
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
stitchIsExps(List, PExp, PExp)
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%

Coverage

1: package org.overture.pog.obligation;
2:
3: import org.overture.ast.analysis.AnalysisException;
4: import org.overture.ast.expressions.AVariableExp;
5: import org.overture.ast.expressions.PExp;
6: import org.overture.ast.expressions.SBinaryExp;
7: import org.overture.ast.factory.AstExpressionFactory;
8: import org.overture.ast.factory.AstFactory;
9: import org.overture.ast.lex.LexNameToken;
10: import org.overture.ast.types.PType;
11: import org.overture.pog.pub.IPOContextStack;
12: import org.overture.pog.pub.IPogAssistantFactory;
13: import org.overture.pog.pub.POType;
14: import java.util.List;
15: import java.util.Vector;
16:
17: /**
18: * Created by ldc on 08/06/17.
19: */
20: public class OrderedObligation extends ProofObligation
21: {
22:         public OrderedObligation(SBinaryExp node, List<PType> types, IPOContextStack ctxt,IPogAssistantFactory af)
23:                         throws AnalysisException
24:         {
25:                 super(node, POType.ORDERED,ctxt,node.getLocation(),af);
26:
27:                 PExp lExp = node.getLeft();
28:                 PExp rExp = node.getRight();
29:
30:                 PExp r = stitchIsExps(types,lExp,rExp);
31:                 valuetree.setPredicate(ctxt.getPredWithContext(r));
32:         }
33:
34:         private PExp stitchIsExps(List<PType> types, PExp lExp, PExp rExp) {
35:•                if (types.size() == 1){
36:                         return makeIsType(lExp, rExp, types.get(0));
37:                 }
38:                 else {
39:                         return AstExpressionFactory.newAOrBooleanBinaryExp(
40:                                         makeIsType(lExp,rExp,types.get(0)),
41:                                                         stitchIsExps(types.subList(1,types.size()),lExp,rExp));
42:                 }
43:         }
44:
45:         private PExp makeIsType(PExp lExp, PExp rExp, PType type)
46:         {
47:                 PExp lIs = AstExpressionFactory.newAIsExp(type.clone(),lExp.clone());
48:                 PExp rIs = AstExpressionFactory.newAIsExp(type.clone(),rExp.clone());
49:                 PExp andExp = AstExpressionFactory.newAAndBooleanBinaryExp(lIs,rIs);
50:                 return andExp;
51:         }
52: }