Revision 99d9ac94
Added by Teme Kahsai over 8 years ago
| src/backends/Horn/horn_backend.ml | ||
|---|---|---|
| 328 | 328 |
Format.pp_print_newline fmt (); |
| 329 | 329 |
|
| 330 | 330 |
(* Rule for init *) |
| 331 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
| 332 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
| 333 |
pp_machine_init_name m.mname.node_id
|
|
| 334 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
|
| 331 |
(* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
|
|
| 332 |
(* (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
|
|
| 333 |
(* pp_machine_init_name m.mname.node_id *)
|
|
| 334 |
(* (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); *)
|
|
| 335 | 335 |
|
| 336 | 336 |
(* (\* Rule for step *\) *) |
| 337 | 337 |
(* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *) |
Also available in: Unified diff
fixing double printing of horn rules
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@419 041b043f-8d7c-46b2-b46e-ef0dd855326e