matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml

   1 let opcode_table =
   2 (function m ->
   3 (match m with
   4    Matita_freescale_opcode.HC05 -> Obj.magic (Matita_freescale_table_HC05.opcode_table_HC05)
   5  | Matita_freescale_opcode.HC08 -> Obj.magic (Matita_freescale_table_HC08.opcode_table_HC08)
   6  | Matita_freescale_opcode.HCS08 -> Obj.magic (Matita_freescale_table_HCS08.opcode_table_HCS08)
   7  | Matita_freescale_opcode.RS08 -> Obj.magic (Matita_freescale_table_RS08.opcode_table_RS08))
   8 )
   9 ;;
  10
  11 let full_info_of_word16 =
  12 (function m -> (function borw -> (let rec aux =
  13 (function param ->
  14 (match param with
  15    Matita_list_list.Nil -> (Matita_datatypes_constructors.None)
  16  | Matita_list_list.Cons(hd,tl) ->
  17 (match (Matita_freescale_extra.thd4T hd) with
  18    Matita_freescale_opcode.Byte(b) ->
  19 (match borw with
  20    Matita_freescale_opcode.Byte(borw') ->
  21 (match (Matita_freescale_byte8.eq_b8 borw' b) with
  22    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(hd))
  23  | Matita_datatypes_bool.False -> (aux tl))
  24
  25  | Matita_freescale_opcode.Word(_) -> (aux tl))
  26
  27  | Matita_freescale_opcode.Word(w) ->
  28 (match borw with
  29    Matita_freescale_opcode.Byte(_) -> (aux tl)
  30  | Matita_freescale_opcode.Word(borw') ->
  31 (match (Matita_freescale_word16.eq_w16 borw' w) with
  32    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(hd))
  33  | Matita_datatypes_bool.False -> (aux tl))
  34 )
  35 )
  36 )
  37 ) in aux (opcode_table m))))
  38 ;;
  39
  40 type t_byte8 =
  41 TByte of Matita_freescale_byte8.byte8
  42 ;;
  43
  44 let t_byte8_rec =
  45 (function m -> (function f -> (function t ->
  46 (match t with
  47    TByte(b) -> (f b))
  48 )))
  49 ;;
  50
  51 let t_byte8_rect =
  52 (function m -> (function f -> (function t ->
  53 (match t with
  54    TByte(b) -> (f b))
  55 )))
  56 ;;
  57
  58 let t_byte8_OF_bitrigesim =
  59 (function a -> (function m -> (TByte((Matita_freescale_aux_bases.byte8_of_bitrigesim a)))))
  60 ;;
  61
  62 type mA_check =
  63 MaINH
  64  | MaINHA
  65  | MaINHX
  66  | MaINHH
  67  | MaINHX0ADD
  68  | MaINHX1ADD of Matita_freescale_byte8.byte8
  69  | MaINHX2ADD of Matita_freescale_word16.word16
  70  | MaIMM1 of Matita_freescale_byte8.byte8
  71  | MaIMM1EXT of Matita_freescale_byte8.byte8
  72  | MaIMM2 of Matita_freescale_word16.word16
  73  | MaDIR1 of Matita_freescale_byte8.byte8
  74  | MaDIR2 of Matita_freescale_word16.word16
  75  | MaIX0
  76  | MaIX1 of Matita_freescale_byte8.byte8
  77  | MaIX2 of Matita_freescale_word16.word16
  78  | MaSP1 of Matita_freescale_byte8.byte8
  79  | MaSP2 of Matita_freescale_word16.word16
  80  | MaDIR1_to_DIR1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  81  | MaIMM1_to_DIR1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  82  | MaIX0p_to_DIR1 of Matita_freescale_byte8.byte8
  83  | MaDIR1_to_IX0p of Matita_freescale_byte8.byte8
  84  | MaINHA_and_IMM1 of Matita_freescale_byte8.byte8
  85  | MaINHX_and_IMM1 of Matita_freescale_byte8.byte8
  86  | MaIMM1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  87  | MaDIR1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  88  | MaIX0_and_IMM1 of Matita_freescale_byte8.byte8
  89  | MaIX0p_and_IMM1 of Matita_freescale_byte8.byte8
  90  | MaIX1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  91  | MaIX1p_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  92  | MaSP1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  93  | MaDIRn of Matita_freescale_aux_bases.oct * Matita_freescale_byte8.byte8
  94  | MaDIRn_and_IMM1 of Matita_freescale_aux_bases.oct * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
  95  | MaTNY of Matita_freescale_exadecim.exadecim
  96  | MaSRT of Matita_freescale_aux_bases.bitrigesim
  97 ;;
  98
  99 let mA_check_rec =
 100 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function f -> (function f1 -> (function f2 -> (function f3 -> (function f4 -> (function f5 -> (function f6 -> (function p5 -> (function f7 -> (function f8 -> (function f9 -> (function f10 -> (function f11 -> (function f12 -> (function f13 -> (function f14 -> (function f15 -> (function f16 -> (function f17 -> (function f18 -> (function f19 -> (function f20 -> (function f21 -> (function f22 -> (function f23 -> (function f24 -> (function f25 -> (function f26 -> (function f27 -> (function i -> (function m ->
 101 (match m with
 102    MaINH -> p
 103  | MaINHA -> p1
 104  | MaINHX -> p2
 105  | MaINHH -> p3
 106  | MaINHX0ADD -> p4
 107  | MaINHX1ADD(b) -> (f b)
 108  | MaINHX2ADD(w) -> (f1 w)
 109  | MaIMM1(b) -> (f2 b)
 110  | MaIMM1EXT(b) -> (f3 b)
 111  | MaIMM2(w) -> (f4 w)
 112  | MaDIR1(b) -> (f5 b)
 113  | MaDIR2(w) -> (f6 w)
 114  | MaIX0 -> p5
 115  | MaIX1(b) -> (f7 b)
 116  | MaIX2(w) -> (f8 w)
 117  | MaSP1(b) -> (f9 b)
 118  | MaSP2(w) -> (f10 w)
 119  | MaDIR1_to_DIR1(b,b1) -> (f11 b b1)
 120  | MaIMM1_to_DIR1(b,b1) -> (f12 b b1)
 121  | MaIX0p_to_DIR1(b) -> (f13 b)
 122  | MaDIR1_to_IX0p(b) -> (f14 b)
 123  | MaINHA_and_IMM1(b) -> (f15 b)
 124  | MaINHX_and_IMM1(b) -> (f16 b)
 125  | MaIMM1_and_IMM1(b,b1) -> (f17 b b1)
 126  | MaDIR1_and_IMM1(b,b1) -> (f18 b b1)
 127  | MaIX0_and_IMM1(b) -> (f19 b)
 128  | MaIX0p_and_IMM1(b) -> (f20 b)
 129  | MaIX1_and_IMM1(b,b1) -> (f21 b b1)
 130  | MaIX1p_and_IMM1(b,b1) -> (f22 b b1)
 131  | MaSP1_and_IMM1(b,b1) -> (f23 b b1)
 132  | MaDIRn(o,b) -> (f24 o b)
 133  | MaDIRn_and_IMM1(o,b,b1) -> (f25 o b b1)
 134  | MaTNY(e) -> (f26 e)
 135  | MaSRT(b) -> (f27 b))
 136 ))))))))))))))))))))))))))))))))))))
 137 ;;
 138
 139 let mA_check_rect =
 140 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function f -> (function f1 -> (function f2 -> (function f3 -> (function f4 -> (function f5 -> (function f6 -> (function p5 -> (function f7 -> (function f8 -> (function f9 -> (function f10 -> (function f11 -> (function f12 -> (function f13 -> (function f14 -> (function f15 -> (function f16 -> (function f17 -> (function f18 -> (function f19 -> (function f20 -> (function f21 -> (function f22 -> (function f23 -> (function f24 -> (function f25 -> (function f26 -> (function f27 -> (function i -> (function m ->
 141 (match m with
 142    MaINH -> p
 143  | MaINHA -> p1
 144  | MaINHX -> p2
 145  | MaINHH -> p3
 146  | MaINHX0ADD -> p4
 147  | MaINHX1ADD(b) -> (f b)
 148  | MaINHX2ADD(w) -> (f1 w)
 149  | MaIMM1(b) -> (f2 b)
 150  | MaIMM1EXT(b) -> (f3 b)
 151  | MaIMM2(w) -> (f4 w)
 152  | MaDIR1(b) -> (f5 b)
 153  | MaDIR2(w) -> (f6 w)
 154  | MaIX0 -> p5
 155  | MaIX1(b) -> (f7 b)
 156  | MaIX2(w) -> (f8 w)
 157  | MaSP1(b) -> (f9 b)
 158  | MaSP2(w) -> (f10 w)
 159  | MaDIR1_to_DIR1(b,b1) -> (f11 b b1)
 160  | MaIMM1_to_DIR1(b,b1) -> (f12 b b1)
 161  | MaIX0p_to_DIR1(b) -> (f13 b)
 162  | MaDIR1_to_IX0p(b) -> (f14 b)
 163  | MaINHA_and_IMM1(b) -> (f15 b)
 164  | MaINHX_and_IMM1(b) -> (f16 b)
 165  | MaIMM1_and_IMM1(b,b1) -> (f17 b b1)
 166  | MaDIR1_and_IMM1(b,b1) -> (f18 b b1)
 167  | MaIX0_and_IMM1(b) -> (f19 b)
 168  | MaIX0p_and_IMM1(b) -> (f20 b)
 169  | MaIX1_and_IMM1(b,b1) -> (f21 b b1)
 170  | MaIX1p_and_IMM1(b,b1) -> (f22 b b1)
 171  | MaSP1_and_IMM1(b,b1) -> (f23 b b1)
 172  | MaDIRn(o,b) -> (f24 o b)
 173  | MaDIRn_and_IMM1(o,b,b1) -> (f25 o b b1)
 174  | MaTNY(e) -> (f26 e)
 175  | MaSRT(b) -> (f27 b))
 176 ))))))))))))))))))))))))))))))))))))
 177 ;;
 178
 179 type instruction =
 180 Instr of Matita_freescale_opcode.instr_mode * Matita_freescale_opcode.opcode * mA_check
 181 ;;
 182
 183 let instruction_rec =
 184 (function f -> (function i ->
 185 (match i with
 186    Instr(i1,o,m) -> (f i1 o m))
 187 ))
 188 ;;
 189
 190 let instruction_rect =
 191 (function f -> (function i ->
 192 (match i with
 193    Instr(i1,o,m) -> (f i1 o m))
 194 ))
 195 ;;
 196
 197 let args_picker =
 198 (function m -> (function i -> (function args ->
 199 (match args with
 200    MaINH -> Obj.magic ((Matita_list_list.Nil))
 201  | MaINHA -> Obj.magic ((Matita_list_list.Nil))
 202  | MaINHX -> Obj.magic ((Matita_list_list.Nil))
 203  | MaINHH -> Obj.magic ((Matita_list_list.Nil))
 204  | MaINHX0ADD -> Obj.magic ((Matita_list_list.Nil))
 205  | MaINHX1ADD(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 206  | MaINHX2ADD(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
 207  | MaIMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 208  | MaIMM1EXT(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 209  | MaIMM2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
 210  | MaDIR1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 211  | MaDIR2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
 212  | MaIX0 -> Obj.magic ((Matita_list_list.Nil))
 213  | MaIX1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 214  | MaIX2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
 215  | MaSP1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 216  | MaSP2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
 217  | MaDIR1_to_DIR1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 218  | MaIMM1_to_DIR1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 219  | MaIX0p_to_DIR1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 220  | MaDIR1_to_IX0p(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 221  | MaINHA_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 222  | MaINHX_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 223  | MaIMM1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 224  | MaDIR1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 225  | MaIX0_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 226  | MaIX0p_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 227  | MaIX1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 228  | MaIX1p_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 229  | MaSP1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 230  | MaDIRn(_,b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
 231  | MaDIRn_and_IMM1(_,b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
 232  | MaTNY(_) -> Obj.magic ((Matita_list_list.Nil))
 233  | MaSRT(_) -> Obj.magic ((Matita_list_list.Nil)))
 234 )))
 235 ;;
 236
 237 let bytes_of_pseudo_instr_mode_param =
 238 (function m -> (function o -> (function i -> (function p -> (let rec aux =
 239 (function param ->
 240 (match param with
 241    Matita_list_list.Nil -> (Matita_datatypes_constructors.None)
 242  | Matita_list_list.Cons(hd,tl) ->
 243 (match (Matita_freescale_extra.and_bool (Matita_freescale_opcode.eqop m o (Matita_freescale_extra.fst4T hd)) (Matita_freescale_opcode.eqim i (Matita_freescale_extra.snd4T hd))) with
 244    Matita_datatypes_bool.True ->
 245 (match (Matita_freescale_extra.thd4T hd) with
 246    Matita_freescale_opcode.Byte(isab) -> (Matita_datatypes_constructors.Some((Matita_list_list.append (Matita_list_list.Cons((TByte(isab)),(Matita_list_list.Nil))) (args_picker m i p))))
 247  | Matita_freescale_opcode.Word(isaw) -> (Matita_datatypes_constructors.Some((Matita_list_list.append (Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h isaw))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l isaw))),(Matita_list_list.Nil))))) (args_picker m i p)))))
 248
 249  | Matita_datatypes_bool.False -> (aux tl))
 250 )
 251 ) in aux (opcode_table m))))))
 252 ;;
 253
 254 let opcode_to_any =
 255 (function m -> (function o -> (Matita_freescale_opcode.AnyOP(o))))
 256 ;;
 257
 258 let compile =
 259 (function mcu -> (function i -> (function op -> (function arg -> (let res = (bytes_of_pseudo_instr_mode_param mcu (opcode_to_any mcu op) i arg) in (let value = (
 260 (match res with
 261    Matita_datatypes_constructors.None -> Obj.magic ((Matita_logic_connectives.false_rect))
 262  | Matita_datatypes_constructors.Some(v) -> Obj.magic (v))
 263 ) in value))))))
 264 ;;
 265
 266 let source_to_byte8 =
 267 (function mcu ->
 268 (match mcu with
 269    Matita_freescale_opcode.HC05 -> Obj.magic ((function l -> (let rec aux =
 270 (function p1 -> (function p2 ->
 271 (match p1 with
 272    Matita_list_list.Nil -> p2
 273  | Matita_list_list.Cons(hd,tl) ->
 274 (match hd with
 275    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
 276 )
 277 )) in aux l (Matita_list_list.Nil))))
 278  | Matita_freescale_opcode.HC08 -> Obj.magic ((function l -> (let rec aux =
 279 (function p1 -> (function p2 ->
 280 (match p1 with
 281    Matita_list_list.Nil -> p2
 282  | Matita_list_list.Cons(hd,tl) ->
 283 (match hd with
 284    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
 285 )
 286 )) in aux l (Matita_list_list.Nil))))
 287  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function l -> (let rec aux =
 288 (function p1 -> (function p2 ->
 289 (match p1 with
 290    Matita_list_list.Nil -> p2
 291  | Matita_list_list.Cons(hd,tl) ->
 292 (match hd with
 293    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
 294 )
 295 )) in aux l (Matita_list_list.Nil))))
 296  | Matita_freescale_opcode.RS08 -> Obj.magic ((function l -> (let rec aux =
 297 (function p1 -> (function p2 ->
 298 (match p1 with
 299    Matita_list_list.Nil -> p2
 300  | Matita_list_list.Cons(hd,tl) ->
 301 (match hd with
 302    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
 303 )
 304 )) in aux l (Matita_list_list.Nil)))))
 305 )
 306 ;;
 307