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

   1 type error_type =
   2 ILL_OP
   3  | ILL_FETCH_AD
   4  | ILL_EX_AD
   5 ;;
   6
   7 let error_type_rec =
   8 (function p -> (function p1 -> (function p2 -> (function e ->
   9 (match e with
  10    ILL_OP -> p
  11  | ILL_FETCH_AD -> p1
  12  | ILL_EX_AD -> p2)
  13 ))))
  14 ;;
  15
  16 let error_type_rect =
  17 (function p -> (function p1 -> (function p2 -> (function e ->
  18 (match e with
  19    ILL_OP -> p
  20  | ILL_FETCH_AD -> p1
  21  | ILL_EX_AD -> p2)
  22 ))))
  23 ;;
  24
  25 type ('a) fetch_result =
  26 FetchERR of error_type
  27  | FetchOK of 'a * Matita_freescale_word16.word16
  28 ;;
  29
  30 let fetch_result_rec =
  31 (function f -> (function f1 -> (function f2 ->
  32 (match f2 with
  33    FetchERR(e) -> (f e)
  34  | FetchOK(t,w) -> (f1 t w))
  35 )))
  36 ;;
  37
  38 let fetch_result_rect =
  39 (function f -> (function f1 -> (function f2 ->
  40 (match f2 with
  41    FetchERR(e) -> (f e)
  42  | FetchOK(t,w) -> (f1 t w))
  43 )))
  44 ;;
  45
  46 let rS08_memory_filter_read_aux =
  47 (function t -> (function s -> (function addr -> (function fREG -> (function fMEM ->
  48 (match s with
  49    Matita_freescale_status.Mk_any_status(alu,mem,chk,_) ->
  50 (match Obj.magic(alu) with
  51    Matita_freescale_status.Mk_alu_RS08(_,_,_,_,xm,psm,_,_) ->
  52 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
  53    Matita_datatypes_bool.True -> (fREG xm)
  54  | Matita_datatypes_bool.False ->
  55 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
  56    Matita_datatypes_bool.True -> (fREG psm)
  57  | Matita_datatypes_bool.False ->
  58 (match (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) with
  59    Matita_datatypes_bool.True -> (fMEM mem chk (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),xm)))
  60  | Matita_datatypes_bool.False ->
  61 (match (Matita_freescale_word16.in_range addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) with
  62    Matita_datatypes_bool.True -> (fMEM mem chk (Matita_freescale_word16.or_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_freescale_word16.Mk_word16(psm,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))) (Matita_freescale_word16.and_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))))))
  63  | Matita_datatypes_bool.False -> (fMEM mem chk addr))
  64 )
  65 )
  66 )
  67 )
  68 )
  69 )))))
  70 ;;
  71
  72 let rS08_memory_filter_read =
  73 (function t -> (function s -> (function addr -> (rS08_memory_filter_read_aux t s addr (function b -> (Matita_datatypes_constructors.Some(b))) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_read t m c a))))))))
  74 ;;
  75
  76 let rS08_memory_filter_read_bit =
  77 (function t -> (function s -> (function addr -> (function sub -> (rS08_memory_filter_read_aux t s addr (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_struct.bits_of_byte8 b))))) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_read_bit t m c a sub)))))))))
  78 ;;
  79
  80 let memory_filter_read =
  81 (function m -> (function t ->
  82 (match m with
  83    Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (Matita_freescale_memory_abs.mem_read t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr))))
  84  | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (Matita_freescale_memory_abs.mem_read t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr))))
  85  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (Matita_freescale_memory_abs.mem_read t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr))))
  86  | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (rS08_memory_filter_read t s addr)))))
  87 ))
  88 ;;
  89
  90 let memory_filter_read_bit =
  91 (function m -> (function t ->
  92 (match m with
  93    Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (function sub -> (Matita_freescale_memory_abs.mem_read_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr sub)))))
  94  | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (function sub -> (Matita_freescale_memory_abs.mem_read_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr sub)))))
  95  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (Matita_freescale_memory_abs.mem_read_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr sub)))))
  96  | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (rS08_memory_filter_read_bit t s addr sub))))))
  97 ))
  98 ;;
  99
 100 let rS08_memory_filter_write_aux =
 101 (function t -> (function s -> (function addr -> (function fREG -> (function fMEM ->
 102 (match s with
 103    Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) ->
 104 (match Obj.magic(alu) with
 105    Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl) ->
 106 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
 107    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,(fREG xm),psm,zfl,cfl))),mem,chk,clk))))
 108  | Matita_datatypes_bool.False ->
 109 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
 110    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,(fREG psm),zfl,cfl))),mem,chk,clk))))
 111  | Matita_datatypes_bool.False ->
 112 (match (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) with
 113    Matita_datatypes_bool.True -> (Matita_freescale_extra.opt_map (fMEM mem chk (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),xm))) (function mem' -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl))),mem',chk,clk))))))
 114  | Matita_datatypes_bool.False ->
 115 (match (Matita_freescale_word16.in_range addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) with
 116    Matita_datatypes_bool.True -> (Matita_freescale_extra.opt_map (fMEM mem chk (Matita_freescale_word16.or_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_freescale_word16.Mk_word16(psm,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))) (Matita_freescale_word16.and_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))))))) (function mem' -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl))),mem',chk,clk))))))
 117  | Matita_datatypes_bool.False -> (Matita_freescale_extra.opt_map (fMEM mem chk addr) (function mem' -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl))),mem',chk,clk)))))))
 118 )
 119 )
 120 )
 121 )
 122 )
 123 )))))
 124 ;;
 125
 126 let rS08_memory_filter_write =
 127 (function t -> (function s -> (function addr -> (function val_ -> (rS08_memory_filter_write_aux t s addr (function b -> val_) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_update t m c a val_)))))))))
 128 ;;
 129
 130 let rS08_memory_filter_write_bit =
 131 (function t -> (function s -> (function addr -> (function sub -> (function val_ -> (rS08_memory_filter_write_aux t s addr (function b -> (Matita_freescale_memory_struct.byte8_of_bits (Matita_freescale_memory_struct.setn_array8T sub (Matita_freescale_memory_struct.bits_of_byte8 b) val_))) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_update_bit t m c a sub val_))))))))))
 132 ;;
 133
 134 let memory_filter_write =
 135 (function m -> (function t ->
 136 (match m with
 137    Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC05 t s mem)))))))))
 138  | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC08 t s mem)))))))))
 139  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 t s mem)))))))))
 140  | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (rS08_memory_filter_write t s addr val_))))))
 141 ))
 142 ;;
 143
 144 let memory_filter_write_bit =
 145 (function m -> (function t ->
 146 (match m with
 147    Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr sub val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC05 t s mem))))))))))
 148  | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr sub val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC08 t s mem))))))))))
 149  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr sub val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 t s mem))))))))))
 150  | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (rS08_memory_filter_write_bit t s addr sub val_)))))))
 151 ))
 152 ;;
 153
 154 let filtered_inc_w16 =
 155 (function m -> (function t -> (function s -> (function w -> (Matita_freescale_status.get_pc_reg m t (Matita_freescale_status.set_pc_reg m t s (Matita_freescale_word16.succ_w16 w)))))))
 156 ;;
 157
 158 let filtered_plus_w16 =
 159 let rec filtered_plus_w16 =
 160 (function m -> (function t -> (function s -> (function w -> (function n ->
 161 (match n with
 162    Matita_nat_nat.O -> w
 163  | Matita_nat_nat.S(n') -> (filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n'))
 164 ))))) in filtered_plus_w16
 165 ;;
 166
 167 let fetch =
 168 (function m -> (function t -> (function s -> (let pc = (Matita_freescale_status.get_pc_reg m t s) in (let pc_next1 = (filtered_inc_w16 m t s pc) in (let pc_next2 = (filtered_inc_w16 m t s pc_next1) in
 169 (match (memory_filter_read m t s pc) with
 170    Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
 171  | Matita_datatypes_constructors.Some(bh) ->
 172 (match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Byte(bh))) with
 173    Matita_datatypes_constructors.None ->
 174 (match m with
 175    Matita_freescale_opcode.HC05 -> (FetchERR(ILL_OP))
 176  | Matita_freescale_opcode.HC08 ->
 177 (match (Matita_freescale_byte8.eq_b8 bh (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE))) with
 178    Matita_datatypes_bool.True ->
 179 (match (memory_filter_read m t s pc_next1) with
 180    Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
 181  | Matita_datatypes_constructors.Some(bl) ->
 182 (match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Word((Matita_freescale_word16.Mk_word16(bh,bl))))) with
 183    Matita_datatypes_constructors.None -> (FetchERR(ILL_OP))
 184  | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next2)))
 185 )
 186
 187  | Matita_datatypes_bool.False -> (FetchERR(ILL_OP)))
 188
 189  | Matita_freescale_opcode.HCS08 ->
 190 (match (Matita_freescale_byte8.eq_b8 bh (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE))) with
 191    Matita_datatypes_bool.True ->
 192 (match (memory_filter_read m t s pc_next1) with
 193    Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
 194  | Matita_datatypes_constructors.Some(bl) ->
 195 (match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Word((Matita_freescale_word16.Mk_word16(bh,bl))))) with
 196    Matita_datatypes_constructors.None -> (FetchERR(ILL_OP))
 197  | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next2)))
 198 )
 199
 200  | Matita_datatypes_bool.False -> (FetchERR(ILL_OP)))
 201
 202  | Matita_freescale_opcode.RS08 -> (FetchERR(ILL_OP)))
 203
 204  | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next1)))
 205 )
 206 ))))))
 207 ;;
 208
 209 let loadb_from =
 210 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (Matita_freescale_extra.opt_map (memory_filter_read m t s addr) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,(filtered_plus_w16 m t s cur_pc fetched)))))))))))))
 211 ;;
 212
 213 let loadbit_from =
 214 (function m -> (function t -> (function s -> (function addr -> (function sub -> (function cur_pc -> (function fetched -> (Matita_freescale_extra.opt_map (memory_filter_read_bit m t s addr sub) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,(filtered_plus_w16 m t s cur_pc fetched))))))))))))))
 215 ;;
 216
 217 let loadw_from =
 218 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (Matita_freescale_extra.opt_map (memory_filter_read m t s addr) (function bh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (Matita_freescale_word16.succ_w16 addr)) (function bl -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(bh,bl)),(filtered_plus_w16 m t s cur_pc fetched)))))))))))))))
 219 ;;
 220
 221 let writeb_to =
 222 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (function writeb -> (Matita_freescale_extra.opt_map (memory_filter_write m t s addr writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,(filtered_plus_w16 m t s cur_pc fetched))))))))))))))
 223 ;;
 224
 225 let writebit_to =
 226 (function m -> (function t -> (function s -> (function addr -> (function sub -> (function cur_pc -> (function fetched -> (function writeb -> (Matita_freescale_extra.opt_map (memory_filter_write_bit m t s addr sub writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,(filtered_plus_w16 m t s cur_pc fetched)))))))))))))))
 227 ;;
 228
 229 let writew_to =
 230 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (function writew -> (Matita_freescale_extra.opt_map (memory_filter_write m t s addr (Matita_freescale_word16.w16h writew)) (function tmps1 -> (Matita_freescale_extra.opt_map (memory_filter_write m t tmps1 (Matita_freescale_word16.succ_w16 addr) (Matita_freescale_word16.w16l writew)) (function tmps2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps2,(filtered_plus_w16 m t tmps2 cur_pc fetched))))))))))))))))
 231 ;;
 232
 233 type aux_load_typing = (Matita_freescale_status.any_status -> (Matita_freescale_word16.word16 -> (Matita_freescale_word16.word16 -> (Matita_nat_nat.nat -> ((Matita_freescale_status.any_status,unit (* TOO POLYMORPHIC TYPE *),Matita_freescale_word16.word16) Matita_freescale_extra.prod3T) Matita_datatypes_constructors.option))))
 234 ;;
 235
 236 let aux_load =
 237 (function m -> (function t -> (function byteflag ->
 238 (match byteflag with
 239    Matita_datatypes_bool.True -> Obj.magic ((loadb_from m t))
 240  | Matita_datatypes_bool.False -> Obj.magic ((loadw_from m t)))
 241 )))
 242 ;;
 243
 244 type aux_write_typing = (Matita_freescale_status.any_status -> (Matita_freescale_word16.word16 -> (Matita_freescale_word16.word16 -> (Matita_nat_nat.nat -> (unit (* TOO POLYMORPHIC TYPE *) -> ((Matita_freescale_status.any_status,Matita_freescale_word16.word16) Matita_datatypes_constructors.prod) Matita_datatypes_constructors.option)))))
 245 ;;
 246
 247 let aux_write =
 248 (function m -> (function t -> (function byteflag ->
 249 (match byteflag with
 250    Matita_datatypes_bool.True -> Obj.magic ((writeb_to m t))
 251  | Matita_datatypes_bool.False -> Obj.magic ((writew_to m t)))
 252 )))
 253 ;;
 254
 255 let mode_IMM1_load =
 256 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,(filtered_inc_w16 m t s cur_pc)))))))))))
 257 ;;
 258
 259 let mode_IMM1EXT_load =
 260 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b)),(filtered_inc_w16 m t s cur_pc)))))))))))
 261 ;;
 262
 263 let mode_IMM2_load =
 264 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function bh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function bl -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(bh,bl)),(filtered_plus_w16 m t s cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))
 265 ;;
 266
 267 let mode_DIR1_load =
 268 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (aux_load m t byteflag s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))
 269 ;;
 270
 271 let mode_DIR1n_load =
 272 (function m -> (function t -> (function s -> (function cur_pc -> (function sub -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (loadbit_from m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) sub cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))
 273 ;;
 274
 275 let mode_DIR1_write =
 276 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (aux_write m t byteflag s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writebw)))))))))
 277 ;;
 278
 279 let mode_DIR1n_write =
 280 (function m -> (function t -> (function s -> (function cur_pc -> (function sub -> (function writeb -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (writebit_to m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) sub cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writeb)))))))))
 281 ;;
 282
 283 let mode_DIR2_load =
 284 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addrh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function addrl -> (aux_load m t byteflag s (Matita_freescale_word16.Mk_word16(addrh,addrl)) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))
 285 ;;
 286
 287 let mode_DIR2_write =
 288 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addrh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function addrl -> (aux_write m t byteflag s (Matita_freescale_word16.Mk_word16(addrh,addrl)) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) writebw)))))))))))
 289 ;;
 290
 291 let get_IX =
 292 (function m -> (function t -> (function s ->
 293 (match m with
 294    Matita_freescale_opcode.HC05 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function indx -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),indx))))))
 295  | Matita_freescale_opcode.HC08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s) (function indx -> (Matita_datatypes_constructors.Some(indx))))
 296  | Matita_freescale_opcode.HCS08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s) (function indx -> (Matita_datatypes_constructors.Some(indx))))
 297  | Matita_freescale_opcode.RS08 -> (Matita_datatypes_constructors.None))
 298 )))
 299 ;;
 300
 301 let mode_IX0_load =
 302 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (aux_load m t byteflag s addr cur_pc Matita_nat_nat.O))))))))
 303 ;;
 304
 305 let mode_IX0_write =
 306 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (aux_write m t byteflag s addr cur_pc Matita_nat_nat.O writebw)))))))))
 307 ;;
 308
 309 let mode_IX1_load =
 310 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))))
 311 ;;
 312
 313 let mode_IX1ADD_load =
 314 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function b -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b))),(filtered_inc_w16 m t s cur_pc)))))))))))))
 315 ;;
 316
 317 let mode_IX1_write =
 318 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writebw)))))))))))
 319 ;;
 320
 321 let mode_IX2_load =
 322 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))
 323 ;;
 324
 325 let mode_IX2ADD_load =
 326 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function bh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function bl -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(bh,bl))),(filtered_plus_w16 m t s cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))
 327 ;;
 328
 329 let mode_IX2_write =
 330 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) writebw)))))))))))))
 331 ;;
 332
 333 let mode_SP1_load =
 334 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))))
 335 ;;
 336
 337 let mode_SP1_write =
 338 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writebw)))))))))))
 339 ;;
 340
 341 let mode_SP2_load =
 342 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))
 343 ;;
 344
 345 let mode_SP2_write =
 346 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) writebw)))))))))))))
 347 ;;
 348
 349 let aux_inc_indX_16 =
 350 (function m -> (function t -> (function s -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s) (function x_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_16_reg m t s (Matita_freescale_word16.succ_w16 x_op)) (function s_tmp -> (Matita_datatypes_constructors.Some(s_tmp)))))))))
 351 ;;
 352
 353 let multi_mode_load =
 354 (function byteflag -> (function m -> (function t ->
 355 (match byteflag with
 356    Matita_datatypes_bool.True -> Obj.magic ((function s -> (function cur_pc -> (function i ->
 357 (match i with
 358    Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
 359  | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_status.get_acc_8_low_reg m t s),cur_pc))))
 360  | Matita_freescale_opcode.MODE_INHX -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function indx -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,indx,cur_pc))))))
 361  | Matita_freescale_opcode.MODE_INHH -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_high_reg m t s) (function indx -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,indx,cur_pc))))))
 362  | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
 363  | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
 364  | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
 365  | Matita_freescale_opcode.MODE_IMM1 -> (mode_IMM1_load m t s cur_pc)
 366  | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
 367  | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
 368  | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
 369  | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_load Matita_datatypes_bool.True m t s cur_pc)
 370  | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc)
 371  | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc)
 372  | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_load Matita_datatypes_bool.True m t s cur_pc)
 373  | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_load Matita_datatypes_bool.True m t s cur_pc)
 374  | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_load Matita_datatypes_bool.True m t s cur_pc)
 375  | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
 376  | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (mode_IMM1_load m t s cur_pc)
 377  | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc)
 378  | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
 379  | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.None)
 380  | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_datatypes_constructors.None)
 381  | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
 382  | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_datatypes_constructors.None)
 383  | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_datatypes_constructors.None)
 384  | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
 385  | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_datatypes_constructors.None)
 386  | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
 387  | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_datatypes_constructors.None)
 388  | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
 389  | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
 390  | Matita_freescale_opcode.MODE_TNY(e) -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,e))))) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,cur_pc))))))
 391  | Matita_freescale_opcode.MODE_SRT(e) -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_aux_bases.byte8_of_bitrigesim e)))) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,cur_pc)))))))
 392 ))))
 393  | Matita_datatypes_bool.False -> Obj.magic ((function s -> (function cur_pc -> (function i ->
 394 (match i with
 395    Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
 396  | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.None)
 397  | Matita_freescale_opcode.MODE_INHX -> (Matita_datatypes_constructors.None)
 398  | Matita_freescale_opcode.MODE_INHH -> (Matita_datatypes_constructors.None)
 399  | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_freescale_extra.opt_map (get_IX m t s) (function w -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,w,cur_pc))))))
 400  | Matita_freescale_opcode.MODE_INHX1ADD -> (mode_IX1ADD_load m t s cur_pc)
 401  | Matita_freescale_opcode.MODE_INHX2ADD -> (mode_IX2ADD_load m t s cur_pc)
 402  | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
 403  | Matita_freescale_opcode.MODE_IMM1EXT -> (mode_IMM1EXT_load m t s cur_pc)
 404  | Matita_freescale_opcode.MODE_IMM2 -> (mode_IMM2_load m t s cur_pc)
 405  | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.False m t s cur_pc)
 406  | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_load Matita_datatypes_bool.False m t s cur_pc)
 407  | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_load Matita_datatypes_bool.False m t s cur_pc)
 408  | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_load Matita_datatypes_bool.False m t s cur_pc)
 409  | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_load Matita_datatypes_bool.False m t s cur_pc)
 410  | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_load Matita_datatypes_bool.False m t s cur_pc)
 411  | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_load Matita_datatypes_bool.False m t s cur_pc)
 412  | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (Matita_datatypes_constructors.None)
 413  | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (Matita_datatypes_constructors.None)
 414  | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_datatypes_constructors.None)
 415  | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_datatypes_constructors.None)
 416  | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc) (function s_immb_and_PC ->
 417 (match s_immb_and_PC with
 418    Matita_freescale_extra.TripleT(_,immb,cur_pc') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16((Matita_freescale_status.get_acc_8_low_reg m t s),immb)),cur_pc')))))
 419 ))
 420  | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function x_op -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc) (function s_immb_and_PC ->
 421 (match s_immb_and_PC with
 422    Matita_freescale_extra.TripleT(_,immb,cur_pc') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(x_op,immb)),cur_pc')))))
 423 ))))
 424  | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc) (function s_immb1_and_PC ->
 425 (match s_immb1_and_PC with
 426    Matita_freescale_extra.TripleT(_,immb1,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb2_and_PC ->
 427 (match s_immb2_and_PC with
 428    Matita_freescale_extra.TripleT(_,immb2,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(immb1,immb2)),cur_pc'')))))
 429 )))
 430 ))
 431  | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc) (function s_dirb_and_PC ->
 432 (match s_dirb_and_PC with
 433    Matita_freescale_extra.TripleT(_,dirb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 434 (match s_immb_and_PC with
 435    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(dirb,immb)),cur_pc'')))))
 436 )))
 437 ))
 438  | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
 439 (match s_ixb_and_PC with
 440    Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 441 (match s_immb_and_PC with
 442    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))
 443 )))
 444 ))
 445  | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
 446 (match s_ixb_and_PC with
 447    Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 448 (match s_immb_and_PC with
 449    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s) (function s' -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s',(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))))
 450 )))
 451 ))
 452  | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
 453 (match s_ixb_and_PC with
 454    Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 455 (match s_immb_and_PC with
 456    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))
 457 )))
 458 ))
 459  | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
 460 (match s_ixb_and_PC with
 461    Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 462 (match s_immb_and_PC with
 463    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s) (function s' -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s',(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))))
 464 )))
 465 ))
 466  | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_SP1_load Matita_datatypes_bool.True m t s cur_pc) (function s_spb_and_PC ->
 467 (match s_spb_and_PC with
 468    Matita_freescale_extra.TripleT(_,spb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 469 (match s_immb_and_PC with
 470    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(spb,immb)),cur_pc'')))))
 471 )))
 472 ))
 473  | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
 474  | Matita_freescale_opcode.MODE_DIRn_and_IMM1(msk) -> (Matita_freescale_extra.opt_map (mode_DIR1n_load m t s cur_pc msk) (function s_dirbn_and_PC ->
 475 (match s_dirbn_and_PC with
 476    Matita_freescale_extra.TripleT(_,dirbn,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
 477 (match s_immb_and_PC with
 478    Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,
 479 (match dirbn with
 480    Matita_datatypes_bool.True -> Matita_freescale_exadecim.X1
 481  | Matita_datatypes_bool.False -> Matita_freescale_exadecim.X0)
 482 )),immb)),cur_pc'')))))
 483 )))
 484 ))
 485  | Matita_freescale_opcode.MODE_TNY(_) -> (Matita_datatypes_constructors.None)
 486  | Matita_freescale_opcode.MODE_SRT(_) -> (Matita_datatypes_constructors.None))
 487 )))))
 488 )))
 489 ;;
 490
 491 let multi_mode_write =
 492 (function byteflag -> (function m -> (function t ->
 493 (match byteflag with
 494    Matita_datatypes_bool.True -> Obj.magic ((function s -> (function cur_pc -> (function i -> (function writeb ->
 495 (match i with
 496    Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
 497  | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s writeb),cur_pc))))
 498  | Matita_freescale_opcode.MODE_INHX -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
 499  | Matita_freescale_opcode.MODE_INHH -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_high_reg m t s writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
 500  | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
 501  | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
 502  | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
 503  | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
 504  | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
 505  | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
 506  | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 507  | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_write Matita_datatypes_bool.True m t s cur_pc writeb)
 508  | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb)
 509  | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 510  | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_write Matita_datatypes_bool.True m t s cur_pc writeb)
 511  | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 512  | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_write Matita_datatypes_bool.True m t s cur_pc writeb)
 513  | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 514  | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 515  | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_freescale_extra.opt_map (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb) (function s_and_PC ->
 516 (match s_and_PC with
 517    Matita_datatypes_constructors.Pair(s_op,pC_op) -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s_op) (function s_op' -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_op',pC_op)))))))
 518 ))
 519  | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_freescale_extra.opt_map (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb) (function s_and_PC ->
 520 (match s_and_PC with
 521    Matita_datatypes_constructors.Pair(s_op,pC_op) -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s_op) (function s_op' -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_op',pC_op)))))))
 522 ))
 523  | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s writeb),cur_pc))))
 524  | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
 525  | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
 526  | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 527  | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb)
 528  | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
 529  | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (mode_IX1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 530  | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
 531  | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (mode_SP1_write Matita_datatypes_bool.True m t s cur_pc writeb)
 532  | Matita_freescale_opcode.MODE_DIRn(msk) -> (mode_DIR1n_write m t s cur_pc msk (Matita_freescale_memory_struct.getn_array8T msk (Matita_freescale_memory_struct.bits_of_byte8 writeb)))
 533  | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
 534  | Matita_freescale_opcode.MODE_TNY(e) -> (Matita_freescale_extra.opt_map (memory_filter_write m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,e)))) writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
 535  | Matita_freescale_opcode.MODE_SRT(e) -> (Matita_freescale_extra.opt_map (memory_filter_write m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_aux_bases.byte8_of_bitrigesim e))) writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc)))))))
 536 )))))
 537  | Matita_datatypes_bool.False -> Obj.magic ((function s -> (function cur_pc -> (function i -> (function writew ->
 538 (match i with
 539    Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
 540  | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.None)
 541  | Matita_freescale_opcode.MODE_INHX -> (Matita_datatypes_constructors.None)
 542  | Matita_freescale_opcode.MODE_INHH -> (Matita_datatypes_constructors.None)
 543  | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
 544  | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
 545  | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
 546  | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
 547  | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
 548  | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
 549  | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.False m t s cur_pc writew)
 550  | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_write Matita_datatypes_bool.False m t s cur_pc writew)
 551  | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_write Matita_datatypes_bool.False m t s cur_pc writew)
 552  | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_write Matita_datatypes_bool.False m t s cur_pc writew)
 553  | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_write Matita_datatypes_bool.False m t s cur_pc writew)
 554  | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_write Matita_datatypes_bool.False m t s cur_pc writew)
 555  | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_write Matita_datatypes_bool.False m t s cur_pc writew)
 556  | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (Matita_datatypes_constructors.None)
 557  | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (Matita_datatypes_constructors.None)
 558  | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_datatypes_constructors.None)
 559  | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_datatypes_constructors.None)
 560  | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.None)
 561  | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_datatypes_constructors.None)
 562  | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
 563  | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_datatypes_constructors.None)
 564  | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_datatypes_constructors.None)
 565  | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
 566  | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_datatypes_constructors.None)
 567  | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
 568  | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_datatypes_constructors.None)
 569  | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
 570  | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
 571  | Matita_freescale_opcode.MODE_TNY(_) -> (Matita_datatypes_constructors.None)
 572  | Matita_freescale_opcode.MODE_SRT(_) -> (Matita_datatypes_constructors.None))
 573 ))))))
 574 )))
 575 ;;