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 org.overturetool.vdmj.lex.LexLocation;
27 import org.overturetool.vdmj.pog.POContextStack;
28 import org.overturetool.vdmj.pog.POImpliesContext;
29 import org.overturetool.vdmj.pog.ProofObligationList;
30 import org.overturetool.vdmj.runtime.Context;
31 import org.overturetool.vdmj.runtime.ValueException;
32 import org.overturetool.vdmj.typechecker.Environment;
33 import org.overturetool.vdmj.typechecker.NameScope;
34 import org.overturetool.vdmj.types.BooleanType;
35 import org.overturetool.vdmj.types.Type;
36 import org.overturetool.vdmj.types.TypeList;
37 import org.overturetool.vdmj.values.Value;
38
39 public class ElseIfExpression extends Expression
40 {
41 private static final long serialVersionUID = 1L;
42 public final Expression elseIfExp;
43 public final Expression thenExp;
44
45 public ElseIfExpression(LexLocation location,
46 Expression elseIfExp, Expression thenExp)
47 {
48 super(location);
49 this.elseIfExp = elseIfExp;
50 this.thenExp = thenExp;
51 }
52
53 @Override
54 public String toString()
55 {
56 return "elseif " + elseIfExp + "\nthen " + thenExp;
57 }
58
59 @Override
60 public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope)
61 {
62 if (!elseIfExp.typeCheck(env, null, scope).isType(BooleanType.class))
63 {
64 report(3086, "Else clause is not a boolean");
65 }
66
67 return thenExp.typeCheck(env, null, scope);
68 }
69
70 @Override
71 public Expression findExpression(int lineno)
72 {
73 Expression found = super.findExpression(lineno);
74 if (found != null) return found;
75
76 return thenExp.findExpression(lineno);
77 }
78
79 @Override
80 public Value eval(Context ctxt)
81 {
82 breakpoint.check(location, ctxt);
83
84 try
85 {
86 return elseIfExp.eval(ctxt).boolValue(ctxt) ? thenExp.eval(ctxt) : null;
87 }
88 catch (ValueException e)
89 {
90 return abort(e);
91 }
92 }
93
94 @Override
95 public ProofObligationList getProofObligations(POContextStack ctxt)
96 {
97 ctxt.push(new POImpliesContext(elseIfExp));
98 ProofObligationList obligations = thenExp.getProofObligations(ctxt);
99 ctxt.pop();
100
101 return obligations;
102 }
103
104 @Override
105 public String kind()
106 {
107 return "elseif";
108 }
109 }