Line data Source code
1 : // Author(s): Muck van Weerdenburg/Jan Friso Groote
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/data/detail/rewrite/jittyc.h
10 :
11 : #ifndef MCRL2_DATA_MATCH_TREE_H
12 : #define MCRL2_DATA_MATCH_TREE_H
13 :
14 : #include "mcrl2/data/function_symbol.h"
15 : #include "mcrl2/atermpp/aterm_io.h"
16 :
17 : namespace mcrl2
18 : {
19 : namespace data
20 : {
21 : namespace detail
22 : {
23 :
24 : /// This is a list where variables and aterm ints can be stored.
25 : class variable_or_number: public atermpp::aterm
26 : {
27 : public:
28 : /// Default constructor
29 : variable_or_number()
30 : {}
31 :
32 : /// Constructor
33 6392 : variable_or_number(const atermpp::aterm& v):
34 6392 : atermpp::aterm(v)
35 : {
36 6392 : assert(is_variable(v) || v.type_is_int());
37 6392 : }
38 : };
39 :
40 : typedef atermpp::term_list<variable_or_number> variable_or_number_list;
41 :
42 : class match_tree:public atermpp::aterm_appl
43 : {
44 : public:
45 : /// Default constructor
46 30997 : match_tree()
47 30997 : : atermpp::aterm_appl(afunUndefined())
48 30997 : {}
49 :
50 : /// Constructor based on an aterm.
51 104765 : match_tree(const atermpp::aterm& t):
52 104765 : atermpp::aterm_appl(t)
53 : {
54 104765 : assert(!is_defined() || isS() || isA() || isM() || isF() ||
55 : isN() || isD() || isR () || isC() || isX() || isRe() ||
56 : isCRe() || isMe());
57 104765 : }
58 :
59 : protected:
60 149052 : atermpp::function_symbol afunUndefined() const
61 : {
62 149052 : static atermpp::function_symbol afunUndefined("@@Match_tree_dummy",0); // Undefined match term. Used as default match term
63 149052 : return afunUndefined;
64 : }
65 :
66 155625 : atermpp::function_symbol afunS() const
67 : {
68 155625 : static atermpp::function_symbol afunS("@@S",2); // Store term ( target_variable, result_tree )
69 155625 : return afunS;
70 : }
71 :
72 86959 : atermpp::function_symbol afunA() const
73 : {
74 86959 : static atermpp::function_symbol afunA("@@A",1); // Rewrite argument ( number of an argument as an aterm_int )
75 86959 : return afunA;
76 : }
77 :
78 :
79 113034 : atermpp::function_symbol afunM() const
80 : {
81 113034 : static atermpp::function_symbol afunM("@@M",3); // Match term ( match_variable, true_tree , false_tree )
82 113034 : return afunM;
83 : }
84 :
85 93111 : atermpp::function_symbol afunF() const
86 : {
87 93111 : static atermpp::function_symbol afunF("@@F",3); // Match function ( match_function, true_tree, false_tree )
88 93111 : return afunF;
89 : }
90 :
91 93217 : atermpp::function_symbol afunN() const
92 : {
93 93217 : static atermpp::function_symbol afunN("@@N",1); // Go to next parameter ( result_tree )
94 93217 : return afunN;
95 : }
96 :
97 79053 : atermpp::function_symbol afunD() const
98 : {
99 79053 : static atermpp::function_symbol afunD("@@D",1); // Go down a level ( result_tree )
100 79053 : return afunD;
101 : }
102 :
103 43542 : atermpp::function_symbol afunR() const
104 : {
105 43542 : static atermpp::function_symbol afunR("@@R",1); // End of tree ( matching_rule )
106 43542 : return afunR;
107 : }
108 :
109 26486 : atermpp::function_symbol afunC() const
110 : {
111 26486 : static atermpp::function_symbol afunC("@@C",3); // Check condition ( condition, true_tree, false_tree )
112 26486 : return afunC;
113 : }
114 :
115 25692 : atermpp::function_symbol afunX() const
116 : {
117 25692 : static atermpp::function_symbol afunX("@@X",0); // End of tree
118 25692 : return afunX;
119 : }
120 :
121 66991 : atermpp::function_symbol afunRe() const
122 : {
123 66991 : static atermpp::function_symbol afunRe("@@Re",2); // End of tree ( matching_rule , vars_of_rule)
124 66991 : return afunRe;
125 : }
126 :
127 29785 : atermpp::function_symbol afunCRe() const
128 : {
129 29785 : static atermpp::function_symbol afunCRe("@@CRe",4); // End of tree ( condition, matching_rule, vars_of_condition, vars_of_rule )
130 29785 : return afunCRe;
131 : }
132 :
133 8462 : atermpp::function_symbol afunMe() const
134 : {
135 8462 : static atermpp::function_symbol afunMe("@@Me",2); // Match term ( match_variable, variable_index )
136 8462 : return afunMe;
137 : }
138 :
139 : public:
140 118055 : bool is_defined() const
141 : {
142 118055 : return this->function()!=afunUndefined();
143 : }
144 :
145 147416 : bool isS() const
146 : {
147 147416 : return this->function()==afunS();
148 : }
149 :
150 85671 : bool isA() const
151 : {
152 85671 : return this->function()==afunA();
153 : }
154 :
155 111312 : bool isM() const
156 : {
157 111312 : return this->function()==afunM();
158 : }
159 :
160 86623 : bool isF() const
161 : {
162 86623 : return this->function()==afunF();
163 : }
164 :
165 85625 : bool isN() const
166 : {
167 85625 : return this->function()==afunN();
168 : }
169 :
170 73943 : bool isD() const
171 : {
172 73943 : return this->function()==afunD();
173 : }
174 :
175 39734 : bool isR() const
176 : {
177 39734 : return this->function()==afunR();
178 : }
179 :
180 26394 : bool isC() const
181 : {
182 26394 : return this->function()==afunC();
183 : }
184 :
185 23916 : bool isX() const
186 : {
187 23916 : return this->function()==afunX();
188 : }
189 :
190 59099 : bool isRe() const
191 : {
192 59099 : return this->function()==afunRe();
193 : }
194 :
195 29453 : bool isCRe() const
196 : {
197 29453 : return this->function()==afunCRe();
198 : }
199 :
200 7930 : bool isMe() const
201 : {
202 7930 : return this->function()==afunMe();
203 : }
204 : };
205 :
206 : // Store term ( target_variable, result_tree )
207 : class match_tree_S:public match_tree
208 : {
209 : public:
210 : match_tree_S()
211 : {}
212 :
213 18379 : match_tree_S(const atermpp::aterm& t)
214 18379 : : match_tree(t)
215 : {
216 18379 : assert(isS());
217 18379 : }
218 :
219 8209 : match_tree_S(const variable& target_variable, const match_tree& result_tree)
220 8209 : : match_tree(atermpp::aterm_appl(afunS(),target_variable,result_tree))
221 8209 : {}
222 :
223 24391 : const variable& target_variable() const
224 : {
225 24391 : return atermpp::down_cast<const variable>((*this)[0]);
226 : }
227 :
228 4581 : const match_tree& subtree() const
229 : {
230 4581 : return atermpp::down_cast<const match_tree>((*this)[1]);
231 : }
232 : };
233 :
234 : // Rewrite argument ( a number of an arguments as a aterm_int )
235 :
236 : class match_tree_A:public match_tree
237 : {
238 : public:
239 : match_tree_A()
240 : {}
241 :
242 1906 : match_tree_A(const atermpp::aterm& t)
243 1906 : : match_tree(t)
244 : {
245 1906 : assert(isA());
246 1906 : }
247 :
248 1288 : match_tree_A(const std::size_t n)
249 1288 : : match_tree(atermpp::aterm_appl(afunA(),atermpp::aterm_int(n)))
250 1288 : {}
251 :
252 1906 : std::size_t variable_index() const
253 : {
254 1906 : return atermpp::down_cast<const atermpp::aterm_int>((*this)[0]).value();
255 : }
256 : };
257 :
258 :
259 : // Match term ( match_variable, true_tree , false_tree )
260 : class match_tree_M:public match_tree
261 : {
262 : public:
263 : match_tree_M()
264 : {}
265 :
266 1410 : match_tree_M(const atermpp::aterm& t)
267 1410 : : match_tree(t)
268 : {
269 1410 : assert(isM());
270 1410 : }
271 :
272 1722 : match_tree_M(const variable& match_variable, const match_tree& true_tree, const match_tree& false_tree)
273 1722 : : match_tree(atermpp::aterm_appl(afunM(),match_variable,true_tree,false_tree))
274 1722 : {}
275 :
276 1410 : const variable& match_variable() const
277 : {
278 1410 : return atermpp::down_cast<const variable>((*this)[0]);
279 : }
280 :
281 1268 : const match_tree& true_tree() const
282 : {
283 1268 : return atermpp::down_cast<const match_tree>((*this)[1]);
284 : }
285 :
286 1268 : const match_tree& false_tree() const
287 : {
288 1268 : return atermpp::down_cast<const match_tree>((*this)[2]);
289 : }
290 : };
291 :
292 : // Match function ( match_function, true_tree, false_tree )
293 : class match_tree_F:public match_tree
294 : {
295 : public:
296 : match_tree_F()
297 : {}
298 :
299 4918 : match_tree_F(const atermpp::aterm& t)
300 4918 : : match_tree(t)
301 : {
302 4918 : assert(isF());
303 4918 : }
304 :
305 6488 : match_tree_F(const data::function_symbol& function, const match_tree& true_tree, const match_tree& false_tree)
306 6488 : : match_tree(atermpp::aterm_appl(afunF(),function,true_tree,false_tree))
307 6488 : {}
308 :
309 5882 : const data::function_symbol& function() const
310 : {
311 5882 : return atermpp::down_cast<const data::function_symbol>((*this)[0]);
312 : }
313 :
314 1704 : const match_tree& true_tree() const
315 : {
316 1704 : return atermpp::down_cast<const match_tree>((*this)[1]);
317 : }
318 :
319 1704 : const match_tree& false_tree() const
320 : {
321 1704 : return atermpp::down_cast<const match_tree>((*this)[2]);
322 : }
323 : };
324 :
325 : // Go to next parameter ( result_tree )
326 : class match_tree_N:public match_tree
327 : {
328 : public:
329 : match_tree_N()
330 : {}
331 :
332 3442 : match_tree_N(const atermpp::aterm& t)
333 3442 : : match_tree(t)
334 : {
335 3442 : assert(isN());
336 3442 : }
337 :
338 : /// Constructor. Builds a new term around a match_tree.
339 : /// The extra non-used std::size_t is provided, to distinghuish this
340 : /// constructor from the default copy constructor.
341 7592 : match_tree_N(const match_tree& result_tree, std::size_t)
342 7592 : : match_tree(atermpp::aterm_appl(afunN(),result_tree))
343 7592 : {}
344 :
345 3442 : const match_tree& subtree() const
346 : {
347 3442 : return atermpp::down_cast<const match_tree>((*this)[0]);
348 : }
349 : };
350 :
351 : // Go down a level ( result_tree )
352 : class match_tree_D:public match_tree
353 : {
354 : public:
355 : match_tree_D()
356 : {}
357 :
358 1168 : match_tree_D(const atermpp::aterm& t)
359 1168 : : match_tree(t)
360 : {
361 1168 : assert(isD());
362 1168 : }
363 :
364 : /// Constructor. Builds a new term around a match_tree.
365 : /// The extra non-used std::size_t is provided, to distinghuish this
366 : /// constructor from the default copy constructor.
367 5110 : match_tree_D(const match_tree& result_tree, std::size_t)
368 5110 : : match_tree(atermpp::aterm_appl(afunD(),result_tree))
369 5110 : {}
370 :
371 1168 : const match_tree& subtree() const
372 : {
373 1168 : return atermpp::down_cast<const match_tree>((*this)[0]);
374 : }
375 : };
376 :
377 : // End of tree ( matching_rule )
378 : class match_tree_R:public match_tree
379 : {
380 :
381 : public:
382 : match_tree_R()
383 : {}
384 :
385 2502 : match_tree_R(const atermpp::aterm& t)
386 2502 : : match_tree(t)
387 : {
388 2502 : assert(isR());
389 2502 : }
390 :
391 3808 : match_tree_R(const data_expression& e)
392 3808 : : match_tree(atermpp::aterm_appl(afunR(),e))
393 3808 : {}
394 :
395 3753 : const data_expression& result() const
396 : {
397 3753 : return atermpp::down_cast<const data_expression>((*this)[0]);
398 : }
399 : };
400 :
401 : // Check condition ( condition, true_tree, false_tree )
402 : class match_tree_C:public match_tree
403 : {
404 : public:
405 : match_tree_C()
406 : {}
407 :
408 116 : match_tree_C(const atermpp::aterm& t)
409 116 : : match_tree(t)
410 : {
411 116 : assert(isC());
412 116 : }
413 :
414 92 : match_tree_C(const data_expression& condition, const match_tree& true_tree, const match_tree& false_tree)
415 92 : : match_tree(atermpp::aterm_appl(afunC(),condition,true_tree,false_tree))
416 92 : {}
417 :
418 116 : const data_expression& condition() const
419 : {
420 116 : return atermpp::down_cast<const data_expression>((*this)[0]);
421 : }
422 :
423 116 : const match_tree& true_tree() const
424 : {
425 116 : return atermpp::down_cast<const match_tree>((*this)[1]);
426 : }
427 :
428 116 : const match_tree& false_tree() const
429 : {
430 116 : return atermpp::down_cast<const match_tree>((*this)[2]);
431 : }
432 : };
433 :
434 : // End of tree
435 : class match_tree_X:public match_tree
436 : {
437 : public:
438 : match_tree_X(const atermpp::aterm& t)
439 : : match_tree(t)
440 : {
441 : assert(isX());
442 : }
443 :
444 1776 : match_tree_X()
445 1776 : : match_tree(atermpp::aterm_appl(afunX()))
446 1776 : {}
447 : };
448 :
449 : // End of tree ( matching_rule , vars_of_rule)
450 : // The var_of_rule is a list with variables and aterm_ints.
451 : class match_tree_Re:public match_tree
452 : {
453 : public:
454 13290 : match_tree_Re()
455 13290 : {}
456 :
457 9182 : match_tree_Re(const atermpp::aterm& t)
458 9182 : : match_tree(t)
459 : {
460 9182 : assert(isRe());
461 9182 : }
462 :
463 7892 : match_tree_Re(const data_expression& result, const variable_or_number_list& vars)
464 7892 : : match_tree(atermpp::aterm_appl(afunRe(),result,vars))
465 7892 : {}
466 :
467 9028 : const data_expression& result() const
468 : {
469 9028 : return atermpp::down_cast<const data_expression>((*this)[0]);
470 : }
471 :
472 9028 : const variable_or_number_list& variables() const
473 : {
474 9028 : return atermpp::down_cast<const variable_or_number_list>((*this)[1]);
475 : }
476 : };
477 :
478 : // End of tree ( condition, matching_rule, vars_of_condition, vars_of_rule )
479 : // The last two parameters consist of a list with variables and numbers.
480 : class match_tree_CRe:public match_tree
481 : {
482 : public:
483 : match_tree_CRe()
484 : {}
485 :
486 336 : match_tree_CRe(const atermpp::aterm& t)
487 336 : : match_tree(t)
488 : {
489 336 : assert(isCRe());
490 336 : }
491 :
492 332 : match_tree_CRe(const data_expression& condition, const data_expression& result, const variable_or_number_list& vars_condition, const variable_or_number_list& vars_rule)
493 332 : : match_tree(atermpp::aterm_appl(afunCRe(),condition,result,vars_condition,vars_rule))
494 332 : {}
495 :
496 336 : const data_expression& condition() const
497 : {
498 336 : return atermpp::down_cast<const data_expression>((*this)[0]);
499 : }
500 :
501 336 : const data_expression& result() const
502 : {
503 336 : return atermpp::down_cast<const data_expression>((*this)[1]);
504 : }
505 :
506 336 : const variable_or_number_list& variables_condition() const
507 : {
508 336 : return atermpp::down_cast<const variable_or_number_list>((*this)[2]);
509 : }
510 :
511 336 : const variable_or_number_list& variables_result() const
512 : {
513 336 : return atermpp::down_cast<const variable_or_number_list>((*this)[3]);
514 : }
515 : };
516 :
517 : // Match term ( match_variable, variable_index )
518 : class match_tree_Me:public match_tree
519 : {
520 : public:
521 : match_tree_Me()
522 : {}
523 :
524 1198 : match_tree_Me(const atermpp::aterm& t)
525 1198 : : match_tree(t)
526 : {
527 1198 : assert(isMe());
528 1198 : }
529 :
530 532 : match_tree_Me(const variable& match_variable, const std::size_t variable_index)
531 532 : : match_tree(atermpp::aterm_appl(afunMe(),match_variable,atermpp::aterm_int(variable_index)))
532 532 : {}
533 :
534 1198 : const variable& match_variable() const
535 : {
536 1198 : return atermpp::down_cast<const variable>((*this)[0]);
537 : }
538 :
539 1198 : std::size_t variable_index() const
540 : {
541 1198 : return (atermpp::down_cast<const atermpp::aterm_int>((*this)[1])).value();
542 : }
543 : };
544 :
545 : typedef atermpp::term_list < match_tree > match_tree_list;
546 : typedef std::vector < match_tree > match_tree_vector;
547 : typedef atermpp::term_list < match_tree_list > match_tree_list_list;
548 : typedef atermpp::term_list < match_tree_list_list > match_tree_list_list_list;
549 :
550 : // Structure for build_tree parameters
551 : class build_pars
552 : {
553 : public:
554 : match_tree_list_list Flist; // List of sequences of which the first action is an F
555 : match_tree_list_list Slist; // List of sequences of which the first action is an S
556 : match_tree_list_list Mlist; // List of sequences of which the first action is an M
557 : match_tree_list_list_list stack; // Stack to maintain the sequences that do not have to
558 : // do anything in the current term
559 : match_tree_list_list upstack; // List of sequences that have done an F at the current
560 : // level
561 :
562 : // Initialise.
563 1080 : build_pars()
564 1080 : : Flist(),
565 1080 : Slist(),
566 1080 : Mlist(),
567 2160 : stack({ match_tree_list_list() }),
568 1080 : upstack()
569 :
570 : {
571 1080 : }
572 : };
573 :
574 :
575 : inline
576 7750 : std::ostream& operator<<(std::ostream& s, const match_tree& t)
577 : {
578 : using atermpp::down_cast;
579 7750 : if (t.isS())
580 : {
581 1527 : const match_tree_S& tS = down_cast<match_tree_S>(t);
582 1527 : s << "@@S(" << tS.target_variable() << ", " << tS.subtree() << ")";
583 : }
584 : else
585 6223 : if (t.isA())
586 : {
587 722 : const match_tree_A& tA = down_cast<match_tree_A>(t);
588 722 : s << "@@A(" << tA.variable_index() << ")";
589 : }
590 : else
591 5501 : if (t.isM())
592 : {
593 368 : const match_tree_M& tM = down_cast<match_tree_M>(t);
594 368 : s << "@@M(" << tM.match_variable() << ", " << tM.true_tree() << ", " << tM.false_tree() << ")";
595 : }
596 : else
597 5133 : if (t.isF())
598 : {
599 852 : const match_tree_F& tF = down_cast<match_tree_F>(t);
600 852 : s << "@@F(" << tF.function() << ", " << tF.true_tree() << ", " << tF.false_tree() << ")";
601 : }
602 : else
603 4281 : if (t.isN())
604 : {
605 1721 : const match_tree_N& tN = down_cast<match_tree_N>(t);
606 1721 : s << "@@N(" << tN.subtree() << ")";
607 : }
608 : else
609 2560 : if (t.isD())
610 : {
611 584 : const match_tree_D& tD = down_cast<match_tree_D>(t);
612 584 : s << "@@D(" << tD.subtree() << ")";
613 : }
614 : else
615 1976 : if (t.isR())
616 : {
617 1251 : const match_tree_R& tR = down_cast<match_tree_R>(t);
618 1251 : s << "@@R(" << tR.result() << ")";
619 : }
620 : else
621 725 : if (t.isC())
622 : {
623 58 : const match_tree_C& tC = down_cast<match_tree_C>(t);
624 58 : s << "@@C(" << tC.condition() << ", " << tC.true_tree() << ", " << tC.false_tree() << ")";
625 : }
626 : else
627 667 : if (t.isX())
628 : {
629 667 : s << "@@X";
630 : }
631 : else
632 0 : if (t.isRe())
633 : {
634 0 : const match_tree_Re& tRe = down_cast<match_tree_Re>(t);
635 0 : s << "@@Re(" << tRe.result() << ", " << tRe.variables() << ")";
636 : }
637 : else
638 0 : if (t.isCRe())
639 : {
640 0 : const match_tree_CRe& tCRe = down_cast<match_tree_CRe>(t);
641 0 : s << "@@CRe(" << tCRe.condition() << ", " << tCRe.result() << ", "
642 0 : << tCRe.variables_condition() << ", " << tCRe.variables_result() << ")";
643 : }
644 : else
645 0 : if (t.isMe())
646 : {
647 0 : const match_tree_Me& tMe = down_cast<match_tree_Me>(t);
648 0 : s << "@@Me(" << tMe.match_variable() << ", " << tMe.variable_index() << ")";
649 : }
650 7750 : return s;
651 : }
652 :
653 : } // namespace detail
654 :
655 : } // namespace data
656 :
657 : } // namespace mcrl2
658 :
659 : #endif // MCRL2_DATA_MATCH_TREE_H
|
