source: Deliverables/D4.1/MatitaPretty.ml @ 550

Last change on this file since 550 was 339, checked in by sacerdot, 9 years ago

New: pretty printer from HEX files to .ma files.

File size: 4.9 KB
RevLine 
[339]1open BitVectors;;
2open ASM;;
3
4let hex_string_of_vect v =
5 "[[" ^ String.concat ";" (List.map string_of_bool (Obj.magic v)) ^ "]]"
6;;
7
8let pp_arg =
9 function
10    `A -> "ACC_A"
11  | `B -> "ACC_B"
12  | `C -> "CARRY"
13  | `DPTR -> "DPTR"
14  | `ADDR11 x -> "ADDR11 " ^ hex_string_of_vect x
15  | `ADDR16 x -> "ADDR16 " ^ hex_string_of_vect x
16  | `DATA x -> "DATA " ^ hex_string_of_vect x
17  | `DATA16 x -> "DATA16 " ^ hex_string_of_vect x
18  | `BIT x -> "BIT_ADDR " ^ hex_string_of_vect (x: byte)
19  | `NBIT x -> "N_BIT_ADDR " ^ hex_string_of_vect (x: byte)
20  | `REG (r1, r2, r3) -> "REGISTER " ^ hex_string_of_vect (Obj.magic [r1;r2;r3])
21  | `REL x -> "RELATIVE " ^ hex_string_of_vect x
22  | `A_DPTR -> "ACC_DPTR"
23  | `A_PC -> "ACC_PC"
24  | `DIRECT x -> "DIRECT " ^ hex_string_of_vect (x: byte)
25  | `EXT_INDIRECT x -> "EXT_INDIRECT " ^ string_of_bool x
26  | `EXT_IND_DPTR -> "EXT_INDIRECT_DPTR"
27(* DPM: weird: this seems to be reversed in mcu8051ide: change made. *)
28  | `INDIRECT x -> "INDIRECT " ^ string_of_bool x
29  | `IND_DPTR -> "INDIRECT_DPTR"
30  | `Label s -> s
31;;
32
33let pp_arg a = "(" ^ pp_arg a ^ ")";;
34
35let pp_jump =
36 function
37    `CJNE (`U1 (a1,a2),a3) -> "CJNE … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉) " ^ pp_arg a3
38  | `CJNE (`U2 (a1,a2),a3) -> "CJNE … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉) " ^ pp_arg a3
39  | `DJNZ (a1,a2) -> "DJNZ … " ^ pp_arg a1 ^ " " ^ pp_arg a2
40  | `JB (a1,a2) -> "JB … " ^ pp_arg a1 ^ " " ^ pp_arg a2
41  | `JBC (a1,a2) -> "JBC … " ^ pp_arg a1 ^ " " ^ pp_arg a2
42  | `JC a1 -> "JC … " ^ pp_arg a1
43  | `JNB (a1,a2) -> "JNB … " ^ pp_arg a1 ^ " " ^ pp_arg a2
44  | `JNC a1 -> "JNC … " ^ pp_arg a1
45  | `JNZ a1 -> "JNZ … " ^ pp_arg a1
46  | `JZ a1 -> "JZ … " ^ pp_arg a1
47
48let pp_jump j =
49 "Jump … (" ^ pp_jump j ^ ")"
50;;
51
52let pp_matita_instruction =
53 function
54    `Label l -> l ^ ":"
55  | `Cost l -> l ^ ":"
56  | `Jmp j -> "Jump " ^ j
57  | `Call j -> "Call " ^ j
58  | `WithLabel i -> pp_jump i
59  |  (#jump as i) -> pp_jump i
60  | `Mov (a1,a2) -> "MOV … " ^ pp_arg a1 ^ " " ^ a2
61  | `ACALL a1 -> "ACALL … " ^ pp_arg a1
62  | `ADD (a1,a2) -> "ADD … " ^ pp_arg a1 ^ " " ^ pp_arg a2
63  | `ADDC (a1,a2) -> "ADDC … " ^ pp_arg a1 ^ " " ^ pp_arg a2
64  | `AJMP a1 -> "AJMP … " ^ pp_arg a1
65  | `ANL (`U1 (a1,a2)) -> "ANL … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
66  | `ANL (`U2 (a1,a2)) -> "ANL … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
67  | `ANL (`U3 (a1,a2)) -> "ANL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
68  | `CLR a1 -> "CLR … " ^ pp_arg a1
69  | `CPL a1 -> "CPL … " ^ pp_arg a1
70  | `DA a1 -> "DA … " ^ pp_arg a1
71  | `DEC a1 -> "DEC … " ^ pp_arg a1
72  | `DIV (a1,a2) -> "DIV … " ^ pp_arg a1 ^ " " ^ pp_arg a2
73  | `INC a1 -> "INC … " ^ pp_arg a1
74  | `JMP a1 -> "JMP … " ^ pp_arg a1
75  | `LCALL a1 -> "LCALL … " ^ pp_arg a1
76  | `LJMP a1 -> "LJMP … " ^ pp_arg a1
77  | `MOV (`U1 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))))"
78  | `MOV (`U2 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))))"
79  | `MOV (`U3 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))))"
80  | `MOV (`U4 (a1,a2)) -> "MOV … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))"
81  | `MOV (`U5 (a1,a2)) -> "MOV … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
82  | `MOV (`U6 (a1,a2)) -> "MOV … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
83  | `MOVC (a1,a2) -> "MOVC … " ^ pp_arg a1 ^ " " ^ pp_arg a2
84  | `MOVX (`U1 (a1,a2)) -> "MOVX … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
85  | `MOVX (`U2 (a1,a2)) -> "MOVX … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
86  | `MUL(a1, a2) -> "MUL … " ^ pp_arg a1 ^ " " ^ pp_arg a2
87  | `NOP -> "NOP … "
88  | `ORL (`U1 (a1,a2)) -> "ORL … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
89  | `ORL (`U2 (a1,a2)) -> "ORL … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
90  | `ORL (`U3 (a1,a2)) -> "ORL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
91  | `POP a1 -> "POP … " ^ pp_arg a1
92  | `PUSH a1 -> "PUSH … " ^ pp_arg a1
93  | `RET -> "RET … "
94  | `RETI -> "RETI … "
95  | `RL a1 -> "RL … " ^ pp_arg a1
96  | `RLC a1 -> "RLC … " ^ pp_arg a1
97  | `RR a1 -> "RR … " ^ pp_arg a1
98  | `RRC a1 -> "RRC … " ^ pp_arg a1
99  | `SETB a1 -> "SETB … " ^ pp_arg a1
100  | `SJMP a1 -> "SJMP … " ^ pp_arg a1
101  | `SUBB (a1,a2) -> "SUBB … " ^ pp_arg a1 ^ " " ^ pp_arg a2
102  | `SWAP a1 -> "SWAP … " ^ pp_arg a1
103  | `XCH (a1,a2) -> "XCH … " ^ pp_arg a1 ^ " " ^ pp_arg a2
104  | `XCHD(a1,a2) -> "XCHD … " ^ pp_arg a1 ^ " " ^ pp_arg a2
105  | `XRL (`U1 (a1,a2)) -> "XRL … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
106  | `XRL (`U2 (a1,a2)) -> "XRL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
Note: See TracBrowser for help on using the repository browser.