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

open BitVectors;;
open ASM;;

let hex_string_of_vect v =
 "[[" ^ String.concat ";" (List.map string_of_bool (Obj.magic v)) ^ "]]"
;;

let pp_arg =
 function
    `A -> "ACC_A"
  | `B -> "ACC_B"
  | `C -> "CARRY"
  | `DPTR -> "DPTR"
  | `ADDR11 x -> "ADDR11 " ^ hex_string_of_vect x
  | `ADDR16 x -> "ADDR16 " ^ hex_string_of_vect x
  | `DATA x -> "DATA " ^ hex_string_of_vect x
  | `DATA16 x -> "DATA16 " ^ hex_string_of_vect x
  | `BIT x -> "BIT_ADDR " ^ hex_string_of_vect (x: byte)
  | `NBIT x -> "N_BIT_ADDR " ^ hex_string_of_vect (x: byte)
  | `REG (r1, r2, r3) -> "REGISTER " ^ hex_string_of_vect (Obj.magic [r1;r2;r3])
  | `REL x -> "RELATIVE " ^ hex_string_of_vect x
  | `A_DPTR -> "ACC_DPTR"
  | `A_PC -> "ACC_PC"
  | `DIRECT x -> "DIRECT " ^ hex_string_of_vect (x: byte)
  | `EXT_INDIRECT x -> "EXT_INDIRECT " ^ string_of_bool x
  | `EXT_IND_DPTR -> "EXT_INDIRECT_DPTR"
(* DPM: weird: this seems to be reversed in mcu8051ide: change made. *)
  | `INDIRECT x -> "INDIRECT " ^ string_of_bool x
  | `IND_DPTR -> "INDIRECT_DPTR"
  | `Label s -> s
;;

let pp_arg a = "(" ^ pp_arg a ^ ")";;

let pp_jump =
 function
    `CJNE (`U1 (a1,a2),a3) -> "CJNE … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉) " ^ pp_arg a3
  | `CJNE (`U2 (a1,a2),a3) -> "CJNE … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉) " ^ pp_arg a3
  | `DJNZ (a1,a2) -> "DJNZ … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `JB (a1,a2) -> "JB … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `JBC (a1,a2) -> "JBC … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `JC a1 -> "JC … " ^ pp_arg a1
  | `JNB (a1,a2) -> "JNB … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `JNC a1 -> "JNC … " ^ pp_arg a1
  | `JNZ a1 -> "JNZ … " ^ pp_arg a1
  | `JZ a1 -> "JZ … " ^ pp_arg a1

let pp_jump j =
 "Jump … (" ^ pp_jump j ^ ")"
;;

let pp_matita_instruction =
 function
    `Label l -> l ^ ":"
  | `Cost l -> l ^ ":"
  | `Jmp j -> "Jump " ^ j
  | `Call j -> "Call " ^ j
  | `WithLabel i -> pp_jump i
  |  (#jump as i) -> pp_jump i
  | `Mov (a1,a2) -> "MOV … " ^ pp_arg a1 ^ " " ^ a2
  | `ACALL a1 -> "ACALL … " ^ pp_arg a1
  | `ADD (a1,a2) -> "ADD … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `ADDC (a1,a2) -> "ADDC … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `AJMP a1 -> "AJMP … " ^ pp_arg a1
  | `ANL (`U1 (a1,a2)) -> "ANL … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
  | `ANL (`U2 (a1,a2)) -> "ANL … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
  | `ANL (`U3 (a1,a2)) -> "ANL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
  | `CLR a1 -> "CLR … " ^ pp_arg a1
  | `CPL a1 -> "CPL … " ^ pp_arg a1
  | `DA a1 -> "DA … " ^ pp_arg a1
  | `DEC a1 -> "DEC … " ^ pp_arg a1
  | `DIV (a1,a2) -> "DIV … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `INC a1 -> "INC … " ^ pp_arg a1
  | `JMP a1 -> "JMP … " ^ pp_arg a1
  | `LCALL a1 -> "LCALL … " ^ pp_arg a1
  | `LJMP a1 -> "LJMP … " ^ pp_arg a1
  | `MOV (`U1 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))))"
  | `MOV (`U2 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))))"
  | `MOV (`U3 (a1,a2)) -> "MOV … (Left … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))))"
  | `MOV (`U4 (a1,a2)) -> "MOV … (Left … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)))"
  | `MOV (`U5 (a1,a2)) -> "MOV … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
  | `MOV (`U6 (a1,a2)) -> "MOV … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
  | `MOVC (a1,a2) -> "MOVC … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `MOVX (`U1 (a1,a2)) -> "MOVX … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
  | `MOVX (`U2 (a1,a2)) -> "MOVX … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
  | `MUL(a1, a2) -> "MUL … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `NOP -> "NOP … "
  | `ORL (`U1 (a1,a2)) -> "ORL … (Left … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
  | `ORL (`U2 (a1,a2)) -> "ORL … (Left … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉))"
  | `ORL (`U3 (a1,a2)) -> "ORL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
  | `POP a1 -> "POP … " ^ pp_arg a1
  | `PUSH a1 -> "PUSH … " ^ pp_arg a1
  | `RET -> "RET … "
  | `RETI -> "RETI … "
  | `RL a1 -> "RL … " ^ pp_arg a1
  | `RLC a1 -> "RLC … " ^ pp_arg a1
  | `RR a1 -> "RR … " ^ pp_arg a1
  | `RRC a1 -> "RRC … " ^ pp_arg a1
  | `SETB a1 -> "SETB … " ^ pp_arg a1
  | `SJMP a1 -> "SJMP … " ^ pp_arg a1
  | `SUBB (a1,a2) -> "SUBB … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `SWAP a1 -> "SWAP … " ^ pp_arg a1
  | `XCH (a1,a2) -> "XCH … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `XCHD(a1,a2) -> "XCHD … " ^ pp_arg a1 ^ " " ^ pp_arg a2
  | `XRL (`U1 (a1,a2)) -> "XRL … (Left … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"
  | `XRL (`U2 (a1,a2)) -> "XRL … (Right … 〈" ^ pp_arg a1 ^ "," ^ pp_arg a2 ^ "〉)"