CristalCaveGem » LustreC

let usage = "Usage: lustrec [options] <source-file>"

let type_decls env decls =  

  report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?");

let check_lusi header =

  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)

  header, new_tenv, new_cenv

let rec compile basename extension =

      let lusi_out = open_out lusi_name in

      let lusi_fmt = formatter_of_out_channel lusi_out in

      Typing.uneval_prog_generics prog;

      Printers.pp_lusi_header lusi_fmt source_name prog

    )

    | (Types.Error (loc,err)) as exc ->

      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."

	Types.pp_error err;

      raise exc

  in

  (* Computes and stores generic calls for each node,

  (* Printing code *)

  let basename    =  Filename.basename basename in

  let _ = match !Options.output with

      "C" -> 

	begin

	  let header_file = destname ^ ".h" in (* Could be changed *)

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

	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)

      end

    | "horn" ->

      begin

	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

    let basename = Filename.chop_suffix filename ext in

    compile basename ext

  else

let _ =

  Corelang.add_internal_funs ();