Project

General

Profile

Revision dc893173 src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
324 324
(* printing code *)
325 325
let stage3 prog machine_code dependencies basename =
326 326
  let basename    =  Filename.basename basename in
327
  let destname = !Options.dest_dir ^ "/" ^ basename in
328 327
  match !Options.output with
329
      "C" -> 
330
	begin
331
	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
332
	  let source_lib_file = destname ^ ".c" in (* Could be changed *)
333
	  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
334
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
335
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
336
	  C_backend.translate_to_c
337
	    alloc_header_file source_lib_file source_main_file makefile_file
338
	    basename prog machine_code dependencies
339
	end
340
    | "java" ->
341
      begin
342
	(Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
343
    (*let source_file = basename ^ ".java" in
344
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
345
      let source_out = open_out source_file in
346
      let source_fmt = formatter_of_out_channel source_out in
347
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
348
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
349
      end
350
    | "horn" ->
351
      begin
352
	let source_file = destname ^ ".smt2" in (* Could be changed *)
353
	let source_out = open_out source_file in
354
	let fmt = formatter_of_out_channel source_out in
355
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
356
        Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
357
	(* Tracability file if option is activated *)
358
	if !Options.traces then (
359
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
360
	let traces_out = open_out traces_file in
361
	let fmt = formatter_of_out_channel traces_out in
362
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
363
	Horn_backend_traces.traces_file fmt basename prog machine_code;
364
	)
365
      end
366
    | "lustre" ->
328
    "C" -> 
367 329
      begin
368
	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
369
	let source_out = open_out source_file in
370
	let fmt = formatter_of_out_channel source_out in
371
	Printers.pp_prog fmt prog;
372
(*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
373
	()
330
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
331
	C_backend.translate_to_c
332
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
333
	  basename prog machine_code dependencies
374 334
      end
375

  
376
    | _ -> assert false
335
  | "java" ->
336
     begin
337
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
338
     (*let source_file = basename ^ ".java" in
339
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
340
       let source_out = open_out source_file in
341
       let source_fmt = formatter_of_out_channel source_out in
342
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
343
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
344
     end
345
  | "horn" ->
346
     begin
347
       let destname = !Options.dest_dir ^ "/" ^ basename in
348
       let source_file = destname ^ ".smt2" in (* Could be changed *)
349
       let source_out = open_out source_file in
350
       let fmt = formatter_of_out_channel source_out in
351
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
352
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
353
       (* Tracability file if option is activated *)
354
       if !Options.traces then (
355
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
356
	 let traces_out = open_out traces_file in
357
	 let fmt = formatter_of_out_channel traces_out in
358
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
359
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
360
       )
361
     end
362
  | "lustre" ->
363
     begin
364
       let destname = !Options.dest_dir ^ "/" ^ basename in
365
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
366
       let source_out = open_out source_file in
367
       let fmt = formatter_of_out_channel source_out in
368
       Printers.pp_prog fmt prog;
369
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
370
       ()
371
     end
372

  
373
  | _ -> assert false
377 374

  
378 375
(* compile a .lus source file *)
379 376
let rec compile_source dirname basename extension =

Also available in: Unified diff