Project

General

Profile

Revision 933ee7a3

View differences:

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);
src/main_lustre_compiler.ml
262 262
	let traces_out = open_out traces_file in
263 263
	let fmt = formatter_of_out_channel traces_out in
264 264
	Horn_backend.traces_file fmt basename prog machine_code;
265

  
266

  
267 265
	)
268 266
      end
269 267
    | "lustre" ->

Also available in: Unified diff