open BitVectors;;
open ASMInterpret;;
open Util;;
open MatitaPretty;;

let hex = IntelHex.intel_hex_of_file Sys.argv.(1) in
let mem = IntelHex.process_intel_hex hex in
let status = ASMInterpret.load_mem mem ASMInterpret.initialize in
let mem_pretty_print status =
  let rec aux status pc =
    let instr, pc', cost = ASMInterpret.fetch status.ASMInterpret.code_memory pc in
      print_string $ pp_matita_instruction instr;
      if int_of_vect pc' <= 200 then (* DPM: hardcoded on a case-by-case basis *)
       begin
        print_string ";\n  ";
        aux status pc'
       end
  in
    aux status status.ASMInterpret.pc
in
 print_string "include \"ASM.ma\".\n\nndefinition test: List instruction ≝\n [";
 mem_pretty_print status;
 print_endline "].\n @.\nnqed."
;;