Method: alt2Exp(ACaseAlternative, ACasesExp, 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.LinkedList;
27: import java.util.List;
28:
29: import org.overture.ast.analysis.AnalysisException;
30: import org.overture.ast.expressions.ACaseAlternative;
31: import org.overture.ast.expressions.ACasesExp;
32: import org.overture.ast.expressions.AEqualsBinaryExp;
33: import org.overture.ast.expressions.AExistsExp;
34: import org.overture.ast.expressions.AOrBooleanBinaryExp;
35: import org.overture.ast.expressions.PExp;
36: import org.overture.ast.factory.AstExpressionFactory;
37: import org.overture.ast.patterns.ATypeMultipleBind;
38: import org.overture.ast.patterns.PMultipleBind;
39: import org.overture.ast.patterns.PPattern;
40: import org.overture.pog.pub.IPOContextStack;
41: import org.overture.pog.pub.IPogAssistantFactory;
42: import org.overture.pog.pub.POType;
43:
44: public class CasesExhaustiveObligation extends ProofObligation
45: {
46:         /**
47:          * VDM bit: cases x: a -> .... default -> ... yields PO: x = a or (exists default : X & x = default)
48:          */
49:         private static final long serialVersionUID = -2266396606434510800L;
50:
51:         // gkanos: Added parameter for the use of assistant.
52:         public CasesExhaustiveObligation(ACasesExp exp, IPOContextStack ctxt,
53:                         IPogAssistantFactory assistantFactory) throws AnalysisException
54:         {
55:                 super(exp, POType.CASES_EXHAUSTIVE, ctxt, exp.getLocation(), assistantFactory);
56:
57:                 PExp initialExp = alt2Exp(exp.getCases().getFirst(), exp, assistantFactory);
58:                 List<ACaseAlternative> initialCases = new LinkedList<ACaseAlternative>(exp.getCases());
59:                 initialCases.remove(0);
60:
61:                 PExp pred = recOnExp(exp.clone(), initialCases, initialExp, assistantFactory);
62:
63:                 stitch = pred.clone();
64:                 valuetree.setPredicate(ctxt.getPredWithContext(pred));
65:         }
66:
67:         private PExp recOnExp(ACasesExp exp, List<ACaseAlternative> cases, PExp r,
68:                         IPogAssistantFactory assistantFactory) throws AnalysisException
69:         {
70:                 if (cases.isEmpty())
71:                 {
72:                         return r;
73:                 }
74:
75:                 AOrBooleanBinaryExp orExp = AstExpressionFactory.newAOrBooleanBinaryExp(r, alt2Exp(cases.get(0), exp.clone(), assistantFactory));
76:
77:                 List<ACaseAlternative> newCases = new LinkedList<ACaseAlternative>(cases);
78:                 newCases.remove(0);
79:
80:                 return recOnExp(exp, newCases, orExp, assistantFactory);
81:         }
82:
83:         private PExp alt2Exp(ACaseAlternative alt, ACasesExp exp,
84:                         IPogAssistantFactory assistantFactory) throws AnalysisException
85:         {
86:•                if (assistantFactory.createPPatternAssistant(null).isSimple(alt.getPattern()))
87:                 {
88:                         AEqualsBinaryExp equalsExp = AstExpressionFactory.newAEqualsBinaryExp(exp.getExpression().clone(), patternToExp(alt.getPattern().clone()));
89:                         return equalsExp;
90:                 } else
91:                 {
92:                         PExp matching = patternToExp(alt.getPattern().clone());
93:
94:                         AExistsExp existsExp = new AExistsExp();
95:
96:                         ATypeMultipleBind tbind = new ATypeMultipleBind();
97:                         List<PPattern> plist = new LinkedList<PPattern>();
98:                         plist.add(alt.getPattern().clone());
99:                         tbind.setPlist(plist);
100:                         tbind.setType(exp.getExpression().getType().clone());
101:                         List<PMultipleBind> bindList = new LinkedList<PMultipleBind>();
102:                         bindList.add(tbind);
103:                         existsExp.setBindList(bindList);
104:
105:                         AEqualsBinaryExp equalsExp = AstExpressionFactory.newAEqualsBinaryExp(exp.getExpression().clone(), matching);
106:                         existsExp.setPredicate(equalsExp);
107:
108:                         return existsExp;
109:                 }
110:         }
111:
112: };