Revision 933ee7a3
Added by Teme Kahsai almost 10 years ago
src/backends/Horn/horn_backend.ml | ||
---|---|---|
626 | 626 |
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) |
627 | 627 |
in |
628 | 628 |
|
629 |
Format.fprintf fmt " <Init name=\"%a\">@."
|
|
630 |
pp_machine_init_name m.mname.node_id;
|
|
631 |
|
|
629 |
let pp_prefix_rev fmt prefix =
|
|
630 |
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
|
|
631 |
in |
|
632 | 632 |
|
633 |
let input_vars = rename_machine_list m.mname.node_id m.mstep.step_inputs in |
|
634 |
Format.fprintf fmt "\t<input name=\"%a\" type=\"%a\">%a</input> @." |
|
633 |
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in |
|
634 |
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in |
|
635 |
Format.fprintf fmt " <input name=\"%a\" type=\"%a\">%a</input> @." |
|
635 | 636 |
(Utils.fprintf_list ~sep:" | " pp_var) input_vars |
636 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) input_vars
|
|
637 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) input_vars
|
|
637 | 638 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs); |
638 | 639 |
|
639 |
Format.fprintf fmt "\t<output name=\"%a\" type=\"\">%a</output> @." |
|
640 |
(Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_outputs) |
|
640 |
Format.fprintf fmt " <output name=\"%a\" type=\"%a\">%a</output> @." |
|
641 |
(Utils.fprintf_list ~sep:" | " pp_var) output_vars |
|
642 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars |
|
641 | 643 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
642 | 644 |
|
643 |
Format.fprintf fmt "\t<local name=\"%a\" type=\"\">%t%a</local> @." |
|
644 |
(Utils.fprintf_list ~sep:" | " pp_var) (rename_next_list (full_memory_vars machines m)) |
|
645 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ") |
|
646 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; |
|
647 |
|
|
648 |
Format.fprintf fmt " </Init>@."; |
|
649 |
|
|
645 |
let init_local_vars = (rename_next_list (full_memory_vars machines m)) in |
|
646 |
let step_local_vars = (rename_current_list (full_memory_vars machines m)) in |
|
650 | 647 |
|
651 |
Format.fprintf fmt " <Step name=\"%a\">@." |
|
652 |
pp_machine_step_name m.mname.node_id; |
|
653 |
|
|
654 |
Format.fprintf fmt "\t<input name=\"%a\" type=\"\">%a</input> @." |
|
655 |
(Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_inputs) |
|
656 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs); |
|
657 |
|
|
658 |
Format.fprintf fmt "\t<output name=\"%a\" type=\"\">%a</output> @." |
|
659 |
(Utils.fprintf_list ~sep:" | " pp_var) (rename_machine_list m.mname.node_id m.mstep.step_outputs) |
|
660 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
|
648 |
Format.fprintf fmt " <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @." |
|
649 |
(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars |
|
650 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) init_local_vars |
|
651 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "") |
|
652 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next; |
|
661 | 653 |
|
662 |
Format.fprintf fmt "\t<local name=\"%a\" type=\"\">%t%a</local> @." |
|
663 |
(Utils.fprintf_list ~sep:" | " pp_var) ((rename_current_list (full_memory_vars machines m)) @ |
|
664 |
(rename_next_list (full_memory_vars machines m))) |
|
665 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ") |
|
666 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next); |
|
654 |
Format.fprintf fmt " <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @." |
|
655 |
(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars |
|
656 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) step_local_vars |
|
657 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "") |
|
658 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)" |
|
659 |
Printers.pp_expr ee)) (memories_old); |
|
667 | 660 |
|
668 |
Format.fprintf fmt " </Step>@."; |
|
669 | 661 |
Format.fprintf fmt " </Node>@."; |
670 | 662 |
|
671 | 663 |
) (List.rev machines); |
Also available in: Unified diff
synch with svn