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

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

1) README upated
2) executable now reads the name of the HEX file from argv

File size: 784 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' <= 200 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 labelled_instruction ≝\n [";
22 mem_pretty_print status;
23 print_endline "].\n @.\nnqed."
24;;
Note: See TracBrowser for help on using the repository browser.