Revision a7062da6
Added by LĂ©lio Brun over 3 years ago
src/backends/Horn/horn_backend_printers.ml | ||
---|---|---|
14 | 14 |
|
15 | 15 |
This is a modified version that handle reset *) |
16 | 16 |
|
17 |
open Utils |
|
17 | 18 |
open Format |
18 | 19 |
open Lustre_types |
19 | 20 |
open Machine_code_types |
... | ... | |
218 | 219 |
in |
219 | 220 |
|
220 | 221 |
fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n) |
221 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
222 |
(pp_print_list (pp_horn_var m))
|
|
222 | 223 |
(rename_machine_list (concat m.mname.node_id i) |
223 | 224 |
(rename_current_list (full_memory_vars machines target_machine)) |
224 | 225 |
@ rename_machine_list (concat m.mname.node_id i) |
... | ... | |
261 | 262 |
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x; |
262 | 263 |
fprintf fmt ")@]" |
263 | 264 |
| _ -> |
264 |
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n)
|
|
265 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
|
|
266 |
inputs |
|
267 |
(Utils.pp_final_char_if_non_empty "@ " inputs)
|
|
268 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
|
|
265 |
fprintf fmt "(%a @[<v 0>%a%a%a)@]" pp_machine_step_name (node_name n)
|
|
266 |
(pp_print_list ~pp_epilogue:pp_print_cut
|
|
267 |
(pp_horn_val m self (pp_horn_var m))) inputs
|
|
268 |
(pp_print_list ~pp_epilogue:pp_print_cut
|
|
269 |
(pp_horn_val m self (pp_horn_var m)))
|
|
269 | 270 |
(List.map (fun v -> mk_val (Var v) v.var_type) outputs) |
270 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
|
271 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
272 |
(mid_mems @ next_mems) |
|
271 |
(pp_print_list (pp_horn_var m)) (mid_mems @ next_mems) |
|
273 | 272 |
with Not_found -> |
274 | 273 |
(* stateless node instance *) |
275 | 274 |
let n, _ = List.assoc i m.mcalls in |
276 |
fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n) |
|
277 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
|
278 |
inputs |
|
279 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
|
280 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) |
|
275 |
fprintf fmt "(%a @[<v 0>%a%a)@]" pp_machine_stateless_name (node_name n) |
|
276 |
(pp_print_list ~pp_epilogue:pp_print_cut |
|
277 |
(pp_horn_val m self (pp_horn_var m))) inputs |
|
278 |
(pp_print_list (pp_horn_val m self (pp_horn_var m))) |
|
281 | 279 |
(List.map (fun v -> mk_val (Var v) v.var_type) outputs) |
282 | 280 |
|
283 | 281 |
(* Print the instruction and update the set of reset instances *) |
... | ... | |
370 | 368 |
fprintf fmt "@[<v 5>(and @ "; |
371 | 369 |
|
372 | 370 |
(* print "x_m = x_c" for each local memory *) |
373 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
|
371 |
(pp_print_list (fun fmt v ->
|
|
374 | 372 |
fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m) |
375 | 373 |
(rename_current v))) |
376 | 374 |
fmt locals; |
... | ... | |
378 | 376 |
|
379 | 377 |
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special |
380 | 378 |
treatment for _arrow: _first = true *) |
381 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
|
|
379 |
(pp_print_list (fun fmt (id, (n, _)) ->
|
|
382 | 380 |
let name = node_name n in |
383 | 381 |
if name = "_arrow" then |
384 | 382 |
fprintf fmt "(= %s._arrow._first_m true)" (concat m.mname.node_id id) |
385 | 383 |
else |
386 | 384 |
let machine_n = get_machine machines name in |
387 | 385 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" name |
388 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
386 |
(pp_print_list (pp_horn_var m))
|
|
389 | 387 |
(rename_machine_list |
390 | 388 |
(concat m.mname.node_id id) |
391 | 389 |
(reset_vars machines machine_n)))) |
... | ... | |
405 | 403 |
fprintf fmt "; %s@." m.mname.node_id; |
406 | 404 |
|
407 | 405 |
(* Printing variables *) |
408 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
|
406 |
pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
|
|
409 | 407 |
(inout_vars m |
410 | 408 |
@ rename_current_list (full_memory_vars machines m) |
411 | 409 |
@ rename_mid_list (full_memory_vars machines m) |
... | ... | |
417 | 415 |
(* Declaring single predicate *) |
418 | 416 |
fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name |
419 | 417 |
m.mname.node_id |
420 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
418 |
(pp_print_list pp_type)
|
|
421 | 419 |
(List.map (fun v -> v.var_type) (inout_vars m)); |
422 | 420 |
|
423 | 421 |
match m.mstep.step_asserts with |
... | ... | |
430 | 428 |
(* No reset info for stateless nodes *) m fmt m.mstep.step_instrs); |
431 | 429 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name |
432 | 430 |
m.mname.node_id |
433 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
|
431 |
(pp_print_list (pp_horn_var m))
|
|
434 | 432 |
(inout_vars m) |
435 | 433 |
| assertsl -> |
436 | 434 |
let pp_val = |
... | ... | |
443 | 441 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
444 | 442 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) |
445 | 443 |
assertsl pp_machine_stateless_name m.mname.node_id |
446 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
|
444 |
(pp_print_list (pp_horn_var m))
|
|
447 | 445 |
(step_vars machines m)) |
448 | 446 |
else ( |
449 | 447 |
(* Declaring predicate *) |
450 | 448 |
fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name |
451 | 449 |
m.mname.node_id |
452 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
450 |
(pp_print_list pp_type)
|
|
453 | 451 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
454 | 452 |
|
455 | 453 |
fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id |
456 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
454 |
(pp_print_list pp_type)
|
|
457 | 455 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
458 | 456 |
|
459 | 457 |
pp_print_newline fmt (); |
... | ... | |
462 | 460 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
463 | 461 |
(pp_machine_reset machines) |
464 | 462 |
m pp_machine_reset_name m.mname.node_id |
465 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
463 |
(pp_print_list (pp_horn_var m))
|
|
466 | 464 |
(reset_vars machines m); |
467 | 465 |
|
468 | 466 |
match m.mstep.step_asserts with |
... | ... | |
473 | 471 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
474 | 472 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name |
475 | 473 |
m.mname.node_id |
476 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
474 |
(pp_print_list (pp_horn_var m))
|
|
477 | 475 |
(step_vars machines m) |
478 | 476 |
| assertsl -> |
479 | 477 |
let pp_val = |
... | ... | |
487 | 485 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
488 | 486 |
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) |
489 | 487 |
assertsl pp_machine_step_name m.mname.node_id |
490 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
|
488 |
(pp_print_list (pp_horn_var m))
|
|
491 | 489 |
(step_vars machines m))) |
492 | 490 |
|
493 | 491 |
let mk_flags arity = |
... | ... | |
527 | 525 |
(* Check if there is annotation for s-function *) |
528 | 526 |
if m.mannot != [] then |
529 | 527 |
Format.fprintf fmt "; @[%a@]@]@\n" |
530 |
(Utils.fprintf_list ~sep:"@ " Printers.pp_s_function)
|
|
528 |
(pp_print_list Printers.pp_s_function)
|
|
531 | 529 |
m.mannot; |
532 | 530 |
|
533 | 531 |
(* Printing variables *) |
534 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
|
532 |
pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
|
|
535 | 533 |
(step_vars machines m |
536 | 534 |
@ rename_machine_list m.mname.node_id m.mstep.step_locals); |
537 | 535 |
Format.pp_print_newline fmt (); |
... | ... | |
541 | 539 |
(* Declaring single predicate *) |
542 | 540 |
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name |
543 | 541 |
m.mname.node_id |
544 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
542 |
(pp_print_list pp_type)
|
|
545 | 543 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
546 | 544 |
Format.pp_print_newline fmt (); |
547 | 545 |
(* Rule for single predicate *) |
548 | 546 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
549 | 547 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
550 | 548 |
str_flags |
551 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
|
549 |
(pp_print_list (pp_horn_var m))
|
|
552 | 550 |
(reset_vars machines m) pp_machine_stateless_name m.mname.node_id |
553 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
|
551 |
(pp_print_list (pp_horn_var m))
|
|
554 | 552 |
(reset_vars machines m)) |
555 | 553 |
else ( |
556 | 554 |
(* Declaring predicate *) |
557 | 555 |
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name |
558 | 556 |
m.mname.node_id |
559 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
557 |
(pp_print_list pp_type)
|
|
560 | 558 |
(List.map (fun v -> v.var_type) (inout_vars m)); |
561 | 559 |
|
562 | 560 |
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name |
563 | 561 |
m.mname.node_id |
564 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
562 |
(pp_print_list pp_type)
|
|
565 | 563 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
566 | 564 |
|
567 | 565 |
Format.pp_print_newline fmt (); |
... | ... | |
573 | 571 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
574 | 572 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name |
575 | 573 |
m.mname.node_id |
576 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
574 |
(pp_print_list (pp_horn_var m))
|
|
577 | 575 |
(step_vars machines m) |
578 | 576 |
| assertsl -> |
579 | 577 |
let pp_val = |
... | ... | |
587 | 585 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
588 | 586 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
589 | 587 |
pp_machine_step_name m.mname.node_id |
590 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
|
588 |
(pp_print_list (pp_horn_var m))
|
|
591 | 589 |
(step_vars machines m))) |
592 | 590 |
|
593 | 591 |
(**************** XML printing functions *************) |
... | ... | |
606 | 604 |
| Expr_array a -> |
607 | 605 |
fprintf fmt "[%a]" pp_xml_tuple a |
608 | 606 |
| Expr_access (a, d) -> |
609 |
fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
|
|
607 |
fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp d |
|
610 | 608 |
| Expr_power (a, d) -> |
611 |
fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
|
|
609 |
fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp d |
|
612 | 610 |
| Expr_tuple el -> |
613 | 611 |
fprintf fmt "(%a)" pp_xml_tuple el |
614 | 612 |
| Expr_ite (c, t, e) -> |
... | ... | |
628 | 626 |
| Expr_appl (id, e, r) -> |
629 | 627 |
pp_xml_app fmt id e r) |
630 | 628 |
|
631 |
and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
|
|
629 |
and pp_xml_tuple fmt el = pp_comma_list pp_xml_expr fmt el
|
|
632 | 630 |
|
633 | 631 |
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h |
634 | 632 |
|
635 |
and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
|
|
633 |
and pp_xml_handlers fmt hl = pp_print_list pp_xml_handler fmt hl
|
|
636 | 634 |
|
637 | 635 |
and pp_xml_app fmt id e r = |
638 | 636 |
match r with |
... | ... | |
684 | 682 |
|
685 | 683 |
and pp_xml_eexpr fmt e = |
686 | 684 |
fprintf fmt "%a%t %a" |
687 |
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
|
|
685 |
(pp_print_list ~pp_sep:pp_print_semicolon Printers.pp_quantifiers)
|
|
688 | 686 |
e.eexpr_quantifiers |
689 | 687 |
(fun fmt -> |
690 | 688 |
match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";") |
... | ... | |
709 | 707 |
Format.pp_print_string fmt x |
710 | 708 |
| _ -> |
711 | 709 |
Format.fprintf fmt "%a" |
712 |
(Utils.fprintf_list ~sep:"/" Format.pp_print_string) |
|
710 |
(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/") |
|
711 |
pp_print_string) |
|
713 | 712 |
kwds) |
714 | 713 |
pp_xml_sf_value ee |
715 | 714 |
in |
716 |
Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
|
|
715 |
pp_print_list pp_xml_annot fmt expr_ann.annots
|
|
717 | 716 |
|
718 | 717 |
and pp_xml_expr_annot fmt expr_ann = |
719 | 718 |
let pp_xml_annot fmt (kwds, ee) = |
... | ... | |
726 | 725 |
Format.pp_print_string fmt x |
727 | 726 |
| _ -> |
728 | 727 |
Format.fprintf fmt "/%a/" |
729 |
(Utils.fprintf_list ~sep:"/" Format.pp_print_string) |
|
728 |
(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/") |
|
729 |
pp_print_string) |
|
730 | 730 |
kwds) |
731 | 731 |
pp_xml_eexpr ee |
732 | 732 |
in |
733 |
Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
|
|
733 |
pp_print_list pp_xml_annot fmt expr_ann.annots
|
|
734 | 734 |
|
735 | 735 |
(* Local Variables: *) |
736 | 736 |
(* compile-command:"make -C ../../.." *) |
Also available in: Unified diff
another step towards refactoring