source: Deliverables/D4.1/ToMatita.ml @ 1981

Last change on this file since 1981 was 664, checked in by mulligan, 10 years ago

Changed output of Intel HEX files so we no longer have those gargantuan blocks of zeroes at the end.

File size: 773 bytes
Line 
1open BitVectors;;
2open ASMInterpret;;
3open Util;;
4open MatitaPretty;;
5
6let hex = IntelHex.intel_hex_of_file Sys.argv.(1) in
7let mem = IntelHex.process_intel_hex hex in
8let status = ASMInterpret.load_mem mem ASMInterpret.initialize in
9let mem_pretty_print status =
10  let rec aux status pc =
11    let instr, pc', cost = ASMInterpret.fetch status.ASMInterpret.code_memory pc in
12      print_string $ pp_matita_instruction instr;
13      if int_of_vect pc' <= 800 then (* DPM: hardcoded on a case-by-case basis *)
14       begin
15        print_string ";\n  ";
16        aux status pc'
17       end
18  in
19    aux status status.ASMInterpret.pc
20in
21 print_string "include \"ASM.ma\".\n\nndefinition test: List instruction ≝\n [";
22 mem_pretty_print status;
23 print_endline "].\n @.\nnqed."
24;;
Note: See TracBrowser for help on using the repository browser.