this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Pierre Wilke <wilke.pierre@gmail.com>
6 * Guido Tack <guido.tack@monash.edu>
7 */
8
9/* This Source Code Form is subject to the terms of the Mozilla Public
10 * License, v. 2.0. If a copy of the MPL was not distributed with this
11 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
12
13#include <minizinc/astexception.hh>
14#include <minizinc/hash.hh>
15#include <minizinc/iter.hh>
16#include <minizinc/model.hh>
17#include <minizinc/prettyprinter.hh>
18
19#include <iomanip>
20#include <limits>
21#include <map>
22#include <sstream>
23#include <string>
24#include <vector>
25
26namespace MiniZinc {
27
28int precedence(const Expression* e) {
29 if (const BinOp* bo = e->dyn_cast<BinOp>()) {
30 switch (bo->op()) {
31 case BOT_EQUIV:
32 return 1200;
33 case BOT_IMPL:
34 return 1100;
35 case BOT_RIMPL:
36 return 1100;
37 case BOT_OR:
38 return 1000;
39 case BOT_XOR:
40 return 1000;
41 case BOT_AND:
42 return 900;
43 case BOT_LE:
44 return 800;
45 case BOT_LQ:
46 return 800;
47 case BOT_GR:
48 return 800;
49 case BOT_GQ:
50 return 800;
51 case BOT_EQ:
52 return 800;
53 case BOT_NQ:
54 return 800;
55 case BOT_IN:
56 return 700;
57 case BOT_SUBSET:
58 return 700;
59 case BOT_SUPERSET:
60 return 700;
61 case BOT_UNION:
62 return 600;
63 case BOT_DIFF:
64 return 600;
65 case BOT_SYMDIFF:
66 return 600;
67 case BOT_DOTDOT:
68 return 500;
69 case BOT_PLUS:
70 return 400;
71 case BOT_MINUS:
72 return 400;
73 case BOT_MULT:
74 return 300;
75 case BOT_IDIV:
76 return 300;
77 case BOT_MOD:
78 return 300;
79 case BOT_DIV:
80 return 300;
81 case BOT_INTERSECT:
82 return 300;
83 case BOT_POW:
84 return 200;
85 case BOT_PLUSPLUS:
86 return 200;
87 default:
88 assert(false);
89 return -1;
90 }
91
92 } else if (e->isa<Let>()) {
93 return 1300;
94
95 } else {
96 return 0;
97 }
98}
99
100enum Assoc { AS_LEFT, AS_RIGHT, AS_NONE };
101
102Assoc assoc(const BinOp* bo) {
103 switch (bo->op()) {
104 case BOT_LE:
105 case BOT_LQ:
106 case BOT_GR:
107 case BOT_GQ:
108 case BOT_NQ:
109 case BOT_EQ:
110 case BOT_IN:
111 case BOT_SUBSET:
112 case BOT_SUPERSET:
113 case BOT_DOTDOT:
114 return AS_NONE;
115 case BOT_PLUSPLUS:
116 return AS_RIGHT;
117 default:
118 return AS_LEFT;
119 }
120}
121
122enum Parentheses { PN_LEFT = 1, PN_RIGHT = 2 };
123
124Parentheses needParens(const BinOp* bo, const Expression* left, const Expression* right) {
125 int pbo = precedence(bo);
126 int pl = precedence(left);
127 int pr = precedence(right);
128 int ret = (pbo < pl) || (pbo == pl && assoc(bo) != AS_LEFT);
129 ret += 2 * ((pbo < pr) || (pbo == pr && assoc(bo) != AS_RIGHT));
130 return static_cast<Parentheses>(ret);
131}
132
133std::string Printer::escapeStringLit(const ASTString& s) {
134 const char* sc = s.c_str();
135 std::ostringstream ret;
136 for (unsigned int i = 0; i < s.size(); i++) {
137 switch (sc[i]) {
138 case '\n':
139 ret << "\\n";
140 break;
141 case '\t':
142 ret << "\\t";
143 break;
144 case '"':
145 ret << "\\\"";
146 break;
147 case '\\':
148 ret << "\\\\";
149 break;
150 default:
151 ret << sc[i];
152 }
153 }
154 return ret.str();
155}
156
157void ppFloatVal(std::ostream& os, const FloatVal& fv, bool hexFloat) {
158 std::ostringstream oss;
159 if (fv.isFinite()) {
160 if (hexFloat) {
161 throw InternalError("disabled due to hexfloat being not supported by g++ 4.9");
162 // std::hexfloat(oss);
163 oss << fv.toDouble();
164 os << oss.str();
165 } else {
166 oss << std::setprecision(std::numeric_limits<double>::digits10 + 1);
167 oss << fv;
168 if (oss.str().find("e") == std::string::npos && oss.str().find(".") == std::string::npos)
169 oss << ".0";
170 os << oss.str();
171 }
172 } else {
173 if (fv.isPlusInfinity())
174 os << "infinity";
175 else
176 os << "-infinity";
177 }
178}
179
180class PlainPrinter {
181public:
182 EnvI* env;
183 std::ostream& os;
184 bool _flatZinc;
185 PlainPrinter(std::ostream& os0, bool flatZinc, EnvI* env0)
186 : env(env0), os(os0), _flatZinc(flatZinc) {}
187
188 void p(const Type& type, const Expression* e) {
189 switch (type.ti()) {
190 case Type::TI_PAR:
191 break;
192 case Type::TI_VAR:
193 os << "var ";
194 break;
195 }
196 if (type.ot() == Type::OT_OPTIONAL) os << "opt ";
197 if (type.st() == Type::ST_SET) os << "set of ";
198 if (e == NULL) {
199 switch (type.bt()) {
200 case Type::BT_INT:
201 os << "int";
202 break;
203 case Type::BT_BOOL:
204 os << "bool";
205 break;
206 case Type::BT_FLOAT:
207 os << "float";
208 break;
209 case Type::BT_STRING:
210 os << "string";
211 break;
212 case Type::BT_ANN:
213 os << "ann";
214 break;
215 case Type::BT_BOT:
216 os << "bot";
217 break;
218 case Type::BT_TOP:
219 os << "top";
220 break;
221 case Type::BT_UNKNOWN:
222 os << "???";
223 break;
224 }
225 } else {
226 p(e);
227 }
228 }
229
230 void p(const Annotation& ann) {
231 for (ExpressionSetIter it = ann.begin(); it != ann.end(); ++it) {
232 os << ":: ";
233 p(*it);
234 }
235 }
236
237 void p(const Expression* e) {
238 if (e == NULL) return;
239 switch (e->eid()) {
240 case Expression::E_INTLIT:
241 os << e->cast<IntLit>()->v();
242 break;
243 case Expression::E_FLOATLIT: {
244 ppFloatVal(os, e->cast<FloatLit>()->v());
245 } break;
246 case Expression::E_SETLIT: {
247 const SetLit& sl = *e->cast<SetLit>();
248 if (sl.isv()) {
249 if (sl.isv()->size() == 0) {
250 os << (_flatZinc ? "1..0" : "{}");
251 } else if (sl.isv()->size() == 1) {
252 os << sl.isv()->min(0) << ".." << sl.isv()->max(0);
253 } else {
254 if (!sl.isv()->min(0).isFinite())
255 os << sl.isv()->min(0) << ".." << sl.isv()->max(0) << "++";
256 os << "{";
257 for (IntSetRanges isr(sl.isv()); isr();) {
258 if (isr.min().isFinite() && isr.max().isFinite()) {
259 for (IntVal i = isr.min(); i <= isr.max(); i++) {
260 os << i;
261 if (i < isr.max()) os << ",";
262 }
263 ++isr;
264 if (isr()) os << ",";
265 }
266 }
267 os << "}";
268 if (!sl.isv()->max(sl.isv()->size() - 1).isFinite())
269 os << "++" << sl.isv()->min(sl.isv()->size() - 1) << ".."
270 << sl.isv()->max(sl.isv()->size() - 1);
271 }
272 } else if (sl.fsv()) {
273 if (sl.fsv()->size() == 0) {
274 os << (_flatZinc ? "1.0..0.0" : "{}");
275 } else if (sl.fsv()->size() == 1) {
276 ppFloatVal(os, sl.fsv()->min(0));
277 os << "..";
278 ppFloatVal(os, sl.fsv()->max(0));
279 } else {
280 bool allSingleton = true;
281 for (FloatSetRanges isr(sl.fsv()); isr(); ++isr) {
282 if (isr.min() != isr.max()) {
283 allSingleton = false;
284 break;
285 }
286 }
287 if (allSingleton) {
288 os << "{";
289 bool first = true;
290 for (FloatSetRanges isr(sl.fsv()); isr(); ++isr) {
291 if (!first) os << ",";
292 first = false;
293 ppFloatVal(os, isr.min());
294 }
295 os << "}";
296 } else {
297 bool first = true;
298 for (FloatSetRanges isr(sl.fsv()); isr(); ++isr) {
299 if (!first) os << "++";
300 first = false;
301 ppFloatVal(os, isr.min());
302 os << "..";
303 ppFloatVal(os, isr.max());
304 }
305 }
306 }
307 } else {
308 os << "{";
309 for (unsigned int i = 0; i < sl.v().size(); i++) {
310 p(sl.v()[i]);
311 if (i < sl.v().size() - 1) os << ",";
312 }
313 os << "}";
314 }
315 } break;
316 case Expression::E_BOOLLIT:
317 os << (e->cast<BoolLit>()->v() ? "true" : "false");
318 break;
319 case Expression::E_STRINGLIT:
320 os << "\"" << Printer::escapeStringLit(e->cast<StringLit>()->v()) << "\"";
321 break;
322 case Expression::E_ID: {
323 if (e == constants().absent) {
324 os << "<>";
325 } else {
326 const Id* id = e->cast<Id>();
327 if (id->decl()) id = id->decl()->id();
328 if (id->idn() == -1) {
329 os << id->v();
330 } else {
331 os << "X_INTRODUCED_" << id->idn() << "_";
332 }
333 }
334 } break;
335 case Expression::E_TIID:
336 os << "$" << e->cast<TIId>()->v();
337 break;
338 case Expression::E_ANON:
339 os << "_";
340 break;
341 case Expression::E_ARRAYLIT: {
342 const ArrayLit& al = *e->cast<ArrayLit>();
343 int n = al.dims();
344 if (n == 1 && al.min(0) == 1) {
345 os << "[";
346 for (unsigned int i = 0; i < al.size(); i++) {
347 p(al[i]);
348 if (i < al.size() - 1) os << ",";
349 }
350 os << "]";
351 } else if (n == 2 && al.min(0) == 1 && al.min(1) == 1 && al.max(1) != 0) {
352 os << "[|";
353 for (int i = 0; i < al.max(0); i++) {
354 for (int j = 0; j < al.max(1); j++) {
355 p(al[i * al.max(1) + j]);
356 if (j < al.max(1) - 1) os << ",";
357 }
358 if (i < al.max(0) - 1) os << "|";
359 }
360 os << "|]";
361 } else {
362 os << "array" << n << "d(";
363 for (int i = 0; i < al.dims(); i++) {
364 os << al.min(i) << ".." << al.max(i);
365 os << ",";
366 }
367 os << "[";
368 for (unsigned int i = 0; i < al.size(); i++) {
369 p(al[i]);
370 if (i < al.size() - 1) os << ",";
371 }
372 os << "])";
373 }
374 } break;
375 case Expression::E_ARRAYACCESS: {
376 const ArrayAccess& aa = *e->cast<ArrayAccess>();
377 p(aa.v());
378 os << "[";
379 for (unsigned int i = 0; i < aa.idx().size(); i++) {
380 p(aa.idx()[i]);
381 if (i < aa.idx().size() - 1) os << ",";
382 }
383 os << "]";
384 } break;
385 case Expression::E_COMP: {
386 const Comprehension& c = *e->cast<Comprehension>();
387 os << (c.set() ? "{" : "[");
388 p(c.e());
389 os << " | ";
390 for (int i = 0; i < c.n_generators(); i++) {
391 for (int j = 0; j < c.n_decls(i); j++) {
392 os << c.decl(i, j)->id()->v();
393 if (j < c.n_decls(i) - 1) os << ",";
394 }
395 if (c.in(i) == NULL) {
396 os << " = ";
397 p(c.where(i));
398 } else {
399 os << " in ";
400 p(c.in(i));
401 if (c.where(i) != NULL) {
402 os << " where ";
403 p(c.where(i));
404 }
405 }
406 if (i < c.n_generators()) os << ", ";
407 }
408 os << (c.set() ? "}" : "]");
409 } break;
410 case Expression::E_ITE: {
411 const ITE& ite = *e->cast<ITE>();
412 for (int i = 0; i < ite.size(); i++) {
413 os << (i == 0 ? "if " : " elseif ");
414 p(ite.e_if(i));
415 os << " then ";
416 p(ite.e_then(i));
417 }
418 os << " else ";
419 p(ite.e_else());
420 os << " endif";
421 } break;
422 case Expression::E_BINOP: {
423 const BinOp& bo = *e->cast<BinOp>();
424 Parentheses ps = needParens(&bo, bo.lhs(), bo.rhs());
425 if (ps & PN_LEFT) os << "(";
426 p(bo.lhs());
427 if (ps & PN_LEFT) os << ")";
428 switch (bo.op()) {
429 case BOT_PLUS:
430 os << "+";
431 break;
432 case BOT_MINUS:
433 os << "-";
434 break;
435 case BOT_MULT:
436 os << "*";
437 break;
438 case BOT_POW:
439 os << "^";
440 break;
441 case BOT_DIV:
442 os << "/";
443 break;
444 case BOT_IDIV:
445 os << " div ";
446 break;
447 case BOT_MOD:
448 os << " mod ";
449 break;
450 case BOT_LE:
451 os << " < ";
452 break;
453 case BOT_LQ:
454 os << "<=";
455 break;
456 case BOT_GR:
457 os << " > ";
458 break;
459 case BOT_GQ:
460 os << ">=";
461 break;
462 case BOT_EQ:
463 os << "==";
464 break;
465 case BOT_NQ:
466 os << "!=";
467 break;
468 case BOT_IN:
469 os << " in ";
470 break;
471 case BOT_SUBSET:
472 os << " subset ";
473 break;
474 case BOT_SUPERSET:
475 os << " superset ";
476 break;
477 case BOT_UNION:
478 os << " union ";
479 break;
480 case BOT_DIFF:
481 os << " diff ";
482 break;
483 case BOT_SYMDIFF:
484 os << " symdiff ";
485 break;
486 case BOT_INTERSECT:
487 os << " intersect ";
488 break;
489 case BOT_PLUSPLUS:
490 os << "++";
491 break;
492 case BOT_EQUIV:
493 os << " <-> ";
494 break;
495 case BOT_IMPL:
496 os << " -> ";
497 break;
498 case BOT_RIMPL:
499 os << " <- ";
500 break;
501 case BOT_OR:
502 os << " \\/ ";
503 break;
504 case BOT_AND:
505 os << " /\\ ";
506 break;
507 case BOT_XOR:
508 os << " xor ";
509 break;
510 case BOT_DOTDOT:
511 os << "..";
512 break;
513 default:
514 assert(false);
515 break;
516 }
517
518 if (ps & PN_RIGHT) os << "(";
519 p(bo.rhs());
520 if (ps & PN_RIGHT) os << ")";
521 } break;
522 case Expression::E_UNOP: {
523 const UnOp& uo = *e->cast<UnOp>();
524 switch (uo.op()) {
525 case UOT_NOT:
526 os << "not ";
527 break;
528 case UOT_PLUS:
529 os << "+";
530 break;
531 case UOT_MINUS:
532 os << "-";
533 break;
534 default:
535 assert(false);
536 break;
537 }
538 bool needParen = (uo.e()->isa<BinOp>() || uo.e()->isa<UnOp>() || !uo.ann().isEmpty());
539 if (needParen) os << "(";
540 p(uo.e());
541 if (needParen) os << ")";
542 } break;
543 case Expression::E_CALL: {
544 const Call& c = *e->cast<Call>();
545 os << c.id() << "(";
546 for (unsigned int i = 0; i < c.n_args(); i++) {
547 p(c.arg(i));
548 if (i < c.n_args() - 1) os << ",";
549 }
550 os << ")";
551 } break;
552 case Expression::E_VARDECL: {
553 const VarDecl& vd = *e->cast<VarDecl>();
554 p(vd.ti());
555 if (!vd.ti()->isEnum()) {
556 os << ":";
557 }
558 if (vd.id()->idn() != -1) {
559 os << " X_INTRODUCED_" << vd.id()->idn() << "_";
560 } else if (vd.id()->v().size() != 0)
561 os << " " << vd.id()->v();
562 if (vd.introduced()) {
563 os << " ::var_is_introduced ";
564 }
565 p(vd.ann());
566 if (vd.e()) {
567 os << " = ";
568 p(vd.e());
569 }
570 } break;
571 case Expression::E_LET: {
572 const Let& l = *e->cast<Let>();
573 os << "let {";
574
575 for (unsigned int i = 0; i < l.let().size(); i++) {
576 const Expression* li = l.let()[i];
577 if (!li->isa<VarDecl>()) os << "constraint ";
578 p(li);
579 if (i < l.let().size() - 1) os << ", ";
580 }
581 os << "} in (";
582 p(l.in());
583 os << ")";
584 } break;
585 case Expression::E_TI: {
586 const TypeInst& ti = *e->cast<TypeInst>();
587 if (ti.isEnum()) {
588 os << "enum";
589 } else if (env) {
590 os << ti.type().toString(*env);
591 } else {
592 if (ti.isarray()) {
593 os << "array [";
594 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
595 p(Type::parint(), ti.ranges()[i]);
596 if (i < ti.ranges().size() - 1) os << ",";
597 }
598 os << "] of ";
599 }
600 p(ti.type(), ti.domain());
601 }
602 }
603 }
604 if (!e->isa<VarDecl>()) {
605 p(e->ann());
606 }
607 }
608
609 void p(const Item* i) {
610 if (i == NULL) return;
611 if (i->removed()) os << "% ";
612 switch (i->iid()) {
613 case Item::II_INC:
614 os << "include \"" << i->cast<IncludeI>()->f() << "\"";
615 break;
616 case Item::II_VD:
617 p(i->cast<VarDeclI>()->e());
618 break;
619 case Item::II_ASN:
620 os << i->cast<AssignI>()->id() << " = ";
621 p(i->cast<AssignI>()->e());
622 break;
623 case Item::II_CON:
624 os << "constraint ";
625 p(i->cast<ConstraintI>()->e());
626 break;
627 case Item::II_SOL: {
628 const SolveI* si = i->cast<SolveI>();
629 os << "solve ";
630 p(si->ann());
631 switch (si->st()) {
632 case SolveI::ST_SAT:
633 os << " satisfy";
634 break;
635 case SolveI::ST_MIN:
636 os << " minimize ";
637 p(si->e());
638 break;
639 case SolveI::ST_MAX:
640 os << " maximize ";
641 p(si->e());
642 break;
643 }
644 } break;
645 case Item::II_OUT:
646 os << "output ";
647 p(i->cast<OutputI>()->e());
648 break;
649 case Item::II_FUN: {
650 const FunctionI& fi = *i->cast<FunctionI>();
651 if (fi.ti()->type().isann() && fi.e() == NULL) {
652 os << "annotation ";
653 } else if (fi.ti()->type() == Type::parbool()) {
654 os << "test ";
655 } else if (fi.ti()->type() == Type::varbool()) {
656 os << "predicate ";
657 } else {
658 os << "function ";
659 p(fi.ti());
660 os << " : ";
661 }
662 os << fi.id();
663 if (fi.params().size() > 0) {
664 os << "(";
665 for (unsigned int i = 0; i < fi.params().size(); i++) {
666 p(fi.params()[i]);
667 if (i < fi.params().size() - 1) os << ",";
668 }
669 os << ")";
670 }
671 p(fi.ann());
672 if (fi.e()) {
673 os << " = ";
674 p(fi.e());
675 }
676 } break;
677 }
678 os << ";" << std::endl;
679 }
680};
681
682template <class T>
683class ExpressionMapper {
684protected:
685 T& _t;
686
687public:
688 ExpressionMapper(T& t) : _t(t) {}
689 typename T::ret map(const Expression* e) {
690 switch (e->eid()) {
691 case Expression::E_INTLIT:
692 return _t.mapIntLit(*e->cast<IntLit>());
693 case Expression::E_FLOATLIT:
694 return _t.mapFloatLit(*e->cast<FloatLit>());
695 case Expression::E_SETLIT:
696 return _t.mapSetLit(*e->cast<SetLit>());
697 case Expression::E_BOOLLIT:
698 return _t.mapBoolLit(*e->cast<BoolLit>());
699 case Expression::E_STRINGLIT:
700 return _t.mapStringLit(*e->cast<StringLit>());
701 case Expression::E_ID:
702 return _t.mapId(*e->cast<Id>());
703 case Expression::E_ANON:
704 return _t.mapAnonVar(*e->cast<AnonVar>());
705 case Expression::E_ARRAYLIT:
706 return _t.mapArrayLit(*e->cast<ArrayLit>());
707 case Expression::E_ARRAYACCESS:
708 return _t.mapArrayAccess(*e->cast<ArrayAccess>());
709 case Expression::E_COMP:
710 return _t.mapComprehension(*e->cast<Comprehension>());
711 case Expression::E_ITE:
712 return _t.mapITE(*e->cast<ITE>());
713 case Expression::E_BINOP:
714 return _t.mapBinOp(*e->cast<BinOp>());
715 case Expression::E_UNOP:
716 return _t.mapUnOp(*e->cast<UnOp>());
717 case Expression::E_CALL:
718 return _t.mapCall(*e->cast<Call>());
719 case Expression::E_VARDECL:
720 return _t.mapVarDecl(*e->cast<VarDecl>());
721 case Expression::E_LET:
722 return _t.mapLet(*e->cast<Let>());
723 case Expression::E_TI:
724 return _t.mapTypeInst(*e->cast<TypeInst>());
725 case Expression::E_TIID:
726 return _t.mapTIId(*e->cast<TIId>());
727 default:
728 assert(false);
729 return typename T::ret();
730 break;
731 }
732 }
733};
734
735class Document {
736private:
737 int level;
738
739public:
740 Document() : level(0) {}
741 virtual ~Document() {}
742 int getLevel() { return level; }
743 // Make this object a child of "d".
744 virtual void setParent(Document* d) { level = d->level + 1; }
745};
746
747class BreakPoint : public Document {
748private:
749 bool dontSimplify;
750
751public:
752 BreakPoint() { dontSimplify = false; }
753 BreakPoint(bool ds) { dontSimplify = ds; }
754 virtual ~BreakPoint() {}
755 void setDontSimplify(bool b) { dontSimplify = b; }
756 bool getDontSimplify() { return dontSimplify; }
757};
758
759class StringDocument : public Document {
760private:
761 std::string stringDocument;
762
763public:
764 StringDocument() {}
765 virtual ~StringDocument() {}
766
767 StringDocument(std::string s) : stringDocument(s) {}
768
769 std::string getString() { return stringDocument; }
770 void setString(std::string s) { stringDocument = s; }
771};
772
773class DocumentList : public Document {
774private:
775 std::vector<Document*> docs;
776 std::string beginToken;
777 std::string separator;
778 std::string endToken;
779 bool unbreakable;
780 bool alignment;
781
782public:
783 virtual ~DocumentList() {
784 std::vector<Document*>::iterator it;
785 for (it = docs.begin(); it != docs.end(); it++) {
786 delete *it;
787 }
788 }
789 DocumentList(std::string _beginToken = "", std::string _separator = "",
790 std::string _endToken = "", bool _alignment = true);
791
792 void addDocumentToList(Document* d) {
793 docs.push_back(d);
794 d->setParent(this);
795 }
796
797 void setParent(Document* d) {
798 Document::setParent(d);
799 std::vector<Document*>::iterator it;
800 for (it = docs.begin(); it != docs.end(); it++) {
801 (*it)->setParent(this);
802 }
803 }
804
805 void addStringToList(std::string s) { addDocumentToList(new StringDocument(s)); }
806
807 void addBreakPoint(bool b = false) { addDocumentToList(new BreakPoint(b)); }
808
809 std::vector<Document*> getDocs() { return docs; }
810
811 void setList(std::vector<Document*> ld) { docs = ld; }
812
813 std::string getBeginToken() { return beginToken; }
814
815 std::string getEndToken() { return endToken; }
816
817 std::string getSeparator() { return separator; }
818
819 bool getUnbreakable() { return unbreakable; }
820
821 void setUnbreakable(bool b) { unbreakable = b; }
822
823 bool getAlignment() { return alignment; }
824};
825
826DocumentList::DocumentList(std::string _beginToken, std::string _separator, std::string _endToken,
827 bool _alignment) {
828 beginToken = _beginToken;
829 separator = _separator;
830 endToken = _endToken;
831 alignment = _alignment;
832 unbreakable = false;
833}
834
835class Line {
836private:
837 int indentation;
838 int lineLength;
839 std::vector<std::string> text;
840
841public:
842 Line() : indentation(0), lineLength(0), text(0) {}
843 Line(const Line& l) : indentation(l.indentation), lineLength(l.lineLength), text(l.text) {}
844 Line(const int indent) : indentation(indent), lineLength(0), text(0) {}
845 bool operator==(const Line& l) { return &l == this; }
846
847 void setIndentation(int i) { indentation = i; }
848
849 int getLength() const { return lineLength; }
850 int getIndentation() const { return indentation; }
851 int getSpaceLeft(int maxwidth);
852 void addString(const std::string& s);
853 void concatenateLines(Line& l);
854
855 void print(std::ostream& os) const {
856 for (int i = 0; i < getIndentation(); i++) {
857 os << " ";
858 }
859 std::vector<std::string>::const_iterator it;
860 for (it = text.begin(); it != text.end(); it++) {
861 os << (*it);
862 }
863 os << "\n";
864 }
865};
866
867int Line::getSpaceLeft(int maxwidth) { return maxwidth - lineLength - indentation; }
868void Line::addString(const std::string& s) {
869 lineLength += static_cast<int>(s.size());
870 text.push_back(s);
871}
872void Line::concatenateLines(Line& l) {
873 text.insert(text.end(), l.text.begin(), l.text.end());
874 lineLength += l.lineLength;
875}
876
877class LinesToSimplify {
878private:
879 std::map<int, std::vector<int> > lines;
880
881 // (i,j) in parent <=> j can only be simplified if i is simplified
882 std::vector<std::pair<int, int> > parent;
883 /*
884 * if i can't simplify, remove j and his parents
885 */
886 // mostRecentlyAdded[level] = line of the most recently added
887 std::map<int, int> mostRecentlyAdded;
888
889public:
890 std::vector<int>* getLinesForPriority(int p) {
891 std::map<int, std::vector<int> >::iterator it;
892 for (it = lines.begin(); it != lines.end(); it++) {
893 if (it->first == p) return &(it->second);
894 }
895 return NULL;
896 }
897 void addLine(int p, int l, int par = -1) {
898 if (par == -1) {
899 for (int i = p - 1; i >= 0; i--) {
900 std::map<int, int>::iterator it = mostRecentlyAdded.find(i);
901 if (it != mostRecentlyAdded.end()) {
902 par = it->second;
903 break;
904 }
905 }
906 }
907 if (par != -1) parent.push_back(std::pair<int, int>(l, par));
908 mostRecentlyAdded.insert(std::pair<int, int>(p, l));
909 std::map<int, std::vector<int> >::iterator it;
910 for (it = lines.begin(); it != lines.end(); it++) {
911 if (it->first == p) {
912 it->second.push_back(l);
913 return;
914 }
915 }
916 std::vector<int> v;
917 v.push_back(l);
918 lines.insert(std::pair<int, std::vector<int> >(p, v));
919 }
920 void decrementLine(std::vector<int>* vec, int l) {
921 std::vector<int>::iterator vit;
922 if (vec != NULL) {
923 for (vit = vec->begin(); vit != vec->end(); vit++) {
924 if (*vit >= l) *vit = *vit - 1;
925 }
926 }
927 // Now the map
928 std::map<int, std::vector<int> >::iterator it;
929 for (it = lines.begin(); it != lines.end(); it++) {
930 for (vit = it->second.begin(); vit != it->second.end(); vit++) {
931 if (*vit >= l) *vit = *vit - 1;
932 }
933 }
934 // And the parent table
935 std::vector<std::pair<int, int> >::iterator vpit;
936 for (vpit = parent.begin(); vpit != parent.end(); vpit++) {
937 if (vpit->first >= l) vpit->first--;
938 if (vpit->second >= l) vpit->second--;
939 }
940 }
941 void remove(LinesToSimplify& lts) {
942 std::map<int, std::vector<int> >::iterator it;
943 for (it = lts.lines.begin(); it != lts.lines.end(); it++) {
944 std::vector<int>::iterator vit;
945 for (vit = it->second.begin(); vit != it->second.end(); vit++) {
946 remove(NULL, *vit, false);
947 }
948 }
949 }
950 void remove(std::vector<int>* v, int i, bool success = true) {
951 if (v != NULL) {
952 v->erase(std::remove(v->begin(), v->end(), i), v->end());
953 }
954 std::map<int, std::vector<int> >::iterator it;
955 for (it = lines.begin(); it != lines.end(); it++) {
956 std::vector<int>* v = &(it->second);
957 v->erase(std::remove(v->begin(), v->end(), i), v->end());
958 }
959 // Call on its parent
960 if (!success) {
961 std::vector<std::pair<int, int> >::iterator vpit;
962 for (vpit = parent.begin(); vpit != parent.end(); vpit++) {
963 if (vpit->first == i && vpit->second != i && vpit->second != -1) {
964 remove(v, vpit->second, false);
965 }
966 }
967 }
968 }
969 std::vector<int>* getLinesToSimplify() {
970 std::vector<int>* vec = new std::vector<int>();
971 std::map<int, std::vector<int> >::iterator it;
972 for (it = lines.begin(); it != lines.end(); it++) {
973 std::vector<int>& svec = it->second;
974 vec->insert(vec->begin(), svec.begin(), svec.end());
975 }
976 return vec;
977 }
978};
979
980Document* expressionToDocument(const Expression* e);
981Document* annotationToDocument(const Annotation& ann);
982Document* tiexpressionToDocument(const Type& type, const Expression* e) {
983 DocumentList* dl = new DocumentList("", "", "", false);
984 switch (type.ti()) {
985 case Type::TI_PAR:
986 break;
987 case Type::TI_VAR:
988 dl->addStringToList("var ");
989 break;
990 }
991 if (type.ot() == Type::OT_OPTIONAL) dl->addStringToList("opt ");
992 if (type.st() == Type::ST_SET) dl->addStringToList("set of ");
993 if (e == NULL) {
994 switch (type.bt()) {
995 case Type::BT_INT:
996 dl->addStringToList("int");
997 break;
998 case Type::BT_BOOL:
999 dl->addStringToList("bool");
1000 break;
1001 case Type::BT_FLOAT:
1002 dl->addStringToList("float");
1003 break;
1004 case Type::BT_STRING:
1005 dl->addStringToList("string");
1006 break;
1007 case Type::BT_ANN:
1008 dl->addStringToList("ann");
1009 break;
1010 case Type::BT_BOT:
1011 dl->addStringToList("bot");
1012 break;
1013 case Type::BT_TOP:
1014 dl->addStringToList("top");
1015 break;
1016 case Type::BT_UNKNOWN:
1017 dl->addStringToList("???");
1018 break;
1019 }
1020 } else {
1021 dl->addDocumentToList(expressionToDocument(e));
1022 }
1023 return dl;
1024}
1025
1026class ExpressionDocumentMapper {
1027public:
1028 typedef Document* ret;
1029 ret mapIntLit(const IntLit& il) {
1030 std::ostringstream oss;
1031 oss << il.v();
1032 return new StringDocument(oss.str());
1033 }
1034 ret mapFloatLit(const FloatLit& fl) {
1035 std::ostringstream oss;
1036 ppFloatVal(oss, fl.v());
1037 return new StringDocument(oss.str());
1038 }
1039 ret mapSetLit(const SetLit& sl) {
1040 DocumentList* dl;
1041 if (sl.isv()) {
1042 if (sl.isv()->size() == 0) {
1043 dl = new DocumentList("1..0", "", "");
1044 } else if (sl.isv()->size() == 1) {
1045 dl = new DocumentList("", "..", "");
1046 {
1047 std::ostringstream oss;
1048 oss << sl.isv()->min(0);
1049 dl->addDocumentToList(new StringDocument(oss.str()));
1050 }
1051 {
1052 std::ostringstream oss;
1053 oss << sl.isv()->max(0);
1054 dl->addDocumentToList(new StringDocument(oss.str()));
1055 }
1056 } else {
1057 dl = new DocumentList("{", ", ", "}", true);
1058 IntSetRanges isr(sl.isv());
1059 for (Ranges::ToValues<IntSetRanges> isv(isr); isv(); ++isv) {
1060 std::ostringstream oss;
1061 oss << isv.val();
1062 dl->addDocumentToList(new StringDocument(oss.str()));
1063 }
1064 }
1065 } else if (sl.fsv()) {
1066 if (sl.fsv()->size() == 0) {
1067 dl = new DocumentList("1.0..0.0", "", "");
1068 } else if (sl.fsv()->size() == 1) {
1069 dl = new DocumentList("", "..", "");
1070 {
1071 std::ostringstream oss;
1072 ppFloatVal(oss, sl.fsv()->min(0));
1073 dl->addDocumentToList(new StringDocument(oss.str()));
1074 }
1075 {
1076 std::ostringstream oss;
1077 ppFloatVal(oss, sl.fsv()->max(0));
1078 dl->addDocumentToList(new StringDocument(oss.str()));
1079 }
1080 } else {
1081 dl = new DocumentList("", "++", "", true);
1082 FloatSetRanges fsr(sl.fsv());
1083 for (; fsr(); ++fsr) {
1084 std::ostringstream oss;
1085 ppFloatVal(oss, fsr.min());
1086 oss << "..";
1087 ppFloatVal(oss, fsr.max());
1088 dl->addDocumentToList(new StringDocument(oss.str()));
1089 }
1090 }
1091
1092 } else {
1093 dl = new DocumentList("{", ", ", "}", true);
1094 for (unsigned int i = 0; i < sl.v().size(); i++) {
1095 dl->addDocumentToList(expressionToDocument((sl.v()[i])));
1096 }
1097 }
1098 return dl;
1099 }
1100 ret mapBoolLit(const BoolLit& bl) {
1101 return new StringDocument(std::string(bl.v() ? "true" : "false"));
1102 }
1103 ret mapStringLit(const StringLit& sl) {
1104 std::ostringstream oss;
1105 oss << "\"" << Printer::escapeStringLit(sl.v()) << "\"";
1106 return new StringDocument(oss.str());
1107 }
1108 ret mapId(const Id& id) {
1109 if (&id == constants().absent) return new StringDocument("<>");
1110 if (id.idn() == -1)
1111 return new StringDocument(id.v().str());
1112 else {
1113 std::ostringstream oss;
1114 oss << "X_INTRODUCED_" << id.idn() << "_";
1115 return new StringDocument(oss.str());
1116 }
1117 }
1118 ret mapTIId(const TIId& id) { return new StringDocument("$" + id.v().str()); }
1119 ret mapAnonVar(const AnonVar&) { return new StringDocument("_"); }
1120 ret mapArrayLit(const ArrayLit& al) {
1121 /// TODO: test multi-dimensional arrays handling
1122 DocumentList* dl;
1123 int n = al.dims();
1124 if (n == 1 && al.min(0) == 1) {
1125 dl = new DocumentList("[", ", ", "]");
1126 for (unsigned int i = 0; i < al.size(); i++)
1127 dl->addDocumentToList(expressionToDocument(al[i]));
1128 } else if (n == 2 && al.min(0) == 1 && al.min(1) == 1) {
1129 dl = new DocumentList("[| ", " | ", " |]");
1130 for (int i = 0; i < al.max(0); i++) {
1131 DocumentList* row = new DocumentList("", ", ", "");
1132 for (int j = 0; j < al.max(1); j++) {
1133 row->addDocumentToList(expressionToDocument(al[i * al.max(1) + j]));
1134 }
1135 dl->addDocumentToList(row);
1136 if (i != al.max(0) - 1) dl->addBreakPoint(true); // dont simplify
1137 }
1138 } else {
1139 dl = new DocumentList("", "", "");
1140 std::stringstream oss;
1141 oss << "array" << n << "d";
1142 dl->addStringToList(oss.str());
1143 DocumentList* args = new DocumentList("(", ", ", ")");
1144
1145 for (int i = 0; i < al.dims(); i++) {
1146 oss.str("");
1147 oss << al.min(i) << ".." << al.max(i);
1148 args->addStringToList(oss.str());
1149 }
1150 DocumentList* array = new DocumentList("[", ", ", "]");
1151 for (unsigned int i = 0; i < al.size(); i++)
1152 array->addDocumentToList(expressionToDocument(al[i]));
1153 args->addDocumentToList(array);
1154 dl->addDocumentToList(args);
1155 }
1156 return dl;
1157 }
1158 ret mapArrayAccess(const ArrayAccess& aa) {
1159 DocumentList* dl = new DocumentList("", "", "");
1160
1161 dl->addDocumentToList(expressionToDocument(aa.v()));
1162 DocumentList* args = new DocumentList("[", ", ", "]");
1163 for (unsigned int i = 0; i < aa.idx().size(); i++) {
1164 args->addDocumentToList(expressionToDocument(aa.idx()[i]));
1165 }
1166 dl->addDocumentToList(args);
1167 return dl;
1168 }
1169 ret mapComprehension(const Comprehension& c) {
1170 std::ostringstream oss;
1171 DocumentList* dl;
1172 if (c.set())
1173 dl = new DocumentList("{ ", " | ", " }");
1174 else
1175 dl = new DocumentList("[ ", " | ", " ]");
1176 dl->addDocumentToList(expressionToDocument(c.e()));
1177 DocumentList* head = new DocumentList("", " ", "");
1178 DocumentList* generators = new DocumentList("", ", ", "");
1179 for (int i = 0; i < c.n_generators(); i++) {
1180 DocumentList* gen = new DocumentList("", "", "");
1181 DocumentList* idents = new DocumentList("", ", ", "");
1182 for (int j = 0; j < c.n_decls(i); j++) {
1183 idents->addStringToList(c.decl(i, j)->id()->v().str());
1184 }
1185 gen->addDocumentToList(idents);
1186 if (c.in(i) == NULL) {
1187 gen->addStringToList(" = ");
1188 gen->addDocumentToList(expressionToDocument(c.where(i)));
1189 } else {
1190 gen->addStringToList(" in ");
1191 gen->addDocumentToList(expressionToDocument(c.in(i)));
1192 if (c.where(i) != NULL) {
1193 gen->addStringToList(" where ");
1194 gen->addDocumentToList(expressionToDocument(c.where(i)));
1195 }
1196 }
1197 generators->addDocumentToList(gen);
1198 }
1199 head->addDocumentToList(generators);
1200 dl->addDocumentToList(head);
1201
1202 return dl;
1203 }
1204 ret mapITE(const ITE& ite) {
1205 DocumentList* dl = new DocumentList("", "", "");
1206 for (int i = 0; i < ite.size(); i++) {
1207 std::string beg = (i == 0 ? "if " : " elseif ");
1208 dl->addStringToList(beg);
1209 dl->addDocumentToList(expressionToDocument(ite.e_if(i)));
1210 dl->addStringToList(" then ");
1211
1212 DocumentList* ifdoc = new DocumentList("", "", "", false);
1213 ifdoc->addBreakPoint();
1214 ifdoc->addDocumentToList(expressionToDocument(ite.e_then(i)));
1215 dl->addDocumentToList(ifdoc);
1216 dl->addStringToList(" ");
1217 }
1218 dl->addBreakPoint();
1219 dl->addStringToList("else ");
1220
1221 DocumentList* elsedoc = new DocumentList("", "", "", false);
1222 elsedoc->addBreakPoint();
1223 elsedoc->addDocumentToList(expressionToDocument(ite.e_else()));
1224 dl->addDocumentToList(elsedoc);
1225 dl->addStringToList(" ");
1226 dl->addBreakPoint();
1227 dl->addStringToList("endif");
1228
1229 return dl;
1230 }
1231 ret mapBinOp(const BinOp& bo) {
1232 Parentheses ps = needParens(&bo, bo.lhs(), bo.rhs());
1233 DocumentList* opLeft;
1234 DocumentList* dl;
1235 DocumentList* opRight;
1236 bool linebreak = false;
1237 if (ps & PN_LEFT)
1238 opLeft = new DocumentList("(", " ", ")");
1239 else
1240 opLeft = new DocumentList("", " ", "");
1241 opLeft->addDocumentToList(expressionToDocument(bo.lhs()));
1242 std::string op;
1243 switch (bo.op()) {
1244 case BOT_PLUS:
1245 op = "+";
1246 break;
1247 case BOT_MINUS:
1248 op = "-";
1249 break;
1250 case BOT_MULT:
1251 op = "*";
1252 break;
1253 case BOT_POW:
1254 op = "^";
1255 break;
1256 case BOT_DIV:
1257 op = "/";
1258 break;
1259 case BOT_IDIV:
1260 op = " div ";
1261 break;
1262 case BOT_MOD:
1263 op = " mod ";
1264 break;
1265 case BOT_LE:
1266 op = " < ";
1267 break;
1268 case BOT_LQ:
1269 op = "<=";
1270 break;
1271 case BOT_GR:
1272 op = " > ";
1273 break;
1274 case BOT_GQ:
1275 op = ">=";
1276 break;
1277 case BOT_EQ:
1278 op = "==";
1279 break;
1280 case BOT_NQ:
1281 op = "!=";
1282 break;
1283 case BOT_IN:
1284 op = " in ";
1285 break;
1286 case BOT_SUBSET:
1287 op = " subset ";
1288 break;
1289 case BOT_SUPERSET:
1290 op = " superset ";
1291 break;
1292 case BOT_UNION:
1293 op = " union ";
1294 break;
1295 case BOT_DIFF:
1296 op = " diff ";
1297 break;
1298 case BOT_SYMDIFF:
1299 op = " symdiff ";
1300 break;
1301 case BOT_INTERSECT:
1302 op = " intersect ";
1303 break;
1304 case BOT_PLUSPLUS:
1305 op = "++";
1306 linebreak = true;
1307 break;
1308 case BOT_EQUIV:
1309 op = " <-> ";
1310 break;
1311 case BOT_IMPL:
1312 op = " -> ";
1313 break;
1314 case BOT_RIMPL:
1315 op = " <- ";
1316 break;
1317 case BOT_OR:
1318 op = " \\/ ";
1319 linebreak = true;
1320 break;
1321 case BOT_AND:
1322 op = " /\\ ";
1323 linebreak = true;
1324 break;
1325 case BOT_XOR:
1326 op = " xor ";
1327 break;
1328 case BOT_DOTDOT:
1329 op = "..";
1330 break;
1331 default:
1332 assert(false);
1333 break;
1334 }
1335 dl = new DocumentList("", op, "");
1336
1337 if (ps & PN_RIGHT)
1338 opRight = new DocumentList("(", " ", ")");
1339 else
1340 opRight = new DocumentList("", "", "");
1341 opRight->addDocumentToList(expressionToDocument(bo.rhs()));
1342 dl->addDocumentToList(opLeft);
1343 if (linebreak) dl->addBreakPoint();
1344 dl->addDocumentToList(opRight);
1345
1346 return dl;
1347 }
1348 ret mapUnOp(const UnOp& uo) {
1349 DocumentList* dl = new DocumentList("", "", "");
1350 std::string op;
1351 switch (uo.op()) {
1352 case UOT_NOT:
1353 op = "not ";
1354 break;
1355 case UOT_PLUS:
1356 op = "+";
1357 break;
1358 case UOT_MINUS:
1359 op = "-";
1360 break;
1361 default:
1362 assert(false);
1363 break;
1364 }
1365 dl->addStringToList(op);
1366 DocumentList* unop;
1367 bool needParen = (uo.e()->isa<BinOp>() || uo.e()->isa<UnOp>());
1368 if (needParen)
1369 unop = new DocumentList("(", " ", ")");
1370 else
1371 unop = new DocumentList("", " ", "");
1372
1373 unop->addDocumentToList(expressionToDocument(uo.e()));
1374 dl->addDocumentToList(unop);
1375 return dl;
1376 }
1377 ret mapCall(const Call& c) {
1378 if (c.n_args() == 1) {
1379 /*
1380 * if we have only one argument, and this is an array comprehension,
1381 * we convert it into the following syntax
1382 * forall (f(i,j) | i in 1..10)
1383 * -->
1384 * forall (i in 1..10) (f(i,j))
1385 */
1386
1387 const Expression* e = c.arg(0);
1388 if (e->isa<Comprehension>()) {
1389 const Comprehension* com = e->cast<Comprehension>();
1390 if (!com->set()) {
1391 DocumentList* dl = new DocumentList("", " ", "");
1392 dl->addStringToList(c.id().str());
1393 DocumentList* args = new DocumentList("", " ", "", false);
1394 DocumentList* generators = new DocumentList("", ", ", "");
1395
1396 for (int i = 0; i < com->n_generators(); i++) {
1397 DocumentList* gen = new DocumentList("", "", "");
1398 DocumentList* idents = new DocumentList("", ", ", "");
1399 for (int j = 0; j < com->n_decls(i); j++) {
1400 idents->addStringToList(com->decl(i, j)->id()->v().str());
1401 }
1402 gen->addDocumentToList(idents);
1403 if (com->in(i) == NULL) {
1404 gen->addStringToList(" = ");
1405 gen->addDocumentToList(expressionToDocument(com->where(i)));
1406 } else {
1407 gen->addStringToList(" in ");
1408 gen->addDocumentToList(expressionToDocument(com->in(i)));
1409 if (com->where(i) != NULL) {
1410 gen->addStringToList(" where ");
1411 gen->addDocumentToList(expressionToDocument(com->where(i)));
1412 }
1413 }
1414 generators->addDocumentToList(gen);
1415 }
1416
1417 args->addStringToList("(");
1418 args->addDocumentToList(generators);
1419 args->addStringToList(")");
1420
1421 args->addStringToList("(");
1422 args->addBreakPoint();
1423 args->addDocumentToList(expressionToDocument(com->e()));
1424
1425 dl->addDocumentToList(args);
1426 dl->addBreakPoint();
1427 dl->addStringToList(")");
1428
1429 return dl;
1430 }
1431 }
1432 }
1433 std::string beg = c.id().str() + "(";
1434 DocumentList* dl = new DocumentList(beg, ", ", ")");
1435 for (unsigned int i = 0; i < c.n_args(); i++) {
1436 dl->addDocumentToList(expressionToDocument(c.arg(i)));
1437 }
1438 return dl;
1439 }
1440 ret mapVarDecl(const VarDecl& vd) {
1441 std::ostringstream oss;
1442 DocumentList* dl = new DocumentList("", "", "");
1443 dl->addDocumentToList(expressionToDocument(vd.ti()));
1444 dl->addStringToList(": ");
1445 if (vd.id()->idn() == -1) {
1446 dl->addStringToList(vd.id()->v().str());
1447 } else {
1448 std::ostringstream oss;
1449 oss << "X_INTRODUCED_" << vd.id()->idn() << "_";
1450 dl->addStringToList(oss.str());
1451 }
1452
1453 if (vd.introduced()) {
1454 dl->addStringToList(" ::var_is_introduced ");
1455 }
1456 if (!vd.ann().isEmpty()) {
1457 dl->addDocumentToList(annotationToDocument(vd.ann()));
1458 }
1459 if (vd.e()) {
1460 dl->addStringToList(" = ");
1461 dl->addDocumentToList(expressionToDocument(vd.e()));
1462 }
1463 return dl;
1464 }
1465 ret mapLet(const Let& l) {
1466 DocumentList* letin = new DocumentList("", "", "", false);
1467 DocumentList* lets = new DocumentList("", " ", "", true);
1468 DocumentList* inexpr = new DocumentList("", "", "");
1469 bool ds = l.let().size() > 1;
1470
1471 for (unsigned int i = 0; i < l.let().size(); i++) {
1472 if (i != 0) lets->addBreakPoint(ds);
1473 DocumentList* exp = new DocumentList("", " ", ",");
1474 const Expression* li = l.let()[i];
1475 if (!li->isa<VarDecl>()) exp->addStringToList("constraint");
1476 exp->addDocumentToList(expressionToDocument(li));
1477 lets->addDocumentToList(exp);
1478 }
1479
1480 inexpr->addDocumentToList(expressionToDocument(l.in()));
1481 letin->addBreakPoint(ds);
1482 letin->addDocumentToList(lets);
1483
1484 DocumentList* letin2 = new DocumentList("", "", "", false);
1485
1486 letin2->addBreakPoint();
1487 letin2->addDocumentToList(inexpr);
1488
1489 DocumentList* dl = new DocumentList("", "", "");
1490 dl->addStringToList("let {");
1491 dl->addDocumentToList(letin);
1492 dl->addBreakPoint(ds);
1493 dl->addStringToList("} in (");
1494 dl->addDocumentToList(letin2);
1495 // dl->addBreakPoint();
1496 dl->addStringToList(")");
1497 return dl;
1498 }
1499 ret mapTypeInst(const TypeInst& ti) {
1500 DocumentList* dl = new DocumentList("", "", "");
1501 if (ti.isarray()) {
1502 dl->addStringToList("array [");
1503 DocumentList* ran = new DocumentList("", ", ", "");
1504 for (unsigned int i = 0; i < ti.ranges().size(); i++) {
1505 ran->addDocumentToList(tiexpressionToDocument(Type::parint(), ti.ranges()[i]));
1506 }
1507 dl->addDocumentToList(ran);
1508 dl->addStringToList("] of ");
1509 }
1510 dl->addDocumentToList(tiexpressionToDocument(ti.type(), ti.domain()));
1511 return dl;
1512 }
1513};
1514
1515Document* annotationToDocument(const Annotation& ann) {
1516 DocumentList* dl = new DocumentList(" :: ", " :: ", "");
1517 for (ExpressionSetIter it = ann.begin(); it != ann.end(); ++it) {
1518 dl->addDocumentToList(expressionToDocument(*it));
1519 }
1520 return dl;
1521}
1522
1523Document* expressionToDocument(const Expression* e) {
1524 if (e == NULL) return new StringDocument("NULL");
1525 ExpressionDocumentMapper esm;
1526 ExpressionMapper<ExpressionDocumentMapper> em(esm);
1527 DocumentList* dl = new DocumentList("", "", "");
1528 Document* s = em.map(e);
1529 dl->addDocumentToList(s);
1530 if (!e->isa<VarDecl>() && !e->ann().isEmpty()) {
1531 dl->addDocumentToList(annotationToDocument(e->ann()));
1532 }
1533 return dl;
1534}
1535
1536class ItemDocumentMapper {
1537public:
1538 typedef Document* ret;
1539 ret mapIncludeI(const IncludeI& ii) {
1540 std::ostringstream oss;
1541 oss << "include \"" << ii.f() << "\";";
1542 return new StringDocument(oss.str());
1543 }
1544 ret mapVarDeclI(const VarDeclI& vi) {
1545 DocumentList* dl = new DocumentList("", " ", ";");
1546 dl->addDocumentToList(expressionToDocument(vi.e()));
1547 return dl;
1548 }
1549 ret mapAssignI(const AssignI& ai) {
1550 DocumentList* dl = new DocumentList("", " = ", ";");
1551 dl->addStringToList(ai.id().str());
1552 dl->addDocumentToList(expressionToDocument(ai.e()));
1553 return dl;
1554 }
1555 ret mapConstraintI(const ConstraintI& ci) {
1556 DocumentList* dl = new DocumentList("constraint ", " ", ";");
1557 dl->addDocumentToList(expressionToDocument(ci.e()));
1558 return dl;
1559 }
1560 ret mapSolveI(const SolveI& si) {
1561 DocumentList* dl = new DocumentList("", "", ";");
1562 dl->addStringToList("solve");
1563 if (!si.ann().isEmpty()) dl->addDocumentToList(annotationToDocument(si.ann()));
1564 switch (si.st()) {
1565 case SolveI::ST_SAT:
1566 dl->addStringToList(" satisfy");
1567 break;
1568 case SolveI::ST_MIN:
1569 dl->addStringToList(" minimize ");
1570 dl->addDocumentToList(expressionToDocument(si.e()));
1571 break;
1572 case SolveI::ST_MAX:
1573 dl->addStringToList(" maximize ");
1574 dl->addDocumentToList(expressionToDocument(si.e()));
1575 break;
1576 }
1577 return dl;
1578 }
1579 ret mapOutputI(const OutputI& oi) {
1580 DocumentList* dl = new DocumentList("output ", " ", ";");
1581 dl->addDocumentToList(expressionToDocument(oi.e()));
1582 return dl;
1583 }
1584 ret mapFunctionI(const FunctionI& fi) {
1585 DocumentList* dl;
1586 if (fi.ti()->type().isann() && fi.e() == NULL) {
1587 dl = new DocumentList("annotation ", " ", ";", false);
1588 } else if (fi.ti()->type() == Type::parbool()) {
1589 dl = new DocumentList("test ", "", ";", false);
1590 } else if (fi.ti()->type() == Type::varbool()) {
1591 dl = new DocumentList("predicate ", "", ";", false);
1592 } else {
1593 dl = new DocumentList("function ", "", ";", false);
1594 dl->addDocumentToList(expressionToDocument(fi.ti()));
1595 dl->addStringToList(": ");
1596 }
1597 dl->addStringToList(fi.id().str());
1598 if (fi.params().size() > 0) {
1599 DocumentList* params = new DocumentList("(", ", ", ")");
1600 for (unsigned int i = 0; i < fi.params().size(); i++) {
1601 DocumentList* par = new DocumentList("", "", "");
1602 par->setUnbreakable(true);
1603 par->addDocumentToList(expressionToDocument(fi.params()[i]));
1604 params->addDocumentToList(par);
1605 }
1606 dl->addDocumentToList(params);
1607 }
1608 if (!fi.ann().isEmpty()) {
1609 dl->addDocumentToList(annotationToDocument(fi.ann()));
1610 }
1611 if (fi.e()) {
1612 dl->addStringToList(" = ");
1613 dl->addBreakPoint();
1614 dl->addDocumentToList(expressionToDocument(fi.e()));
1615 }
1616
1617 return dl;
1618 }
1619};
1620
1621class PrettyPrinter {
1622public:
1623 /*
1624 * \brief Constructor for class Pretty Printer
1625 * \param maxwidth (default 80) : number of rows
1626 * \param indentationBase : spaces that represent the atomic number of spaces
1627 * \param sim : whether we want to simplify the result
1628 * \param deepSimp : whether we want to simplify at each breakpoint or not
1629 */
1630 PrettyPrinter(int _maxwidth = 80, int _indentationBase = 4, bool sim = false,
1631 bool deepSimp = false);
1632
1633 void print(Document* d);
1634 void print(std::ostream& os) const;
1635
1636private:
1637 int maxwidth;
1638 int indentationBase;
1639 int currentLine;
1640 int currentItem;
1641 std::vector<std::vector<Line> > items;
1642 std::vector<LinesToSimplify> linesToSimplify;
1643 std::vector<LinesToSimplify> linesNotToSimplify;
1644 bool simp;
1645 bool deeplySimp;
1646
1647 void addItem();
1648
1649 void addLine(int indentation, bool bp = false, bool ds = false, int level = 0);
1650 static std::string printSpaces(int n);
1651 const std::vector<Line>& getCurrentItemLines() const;
1652
1653 void printDocument(Document* d, bool alignment, int startColAlignment,
1654 const std::string& before = "", const std::string& after = "");
1655 void printDocList(DocumentList* d, int startColAlignment, const std::string& before = "",
1656 const std::string& after = "");
1657 void printStringDoc(StringDocument* d, bool alignment, int startColAlignment,
1658 const std::string& before = "", const std::string& after = "");
1659 void printString(const std::string& s, bool alignment, int startColAlignment);
1660 bool simplify(int item, int line, std::vector<int>* vec);
1661 void simplifyItem(int item);
1662};
1663
1664void PrettyPrinter::print(Document* d) {
1665 addItem();
1666 addLine(0);
1667 printDocument(d, true, 0);
1668 if (simp) simplifyItem(currentItem);
1669}
1670
1671PrettyPrinter::PrettyPrinter(int _maxwidth, int _indentationBase, bool sim, bool deepsim) {
1672 maxwidth = _maxwidth;
1673 indentationBase = _indentationBase;
1674 currentLine = -1;
1675 currentItem = -1;
1676
1677 simp = sim;
1678 deeplySimp = deepsim;
1679}
1680const std::vector<Line>& PrettyPrinter::getCurrentItemLines() const { return items[currentItem]; }
1681
1682void PrettyPrinter::addLine(int indentation, bool bp, bool simpl, int level) {
1683 items[currentItem].push_back(Line(indentation));
1684 currentLine++;
1685 if (bp && deeplySimp) {
1686 linesToSimplify[currentItem].addLine(level, currentLine);
1687 if (!simpl) linesNotToSimplify[currentItem].addLine(0, currentLine);
1688 }
1689}
1690void PrettyPrinter::addItem() {
1691 items.push_back(std::vector<Line>());
1692 linesToSimplify.push_back(LinesToSimplify());
1693 linesNotToSimplify.push_back(LinesToSimplify());
1694 currentItem++;
1695 currentLine = -1;
1696}
1697
1698void PrettyPrinter::print(std::ostream& os) const {
1699 std::vector<Line>::const_iterator it;
1700 int nItems = static_cast<int>(items.size());
1701 for (int item = 0; item < nItems; item++) {
1702 for (it = items[item].begin(); it != items[item].end(); it++) {
1703 it->print(os);
1704 }
1705 // os << std::endl;
1706 }
1707}
1708std::string PrettyPrinter::printSpaces(int n) {
1709 std::string result;
1710 for (int i = 0; i < n; i++) {
1711 result += " ";
1712 }
1713 return result;
1714}
1715
1716void PrettyPrinter::printDocument(Document* d, bool alignment, int alignmentCol,
1717 const std::string& before, const std::string& after) {
1718 if (DocumentList* dl = dynamic_cast<DocumentList*>(d)) {
1719 printDocList(dl, alignmentCol, before, after);
1720 } else if (StringDocument* sd = dynamic_cast<StringDocument*>(d)) {
1721 printStringDoc(sd, alignment, alignmentCol, before, after);
1722 } else if (BreakPoint* bp = dynamic_cast<BreakPoint*>(d)) {
1723 printString(before, alignment, alignmentCol);
1724 addLine(alignmentCol, deeplySimp, !bp->getDontSimplify(), d->getLevel());
1725 printString(after, alignment, alignmentCol);
1726 } else {
1727 throw InternalError("PrettyPrinter::print : Wrong type of document");
1728 }
1729}
1730
1731void PrettyPrinter::printStringDoc(StringDocument* d, bool alignment, int alignmentCol,
1732 const std::string& before, const std::string& after) {
1733 std::string s;
1734 if (d != NULL) s = d->getString();
1735 s = before + s + after;
1736 printString(s, alignment, alignmentCol);
1737}
1738
1739void PrettyPrinter::printString(const std::string& s, bool alignment, int alignmentCol) {
1740 Line& l = items[currentItem][currentLine];
1741 int size = static_cast<int>(s.size());
1742 if (size <= l.getSpaceLeft(maxwidth)) {
1743 l.addString(s);
1744 } else {
1745 int col = alignment && maxwidth - alignmentCol >= size ? alignmentCol : indentationBase;
1746 addLine(col);
1747 items[currentItem][currentLine].addString(s);
1748 }
1749}
1750
1751void PrettyPrinter::printDocList(DocumentList* d, int alignmentCol, const std::string& super_before,
1752 const std::string& super_after) {
1753 std::vector<Document*> ld = d->getDocs();
1754 std::string beginToken = d->getBeginToken();
1755 std::string separator = d->getSeparator();
1756 std::string endToken = d->getEndToken();
1757 bool _alignment = d->getAlignment();
1758 if (d->getUnbreakable()) {
1759 addLine(alignmentCol);
1760 }
1761 int currentCol = items[currentItem][currentLine].getIndentation() +
1762 items[currentItem][currentLine].getLength();
1763 int newAlignmentCol =
1764 _alignment ? currentCol + static_cast<int>(beginToken.size()) : alignmentCol;
1765 int vectorSize = static_cast<int>(ld.size());
1766 int lastVisibleElementIndex;
1767 for (int i = 0; i < vectorSize; i++) {
1768 if (!dynamic_cast<BreakPoint*>(ld[i])) lastVisibleElementIndex = i;
1769 }
1770 if (vectorSize == 0) {
1771 printStringDoc(NULL, true, newAlignmentCol, super_before + beginToken, endToken + super_after);
1772 }
1773 for (int i = 0; i < vectorSize; i++) {
1774 Document* subdoc = ld[i];
1775 bool bp = false;
1776 if (dynamic_cast<BreakPoint*>(subdoc)) {
1777 if (!_alignment) newAlignmentCol += indentationBase;
1778 bp = true;
1779 }
1780 std::string af, be;
1781 if (i != vectorSize - 1) {
1782 if (bp || lastVisibleElementIndex <= i)
1783 af = "";
1784 else
1785 af = separator;
1786 } else {
1787 af = endToken + super_after;
1788 }
1789 if (i == 0) {
1790 be = super_before + beginToken;
1791 } else {
1792 be = "";
1793 }
1794 printDocument(subdoc, _alignment, newAlignmentCol, be, af);
1795 }
1796 if (d->getUnbreakable()) {
1797 simplify(currentItem, currentLine, NULL);
1798 }
1799}
1800void PrettyPrinter::simplifyItem(int item) {
1801 linesToSimplify[item].remove(linesNotToSimplify[item]);
1802 std::vector<int>* vec = (linesToSimplify[item].getLinesToSimplify());
1803 while (!vec->empty()) {
1804 if (!simplify(item, (*vec)[0], vec)) break;
1805 }
1806 delete vec;
1807}
1808
1809bool PrettyPrinter::simplify(int item, int line, std::vector<int>* vec) {
1810 if (line == 0) {
1811 linesToSimplify[item].remove(vec, line, false);
1812 return false;
1813 }
1814 if (items[item][line].getLength() > items[item][line - 1].getSpaceLeft(maxwidth)) {
1815 linesToSimplify[item].remove(vec, line, false);
1816 return false;
1817 } else {
1818 linesToSimplify[item].remove(vec, line, true);
1819 items[item][line - 1].concatenateLines(items[item][line]);
1820 items[item].erase(items[item].begin() + line);
1821
1822 linesToSimplify[item].decrementLine(vec, line);
1823 currentLine--;
1824 }
1825
1826 return true;
1827}
1828
1829Printer::Printer(std::ostream& os, int width, bool flatZinc, EnvI* env0)
1830 : env(env0), ism(NULL), printer(NULL), _os(os), _width(width), _flatZinc(flatZinc) {}
1831void Printer::init(void) {
1832 if (ism == NULL) {
1833 ism = new ItemDocumentMapper();
1834 printer = new PrettyPrinter(_width, 4, true, true);
1835 }
1836}
1837Printer::~Printer(void) {
1838 delete printer;
1839 delete ism;
1840}
1841
1842void Printer::p(Document* d) {
1843 printer->print(d);
1844 printer->print(_os);
1845 delete printer;
1846 printer = new PrettyPrinter(_width, 4, true, true);
1847}
1848void Printer::p(const Item* i) {
1849 Document* d;
1850 switch (i->iid()) {
1851 case Item::II_INC:
1852 d = ism->mapIncludeI(*i->cast<IncludeI>());
1853 break;
1854 case Item::II_VD:
1855 d = ism->mapVarDeclI(*i->cast<VarDeclI>());
1856 break;
1857 case Item::II_ASN:
1858 d = ism->mapAssignI(*i->cast<AssignI>());
1859 break;
1860 case Item::II_CON:
1861 d = ism->mapConstraintI(*i->cast<ConstraintI>());
1862 break;
1863 case Item::II_SOL:
1864 d = ism->mapSolveI(*i->cast<SolveI>());
1865 break;
1866 case Item::II_OUT:
1867 d = ism->mapOutputI(*i->cast<OutputI>());
1868 break;
1869 case Item::II_FUN:
1870 d = ism->mapFunctionI(*i->cast<FunctionI>());
1871 break;
1872 }
1873 p(d);
1874 delete d;
1875}
1876
1877void Printer::print(const Expression* e) {
1878 if (_width == 0) {
1879 PlainPrinter p(_os, _flatZinc, env);
1880 p.p(e);
1881 } else {
1882 init();
1883 Document* d = expressionToDocument(e);
1884 p(d);
1885 delete d;
1886 }
1887}
1888void Printer::print(const Item* i) {
1889 if (_width == 0) {
1890 PlainPrinter p(_os, _flatZinc, env);
1891 p.p(i);
1892 } else {
1893 init();
1894 p(i);
1895 }
1896}
1897void Printer::print(const Model* m) {
1898 if (_width == 0) {
1899 PlainPrinter p(_os, _flatZinc, env);
1900 for (unsigned int i = 0; i < m->size(); i++) {
1901 p.p((*m)[i]);
1902 }
1903 } else {
1904 init();
1905 for (unsigned int i = 0; i < m->size(); i++) {
1906 p((*m)[i]);
1907 }
1908 }
1909}
1910
1911} // namespace MiniZinc
1912
1913void debugprint(MiniZinc::Expression* e) { std::cerr << *e << "\n"; }
1914void debugprint(MiniZinc::Item* i) { std::cerr << *i; }
1915void debugprint(MiniZinc::Model* m) {
1916 MiniZinc::Printer p(std::cerr, 0);
1917 p.print(m);
1918}
1919void debugprint(const MiniZinc::Location& loc) { std::cerr << loc << std::endl; }