Method: getSetBindList(ILexNameToken, ILexNameToken)

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.List;
27: import java.util.Vector;
28:
29: import org.overture.ast.analysis.AnalysisException;
30: import org.overture.ast.expressions.AApplyExp;
31: import org.overture.ast.expressions.AExistsExp;
32: import org.overture.ast.expressions.AForAllExp;
33: import org.overture.ast.expressions.AMapCompMapExp;
34: import org.overture.ast.expressions.AMapDomainUnaryExp;
35: import org.overture.ast.expressions.AMapEnumMapExp;
36: import org.overture.ast.expressions.AMapletExp;
37: import org.overture.ast.expressions.PExp;
38: import org.overture.ast.factory.AstExpressionFactory;
39: import org.overture.ast.intf.lex.ILexNameToken;
40: import org.overture.ast.patterns.PMultipleBind;
41: import org.overture.ast.types.ABooleanBasicType;
42: import org.overture.ast.types.AMapMapType;
43: import org.overture.ast.types.ANatNumericBasicType;
44: import org.overture.ast.types.PType;
45: import org.overture.pog.pub.IPOContextStack;
46: import org.overture.pog.pub.IPogAssistantFactory;
47: import org.overture.pog.pub.POType;
48:
49: public class FiniteMapObligation extends ProofObligation
50: {
51:         private static final long serialVersionUID = -2891663568497319141L;
52:
53:         public FiniteMapObligation(AMapCompMapExp exp, PType mapType,
54:                         IPOContextStack ctxt, IPogAssistantFactory af)
55:                         throws AnalysisException
56:         {
57:                 super(exp, POType.FINITE_MAP, ctxt, exp.getLocation(), af);
58:
59:                 ILexNameToken finmap = getUnique("finmap");
60:                 ILexNameToken findex = getUnique("findex");
61:
62:                 // eg. { a |-> b | a:A, b:B & p(a,b) }, gives...
63:                 //
64:                 // exists m:map nat to map A to B &
65:                 // forall a:A, b:B &
66:                 // p(a,b) => exists idx in set dom m &
67:                 // m(idx) = { a |-> b }
68:
69:                 AExistsExp existsExp = new AExistsExp();
70:                 AMapMapType natmaptype = new AMapMapType();
71:                 natmaptype.setFrom(new ANatNumericBasicType());
72:                 natmaptype.setTo(mapType.clone());
73:
74:                 existsExp.setBindList(getMultipleTypeBindList(natmaptype, finmap));
75:                 existsExp.setPredicate(getForallExp(exp.clone(), finmap, findex));
76:
77:                 stitch = existsExp.clone();
78:                 valuetree.setPredicate(ctxt.getPredWithContext(existsExp));
79:         }
80:
81:         /**
82:          * forall a:A, b:B & p(a,b) => exists idx in set dom m & m(idx) = { a |-> b }
83:          */
84:         private PExp getForallExp(AMapCompMapExp exp, ILexNameToken finmap,
85:                         ILexNameToken findex)
86:         {
87:                 AForAllExp forallExp = new AForAllExp();
88:                 forallExp.setBindList(exp.clone().getBindings());
89:                 forallExp.setPredicate(getImpliesExpression(exp, finmap, findex));
90:                 return forallExp;
91:         }
92:
93:         /**
94:          * p(a,b) => exists idx in set dom m & m(idx) = { a |-> b }
95:          */
96:         private PExp getImpliesExpression(AMapCompMapExp exp, ILexNameToken finmap,
97:                         ILexNameToken findex)
98:         {
99:                 if (exp.getPredicate() == null) // Map comprehension has no predicate
100:                 {
101:                         return getImpliesExists(exp, finmap, findex);
102:                 } else
103:                 {
104:                         return AstExpressionFactory.newAImpliesBooleanBinaryExp(exp.getPredicate(), getImpliesExists(exp, finmap, findex));
105:                 }
106:         }
107:
108:         /**
109:          * exists idx in set dom m & m(idx) = { a |-> b }
110:          */
111:         private PExp getImpliesExists(AMapCompMapExp exp, ILexNameToken finmap,
112:                         ILexNameToken findex)
113:         {
114:                 AExistsExp exists = new AExistsExp();
115:                 exists.setBindList(getSetBindList(finmap, findex));
116:                 exists.setPredicate(getExistsPredicate(exp, finmap, findex));
117:                 return exists;
118:         }
119:
120:         /**
121:          * idx in set dom m
122:          */
123:         private List<PMultipleBind> getSetBindList(ILexNameToken finmap,
124:                         ILexNameToken findex)
125:         {
126:                 AMapDomainUnaryExp domExp = new AMapDomainUnaryExp();
127:                 domExp.setType(new ABooleanBasicType());
128:                 domExp.setExp(getVarExp(finmap));
129:                 return getMultipleSetBindList(domExp, findex);
130:         }
131:
132:         /**
133:          * m(idx) = { a |-> b }
134:          */
135:         private PExp getExistsPredicate(AMapCompMapExp exp, ILexNameToken finmap,
136:                         ILexNameToken findex)
137:         {
138:                 AApplyExp apply = getApplyExp(getVarExp(finmap), getVarExp(findex));
139:
140:                 AMapEnumMapExp setEnum = new AMapEnumMapExp();
141:                 List<AMapletExp> members = new Vector<AMapletExp>();
142:                 members.add(exp.getFirst().clone());
143:                 setEnum.setMembers(members);
144:
145:                 return getEqualsExp(apply, setEnum);
146:         }
147: }