Revision c518d082
Added by Xavier Thirioux almost 9 years ago
src/main_lustre_compiler.ml | ||
---|---|---|
28 | 28 |
|
29 | 29 |
let usage = "Usage: lustrec [options] <source-file>" |
30 | 30 |
|
31 |
let extensions = [".ec";".lus"]
|
|
31 |
let extensions = [".ec"; ".lus"; ".lusi"]
|
|
32 | 32 |
|
33 | 33 |
let type_decls env decls = |
34 | 34 |
report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?"); |
... | ... | |
79 | 79 |
|
80 | 80 |
let check_lusi header = |
81 | 81 |
let new_tenv = type_decls Basic_library.type_env header in (* Typing *) |
82 |
let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in (* Clock calculus *)
|
|
82 |
let new_cenv = clock_decls Basic_library.clock_env header in (* Clock calculus *) |
|
83 | 83 |
header, new_tenv, new_cenv |
84 | 84 |
|
85 | 85 |
let rec compile basename extension = |
... | ... | |
192 | 192 |
let lusi_out = open_out lusi_name in |
193 | 193 |
let lusi_fmt = formatter_of_out_channel lusi_out in |
194 | 194 |
Typing.uneval_prog_generics prog; |
195 |
Clock_calculus.uneval_prog_generics prog; |
|
195 | 196 |
Printers.pp_lusi_header lusi_fmt source_name prog |
196 | 197 |
) |
197 | 198 |
| (Types.Error (loc,err)) as exc -> |
198 | 199 |
Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@." |
199 | 200 |
Types.pp_error err; |
200 | 201 |
raise exc |
202 |
| Clocks.Error (loc, err) as exc -> |
|
203 |
Format.eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@]@." |
|
204 |
Clocks.pp_error err; |
|
205 |
raise exc |
|
201 | 206 |
in |
202 | 207 |
|
203 | 208 |
(* Computes and stores generic calls for each node, |
... | ... | |
226 | 231 |
|
227 | 232 |
(* Printing code *) |
228 | 233 |
let basename = Filename.basename basename in |
234 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
229 | 235 |
let _ = match !Options.output with |
230 | 236 |
"C" -> |
231 | 237 |
begin |
232 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
233 | 238 |
let header_file = destname ^ ".h" in (* Could be changed *) |
234 | 239 |
let source_file = destname ^ ".c" in (* Could be changed *) |
235 | 240 |
let makefile_file = destname ^ ".makefile" in (* Could be changed *) |
... | ... | |
268 | 273 |
end |
269 | 274 |
| "horn" -> |
270 | 275 |
begin |
271 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
272 | 276 |
let source_file = destname ^ ".smt2" in (* Could be changed *) |
273 | 277 |
let source_out = open_out source_file in |
274 | 278 |
let fmt = formatter_of_out_channel source_out in |
... | ... | |
286 | 290 |
let basename = Filename.chop_suffix filename ext in |
287 | 291 |
compile basename ext |
288 | 292 |
else |
289 |
raise (Arg.Bad ("Can only compile *.lus or *.ec files")) |
|
293 |
raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
|
|
290 | 294 |
|
291 | 295 |
let _ = |
292 | 296 |
Corelang.add_internal_funs (); |
Also available in: Unified diff
- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files