Revision b8dfc744
Added by Pierre-Loïc Garoche almost 4 years ago
| src/tools/seal/seal_export.ml | ||
|---|---|---|
| 101 | 101 |
|
| 102 | 102 |
|
| 103 | 103 |
let to_lustre basename prog m sw_init sw_step init_out update_out = |
| 104 |
let loc = Location.dummy_loc in |
|
| 104 | 105 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
| 105 |
|
|
| 106 |
Global.type_env := Typing.type_node !Global.type_env new_node loc; |
|
| 107 |
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node; |
|
| 108 |
|
|
| 106 | 109 |
(* Format.eprintf "%a@." Printers.pp_node new_node; *) |
| 107 | 110 |
|
| 108 | 111 |
(* Main output *) |
| ... | ... | |
| 110 | 113 |
let new_top = |
| 111 | 114 |
Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node) |
| 112 | 115 |
in |
| 113 |
let out = open_out output_file in |
|
| 116 |
let out = open_out output_file in
|
|
| 114 | 117 |
let fmt = Format.formatter_of_out_channel out in |
| 115 | 118 |
Format.fprintf fmt "%a@." Printers.pp_prog [new_top]; |
| 116 | 119 |
|
Also available in: Unified diff
valid _verif node for seal-export lustre