helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_multivm.ml

   1 let execute_ADC_ADD_aux =
   2 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function setflag -> (function fAMC -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
   3 (match s_M_PC with
   4    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let a_op = (Matita_freescale_status.get_acc_8_low_reg m t s_tmp1) in
   5 (match (fAMC a_op m_op (Matita_freescale_status.get_c_flag m t s_tmp1)) with
   6    Matita_datatypes_constructors.Pair(r_op,carry) -> (let a7 = (Matita_freescale_byte8.mSB_b8 a_op) in (let m7 = (Matita_freescale_byte8.mSB_b8 m_op) in (let r7 = (Matita_freescale_byte8.mSB_b8 r_op) in (let a3 = (Matita_freescale_exadecim.mSB_ex (Matita_freescale_byte8.b8l a_op)) in (let m3 = (Matita_freescale_exadecim.mSB_ex (Matita_freescale_byte8.b8l m_op)) in (let r3 = (Matita_freescale_exadecim.mSB_ex (Matita_freescale_byte8.b8l r_op)) in (let s_tmp2 =
   7 (match setflag with
   8    Matita_datatypes_bool.True -> (Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 r_op)
   9  | Matita_datatypes_bool.False -> s_tmp1)
  10  in (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp4 = (Matita_freescale_status.set_c_flag m t s_tmp3 (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool a7 m7) (Matita_freescale_extra.and_bool m7 (Matita_freescale_extra.not_bool r7))) (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool r7) a7))) in (let s_tmp5 = (Matita_freescale_status.setweak_n_flag m t s_tmp4 r7) in (let s_tmp6 = (Matita_freescale_status.setweak_h_flag m t s_tmp5 (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool a3 m3) (Matita_freescale_extra.and_bool m3 (Matita_freescale_extra.not_bool r3))) (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool r3) a3))) in (let s_tmp7 = (Matita_freescale_status.setweak_v_flag m t s_tmp6 (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool a7 m7) (Matita_freescale_extra.not_bool r7)) (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool a7) (Matita_freescale_extra.not_bool m7)) r7))) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp7,new_pc)))))))))))))))))
  11 ))
  12 )))))))))
  13 ;;
  14
  15 let execute_AND_BIT_EOR_ORA_aux =
  16 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function setflag -> (function fAM -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
  17 (match s_M_PC with
  18    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let r_op = (fAM (Matita_freescale_status.get_acc_8_low_reg m t s_tmp1) m_op) in (let s_tmp2 =
  19 (match setflag with
  20    Matita_datatypes_bool.True -> (Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 r_op)
  21  | Matita_datatypes_bool.False -> s_tmp1)
  22  in (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 (Matita_freescale_byte8.mSB_b8 r_op)) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc))))))))))
  23 )))))))))
  24 ;;
  25
  26 let execute_ASL_ASR_LSR_ROL_ROR_aux =
  27 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function fMC -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
  28 (match s_M_PC with
  29    Matita_freescale_extra.TripleT(s_tmp1,m_op,_) ->
  30 (match (fMC m_op (Matita_freescale_status.get_c_flag m t s_tmp1)) with
  31    Matita_datatypes_constructors.Pair(r_op,carry) -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s_tmp1 cur_pc i r_op) (function s_PC ->
  32 (match s_PC with
  33    Matita_datatypes_constructors.Pair(s_tmp2,new_pc) -> (let s_tmp3 = (Matita_freescale_status.set_c_flag m t s_tmp2 carry) in (let s_tmp4 = (Matita_freescale_status.set_z_flag m t s_tmp3 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp5 = (Matita_freescale_status.setweak_n_flag m t s_tmp4 (Matita_freescale_byte8.mSB_b8 r_op)) in (let s_tmp6 = (Matita_freescale_status.setweak_v_flag m t s_tmp5 (Matita_freescale_extra.xor_bool (Matita_freescale_byte8.mSB_b8 r_op) carry)) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp6,new_pc)))))))))
  34 )))
  35 )
  36 ))))))))
  37 ;;
  38
  39 let byte_extension =
  40 (function b -> (Matita_freescale_word16.Mk_word16(
  41 (match (Matita_freescale_byte8.mSB_b8 b) with
  42    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))
  43  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
  44 ,b)))
  45 ;;
  46
  47 let branched_pc =
  48 (function m -> (function t -> (function s -> (function cur_pc -> (function b -> (Matita_freescale_status.get_pc_reg m t (Matita_freescale_status.set_pc_reg m t s (Matita_freescale_word16.plus_w16nc cur_pc (byte_extension b)))))))))
  49 ;;
  50
  51 let execute_any_BRANCH =
  52 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function fCOND -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
  53 (match s_M_PC with
  54    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) ->
  55 (match fCOND with
  56    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,(branched_pc m t s_tmp1 new_pc m_op)))))
  57  | Matita_datatypes_bool.False -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,new_pc)))))
  58 )
  59 ))))))))
  60 ;;
  61
  62 let execute_BCLRn_BSETn_aux =
  63 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function optval -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s cur_pc i optval) (function s_PC ->
  64 (match s_PC with
  65    Matita_datatypes_constructors.Pair(s_tmp1,new_pc) -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,new_pc)))))
  66 ))))))))
  67 ;;
  68
  69 let execute_BRCLRn_BRSETn_aux =
  70 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function fCOND -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
  71 (match s_M_PC with
  72    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) ->
  73 (match m_op with
  74    Matita_freescale_word16.Mk_word16(mH_op,mL_op) ->
  75 (match (fCOND mH_op) with
  76    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,(branched_pc m t s_tmp1 new_pc mL_op)))))
  77  | Matita_datatypes_bool.False -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,new_pc)))))
  78 )
  79 )
  80 ))))))))
  81 ;;
  82
  83 let execute_COM_DEC_INC_NEG_aux =
  84 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function fM -> (function fV -> (function fC -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
  85 (match s_M_PC with
  86    Matita_freescale_extra.TripleT(s_tmp1,m_op,_) -> (let r_op = (fM m_op) in (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s_tmp1 cur_pc i r_op) (function s_PC ->
  87 (match s_PC with
  88    Matita_datatypes_constructors.Pair(s_tmp2,new_pc) -> (let s_tmp3 = (Matita_freescale_status.set_c_flag m t s_tmp2 (fC (Matita_freescale_status.get_c_flag m t s_tmp2) r_op)) in (let s_tmp4 = (Matita_freescale_status.set_z_flag m t s_tmp3 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp5 = (Matita_freescale_status.setweak_n_flag m t s_tmp4 (Matita_freescale_byte8.mSB_b8 r_op)) in (let s_tmp6 = (Matita_freescale_status.setweak_v_flag m t s_tmp5 (fV (Matita_freescale_byte8.mSB_b8 m_op) (Matita_freescale_byte8.mSB_b8 r_op))) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp6,new_pc)))))))))
  89 ))))
  90 ))))))))))
  91 ;;
  92
  93 let execute_SBC_SUB_aux =
  94 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (function setflag -> (function fAMC -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
  95 (match s_M_PC with
  96    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let a_op = (Matita_freescale_status.get_acc_8_low_reg m t s_tmp1) in
  97 (match (fAMC a_op m_op (Matita_freescale_status.get_c_flag m t s_tmp1)) with
  98    Matita_datatypes_constructors.Pair(r_op,carry) -> (let a7 = (Matita_freescale_byte8.mSB_b8 a_op) in (let m7 = (Matita_freescale_byte8.mSB_b8 m_op) in (let r7 = (Matita_freescale_byte8.mSB_b8 r_op) in (let s_tmp2 =
  99 (match setflag with
 100    Matita_datatypes_bool.True -> (Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 r_op)
 101  | Matita_datatypes_bool.False -> s_tmp1)
 102  in (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp4 = (Matita_freescale_status.set_c_flag m t s_tmp3 (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool a7) m7) (Matita_freescale_extra.and_bool m7 r7)) (Matita_freescale_extra.and_bool r7 (Matita_freescale_extra.not_bool a7)))) in (let s_tmp5 = (Matita_freescale_status.setweak_n_flag m t s_tmp4 r7) in (let s_tmp6 = (Matita_freescale_status.setweak_v_flag m t s_tmp5 (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool a7 (Matita_freescale_extra.not_bool m7)) (Matita_freescale_extra.not_bool r7)) (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool a7) m7) r7))) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp6,new_pc)))))))))))))
 103 ))
 104 )))))))))
 105 ;;
 106
 107 let aux_push =
 108 (function m -> (function t -> (function s -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function sP_op -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.memory_filter_write m t s sP_op val_) (function s_tmp1 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_sp_reg m t s_tmp1 (Matita_freescale_word16.pred_w16 sP_op)) (function s_tmp2 -> (Matita_datatypes_constructors.Some(s_tmp2))))))))))))
 109 ;;
 110
 111 let aux_pop =
 112 (function m -> (function t -> (function s -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function sP_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_sp_reg m t s (Matita_freescale_word16.succ_w16 sP_op)) (function s_tmp1 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s_tmp1) (function sP_op' -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.memory_filter_read m t s_tmp1 sP_op') (function val_ -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,val_)))))))))))))))
 113 ;;
 114
 115 let aux_get_CCR =
 116 (function m -> (function t -> (function s -> (let v_comp =
 117 (match (Matita_freescale_status.get_v_flag m t s) with
 118    Matita_datatypes_constructors.None -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0))
 119  | Matita_datatypes_constructors.Some(v_val) ->
 120 (match v_val with
 121    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0))
 122  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 123 )
 124  in (let h_comp =
 125 (match (Matita_freescale_status.get_h_flag m t s) with
 126    Matita_datatypes_constructors.None -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 127  | Matita_datatypes_constructors.Some(h_val) ->
 128 (match h_val with
 129    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0))
 130  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 131 )
 132  in (let i_comp =
 133 (match (Matita_freescale_status.get_i_flag m t s) with
 134    Matita_datatypes_constructors.None -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 135  | Matita_datatypes_constructors.Some(i_val) ->
 136 (match i_val with
 137    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8))
 138  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 139 )
 140  in (let n_comp =
 141 (match (Matita_freescale_status.get_n_flag m t s) with
 142    Matita_datatypes_constructors.None -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 143  | Matita_datatypes_constructors.Some(n_val) ->
 144 (match n_val with
 145    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4))
 146  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 147 )
 148  in (let z_comp =
 149 (match (Matita_freescale_status.get_z_flag m t s) with
 150    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2))
 151  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 152  in (let c_comp =
 153 (match (Matita_freescale_status.get_c_flag m t s) with
 154    Matita_datatypes_bool.True -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1))
 155  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))
 156  in (Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X6,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.or_b8 v_comp (Matita_freescale_byte8.or_b8 h_comp (Matita_freescale_byte8.or_b8 i_comp (Matita_freescale_byte8.or_b8 n_comp (Matita_freescale_byte8.or_b8 z_comp c_comp)))))))))))))))
 157 ;;
 158
 159 let aux_set_CCR =
 160 (function m -> (function t -> (function s -> (function cCR -> (let s_tmp1 = (Matita_freescale_status.set_c_flag m t s (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)) (Matita_freescale_byte8.and_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)) cCR))) in (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)) (Matita_freescale_byte8.and_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X2)) cCR))) in (let s_tmp3 = (Matita_freescale_status.setweak_n_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)) (Matita_freescale_byte8.and_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X4)) cCR))) in (let s_tmp4 = (Matita_freescale_status.setweak_i_flag m t s_tmp3 (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)) (Matita_freescale_byte8.and_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X8)) cCR))) in (let s_tmp5 = (Matita_freescale_status.setweak_h_flag m t s_tmp4 (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.and_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.X0)) cCR))) in (let s_tmp6 = (Matita_freescale_status.setweak_v_flag m t s_tmp5 (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.and_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) cCR))) in s_tmp6))))))))))
 161 ;;
 162
 163 let execute_ADC =
 164 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ADC_ADD_aux m t s i cur_pc Matita_datatypes_bool.True (function a_op -> (function m_op -> (function c_op -> (Matita_freescale_byte8.plus_b8 a_op m_op c_op))))))))))
 165 ;;
 166
 167 let execute_ADD =
 168 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ADC_ADD_aux m t s i cur_pc Matita_datatypes_bool.True (function a_op -> (function m_op -> (function c_op -> (Matita_freescale_byte8.plus_b8 a_op m_op Matita_datatypes_bool.False))))))))))
 169 ;;
 170
 171 let execute_AIS =
 172 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 173 (match s_M_PC with
 174    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s_tmp1) (function sP_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_sp_reg m t s_tmp1 (Matita_freescale_word16.plus_w16nc sP_op (byte_extension m_op))) (function s_tmp2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,new_pc)))))))))
 175 )))))))
 176 ;;
 177
 178 let execute_AIX =
 179 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 180 (match s_M_PC with
 181    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s_tmp1) (function hX_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_16_reg m t s_tmp1 (Matita_freescale_word16.plus_w16nc hX_op (byte_extension m_op))) (function s_tmp2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,new_pc)))))))))
 182 )))))))
 183 ;;
 184
 185 let execute_AND =
 186 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_AND_BIT_EOR_ORA_aux m t s i cur_pc Matita_datatypes_bool.True Matita_freescale_byte8.and_b8))))))
 187 ;;
 188
 189 let execute_ASL =
 190 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (function m_op -> (function c_op -> (Matita_freescale_byte8.rcl_b8 m_op Matita_datatypes_bool.False)))))))))
 191 ;;
 192
 193 let execute_ASR =
 194 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (function m_op -> (function c_op -> (Matita_freescale_byte8.rcr_b8 m_op (Matita_freescale_byte8.mSB_b8 m_op))))))))))
 195 ;;
 196
 197 let execute_BCC =
 198 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool (Matita_freescale_status.get_c_flag m t s))))))))
 199 ;;
 200
 201 let execute_BCLRn =
 202 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_BCLRn_BSETn_aux m t s i cur_pc (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))))
 203 ;;
 204
 205 let execute_BCS =
 206 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_status.get_c_flag m t s)))))))
 207 ;;
 208
 209 let execute_BEQ =
 210 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_status.get_z_flag m t s)))))))
 211 ;;
 212
 213 let execute_BGE =
 214 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_n_flag m t s) (function n_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_v_flag m t s) (function v_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool (Matita_freescale_extra.xor_bool n_op v_op))))))))))))
 215 ;;
 216
 217 let execute_BGND =
 218 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s,cur_pc)))))))))
 219 ;;
 220
 221 let execute_BGT =
 222 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_n_flag m t s) (function n_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_v_flag m t s) (function v_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool (Matita_freescale_extra.or_bool (Matita_freescale_status.get_z_flag m t s) (Matita_freescale_extra.xor_bool n_op v_op)))))))))))))
 223 ;;
 224
 225 let execute_BHCC =
 226 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_h_flag m t s) (function h_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool h_op)))))))))
 227 ;;
 228
 229 let execute_BHCS =
 230 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_h_flag m t s) (function h_op -> (execute_any_BRANCH m t s i cur_pc h_op))))))))
 231 ;;
 232
 233 let execute_BHI =
 234 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool (Matita_freescale_extra.or_bool (Matita_freescale_status.get_c_flag m t s) (Matita_freescale_status.get_z_flag m t s)))))))))
 235 ;;
 236
 237 let execute_BIH =
 238 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_irq_flag m t s) (function iRQ_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool iRQ_op)))))))))
 239 ;;
 240
 241 let execute_BIL =
 242 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_irq_flag m t s) (function iRQ_op -> (execute_any_BRANCH m t s i cur_pc iRQ_op))))))))
 243 ;;
 244
 245 let execute_BIT =
 246 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_AND_BIT_EOR_ORA_aux m t s i cur_pc Matita_datatypes_bool.False Matita_freescale_byte8.and_b8))))))
 247 ;;
 248
 249 let execute_BLE =
 250 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_n_flag m t s) (function n_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_v_flag m t s) (function v_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.or_bool (Matita_freescale_status.get_z_flag m t s) (Matita_freescale_extra.xor_bool n_op v_op))))))))))))
 251 ;;
 252
 253 let execute_BLS =
 254 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.or_bool (Matita_freescale_status.get_c_flag m t s) (Matita_freescale_status.get_z_flag m t s))))))))
 255 ;;
 256
 257 let execute_BLT =
 258 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_n_flag m t s) (function n_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_v_flag m t s) (function v_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.xor_bool n_op v_op)))))))))))
 259 ;;
 260
 261 let execute_BMC =
 262 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_i_flag m t s) (function i_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool i_op)))))))))
 263 ;;
 264
 265 let execute_BMI =
 266 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_n_flag m t s) (function n_op -> (execute_any_BRANCH m t s i cur_pc n_op))))))))
 267 ;;
 268
 269 let execute_BMS =
 270 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_i_flag m t s) (function i_op -> (execute_any_BRANCH m t s i cur_pc i_op))))))))
 271 ;;
 272
 273 let execute_BNE =
 274 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool (Matita_freescale_status.get_z_flag m t s))))))))
 275 ;;
 276
 277 let execute_BPL =
 278 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_n_flag m t s) (function n_op -> (execute_any_BRANCH m t s i cur_pc (Matita_freescale_extra.not_bool n_op)))))))))
 279 ;;
 280
 281 let execute_BRA =
 282 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc Matita_datatypes_bool.True))))))
 283 ;;
 284
 285 let execute_BRCLRn =
 286 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_BRCLRn_BRSETn_aux m t s i cur_pc (function mn_op -> (Matita_freescale_byte8.eq_b8 mn_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))))))
 287 ;;
 288
 289 let execute_BRN =
 290 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_any_BRANCH m t s i cur_pc Matita_datatypes_bool.False))))))
 291 ;;
 292
 293 let execute_BRSETn =
 294 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_BRCLRn_BRSETn_aux m t s i cur_pc (function mn_op -> (Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 mn_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))))))
 295 ;;
 296
 297 let execute_BSETn =
 298 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_BCLRn_BSETn_aux m t s i cur_pc (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))))))
 299 ;;
 300
 301 let execute_BSR =
 302 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 303 (match s_M_PC with
 304    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let aux = (Matita_freescale_extra.opt_map (aux_push m t s_tmp1 (Matita_freescale_word16.w16l new_pc)) (function s_tmp2 -> (Matita_freescale_extra.opt_map (aux_push m t s_tmp2 (Matita_freescale_word16.w16h new_pc)) (function s_tmp3 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp3,(branched_pc m t s_tmp3 new_pc m_op))))))))) in
 305 (match m with
 306    Matita_freescale_opcode.HC05 -> aux
 307  | Matita_freescale_opcode.HC08 -> aux
 308  | Matita_freescale_opcode.HCS08 -> aux
 309  | Matita_freescale_opcode.RS08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_spc_reg m t s_tmp1 new_pc) (function s_tmp2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,(branched_pc m t s_tmp2 new_pc m_op))))))))
 310 ))
 311 )))))))
 312 ;;
 313
 314 let execute_CBEQA =
 315 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
 316 (match s_M_PC with
 317    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) ->
 318 (match m_op with
 319    Matita_freescale_word16.Mk_word16(mH_op,mL_op) ->
 320 (match (Matita_freescale_byte8.eq_b8 (Matita_freescale_status.get_acc_8_low_reg m t s_tmp1) mH_op) with
 321    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,(branched_pc m t s_tmp1 new_pc mL_op)))))
 322  | Matita_datatypes_bool.False -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,new_pc)))))
 323 )
 324 )
 325 )))))))
 326 ;;
 327
 328 let execute_CBEQX =
 329 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
 330 (match s_M_PC with
 331    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) ->
 332 (match m_op with
 333    Matita_freescale_word16.Mk_word16(mH_op,mL_op) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s_tmp1) (function x_op ->
 334 (match (Matita_freescale_byte8.eq_b8 x_op mH_op) with
 335    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,(branched_pc m t s_tmp1 new_pc mL_op)))))
 336  | Matita_datatypes_bool.False -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,new_pc)))))
 337 )))
 338 )
 339 )))))))
 340 ;;
 341
 342 let execute_CLC =
 343 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_c_flag m t s Matita_datatypes_bool.False),cur_pc)))))))))
 344 ;;
 345
 346 let execute_CLI =
 347 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_i_flag m t s Matita_datatypes_bool.False) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp,cur_pc)))))))))))
 348 ;;
 349
 350 let execute_CLR =
 351 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s cur_pc i (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) (function s_PC ->
 352 (match s_PC with
 353    Matita_datatypes_constructors.Pair(s_tmp1,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 Matita_datatypes_bool.True) in (let s_tmp3 = (Matita_freescale_status.setweak_n_flag m t s_tmp2 Matita_datatypes_bool.False) in (let s_tmp4 = (Matita_freescale_status.setweak_v_flag m t s_tmp3 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp4,new_pc))))))))
 354 )))))))
 355 ;;
 356
 357 let execute_CMP =
 358 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_SBC_SUB_aux m t s i cur_pc Matita_datatypes_bool.False (function a_op -> (function m_op -> (function c_op -> (Matita_freescale_byte8.plus_b8 a_op (Matita_freescale_byte8.compl_b8 m_op) Matita_datatypes_bool.False))))))))))
 359 ;;
 360
 361 let execute_COM =
 362 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_COM_DEC_INC_NEG_aux m t s i cur_pc Matita_freescale_byte8.not_b8 (function m7 -> (function r7 -> Matita_datatypes_bool.False)) (function c_op -> (function r_op -> Matita_datatypes_bool.True))))))))
 363 ;;
 364
 365 let execute_CPHX =
 366 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
 367 (match s_M_PC with
 368    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s_tmp1) (function x_op ->
 369 (match (Matita_freescale_word16.plus_w16 x_op (Matita_freescale_word16.compl_w16 m_op) Matita_datatypes_bool.False) with
 370    Matita_datatypes_constructors.Pair(r_op,carry) -> (let x15 = (Matita_freescale_word16.mSB_w16 x_op) in (let m15 = (Matita_freescale_word16.mSB_w16 m_op) in (let r15 = (Matita_freescale_word16.mSB_w16 r_op) in (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_word16.eq_w16 r_op (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.X0)))))) in (let s_tmp3 = (Matita_freescale_status.set_c_flag m t s_tmp2 (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool x15) m15) (Matita_freescale_extra.and_bool m15 r15)) (Matita_freescale_extra.and_bool r15 (Matita_freescale_extra.not_bool x15)))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 r15) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool x15 (Matita_freescale_extra.not_bool m15)) (Matita_freescale_extra.not_bool r15)) (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool x15) m15) r15))) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc))))))))))))
 371 )))
 372 )))))))
 373 ;;
 374
 375 let execute_CPX =
 376 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 377 (match s_M_PC with
 378    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s_tmp1) (function x_op ->
 379 (match (Matita_freescale_byte8.plus_b8 x_op (Matita_freescale_byte8.compl_b8 m_op) Matita_datatypes_bool.False) with
 380    Matita_datatypes_constructors.Pair(r_op,carry) -> (let x7 = (Matita_freescale_byte8.mSB_b8 x_op) in (let m7 = (Matita_freescale_byte8.mSB_b8 m_op) in (let r7 = (Matita_freescale_byte8.mSB_b8 r_op) in (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp3 = (Matita_freescale_status.set_c_flag m t s_tmp2 (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool x7) m7) (Matita_freescale_extra.and_bool m7 r7)) (Matita_freescale_extra.and_bool r7 (Matita_freescale_extra.not_bool x7)))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 r7) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 (Matita_freescale_extra.or_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool x7 (Matita_freescale_extra.not_bool m7)) (Matita_freescale_extra.not_bool r7)) (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool x7) m7) r7))) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc))))))))))))
 381 )))
 382 )))))))
 383 ;;
 384
 385 let execute_DAA =
 386 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_h_flag m t s) (function h -> (let m_op = (Matita_freescale_status.get_acc_8_low_reg m t s) in
 387 (match (Matita_freescale_byte8.daa_b8 h (Matita_freescale_status.get_c_flag m t s) m_op) with
 388    Matita_datatypes_constructors.Pair(r_op,carry) -> (let s_tmp1 = (Matita_freescale_status.set_acc_8_low_reg m t s r_op) in (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp3 = (Matita_freescale_status.set_c_flag m t s_tmp2 carry) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 (Matita_freescale_byte8.mSB_b8 r_op)) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 (Matita_freescale_extra.xor_bool (Matita_freescale_byte8.mSB_b8 m_op) (Matita_freescale_byte8.mSB_b8 r_op))) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,cur_pc))))))))))
 389 ))))))))
 390 ;;
 391
 392 let execute_DBNZ =
 393 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
 394 (match s_M_PC with
 395    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) ->
 396 (match m_op with
 397    Matita_freescale_word16.Mk_word16(mH_op,mL_op) -> (let mH_op' = (Matita_freescale_byte8.pred_b8 mH_op) in (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s_tmp1 cur_pc i mH_op') (function s_PC ->
 398 (match s_PC with
 399    Matita_datatypes_constructors.Pair(s_tmp2,_) ->
 400 (match (Matita_freescale_byte8.eq_b8 mH_op' (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with
 401    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,new_pc))))
 402  | Matita_datatypes_bool.False -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,(branched_pc m t s_tmp2 new_pc mL_op))))))
 403 )
 404 ))))
 405 )
 406 )))))))
 407 ;;
 408
 409 let execute_DEC =
 410 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_COM_DEC_INC_NEG_aux m t s i cur_pc Matita_freescale_byte8.pred_b8 (function m7 -> (function r7 -> (Matita_freescale_extra.and_bool m7 (Matita_freescale_extra.not_bool r7)))) (function c_op -> (function r_op -> c_op))))))))
 411 ;;
 412
 413 let execute_DIV =
 414 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_high_reg m t s) (function h_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function x_op ->
 415 (match (Matita_freescale_word16.div_b8 (Matita_freescale_word16.Mk_word16(h_op,(Matita_freescale_status.get_acc_8_low_reg m t s))) x_op) with
 416    Matita_freescale_extra.TripleT(quoz,rest,overflow) -> (let s_tmp1 = (Matita_freescale_status.set_c_flag m t s overflow) in (let s_tmp2 =
 417 (match overflow with
 418    Matita_datatypes_bool.True -> s_tmp1
 419  | Matita_datatypes_bool.False -> (Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 quoz))
 420  in (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 (Matita_freescale_status.get_acc_8_low_reg m t s_tmp2) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (Matita_freescale_extra.opt_map
 421 (match overflow with
 422    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(s_tmp3))
 423  | Matita_datatypes_bool.False -> (Matita_freescale_status.set_indX_8_high_reg m t s_tmp3 rest))
 424  (function s_tmp4 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp4,cur_pc))))))))))
 425 )))))))))
 426 ;;
 427
 428 let execute_EOR =
 429 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_AND_BIT_EOR_ORA_aux m t s i cur_pc Matita_datatypes_bool.True Matita_freescale_byte8.xor_b8))))))
 430 ;;
 431
 432 let execute_INC =
 433 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_COM_DEC_INC_NEG_aux m t s i cur_pc Matita_freescale_byte8.succ_b8 (function m7 -> (function r7 -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.not_bool m7) r7))) (function c_op -> (function r_op -> c_op))))))))
 434 ;;
 435
 436 let execute_JMP =
 437 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_extra.fst3T s_M_PC),(Matita_freescale_extra.snd3T s_M_PC))))))))))))
 438 ;;
 439
 440 let execute_JSR =
 441 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
 442 (match s_M_PC with
 443    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let aux = (Matita_freescale_extra.opt_map (aux_push m t s_tmp1 (Matita_freescale_word16.w16l new_pc)) (function s_tmp2 -> (Matita_freescale_extra.opt_map (aux_push m t s_tmp2 (Matita_freescale_word16.w16h new_pc)) (function s_tmp3 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp3,m_op)))))))) in
 444 (match m with
 445    Matita_freescale_opcode.HC05 -> aux
 446  | Matita_freescale_opcode.HC08 -> aux
 447  | Matita_freescale_opcode.HCS08 -> aux
 448  | Matita_freescale_opcode.RS08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_spc_reg m t s_tmp1 new_pc) (function s_tmp2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,m_op)))))))
 449 ))
 450 )))))))
 451 ;;
 452
 453 let execute_LDA =
 454 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 455 (match s_M_PC with
 456    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 m_op) in (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 m_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 (Matita_freescale_byte8.mSB_b8 m_op)) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc)))))))))
 457 )))))))
 458 ;;
 459
 460 let execute_LDHX =
 461 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.False m t s cur_pc i) (function s_M_PC ->
 462 (match s_M_PC with
 463    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_16_reg m t s_tmp1 m_op) (function s_tmp2 -> (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_word16.eq_w16 m_op (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.X0)))))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 (Matita_freescale_word16.mSB_w16 m_op)) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc))))))))))
 464 )))))))
 465 ;;
 466
 467 let execute_LDX =
 468 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 469 (match s_M_PC with
 470    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s_tmp1 m_op) (function s_tmp2 -> (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 m_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 (Matita_freescale_byte8.mSB_b8 m_op)) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc))))))))))
 471 )))))))
 472 ;;
 473
 474 let execute_LSR =
 475 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (function m_op -> (function c_op -> (Matita_freescale_byte8.rcr_b8 m_op Matita_datatypes_bool.False)))))))))
 476 ;;
 477
 478 let execute_MOV =
 479 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_R_PC ->
 480 (match s_R_PC with
 481    Matita_freescale_extra.TripleT(s_tmp1,r_op,tmp_pc) -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s_tmp1 tmp_pc i r_op) (function s_PC ->
 482 (match s_PC with
 483    Matita_datatypes_constructors.Pair(s_tmp2,new_pc) -> (let s_tmp3 = (Matita_freescale_status.set_z_flag m t s_tmp2 (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp4 = (Matita_freescale_status.setweak_n_flag m t s_tmp3 (Matita_freescale_byte8.mSB_b8 r_op)) in (let s_tmp5 = (Matita_freescale_status.setweak_v_flag m t s_tmp4 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp5,new_pc))))))))
 484 )))
 485 )))))))
 486 ;;
 487
 488 let execute_MUL =
 489 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function x_op -> (let r_op = (Matita_freescale_word16.mul_b8 x_op (Matita_freescale_status.get_acc_8_low_reg m t s)) in (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s (Matita_freescale_word16.w16h r_op)) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s_tmp (Matita_freescale_word16.w16l r_op)),cur_pc))))))))))))))
 490 ;;
 491
 492 let execute_NEG =
 493 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_COM_DEC_INC_NEG_aux m t s i cur_pc Matita_freescale_byte8.compl_b8 (function m7 -> (function r7 -> (Matita_freescale_extra.and_bool m7 r7))) (function c_op -> (function r_op -> (Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 r_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))))))))
 494 ;;
 495
 496 let execute_NOP =
 497 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s,cur_pc)))))))))
 498 ;;
 499
 500 let execute_NSA =
 501 (function m -> (function t -> (function s -> (function i -> (function cur_pc ->
 502 (match (Matita_freescale_status.get_acc_8_low_reg m t s) with
 503    Matita_freescale_byte8.Mk_byte8(ah,al) -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s (Matita_freescale_byte8.Mk_byte8(al,ah))),cur_pc)))))
 504 )))))
 505 ;;
 506
 507 let execute_ORA =
 508 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_AND_BIT_EOR_ORA_aux m t s i cur_pc Matita_datatypes_bool.True Matita_freescale_byte8.or_b8))))))
 509 ;;
 510
 511 let execute_PSHA =
 512 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (aux_push m t s (Matita_freescale_status.get_acc_8_low_reg m t s)) (function s_tmp1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,cur_pc)))))))))))
 513 ;;
 514
 515 let execute_PSHH =
 516 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_high_reg m t s) (function h_op -> (Matita_freescale_extra.opt_map (aux_push m t s h_op) (function s_tmp1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,cur_pc)))))))))))))
 517 ;;
 518
 519 let execute_PSHX =
 520 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function h_op -> (Matita_freescale_extra.opt_map (aux_push m t s h_op) (function s_tmp1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp1,cur_pc)))))))))))))
 521 ;;
 522
 523 let execute_PULA =
 524 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (aux_pop m t s) (function s_and_A ->
 525 (match s_and_A with
 526    Matita_datatypes_constructors.Pair(s_tmp1,a_op) -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 a_op),cur_pc)))))
 527 )))))))
 528 ;;
 529
 530 let execute_PULH =
 531 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (aux_pop m t s) (function s_and_H ->
 532 (match s_and_H with
 533    Matita_datatypes_constructors.Pair(s_tmp1,h_op) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_high_reg m t s_tmp1 h_op) (function s_tmp2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,cur_pc)))))))
 534 )))))))
 535 ;;
 536
 537 let execute_PULX =
 538 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (aux_pop m t s) (function s_and_X ->
 539 (match s_and_X with
 540    Matita_datatypes_constructors.Pair(s_tmp1,x_op) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s_tmp1 x_op) (function s_tmp2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,cur_pc)))))))
 541 )))))))
 542 ;;
 543
 544 let execute_ROL =
 545 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (function m_op -> (function c_op -> (Matita_freescale_byte8.rcl_b8 m_op c_op)))))))))
 546 ;;
 547
 548 let execute_ROR =
 549 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (function m_op -> (function c_op -> (Matita_freescale_byte8.rcr_b8 m_op c_op)))))))))
 550 ;;
 551
 552 let execute_RSP =
 553 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function sP_op ->
 554 (match sP_op with
 555    Matita_freescale_word16.Mk_word16(sph,spl) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_sp_reg m t s (Matita_freescale_word16.Mk_word16(sph,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp,cur_pc)))))))
 556 )))))))
 557 ;;
 558
 559 let execute_RTI =
 560 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (aux_pop m t s) (function s_and_CCR ->
 561 (match s_and_CCR with
 562    Matita_datatypes_constructors.Pair(s_tmp1,cCR_op) -> (let s_tmp2 = (aux_set_CCR m t s_tmp1 cCR_op) in (Matita_freescale_extra.opt_map (aux_pop m t s_tmp2) (function s_and_A ->
 563 (match s_and_A with
 564    Matita_datatypes_constructors.Pair(s_tmp3,a_op) -> (let s_tmp4 = (Matita_freescale_status.set_acc_8_low_reg m t s_tmp3 a_op) in (Matita_freescale_extra.opt_map (aux_pop m t s_tmp4) (function s_and_X ->
 565 (match s_and_X with
 566    Matita_datatypes_constructors.Pair(s_tmp5,x_op) -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s_tmp5 x_op) (function s_tmp6 -> (Matita_freescale_extra.opt_map (aux_pop m t s_tmp6) (function s_and_PCH ->
 567 (match s_and_PCH with
 568    Matita_datatypes_constructors.Pair(s_tmp7,pCH_op) -> (Matita_freescale_extra.opt_map (aux_pop m t s_tmp7) (function s_and_PCL ->
 569 (match s_and_PCL with
 570    Matita_datatypes_constructors.Pair(s_tmp8,pCL_op) -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp8,(Matita_freescale_word16.Mk_word16(pCH_op,pCL_op)))))))
 571 )))
 572 )))))
 573 ))))
 574 ))))
 575 )))))))
 576 ;;
 577
 578 let execute_RTS =
 579 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (let aux = (Matita_freescale_extra.opt_map (aux_pop m t s) (function s_and_PCH ->
 580 (match s_and_PCH with
 581    Matita_datatypes_constructors.Pair(s_tmp1,pCH_op) -> (Matita_freescale_extra.opt_map (aux_pop m t s_tmp1) (function s_and_PCL ->
 582 (match s_and_PCL with
 583    Matita_datatypes_constructors.Pair(s_tmp2,pCL_op) -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp2,(Matita_freescale_word16.Mk_word16(pCH_op,pCL_op)))))))
 584 )))
 585 )) in
 586 (match m with
 587    Matita_freescale_opcode.HC05 -> aux
 588  | Matita_freescale_opcode.HC08 -> aux
 589  | Matita_freescale_opcode.HCS08 -> aux
 590  | Matita_freescale_opcode.RS08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_spc_reg m t s) (function sPC_op -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s,sPC_op)))))))
 591 ))))))
 592 ;;
 593
 594 let execute_SBC =
 595 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_SBC_SUB_aux m t s i cur_pc Matita_datatypes_bool.True (function a_op -> (function m_op -> (function c_op ->
 596 (match (Matita_freescale_byte8.plus_b8 a_op (Matita_freescale_byte8.compl_b8 m_op) Matita_datatypes_bool.False) with
 597    Matita_datatypes_constructors.Pair(resb,resc) ->
 598 (match c_op with
 599    Matita_datatypes_bool.True -> (Matita_freescale_byte8.plus_b8 resb (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)) Matita_datatypes_bool.False)
 600  | Matita_datatypes_bool.False -> (Matita_datatypes_constructors.Pair(resb,resc)))
 601 )
 602 )))))))))
 603 ;;
 604
 605 let execute_SEC =
 606 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_c_flag m t s Matita_datatypes_bool.True),cur_pc)))))))))
 607 ;;
 608
 609 let execute_SEI =
 610 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_i_flag m t s Matita_datatypes_bool.True) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp,cur_pc)))))))))))
 611 ;;
 612
 613 let execute_SHA =
 614 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_spc_reg m t s) (function sPC_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_spc_reg m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_status.get_acc_8_low_reg m t s),(Matita_freescale_word16.w16l sPC_op)))) (function s_tmp1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 (Matita_freescale_word16.w16h sPC_op)),cur_pc)))))))))))))
 615 ;;
 616
 617 let execute_SLA =
 618 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_spc_reg m t s) (function sPC_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_spc_reg m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_word16.w16h sPC_op),(Matita_freescale_status.get_acc_8_low_reg m t s)))) (function s_tmp1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s_tmp1 (Matita_freescale_word16.w16l sPC_op)),cur_pc)))))))))))))
 619 ;;
 620
 621 let execute_STA =
 622 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (let a_op = (Matita_freescale_status.get_acc_8_low_reg m t s) in (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s cur_pc i a_op) (function s_op_and_PC ->
 623 (match s_op_and_PC with
 624    Matita_datatypes_constructors.Pair(s_tmp1,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_byte8.eq_b8 a_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp3 = (Matita_freescale_status.setweak_n_flag m t s_tmp2 (Matita_freescale_byte8.mSB_b8 a_op)) in (let s_tmp4 = (Matita_freescale_status.setweak_v_flag m t s_tmp3 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp4,new_pc))))))))
 625 ))))))))
 626 ;;
 627
 628 let execute_STHX =
 629 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (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_load_write.multi_mode_write Matita_datatypes_bool.False m t s cur_pc i x_op) (function s_op_and_PC ->
 630 (match s_op_and_PC with
 631    Matita_datatypes_constructors.Pair(s_tmp1,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_word16.eq_w16 x_op (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.X0)))))) in (let s_tmp3 = (Matita_freescale_status.setweak_n_flag m t s_tmp2 (Matita_freescale_word16.mSB_w16 x_op)) in (let s_tmp4 = (Matita_freescale_status.setweak_v_flag m t s_tmp3 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp4,new_pc))))))))
 632 )))))))))
 633 ;;
 634
 635 let execute_STOP =
 636 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.setweak_i_flag m t s Matita_datatypes_bool.False),cur_pc)))))))))
 637 ;;
 638
 639 let execute_STX =
 640 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function x_op -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_write Matita_datatypes_bool.True m t s cur_pc i x_op) (function s_op_and_PC ->
 641 (match s_op_and_PC with
 642    Matita_datatypes_constructors.Pair(s_tmp1,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_byte8.eq_b8 x_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp3 = (Matita_freescale_status.setweak_n_flag m t s_tmp2 (Matita_freescale_byte8.mSB_b8 x_op)) in (let s_tmp4 = (Matita_freescale_status.setweak_v_flag m t s_tmp3 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp4,new_pc))))))))
 643 )))))))))
 644 ;;
 645
 646 let execute_SUB =
 647 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (execute_SBC_SUB_aux m t s i cur_pc Matita_datatypes_bool.True (function a_op -> (function m_op -> (function c_op -> (Matita_freescale_byte8.plus_b8 a_op (Matita_freescale_byte8.compl_b8 m_op) Matita_datatypes_bool.False))))))))))
 648 ;;
 649
 650 let execute_SWI =
 651 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (let vector = (Matita_freescale_status.get_pc_reg m t (Matita_freescale_status.set_pc_reg m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XC)))))) in (Matita_freescale_extra.opt_map (aux_push m t s (Matita_freescale_word16.w16l cur_pc)) (function s_tmp1 -> (Matita_freescale_extra.opt_map (aux_push m t s_tmp1 (Matita_freescale_word16.w16h cur_pc)) (function s_tmp2 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s_tmp2) (function x_op -> (Matita_freescale_extra.opt_map (aux_push m t s_tmp2 x_op) (function s_tmp3 -> (Matita_freescale_extra.opt_map (aux_push m t s_tmp3 (Matita_freescale_status.get_acc_8_low_reg m t s_tmp3)) (function s_tmp4 -> (Matita_freescale_extra.opt_map (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4)) (function s_tmp5 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_i_flag m t s_tmp5 Matita_datatypes_bool.True) (function s_tmp6 -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.memory_filter_read m t s_tmp6 vector) (function addrh -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.memory_filter_read m t s_tmp6 (Matita_freescale_word16.succ_w16 vector)) (function addrl -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp6,(Matita_freescale_word16.Mk_word16(addrh,addrl))))))))))))))))))))))))))))))
 652 ;;
 653
 654 let execute_TAP =
 655 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((aux_set_CCR m t s (Matita_freescale_status.get_acc_8_low_reg m t s)),cur_pc)))))))))
 656 ;;
 657
 658 let execute_TAX =
 659 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s (Matita_freescale_status.get_acc_8_low_reg m t s)) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp,cur_pc)))))))))))
 660 ;;
 661
 662 let execute_TPA =
 663 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s (aux_get_CCR m t s)),cur_pc)))))))))
 664 ;;
 665
 666 let execute_TST =
 667 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_load_write.multi_mode_load Matita_datatypes_bool.True m t s cur_pc i) (function s_M_PC ->
 668 (match s_M_PC with
 669    Matita_freescale_extra.TripleT(s_tmp1,m_op,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_z_flag m t s_tmp1 (Matita_freescale_byte8.eq_b8 m_op (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) in (let s_tmp3 = (Matita_freescale_status.setweak_n_flag m t s_tmp2 (Matita_freescale_byte8.mSB_b8 m_op)) in (let s_tmp4 = (Matita_freescale_status.setweak_v_flag m t s_tmp3 Matita_datatypes_bool.False) in (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp4,new_pc))))))))
 670 )))))))
 671 ;;
 672
 673 let execute_TSX =
 674 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function sP_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_16_reg m t s (Matita_freescale_word16.succ_w16 sP_op)) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp,cur_pc)))))))))))))
 675 ;;
 676
 677 let execute_TXA =
 678 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function x_op -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s x_op),cur_pc)))))))))))
 679 ;;
 680
 681 let execute_TXS =
 682 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (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_sp_reg m t s (Matita_freescale_word16.pred_w16 x_op)) (function s_tmp -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_tmp,cur_pc)))))))))))))
 683 ;;
 684
 685 let execute_WAIT =
 686 (function m -> (function t -> (function s -> (function i -> (function cur_pc -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.setweak_i_flag m t s Matita_datatypes_bool.False),cur_pc)))))))))
 687 ;;
 688
 689 type susp_type =
 690 BGND_MODE
 691  | STOP_MODE
 692  | WAIT_MODE
 693 ;;
 694
 695 let susp_type_rec =
 696 (function p -> (function p1 -> (function p2 -> (function s ->
 697 (match s with
 698    BGND_MODE -> p
 699  | STOP_MODE -> p1
 700  | WAIT_MODE -> p2)
 701 ))))
 702 ;;
 703
 704 let susp_type_rect =
 705 (function p -> (function p1 -> (function p2 -> (function s ->
 706 (match s with
 707    BGND_MODE -> p
 708  | STOP_MODE -> p1
 709  | WAIT_MODE -> p2)
 710 ))))
 711 ;;
 712
 713 type ('a) tick_result =
 714 TickERR of 'a * Matita_freescale_load_write.error_type
 715  | TickSUSP of 'a * susp_type
 716  | TickOK of 'a
 717 ;;
 718
 719 let tick_result_rec =
 720 (function f -> (function f1 -> (function f2 -> (function t ->
 721 (match t with
 722    TickERR(t1,e) -> (f t1 e)
 723  | TickSUSP(t1,s) -> (f1 t1 s)
 724  | TickOK(t1) -> (f2 t1))
 725 ))))
 726 ;;
 727
 728 let tick_result_rect =
 729 (function f -> (function f1 -> (function f2 -> (function t ->
 730 (match t with
 731    TickERR(t1,e) -> (f t1 e)
 732  | TickSUSP(t1,s) -> (f1 t1 s)
 733  | TickOK(t1) -> (f2 t1))
 734 ))))
 735 ;;
 736
 737 let tick_execute =
 738 (function m -> (function t -> (function s -> (function pseudo -> (function mode -> (function cur_pc -> (let abs_pseudo =
 739 (match pseudo with
 740    Matita_freescale_opcode.AnyOP(pseudo') -> pseudo')
 741  in (let a_status_and_fetch =
 742 (match abs_pseudo with
 743    Matita_freescale_opcode.ADC -> (execute_ADC m t s mode cur_pc)
 744  | Matita_freescale_opcode.ADD -> (execute_ADD m t s mode cur_pc)
 745  | Matita_freescale_opcode.AIS -> (execute_AIS m t s mode cur_pc)
 746  | Matita_freescale_opcode.AIX -> (execute_AIX m t s mode cur_pc)
 747  | Matita_freescale_opcode.AND -> (execute_AND m t s mode cur_pc)
 748  | Matita_freescale_opcode.ASL -> (execute_ASL m t s mode cur_pc)
 749  | Matita_freescale_opcode.ASR -> (execute_ASR m t s mode cur_pc)
 750  | Matita_freescale_opcode.BCC -> (execute_BCC m t s mode cur_pc)
 751  | Matita_freescale_opcode.BCLRn -> (execute_BCLRn m t s mode cur_pc)
 752  | Matita_freescale_opcode.BCS -> (execute_BCS m t s mode cur_pc)
 753  | Matita_freescale_opcode.BEQ -> (execute_BEQ m t s mode cur_pc)
 754  | Matita_freescale_opcode.BGE -> (execute_BGE m t s mode cur_pc)
 755  | Matita_freescale_opcode.BGND -> (execute_BGND m t s mode cur_pc)
 756  | Matita_freescale_opcode.BGT -> (execute_BGT m t s mode cur_pc)
 757  | Matita_freescale_opcode.BHCC -> (execute_BHCC m t s mode cur_pc)
 758  | Matita_freescale_opcode.BHCS -> (execute_BHCS m t s mode cur_pc)
 759  | Matita_freescale_opcode.BHI -> (execute_BHI m t s mode cur_pc)
 760  | Matita_freescale_opcode.BIH -> (execute_BIH m t s mode cur_pc)
 761  | Matita_freescale_opcode.BIL -> (execute_BIL m t s mode cur_pc)
 762  | Matita_freescale_opcode.BIT -> (execute_BIT m t s mode cur_pc)
 763  | Matita_freescale_opcode.BLE -> (execute_BLE m t s mode cur_pc)
 764  | Matita_freescale_opcode.BLS -> (execute_BLS m t s mode cur_pc)
 765  | Matita_freescale_opcode.BLT -> (execute_BLT m t s mode cur_pc)
 766  | Matita_freescale_opcode.BMC -> (execute_BMC m t s mode cur_pc)
 767  | Matita_freescale_opcode.BMI -> (execute_BMI m t s mode cur_pc)
 768  | Matita_freescale_opcode.BMS -> (execute_BMS m t s mode cur_pc)
 769  | Matita_freescale_opcode.BNE -> (execute_BNE m t s mode cur_pc)
 770  | Matita_freescale_opcode.BPL -> (execute_BPL m t s mode cur_pc)
 771  | Matita_freescale_opcode.BRA -> (execute_BRA m t s mode cur_pc)
 772  | Matita_freescale_opcode.BRCLRn -> (execute_BRCLRn m t s mode cur_pc)
 773  | Matita_freescale_opcode.BRN -> (execute_BRN m t s mode cur_pc)
 774  | Matita_freescale_opcode.BRSETn -> (execute_BRSETn m t s mode cur_pc)
 775  | Matita_freescale_opcode.BSETn -> (execute_BSETn m t s mode cur_pc)
 776  | Matita_freescale_opcode.BSR -> (execute_BSR m t s mode cur_pc)
 777  | Matita_freescale_opcode.CBEQA -> (execute_CBEQA m t s mode cur_pc)
 778  | Matita_freescale_opcode.CBEQX -> (execute_CBEQX m t s mode cur_pc)
 779  | Matita_freescale_opcode.CLC -> (execute_CLC m t s mode cur_pc)
 780  | Matita_freescale_opcode.CLI -> (execute_CLI m t s mode cur_pc)
 781  | Matita_freescale_opcode.CLR -> (execute_CLR m t s mode cur_pc)
 782  | Matita_freescale_opcode.CMP -> (execute_CMP m t s mode cur_pc)
 783  | Matita_freescale_opcode.COM -> (execute_COM m t s mode cur_pc)
 784  | Matita_freescale_opcode.CPHX -> (execute_CPHX m t s mode cur_pc)
 785  | Matita_freescale_opcode.CPX -> (execute_CPX m t s mode cur_pc)
 786  | Matita_freescale_opcode.DAA -> (execute_DAA m t s mode cur_pc)
 787  | Matita_freescale_opcode.DBNZ -> (execute_DBNZ m t s mode cur_pc)
 788  | Matita_freescale_opcode.DEC -> (execute_DEC m t s mode cur_pc)
 789  | Matita_freescale_opcode.DIV -> (execute_DIV m t s mode cur_pc)
 790  | Matita_freescale_opcode.EOR -> (execute_EOR m t s mode cur_pc)
 791  | Matita_freescale_opcode.INC -> (execute_INC m t s mode cur_pc)
 792  | Matita_freescale_opcode.JMP -> (execute_JMP m t s mode cur_pc)
 793  | Matita_freescale_opcode.JSR -> (execute_JSR m t s mode cur_pc)
 794  | Matita_freescale_opcode.LDA -> (execute_LDA m t s mode cur_pc)
 795  | Matita_freescale_opcode.LDHX -> (execute_LDHX m t s mode cur_pc)
 796  | Matita_freescale_opcode.LDX -> (execute_LDX m t s mode cur_pc)
 797  | Matita_freescale_opcode.LSR -> (execute_LSR m t s mode cur_pc)
 798  | Matita_freescale_opcode.MOV -> (execute_MOV m t s mode cur_pc)
 799  | Matita_freescale_opcode.MUL -> (execute_MUL m t s mode cur_pc)
 800  | Matita_freescale_opcode.NEG -> (execute_NEG m t s mode cur_pc)
 801  | Matita_freescale_opcode.NOP -> (execute_NOP m t s mode cur_pc)
 802  | Matita_freescale_opcode.NSA -> (execute_NSA m t s mode cur_pc)
 803  | Matita_freescale_opcode.ORA -> (execute_ORA m t s mode cur_pc)
 804  | Matita_freescale_opcode.PSHA -> (execute_PSHA m t s mode cur_pc)
 805  | Matita_freescale_opcode.PSHH -> (execute_PSHH m t s mode cur_pc)
 806  | Matita_freescale_opcode.PSHX -> (execute_PSHX m t s mode cur_pc)
 807  | Matita_freescale_opcode.PULA -> (execute_PULA m t s mode cur_pc)
 808  | Matita_freescale_opcode.PULH -> (execute_PULH m t s mode cur_pc)
 809  | Matita_freescale_opcode.PULX -> (execute_PULX m t s mode cur_pc)
 810  | Matita_freescale_opcode.ROL -> (execute_ROL m t s mode cur_pc)
 811  | Matita_freescale_opcode.ROR -> (execute_ROR m t s mode cur_pc)
 812  | Matita_freescale_opcode.RSP -> (execute_RSP m t s mode cur_pc)
 813  | Matita_freescale_opcode.RTI -> (execute_RTI m t s mode cur_pc)
 814  | Matita_freescale_opcode.RTS -> (execute_RTS m t s mode cur_pc)
 815  | Matita_freescale_opcode.SBC -> (execute_SBC m t s mode cur_pc)
 816  | Matita_freescale_opcode.SEC -> (execute_SEC m t s mode cur_pc)
 817  | Matita_freescale_opcode.SEI -> (execute_SEI m t s mode cur_pc)
 818  | Matita_freescale_opcode.SHA -> (execute_SHA m t s mode cur_pc)
 819  | Matita_freescale_opcode.SLA -> (execute_SLA m t s mode cur_pc)
 820  | Matita_freescale_opcode.STA -> (execute_STA m t s mode cur_pc)
 821  | Matita_freescale_opcode.STHX -> (execute_STHX m t s mode cur_pc)
 822  | Matita_freescale_opcode.STOP -> (execute_STOP m t s mode cur_pc)
 823  | Matita_freescale_opcode.STX -> (execute_STX m t s mode cur_pc)
 824  | Matita_freescale_opcode.SUB -> (execute_SUB m t s mode cur_pc)
 825  | Matita_freescale_opcode.SWI -> (execute_SWI m t s mode cur_pc)
 826  | Matita_freescale_opcode.TAP -> (execute_TAP m t s mode cur_pc)
 827  | Matita_freescale_opcode.TAX -> (execute_TAX m t s mode cur_pc)
 828  | Matita_freescale_opcode.TPA -> (execute_TPA m t s mode cur_pc)
 829  | Matita_freescale_opcode.TST -> (execute_TST m t s mode cur_pc)
 830  | Matita_freescale_opcode.TSX -> (execute_TSX m t s mode cur_pc)
 831  | Matita_freescale_opcode.TXA -> (execute_TXA m t s mode cur_pc)
 832  | Matita_freescale_opcode.TXS -> (execute_TXS m t s mode cur_pc)
 833  | Matita_freescale_opcode.WAIT -> (execute_WAIT m t s mode cur_pc))
 834  in
 835 (match a_status_and_fetch with
 836    Matita_datatypes_constructors.None -> (TickERR((Matita_freescale_status.set_clk_desc m t s (Matita_datatypes_constructors.None)),Matita_freescale_load_write.ILL_EX_AD))
 837  | Matita_datatypes_constructors.Some(status_and_newpc) ->
 838 (match status_and_newpc with
 839    Matita_datatypes_constructors.Pair(s_tmp1,new_pc) -> (let s_tmp2 = (Matita_freescale_status.set_pc_reg m t s_tmp1 new_pc) in (let s_tmp3 = (Matita_freescale_status.set_clk_desc m t s_tmp2 (Matita_datatypes_constructors.None)) in (let abs_magic = (Matita_freescale_opcode.magic_of_opcode abs_pseudo) in
 840 (match (Matita_freescale_byte8.eq_b8 abs_magic (Matita_freescale_opcode.magic_of_opcode Matita_freescale_opcode.BGND)) with
 841    Matita_datatypes_bool.True -> (TickSUSP(s_tmp3,BGND_MODE))
 842  | Matita_datatypes_bool.False ->
 843 (match (Matita_freescale_byte8.eq_b8 abs_magic (Matita_freescale_opcode.magic_of_opcode Matita_freescale_opcode.STOP)) with
 844    Matita_datatypes_bool.True -> (TickSUSP(s_tmp3,STOP_MODE))
 845  | Matita_datatypes_bool.False ->
 846 (match (Matita_freescale_byte8.eq_b8 abs_magic (Matita_freescale_opcode.magic_of_opcode Matita_freescale_opcode.WAIT)) with
 847    Matita_datatypes_bool.True -> (TickSUSP(s_tmp3,WAIT_MODE))
 848  | Matita_datatypes_bool.False -> (TickOK(s_tmp3)))
 849 )
 850 )
 851 ))))
 852 )
 853 ))))))))
 854 ;;
 855
 856 let tick =
 857 (function m -> (function t -> (function s -> (let opt_info = (Matita_freescale_status.get_clk_desc m t s) in
 858 (match opt_info with
 859    Matita_datatypes_constructors.None ->
 860 (match (Matita_freescale_load_write.fetch m t s) with
 861    Matita_freescale_load_write.FetchERR(err) -> (TickERR(s,err))
 862  | Matita_freescale_load_write.FetchOK(fetch_info,cur_pc) ->
 863 (match fetch_info with
 864    Matita_freescale_extra.QuadrupleT(pseudo,mode,_,tot_clk) ->
 865 (match (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)) tot_clk) with
 866    Matita_datatypes_bool.True -> (tick_execute m t s pseudo mode cur_pc)
 867  | Matita_datatypes_bool.False -> (TickOK((Matita_freescale_status.set_clk_desc m t s (Matita_datatypes_constructors.Some((Matita_freescale_extra.QuintupleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)),pseudo,mode,tot_clk,cur_pc))))))))
 868 )
 869 )
 870
 871  | Matita_datatypes_constructors.Some(info) ->
 872 (match info with
 873    Matita_freescale_extra.QuintupleT(cur_clk,pseudo,mode,tot_clk,cur_pc) ->
 874 (match (Matita_freescale_byte8.eq_b8 (Matita_freescale_byte8.succ_b8 cur_clk) tot_clk) with
 875    Matita_datatypes_bool.True -> (tick_execute m t s pseudo mode cur_pc)
 876  | Matita_datatypes_bool.False -> (TickOK((Matita_freescale_status.set_clk_desc m t s (Matita_datatypes_constructors.Some((Matita_freescale_extra.QuintupleT((Matita_freescale_byte8.succ_b8 cur_clk),pseudo,mode,tot_clk,cur_pc))))))))
 877 )
 878 )
 879 ))))
 880 ;;
 881
 882 let execute =
 883 let rec execute =
 884 (function m -> (function t -> (function s -> (function n ->
 885 (match s with
 886    TickERR(s',error) -> print_string("e") ; (TickERR(s',error))
 887  | TickSUSP(s',susp) -> print_string("s") ; (TickSUSP(s',susp))
 888  | TickOK(s') ->
 889 (match n with
 890    Matita_nat_nat.O -> (TickOK(s'))
 891  | Matita_nat_nat.S(n') -> print_string(".") ; (execute m t (tick m t s') n'))
 892 )
 893 )))) in execute
 894 ;;