open Extracted.Errors
open ClightPrinter

let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)

let string_of_intensional_event =
 function
    Extracted.StructuredTraces.IEVcost cl ->
     "COST(k_" ^ string_of_pos cl ^") "
  | Extracted.StructuredTraces.IEVcall id ->
     "CALL(fun_" ^ string_of_pos id ^ ") "
  | Extracted.StructuredTraces.IEVtailcall _ -> assert false
  | Extracted.StructuredTraces.IEVret id ->
     "RET(fun_" ^ string_of_pos id ^ ") "
;;

let string_of_pass =
 function
 | Extracted.Compiler.Clight_pass                -> "Clight_pass               "
 | Extracted.Compiler.Clight_switch_removed_pass -> "Clight_switch_removed_pass"
 | Extracted.Compiler.Clight_label_pass          -> "Clight_label_pass         "
 | Extracted.Compiler.Clight_simplified_pass     -> "Clight_simplified_pass    "
 | Extracted.Compiler.Cminor_pass                -> "Cminor_pass               "
 | Extracted.Compiler.Rtlabs_pass                -> "Rtlabs_pass               "
 | Extracted.Compiler.Rtl_separate_pass          -> "Rtl_separate_pass         "
 | Extracted.Compiler.Rtl_uniq_pass              -> "Rtl_uniq_pass             "
 | Extracted.Compiler.Ertl_pass                  -> "Ertl_pass                 "
 | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass                  "
 | Extracted.Compiler.Lin_pass                   -> "Lin_pass                  "
 | Extracted.Compiler.Assembly_pass              -> "Assembly_pass             "
 | Extracted.Compiler.Object_code_pass           -> "Object_code_pass          "
;;

List.iter (fun filename ->
let do_exec = Options.interpretations_requested () in
let cl = ClightParser.process filename in
let observe =
 let rec infinity = Extracted.Nat.S infinity in
 (fun pass prog ->
   if do_exec || pass = Extracted.Compiler.Object_code_pass then
    Printer.print_program filename pass prog;
   if do_exec then
    Extracted.Semantics.run_and_print pass prog infinity
     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
       Extracted.Types.It)
     (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
       Extracted.Types.It)
     (fun msg -> print_endline (Error.errormsg msg); flush stdout;
       Extracted.Types.It)
     (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
       flush stdout; Extracted.Types.It)
   else
    Extracted.Types.It)
in
let output = 
  match Extracted.Compiler.compile observe cl with
  | OK o -> o
  | Error m -> failwith (Error.errormsg m) in
if Options.annotation_requested () then
 begin
  let labelled = output.Extracted.Compiler.c_labelled_clight in
  let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
  let init_costlabel = output.Extracted.Compiler.c_init_costlabel in
  let s_costmap = output.Extracted.Compiler.c_stack_cost in
  let maxstack = output.Extracted.Compiler.c_max_stack in
  let style = Cost_instrumented (l_costmap,init_costlabel,s_costmap,maxstack) in
  let instrumented = ClightPrinter.print_program style labelled in
  let basename =
   (match Options.get_output_files () with
      None -> Filename.chop_extension filename
    | Some s -> s) in
  let och = open_out (basename ^ "-instrumented.c") in
  output_string och instrumented;
  close_out och;
  let och = open_out (basename ^ ".cerco") in
  output_string och "__cost\n";
  output_string och "__cost_incr\n";
  close_out och;
  let och = open_out (basename ^ ".stack_cerco") in
  output_string och "__stack_size\n";
  output_string och "__stack_size_max\n";
  output_string och "__stack_size_incr\n";
  close_out och
 end
) (OptionsParsing.results ())