dekker.one
The models, scripts, and results of the benchmarks performed for a Half Reification Journal paper
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Guido Tack <guido.tack@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#include <minizinc/astexception.hh>
13#include <minizinc/astiterator.hh>
14#include <minizinc/flatten_internal.hh>
15#include <minizinc/hash.hh>
16#include <minizinc/prettyprinter.hh>
17#include <minizinc/typecheck.hh>
18
19#include <sstream>
20#include <string>
21#include <unordered_map>
22#include <utility>
23
24namespace MiniZinc {
25
26Scopes::Scopes() { _s.emplace_back(ST_TOPLEVEL); }
27
28void Scopes::add(EnvI& env, VarDecl* vd) {
29 if (!_s.back().toplevel() && vd->ti()->isEnum() && (vd->e() != nullptr)) {
30 throw TypeError(env, vd->loc(), "enums are only allowed at top level");
31 }
32 if (vd->id()->idn() == -1 && vd->id()->v() == "") {
33 return;
34 }
35 // If the current scope is ST_INNER, check if vd shadows another
36 // declaration from the same functional or toplevel scope
37 if (_s.back().st == ST_INNER) {
38 assert(_s.size() > 1); // at least toplevel scope above
39 for (int i = static_cast<int>(_s.size()) - 2; i >= 0; i--) {
40 auto previous = _s[i].m.find(vd->id());
41 if (previous != _s[i].m.end()) {
42 std::ostringstream oss;
43 ASTString warnloc_f = vd->loc().filename();
44 unsigned int warnloc_l = vd->id()->loc().firstLine();
45 unsigned int warnloc_c = vd->id()->loc().firstColumn();
46 unsigned int earlier_l = previous->second->id()->loc().firstLine();
47 unsigned int earlier_c = previous->second->id()->loc().firstColumn();
48 oss << "\n " << warnloc_f << ":" << warnloc_l << "." << warnloc_c << ":\n";
49 oss << " Variable `" << *vd->id() << "' shadows variable with the same name in line "
50 << earlier_l << "." << earlier_c;
51 env.addWarning(oss.str());
52 break;
53 }
54 if (_s[i].st != ST_INNER) {
55 break;
56 }
57 }
58 }
59
60 auto vdi = _s.back().m.find(vd->id());
61 if (vdi == _s.back().m.end()) {
62 _s.back().m.insert(vd->id(), vd);
63 } else {
64 std::ostringstream ss;
65 ss << "identifier `" << vd->id()->str() << "' already defined";
66 throw TypeError(env, vd->loc(), ss.str());
67 }
68}
69
70void Scopes::pushToplevel() { _s.emplace_back(ST_TOPLEVEL); }
71
72void Scopes::pushFun() { _s.emplace_back(ST_FUN); }
73
74void Scopes::push() { _s.emplace_back(ST_INNER); }
75
76void Scopes::pop() { _s.pop_back(); }
77
78VarDecl* Scopes::find(Id* ident) {
79 int cur = static_cast<int>(_s.size()) - 1;
80 for (;;) {
81 auto vdi = _s[cur].m.find(ident);
82 if (vdi == _s[cur].m.end()) {
83 if (_s[cur].toplevel()) {
84 if (cur > 0) {
85 cur = 0;
86 } else {
87 return nullptr;
88 }
89 } else {
90 cur--;
91 }
92 } else {
93 return vdi->second;
94 }
95 }
96}
97
98VarDecl* Scopes::findSimilar(Id* ident) {
99 VarDecl* mostSimilar = nullptr;
100 int cur = static_cast<int>(_s.size()) - 1;
101 int minEdits = 3;
102 for (;;) {
103 for (auto decls : _s[cur].m) {
104 int edits = ident->levenshteinDistance(decls.first);
105 if (edits < minEdits && std::abs(static_cast<int>(ident->v().size()) -
106 static_cast<int>(decls.first->v().size())) <= 3) {
107 minEdits = edits;
108 mostSimilar = decls.second;
109 }
110 }
111 if (_s[cur].toplevel()) {
112 if (cur > 0) {
113 cur = 0;
114 } else {
115 break;
116 }
117 } else {
118 cur--;
119 }
120 }
121 return mostSimilar;
122}
123
124class VarDeclCmp {
125private:
126 std::unordered_map<VarDecl*, int>& _pos;
127
128public:
129 VarDeclCmp(std::unordered_map<VarDecl*, int>& pos) : _pos(pos) {}
130 bool operator()(Expression* e0, Expression* e1) {
131 if (auto* vd0 = Expression::dynamicCast<VarDecl>(e0)) {
132 if (auto* vd1 = Expression::dynamicCast<VarDecl>(e1)) {
133 return _pos[vd0] < _pos[vd1];
134 }
135 return true;
136 }
137 return false;
138 }
139};
140class ItemCmp {
141private:
142 std::unordered_map<VarDecl*, int>& _pos;
143
144public:
145 ItemCmp(std::unordered_map<VarDecl*, int>& pos) : _pos(pos) {}
146 bool operator()(Item* i0, Item* i1) {
147 if (auto* vd0 = i0->cast<VarDeclI>()) {
148 if (auto* vd1 = i1->cast<VarDeclI>()) {
149 return _pos[vd0->e()] < _pos[vd1->e()];
150 }
151 return true;
152 }
153 return false;
154 }
155};
156
157// Create all required mapping functions for a new enum
158// (mapping enum identifiers to strings, and mapping between different enums)
159void create_enum_mapper(EnvI& env, Model* m, unsigned int enumId, VarDecl* vd, Model* enumItems) {
160 GCLock lock;
161
162 Id* ident = vd->id();
163
164 if (vd->e() == nullptr) {
165 // Enum without right hand side (may be supplied later in an assignment
166 // item, or we may be runnint in --model-interface-only mode).
167 // Need to create stub function declarations, so that the type checker
168 // is happy.
169 Type tx = Type::parint();
170 tx.ot(Type::OT_OPTIONAL);
171 auto* ti_aa = new TypeInst(Location().introduce(), tx);
172 auto* vd_aa = new VarDecl(Location().introduce(), ti_aa, "x");
173 vd_aa->toplevel(false);
174
175 auto* ti_ab = new TypeInst(Location().introduce(), Type::parbool());
176 auto* vd_ab = new VarDecl(Location().introduce(), ti_ab, "b");
177 vd_ab->toplevel(false);
178
179 auto* ti_aj = new TypeInst(Location().introduce(), Type::parbool());
180 auto* vd_aj = new VarDecl(Location().introduce(), ti_aj, "json");
181 vd_aj->toplevel(false);
182
183 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
184 std::vector<VarDecl*> fi_params(3);
185 fi_params[0] = vd_aa;
186 fi_params[1] = vd_ab;
187 fi_params[2] = vd_aj;
188 auto* fi =
189 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
190 ti_fi, fi_params, nullptr);
191 enumItems->addItem(fi);
192
193 return;
194 }
195
196 Call* c = vd->e()->dynamicCast<Call>();
197 auto* al = vd->e()->dynamicCast<ArrayLit>();
198
199 std::vector<Expression*> parts;
200 if (vd->e()->isa<SetLit>()) {
201 parts.push_back(vd->e());
202 } else if ((al != nullptr) || ((c != nullptr) && c->id() == "anon_enum" && c->argCount() == 1 &&
203 c->arg(0)->isa<ArrayLit>())) {
204 if (c != nullptr) {
205 al = c->arg(0)->cast<ArrayLit>();
206 }
207 std::vector<Expression*> enumIds(al->size());
208 for (unsigned int i = 0; i < al->size(); i++) {
209 if (Id* eid = (*al)[i]->dynamicCast<Id>()) {
210 enumIds[i] = eid;
211 } else {
212 std::ostringstream ss;
213 ss << "invalid initialisation for enum `" << ident->v() << "'";
214 throw TypeError(env, vd->e()->loc(), ss.str());
215 }
216 }
217 parts.push_back(new SetLit(vd->e()->loc(), enumIds));
218 } else if (c != nullptr) {
219 if (c->id() == "enumFromConstructors") {
220 if (c->argCount() != 1 || !c->arg(0)->isa<ArrayLit>()) {
221 throw TypeError(env, c->loc(),
222 "enumFromConstructors used with incorrect argument type (only supports "
223 "array literals)");
224 }
225 auto* al = c->arg(0)->cast<ArrayLit>();
226 for (unsigned int i = 0; i < al->size(); i++) {
227 parts.push_back((*al)[i]);
228 }
229 } else {
230 parts.push_back(c);
231 }
232 } else {
233 throw TypeError(env, vd->e()->loc(),
234 std::string("invalid initialisation for enum `") + ident->v().c_str() + "'");
235 }
236
237 std::vector<Expression*> partCardinality;
238 for (unsigned int p = 0; p < parts.size(); p++) {
239 if (auto* sl = parts[p]->dynamicCast<SetLit>()) {
240 for (unsigned int i = 0; i < sl->v().size(); i++) {
241 if (!sl->v()[i]->isa<Id>()) {
242 throw TypeError(
243 env, sl->v()[i]->loc(),
244 std::string("invalid initialisation for enum `") + ident->v().c_str() + "'");
245 }
246 auto* ti_id = new TypeInst(sl->v()[i]->loc(), Type::parenum(enumId));
247
248 std::vector<Expression*> toEnumArgs(2);
249 toEnumArgs[0] = vd->id();
250 if (partCardinality.empty()) {
251 toEnumArgs[1] = IntLit::a(i + 1);
252 } else {
253 toEnumArgs[1] =
254 new BinOp(Location().introduce(), partCardinality.back(), BOT_PLUS, IntLit::a(i + 1));
255 }
256 Call* toEnum = new Call(sl->v()[i]->loc(), ASTString("to_enum"), toEnumArgs);
257 auto* vd_id = new VarDecl(ti_id->loc(), ti_id, sl->v()[i]->cast<Id>()->str(), toEnum);
258 auto* vdi_id = new VarDeclI(vd_id->loc(), vd_id);
259 std::string str(sl->v()[i]->cast<Id>()->str().c_str());
260 env.reverseEnum[str] = vdi_id;
261 enumItems->addItem(vdi_id);
262 if (i == sl->v().size() - 1) {
263 // remember the last identifier
264 partCardinality.push_back(toEnumArgs[1]);
265 }
266 }
267
268 std::string name =
269 create_enum_to_string_name(ident, "_enum_to_string_" + std::to_string(p) + "_");
270 std::vector<Expression*> al_args(sl->v().size());
271 for (unsigned int i = 0; i < sl->v().size(); i++) {
272 std::string str(sl->v()[i]->cast<Id>()->str().c_str());
273 if (str.size() >= 2 && str[0] == '\'' && str[str.size() - 1] == '\'') {
274 al_args[i] =
275 new StringLit(Location().introduce(), ASTString(str.substr(1, str.size() - 2)));
276 } else {
277 al_args[i] = new StringLit(Location().introduce(), ASTString(str));
278 }
279 /// TODO: reimplement reverseEnum with a symbol table into the model (so you can evalPar an
280 /// expression)
281 }
282 auto* al = new ArrayLit(Location().introduce(), al_args);
283
284 std::vector<TypeInst*> ranges(1);
285 ranges[0] = new TypeInst(Location().introduce(), Type::parint());
286 auto* ti = new TypeInst(Location().introduce(), Type::parstring(1));
287 ti->setRanges(ranges);
288 auto* vd_enumToString = new VarDecl(Location().introduce(), ti, name, al);
289 enumItems->addItem(new VarDeclI(Location().introduce(), vd_enumToString));
290
291 Type tx = Type::parint();
292 tx.ot(Type::OT_OPTIONAL);
293 auto* ti_aa = new TypeInst(Location().introduce(), tx);
294 auto* vd_aa = new VarDecl(Location().introduce(), ti_aa, "x");
295 vd_aa->toplevel(false);
296 auto* ti_ab = new TypeInst(Location().introduce(), Type::parbool());
297 auto* vd_ab = new VarDecl(Location().introduce(), ti_ab, "b");
298 vd_ab->toplevel(false);
299 auto* ti_aj = new TypeInst(Location().introduce(), Type::parbool());
300 auto* vd_aj = new VarDecl(Location().introduce(), ti_aj, "json");
301 vd_aj->toplevel(false);
302 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
303 std::vector<VarDecl*> fi_params(3);
304 fi_params[0] = vd_aa;
305 fi_params[1] = vd_ab;
306 fi_params[2] = vd_aj;
307
308 std::vector<Expression*> deopt_args(1);
309 deopt_args[0] = vd_aa->id();
310 Call* deopt = new Call(Location().introduce(), "deopt", deopt_args);
311 Call* occurs = new Call(Location().introduce(), "occurs", deopt_args);
312 std::vector<Expression*> aa_args(1);
313 aa_args[0] = deopt;
314 auto* aa = new ArrayAccess(Location().introduce(), vd_enumToString->id(), aa_args);
315
316 auto* sl_absent = new StringLit(Location().introduce(), "<>");
317
318 ITE* if_absent = new ITE(
319 Location().introduce(),
320 {vd_aj->id(), new StringLit(Location().introduce(), ASTString("null"))}, sl_absent);
321
322 auto* json_e_quote = new StringLit(Location().introduce(), ASTString("{\"e\":\""));
323 auto* json_e_quote_end = new StringLit(Location().introduce(), ASTString("\"}"));
324 auto* quote_aa = new BinOp(Location().introduce(), json_e_quote, BOT_PLUSPLUS, aa);
325 auto* quote_aa2 = new BinOp(Location().introduce(), quote_aa, BOT_PLUSPLUS, json_e_quote_end);
326
327 Call* quote_dzn = new Call(Location().introduce(), ASTString("showDznId"), {aa});
328
329 std::vector<Expression*> ite_ifelse(2);
330 ite_ifelse[0] = occurs;
331 ite_ifelse[1] =
332 new ITE(Location().introduce(), {vd_ab->id(), quote_dzn, vd_aj->id(), quote_aa2}, aa);
333
334 ITE* ite = new ITE(Location().introduce(), ite_ifelse, if_absent);
335
336 std::string toString = "_toString_";
337 if (parts.size() > 1) {
338 toString += std::to_string(p) + "_";
339 }
340
341 auto* fi = new FunctionI(Location().introduce(), create_enum_to_string_name(ident, toString),
342 ti_fi, fi_params, ite);
343 enumItems->addItem(fi);
344 } else if (Call* c = parts[p]->dynamicCast<Call>()) {
345 if (c->id() == "anon_enum") {
346 Type tx = Type::parint();
347 tx.ot(Type::OT_OPTIONAL);
348 auto* ti_aa = new TypeInst(Location().introduce(), tx);
349 auto* vd_aa = new VarDecl(Location().introduce(), ti_aa, "x");
350 vd_aa->toplevel(false);
351
352 auto* ti_ab = new TypeInst(Location().introduce(), Type::parbool());
353 auto* vd_ab = new VarDecl(Location().introduce(), ti_ab, "b");
354 vd_ab->toplevel(false);
355
356 auto* ti_aj = new TypeInst(Location().introduce(), Type::parbool());
357 auto* vd_aj = new VarDecl(Location().introduce(), ti_aj, "json");
358 vd_aj->toplevel(false);
359
360 std::vector<Expression*> deopt_args(1);
361 deopt_args[0] = vd_aa->id();
362 Call* deopt = new Call(Location().introduce(), "deopt", deopt_args);
363 Call* if_absent = new Call(Location().introduce(), "absent", deopt_args);
364 auto* sl_absent_dzn = new StringLit(Location().introduce(), "<>");
365 ITE* sl_absent = new ITE(
366 Location().introduce(),
367 {vd_aj->id(), new StringLit(Location().introduce(), ASTString("null"))}, sl_absent_dzn);
368
369 auto* sl_dzn = new StringLit(Location().introduce(), ASTString(std::string("to_enum(") +
370 ident->str().c_str() + ","));
371
372 std::vector<Expression*> showIntArgs(1);
373 if (partCardinality.empty()) {
374 showIntArgs[0] = deopt;
375 partCardinality.push_back(c->arg(0));
376 } else {
377 showIntArgs[0] =
378 new BinOp(Location().introduce(), partCardinality.back(), BOT_PLUS, deopt);
379 partCardinality.push_back(
380 new BinOp(Location().introduce(), partCardinality.back(), BOT_PLUS, c->arg(0)));
381 }
382
383 Call* showInt = new Call(Location().introduce(), constants().ids.show, showIntArgs);
384 auto* construct_string_dzn =
385 new BinOp(Location().introduce(), sl_dzn, BOT_PLUSPLUS, showInt);
386 auto* closing_bracket = new StringLit(Location().introduce(), ASTString(")"));
387 auto* construct_string_dzn_2 =
388 new BinOp(Location().introduce(), construct_string_dzn, BOT_PLUSPLUS, closing_bracket);
389
390 auto* sl = new StringLit(Location().introduce(),
391 ASTString(std::string(ident->str().c_str()) + "_"));
392 auto* construct_string = new BinOp(Location().introduce(), sl, BOT_PLUSPLUS, showInt);
393
394 auto* json_e_quote = new StringLit(Location().introduce(), ASTString("{\"e\":\""));
395 auto* json_e_quote_mid = new StringLit(Location().introduce(), ASTString("\", \"i\":"));
396 auto* json_e_quote_end = new StringLit(Location().introduce(), ASTString("}"));
397 auto* construct_string_json =
398 new BinOp(Location().introduce(), json_e_quote, BOT_PLUSPLUS,
399 new StringLit(Location().introduce(), ident->str()));
400 auto* construct_string_json_1a = new BinOp(Location().introduce(), construct_string_json,
401 BOT_PLUSPLUS, json_e_quote_mid);
402 auto* construct_string_json_1b =
403 new BinOp(Location().introduce(), construct_string_json_1a, BOT_PLUSPLUS, showInt);
404 auto* construct_string_json_2 = new BinOp(Location().introduce(), construct_string_json_1b,
405 BOT_PLUSPLUS, json_e_quote_end);
406
407 std::vector<Expression*> if_then(6);
408 if_then[0] = if_absent;
409 if_then[1] = sl_absent;
410 if_then[2] = vd_ab->id();
411 if_then[3] = construct_string_dzn_2;
412 if_then[4] = vd_aj->id();
413 if_then[5] = construct_string_json_2;
414 ITE* ite = new ITE(Location().introduce(), if_then, construct_string);
415
416 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
417 std::vector<VarDecl*> fi_params(3);
418 fi_params[0] = vd_aa;
419 fi_params[1] = vd_ab;
420 fi_params[2] = vd_aj;
421 std::string toString = "_toString_";
422 if (parts.size() > 1) {
423 toString += std::to_string(p) + "_";
424 }
425
426 auto* fi =
427 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, toString),
428 ti_fi, fi_params, ite);
429 enumItems->addItem(fi);
430 } else {
431 // This is an enum constructor C(E)
432
433 if (c->argCount() != 1 || !c->arg(0)->isa<Id>()) {
434 throw TypeError(env, c->loc(),
435 "enum constructors must have a single identifier as argument");
436 }
437 Id* otherEnumId = c->arg(0)->cast<Id>();
438
439 // Generate:
440 /*
441 function X: C(E: x) = to_enum(X,partCardinality.back()+x)
442 function var X: C(var E: x) = to_enum(X,partCardinality.back()+x)
443 function opt X: C(opt E: x) = if occurs(x) then C(deopt(x)) else to_enum(x,<>) endif
444 function var opt X: C(var opt E: x) = if occurs(x) then C(deopt(x)) else to_enum(x,<>)
445 endif
446 function set of X: C(set of E: x) = { C(i) | i in x }
447 function var set of X: C(var set of E: x) = { C(i) | i in x }
448 */
449 {
450 Type Xt = Type::parint();
451 Xt.enumId(enumId);
452 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt);
453 auto* Cfn_x_ti = new TypeInst(Location().introduce(), Type(), otherEnumId);
454 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
455 vd_x->toplevel(false);
456 Expression* realX;
457 if (partCardinality.empty()) {
458 realX = vd_x->id();
459 } else {
460 realX = new BinOp(Location().introduce(), partCardinality.back(), BOT_PLUS, vd_x->id());
461 }
462 auto* Cfn_body = new Call(Location().introduce(), "to_enum", {vd->id(), realX});
463
464 std::string Cfn_id(c->id().c_str());
465 auto* Cfn = new FunctionI(Location().introduce(), Cfn_id, Cfn_ti, {vd_x}, Cfn_body);
466 env.reverseEnum[Cfn_id] = Cfn;
467 enumItems->addItem(Cfn);
468 }
469 {
470 Type Xt = Type::varint();
471 Xt.enumId(enumId);
472 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt);
473 Type argT;
474 argT.ti(Type::TI_VAR);
475 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, otherEnumId);
476 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
477 vd_x->toplevel(false);
478 Expression* realX;
479 if (partCardinality.empty()) {
480 realX = vd_x->id();
481 } else {
482 realX = new BinOp(Location().introduce(), partCardinality.back(), BOT_PLUS, vd_x->id());
483 }
484 auto* Cfn_body = new Call(Location().introduce(), "to_enum", {vd->id(), realX});
485
486 std::string Cfn_id(c->id().c_str());
487 auto* Cfn = new FunctionI(Location().introduce(), Cfn_id, Cfn_ti, {vd_x}, Cfn_body);
488 enumItems->addItem(Cfn);
489 }
490 {
491 Type Xt = Type::parint();
492 Xt.ot(Type::OT_OPTIONAL);
493 Xt.enumId(enumId);
494 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt);
495 Type argT;
496 argT.ot(Type::OT_OPTIONAL);
497 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, otherEnumId);
498 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
499 std::string Cfn_id(c->id().c_str());
500 vd_x->toplevel(false);
501 auto* occurs = new Call(Location().introduce(), "occurs", {vd_x->id()});
502 auto* deopt = new Call(Location().introduce(), "deopt", {vd_x->id()});
503 auto* inv = new Call(Location().introduce(), Cfn_id, {deopt});
504 auto* toEnumAbsent =
505 new Call(Location().introduce(), "to_enum", {vd->id(), constants().absent});
506 auto* ite = new ITE(Location().introduce(), {occurs, inv}, toEnumAbsent);
507 auto* Cfn = new FunctionI(Location().introduce(), Cfn_id, Cfn_ti, {vd_x}, ite);
508 enumItems->addItem(Cfn);
509 }
510 {
511 Type Xt = Type::varint();
512 Xt.ot(Type::OT_OPTIONAL);
513 Xt.enumId(enumId);
514 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt);
515 Type argT;
516 argT.ti(Type::TI_VAR);
517 argT.ot(Type::OT_OPTIONAL);
518 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, otherEnumId);
519 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
520 std::string Cfn_id(c->id().c_str());
521 vd_x->toplevel(false);
522 auto* occurs = new Call(Location().introduce(), "occurs", {vd_x->id()});
523 auto* deopt = new Call(Location().introduce(), "deopt", {vd_x->id()});
524 auto* toEnumAbsent =
525 new Call(Location().introduce(), "to_enum", {vd->id(), constants().absent});
526 auto* inv = new Call(Location().introduce(), Cfn_id, {deopt});
527 auto* ite = new ITE(Location().introduce(), {occurs, inv}, toEnumAbsent);
528 auto* Cfn = new FunctionI(Location().introduce(), Cfn_id, Cfn_ti, {vd_x}, ite);
529 enumItems->addItem(Cfn);
530 }
531 {
532 Type Xt = Type::parint();
533 Xt.st(Type::ST_SET);
534 Xt.enumId(enumId);
535 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt);
536 Type argT;
537 argT.st(Type::ST_SET);
538 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, otherEnumId);
539 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
540 std::string Cfn_id(c->id().c_str());
541 vd_x->toplevel(false);
542 auto* s_ti = new TypeInst(Location().introduce(), Type::parint());
543 auto* s = new VarDecl(Location().introduce(), s_ti, "s", nullptr);
544 s->toplevel(false);
545 auto* inv = new Call(Location().introduce(), Cfn_id, {s->id()});
546 Generator gen({s}, vd_x->id(), nullptr);
547 Generators gens;
548 gens.g = {gen};
549 auto* comprehension = new Comprehension(Location().introduce(), inv, gens, true);
550 auto* Cfn = new FunctionI(Location().introduce(), Cfn_id, Cfn_ti, {vd_x}, comprehension);
551 enumItems->addItem(Cfn);
552 }
553 {
554 Type Xt = Type::varint();
555 Xt.st(Type::ST_SET);
556 Xt.enumId(enumId);
557 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt);
558 Type argT;
559 argT.ti(Type::TI_VAR);
560 argT.st(Type::ST_SET);
561 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, otherEnumId);
562 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
563 std::string Cfn_id(c->id().c_str());
564 vd_x->toplevel(false);
565 auto* s_ti = new TypeInst(Location().introduce(), Type::parint());
566 auto* s = new VarDecl(Location().introduce(), s_ti, "s", nullptr);
567 s->toplevel(false);
568 auto* inv = new Call(Location().introduce(), Cfn_id, {s->id()});
569 Generator gen({s}, vd_x->id(), nullptr);
570 Generators gens;
571 gens.g = {gen};
572 auto* comprehension = new Comprehension(Location().introduce(), inv, gens, true);
573 auto* Cfn = new FunctionI(Location().introduce(), Cfn_id, Cfn_ti, {vd_x}, comprehension);
574 enumItems->addItem(Cfn);
575 }
576 /*
577 function E: C⁻¹(X: x) = to_enum(E,x-partCardinality.back())
578 function var E: C⁻¹(var X: x) = to_enum(E,x-partCardinality.back())
579 function opt E: C⁻¹(opt X: x) = if occurs(x) then C⁻¹(deopt(x)) else to_enum(x,<>) endif
580 function var opt E: C⁻¹(var opt X: x) = if occurs(x) then C⁻¹(deopt(x)) else to_enum(x,<>)
581 endif
582 function set of E: C⁻¹(set of X: x) = { C⁻¹(i) | i in x }
583 function var set of E: C⁻¹(var set of X: x) = { C⁻¹(i) | i in x }
584 */
585 {
586 auto* toEfn_ti = new TypeInst(Location().introduce(), Type(), otherEnumId);
587 Type Xt = Type::parint();
588 Xt.enumId(enumId);
589 auto* toEfn_x_ti = new TypeInst(Location().introduce(), Xt, vd->id());
590 auto* vd_x = new VarDecl(Location().introduce(), toEfn_x_ti, "x");
591 vd_x->toplevel(false);
592 Expression* realX;
593 if (partCardinality.empty()) {
594 realX = vd_x->id();
595 } else {
596 realX =
597 new BinOp(Location().introduce(), vd_x->id(), BOT_MINUS, partCardinality.back());
598 }
599 auto* toEfn_body = new Call(Location().introduce(), "to_enum", {otherEnumId, realX});
600
601 std::string Cinv_id(std::string(c->id().c_str()) + "⁻¹");
602 auto* toEfn =
603 new FunctionI(Location().introduce(), Cinv_id, toEfn_ti, {vd_x}, toEfn_body);
604 enumItems->addItem(toEfn);
605 }
606 {
607 Type rT;
608 rT.ti(Type::TI_VAR);
609 auto* toEfn_ti = new TypeInst(Location().introduce(), rT, otherEnumId);
610 Type Xt = Type::varint();
611 Xt.enumId(enumId);
612 auto* toEfn_x_ti = new TypeInst(Location().introduce(), Xt, vd->id());
613 auto* vd_x = new VarDecl(Location().introduce(), toEfn_x_ti, "x");
614 vd_x->toplevel(false);
615 Expression* realX;
616 if (partCardinality.empty()) {
617 realX = vd_x->id();
618 } else {
619 realX =
620 new BinOp(Location().introduce(), vd_x->id(), BOT_MINUS, partCardinality.back());
621 }
622 auto* toEfn_body = new Call(Location().introduce(), "to_enum", {otherEnumId, realX});
623
624 std::string Cinv_id(std::string(c->id().c_str()) + "⁻¹");
625 auto* toEfn =
626 new FunctionI(Location().introduce(), Cinv_id, toEfn_ti, {vd_x}, toEfn_body);
627 enumItems->addItem(toEfn);
628 }
629 {
630 Type rt;
631 rt.ot(Type::OT_OPTIONAL);
632 auto* Cfn_ti = new TypeInst(Location().introduce(), rt, otherEnumId);
633 Type argT;
634 argT.ot(Type::OT_OPTIONAL);
635 argT.enumId(enumId);
636 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, vd->id());
637 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
638 std::string Cinv_id(std::string(c->id().c_str()) + "⁻¹");
639 vd_x->toplevel(false);
640 auto* occurs = new Call(Location().introduce(), "occurs", {vd_x->id()});
641 auto* deopt = new Call(Location().introduce(), "deopt", {vd_x->id()});
642 auto* inv = new Call(Location().introduce(), Cinv_id, {deopt});
643 auto* toEnumAbsent =
644 new Call(Location().introduce(), "to_enum", {otherEnumId, constants().absent});
645 auto* ite = new ITE(Location().introduce(), {occurs, inv}, toEnumAbsent);
646 auto* Cfn = new FunctionI(Location().introduce(), Cinv_id, Cfn_ti, {vd_x}, ite);
647 enumItems->addItem(Cfn);
648 }
649 {
650 Type rt;
651 rt.ti(Type::TI_VAR);
652 rt.ot(Type::OT_OPTIONAL);
653 auto* Cfn_ti = new TypeInst(Location().introduce(), rt, otherEnumId);
654 Type argT = Type::varint();
655 argT.ot(Type::OT_OPTIONAL);
656 argT.enumId(enumId);
657 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, vd->id());
658 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
659 std::string Cinv_id(std::string(c->id().c_str()) + "⁻¹");
660 vd_x->toplevel(false);
661 auto* occurs = new Call(Location().introduce(), "occurs", {vd_x->id()});
662 auto* deopt = new Call(Location().introduce(), "deopt", {vd_x->id()});
663 auto* inv = new Call(Location().introduce(), Cinv_id, {deopt});
664 auto* toEnumAbsent =
665 new Call(Location().introduce(), "to_enum", {otherEnumId, constants().absent});
666 auto* ite = new ITE(Location().introduce(), {occurs, inv}, toEnumAbsent);
667 auto* Cfn = new FunctionI(Location().introduce(), Cinv_id, Cfn_ti, {vd_x}, ite);
668 enumItems->addItem(Cfn);
669 }
670 {
671 Type Xt;
672 Xt.st(Type::ST_SET);
673 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt, otherEnumId);
674 Type argT = Type::parint();
675 argT.st(Type::ST_SET);
676 argT.enumId(enumId);
677 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, vd->id());
678 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
679 vd_x->toplevel(false);
680 std::string Cinv_id(std::string(c->id().c_str()) + "⁻¹");
681 auto* s_ti = new TypeInst(Location().introduce(), Type::parint());
682 auto* s = new VarDecl(Location().introduce(), s_ti, "s", nullptr);
683 s->toplevel(false);
684 auto* inv = new Call(Location().introduce(), Cinv_id, {s->id()});
685 Generator gen({s}, vd_x->id(), nullptr);
686 Generators gens;
687 gens.g = {gen};
688 auto* comprehension = new Comprehension(Location().introduce(), inv, gens, true);
689 auto* Cfn = new FunctionI(Location().introduce(), Cinv_id, Cfn_ti, {vd_x}, comprehension);
690 enumItems->addItem(Cfn);
691 }
692 {
693 Type Xt;
694 Xt.ti(Type::TI_VAR);
695 Xt.st(Type::ST_SET);
696 auto* Cfn_ti = new TypeInst(Location().introduce(), Xt, otherEnumId);
697 Type argT = Type::varint();
698 argT.st(Type::ST_SET);
699 argT.enumId(enumId);
700 auto* Cfn_x_ti = new TypeInst(Location().introduce(), argT, vd->id());
701 auto* vd_x = new VarDecl(Location().introduce(), Cfn_x_ti, "x");
702 vd_x->toplevel(false);
703 std::string Cinv_id(std::string(c->id().c_str()) + "⁻¹");
704 auto* s_ti = new TypeInst(Location().introduce(), Type::varint());
705 auto* s = new VarDecl(Location().introduce(), s_ti, "s", nullptr);
706 s->toplevel(false);
707 auto* inv = new Call(Location().introduce(), Cinv_id, {s->id()});
708 Generator gen({s}, vd_x->id(), nullptr);
709 Generators gens;
710 gens.g = {gen};
711 auto* comprehension = new Comprehension(Location().introduce(), inv, gens, true);
712 auto* Cfn = new FunctionI(Location().introduce(), Cinv_id, Cfn_ti, {vd_x}, comprehension);
713 enumItems->addItem(Cfn);
714 }
715
716 /*
717 function string: _toString_p_X(opt X: x, bool: b, bool: json) =
718 if absent(x) then "<>" else
719 if json then "{ \"c\": \"C\", \"e\":" else "C(" endif
720 ++_toString_E(to_enum(E,deopt(x)),b,json)
721 ++ if json then "}" else ")" endif
722 endif
723 */
724
725 {
726 Type tx = Type::parint();
727 tx.ot(Type::OT_OPTIONAL);
728 auto* ti_aa = new TypeInst(Location().introduce(), tx);
729 auto* vd_aa = new VarDecl(Location().introduce(), ti_aa, "x");
730 vd_aa->toplevel(false);
731
732 auto* ti_ab = new TypeInst(Location().introduce(), Type::parbool());
733 auto* vd_ab = new VarDecl(Location().introduce(), ti_ab, "b");
734 vd_ab->toplevel(false);
735
736 auto* ti_aj = new TypeInst(Location().introduce(), Type::parbool());
737 auto* vd_aj = new VarDecl(Location().introduce(), ti_aj, "json");
738 vd_aj->toplevel(false);
739
740 std::vector<Expression*> deopt_args(1);
741 deopt_args[0] = vd_aa->id();
742 Call* deopt = new Call(Location().introduce(), "deopt", deopt_args);
743 Call* if_absent = new Call(Location().introduce(), "absent", deopt_args);
744 auto* sl_absent_dzn = new StringLit(Location().introduce(), "<>");
745 ITE* sl_absent =
746 new ITE(Location().introduce(),
747 {vd_aj->id(), new StringLit(Location().introduce(), ASTString("null"))},
748 sl_absent_dzn);
749
750 Call* toEnumE = new Call(Location().introduce(), "to_enum", {otherEnumId, deopt});
751 Call* toString = new Call(Location().introduce(),
752 create_enum_to_string_name(otherEnumId, "_toString_"),
753 {toEnumE, vd_ab->id(), vd_aj->id()});
754
755 auto* openOther =
756 new StringLit(Location().introduce(), std::string(c->id().c_str()) + "(");
757 auto* openJson =
758 new StringLit(Location().introduce(),
759 "{ \"c\" : \"" + std::string(c->id().c_str()) + "\", \"e\" : ");
760 ITE* openConstr = new ITE(Location().introduce(), {vd_aj->id(), openJson}, openOther);
761 auto* closeJson = new StringLit(Location().introduce(), "}");
762 auto* closeOther = new StringLit(Location().introduce(), ")");
763 ITE* closeConstr = new ITE(Location().introduce(), {vd_aj->id(), closeJson}, closeOther);
764
765 auto* concat1 = new BinOp(Location().introduce(), openConstr, BOT_PLUSPLUS, toString);
766 auto* concat2 = new BinOp(Location().introduce(), concat1, BOT_PLUSPLUS, closeConstr);
767
768 ITE* ite = new ITE(Location().introduce(), {if_absent, sl_absent}, concat2);
769 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
770 std::vector<VarDecl*> fi_params(3);
771 fi_params[0] = vd_aa;
772 fi_params[1] = vd_ab;
773 fi_params[2] = vd_aj;
774 std::string XtoString = "_toString_";
775 if (parts.size() > 1) {
776 XtoString += std::to_string(p) + "_";
777 }
778
779 auto* fi =
780 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, XtoString),
781 ti_fi, fi_params, ite);
782 enumItems->addItem(fi);
783 }
784
785 Call* cardE = new Call(Location().introduce(), "card", {otherEnumId});
786 if (partCardinality.empty()) {
787 partCardinality.push_back(cardE);
788 } else {
789 partCardinality.push_back(
790 new BinOp(Location().introduce(), partCardinality.back(), BOT_PLUS, cardE));
791 }
792 }
793 } else {
794 assert(false);
795 }
796 }
797
798 // Create set literal for overall enum
799 Expression* upperBound;
800 if (!partCardinality.empty()) {
801 upperBound = partCardinality.back();
802 } else {
803 // For empty enums, just create 1..0.
804 upperBound = IntLit::a(0);
805 }
806 auto* rhs = new BinOp(vd->loc(), IntLit::a(1), BOT_DOTDOT, upperBound);
807 vd->e(rhs);
808
809 if (parts.size() > 1) {
810 Type tx = Type::parint();
811 tx.ot(Type::OT_OPTIONAL);
812 auto* ti_aa = new TypeInst(Location().introduce(), tx);
813 auto* vd_aa = new VarDecl(Location().introduce(), ti_aa, "x");
814 vd_aa->toplevel(false);
815
816 auto* ti_ab = new TypeInst(Location().introduce(), Type::parbool());
817 auto* vd_ab = new VarDecl(Location().introduce(), ti_ab, "b");
818 vd_ab->toplevel(false);
819
820 auto* ti_aj = new TypeInst(Location().introduce(), Type::parbool());
821 auto* vd_aj = new VarDecl(Location().introduce(), ti_aj, "json");
822 vd_aj->toplevel(false);
823
824 std::vector<Expression*> deopt_args(1);
825 deopt_args[0] = vd_aa->id();
826 Call* deopt = new Call(Location().introduce(), "deopt", deopt_args);
827 Call* if_absent = new Call(Location().introduce(), "absent", deopt_args);
828 auto* sl_absent_dzn = new StringLit(Location().introduce(), "<>");
829 ITE* sl_absent = new ITE(
830 Location().introduce(),
831 {vd_aj->id(), new StringLit(Location().introduce(), ASTString("null"))}, sl_absent_dzn);
832
833 std::vector<Expression*> ite_cases_a;
834 Expression* ite_cases_else;
835 for (unsigned int i = 0; i < parts.size(); i++) {
836 std::string toString = "_toString_" + std::to_string(i) + "_";
837 Expression* aa;
838 if (i == 0) {
839 aa = vd_aa->id();
840 } else {
841 auto* bo = new BinOp(Location().introduce(), deopt, BOT_MINUS, partCardinality[i - 1]);
842 Call* c = new Call(Location().introduce(), "to_enum", {vd->id(), bo});
843 aa = c;
844 }
845 Call* c = new Call(Location().introduce(), create_enum_to_string_name(ident, toString),
846 {aa, vd_ab->id(), vd_aj->id()});
847 if (i < parts.size() - 1) {
848 auto* bo = new BinOp(Location().introduce(), deopt, BOT_LQ, partCardinality[i]);
849 ite_cases_a.push_back(bo);
850 ite_cases_a.push_back(c);
851 } else {
852 ite_cases_else = c;
853 }
854 }
855
856 ITE* ite_cases = new ITE(Location().introduce(), ite_cases_a, ite_cases_else);
857
858 ITE* ite = new ITE(Location().introduce(), {if_absent, sl_absent}, ite_cases);
859
860 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
861 std::vector<VarDecl*> fi_params(3);
862 fi_params[0] = vd_aa;
863 fi_params[1] = vd_ab;
864 fi_params[2] = vd_aj;
865 auto* fi =
866 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
867 ti_fi, fi_params, ite);
868 enumItems->addItem(fi);
869
870 /*
871 function string: _toString_ENUM(opt Foo: x, bool: b, bool: json) =
872 if occurs(x) then
873 if deopt(x)<=partCardinality[1] then _toString_1_ENUM(x,b,json)
874 elseif deopt(x)<=partCardinality[2] then _toString_2_ENUM(x,b,json)
875 ...
876 endif
877 else "<>" endif
878 */
879 }
880
881 {
882 /*
883
884 function _toString_ENUM(array[$U] of opt Foo: x, bool: b, bool: json) =
885 let {
886 array[int] of opt ENUM: xx = array1d(x)
887 } in "[" ++ join(", ", [ _toString_ENUM(xx[i],b,json) | i in index_set(xx) ]) ++ "]";
888
889 */
890
891 TIId* tiid = new TIId(Location().introduce(), "U");
892 auto* ti_range = new TypeInst(Location().introduce(), Type::parint(), tiid);
893 std::vector<TypeInst*> ranges(1);
894 ranges[0] = ti_range;
895
896 Type tx = Type::parint(-1);
897 tx.ot(Type::OT_OPTIONAL);
898 auto* x_ti = new TypeInst(Location().introduce(), tx, ranges, ident);
899 auto* vd_x = new VarDecl(Location().introduce(), x_ti, "x");
900 vd_x->toplevel(false);
901
902 auto* b_ti = new TypeInst(Location().introduce(), Type::parbool());
903 auto* vd_b = new VarDecl(Location().introduce(), b_ti, "b");
904 vd_b->toplevel(false);
905
906 auto* j_ti = new TypeInst(Location().introduce(), Type::parbool());
907 auto* vd_j = new VarDecl(Location().introduce(), j_ti, "json");
908 vd_j->toplevel(false);
909
910 auto* xx_range = new TypeInst(Location().introduce(), Type::parint(), nullptr);
911 std::vector<TypeInst*> xx_ranges(1);
912 xx_ranges[0] = xx_range;
913 auto* xx_ti = new TypeInst(Location().introduce(), tx, xx_ranges, ident);
914
915 std::vector<Expression*> array1dArgs(1);
916 array1dArgs[0] = vd_x->id();
917 Call* array1dCall = new Call(Location().introduce(), "array1d", array1dArgs);
918
919 auto* vd_xx = new VarDecl(Location().introduce(), xx_ti, "xx", array1dCall);
920 vd_xx->toplevel(false);
921
922 auto* idx_i_ti = new TypeInst(Location().introduce(), Type::parint());
923 auto* idx_i = new VarDecl(Location().introduce(), idx_i_ti, "i");
924 idx_i->toplevel(false);
925
926 std::vector<Expression*> aa_xxi_idx(1);
927 aa_xxi_idx[0] = idx_i->id();
928 auto* aa_xxi = new ArrayAccess(Location().introduce(), vd_xx->id(), aa_xxi_idx);
929
930 std::vector<Expression*> _toString_ENUMArgs(3);
931 _toString_ENUMArgs[0] = aa_xxi;
932 _toString_ENUMArgs[1] = vd_b->id();
933 _toString_ENUMArgs[2] = vd_j->id();
934 Call* _toString_ENUM =
935 new Call(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
936 _toString_ENUMArgs);
937
938 std::vector<Expression*> index_set_xx_args(1);
939 index_set_xx_args[0] = vd_xx->id();
940 Call* index_set_xx = new Call(Location().introduce(), "index_set", index_set_xx_args);
941 std::vector<VarDecl*> gen_exps(1);
942 gen_exps[0] = idx_i;
943 Generator gen(gen_exps, index_set_xx, nullptr);
944
945 Generators generators;
946 generators.g.push_back(gen);
947 auto* comp = new Comprehension(Location().introduce(), _toString_ENUM, generators, false);
948
949 std::vector<Expression*> join_args(2);
950 join_args[0] = new StringLit(Location().introduce(), ", ");
951 join_args[1] = comp;
952 Call* join = new Call(Location().introduce(), "join", join_args);
953
954 auto* sl_open = new StringLit(Location().introduce(), "[");
955 auto* bopp0 = new BinOp(Location().introduce(), sl_open, BOT_PLUSPLUS, join);
956 auto* sl_close = new StringLit(Location().introduce(), "]");
957 auto* bopp1 = new BinOp(Location().introduce(), bopp0, BOT_PLUSPLUS, sl_close);
958
959 std::vector<Expression*> let_args(1);
960 let_args[0] = vd_xx;
961 Let* let = new Let(Location().introduce(), let_args, bopp1);
962
963 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
964 std::vector<VarDecl*> fi_params(3);
965 fi_params[0] = vd_x;
966 fi_params[1] = vd_b;
967 fi_params[2] = vd_j;
968 auto* fi =
969 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
970 ti_fi, fi_params, let);
971 enumItems->addItem(fi);
972 }
973
974 {
975 /*
976
977 function _toString_ENUM(opt set of ENUM: x, bool: b, bool: json) =
978 if absent(x) then "<>" else "{" ++ join(", ", [ _toString_ENUM(i,b,json) | i in x ]) ++ "}"
979 endif;
980
981 */
982
983 Type argType = Type::parsetenum(ident->type().enumId());
984 argType.ot(Type::OT_OPTIONAL);
985 auto* x_ti = new TypeInst(Location().introduce(), argType, ident);
986 auto* vd_x = new VarDecl(Location().introduce(), x_ti, "x");
987 vd_x->toplevel(false);
988
989 auto* b_ti = new TypeInst(Location().introduce(), Type::parbool());
990 auto* vd_b = new VarDecl(Location().introduce(), b_ti, "b");
991 vd_b->toplevel(false);
992
993 auto* j_ti = new TypeInst(Location().introduce(), Type::parbool());
994 auto* vd_j = new VarDecl(Location().introduce(), j_ti, "json");
995 vd_j->toplevel(false);
996
997 auto* idx_i_ti = new TypeInst(Location().introduce(), Type::parint());
998 auto* idx_i = new VarDecl(Location().introduce(), idx_i_ti, "i");
999 idx_i->toplevel(false);
1000
1001 std::vector<Expression*> _toString_ENUMArgs(3);
1002 _toString_ENUMArgs[0] = idx_i->id();
1003 _toString_ENUMArgs[1] = vd_b->id();
1004 _toString_ENUMArgs[2] = vd_j->id();
1005 Call* _toString_ENUM =
1006 new Call(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
1007 _toString_ENUMArgs);
1008
1009 std::vector<Expression*> deopt_args(1);
1010 deopt_args[0] = vd_x->id();
1011 Call* deopt = new Call(Location().introduce(), "deopt", deopt_args);
1012 Call* if_absent = new Call(Location().introduce(), "absent", deopt_args);
1013 auto* sl_absent_dzn = new StringLit(Location().introduce(), "<>");
1014 ITE* sl_absent = new ITE(Location().introduce(),
1015 {vd_j->id(), new StringLit(Location().introduce(), ASTString("null"))},
1016 sl_absent_dzn);
1017
1018 std::vector<VarDecl*> gen_exps(1);
1019 gen_exps[0] = idx_i;
1020 Generator gen(gen_exps, deopt, nullptr);
1021
1022 Generators generators;
1023 generators.g.push_back(gen);
1024 auto* comp = new Comprehension(Location().introduce(), _toString_ENUM, generators, false);
1025
1026 std::vector<Expression*> join_args(2);
1027 join_args[0] = new StringLit(Location().introduce(), ", ");
1028 join_args[1] = comp;
1029 Call* join = new Call(Location().introduce(), "join", join_args);
1030
1031 ITE* json_set =
1032 new ITE(Location().introduce(),
1033 {vd_j->id(), new StringLit(Location().introduce(), ASTString("\"set\":["))},
1034 new StringLit(Location().introduce(), ASTString("")));
1035 ITE* json_set_close = new ITE(
1036 Location().introduce(), {vd_j->id(), new StringLit(Location().introduce(), ASTString("]"))},
1037 new StringLit(Location().introduce(), ASTString("")));
1038
1039 auto* sl_open = new StringLit(Location().introduce(), "{");
1040 auto* bopp0 = new BinOp(Location().introduce(), sl_open, BOT_PLUSPLUS, json_set);
1041 auto* bopp1 = new BinOp(Location().introduce(), bopp0, BOT_PLUSPLUS, join);
1042 auto* bopp2 = new BinOp(Location().introduce(), bopp1, BOT_PLUSPLUS, json_set_close);
1043 auto* sl_close = new StringLit(Location().introduce(), "}");
1044 auto* bopp3 = new BinOp(Location().introduce(), bopp2, BOT_PLUSPLUS, sl_close);
1045
1046 std::vector<Expression*> if_then(2);
1047 if_then[0] = if_absent;
1048 if_then[1] = sl_absent;
1049 ITE* ite = new ITE(Location().introduce(), if_then, bopp3);
1050
1051 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
1052 std::vector<VarDecl*> fi_params(3);
1053 fi_params[0] = vd_x;
1054 fi_params[1] = vd_b;
1055 fi_params[2] = vd_j;
1056 auto* fi =
1057 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
1058 ti_fi, fi_params, ite);
1059 enumItems->addItem(fi);
1060 }
1061
1062 {
1063 /*
1064
1065 function _toString_ENUM(array[$U] of opt set of ENUM: x, bool: b, bool: json) =
1066 let {
1067 array[int] of opt set of ENUM: xx = array1d(x)
1068 } in "[" ++ join(", ", [ _toString_ENUM(xx[i],b,json) | i in index_set(xx) ]) ++ "]";
1069
1070 */
1071
1072 TIId* tiid = new TIId(Location().introduce(), "U");
1073 auto* ti_range = new TypeInst(Location().introduce(), Type::parint(), tiid);
1074 std::vector<TypeInst*> ranges(1);
1075 ranges[0] = ti_range;
1076
1077 Type tx = Type::parsetint(-1);
1078 tx.ot(Type::OT_OPTIONAL);
1079 auto* x_ti = new TypeInst(Location().introduce(), tx, ranges, ident);
1080 auto* vd_x = new VarDecl(Location().introduce(), x_ti, "x");
1081 vd_x->toplevel(false);
1082
1083 auto* b_ti = new TypeInst(Location().introduce(), Type::parbool());
1084 auto* vd_b = new VarDecl(Location().introduce(), b_ti, "b");
1085 vd_b->toplevel(false);
1086
1087 auto* j_ti = new TypeInst(Location().introduce(), Type::parbool());
1088 auto* vd_j = new VarDecl(Location().introduce(), j_ti, "json");
1089 vd_j->toplevel(false);
1090
1091 auto* xx_range = new TypeInst(Location().introduce(), Type::parint(), nullptr);
1092 std::vector<TypeInst*> xx_ranges(1);
1093 xx_ranges[0] = xx_range;
1094 auto* xx_ti = new TypeInst(Location().introduce(), tx, xx_ranges, ident);
1095
1096 std::vector<Expression*> array1dArgs(1);
1097 array1dArgs[0] = vd_x->id();
1098 Call* array1dCall = new Call(Location().introduce(), "array1d", array1dArgs);
1099
1100 auto* vd_xx = new VarDecl(Location().introduce(), xx_ti, "xx", array1dCall);
1101 vd_xx->toplevel(false);
1102
1103 auto* idx_i_ti = new TypeInst(Location().introduce(), Type::parint());
1104 auto* idx_i = new VarDecl(Location().introduce(), idx_i_ti, "i");
1105 idx_i->toplevel(false);
1106
1107 std::vector<Expression*> aa_xxi_idx(1);
1108 aa_xxi_idx[0] = idx_i->id();
1109 auto* aa_xxi = new ArrayAccess(Location().introduce(), vd_xx->id(), aa_xxi_idx);
1110
1111 std::vector<Expression*> _toString_ENUMArgs(3);
1112 _toString_ENUMArgs[0] = aa_xxi;
1113 _toString_ENUMArgs[1] = vd_b->id();
1114 _toString_ENUMArgs[2] = vd_j->id();
1115 Call* _toString_ENUM =
1116 new Call(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
1117 _toString_ENUMArgs);
1118
1119 std::vector<Expression*> index_set_xx_args(1);
1120 index_set_xx_args[0] = vd_xx->id();
1121 Call* index_set_xx = new Call(Location().introduce(), "index_set", index_set_xx_args);
1122 std::vector<VarDecl*> gen_exps(1);
1123 gen_exps[0] = idx_i;
1124 Generator gen(gen_exps, index_set_xx, nullptr);
1125
1126 Generators generators;
1127 generators.g.push_back(gen);
1128 auto* comp = new Comprehension(Location().introduce(), _toString_ENUM, generators, false);
1129
1130 std::vector<Expression*> join_args(2);
1131 join_args[0] = new StringLit(Location().introduce(), ", ");
1132 join_args[1] = comp;
1133 Call* join = new Call(Location().introduce(), "join", join_args);
1134
1135 auto* sl_open = new StringLit(Location().introduce(), "[");
1136 auto* bopp0 = new BinOp(Location().introduce(), sl_open, BOT_PLUSPLUS, join);
1137 auto* sl_close = new StringLit(Location().introduce(), "]");
1138 auto* bopp1 = new BinOp(Location().introduce(), bopp0, BOT_PLUSPLUS, sl_close);
1139
1140 std::vector<Expression*> let_args(1);
1141 let_args[0] = vd_xx;
1142 Let* let = new Let(Location().introduce(), let_args, bopp1);
1143
1144 auto* ti_fi = new TypeInst(Location().introduce(), Type::parstring());
1145 std::vector<VarDecl*> fi_params(3);
1146 fi_params[0] = vd_x;
1147 fi_params[1] = vd_b;
1148 fi_params[2] = vd_j;
1149 auto* fi =
1150 new FunctionI(Location().introduce(), create_enum_to_string_name(ident, "_toString_"),
1151 ti_fi, fi_params, let);
1152 enumItems->addItem(fi);
1153 }
1154}
1155
1156void TopoSorter::add(EnvI& env, VarDeclI* vdi, bool handleEnums, Model* enumItems) {
1157 VarDecl* vd = vdi->e();
1158 if (handleEnums && vd->ti()->isEnum()) {
1159 unsigned int enumId = env.registerEnum(vdi);
1160 Type vdt = vd->type();
1161 vdt.enumId(enumId);
1162 vd->ti()->type(vdt);
1163 vd->type(vdt);
1164
1165 create_enum_mapper(env, model, enumId, vd, enumItems);
1166 }
1167 scopes.add(env, vd);
1168}
1169
1170VarDecl* TopoSorter::get(EnvI& env, const ASTString& id_v, const Location& loc) {
1171 GCLock lock;
1172 Id* ident = new Id(Location(), id_v, nullptr);
1173 VarDecl* decl = scopes.find(ident);
1174 if (decl == nullptr) {
1175 std::ostringstream ss;
1176 ss << "undefined identifier `" << ident->str() << "'";
1177 VarDecl* similar = scopes.findSimilar(ident);
1178 if (similar != nullptr) {
1179 ss << ", did you mean `" << *similar->id() << "'?";
1180 }
1181 throw TypeError(env, loc, ss.str());
1182 }
1183 return decl;
1184}
1185
1186VarDecl* TopoSorter::checkId(EnvI& env, Id* ident, const Location& loc) {
1187 VarDecl* decl = scopes.find(ident);
1188 if (decl == nullptr) {
1189 std::ostringstream ss;
1190 ss << "undefined identifier `" << ident->str() << "'";
1191 VarDecl* similar = scopes.findSimilar(ident);
1192 if (similar != nullptr) {
1193 ss << ", did you mean `" << *similar->id() << "'?";
1194 }
1195 throw TypeError(env, loc, ss.str());
1196 }
1197 auto pi = pos.find(decl);
1198 if (pi == pos.end()) {
1199 // new id
1200 scopes.pushToplevel();
1201 run(env, decl);
1202 scopes.pop();
1203 } else {
1204 // previously seen, check if circular
1205 if (pi->second == -1) {
1206 std::ostringstream ss;
1207 ss << "circular definition of `" << ident->str() << "'";
1208 throw TypeError(env, loc, ss.str());
1209 }
1210 }
1211 return decl;
1212}
1213
1214VarDecl* TopoSorter::checkId(EnvI& env, const ASTString& id_v, const Location& loc) {
1215 GCLock lock;
1216 Id* id = new Id(loc, id_v, nullptr);
1217 return checkId(env, id, loc);
1218}
1219
1220void TopoSorter::run(EnvI& env, Expression* e) {
1221 if (e == nullptr) {
1222 return;
1223 }
1224 switch (e->eid()) {
1225 case Expression::E_INTLIT:
1226 case Expression::E_FLOATLIT:
1227 case Expression::E_BOOLLIT:
1228 case Expression::E_STRINGLIT:
1229 case Expression::E_ANON:
1230 break;
1231 case Expression::E_SETLIT: {
1232 auto* sl = e->cast<SetLit>();
1233 if (sl->isv() == nullptr && sl->fsv() == nullptr) {
1234 for (unsigned int i = 0; i < sl->v().size(); i++) {
1235 run(env, sl->v()[i]);
1236 }
1237 }
1238 } break;
1239 case Expression::E_ID: {
1240 if (e != constants().absent) {
1241 VarDecl* vd = checkId(env, e->cast<Id>(), e->loc());
1242 e->cast<Id>()->decl(vd);
1243 }
1244 } break;
1245 case Expression::E_ARRAYLIT: {
1246 auto* al = e->cast<ArrayLit>();
1247 for (unsigned int i = 0; i < al->size(); i++) {
1248 run(env, (*al)[i]);
1249 }
1250 } break;
1251 case Expression::E_ARRAYACCESS: {
1252 auto* ae = e->cast<ArrayAccess>();
1253 run(env, ae->v());
1254 for (unsigned int i = 0; i < ae->idx().size(); i++) {
1255 run(env, ae->idx()[i]);
1256 }
1257 } break;
1258 case Expression::E_COMP: {
1259 auto* ce = e->cast<Comprehension>();
1260 scopes.push();
1261 for (int i = 0; i < ce->numberOfGenerators(); i++) {
1262 run(env, ce->in(i));
1263 for (int j = 0; j < ce->numberOfDecls(i); j++) {
1264 run(env, ce->decl(i, j));
1265 scopes.add(env, ce->decl(i, j));
1266 }
1267 if (ce->where(i) != nullptr) {
1268 run(env, ce->where(i));
1269 }
1270 }
1271 run(env, ce->e());
1272 scopes.pop();
1273 } break;
1274 case Expression::E_ITE: {
1275 ITE* ite = e->cast<ITE>();
1276 for (int i = 0; i < ite->size(); i++) {
1277 run(env, ite->ifExpr(i));
1278 run(env, ite->thenExpr(i));
1279 }
1280 run(env, ite->elseExpr());
1281 } break;
1282 case Expression::E_BINOP: {
1283 auto* be = e->cast<BinOp>();
1284 std::vector<Expression*> todo;
1285 todo.push_back(be->lhs());
1286 todo.push_back(be->rhs());
1287 while (!todo.empty()) {
1288 Expression* be = todo.back();
1289 todo.pop_back();
1290 if (auto* e_bo = be->dynamicCast<BinOp>()) {
1291 todo.push_back(e_bo->lhs());
1292 todo.push_back(e_bo->rhs());
1293 for (ExpressionSetIter it = e_bo->ann().begin(); it != e_bo->ann().end(); ++it) {
1294 run(env, *it);
1295 }
1296 } else {
1297 run(env, be);
1298 }
1299 }
1300 } break;
1301 case Expression::E_UNOP: {
1302 UnOp* ue = e->cast<UnOp>();
1303 run(env, ue->e());
1304 } break;
1305 case Expression::E_CALL: {
1306 Call* ce = e->cast<Call>();
1307 for (unsigned int i = 0; i < ce->argCount(); i++) {
1308 run(env, ce->arg(i));
1309 }
1310 } break;
1311 case Expression::E_VARDECL: {
1312 auto* ve = e->cast<VarDecl>();
1313 auto pi = pos.find(ve);
1314 if (pi == pos.end()) {
1315 pos.insert(std::pair<VarDecl*, int>(ve, -1));
1316 run(env, ve->ti());
1317 run(env, ve->e());
1318 ve->payload(static_cast<int>(decls.size()));
1319 decls.push_back(ve);
1320 pi = pos.find(ve);
1321 pi->second = static_cast<int>(decls.size()) - 1;
1322 } else {
1323 assert(pi->second != -1);
1324 }
1325 } break;
1326 case Expression::E_TI: {
1327 auto* ti = e->cast<TypeInst>();
1328 for (unsigned int i = 0; i < ti->ranges().size(); i++) {
1329 run(env, ti->ranges()[i]);
1330 }
1331 run(env, ti->domain());
1332 } break;
1333 case Expression::E_TIID:
1334 break;
1335 case Expression::E_LET: {
1336 Let* let = e->cast<Let>();
1337 scopes.push();
1338 for (unsigned int i = 0; i < let->let().size(); i++) {
1339 run(env, let->let()[i]);
1340 if (auto* vd = let->let()[i]->dynamicCast<VarDecl>()) {
1341 scopes.add(env, vd);
1342 }
1343 }
1344 run(env, let->in());
1345 VarDeclCmp poscmp(pos);
1346 std::stable_sort(let->let().begin(), let->let().end(), poscmp);
1347 for (unsigned int i = 0, j = 0; i < let->let().size(); i++) {
1348 if (auto* vd = let->let()[i]->dynamicCast<VarDecl>()) {
1349 let->letOrig()[j++] = vd->e();
1350 for (unsigned int k = 0; k < vd->ti()->ranges().size(); k++) {
1351 let->letOrig()[j++] = vd->ti()->ranges()[k]->domain();
1352 }
1353 }
1354 }
1355 scopes.pop();
1356 } break;
1357 }
1358 if (env.ignoreUnknownIds) {
1359 std::vector<Expression*> toDelete;
1360 for (ExpressionSetIter it = e->ann().begin(); it != e->ann().end(); ++it) {
1361 try {
1362 run(env, *it);
1363 } catch (TypeError&) {
1364 toDelete.push_back(*it);
1365 }
1366 for (Expression* de : toDelete) {
1367 e->ann().remove(de);
1368 }
1369 }
1370 } else {
1371 for (ExpressionSetIter it = e->ann().begin(); it != e->ann().end(); ++it) {
1372 run(env, *it);
1373 }
1374 }
1375}
1376
1377KeepAlive add_coercion(EnvI& env, Model* m, Expression* e, const Type& funarg_t) {
1378 if (e->isa<ArrayAccess>() && e->type().dim() > 0) {
1379 auto* aa = e->cast<ArrayAccess>();
1380 // Turn ArrayAccess into a slicing operation
1381 std::vector<Expression*> args;
1382 args.push_back(aa->v());
1383 args.push_back(nullptr);
1384 std::vector<Expression*> slice;
1385 GCLock lock;
1386 for (unsigned int i = 0; i < aa->idx().size(); i++) {
1387 if (aa->idx()[i]->type().isSet()) {
1388 bool needIdxSet = true;
1389 bool needInter = true;
1390 if (auto* sl = aa->idx()[i]->dynamicCast<SetLit>()) {
1391 if ((sl->isv() != nullptr) && sl->isv()->size() == 1) {
1392 if (sl->isv()->min().isFinite() && sl->isv()->max().isFinite()) {
1393 args.push_back(sl);
1394 needIdxSet = false;
1395 } else if (sl->isv()->min() == -IntVal::infinity() &&
1396 sl->isv()->max() == IntVal::infinity()) {
1397 needInter = false;
1398 }
1399 }
1400 }
1401 if (needIdxSet) {
1402 std::ostringstream oss;
1403 oss << "index_set";
1404 if (aa->idx().size() > 1) {
1405 oss << "_" << (i + 1) << "of" << aa->idx().size();
1406 }
1407 std::vector<Expression*> origIdxsetArgs(1);
1408 origIdxsetArgs[0] = aa->v();
1409 Call* origIdxset = new Call(aa->v()->loc(), ASTString(oss.str()), origIdxsetArgs);
1410 FunctionI* fi = m->matchFn(env, origIdxset, false);
1411 if (fi == nullptr) {
1412 throw TypeError(env, e->loc(), "missing builtin " + oss.str());
1413 }
1414 origIdxset->type(fi->rtype(env, origIdxsetArgs, false));
1415 origIdxset->decl(fi);
1416 if (needInter) {
1417 auto* inter = new BinOp(aa->idx()[i]->loc(), aa->idx()[i], BOT_INTERSECT, origIdxset);
1418 inter->type(Type::parsetint());
1419 args.push_back(inter);
1420 } else {
1421 args.push_back(origIdxset);
1422 }
1423 }
1424 slice.push_back(aa->idx()[i]);
1425 } else {
1426 auto* bo = new BinOp(aa->idx()[i]->loc(), aa->idx()[i], BOT_DOTDOT, aa->idx()[i]);
1427 bo->type(Type::parsetint());
1428 slice.push_back(bo);
1429 }
1430 }
1431 auto* a_slice = new ArrayLit(e->loc(), slice);
1432 a_slice->type(Type::parsetint(1));
1433 args[1] = a_slice;
1434 std::ostringstream oss;
1435 oss << "slice_" << (args.size() - 2) << "d";
1436 Call* c = new Call(e->loc(), ASTString(oss.str()), args);
1437 FunctionI* fi = m->matchFn(env, c, false);
1438 if (fi == nullptr) {
1439 throw TypeError(env, e->loc(), "missing builtin " + oss.str());
1440 }
1441 c->type(fi->rtype(env, args, false));
1442 c->decl(fi);
1443 e = c;
1444 }
1445 if (e->type().dim() == funarg_t.dim() &&
1446 (funarg_t.bt() == Type::BT_BOT || funarg_t.bt() == Type::BT_TOP ||
1447 e->type().bt() == funarg_t.bt() || e->type().bt() == Type::BT_BOT)) {
1448 return e;
1449 }
1450 GCLock lock;
1451 Call* c = nullptr;
1452 if (e->type().dim() == 0 && funarg_t.dim() != 0) {
1453 if (e->type().isvar()) {
1454 throw TypeError(env, e->loc(), "cannot coerce var set into array");
1455 }
1456 if (e->type().isOpt()) {
1457 throw TypeError(env, e->loc(), "cannot coerce opt set into array");
1458 }
1459 std::vector<Expression*> set2a_args(1);
1460 set2a_args[0] = e;
1461 Call* set2a = new Call(e->loc(), ASTString("set2array"), set2a_args);
1462 FunctionI* fi = m->matchFn(env, set2a, false);
1463 if (fi != nullptr) {
1464 set2a->type(fi->rtype(env, set2a_args, false));
1465 set2a->decl(fi);
1466 e = set2a;
1467 }
1468 }
1469 if (funarg_t.bt() == Type::BT_TOP || e->type().bt() == funarg_t.bt() ||
1470 e->type().bt() == Type::BT_BOT) {
1471 KeepAlive ka(e);
1472 return ka;
1473 }
1474 std::vector<Expression*> args(1);
1475 args[0] = e;
1476 if (e->type().bt() == Type::BT_BOOL) {
1477 if (funarg_t.bt() == Type::BT_INT) {
1478 c = new Call(e->loc(), constants().ids.bool2int, args);
1479 } else if (funarg_t.bt() == Type::BT_FLOAT) {
1480 c = new Call(e->loc(), constants().ids.bool2float, args);
1481 }
1482 } else if (e->type().bt() == Type::BT_INT) {
1483 if (funarg_t.bt() == Type::BT_FLOAT) {
1484 c = new Call(e->loc(), constants().ids.int2float, args);
1485 }
1486 }
1487 if (c != nullptr) {
1488 FunctionI* fi = m->matchFn(env, c, false);
1489 assert(fi);
1490 Type ct = fi->rtype(env, args, false);
1491 ct.cv(e->type().cv() || ct.cv());
1492 c->type(ct);
1493 c->decl(fi);
1494 KeepAlive ka(c);
1495 return ka;
1496 }
1497 throw TypeError(env, e->loc(),
1498 "cannot determine coercion from type " + e->type().toString(env) + " to type " +
1499 funarg_t.toString(env));
1500}
1501KeepAlive add_coercion(EnvI& env, Model* m, Expression* e, Expression* funarg) {
1502 return add_coercion(env, m, e, funarg->type());
1503}
1504
1505template <bool ignoreVarDecl>
1506class Typer {
1507private:
1508 EnvI& _env;
1509 Model* _model;
1510 std::vector<TypeError>& _typeErrors;
1511 bool _ignoreUndefined;
1512
1513public:
1514 Typer(EnvI& env, Model* model, std::vector<TypeError>& typeErrors, bool ignoreUndefined)
1515 : _env(env), _model(model), _typeErrors(typeErrors), _ignoreUndefined(ignoreUndefined) {}
1516 /// Check annotations when expression is finished
1517 void exit(Expression* e) {
1518 for (ExpressionSetIter it = e->ann().begin(); it != e->ann().end(); ++it) {
1519 if (!(*it)->type().isAnn()) {
1520 throw TypeError(_env, (*it)->loc(),
1521 "expected annotation, got `" + (*it)->type().toString(_env) + "'");
1522 }
1523 }
1524 }
1525 bool enter(Expression* /*e*/) { return true; }
1526 /// Visit integer literal
1527 void vIntLit(const IntLit& /*i*/) {}
1528 /// Visit floating point literal
1529 void vFloatLit(const FloatLit& /*f*/) {}
1530 /// Visit Boolean literal
1531 void vBoolLit(const BoolLit& /*b*/) {}
1532 /// Visit set literal
1533 void vSetLit(SetLit& sl) {
1534 Type ty;
1535 ty.st(Type::ST_SET);
1536 if (sl.isv() != nullptr) {
1537 ty.bt(Type::BT_INT);
1538 ty.enumId(sl.type().enumId());
1539 sl.type(ty);
1540 return;
1541 }
1542 if (sl.fsv() != nullptr) {
1543 ty.bt(Type::BT_FLOAT);
1544 sl.type(ty);
1545 return;
1546 }
1547 unsigned int enumId = sl.v().size() > 0 ? sl.v()[0]->type().enumId() : 0;
1548 for (unsigned int i = 0; i < sl.v().size(); i++) {
1549 Type vi_t = sl.v()[i]->type();
1550 vi_t.ot(Type::OT_PRESENT);
1551 if (sl.v()[i] == constants().absent) {
1552 continue;
1553 }
1554 if (vi_t.dim() > 0) {
1555 throw TypeError(_env, sl.v()[i]->loc(), "set literals cannot contain arrays");
1556 }
1557 if (vi_t.st() == Type::ST_SET) {
1558 throw TypeError(_env, sl.v()[i]->loc(), "set literals cannot contain sets");
1559 }
1560 if (vi_t.isvar()) {
1561 ty.ti(Type::TI_VAR);
1562 }
1563 if (vi_t.cv()) {
1564 ty.cv(true);
1565 }
1566 if (enumId != vi_t.enumId()) {
1567 enumId = 0;
1568 }
1569 if (!Type::btSubtype(vi_t, ty, true)) {
1570 if (ty.bt() == Type::BT_UNKNOWN || Type::btSubtype(ty, vi_t, true)) {
1571 ty.bt(vi_t.bt());
1572 } else {
1573 throw TypeError(_env, sl.loc(), "non-uniform set literal");
1574 }
1575 }
1576 }
1577 ty.enumId(enumId);
1578 if (ty.bt() == Type::BT_UNKNOWN) {
1579 ty.bt(Type::BT_BOT);
1580 } else {
1581 if (ty.isvar() && ty.bt() != Type::BT_INT) {
1582 if (ty.bt() == Type::BT_BOOL) {
1583 ty.bt(Type::BT_INT);
1584 } else {
1585 throw TypeError(_env, sl.loc(), "cannot coerce set literal element to var int");
1586 }
1587 }
1588 for (unsigned int i = 0; i < sl.v().size(); i++) {
1589 sl.v()[i] = add_coercion(_env, _model, sl.v()[i], ty)();
1590 }
1591 }
1592 sl.type(ty);
1593 }
1594 /// Visit string literal
1595 void vStringLit(const StringLit& /*sl*/) {}
1596 /// Visit identifier
1597 void vId(Id& id) {
1598 if (&id != constants().absent) {
1599 assert(!id.decl()->type().isunknown());
1600 id.type(id.decl()->type());
1601 }
1602 }
1603 /// Visit anonymous variable
1604 void vAnonVar(const AnonVar& /*v*/) {}
1605 /// Visit array literal
1606 void vArrayLit(ArrayLit& al) {
1607 Type ty;
1608 ty.dim(static_cast<int>(al.dims()));
1609 std::vector<AnonVar*> anons;
1610 bool haveAbsents = false;
1611 bool haveInferredType = false;
1612 for (unsigned int i = 0; i < al.size(); i++) {
1613 Expression* vi = al[i];
1614 if (vi->type().dim() > 0) {
1615 throw TypeError(_env, vi->loc(), "arrays cannot be elements of arrays");
1616 }
1617 if (vi == constants().absent) {
1618 haveAbsents = true;
1619 }
1620 auto* av = vi->dynamicCast<AnonVar>();
1621 if (av != nullptr) {
1622 ty.ti(Type::TI_VAR);
1623 anons.push_back(av);
1624 } else if (vi->type().isvar()) {
1625 ty.ti(Type::TI_VAR);
1626 }
1627 if (vi->type().cv()) {
1628 ty.cv(true);
1629 }
1630 if (vi->type().isOpt()) {
1631 ty.ot(Type::OT_OPTIONAL);
1632 }
1633
1634 if (ty.bt() == Type::BT_UNKNOWN) {
1635 if (av == nullptr) {
1636 if (haveInferredType) {
1637 if (ty.st() != vi->type().st() && vi->type().ot() != Type::OT_OPTIONAL) {
1638 throw TypeError(_env, al.loc(), "non-uniform array literal");
1639 }
1640 } else {
1641 haveInferredType = true;
1642 ty.st(vi->type().st());
1643 }
1644 if (vi->type().bt() != Type::BT_BOT) {
1645 ty.bt(vi->type().bt());
1646 ty.enumId(vi->type().enumId());
1647 }
1648 }
1649 } else {
1650 if (av == nullptr) {
1651 if (vi->type().bt() == Type::BT_BOT) {
1652 if (vi->type().st() != ty.st() && vi->type().ot() != Type::OT_OPTIONAL) {
1653 throw TypeError(_env, al.loc(), "non-uniform array literal");
1654 }
1655 if (vi->type().enumId() != 0 && ty.enumId() != vi->type().enumId()) {
1656 ty.enumId(0);
1657 }
1658 } else {
1659 unsigned int tyEnumId = ty.enumId();
1660 ty.enumId(vi->type().enumId());
1661 if (Type::btSubtype(ty, vi->type(), true)) {
1662 ty.bt(vi->type().bt());
1663 }
1664 if (tyEnumId != vi->type().enumId()) {
1665 ty.enumId(0);
1666 }
1667 if (!Type::btSubtype(vi->type(), ty, true) || ty.st() != vi->type().st()) {
1668 throw TypeError(_env, al.loc(), "non-uniform array literal");
1669 }
1670 }
1671 }
1672 }
1673 }
1674 if (ty.bt() == Type::BT_UNKNOWN) {
1675 ty.bt(Type::BT_BOT);
1676 if (!anons.empty()) {
1677 throw TypeError(_env, al.loc(),
1678 "array literal must contain at least one non-anonymous variable");
1679 }
1680 if (haveAbsents) {
1681 throw TypeError(_env, al.loc(), "array literal must contain at least one non-absent value");
1682 }
1683 } else {
1684 Type at = ty;
1685 at.dim(0);
1686 if (at.ti() == Type::TI_VAR && at.st() == Type::ST_SET && at.bt() != Type::BT_INT) {
1687 if (at.bt() == Type::BT_BOOL) {
1688 ty.bt(Type::BT_INT);
1689 at.bt(Type::BT_INT);
1690 } else {
1691 throw TypeError(_env, al.loc(), "cannot coerce array element to var set of int");
1692 }
1693 }
1694 for (auto& anon : anons) {
1695 anon->type(at);
1696 }
1697 for (unsigned int i = 0; i < al.size(); i++) {
1698 al.set(i, add_coercion(_env, _model, al[i], at)());
1699 }
1700 }
1701 if (ty.enumId() != 0) {
1702 std::vector<unsigned int> enumIds(ty.dim() + 1);
1703 for (int i = 0; i < ty.dim(); i++) {
1704 enumIds[i] = 0;
1705 }
1706 enumIds[ty.dim()] = ty.enumId();
1707 ty.enumId(_env.registerArrayEnum(enumIds));
1708 }
1709 al.type(ty);
1710 }
1711 /// Visit array access
1712 void vArrayAccess(ArrayAccess& aa) {
1713 if (aa.v()->type().dim() == 0) {
1714 if (aa.v()->type().st() == Type::ST_SET) {
1715 Type tv = aa.v()->type();
1716 tv.st(Type::ST_PLAIN);
1717 tv.dim(1);
1718 aa.v(add_coercion(_env, _model, aa.v(), tv)());
1719 } else {
1720 std::ostringstream oss;
1721 oss << "array access attempted on expression of type `" << aa.v()->type().toString(_env)
1722 << "'";
1723 throw TypeError(_env, aa.v()->loc(), oss.str());
1724 }
1725 } else if (aa.v()->isa<ArrayAccess>()) {
1726 aa.v(add_coercion(_env, _model, aa.v(), aa.v()->type())());
1727 }
1728 if (aa.v()->type().dim() != aa.idx().size()) {
1729 std::ostringstream oss;
1730 oss << aa.v()->type().dim() << "-dimensional array accessed with " << aa.idx().size()
1731 << (aa.idx().size() == 1 ? " expression" : " expressions");
1732 throw TypeError(_env, aa.v()->loc(), oss.str());
1733 }
1734 Type tt = aa.v()->type();
1735 if (tt.enumId() != 0) {
1736 const std::vector<unsigned int>& arrayEnumIds = _env.getArrayEnum(tt.enumId());
1737 std::vector<unsigned int> newArrayEnumids;
1738
1739 for (unsigned int i = 0; i < arrayEnumIds.size() - 1; i++) {
1740 Expression* aai = aa.idx()[i];
1741 // Check if index is slice operator, and convert to correct enum type
1742 if (auto* aai_sl = aai->dynamicCast<SetLit>()) {
1743 if (IntSetVal* aai_isv = aai_sl->isv()) {
1744 if (aai_isv->min() == -IntVal::infinity() && aai_isv->max() == IntVal::infinity()) {
1745 Type aai_sl_t = aai_sl->type();
1746 aai_sl_t.enumId(arrayEnumIds[i]);
1747 aai_sl->type(aai_sl_t);
1748 }
1749 }
1750 } else if (auto* aai_bo = aai->dynamicCast<BinOp>()) {
1751 if (aai_bo->op() == BOT_DOTDOT) {
1752 Type aai_bo_t = aai_bo->type();
1753 if (auto* il = aai_bo->lhs()->dynamicCast<IntLit>()) {
1754 if (il->v() == -IntVal::infinity()) {
1755 // Expression is ..X, so result gets enum type of X
1756 aai_bo_t.enumId(aai_bo->rhs()->type().enumId());
1757 }
1758 } else if (auto* il = aai_bo->rhs()->dynamicCast<IntLit>()) {
1759 if (il->v() == IntVal::infinity()) {
1760 // Expression is X.., so result gets enum type of X
1761 aai_bo_t.enumId(aai_bo->lhs()->type().enumId());
1762 }
1763 }
1764 aai_bo->type(aai_bo_t);
1765 }
1766 }
1767 if (aai->type().isSet()) {
1768 newArrayEnumids.push_back(arrayEnumIds[i]);
1769 }
1770
1771 if (arrayEnumIds[i] != 0) {
1772 if (aa.idx()[i]->type().enumId() != arrayEnumIds[i]) {
1773 std::ostringstream oss;
1774 oss << "array index ";
1775 if (aa.idx().size() > 1) {
1776 oss << (i + 1) << " ";
1777 }
1778 oss << "must be `" << _env.getEnum(arrayEnumIds[i])->e()->id()->str() << "', but is `"
1779 << aa.idx()[i]->type().toString(_env) << "'";
1780 throw TypeError(_env, aa.loc(), oss.str());
1781 }
1782 }
1783 }
1784 if (newArrayEnumids.empty()) {
1785 tt.enumId(arrayEnumIds[arrayEnumIds.size() - 1]);
1786 } else {
1787 newArrayEnumids.push_back(arrayEnumIds[arrayEnumIds.size() - 1]);
1788 int newEnumId = _env.registerArrayEnum(newArrayEnumids);
1789 tt.enumId(newEnumId);
1790 }
1791 }
1792 int n_dimensions = 0;
1793 bool isVarAccess = false;
1794 bool isSlice = false;
1795 for (unsigned int i = 0; i < aa.idx().size(); i++) {
1796 Expression* aai = aa.idx()[i];
1797 if (aai->isa<AnonVar>()) {
1798 aai->type(Type::varint());
1799 }
1800 if ((aai->type().bt() != Type::BT_INT && aai->type().bt() != Type::BT_BOOL) ||
1801 aai->type().dim() != 0) {
1802 throw TypeError(_env, aa.loc(),
1803 "array index must be `int' or `set of int', but is `" +
1804 aai->type().toString(_env) + "'");
1805 }
1806 if (aai->type().isSet()) {
1807 if (isVarAccess || aai->type().isvar()) {
1808 throw TypeError(_env, aa.loc(),
1809 "array slicing with variable range or index not supported");
1810 }
1811 isSlice = true;
1812 aa.idx()[i] = add_coercion(_env, _model, aai, Type::varsetint())();
1813 n_dimensions++;
1814 } else {
1815 aa.idx()[i] = add_coercion(_env, _model, aai, Type::varint())();
1816 }
1817
1818 if (aai->type().isOpt()) {
1819 tt.ot(Type::OT_OPTIONAL);
1820 }
1821 if (aai->type().isvar()) {
1822 isVarAccess = true;
1823 if (isSlice) {
1824 throw TypeError(_env, aa.loc(),
1825 "array slicing with variable range or index not supported");
1826 }
1827 tt.ti(Type::TI_VAR);
1828 if (tt.bt() == Type::BT_ANN || tt.bt() == Type::BT_STRING) {
1829 throw TypeError(_env, aai->loc(),
1830 std::string("array access using a variable not supported for array of ") +
1831 (tt.bt() == Type::BT_ANN ? "ann" : "string"));
1832 }
1833 }
1834 tt.dim(n_dimensions);
1835 if (aai->type().cv()) {
1836 tt.cv(true);
1837 }
1838 }
1839 aa.type(tt);
1840 }
1841 /// Visit array comprehension
1842 void vComprehension(Comprehension& c) {
1843 Type tt = c.e()->type();
1844 typedef std::unordered_map<VarDecl*, std::pair<int, int>> genMap_t;
1845 typedef std::unordered_map<VarDecl*, std::vector<Expression*>> whereMap_t;
1846 genMap_t generatorMap;
1847 whereMap_t whereMap;
1848 int declCount = 0;
1849
1850 for (int i = 0; i < c.numberOfGenerators(); i++) {
1851 for (int j = 0; j < c.numberOfDecls(i); j++) {
1852 generatorMap[c.decl(i, j)] = std::pair<int, int>(i, declCount++);
1853 whereMap[c.decl(i, j)] = std::vector<Expression*>();
1854 }
1855 Expression* g_in = c.in(i);
1856 if (g_in != nullptr) {
1857 const Type& ty_in = g_in->type();
1858 if (ty_in == Type::varsetint()) {
1859 if (!c.set()) {
1860 tt.ot(Type::OT_OPTIONAL);
1861 }
1862 tt.ti(Type::TI_VAR);
1863 tt.cv(true);
1864 }
1865 if (ty_in.cv()) {
1866 tt.cv(true);
1867 }
1868 if (c.where(i) != nullptr) {
1869 if (c.where(i)->type() == Type::varbool()) {
1870 if (!c.set()) {
1871 tt.ot(Type::OT_OPTIONAL);
1872 }
1873 tt.ti(Type::TI_VAR);
1874 tt.cv(true);
1875 } else if (c.where(i)->type() != Type::parbool()) {
1876 throw TypeError(
1877 _env, c.where(i)->loc(),
1878 "where clause must be bool, but is `" + c.where(i)->type().toString(_env) + "'");
1879 }
1880 if (c.where(i)->type().cv()) {
1881 tt.cv(true);
1882 }
1883
1884 // Try to move parts of the where clause to earlier generators
1885 std::vector<Expression*> wherePartsStack;
1886 std::vector<Expression*> whereParts;
1887 wherePartsStack.push_back(c.where(i));
1888 while (!wherePartsStack.empty()) {
1889 Expression* e = wherePartsStack.back();
1890 wherePartsStack.pop_back();
1891 if (auto* bo = e->dynamicCast<BinOp>()) {
1892 if (bo->op() == BOT_AND) {
1893 wherePartsStack.push_back(bo->rhs());
1894 wherePartsStack.push_back(bo->lhs());
1895 } else {
1896 whereParts.push_back(e);
1897 }
1898 } else {
1899 whereParts.push_back(e);
1900 }
1901 }
1902
1903 for (auto* wp : whereParts) {
1904 class FindLatestGen : public EVisitor {
1905 public:
1906 int declIndex;
1907 VarDecl* decl;
1908 const genMap_t& generatorMap;
1909 Comprehension* comp;
1910 FindLatestGen(const genMap_t& generatorMap0, Comprehension* comp0)
1911 : declIndex(-1),
1912 decl(comp0->decl(0, 0)),
1913 generatorMap(generatorMap0),
1914 comp(comp0) {}
1915 void vId(const Id& ident) {
1916 auto it = generatorMap.find(ident.decl());
1917 if (it != generatorMap.end() && it->second.second > declIndex) {
1918 declIndex = it->second.second;
1919 decl = ident.decl();
1920 int gen = it->second.first;
1921 while (comp->in(gen) == nullptr && gen < comp->numberOfGenerators() - 1) {
1922 declIndex++;
1923 gen++;
1924 decl = comp->decl(gen, 0);
1925 }
1926 }
1927 }
1928 } flg(generatorMap, &c);
1929 top_down(flg, wp);
1930 whereMap[flg.decl].push_back(wp);
1931 }
1932 }
1933 } else {
1934 assert(c.where(i) != nullptr);
1935 whereMap[c.decl(i, 0)].push_back(c.where(i));
1936 }
1937 }
1938
1939 {
1940 GCLock lock;
1941 Generators generators;
1942 for (int i = 0; i < c.numberOfGenerators(); i++) {
1943 std::vector<VarDecl*> decls;
1944 for (int j = 0; j < c.numberOfDecls(i); j++) {
1945 decls.push_back(c.decl(i, j));
1946 KeepAlive c_in =
1947 c.in(i) != nullptr ? add_coercion(_env, _model, c.in(i), c.in(i)->type()) : nullptr;
1948 if (!whereMap[c.decl(i, j)].empty()) {
1949 // need a generator for all the decls up to this point
1950 Expression* whereExpr = whereMap[c.decl(i, j)][0];
1951 for (unsigned int k = 1; k < whereMap[c.decl(i, j)].size(); k++) {
1952 GCLock lock;
1953 auto* bo =
1954 new BinOp(Location().introduce(), whereExpr, BOT_AND, whereMap[c.decl(i, j)][k]);
1955 Type bo_t = whereMap[c.decl(i, j)][k]->type().isPar() && whereExpr->type().isPar()
1956 ? Type::parbool()
1957 : Type::varbool();
1958 if (whereMap[c.decl(i, j)][k]->type().cv() || whereExpr->type().cv()) {
1959 bo_t.cv(true);
1960 }
1961 bo->type(bo_t);
1962 whereExpr = bo;
1963 }
1964 generators.g.emplace_back(decls, c_in(), whereExpr);
1965 decls.clear();
1966 } else if (j == c.numberOfDecls(i) - 1) {
1967 generators.g.emplace_back(decls, c_in(), nullptr);
1968 decls.clear();
1969 }
1970 }
1971 }
1972 c.init(c.e(), generators);
1973 }
1974
1975 if (c.set()) {
1976 if (c.e()->type().dim() != 0 || c.e()->type().st() == Type::ST_SET) {
1977 throw TypeError(_env, c.e()->loc(),
1978 "set comprehension expression must be scalar, but is `" +
1979 c.e()->type().toString(_env) + "'");
1980 }
1981 tt.st(Type::ST_SET);
1982 if (tt.isvar()) {
1983 c.e(add_coercion(_env, _model, c.e(), Type::varint())());
1984 tt.bt(Type::BT_INT);
1985 }
1986 } else {
1987 if (c.e()->type().dim() != 0) {
1988 throw TypeError(_env, c.e()->loc(), "array comprehension expression cannot be an array");
1989 }
1990 tt.dim(1);
1991 if (tt.enumId() != 0) {
1992 std::vector<unsigned int> enumIds(2);
1993 enumIds[0] = 0;
1994 enumIds[1] = tt.enumId();
1995 tt.enumId(_env.registerArrayEnum(enumIds));
1996 }
1997 }
1998 c.type(tt);
1999 }
2000 /// Visit array comprehension generator
2001 void vComprehensionGenerator(Comprehension& c, int gen_i) {
2002 Expression* g_in = c.in(gen_i);
2003 if (g_in == nullptr) {
2004 // This is an "assignment generator" (i = expr)
2005 assert(c.where(gen_i) != nullptr);
2006 assert(c.numberOfDecls(gen_i) == 1);
2007 const Type& ty_where = c.where(gen_i)->type();
2008 c.decl(gen_i, 0)->type(ty_where);
2009 c.decl(gen_i, 0)->ti()->type(ty_where);
2010 } else {
2011 const Type& ty_in = g_in->type();
2012 if (ty_in != Type::varsetint() && ty_in != Type::parsetint() && ty_in.dim() != 1) {
2013 throw TypeError(_env, g_in->loc(),
2014 "generator expression must be (par or var) set of int or one-dimensional "
2015 "array, but is `" +
2016 ty_in.toString(_env) + "'");
2017 }
2018 Type ty_id;
2019 if (ty_in.dim() == 0) {
2020 ty_id = Type::parint();
2021 ty_id.enumId(ty_in.enumId());
2022 } else {
2023 ty_id = ty_in;
2024 if (ty_in.enumId() != 0) {
2025 const std::vector<unsigned int>& enumIds = _env.getArrayEnum(ty_in.enumId());
2026 ty_id.enumId(enumIds.back());
2027 }
2028 ty_id.dim(0);
2029 }
2030 for (int j = 0; j < c.numberOfDecls(gen_i); j++) {
2031 c.decl(gen_i, j)->type(ty_id);
2032 c.decl(gen_i, j)->ti()->type(ty_id);
2033 }
2034 }
2035 }
2036 /// Visit if-then-else
2037 void vITE(ITE& ite) {
2038 bool mustBeBool = false;
2039 if (ite.elseExpr() == nullptr) {
2040 // this is an "if <cond> then <expr> endif" so the <expr> must be bool
2041 ite.elseExpr(constants().boollit(true));
2042 mustBeBool = true;
2043 }
2044 Type tret = ite.elseExpr()->type();
2045 std::vector<AnonVar*> anons;
2046 bool allpar = !(tret.isvar());
2047 if (tret.isunknown()) {
2048 if (auto* av = ite.elseExpr()->dynamicCast<AnonVar>()) {
2049 allpar = false;
2050 anons.push_back(av);
2051 } else {
2052 throw TypeError(_env, ite.elseExpr()->loc(),
2053 "cannot infer type of expression in `else' branch of conditional");
2054 }
2055 }
2056 bool allpresent = !(tret.isOpt());
2057 bool varcond = false;
2058 for (int i = 0; i < ite.size(); i++) {
2059 Expression* eif = ite.ifExpr(i);
2060 Expression* ethen = ite.thenExpr(i);
2061 varcond = varcond || (eif->type() == Type::varbool());
2062 if (eif->type() != Type::parbool() && eif->type() != Type::varbool()) {
2063 throw TypeError(
2064 _env, eif->loc(),
2065 "expected bool conditional expression, got `" + eif->type().toString(_env) + "'");
2066 }
2067 if (eif->type().cv()) {
2068 tret.cv(true);
2069 }
2070 if (ethen->type().isunknown()) {
2071 if (auto* av = ethen->dynamicCast<AnonVar>()) {
2072 allpar = false;
2073 anons.push_back(av);
2074 } else {
2075 throw TypeError(_env, ethen->loc(),
2076 "cannot infer type of expression in `then' branch of conditional");
2077 }
2078 } else {
2079 if (tret.isbot() || tret.isunknown()) {
2080 tret.bt(ethen->type().bt());
2081 }
2082 if (mustBeBool &&
2083 (ethen->type().bt() != Type::BT_BOOL || ethen->type().dim() > 0 ||
2084 ethen->type().st() != Type::ST_PLAIN || ethen->type().ot() != Type::OT_PRESENT)) {
2085 throw TypeError(_env, ite.loc(),
2086 std::string("conditional without `else' branch must have bool type, ") +
2087 "but `then' branch has type `" + ethen->type().toString(_env) + "'");
2088 }
2089 if ((!ethen->type().isbot() && !Type::btSubtype(ethen->type(), tret, true) &&
2090 !Type::btSubtype(tret, ethen->type(), true)) ||
2091 ethen->type().st() != tret.st() || ethen->type().dim() != tret.dim()) {
2092 throw TypeError(_env, ethen->loc(),
2093 "type mismatch in branches of conditional. `then' branch has type `" +
2094 ethen->type().toString(_env) + "', but `else' branch has type `" +
2095 tret.toString(_env) + "'");
2096 }
2097 if (Type::btSubtype(tret, ethen->type(), true)) {
2098 tret.bt(ethen->type().bt());
2099 }
2100 if (tret.enumId() != 0 && ethen->type().enumId() == 0) {
2101 tret.enumId(0);
2102 }
2103 if (ethen->type().isvar()) {
2104 allpar = false;
2105 }
2106 if (ethen->type().isOpt()) {
2107 allpresent = false;
2108 }
2109 if (ethen->type().cv()) {
2110 tret.cv(true);
2111 }
2112 }
2113 }
2114 Type tret_var(tret);
2115 tret_var.ti(Type::TI_VAR);
2116 for (auto& anon : anons) {
2117 anon->type(tret_var);
2118 }
2119 for (int i = 0; i < ite.size(); i++) {
2120 ite.thenExpr(i, add_coercion(_env, _model, ite.thenExpr(i), tret)());
2121 }
2122 ite.elseExpr(add_coercion(_env, _model, ite.elseExpr(), tret)());
2123 /// TODO: perhaps extend flattener to array types, but for now throw an error
2124 if (varcond && tret.dim() > 0) {
2125 throw TypeError(_env, ite.loc(), "conditional with var condition cannot have array type");
2126 }
2127 if (varcond || !allpar) {
2128 tret.ti(Type::TI_VAR);
2129 }
2130 if (!allpresent) {
2131 tret.ot(Type::OT_OPTIONAL);
2132 }
2133 ite.type(tret);
2134 }
2135 /// Visit binary operator
2136 void vBinOp(BinOp& bop) {
2137 std::vector<Expression*> args(2);
2138 args[0] = bop.lhs();
2139 args[1] = bop.rhs();
2140 if (FunctionI* fi = _model->matchFn(_env, bop.opToString(), args, true)) {
2141 bop.lhs(add_coercion(_env, _model, bop.lhs(), fi->argtype(_env, args, 0))());
2142 bop.rhs(add_coercion(_env, _model, bop.rhs(), fi->argtype(_env, args, 1))());
2143 args[0] = bop.lhs();
2144 args[1] = bop.rhs();
2145 Type ty = fi->rtype(_env, args, true);
2146 ty.cv(bop.lhs()->type().cv() || bop.rhs()->type().cv() || ty.cv());
2147 bop.type(ty);
2148
2149 if (fi->e() != nullptr) {
2150 bop.decl(fi);
2151 } else {
2152 bop.decl(nullptr);
2153 }
2154
2155 if (bop.lhs()->type().isint() && bop.rhs()->type().isint() &&
2156 (bop.op() == BOT_EQ || bop.op() == BOT_GQ || bop.op() == BOT_GR || bop.op() == BOT_NQ ||
2157 bop.op() == BOT_LE || bop.op() == BOT_LQ)) {
2158 Call* call = bop.lhs()->dynamicCast<Call>();
2159 Expression* rhs = bop.rhs();
2160 BinOpType bot = bop.op();
2161 if (call == nullptr) {
2162 call = bop.rhs()->dynamicCast<Call>();
2163 rhs = bop.lhs();
2164 switch (bop.op()) {
2165 case BOT_LQ:
2166 bot = BOT_GQ;
2167 break;
2168 case BOT_LE:
2169 bot = BOT_GR;
2170 break;
2171 case BOT_GQ:
2172 bot = BOT_LQ;
2173 break;
2174 case BOT_GR:
2175 bot = BOT_LE;
2176 break;
2177 default:
2178 break;
2179 }
2180 }
2181 if ((call != nullptr) && (call->id() == "count" || call->id() == "sum") &&
2182 call->type().isvar()) {
2183 if (call->argCount() == 1 && call->arg(0)->isa<Comprehension>()) {
2184 auto* comp = call->arg(0)->cast<Comprehension>();
2185 auto* inner_bo = comp->e()->dynamicCast<BinOp>();
2186 if (inner_bo != nullptr) {
2187 if (inner_bo->op() == BOT_EQ && inner_bo->lhs()->type().isint()) {
2188 Expression* generated = inner_bo->lhs();
2189 Expression* comparedTo = inner_bo->rhs();
2190 if (comp->containsBoundVariable(comparedTo)) {
2191 if (comp->containsBoundVariable(generated)) {
2192 comparedTo = nullptr;
2193 } else {
2194 std::swap(generated, comparedTo);
2195 }
2196 }
2197 if (comparedTo != nullptr) {
2198 GCLock lock;
2199 ASTString cid;
2200 switch (bot) {
2201 case BOT_EQ:
2202 cid = ASTString("count_eq");
2203 break;
2204 case BOT_GQ:
2205 cid = ASTString("count_leq");
2206 break;
2207 case BOT_GR:
2208 cid = ASTString("count_lt");
2209 break;
2210 case BOT_LQ:
2211 cid = ASTString("count_geq");
2212 break;
2213 case BOT_LE:
2214 cid = ASTString("count_gt");
2215 break;
2216 case BOT_NQ:
2217 cid = ASTString("count_neq");
2218 break;
2219 default:
2220 assert(false);
2221 }
2222
2223 comp->e(generated);
2224 Type ct = comp->type();
2225 ct.bt(generated->type().bt());
2226 comp->type(ct);
2227
2228 std::vector<Expression*> args({comp, comparedTo, rhs});
2229 FunctionI* newCall_decl = _model->matchFn(_env, cid, args, true);
2230 if (newCall_decl == nullptr) {
2231 std::ostringstream ss;
2232 ss << "could not replace binary operator by call to " << cid;
2233 throw InternalError(ss.str());
2234 }
2235 Call* newCall = bop.morph(cid, args);
2236 newCall->decl(newCall_decl);
2237 }
2238 }
2239 }
2240 } else if (call->argCount() == 2 && call->arg(0)->type().isIntArray() &&
2241 call->arg(1)->type().isint()) {
2242 GCLock lock;
2243 ASTString cid;
2244 switch (bot) {
2245 case BOT_EQ:
2246 cid = ASTString("count_eq");
2247 break;
2248 case BOT_GQ:
2249 cid = ASTString("count_leq");
2250 break;
2251 case BOT_GR:
2252 cid = ASTString("count_lt");
2253 break;
2254 case BOT_LQ:
2255 cid = ASTString("count_geq");
2256 break;
2257 case BOT_LE:
2258 cid = ASTString("count_gt");
2259 break;
2260 case BOT_NQ:
2261 cid = ASTString("count_neq");
2262 break;
2263 default:
2264 assert(false);
2265 }
2266 std::vector<Expression*> args({call->arg(0), call->arg(1), rhs});
2267 FunctionI* newCall_decl = _model->matchFn(_env, cid, args, true);
2268 if (newCall_decl == nullptr) {
2269 std::ostringstream ss;
2270 ss << "could not replace binary operator by call to " << cid;
2271 throw InternalError(ss.str());
2272 }
2273 Call* newCall = bop.morph(cid, args);
2274 newCall->decl(newCall_decl);
2275 }
2276 }
2277 }
2278 } else {
2279 std::ostringstream ss;
2280 ss << "type error in operator application for `" << bop.opToString()
2281 << "'. No matching operator found with left-hand side type `"
2282 << bop.lhs()->type().toString(_env) << "' and right-hand side type `"
2283 << bop.rhs()->type().toString(_env) << "'";
2284 throw TypeError(_env, bop.loc(), ss.str());
2285 }
2286 }
2287 /// Visit unary operator
2288 void vUnOp(UnOp& uop) {
2289 std::vector<Expression*> args(1);
2290 args[0] = uop.e();
2291 if (FunctionI* fi = _model->matchFn(_env, uop.opToString(), args, true)) {
2292 uop.e(add_coercion(_env, _model, uop.e(), fi->argtype(_env, args, 0))());
2293 args[0] = uop.e();
2294 Type ty = fi->rtype(_env, args, true);
2295 ty.cv(uop.e()->type().cv() || ty.cv());
2296 uop.type(ty);
2297 if (fi->e() != nullptr) {
2298 uop.decl(fi);
2299 }
2300 } else {
2301 std::ostringstream ss;
2302 ss << "type error in operator application for `" << uop.opToString()
2303 << "'. No matching operator found with type `" << uop.e()->type().toString(_env) << "'";
2304 throw TypeError(_env, uop.loc(), ss.str());
2305 }
2306 }
2307
2308 /// Visit call
2309 void vCall(Call& call) {
2310 std::vector<Expression*> args(call.argCount());
2311 for (auto i = static_cast<unsigned int>(args.size()); (i--) != 0U;) {
2312 args[i] = call.arg(i);
2313 }
2314 FunctionI* fi = _model->matchFn(_env, &call, true, true);
2315
2316 if (fi != nullptr && fi->id() == "symmetry_breaking_constraint" && fi->paramCount() == 1 &&
2317 fi->param(0)->type().isbool()) {
2318 GCLock lock;
2319 call.id(ASTString("mzn_symmetry_breaking_constraint"));
2320 fi = _model->matchFn(_env, &call, true, true);
2321 } else if (fi != nullptr && fi->id() == "redundant_constraint" && fi->paramCount() == 1 &&
2322 fi->param(0)->type().isbool()) {
2323 GCLock lock;
2324 call.id(ASTString("mzn_redundant_constraint"));
2325 fi = _model->matchFn(_env, &call, true, true);
2326 }
2327
2328 if ((fi->e() != nullptr) && fi->e()->isa<Call>()) {
2329 Call* next_call = fi->e()->cast<Call>();
2330 if ((next_call->decl() != nullptr) && next_call->argCount() == fi->paramCount() &&
2331 _model->sameOverloading(_env, args, fi, next_call->decl())) {
2332 bool macro = true;
2333 for (unsigned int i = 0; i < fi->paramCount(); i++) {
2334 if (!Expression::equal(next_call->arg(i), fi->param(i)->id())) {
2335 macro = false;
2336 break;
2337 }
2338 }
2339 if (macro) {
2340 // Call is not a macro if it has a reification implementation
2341 GCLock lock;
2342 ASTString reif_id = _env.reifyId(fi->id());
2343 std::vector<Type> tt(fi->paramCount() + 1);
2344 for (unsigned int i = 0; i < fi->paramCount(); i++) {
2345 tt[i] = fi->param(i)->type();
2346 }
2347 tt[fi->paramCount()] = Type::varbool();
2348
2349 macro = _model->matchFn(_env, reif_id, tt, true) == nullptr;
2350 }
2351 if (macro) {
2352 call.decl(next_call->decl());
2353 for (ExpressionSetIter esi = next_call->ann().begin(); esi != next_call->ann().end();
2354 ++esi) {
2355 call.addAnnotation(*esi);
2356 }
2357 call.rehash();
2358 fi = next_call->decl();
2359 }
2360 }
2361 }
2362
2363 bool cv = false;
2364 for (unsigned int i = 0; i < args.size(); i++) {
2365 if (auto* c = call.arg(i)->dynamicCast<Comprehension>()) {
2366 Type t_before = c->e()->type();
2367 Type t = fi->argtype(_env, args, i);
2368 t.dim(0);
2369 c->e(add_coercion(_env, _model, c->e(), t)());
2370 Type t_after = c->e()->type();
2371 if (t_before != t_after) {
2372 Type ct = c->type();
2373 ct.bt(t_after.bt());
2374 c->type(ct);
2375 }
2376 } else {
2377 args[i] = add_coercion(_env, _model, call.arg(i), fi->argtype(_env, args, i))();
2378 call.arg(i, args[i]);
2379 }
2380 cv = cv || args[i]->type().cv();
2381 }
2382 // Replace par enums with their string versions
2383 if (call.id() == "format" || call.id() == "show" || call.id() == "showDzn" ||
2384 call.id() == "showJSON") {
2385 if (call.arg(call.argCount() - 1)->type().isPar()) {
2386 unsigned int enumId = call.arg(call.argCount() - 1)->type().enumId();
2387 if (enumId != 0U && call.arg(call.argCount() - 1)->type().dim() != 0) {
2388 const std::vector<unsigned int>& enumIds = _env.getArrayEnum(enumId);
2389 enumId = enumIds[enumIds.size() - 1];
2390 }
2391 if (enumId > 0) {
2392 VarDecl* enumDecl = _env.getEnum(enumId)->e();
2393 if (enumDecl->e() != nullptr) {
2394 Id* ti_id = _env.getEnum(enumId)->e()->id();
2395 GCLock lock;
2396 std::vector<Expression*> args(3);
2397 args[0] = call.arg(call.argCount() - 1);
2398 if (args[0]->type().dim() > 1) {
2399 std::vector<Expression*> a1dargs(1);
2400 a1dargs[0] = args[0];
2401 Call* array1d = new Call(Location().introduce(), ASTString("array1d"), a1dargs);
2402 Type array1dt = args[0]->type();
2403 array1dt.dim(1);
2404 array1d->type(array1dt);
2405 args[0] = array1d;
2406 }
2407 args[1] = constants().boollit(call.id() == "showDzn");
2408 args[2] = constants().boollit(call.id() == "showJSON");
2409 ASTString enumName(create_enum_to_string_name(ti_id, "_toString_"));
2410 call.id(enumName);
2411 call.args(args);
2412 if (call.id() == "showDzn") {
2413 call.id(constants().ids.show);
2414 }
2415 fi = _model->matchFn(_env, &call, false, true);
2416 }
2417 }
2418 }
2419 }
2420
2421 // Set type and decl
2422 Type ty = fi->rtype(_env, args, true);
2423 ty.cv(cv || ty.cv());
2424 call.type(ty);
2425
2426 if (Call* deprecated = fi->ann().getCall(constants().ann.mzn_deprecated)) {
2427 // rewrite this call into a call to mzn_deprecate(..., e)
2428 GCLock lock;
2429 std::vector<Expression*> params(call.argCount());
2430 for (unsigned int i = 0; i < params.size(); i++) {
2431 params[i] = call.arg(i);
2432 }
2433 Call* origCall = new Call(call.loc(), call.id(), params);
2434 origCall->type(ty);
2435 origCall->decl(fi);
2436 call.id(constants().ids.mzn_deprecate);
2437 std::vector<Expression*> args(
2438 {new StringLit(Location(), fi->id()), deprecated->arg(0), deprecated->arg(1), origCall});
2439 call.args(args);
2440 FunctionI* deprecated_fi = _model->matchFn(_env, &call, false, true);
2441 call.decl(deprecated_fi);
2442 } else {
2443 call.decl(fi);
2444 }
2445 }
2446 /// Visit let
2447 void vLet(Let& let) {
2448 bool cv = false;
2449 bool isVar = false;
2450 for (unsigned int i = 0, j = 0; i < let.let().size(); i++) {
2451 Expression* li = let.let()[i];
2452 cv = cv || li->type().cv();
2453 if (auto* vdi = li->dynamicCast<VarDecl>()) {
2454 if (vdi->e() == nullptr && vdi->type().isSet() && vdi->type().isvar() &&
2455 vdi->ti()->domain() == nullptr) {
2456 std::ostringstream ss;
2457 ss << "set element type for `" << vdi->id()->str() << "' is not finite";
2458 _typeErrors.emplace_back(_env, vdi->loc(), ss.str());
2459 }
2460 if (vdi->type().isPar() && (vdi->e() == nullptr)) {
2461 std::ostringstream ss;
2462 ss << "let variable `" << vdi->id()->v() << "' must be initialised";
2463 throw TypeError(_env, vdi->loc(), ss.str());
2464 }
2465 if (vdi->ti()->hasTiVariable()) {
2466 std::ostringstream ss;
2467 ss << "type-inst variables not allowed in type-inst for let variable `"
2468 << vdi->id()->str() << "'";
2469 _typeErrors.emplace_back(_env, vdi->loc(), ss.str());
2470 }
2471 let.letOrig()[j++] = vdi->e();
2472 for (unsigned int k = 0; k < vdi->ti()->ranges().size(); k++) {
2473 let.letOrig()[j++] = vdi->ti()->ranges()[k]->domain();
2474 }
2475 }
2476 isVar |= li->type().isvar();
2477 }
2478 Type ty = let.in()->type();
2479 ty.cv(cv || ty.cv());
2480 if (isVar && ty.bt() == Type::BT_BOOL && ty.dim() == 0) {
2481 ty.ti(Type::TI_VAR);
2482 }
2483 let.type(ty);
2484 }
2485 /// Visit variable declaration
2486 void vVarDecl(VarDecl& vd) {
2487 if (ignoreVarDecl) {
2488 if (vd.e() != nullptr) {
2489 Type vdt = vd.ti()->type();
2490 Type vet = vd.e()->type();
2491 if (vdt.enumId() != 0 && vdt.dim() > 0 &&
2492 (vd.e()->isa<ArrayLit>() || vd.e()->isa<Comprehension>() ||
2493 (vd.e()->isa<BinOp>() && vd.e()->cast<BinOp>()->op() == BOT_PLUSPLUS))) {
2494 // Special case: index sets of array literals and comprehensions automatically
2495 // coerce to any enum index set
2496 const std::vector<unsigned int>& enumIds = _env.getArrayEnum(vdt.enumId());
2497 if (enumIds[enumIds.size() - 1] == 0) {
2498 vdt.enumId(0);
2499 } else {
2500 std::vector<unsigned int> nEnumIds(enumIds.size());
2501 for (unsigned int i = 0; i < nEnumIds.size() - 1; i++) {
2502 nEnumIds[i] = 0;
2503 }
2504 nEnumIds[nEnumIds.size() - 1] = enumIds[enumIds.size() - 1];
2505 vdt.enumId(_env.registerArrayEnum(nEnumIds));
2506 }
2507 } else if (vd.ti()->isEnum() && vd.e()->isa<Call>()) {
2508 if (vd.e()->cast<Call>()->id() == "anon_enum") {
2509 vet.enumId(vdt.enumId());
2510 }
2511 }
2512
2513 if (vd.type().isunknown()) {
2514 vd.ti()->type(vet);
2515 vd.type(vet);
2516 } else if (!_env.isSubtype(vet, vdt, true)) {
2517 if (vet == Type::bot(1) && vd.e()->isa<ArrayLit>() &&
2518 vd.e()->cast<ArrayLit>()->size() == 0 &&
2519 vdt.dim() != 0) { // NOLINT(bugprone-branch-clone): see TODO in other branch
2520 // this is okay: assigning an empty array (one-dimensional) to an array variable
2521 } else if (vd.ti()->isEnum() && vet == Type::parsetint()) {
2522 // let's ignore this for now (TODO: add an annotation to make sure only
2523 // compiler-generated ones are accepted)
2524 } else {
2525 const Location& loc = vd.e()->loc().isNonAlloc() ? vd.loc() : vd.e()->loc();
2526 std::ostringstream ss;
2527 ss << "initialisation value for `" << vd.id()->str()
2528 << "' has invalid type-inst: expected `" << vd.ti()->type().toString(_env)
2529 << "', actual `" << vd.e()->type().toString(_env) << "'";
2530 _typeErrors.emplace_back(_env, loc, ss.str());
2531 }
2532 } else {
2533 vd.e(add_coercion(_env, _model, vd.e(), vd.ti()->type())());
2534 }
2535 } else {
2536 assert(!vd.type().isunknown());
2537 }
2538 } else {
2539 vd.type(vd.ti()->type());
2540 vd.id()->type(vd.type());
2541 }
2542 }
2543 /// Visit type inst
2544 void vTypeInst(TypeInst& ti) {
2545 Type tt = ti.type();
2546 bool foundEnum =
2547 ti.ranges().size() > 0 && (ti.domain() != nullptr) && ti.domain()->type().enumId() != 0;
2548 if (ti.ranges().size() > 0) {
2549 bool foundTIId = false;
2550 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
2551 TypeInst* ri = ti.ranges()[i];
2552 assert(ri != nullptr);
2553 if (ri->type().cv()) {
2554 tt.cv(true);
2555 }
2556 if (ri->type().enumId() != 0) {
2557 foundEnum = true;
2558 }
2559 if (ri->type() == Type::top()) {
2560 // if (foundTIId) {
2561 // throw TypeError(_env,ri->loc(),
2562 // "only one type-inst variable allowed in array index");
2563 // } else {
2564 foundTIId = true;
2565 // }
2566 } else if (ri->type() != Type::parint()) {
2567 assert(ri->isa<TypeInst>());
2568 auto* riti = ri->cast<TypeInst>();
2569 if (riti->domain() != nullptr) {
2570 throw TypeError(_env, ri->loc(),
2571 "array index set expression has invalid type, expected `set of int', "
2572 "actual `set of " +
2573 ri->type().toString(_env) + "'");
2574 }
2575 throw TypeError(_env, ri->loc(),
2576 "cannot use `" + ri->type().toString(_env) +
2577 "' as array index set (did you mean `int'?)");
2578 }
2579 }
2580 tt.dim(foundTIId ? -1 : static_cast<int>(ti.ranges().size()));
2581 }
2582 if ((ti.domain() != nullptr) && ti.domain()->type().cv()) {
2583 tt.cv(true);
2584 }
2585 if (ti.domain() != nullptr) {
2586 if (TIId* tiid = ti.domain()->dynamicCast<TIId>()) {
2587 if (tiid->isEnum()) {
2588 tt.bt(Type::BT_INT);
2589 }
2590 } else {
2591 if (ti.domain()->type().ti() != Type::TI_PAR || ti.domain()->type().st() != Type::ST_SET) {
2592 throw TypeError(
2593 _env, ti.domain()->loc().isNonAlloc() ? ti.loc() : ti.domain()->loc(),
2594 "type-inst must be par set but is `" + ti.domain()->type().toString(_env) + "'");
2595 }
2596 if (ti.domain()->type().dim() != 0) {
2597 throw TypeError(_env, ti.domain()->loc(), "type-inst cannot be an array");
2598 }
2599 }
2600 }
2601 if (tt.isunknown() && (ti.domain() != nullptr)) {
2602 assert(ti.domain());
2603 switch (ti.domain()->type().bt()) {
2604 case Type::BT_INT:
2605 case Type::BT_FLOAT:
2606 break;
2607 case Type::BT_BOT: {
2608 Type tidt = ti.domain()->type();
2609 tidt.bt(Type::BT_INT);
2610 ti.domain()->type(tidt);
2611 } break;
2612 default:
2613 throw TypeError(_env, ti.domain()->loc(), "type-inst must be int or float");
2614 }
2615 tt.bt(ti.domain()->type().bt());
2616 tt.enumId(ti.domain()->type().enumId());
2617 } else {
2618 // assert(ti.domain()==NULL || ti.domain()->isa<TIId>());
2619 }
2620 if (foundEnum) {
2621 std::vector<unsigned int> enumIds(ti.ranges().size() + 1);
2622 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
2623 enumIds[i] = ti.ranges()[i]->type().enumId();
2624 }
2625 enumIds[ti.ranges().size()] = ti.domain() != nullptr ? ti.domain()->type().enumId() : 0;
2626 int arrayEnumId = _env.registerArrayEnum(enumIds);
2627 tt.enumId(arrayEnumId);
2628 }
2629
2630 if (tt.st() == Type::ST_SET && tt.ti() == Type::TI_VAR && tt.bt() != Type::BT_INT &&
2631 tt.bt() != Type::BT_TOP) {
2632 throw TypeError(_env, ti.loc(), "var set element types other than `int' not allowed");
2633 }
2634 ti.type(tt);
2635 }
2636 void vTIId(TIId& id) {}
2637};
2638
2639void typecheck(Env& env, Model* origModel, std::vector<TypeError>& typeErrors,
2640 bool ignoreUndefinedParameters, bool allowMultiAssignment, bool isFlatZinc) {
2641 Model* m;
2642 if (!isFlatZinc && origModel == env.model()) {
2643 // Combine all items into single model
2644 auto* combinedModel = new Model;
2645 class Combiner : public ItemVisitor {
2646 public:
2647 Model* m;
2648 Combiner(Model* m0) : m(m0) {}
2649 bool enter(Item* i) const {
2650 if (!i->isa<IncludeI>()) {
2651 m->addItem(i);
2652 }
2653 return true;
2654 }
2655 } _combiner(combinedModel);
2656 iter_items(_combiner, origModel);
2657 env.envi().originalModel = origModel;
2658 env.envi().model = combinedModel;
2659 m = combinedModel;
2660 } else {
2661 m = origModel;
2662 }
2663
2664 // Topological sorting
2665 TopoSorter ts(m);
2666
2667 std::vector<FunctionI*> functionItems;
2668 std::vector<AssignI*> assignItems;
2669 auto* enumItems = new Model;
2670
2671 class TSVFuns : public ItemVisitor {
2672 public:
2673 EnvI& env;
2674 Model* model;
2675 std::vector<FunctionI*>& fis;
2676 std::vector<TypeError>& typeErrors;
2677 TSVFuns(EnvI& env0, Model* model0, std::vector<FunctionI*>& fis0,
2678 std::vector<TypeError>& typeErrors0)
2679 : env(env0), model(model0), fis(fis0), typeErrors(typeErrors0) {}
2680 void vFunctionI(FunctionI* i) {
2681 (void)model->registerFn(env, i);
2682 fis.push_back(i);
2683 // check if one of the arguments is annotated with ::annotated_expression
2684 int reifiedAnnotationIdx = -1;
2685 for (int j = 0; j < i->paramCount(); j++) {
2686 Expression* param = i->param(j);
2687 for (auto* ii : param->ann()) {
2688 if (ii->isa<Id>() && ii->cast<Id>()->v() == constants().ann.annotated_expression->v()) {
2689 if (reifiedAnnotationIdx >= 0) {
2690 typeErrors.emplace_back(
2691 env, param->loc(),
2692 "only one argument can be annotated with annotated_expression");
2693 }
2694 reifiedAnnotationIdx = j;
2695 }
2696 }
2697 }
2698 if (reifiedAnnotationIdx >= 0) {
2699 GCLock lock;
2700 if (i->paramCount() == 1) {
2701 // turn into atomic annotation
2702 auto* ti = new TypeInst(Location().introduce(), Type::ann());
2703 auto* vd = new VarDecl(Location().introduce(), ti, i->id());
2704 vd->ann().add(new Call(Location().introduce(),
2705 constants().ann.mzn_add_annotated_expression, {IntLit::a(0)}));
2706 model->addItem(new VarDeclI(Location().introduce(), vd));
2707 } else {
2708 // turn into annotation function with one argument less
2709 std::vector<VarDecl*> newParams(i->paramCount() - 1);
2710 int j = 0;
2711 for (int k = 0; k < i->paramCount(); k++) {
2712 if (k != reifiedAnnotationIdx) {
2713 newParams[j++] = copy(env, i->param(k))->cast<VarDecl>();
2714 }
2715 }
2716 auto* fi = new FunctionI(Location().introduce(), i->id(), i->ti(), newParams);
2717 fi->ann().add(new Call(Location().introduce(),
2718 constants().ann.mzn_add_annotated_expression,
2719 {IntLit::a(reifiedAnnotationIdx)}));
2720 model->addItem(fi);
2721 (void)model->registerFn(env, fi);
2722 fis.push_back(fi);
2723 }
2724 }
2725 }
2726 } _tsvf(env.envi(), m, functionItems, typeErrors);
2727 iter_items(_tsvf, m);
2728
2729 class TSV0 : public ItemVisitor {
2730 public:
2731 EnvI& env;
2732 TopoSorter& ts;
2733 Model* model;
2734 bool hadSolveItem;
2735 std::vector<AssignI*>& ais;
2736 VarDeclI* objective;
2737 Model* enumis;
2738 bool isFlatZinc;
2739 TSV0(EnvI& env0, TopoSorter& ts0, Model* model0, std::vector<AssignI*>& ais0, Model* enumis0,
2740 bool isFlatZinc0)
2741 : env(env0),
2742 ts(ts0),
2743 model(model0),
2744 hadSolveItem(false),
2745 ais(ais0),
2746 objective(nullptr),
2747 enumis(enumis0),
2748 isFlatZinc(isFlatZinc0) {}
2749 void vAssignI(AssignI* i) { ais.push_back(i); }
2750 void vVarDeclI(VarDeclI* i) {
2751 ts.add(env, i, true, enumis);
2752 // initialise new identifier counter to be larger than existing identifier
2753 if (i->e()->id()->idn() >= 0) {
2754 env.minId(i->e()->id()->idn());
2755 } else if (i->e()->id()->v().beginsWith("X_INTRODUCED_") && i->e()->id()->v().endsWith("_")) {
2756 std::string numId = i->e()->id()->v().substr(std::string("X_INTRODUCED_").size());
2757 if (!numId.empty()) {
2758 numId = numId.substr(0, numId.size() - 1);
2759 if (!numId.empty()) {
2760 int vId = -1;
2761 try {
2762 vId = std::stoi(numId);
2763 } catch (std::exception&) {
2764 }
2765 if (vId >= 0) {
2766 env.minId(vId);
2767 }
2768 }
2769 }
2770 }
2771 }
2772 void vSolveI(SolveI* si) {
2773 if (hadSolveItem) {
2774 throw TypeError(env, si->loc(), "Only one solve item allowed");
2775 }
2776 hadSolveItem = true;
2777 if (!isFlatZinc && (si->e() != nullptr)) {
2778 GCLock lock;
2779 auto* ti = new TypeInst(Location().introduce(), Type());
2780 auto* obj = new VarDecl(Location().introduce(), ti, "_objective", si->e());
2781 si->e(obj->id());
2782 obj->addAnnotation(si->st() == SolveI::ST_MAX ? constants().ctx.pos : constants().ctx.neg);
2783 objective = new VarDeclI(Location().introduce(), obj);
2784 }
2785 }
2786 } _tsv0(env.envi(), ts, m, assignItems, enumItems, isFlatZinc);
2787 iter_items(_tsv0, m);
2788 if (_tsv0.objective != nullptr) {
2789 m->addItem(_tsv0.objective);
2790 ts.add(env.envi(), _tsv0.objective, true, enumItems);
2791 }
2792
2793 for (unsigned int i = 0; i < enumItems->size(); i++) {
2794 if (auto* ai = (*enumItems)[i]->dynamicCast<AssignI>()) {
2795 assignItems.push_back(ai);
2796 } else if (auto* vdi = (*enumItems)[i]->dynamicCast<VarDeclI>()) {
2797 m->addItem(vdi);
2798 ts.add(env.envi(), vdi, false, enumItems);
2799 } else {
2800 auto* fi = (*enumItems)[i]->dynamicCast<FunctionI>();
2801 m->addItem(fi);
2802 (void)m->registerFn(env.envi(), fi);
2803 functionItems.push_back(fi);
2804 }
2805 }
2806
2807 auto* enumItems2 = new Model;
2808
2809 for (auto* ai : assignItems) {
2810 VarDecl* vd = nullptr;
2811 if (env.envi().ignoreUnknownIds) {
2812 try {
2813 vd = ts.get(env.envi(), ai->id(), ai->loc());
2814 } catch (TypeError&) {
2815 }
2816 } else {
2817 vd = ts.get(env.envi(), ai->id(), ai->loc());
2818 }
2819 if (vd != nullptr) {
2820 if (vd->e() != nullptr) {
2821 if (allowMultiAssignment) {
2822 GCLock lock;
2823 m->addItem(new ConstraintI(
2824 ai->loc(),
2825 new BinOp(ai->loc(), new Id(Location().introduce(), ai->id(), vd), BOT_EQ, ai->e())));
2826 } else {
2827 throw TypeError(env.envi(), ai->loc(), "multiple assignment to the same variable");
2828 }
2829 } else {
2830 vd->e(ai->e());
2831 vd->ann().add(constants().ann.rhs_from_assignment);
2832 if (vd->ti()->isEnum()) {
2833 create_enum_mapper(env.envi(), m, vd->ti()->type().enumId(), vd, enumItems2);
2834 }
2835 }
2836 }
2837 ai->remove();
2838 }
2839
2840 for (auto& i : *enumItems2) {
2841 if (auto* vdi = i->dynamicCast<VarDeclI>()) {
2842 m->addItem(vdi);
2843 ts.add(env.envi(), vdi, false, enumItems);
2844 } else {
2845 auto* fi = i->cast<FunctionI>();
2846 m->addItem(fi);
2847 (void)m->registerFn(env.envi(), fi);
2848 functionItems.push_back(fi);
2849 }
2850 }
2851
2852 delete enumItems;
2853 delete enumItems2;
2854
2855 class TSV1 : public ItemVisitor {
2856 public:
2857 EnvI& env;
2858 TopoSorter& ts;
2859 TSV1(EnvI& env0, TopoSorter& ts0) : env(env0), ts(ts0) {}
2860 void vVarDeclI(VarDeclI* i) { ts.run(env, i->e()); }
2861 void vAssignI(AssignI* i) {}
2862 void vConstraintI(ConstraintI* i) { ts.run(env, i->e()); }
2863 void vSolveI(SolveI* i) {
2864 for (ExpressionSetIter it = i->ann().begin(); it != i->ann().end(); ++it) {
2865 ts.run(env, *it);
2866 }
2867 ts.run(env, i->e());
2868 }
2869 void vOutputI(OutputI* i) { ts.run(env, i->e()); }
2870 void vFunctionI(FunctionI* fi) {
2871 ts.run(env, fi->ti());
2872 for (unsigned int i = 0; i < fi->paramCount(); i++) {
2873 ts.run(env, fi->param(i));
2874 }
2875 ts.run(env, fi->capturedAnnotationsVar());
2876 for (ExpressionSetIter it = fi->ann().begin(); it != fi->ann().end(); ++it) {
2877 ts.run(env, *it);
2878 }
2879 ts.scopes.pushFun();
2880 for (unsigned int i = 0; i < fi->paramCount(); i++) {
2881 ts.scopes.add(env, fi->param(i));
2882 }
2883 if (fi->capturedAnnotationsVar() != nullptr) {
2884 ts.scopes.add(env, fi->capturedAnnotationsVar());
2885 }
2886 ts.run(env, fi->e());
2887 ts.scopes.pop();
2888 }
2889 } _tsv1(env.envi(), ts);
2890 iter_items(_tsv1, m);
2891
2892 m->sortFn();
2893
2894 {
2895 struct SortByPayload {
2896 bool operator()(Item* i0, Item* i1) {
2897 if (i0->isa<IncludeI>()) {
2898 return !i1->isa<IncludeI>();
2899 }
2900 if (auto* vdi0 = i0->dynamicCast<VarDeclI>()) {
2901 if (auto* vdi1 = i1->dynamicCast<VarDeclI>()) {
2902 return vdi0->e()->payload() < vdi1->e()->payload();
2903 }
2904 return !i1->isa<IncludeI>();
2905 }
2906 return false;
2907 }
2908 } _sbp;
2909
2910 std::stable_sort(m->begin(), m->end(), _sbp);
2911 }
2912
2913 {
2914 Typer<false> ty(env.envi(), m, typeErrors, ignoreUndefinedParameters);
2915 BottomUpIterator<Typer<false>> bottomUpTyper(ty);
2916 for (auto& decl : ts.decls) {
2917 decl->payload(0);
2918 bottomUpTyper.run(decl->ti());
2919 ty.vVarDecl(*decl);
2920 }
2921 for (auto& functionItem : functionItems) {
2922 bottomUpTyper.run(functionItem->ti());
2923 for (unsigned int j = 0; j < functionItem->paramCount(); j++) {
2924 bottomUpTyper.run(functionItem->param(j));
2925 }
2926 if (functionItem->capturedAnnotationsVar() != nullptr) {
2927 bottomUpTyper.run(functionItem->capturedAnnotationsVar());
2928 }
2929 }
2930 }
2931
2932 m->fixFnMap();
2933
2934 {
2935 Typer<true> ty(env.envi(), m, typeErrors, ignoreUndefinedParameters);
2936 BottomUpIterator<Typer<true>> bottomUpTyper(ty);
2937
2938 class TSV2 : public ItemVisitor {
2939 private:
2940 EnvI& _env;
2941 Model* _m;
2942 BottomUpIterator<Typer<true>>& _bottomUpTyper;
2943 std::vector<TypeError>& _typeErrors;
2944
2945 public:
2946 TSV2(EnvI& env0, Model* m0, BottomUpIterator<Typer<true>>& b,
2947 std::vector<TypeError>& typeErrors)
2948 : _env(env0), _m(m0), _bottomUpTyper(b), _typeErrors(typeErrors) {}
2949 void vVarDeclI(VarDeclI* i) {
2950 _bottomUpTyper.run(i->e());
2951 if (i->e()->ti()->hasTiVariable()) {
2952 std::ostringstream ss;
2953 ss << "type-inst variables not allowed in type-inst for `" << i->e()->id()->str() << "'";
2954 _typeErrors.emplace_back(_env, i->e()->loc(), ss.str());
2955 }
2956 VarDecl* vdi = i->e();
2957 if (vdi->e() == nullptr && vdi->type().isSet() && vdi->type().isvar() &&
2958 vdi->ti()->domain() == nullptr) {
2959 std::ostringstream ss;
2960 ss << "set element type for `" << vdi->id()->str() << "' is not finite";
2961 _typeErrors.emplace_back(_env, vdi->loc(), ss.str());
2962 }
2963 if (i->e()->ann().contains(constants().ann.output_only)) {
2964 if (vdi->e() == nullptr) {
2965 _typeErrors.emplace_back(
2966 _env, vdi->loc(),
2967 "variables annotated with ::output_only must have a right hand side");
2968 } else if (vdi->e()->type().isvar()) {
2969 _typeErrors.emplace_back(_env, vdi->loc(),
2970 "variables annotated with ::output_only must be par");
2971 }
2972 }
2973 }
2974 void vAssignI(AssignI* i) {
2975 _bottomUpTyper.run(i->e());
2976 if (!_env.isSubtype(i->e()->type(), i->decl()->ti()->type(), true)) {
2977 std::ostringstream ss;
2978 ss << "assignment value for `" << i->decl()->id()->str()
2979 << "' has invalid type-inst: expected `" << i->decl()->ti()->type().toString(_env)
2980 << "', actual `" << i->e()->type().toString(_env) << "'";
2981 _typeErrors.emplace_back(_env, i->loc(), ss.str());
2982 // Assign to "true" constant to avoid generating further errors that the parameter
2983 // is undefined
2984 i->decl()->e(constants().literalTrue);
2985 }
2986 }
2987 void vConstraintI(ConstraintI* i) {
2988 _bottomUpTyper.run(i->e());
2989 if (!_env.isSubtype(i->e()->type(), Type::varbool(), true)) {
2990 throw TypeError(_env, i->loc(),
2991 "invalid type of constraint, expected `" +
2992 Type::varbool().toString(_env) + "', actual `" +
2993 i->e()->type().toString(_env) + "'");
2994 }
2995 }
2996 void vSolveI(SolveI* i) {
2997 for (ExpressionSetIter it = i->ann().begin(); it != i->ann().end(); ++it) {
2998 _bottomUpTyper.run(*it);
2999 if (!(*it)->type().isAnn()) {
3000 throw TypeError(_env, (*it)->loc(),
3001 "expected annotation, got `" + (*it)->type().toString(_env) + "'");
3002 }
3003 }
3004 _bottomUpTyper.run(i->e());
3005 if (i->e() != nullptr) {
3006 Type et = i->e()->type();
3007 if (et.isbool()) {
3008 Type target_t = Type::varint();
3009 if (et.isOpt()) {
3010 target_t.ot(Type::OT_OPTIONAL);
3011 }
3012 i->e(add_coercion(_env, _env.model, i->e(), target_t)());
3013 }
3014
3015 bool needOptCoercion = et.isOpt() && et.isint();
3016 if (needOptCoercion) {
3017 et.ot(Type::OT_PRESENT);
3018 }
3019
3020 if (!(_env.isSubtype(et, Type::varint(), true) ||
3021 _env.isSubtype(et, Type::varfloat(), true))) {
3022 throw TypeError(_env, i->e()->loc(),
3023 "objective has invalid type, expected int or float, actual `" +
3024 et.toString(_env) + "'");
3025 }
3026
3027 if (needOptCoercion) {
3028 GCLock lock;
3029 std::vector<Expression*> args(2);
3030 args[0] = i->e();
3031 args[1] = constants().boollit(i->st() == SolveI::ST_MAX);
3032 Call* c = new Call(Location().introduce(), ASTString("objective_deopt_"), args);
3033 c->decl(_env.model->matchFn(_env, c, false));
3034 assert(c->decl());
3035 c->type(et);
3036 i->e(c);
3037 }
3038 }
3039 }
3040 void vOutputI(OutputI* i) {
3041 for (ExpressionSetIter it = i->ann().begin(); it != i->ann().end(); ++it) {
3042 _bottomUpTyper.run(*it);
3043 if (!(*it)->type().isAnn()) {
3044 throw TypeError(_env, (*it)->loc(),
3045 "expected annotation, got `" + (*it)->type().toString(_env) + "'");
3046 }
3047 }
3048 _bottomUpTyper.run(i->e());
3049 if (i->e()->type() != Type::parstring(1) && i->e()->type() != Type::bot(1)) {
3050 throw TypeError(_env, i->e()->loc(),
3051 "invalid type in output item, expected `" +
3052 Type::parstring(1).toString(_env) + "', actual `" +
3053 i->e()->type().toString(_env) + "'");
3054 }
3055 }
3056 void vFunctionI(FunctionI* i) {
3057 for (ExpressionSetIter it = i->ann().begin(); it != i->ann().end(); ++it) {
3058 _bottomUpTyper.run(*it);
3059 if (!(*it)->type().isAnn()) {
3060 throw TypeError(_env, (*it)->loc(),
3061 "expected annotation, got `" + (*it)->type().toString(_env) + "'");
3062 }
3063 }
3064 _bottomUpTyper.run(i->ti());
3065 _bottomUpTyper.run(i->e());
3066 if ((i->e() != nullptr) && !_env.isSubtype(i->e()->type(), i->ti()->type(), true)) {
3067 throw TypeError(_env, i->e()->loc(),
3068 "return type of function does not match body, declared type is `" +
3069 i->ti()->type().toString(_env) + "', body type is `" +
3070 i->e()->type().toString(_env) + "'");
3071 }
3072 if ((i->e() != nullptr) && i->e()->type().isPar() && i->ti()->type().isvar()) {
3073 // this is a par function declared as var, so change declared return type
3074 Type i_t = i->ti()->type();
3075 i_t.ti(Type::TI_PAR);
3076 i->ti()->type(i_t);
3077 }
3078 if (i->e() != nullptr) {
3079 i->e(add_coercion(_env, _m, i->e(), i->ti()->type())());
3080 }
3081 }
3082 } _tsv2(env.envi(), m, bottomUpTyper, typeErrors);
3083 iter_items(_tsv2, m);
3084 }
3085
3086 class TSV3 : public ItemVisitor {
3087 public:
3088 EnvI& env;
3089 Model* m;
3090 OutputI* outputItem;
3091 TSV3(EnvI& env0, Model* m0) : env(env0), m(m0), outputItem(nullptr) {}
3092 void vAssignI(AssignI* i) { i->decl()->e(add_coercion(env, m, i->e(), i->decl()->type())()); }
3093 void vOutputI(OutputI* oi) {
3094 if (outputItem == nullptr) {
3095 outputItem = oi;
3096 } else {
3097 GCLock lock;
3098 auto* bo = new BinOp(Location().introduce(), outputItem->e(), BOT_PLUSPLUS, oi->e());
3099 bo->type(Type::parstring(1));
3100 outputItem->e(bo);
3101 oi->remove();
3102 m->setOutputItem(outputItem);
3103 }
3104 }
3105 } _tsv3(env.envi(), m);
3106 if (typeErrors.empty()) {
3107 iter_items(_tsv3, m);
3108 }
3109
3110 // Create a par version of each function that returns par and
3111 // that has a body that can be made par
3112 std::unordered_map<FunctionI*, std::pair<bool, std::vector<FunctionI*>>> fnsToMakePar;
3113 for (auto& f : m->functions()) {
3114 if (f.id() == "mzn_reverse_map_var") {
3115 continue;
3116 }
3117 if (f.e() != nullptr && f.ti()->type().bt() != Type::BT_ANN) {
3118 bool foundVar = false;
3119 for (int i = 0; i < f.paramCount(); i++) {
3120 if (f.param(i)->type().isvar()) {
3121 foundVar = true;
3122 break;
3123 }
3124 }
3125 if (foundVar) {
3126 // create par version of parameter types
3127 std::vector<Type> tv;
3128 for (int i = 0; i < f.paramCount(); i++) {
3129 Type t = f.param(i)->type();
3130 t.cv(false);
3131 t.ti(Type::TI_PAR);
3132 tv.push_back(t);
3133 }
3134 // check if specialised par version of function already exists
3135 FunctionI* fi_par = m->matchFn(env.envi(), f.id(), tv, false);
3136 bool parIsUsable = false;
3137 if (fi_par != nullptr) {
3138 bool foundVar = false;
3139 for (int i = 0; i < fi_par->paramCount(); i++) {
3140 if (fi_par->param(i)->type().isvar()) {
3141 foundVar = true;
3142 break;
3143 }
3144 }
3145 parIsUsable = !foundVar;
3146 }
3147 if (!parIsUsable) {
3148 // check if body of f doesn't contain any free variables in lets,
3149 // all calls in the body have par versions available,
3150 // and all toplevel identifiers used in the body of f are par
3151 class CheckParBody : public EVisitor {
3152 public:
3153 EnvI& env;
3154 Model* m;
3155 CheckParBody(EnvI& env0, Model* m0) : env(env0), m(m0) {}
3156 bool isPar = true;
3157 std::vector<FunctionI*> deps;
3158 bool enter(Expression* e) const {
3159 // if we have already found a var, don't continue
3160 return isPar;
3161 }
3162 void vId(const Id& ident) {
3163 if (ident.decl() != nullptr && ident.type().isvar() && ident.decl()->toplevel()) {
3164 isPar = false;
3165 }
3166 }
3167 void vLet(const Let& let) {
3168 // check if any of the declared variables does not have a RHS
3169 for (auto* e : let.let()) {
3170 if (auto* vd = e->dynamicCast<VarDecl>()) {
3171 if (vd->e() == nullptr) {
3172 isPar = false;
3173 break;
3174 }
3175 }
3176 }
3177 }
3178 void vCall(const Call& c) {
3179 if (!c.type().isAnn()) {
3180 FunctionI* decl = c.decl();
3181 // create par version of parameter types
3182 std::vector<Type> tv;
3183 for (int i = 0; i < decl->paramCount(); i++) {
3184 Type t = decl->param(i)->type();
3185 t.cv(false);
3186 t.ti(Type::TI_PAR);
3187 tv.push_back(t);
3188 }
3189 // check if specialised par version of function already exists
3190 FunctionI* decl_par = m->matchFn(env, decl->id(), tv, false);
3191 bool parIsUsable = decl_par->ti()->type().isPar();
3192 if (parIsUsable && decl_par->e() == nullptr && decl_par->fromStdLib()) {
3193 parIsUsable = true;
3194 } else if (parIsUsable) {
3195 bool foundVar = false;
3196 for (int i = 0; i < decl_par->paramCount(); i++) {
3197 if (decl_par->param(i)->type().isvar()) {
3198 foundVar = true;
3199 break;
3200 }
3201 }
3202 parIsUsable = !foundVar;
3203 }
3204 if (!parIsUsable) {
3205 deps.push_back(decl_par);
3206 }
3207 }
3208 }
3209 } cpb(env.envi(), m);
3210 top_down(cpb, f.e());
3211 if (cpb.isPar) {
3212 fnsToMakePar.insert({&f, {false, cpb.deps}});
3213 }
3214 } else {
3215 fnsToMakePar.insert({fi_par, {true, std::vector<FunctionI*>()}});
3216 }
3217 }
3218 }
3219 }
3220
3221 // Repeatedly remove functions whose dependencies cannot be made par
3222 bool didRemove;
3223 do {
3224 didRemove = false;
3225 std::vector<FunctionI*> toRemove;
3226 for (auto& p : fnsToMakePar) {
3227 for (auto* dep : p.second.second) {
3228 if (fnsToMakePar.find(dep) == fnsToMakePar.end()) {
3229 toRemove.push_back(p.first);
3230 }
3231 }
3232 }
3233 if (!toRemove.empty()) {
3234 didRemove = true;
3235 for (auto* p : toRemove) {
3236 fnsToMakePar.erase(p);
3237 }
3238 }
3239 } while (didRemove);
3240
3241 // Create par versions of remaining functions
3242 if (!fnsToMakePar.empty()) {
3243 // First step: copy and register functions
3244 std::vector<FunctionI*> parFunctions;
3245 CopyMap parCopyMap;
3246 // Step 1a: enter all global declarations into copy map
3247 class EnterGlobalDecls : public EVisitor {
3248 public:
3249 CopyMap& cm;
3250 EnterGlobalDecls(CopyMap& cm0) : cm(cm0) {}
3251 void vId(Id& ident) {
3252 if (ident.decl() != nullptr && ident.decl()->toplevel()) {
3253 cm.insert(ident.decl(), ident.decl());
3254 }
3255 }
3256 } _egd(parCopyMap);
3257 for (auto& p : fnsToMakePar) {
3258 if (!p.second.first) {
3259 for (unsigned int i = 0; i < p.first->paramCount(); i++) {
3260 top_down(_egd, p.first->param(i));
3261 }
3262 if (p.first->capturedAnnotationsVar() != nullptr) {
3263 top_down(_egd, p.first->capturedAnnotationsVar());
3264 }
3265 for (ExpressionSetIter i = p.first->ann().begin(); i != p.first->ann().end(); ++i) {
3266 top_down(_egd, *i);
3267 }
3268 top_down(_egd, p.first->e());
3269 }
3270 }
3271
3272 // Step 1b: copy functions
3273 for (auto& p : fnsToMakePar) {
3274 if (!p.second.first) {
3275 GCLock lock;
3276 auto* cp = copy(env.envi(), parCopyMap, p.first)->cast<FunctionI>();
3277 for (int i = 0; i < cp->paramCount(); i++) {
3278 VarDecl* v = cp->param(i);
3279 Type vt = v->ti()->type();
3280 vt.ti(Type::TI_PAR);
3281 v->ti()->type(vt);
3282 v->type(vt);
3283 }
3284 Type cpt(cp->ti()->type());
3285 cpt.ti(Type::TI_PAR);
3286 cp->ti()->type(cpt);
3287 bool didRegister = m->registerFn(env.envi(), cp, true, false);
3288 if (didRegister) {
3289 m->addItem(cp);
3290 parFunctions.push_back(cp);
3291 }
3292 }
3293 }
3294
3295 // Second step: make function bodies par
3296 // (needs to happen in a separate second step so that
3297 // matchFn will find the correct par function from first step)
3298 class MakeFnPar : public EVisitor {
3299 public:
3300 EnvI& env;
3301 Model* m;
3302 MakeFnPar(EnvI& env0, Model* m0) : env(env0), m(m0) {}
3303 static bool enter(Expression* e) {
3304 Type t(e->type());
3305 t.ti(Type::TI_PAR);
3306 t.cv(false);
3307 e->type(t);
3308 return true;
3309 }
3310 void vCall(Call& c) {
3311 FunctionI* decl = m->matchFn(env, &c, false);
3312 c.decl(decl);
3313 }
3314 void vBinOp(BinOp& bo) {
3315 if (bo.decl() != nullptr) {
3316 std::vector<Type> ta(2);
3317 ta[0] = bo.lhs()->type();
3318 ta[1] = bo.rhs()->type();
3319 FunctionI* decl = m->matchFn(env, bo.opToString(), ta, false);
3320 bo.decl(decl);
3321 }
3322 }
3323 void vUnOp(UnOp& uo) {
3324 if (uo.decl() != nullptr) {
3325 std::vector<Type> ta(1);
3326 ta[0] = uo.e()->type();
3327 FunctionI* decl = m->matchFn(env, uo.opToString(), ta, false);
3328 uo.decl(decl);
3329 }
3330 }
3331 } _mfp(env.envi(), m);
3332
3333 for (auto* p : parFunctions) {
3334 bottom_up(_mfp, p->e());
3335 }
3336 }
3337
3338 try {
3339 m->checkFnOverloading(env.envi());
3340 } catch (TypeError& e) {
3341 typeErrors.push_back(e);
3342 }
3343
3344 for (auto& decl : ts.decls) {
3345 if (decl->toplevel() && decl->type().isPar() && !decl->type().isAnn() && decl->e() == nullptr) {
3346 if (decl->type().isOpt() && decl->type().dim() == 0) {
3347 decl->e(constants().absent);
3348 decl->addAnnotation(constants().ann.mzn_was_undefined);
3349 } else if (!ignoreUndefinedParameters) {
3350 std::ostringstream ss;
3351 ss << " symbol error: variable `" << decl->id()->str()
3352 << "' must be defined (did you forget to specify a data file?)";
3353 typeErrors.emplace_back(env.envi(), decl->loc(), ss.str());
3354 }
3355 }
3356 if (decl->ti()->isEnum()) {
3357 decl->ti()->setIsEnum(false);
3358 Type vdt = decl->ti()->type();
3359 vdt.enumId(0);
3360 decl->ti()->type(vdt);
3361 }
3362 }
3363
3364 for (auto vd_k : env.envi().checkVars) {
3365 try {
3366 VarDecl* vd;
3367 try {
3368 vd = ts.get(env.envi(), vd_k()->cast<VarDecl>()->id()->str(),
3369 vd_k()->cast<VarDecl>()->loc());
3370 } catch (TypeError&) {
3371 if (vd_k()->cast<VarDecl>()->type().isvar()) {
3372 continue; // var can be undefined
3373 }
3374 throw;
3375 }
3376 vd->ann().add(constants().ann.mzn_check_var);
3377 if (vd->type().enumId() != 0) {
3378 GCLock lock;
3379 std::vector<unsigned int> enumIds({vd->type().enumId()});
3380 if (vd->type().dim() > 0) {
3381 enumIds = env.envi().getArrayEnum(vd->type().enumId());
3382 }
3383 std::vector<Expression*> enumIds_a(enumIds.size());
3384 for (unsigned int i = 0; i < enumIds.size(); i++) {
3385 if (enumIds[i] != 0) {
3386 enumIds_a[i] = env.envi().getEnum(enumIds[i])->e()->id();
3387 } else {
3388 enumIds_a[i] = new SetLit(Location().introduce(), std::vector<Expression*>());
3389 }
3390 }
3391 auto* enumIds_al = new ArrayLit(Location().introduce(), enumIds_a);
3392 enumIds_al->type(Type::parsetint(1));
3393 std::vector<Expression*> args({enumIds_al});
3394 Call* checkEnum =
3395 new Call(Location().introduce(), constants().ann.mzn_check_enum_var, args);
3396 checkEnum->type(Type::ann());
3397 checkEnum->decl(env.envi().model->matchFn(env.envi(), checkEnum, false));
3398 vd->ann().add(checkEnum);
3399 }
3400 Type vdktype = vd_k()->type();
3401 vdktype.ti(Type::TI_VAR);
3402 if (!vd_k()->type().isSubtypeOf(vd->type(), false)) {
3403 std::ostringstream ss;
3404 ss << "Solution checker requires `" << vd->id()->str() << "' to be of type `"
3405 << vdktype.toString(env.envi()) << "'";
3406 typeErrors.emplace_back(env.envi(), vd->loc(), ss.str());
3407 }
3408 } catch (TypeError& e) {
3409 typeErrors.emplace_back(env.envi(), e.loc(),
3410 e.msg() + " (required by solution checker model)");
3411 }
3412 }
3413}
3414
3415void typecheck(Env& env, Model* m, AssignI* ai) {
3416 std::vector<TypeError> typeErrors;
3417 Typer<true> ty(env.envi(), m, typeErrors, false);
3418 BottomUpIterator<Typer<true>> bottomUpTyper(ty);
3419 bottomUpTyper.run(ai->e());
3420 if (!typeErrors.empty()) {
3421 throw typeErrors[0];
3422 }
3423 if (!env.envi().isSubtype(ai->e()->type(), ai->decl()->ti()->type(), true)) {
3424 std::ostringstream ss;
3425 ss << "assignment value for `" << ai->decl()->id()->str()
3426 << "' has invalid type-inst: expected `" << ai->decl()->ti()->type().toString(env.envi())
3427 << "', actual `" << ai->e()->type().toString(env.envi()) << "'";
3428 throw TypeError(env.envi(), ai->e()->loc(), ss.str());
3429 }
3430}
3431
3432void output_var_desc_json(Env& env, VarDecl* vd, std::ostream& os, bool extra = false) {
3433 os << " \"" << *vd->id() << "\" : {";
3434 os << "\"type\" : ";
3435 switch (vd->type().bt()) {
3436 case Type::BT_INT:
3437 os << "\"int\"";
3438 break;
3439 case Type::BT_BOOL:
3440 os << "\"bool\"";
3441 break;
3442 case Type::BT_FLOAT:
3443 os << "\"float\"";
3444 break;
3445 case Type::BT_STRING:
3446 os << "\"string\"";
3447 break;
3448 case Type::BT_ANN:
3449 os << "\"ann\"";
3450 break;
3451 default:
3452 os << "\"?\"";
3453 break;
3454 }
3455 if (vd->type().ot() == Type::OT_OPTIONAL) {
3456 os << ", \"optional\" : true";
3457 }
3458 if (vd->type().st() == Type::ST_SET) {
3459 os << ", \"set\" : true";
3460 }
3461 if (vd->type().dim() > 0) {
3462 os << ", \"dim\" : " << vd->type().dim();
3463
3464 if (extra) {
3465 os << ", \"dims\" : [";
3466 bool had_dim = false;
3467 ASTExprVec<TypeInst> ranges = vd->ti()->ranges();
3468 for (auto& range : ranges) {
3469 if (range->type().enumId() > 0) {
3470 os << (had_dim ? "," : "") << "\""
3471 << *env.envi().getEnum(range->type().enumId())->e()->id() << "\"";
3472 } else {
3473 os << (had_dim ? "," : "") << "\"int\"";
3474 }
3475 had_dim = true;
3476 }
3477 os << "]";
3478
3479 if (vd->type().enumId() > 0) {
3480 const std::vector<unsigned int>& enumIds = env.envi().getArrayEnum(vd->type().enumId());
3481 if (enumIds.back() > 0) {
3482 os << ", \"enum_type\" : \"" << *env.envi().getEnum(enumIds.back())->e()->id() << "\"";
3483 }
3484 }
3485 }
3486
3487 } else {
3488 if (extra) {
3489 if (vd->type().enumId() > 0) {
3490 os << ", \"enum_type\" : \"" << *env.envi().getEnum(vd->type().enumId())->e()->id() << "\"";
3491 }
3492 }
3493 }
3494 os << "}";
3495}
3496
3497void output_model_variable_types(Env& env, Model* m, std::ostream& os,
3498 const std::vector<std::string>& skipDirs) {
3499 class VInfVisitor : public ItemVisitor {
3500 public:
3501 Env& env;
3502 const std::vector<std::string>& skipDirs;
3503 bool hadVar;
3504 bool hadEnum;
3505 std::ostringstream ossVars;
3506 std::ostringstream ossEnums;
3507 VInfVisitor(Env& env0, const std::vector<std::string>& skipDirs0)
3508 : env(env0), skipDirs(skipDirs0), hadVar(false), hadEnum(false) {}
3509 bool enter(Item* i) {
3510 if (auto* ii = i->dynamicCast<IncludeI>()) {
3511 std::string prefix =
3512 ii->m()->filepath().substr(0, ii->m()->filepath().size() - ii->f().size());
3513 for (const auto& skip_dir : skipDirs) {
3514 if (prefix.substr(0, skip_dir.size()) == skip_dir) {
3515 return false;
3516 }
3517 }
3518 }
3519 return true;
3520 }
3521 void vVarDeclI(VarDeclI* vdi) {
3522 if (!vdi->e()->type().isAnn() && !vdi->e()->ti()->isEnum()) {
3523 if (hadVar) {
3524 ossVars << ",\n";
3525 }
3526 output_var_desc_json(env, vdi->e(), ossVars, true);
3527 hadVar = true;
3528 } else if (vdi->e()->type().st() == Type::ST_SET && vdi->e()->type().enumId() != 0 &&
3529 !vdi->e()->type().isAnn()) {
3530 if (hadEnum) {
3531 ossEnums << ", ";
3532 }
3533 ossEnums << "\"" << *env.envi().getEnum(vdi->e()->type().enumId())->e()->id() << "\"";
3534 hadEnum = true;
3535 }
3536 }
3537 } _vinf(env, skipDirs);
3538 iter_items(_vinf, m);
3539 os << "{\"var_types\": {";
3540 os << "\n \"vars\": {\n" << _vinf.ossVars.str() << "\n },";
3541 os << "\n \"enums\": [" << _vinf.ossEnums.str() << "]\n";
3542 os << "}}\n";
3543}
3544
3545void output_model_interface(Env& env, Model* m, std::ostream& os,
3546 const std::vector<std::string>& skipDirs) {
3547 class IfcVisitor : public ItemVisitor {
3548 public:
3549 Env& env;
3550 const std::vector<std::string>& skipDirs;
3551 bool hadInput;
3552 bool hadOutput;
3553 bool hadIncludedFiles;
3554 bool hadAddToOutput = false;
3555 std::ostringstream ossInput;
3556 std::ostringstream ossOutput;
3557 std::ostringstream ossIncludedFiles;
3558 std::string method;
3559 bool outputItem;
3560 IfcVisitor(Env& env0, const std::vector<std::string>& skipDirs0)
3561 : env(env0),
3562 skipDirs(skipDirs0),
3563 hadInput(false),
3564 hadOutput(false),
3565 hadIncludedFiles(false),
3566 method("sat"),
3567 outputItem(false) {}
3568 bool enter(Item* i) {
3569 if (auto* ii = i->dynamicCast<IncludeI>()) {
3570 std::string prefix =
3571 ii->m()->filepath().substr(0, ii->m()->filepath().size() - ii->f().size());
3572 for (const auto& skip_dir : skipDirs) {
3573 if (prefix.substr(0, skip_dir.size()) == skip_dir) {
3574 return false;
3575 }
3576 }
3577 if (hadIncludedFiles) {
3578 ossIncludedFiles << ",\n";
3579 }
3580 ossIncludedFiles << " \"" << Printer::escapeStringLit(ii->m()->filepath()) << "\"";
3581 hadIncludedFiles = true;
3582 }
3583 return true;
3584 }
3585 void vVarDeclI(VarDeclI* vdi) {
3586 VarDecl* vd = vdi->e();
3587 if (vd->type().isPar() && !vd->type().isAnn() &&
3588 (vd->e() == nullptr || (vd->e() == constants().absent &&
3589 vd->ann().contains(constants().ann.mzn_was_undefined)))) {
3590 if (hadInput) {
3591 ossInput << ",\n";
3592 }
3593 output_var_desc_json(env, vd, ossInput);
3594 hadInput = true;
3595 } else {
3596 bool process_var = false;
3597 if (vd->ann().contains(constants().ann.add_to_output)) {
3598 if (!hadAddToOutput) {
3599 ossOutput.str("");
3600 hadOutput = false;
3601 }
3602 hadAddToOutput = true;
3603 process_var = true;
3604 } else if (!hadAddToOutput) {
3605 process_var =
3606 vd->type().isvar() &&
3607 (vd->e() == nullptr || vd->ann().contains(constants().ann.rhs_from_assignment));
3608 }
3609 if (process_var) {
3610 if (hadOutput) {
3611 ossOutput << ",\n";
3612 }
3613 output_var_desc_json(env, vd, ossOutput);
3614 hadOutput = true;
3615 }
3616 }
3617 }
3618 void vSolveI(SolveI* si) {
3619 switch (si->st()) {
3620 case SolveI::ST_MIN:
3621 method = "min";
3622 break;
3623 case SolveI::ST_MAX:
3624 method = "max";
3625 break;
3626 case SolveI::ST_SAT:
3627 method = "sat";
3628 break;
3629 }
3630 }
3631 void vOutputI(OutputI* oi) { outputItem = true; }
3632 } _ifc(env, skipDirs);
3633 iter_items(_ifc, m);
3634 os << "{\n \"input\" : {\n"
3635 << _ifc.ossInput.str() << "\n },\n \"output\" : {\n"
3636 << _ifc.ossOutput.str() << "\n }";
3637 os << ",\n \"method\": \"";
3638 os << _ifc.method;
3639 os << "\"";
3640 os << ",\n \"has_output_item\": " << (_ifc.outputItem ? "true" : "false");
3641 os << ",\n \"included_files\": [\n" << _ifc.ossIncludedFiles.str() << "\n ]";
3642 os << "\n}\n";
3643}
3644
3645std::string create_enum_to_string_name(Id* ident, const std::string& prefix) {
3646 std::ostringstream ss;
3647 if (ident->str().c_str()[0] == '\'') {
3648 ss << "'" << prefix << ident->str().substr(1);
3649 } else {
3650 ss << prefix << *ident;
3651 }
3652 return ss.str();
3653}
3654
3655} // namespace MiniZinc