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

Last change on this file since 525 was 437, checked in by sacerdot, 10 years ago
  1. new function assembly_unlabelled_program
  2. the new function is now used in DoTest?.ma
File size: 773 bytes
RevLine 
[339]1open BitVectors;;
2open ASMInterpret;;
3open Util;;
4open MatitaPretty;;
5
[429]6let hex = IntelHex.intel_hex_of_file Sys.argv.(1) in
[339]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
[437]12      print_string $ pp_matita_instruction instr;
[339]13      if int_of_vect pc' <= 200 then (* DPM: hardcoded on a case-by-case basis *)
14       begin
[426]15        print_string ";\n  ";
[339]16        aux status pc'
17       end
18  in
19    aux status status.ASMInterpret.pc
20in
[437]21 print_string "include \"ASM.ma\".\n\nndefinition test: List instruction ≝\n [";
[339]22 mem_pretty_print status;
[426]23 print_endline "].\n @.\nnqed."
[339]24;;
Note: See TracBrowser for help on using the repository browser.