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.overturetool.vdmj.expressions;
25
26 import java.util.List;
27
28 import org.overturetool.vdmj.lex.LexLocation;
29 import org.overturetool.vdmj.pog.CasesExhaustiveObligation;
30 import org.overturetool.vdmj.pog.POContextStack;
31 import org.overturetool.vdmj.pog.ProofObligationList;
32 import org.overturetool.vdmj.runtime.Context;
33 import org.overturetool.vdmj.typechecker.Environment;
34 import org.overturetool.vdmj.typechecker.NameScope;
35 import org.overturetool.vdmj.types.Type;
36 import org.overturetool.vdmj.types.TypeList;
37 import org.overturetool.vdmj.types.TypeSet;
38 import org.overturetool.vdmj.util.Utils;
39 import org.overturetool.vdmj.values.Value;
40
41
42 public class CasesExpression extends Expression
43 {
44 private static final long serialVersionUID = 1L;
45 public final Expression exp;
46 public final List<CaseAlternative> cases;
47 public final Expression others;
48 public Type expType = null;
49
50 public CasesExpression(LexLocation location, Expression exp,
51 List<CaseAlternative> cases, Expression others)
52 {
53 super(location);
54 this.exp = exp;
55 this.cases = cases;
56 this.others = others;
57 }
58
59 @Override
60 public String toString()
61 {
62 return "(cases " + exp + " :\n" +
63 Utils.listToString("", cases, ",\n", "") +
64 (others == null ? "\n" : "others " + others + "\n") + "end)";
65 }
66
67 @Override
68 public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope)
69 {
70 expType = exp.typeCheck(env, null, scope);
71 TypeSet rtypes = new TypeSet();
72
73 for (CaseAlternative c: cases)
74 {
75 rtypes.add(c.typeCheck(env, scope, expType));
76 }
77
78 if (others != null)
79 {
80 rtypes.add(others.typeCheck(env, null, scope));
81 }
82
83 return rtypes.getType(location);
84 }
85
86 @Override
87 public Expression findExpression(int lineno)
88 {
89 Expression found = super.findExpression(lineno);
90 if (found != null) return found;
91
92 found = exp.findExpression(lineno);
93 if (found != null) return found;
94
95 for (CaseAlternative c: cases)
96 {
97 found = c.result.findExpression(lineno);
98 if (found != null) break;
99 }
100
101 return others != null ? others.findExpression(lineno) : null;
102 }
103
104 @Override
105 public Value eval(Context ctxt)
106 {
107 breakpoint.check(location, ctxt);
108
109 Value val = exp.eval(ctxt);
110
111 for (CaseAlternative c: cases)
112 {
113 Value rv = c.eval(val, ctxt);
114 if (rv != null) return rv;
115 }
116
117 if (others != null)
118 {
119 return others.eval(ctxt);
120 }
121
122 return abort(4004, "No cases apply for " + val, ctxt);
123 }
124
125 @Override
126 public ProofObligationList getProofObligations(POContextStack ctxt)
127 {
128 ProofObligationList obligations = new ProofObligationList();
129 int pop = 0;
130
131 for (CaseAlternative alt: cases)
132 {
133 obligations.addAll(alt.getProofObligations(ctxt, expType));
134 pop += alt.plist.size();
135 }
136
137 if (others != null)
138 {
139 obligations.addAll(others.getProofObligations(ctxt));
140 }
141
142 for (int i=0; i<pop; i++)
143 {
144 ctxt.pop();
145 }
146
147 if (others == null)
148 {
149 obligations.add(new CasesExhaustiveObligation(this, ctxt));
150 }
151
152 return obligations;
153 }
154
155 @Override
156 public String kind()
157 {
158 return "cases";
159 }
160 }