type cost_id =
  {
    cost_id : string;
    cost_incr : string;
    extern_costs : string Misc.String.Map.t;
  }
(** This file makes the interface between the cost plug-in and CerCo's
    compiler. *)


let rec read_extern_cost_variables cin =
  try
    let s = input_line cin in
    assert (String.contains s ' ') ;
    let i = String.index s ' ' in
    assert (String.length s > i + 1) ;
    let fun_name = String.sub s 0 i in
    let var_name = String.sub s (i+1) (String.length s - (i+1)) in
    Misc.String.Map.add fun_name var_name (read_extern_cost_variables cin)
  with End_of_file -> Misc.String.Map.empty

(** [multifile_exists exts filename] returns true if and only if the file name
    [filename] concatenated with an extension from the list [exts] exists. *)

let multifile_exists exts filename =
  let f b ext = b || (Sys.file_exists (filename ^ ext)) in
  List.fold_left f false exts

(** [fresh_multifile exts filename] returns a file name whose base is [filename]
    and suffixed with an integer such that the result is fresh when concatenated
    with any extension from the list [exts]. *)

let fresh_multifile exts filename =
  if not (multifile_exists exts filename) then filename
  else
    let rec aux i =
      let new_filename = filename ^ (string_of_int i) in
      if not (multifile_exists exts new_filename) then new_filename
      else aux (i+1) in
    aux 0

(** [index_of e l] returns the index of the element [e] in the list [l], if
    any. *)

let index_of e l =
  let f (i, res) e' =
    let res' = if e' = e then Some i else res in
    (i+1, res') in
  match snd (List.fold_left f (0, None) l) with
    | None -> raise (Failure "Cerco.index_of")
    | Some i -> i

let acc_option lustre_option lustre_verify_option lustre_test_option =
  if lustre_verify_option || lustre_test_option then "-remove-lustre-externals "
  else
    if lustre_option then "-lustre "
    else ""

(** [apply (filename, _)] apply CerCo's compiler on the file [filename]. The
    result is a new C file with cost annotations, the name of the cost
    variable, and the name of the cost update function. *)

let apply acc_name lustre_option lustre_verify_option lustre_test_option
    user_output_filename
    (filename, _) =
  let annotated_ext = "-instrumented.c" in
  let asm_ext = ".s" in
  let cerco_ext = ".cerco" in
  let cerco_stack_ext = ".stack_cerco" in
  let hex_ext = ".hex" in
  let exts =
    [annotated_ext ; asm_ext ; cerco_ext ; cerco_stack_ext ; hex_ext] in
  let tmp_filename =
    if user_output_filename <> "" then user_output_filename else
      let tmp_filename = Filename.chop_extension filename in
      fresh_multifile exts tmp_filename in
  let acc_option =
    acc_option lustre_option lustre_verify_option lustre_test_option in
  let com_acc =
    Printf.sprintf "%s -a %s -o %s %s"
      acc_name acc_option tmp_filename filename in
  let ext_tmp_filename ext = tmp_filename ^ ext in
  let tmp_filenames = List.map ext_tmp_filename exts in
  let index_of s = List.nth tmp_filenames (index_of s exts) in
  let c_tmp_filename = index_of annotated_ext in
  let s_tmp_filename = index_of asm_ext in
  let cerco_tmp_filename = index_of cerco_ext in
  let cerco_stack_tmp_filename = index_of cerco_stack_ext in
  (* let hex_tmp_filename = index_of hex_ext in *)
  let rm () =
    let com =
      "rm -rf " ^ s_tmp_filename ^ " " ^
	(if lustre_test_option then "" else cerco_tmp_filename)
    (* ^ " " ^ hex_tmp_filename *) in
    ignore (Sys.command com) in
  if Sys.command com_acc <> 0 then
    (rm () ; failwith "Error calling acc.")
  else
    (let (_, file) = Frontc.parse c_tmp_filename () in
     let time =
       let cin = open_in cerco_tmp_filename in
       let cost_id = input_line cin in
       let cost_incr = input_line cin in
       let extern_cost_variables = read_extern_cost_variables cin in
       close_in cin ;
      {cost_id = cost_id; cost_incr = cost_incr;
       extern_costs = extern_cost_variables} in
     let stack =
       try
         let cin = try open_in cerco_stack_tmp_filename with _ -> raise Exit in
         let cost_stack_id = input_line cin in
         let cost_stack_max_id = input_line cin in
         let cost_stack_incr = input_line cin in
         let extern_cost_stack_variables = read_extern_cost_variables cin in
         close_in cin ;
         Some ({cost_id = cost_stack_max_id; cost_incr = cost_stack_incr;
                extern_costs = extern_cost_stack_variables},
               cost_stack_id)
       with Exit -> None in
     rm () ;
     (file, c_tmp_filename, time, stack))