Project

General

Profile

Revision f6923c9e src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
216 216

  
217 217
  (* Printing code *)
218 218
  let basename    = Filename.basename basename in
219
  if !Options.java then
220
    failwith "Sorry, but not yet supported !"
219
  let _ = match !Options.output with
220
      "C" -> 
221
	begin
222
	  let header_file = basename ^ ".h" in (* Could be changed *)
223
	  let source_file = basename ^ ".c" in (* Could be changed *)
224
	  let makefile_file = basename ^ ".makefile" in (* Could be changed *)
225
	  let spec_file_opt = if !Options.c_spec then 
226
	      (
227
		let spec_file = basename ^ "_spec.c" in
228
		report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@,@?" header_file source_file spec_file);
229
		Some spec_file 
230
	      ) else (
231
		report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@,@?" header_file source_file);
232
		None 
233
	       )
234
	  in 
235
	  let header_out = open_out header_file in
236
	  let header_fmt = formatter_of_out_channel header_out in
237
	  let source_out = open_out source_file in
238
	  let source_fmt = formatter_of_out_channel source_out in
239
	  let makefile_out = open_out makefile_file in
240
	  let makefile_fmt = formatter_of_out_channel makefile_out in
241
	  let spec_fmt_opt = match spec_file_opt with
242
	      None -> None
243
	    | Some f -> Some (formatter_of_out_channel (open_out f))
244
	  in
245
	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");
246
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;
247
	end
248
    | "java" -> begin
249
      failwith "Sorry, but not yet supported !"
221 250
    (*let source_file = basename ^ ".java" in
222 251
      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
223 252
      let source_out = open_out source_file in
224 253
      let source_fmt = formatter_of_out_channel source_out in
225 254
      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
226 255
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
227
  else begin
228
    let header_file = basename ^ ".h" in (* Could be changed *)
229
    let source_file = basename ^ ".c" in (* Could be changed *)
230
    let makefile_file = basename ^ ".makefile" in (* Could be changed *)
231
    let spec_file_opt = if !Options.c_spec then 
232
	(
233
	  let spec_file = basename ^ "_spec.c" in
234
	  report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@,@?" header_file source_file spec_file);
235
	  Some spec_file 
236
	) else (
237
	  report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@,@?" header_file source_file);
238
	  None 
239
	 )
240
    in 
241
    let header_out = open_out header_file in
242
    let header_fmt = formatter_of_out_channel header_out in
243
    let source_out = open_out source_file in
244
    let source_fmt = formatter_of_out_channel source_out in
245
    let makefile_out = open_out makefile_file in
246
    let makefile_fmt = formatter_of_out_channel makefile_out in
247
    let spec_fmt_opt = match spec_file_opt with
248
	None -> None
249
      | Some f -> Some (formatter_of_out_channel (open_out f))
250
    in
251
    report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");
252
    C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;
253
  end;
256
    end
257
    | "horn" -> begin
258
      let fmt = Format.std_formatter in
259
      Horn_backend.translate fmt basename normalized_prog machine_code
260
    end
261
  in
254 262
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
255 263
  (* We stop the process here *)
256 264
  exit 0

Also available in: Unified diff