]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_multivm.ml
Extracted code. The main executable is medium_tests that runs the emulator on
[helm.git] / 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 ;;