CristalCaveGem » LustreC

	begin

	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);

       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;

	  Lusic.print_lusic_to_h destname lusic_ext

	end

      else

	end

  end

(* compile a .lus source file *)

let rec compile_source dirname basename extension =

  (* Compatibility with Lusi *)

  (* Checking the existence of a lusi (Lustre Interface file) *)

    "C" ->

      begin

        let extension = ".lusi" in

        compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;

      end

  Typing.uneval_prog_generics prog;

  Clock_calculus.uneval_prog_generics prog;

	let source_file = destname ^ ".smt2" in (* Could be changed *)

	let source_out = open_out source_file in

	let fmt = formatter_of_out_channel source_out in

	(* Tracability file if option is activated *)

	if !Options.traces then (

	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)

	let traces_out = open_out traces_file in

	let fmt = formatter_of_out_channel traces_out in

	Horn_backend.traces_file fmt basename prog machine_code;

	)

      end

    | _ -> assert false

  in

  begin

  (* We stop the process here *)

    exit 0

  end