Method: ParameterPatternObligation(AExplicitFunctionDefinition, IPOContextStack, IPogAssistantFactory)

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.HashSet;
27: import java.util.Iterator;
28: import java.util.LinkedList;
29: import java.util.List;
30: import java.util.Set;
31: import java.util.Vector;
32:
33: import org.overture.ast.analysis.AnalysisException;
34: import org.overture.ast.definitions.AExplicitFunctionDefinition;
35: import org.overture.ast.definitions.AExplicitOperationDefinition;
36: import org.overture.ast.definitions.AImplicitFunctionDefinition;
37: import org.overture.ast.definitions.AImplicitOperationDefinition;
38: import org.overture.ast.definitions.PDefinition;
39: import org.overture.ast.expressions.AEqualsBinaryExp;
40: import org.overture.ast.expressions.AExistsExp;
41: import org.overture.ast.expressions.AForAllExp;
42: import org.overture.ast.expressions.AImpliesBooleanBinaryExp;
43: import org.overture.ast.expressions.PExp;
44: import org.overture.ast.factory.AstExpressionFactory;
45: import org.overture.ast.intf.lex.ILexNameToken;
46: import org.overture.ast.patterns.PMultipleBind;
47: import org.overture.ast.patterns.PPattern;
48: import org.overture.ast.typechecker.NameScope;
49: import org.overture.ast.types.AFunctionType;
50: import org.overture.ast.types.AOperationType;
51: import org.overture.ast.types.PType;
52: import org.overture.pog.pub.IPOContextStack;
53: import org.overture.pog.pub.IPogAssistantFactory;
54: import org.overture.pog.pub.POType;
55:
56: public class ParameterPatternObligation extends ProofObligation
57: {
58:         private static final long serialVersionUID = 6831031423902894299L;
59:
60:         public IPogAssistantFactory assistantFactory; // gkanos:variable added by me to pass it as param to the method
61:                                                                                                         // generate.
62:
63:         public ParameterPatternObligation(AExplicitFunctionDefinition def,
64:                         IPOContextStack ctxt, IPogAssistantFactory af)
65:                         throws AnalysisException
66:         {
67:                 super(def, POType.FUNC_PATTERNS, ctxt, def.getLocation(), af);
68:                 this.assistantFactory = af;
69:                 // valuetree.setContext(ctxt.getContextNodeList());
70:                 // cannot clone getPredef as it can be null. We protect the ast in
71:                 // the generate method where it's used
72:                 stitch = generate(def.getPredef(), cloneListPatternList(def.getParamPatternList()), cloneListType(((AFunctionType) def.getType()).getParameters()), ((AFunctionType) def.getType()).getResult().clone());
73:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
74:         }
75:
76:         public ParameterPatternObligation(AImplicitFunctionDefinition def,
77:                         IPOContextStack ctxt, IPogAssistantFactory af)
78:                         throws AnalysisException
79:         {
80:                 super(def, POType.FUNC_PATTERNS, ctxt, def.getLocation(), af);
81:                 this.assistantFactory = af;
82:
83:                 stitch = generate(def.getPredef(), cloneListPatternList(assistantFactory.createAImplicitFunctionDefinitionAssistant().getParamPatternList(def)), cloneListType(((AFunctionType) def.getType()).getParameters()), ((AFunctionType) def.getType()).getResult().clone());
84:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
85:         }
86:
87:         public ParameterPatternObligation(AExplicitOperationDefinition def,
88:                         IPOContextStack ctxt, IPogAssistantFactory af)
89:                         throws AnalysisException
90:         {
91:                 super(def, POType.OPERATION_PATTERNS, ctxt, def.getLocation(), af);
92:                 this.assistantFactory = af;
93:
94:                 stitch = generate(def.getPredef(), cloneListPatternList(assistantFactory.createAExplicitOperationDefinitionAssistant(null).getParamPatternList(def)), cloneListType(((AOperationType) def.getType()).getParameters()), ((AOperationType) def.getType()).getResult().clone());
95:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
96:         }
97:
98:         public ParameterPatternObligation(AImplicitOperationDefinition def,
99:                         IPOContextStack ctxt, IPogAssistantFactory af)
100:                         throws AnalysisException
101:         {
102:                 super(def, POType.OPERATION_PATTERNS, ctxt, def.getLocation(), af);
103:                 this.assistantFactory = af;
104:
105:                 stitch = generate(def.getPredef(), cloneListPatternList(assistantFactory.createAImplicitOperationDefinitionAssistant().getListParamPatternList(def)), cloneListType(((AOperationType) def.getType()).getParameters()), ((AOperationType) def.getType()).getResult().clone());
106:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
107:         }
108:
109:         private PExp generate(PDefinition predef, List<List<PPattern>> plist,
110:                         List<PType> params, PType result) throws AnalysisException
111:         {
112:                 AForAllExp forallExp = new AForAllExp();
113:                 List<PMultipleBind> forallBindList = new Vector<PMultipleBind>();
114:                 List<PExp> arglist = new Vector<PExp>();
115:                 PExp forallPredicate = null;
116:
117:                 for (List<PPattern> paramList : plist)
118:                 {
119:                         Iterator<PType> titer = params.iterator();
120:
121:                         if (!paramList.isEmpty())
122:                         {
123:                                 AExistsExp existsExp = new AExistsExp();
124:                                 List<PMultipleBind> existsBindList = new Vector<PMultipleBind>();
125:                                 PExp existsPredicate = null;
126:
127:                                 Set<ILexNameToken> previousBindings = new HashSet<ILexNameToken>();
128:
129:                                 for (PPattern param : paramList)
130:                                 {
131:                                         ILexNameToken aname = getUnique("arg");
132:                                         ILexNameToken bname = getUnique("bind");
133:
134:                                         PType atype = titer.next();
135:                                         PExp pmatch = patternToExp(param);
136:                                         arglist.add(pmatch.clone());
137:
138:                                         forallBindList.add(getMultipleTypeBind(atype, aname));
139:                                         existsBindList.add(getMultipleTypeBind(atype, bname));
140:
141:                                         for (PDefinition def : assistantFactory.createPPatternAssistant(null).getDefinitions(param, atype, NameScope.LOCAL))
142:                                         {
143:                                                 if (def.getName() != null
144:                                                                 && !previousBindings.contains(def.getName()))
145:                                                 {
146:                                                         existsBindList.add(getMultipleTypeBind(def.getType(), def.getName()));
147:                                                         previousBindings.add(def.getName());
148:                                                 }
149:                                         }
150:
151:                                         AEqualsBinaryExp eq1 = getEqualsExp(getVarExp(aname), getVarExp(bname));
152:                                         AEqualsBinaryExp eq2 = getEqualsExp(pmatch, getVarExp(bname));
153:                                         existsPredicate = makeAnd(existsPredicate, makeAnd(eq1, eq2));
154:                                 }
155:                                 existsExp.setBindList(existsBindList);
156:                                 existsExp.setPredicate(existsPredicate);
157:
158:                                 forallPredicate = makeAnd(forallPredicate, existsExp);
159:                         }
160:
161:                         if (result instanceof AFunctionType)
162:                         {
163:                                 AFunctionType ft = (AFunctionType) result;
164:                                 result = ft.getResult();
165:                                 params = ft.getParameters();
166:                         } else
167:                         {
168:                                 break;
169:                         }
170:                 }
171:
172:                 forallExp.setBindList(forallBindList);
173:
174:                 if (predef != null)
175:                 {
176:                         AImpliesBooleanBinaryExp implies = AstExpressionFactory.newAImpliesBooleanBinaryExp(getApplyExp(getVarExp(predef.getName().clone()), arglist), forallPredicate);
177:                         forallExp.setPredicate(implies);
178:                 } else
179:                 {
180:                         forallExp.setPredicate(forallPredicate);
181:                 }
182:
183:                 return forallExp;
184:         }
185:
186:         private List<List<PPattern>> cloneListPatternList(List<List<PPattern>> list)
187:         {
188:                 List<List<PPattern>> r = new LinkedList<List<PPattern>>();
189:                 for (List<PPattern> list2 : list)
190:                 {
191:                         r.add(cloneList(list2));
192:                 }
193:                 return r;
194:
195:         }
196:
197:         private List<PPattern> cloneList(List<PPattern> list)
198:         {
199:                 List<PPattern> r = new LinkedList<PPattern>();
200:                 for (PPattern p : list)
201:                 {
202:                         r.add(p);
203:                 }
204:                 return r;
205:         }
206:
207: }