Package: POFunctionResultContext

POFunctionResultContext

nameinstructionbranchcomplexitylinemethod
POFunctionResultContext(AExplicitFunctionDefinition)
M: 0 C: 47
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
POFunctionResultContext(AImplicitFunctionDefinition)
M: 0 C: 29
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
getContext()
M: 58 C: 0
0%
M: 4 C: 0
0%
M: 3 C: 0
0%
M: 14 C: 0
0%
M: 1 C: 0
0%
getContextNode(PExp)
M: 0 C: 17
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
getContextNodeMain(PExp)
M: 0 C: 93
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 23
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.contexts;
25:
26: import java.util.LinkedList;
27: import java.util.List;
28:
29: import org.overture.ast.definitions.AEqualsDefinition;
30: import org.overture.ast.definitions.AExplicitFunctionDefinition;
31: import org.overture.ast.definitions.AImplicitFunctionDefinition;
32: import org.overture.ast.definitions.PDefinition;
33: import org.overture.ast.expressions.AExistsExp;
34: import org.overture.ast.expressions.AImpliesBooleanBinaryExp;
35: import org.overture.ast.expressions.ALetDefExp;
36: import org.overture.ast.expressions.PExp;
37: import org.overture.ast.factory.AstExpressionFactory;
38: import org.overture.ast.factory.AstFactory;
39: import org.overture.ast.intf.lex.ILexNameToken;
40: import org.overture.ast.lex.LexNameToken;
41: import org.overture.ast.patterns.APatternTypePair;
42: import org.overture.ast.patterns.ATypeMultipleBind;
43: import org.overture.ast.patterns.PMultipleBind;
44: import org.overture.ast.patterns.PPattern;
45: import org.overture.ast.types.ABooleanBasicType;
46: import org.overture.ast.types.AFunctionType;
47:
48: public class POFunctionResultContext extends POContext
49: {
50:         public final ILexNameToken name;
51:         public final AFunctionType deftype;
52:         public final PExp precondition;
53:         public final PExp body;
54:         public final APatternTypePair result;
55:         public final boolean implicit;
56:         final PDefinition function;
57:
58:         public POFunctionResultContext(AExplicitFunctionDefinition definition)
59:         {
60:                 this.name = definition.getName();
61:                 this.deftype = (AFunctionType) definition.getType();
62:                 this.precondition = definition.getPrecondition();
63:                 this.body = definition.getBody();
64:                 this.implicit = false;
65:                 this.result = AstFactory.newAPatternTypePair(AstFactory.newAIdentifierPattern(new LexNameToken(definition.getName().getModule(), "RESULT", definition.getLocation())), ((AFunctionType) definition.getType()).getResult().clone());
66:                 this.function = definition.clone();
67:                 function.setLocation(null);
68:         }
69:
70:         public POFunctionResultContext(AImplicitFunctionDefinition definition)
71:         {
72:                 this.name = definition.getName();
73:                 this.deftype = (AFunctionType) definition.getType();
74:                 this.precondition = definition.getPrecondition();
75:                 this.body = definition.getBody();
76:                 this.implicit = true;
77:                 this.result = definition.getResult();
78:                 this.function = definition;
79:
80:         }
81:
82:         @Override
83:         public PExp getContextNode(PExp stitch)
84:         {
85:
86:                 PExp stitched = getContextNodeMain(stitch);
87:
88:•                if (precondition == null)
89:                 {
90:                         return stitched;
91:                 } else
92:                 {
93:                         AImpliesBooleanBinaryExp imp = AstExpressionFactory.newAImpliesBooleanBinaryExp(precondition.clone(), stitched);
94:                         return imp;
95:                 }
96:
97:         }
98:
99:         private PExp getContextNodeMain(PExp stitch)
100:         {
101:•                if (implicit)
102:                 {
103:                         AExistsExp exists_exp = new AExistsExp();
104:                         exists_exp.setType(new ABooleanBasicType());
105:                         List<PMultipleBind> binds = new LinkedList<PMultipleBind>();
106:                         ATypeMultipleBind tmBind = new ATypeMultipleBind();
107:                         List<PPattern> patternList = new LinkedList<PPattern>();
108:                         patternList.add(result.getPattern().clone());
109:                         tmBind.setPlist(patternList);
110:                         tmBind.setType(result.getType().clone());
111:                         binds.add(tmBind);
112:                         exists_exp.setBindList(binds);
113:                         exists_exp.setPredicate(stitch);
114:                         return exists_exp;
115:                 }
116:
117:                 else
118:                 {
119:                         ALetDefExp letDefExp = new ALetDefExp();
120:                         AEqualsDefinition localDef = new AEqualsDefinition();
121:                         localDef.setPattern(result.getPattern().clone());
122:                         localDef.setType(result.getType().clone());
123:                         localDef.setTest(body.clone());
124:                         List<PDefinition> defs = new LinkedList<PDefinition>();
125:                         defs.add(localDef);
126:                         letDefExp.setLocalDefs(defs);
127:                         letDefExp.setExpression(stitch);
128:                         return letDefExp;
129:                 }
130:
131:         }
132:
133:         @Override
134:         public String getContext()
135:         {
136:                 StringBuilder sb = new StringBuilder();
137:
138:•                if (precondition != null)
139:                 {
140:                         sb.append(precondition);
141:                         sb.append(" => ");
142:                 }
143:
144:•                if (implicit)
145:                 {
146:                         sb.append("forall ");
147:                         sb.append(result);
148:                         sb.append(" & ");
149:                 } else
150:                 {
151:                         sb.append("let ");
152:                         sb.append(result);
153:                         sb.append(" = ");
154:                         sb.append(body);
155:                         sb.append(" in ");
156:                 }
157:
158:                 return sb.toString();
159:         }
160: }