Revision a0c92fa8
Added by Pierre-Loïc Garoche over 2 years ago
| src/tools/seal/seal_export.ml | ||
|---|---|---|
| 62 | 62 |
match g_opt with |
| 63 | 63 |
| None -> ( |
| 64 | 64 |
Format.eprintf "SEAL issue: process_sw with %a" |
| 65 |
pp_sys sw
|
|
| 65 |
(pp_sys Printers.pp_expr) sw
|
|
| 66 | 66 |
; |
| 67 | 67 |
assert false (* How could this happen anyway ? *) |
| 68 | 68 |
) |
| ... | ... | |
| 117 | 117 |
in |
| 118 | 118 |
new_nd, orig_nd |
| 119 | 119 |
|
| 120 |
|
|
| 121 |
let funsw_to_lustre m update_out = |
|
| 122 |
let orig_nd = m.mname in |
|
| 123 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
|
| 124 |
let output_eq = |
|
| 125 |
let e_update_out = process_sw copy_nd.node_outputs (fun x -> x) update_out in |
|
| 126 |
[ |
|
| 127 |
Eq |
|
| 128 |
{ eq_loc = Location.dummy_loc;
|
|
| 129 |
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; |
|
| 130 |
eq_rhs = e_update_out |
|
| 131 |
}; |
|
| 132 |
] |
|
| 133 |
in |
|
| 134 |
let new_nd = |
|
| 135 |
{ copy_nd with
|
|
| 136 |
node_id = copy_nd.node_id ^ "_seal"; |
|
| 137 |
node_locals = []; |
|
| 138 |
node_stmts = output_eq; |
|
| 139 |
} |
|
| 140 |
in |
|
| 141 |
new_nd, orig_nd |
|
| 142 |
|
|
| 120 | 143 |
|
| 121 |
let to_lustre basename prog m sw_init sw_step init_out update_out = |
|
| 144 |
|
|
| 145 |
let to_lustre basename prog new_node orig_node = |
|
| 122 | 146 |
let loc = Location.dummy_loc in |
| 123 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
|
| 124 | 147 |
Global.type_env := Typing.type_node !Global.type_env new_node loc; |
| 125 | 148 |
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node; |
| 126 | 149 |
|
| ... | ... | |
| 139 | 162 |
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in |
| 140 | 163 |
let out_verif = open_out output_file_verif in |
| 141 | 164 |
let fmt_verif = Format.formatter_of_out_channel out_verif in |
| 142 |
let check_nd = Lustre_utils.check_eq new_node orig_nd in
|
|
| 165 |
let check_nd = Lustre_utils.check_eq new_node orig_node in
|
|
| 143 | 166 |
let check_top = |
| 144 | 167 |
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) |
| 145 | 168 |
in |
| 146 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]); |
|
| 169 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]) |
|
| 170 |
|
|
| 171 |
let node_to_lustre basename prog m sw_init sw_step init_out update_out = |
|
| 172 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
|
| 173 |
to_lustre basename prog new_node orig_nd |
|
| 174 |
|
|
| 175 |
let fun_to_lustre basename prog m update_out = |
|
| 176 |
let new_node, orig_nd = funsw_to_lustre m update_out in |
|
| 177 |
to_lustre basename prog new_node orig_nd |
|
| 178 |
|
|
Also available in: Unified diff
printing nodes + more progress on seal export