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.LexToken;
27 import org.overturetool.vdmj.pog.POContextStack;
28 import org.overturetool.vdmj.pog.ProofObligationList;
29 import org.overturetool.vdmj.pog.SeqModificationObligation;
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.MapType;
35 import org.overturetool.vdmj.types.NumericType;
36 import org.overturetool.vdmj.types.SeqType;
37 import org.overturetool.vdmj.types.Type;
38 import org.overturetool.vdmj.types.TypeList;
39 import org.overturetool.vdmj.types.TypeSet;
40 import org.overturetool.vdmj.types.UnknownType;
41 import org.overturetool.vdmj.values.MapValue;
42 import org.overturetool.vdmj.values.SeqValue;
43 import org.overturetool.vdmj.values.Value;
44 import org.overturetool.vdmj.values.ValueList;
45 import org.overturetool.vdmj.values.ValueMap;
46
47 public class PlusPlusExpression extends BinaryExpression
48 {
49 private static final long serialVersionUID = 1L;
50
51 public PlusPlusExpression(Expression left, LexToken op, Expression right)
52 {
53 super(left, op, right);
54 }
55
56 @Override
57 public Type typeCheck(Environment env, TypeList qualifiers, NameScope scope)
58 {
59 ltype = left.typeCheck(env, null, scope);
60 rtype = right.typeCheck(env, null, scope);
61
62 TypeSet result = new TypeSet();
63 boolean unique = (!ltype.isUnion() && !rtype.isUnion());
64
65 if (ltype.isMap())
66 {
67 if (!rtype.isMap())
68 {
69 concern(unique, 3141, "Right hand of '++' is not a map");
70 detail(unique, "Type", rtype);
71 return new MapType(location);
72 }
73
74 MapType lm = ltype.getMap();
75 MapType rm = rtype.getMap();
76
77 TypeSet domain = new TypeSet(lm.from, rm.from);
78 TypeSet range = new TypeSet(lm.to, rm.to);
79
80 result.add(new MapType(location,
81 domain.getType(location), range.getType(location)));
82 }
83
84 if (ltype.isSeq())
85 {
86 SeqType st = ltype.getSeq();
87
88 if (!rtype.isMap())
89 {
90 concern(unique, 3142, "Right hand of '++' is not a map");
91 detail(unique, "Type", rtype);
92 }
93 else
94 {
95 MapType mr = rtype.getMap();
96
97 if (!mr.from.isType(NumericType.class))
98 {
99 concern(unique, 3143, "Domain of right hand of '++' must be nat1");
100 detail(unique, "Type", mr.from);
101 }
102 }
103
104 result.add(st);
105 }
106
107 if (result.isEmpty())
108 {
109 report(3144, "Left of '++' is neither a map nor a sequence");
110 return new UnknownType(location);
111 }
112
113 return result.getType(location);
114 }
115
116 @Override
117 public Value eval(Context ctxt)
118 {
119 breakpoint.check(location, ctxt);
120
121 try
122 {
123 Value lv = left.eval(ctxt).deref();
124 Value rv = right.eval(ctxt);
125
126 if (lv instanceof MapValue)
127 {
128 ValueMap lm = new ValueMap(lv.mapValue(ctxt));
129 ValueMap rm = rv.mapValue(ctxt);
130
131 for (Value k: rm.keySet())
132 {
133 lm.put(k, rm.get(k));
134 }
135
136 return new MapValue(lm);
137 }
138 else
139 {
140 ValueList seq = lv.seqValue(ctxt);
141 ValueMap map = rv.mapValue(ctxt);
142 ValueList result = new ValueList(seq);
143
144 for (Value k: map.keySet())
145 {
146 int iv = (int)k.intValue(ctxt);
147
148 if (iv < 1 || iv > seq.size())
149 {
150 abort(4025, "Map key not within sequence index range: " + k, ctxt);
151 }
152
153 result.set(iv-1, map.get(k));
154 }
155
156 return new SeqValue(result);
157 }
158 }
159 catch (ValueException e)
160 {
161 return abort(e);
162 }
163 }
164
165 @Override
166 public ProofObligationList getProofObligations(POContextStack ctxt)
167 {
168 ProofObligationList obligations = super.getProofObligations(ctxt);
169
170 if (ltype.isSeq())
171 {
172 obligations.add(new SeqModificationObligation(this, ctxt));
173 }
174
175 return obligations;
176 }
177
178 @Override
179 public String kind()
180 {
181 return "++";
182 }
183 }