Revision 782742b6
Added by Pierre-Loïc Garoche about 5 years ago
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 49 | 49 |
Log.report ~level:1 |
| 50 | 50 |
(fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension)); |
| 51 | 51 |
Lusic.write_lusic true header destname lusic_ext; |
| 52 |
Lusic.print_lusic_to_h destname lusic_ext;
|
|
| 52 |
generate_lusic_header destname lusic_ext;
|
|
| 53 | 53 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.") |
| 54 | 54 |
end |
| 55 | 55 |
|
| ... | ... | |
| 59 | 59 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
| 60 | 60 |
let lusic_ext = extension ^ "c" in |
| 61 | 61 |
let header_name = destname ^ lusic_ext in |
| 62 |
begin
|
|
| 62 |
let do_generate_lusic, lusic_opt =
|
|
| 63 | 63 |
if not (Sys.file_exists header_name) then |
| 64 |
begin |
|
| 65 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
|
| 66 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
|
| 67 |
Lusic.print_lusic_to_h destname lusic_ext |
|
| 68 |
end |
|
| 64 |
true, None |
|
| 69 | 65 |
else |
| 70 | 66 |
let lusic = Lusic.read_lusic destname lusic_ext in |
| 71 |
if not lusic.Lusic.from_lusi then |
|
| 72 |
begin |
|
| 73 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
|
| 74 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
|
| 75 |
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*) |
|
| 76 |
Lusic.print_lusic_to_h destname lusic_ext |
|
| 77 |
end |
|
| 78 |
else |
|
| 79 |
begin |
|
| 80 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); |
|
| 81 |
Modules.check_dependency lusic destname; |
|
| 82 |
let header = lusic.Lusic.contents in |
|
| 83 |
let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in |
|
| 84 |
check_compatibility |
|
| 85 |
(prog, computed_types_env, computed_clocks_env) |
|
| 86 |
(header, declared_types_env, declared_clocks_env) |
|
| 87 |
end |
|
| 88 |
end |
|
| 67 |
not lusic.Lusic.from_lusi, Some lusic |
|
| 68 |
in |
|
| 69 |
if do_generate_lusic then |
|
| 70 |
begin |
|
| 71 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
|
| 72 |
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; |
|
| 73 |
generate_lusic_header destname lusic_ext |
|
| 74 |
end |
|
| 75 |
else |
|
| 76 |
begin |
|
| 77 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); |
|
| 78 |
let lusic = desome lusic_opt in |
|
| 79 |
Modules.check_dependency lusic destname; |
|
| 80 |
let header = lusic.Lusic.contents in |
|
| 81 |
let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in |
|
| 82 |
check_compatibility |
|
| 83 |
(prog, computed_types_env, computed_clocks_env) |
|
| 84 |
(header, declared_types_env, declared_clocks_env) |
|
| 85 |
end |
|
| 86 |
|
|
| 87 |
|
|
| 88 |
|
|
| 89 |
(* begin *) |
|
| 90 |
(* if not (Sys.file_exists header_name) then *) |
|
| 91 |
(* begin *) |
|
| 92 |
(* Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *) |
|
| 93 |
(* Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *) |
|
| 94 |
(* Lusic.print_lusic_to_h destname lusic_ext *) |
|
| 95 |
(* end *) |
|
| 96 |
(* else *) |
|
| 97 |
(* let lusic = Lusic.read_lusic destname lusic_ext in *) |
|
| 98 |
(* if not lusic.Lusic.from_lusi then *) |
|
| 99 |
(* begin *) |
|
| 100 |
(* Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *) |
|
| 101 |
(* Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *) |
|
| 102 |
(* (\*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*\) *) |
|
| 103 |
(* Lusic.print_lusic_to_h destname lusic_ext *) |
|
| 104 |
(* end *) |
|
| 105 |
(* else *) |
|
| 106 |
(* begin *) |
|
| 107 |
(* Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); *) |
|
| 108 |
(* Modules.check_dependency lusic destname; *) |
|
| 109 |
(* let header = lusic.Lusic.contents in *) |
|
| 110 |
(* let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in *) |
|
| 111 |
(* check_compatibility *) |
|
| 112 |
(* (prog, computed_types_env, computed_clocks_env) *) |
|
| 113 |
(* (header, declared_types_env, declared_clocks_env) *) |
|
| 114 |
(* end *) |
|
| 115 |
(* end *) |
|
| 89 | 116 |
|
| 90 | 117 |
|
| 91 | 118 |
|
| ... | ... | |
| 215 | 242 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,"); |
| 216 | 243 |
(* Special treatment of arrows in lustre backend. We want to keep them *) |
| 217 | 244 |
if !Options.output = "lustre" then |
| 218 |
Normalization.unfold_arrow_active := false; |
|
| 245 |
Normalization_common.unfold_arrow_active := false;
|
|
| 219 | 246 |
let prog = Normalization.normalize_prog prog in |
| 220 | 247 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
| 221 | 248 |
|
Also available in: Unified diff
Merged unstable with seahorn