Revision d50b0dc0
Added by Teme Kahsai about 9 years ago
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 70 | 70 |
begin |
| 71 | 71 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
| 72 | 72 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
| 73 |
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*) |
|
| 73 |
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
|
|
| 74 | 74 |
Lusic.print_lusic_to_h destname lusic_ext |
| 75 | 75 |
end |
| 76 | 76 |
else |
| ... | ... | |
| 85 | 85 |
end |
| 86 | 86 |
end |
| 87 | 87 |
|
| 88 |
|
|
| 89 |
|
|
| 88 | 90 |
(* compile a .lus source file *) |
| 89 | 91 |
let rec compile_source dirname basename extension = |
| 90 | 92 |
|
| ... | ... | |
| 155 | 157 |
|
| 156 | 158 |
(* Compatibility with Lusi *) |
| 157 | 159 |
(* Checking the existence of a lusi (Lustre Interface file) *) |
| 158 |
match !Options.output with |
|
| 160 |
(match !Options.output with
|
|
| 159 | 161 |
"C" -> |
| 160 | 162 |
begin |
| 161 | 163 |
let extension = ".lusi" in |
| 162 | 164 |
compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension; |
| 163 | 165 |
end |
| 164 |
|_ -> (); |
|
| 166 |
|_ -> ());
|
|
| 165 | 167 |
|
| 166 | 168 |
Typing.uneval_prog_generics prog; |
| 167 | 169 |
Clock_calculus.uneval_prog_generics prog; |
| ... | ... | |
| 299 | 301 |
let source_file = destname ^ ".smt2" in (* Could be changed *) |
| 300 | 302 |
let source_out = open_out source_file in |
| 301 | 303 |
let fmt = formatter_of_out_channel source_out in |
| 302 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@.. hornification@,");
|
|
| 303 |
Horn_backend.translate fmt basename prog machine_code;
|
|
| 304 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
|
|
| 305 |
Horn_backend.translate fmt basename prog machine_code;
|
|
| 304 | 306 |
(* Tracability file if option is activated *) |
| 305 | 307 |
if !Options.traces then ( |
| 306 |
let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
|
|
| 307 |
let traces_out = open_out traces_file in
|
|
| 308 |
let fmt = formatter_of_out_channel traces_out in
|
|
| 309 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@.. tracing info@,");
|
|
| 310 |
Horn_backend.traces_file fmt basename prog machine_code;
|
|
| 308 |
let traces_file = destname ^ ".traces.xml" in (* Could be changed *) |
|
| 309 |
let traces_out = open_out traces_file in |
|
| 310 |
let fmt = formatter_of_out_channel traces_out in |
|
| 311 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
|
|
| 312 |
Horn_backend.traces_file fmt basename prog machine_code; |
|
| 311 | 313 |
) |
| 312 | 314 |
end |
| 313 | 315 |
| "lustre" -> |
| ... | ... | |
| 323 | 325 |
| _ -> assert false |
| 324 | 326 |
in |
| 325 | 327 |
begin |
| 326 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@.. done @ @]@.");
|
|
| 328 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@."); |
|
| 327 | 329 |
(* We stop the process here *) |
| 328 | 330 |
exit 0 |
| 329 | 331 |
end |
Also available in: Unified diff
sync