Project

General

Profile

Revision d50b0dc0 src/main_lustre_compiler.ml

View differences:

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