8 (function p -> (function p1 -> (function p2 -> (function e ->
17 (function p -> (function p1 -> (function p2 -> (function e ->
25 type ('a) fetch_result =
26 FetchERR of error_type
27 | FetchOK of 'a * Matita_freescale_word16.word16
30 let fetch_result_rec =
31 (function f -> (function f1 -> (function f2 ->
34 | FetchOK(t,w) -> (f1 t w))
38 let fetch_result_rect =
39 (function f -> (function f1 -> (function f2 ->
42 | FetchOK(t,w) -> (f1 t w))
46 let rS08_memory_filter_read_aux =
47 (function t -> (function s -> (function addr -> (function fREG -> (function fMEM ->
49 Matita_freescale_status.Mk_any_status(alu,mem,chk,_) ->
50 (match Obj.magic(alu) with
51 Matita_freescale_status.Mk_alu_RS08(_,_,_,_,xm,psm,_,_) ->
52 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
53 Matita_datatypes_bool.True -> (fREG xm)
54 | Matita_datatypes_bool.False ->
55 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
56 Matita_datatypes_bool.True -> (fREG psm)
57 | Matita_datatypes_bool.False ->
58 (match (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) with
59 Matita_datatypes_bool.True -> (fMEM mem chk (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),xm)))
60 | Matita_datatypes_bool.False ->
61 (match (Matita_freescale_word16.in_range addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) with
62 Matita_datatypes_bool.True -> (fMEM mem chk (Matita_freescale_word16.or_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_freescale_word16.Mk_word16(psm,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))) (Matita_freescale_word16.and_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF)))))))
63 | Matita_datatypes_bool.False -> (fMEM mem chk addr))
72 let rS08_memory_filter_read =
73 (function t -> (function s -> (function addr -> (rS08_memory_filter_read_aux t s addr (function b -> (Matita_datatypes_constructors.Some(b))) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_read t m c a))))))))
76 let rS08_memory_filter_read_bit =
77 (function t -> (function s -> (function addr -> (function sub -> (rS08_memory_filter_read_aux t s addr (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_memory_struct.getn_array8T sub (Matita_freescale_memory_struct.bits_of_byte8 b))))) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_read_bit t m c a sub)))))))))
80 let memory_filter_read =
81 (function m -> (function t ->
83 Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (Matita_freescale_memory_abs.mem_read t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr))))
84 | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (Matita_freescale_memory_abs.mem_read t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr))))
85 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (Matita_freescale_memory_abs.mem_read t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr))))
86 | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (rS08_memory_filter_read t s addr)))))
90 let memory_filter_read_bit =
91 (function m -> (function t ->
93 Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (function sub -> (Matita_freescale_memory_abs.mem_read_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr sub)))))
94 | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (function sub -> (Matita_freescale_memory_abs.mem_read_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr sub)))))
95 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (Matita_freescale_memory_abs.mem_read_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr sub)))))
96 | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (rS08_memory_filter_read_bit t s addr sub))))))
100 let rS08_memory_filter_write_aux =
101 (function t -> (function s -> (function addr -> (function fREG -> (function fMEM ->
103 Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) ->
104 (match Obj.magic(alu) with
105 Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl) ->
106 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
107 Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,(fREG xm),psm,zfl,cfl))),mem,chk,clk))))
108 | Matita_datatypes_bool.False ->
109 (match (Matita_freescale_extra.or_bool (Matita_freescale_extra.or_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) (Matita_freescale_byte8.eq_b8 xm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X1,Matita_freescale_exadecim.XF))))) (Matita_freescale_extra.and_bool (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XD,Matita_freescale_exadecim.XF))))) (Matita_freescale_byte8.eq_b8 psm (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with
110 Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,(fREG psm),zfl,cfl))),mem,chk,clk))))
111 | Matita_datatypes_bool.False ->
112 (match (Matita_freescale_word16.eq_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.XE))))) with
113 Matita_datatypes_bool.True -> (Matita_freescale_extra.opt_map (fMEM mem chk (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),xm))) (function mem' -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl))),mem',chk,clk))))))
114 | Matita_datatypes_bool.False ->
115 (match (Matita_freescale_word16.in_range addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XC,Matita_freescale_exadecim.X0)))) (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))))) with
116 Matita_datatypes_bool.True -> (Matita_freescale_extra.opt_map (fMEM mem chk (Matita_freescale_word16.or_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_datatypes_constructors.fst (Matita_freescale_word16.shr_w16 (Matita_freescale_word16.Mk_word16(psm,(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))) (Matita_freescale_word16.and_w16 addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X3,Matita_freescale_exadecim.XF))))))) (function mem' -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl))),mem',chk,clk))))))
117 | Matita_datatypes_bool.False -> (Matita_freescale_extra.opt_map (fMEM mem chk addr) (function mem' -> (Matita_datatypes_constructors.Some((Matita_freescale_status.Mk_any_status((Obj.magic(Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl))),mem',chk,clk)))))))
126 let rS08_memory_filter_write =
127 (function t -> (function s -> (function addr -> (function val_ -> (rS08_memory_filter_write_aux t s addr (function b -> val_) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_update t m c a val_)))))))))
130 let rS08_memory_filter_write_bit =
131 (function t -> (function s -> (function addr -> (function sub -> (function val_ -> (rS08_memory_filter_write_aux t s addr (function b -> (Matita_freescale_memory_struct.byte8_of_bits (Matita_freescale_memory_struct.setn_array8T sub (Matita_freescale_memory_struct.bits_of_byte8 b) val_))) (function m -> (function c -> (function a -> (Matita_freescale_memory_abs.mem_update_bit t m c a sub val_))))))))))
134 let memory_filter_write =
135 (function m -> (function t ->
137 Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC05 t s mem)))))))))
138 | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC08 t s mem)))))))))
139 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 t s mem)))))))))
140 | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (rS08_memory_filter_write t s addr val_))))))
144 let memory_filter_write_bit =
145 (function m -> (function t ->
147 Matita_freescale_opcode.HC05 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC05 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC05 t s) addr sub val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC05 t s mem))))))))))
148 | Matita_freescale_opcode.HC08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HC08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HC08 t s) addr sub val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HC08 t s mem))))))))))
149 | Matita_freescale_opcode.HCS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (Matita_freescale_extra.opt_map (Matita_freescale_memory_abs.mem_update_bit t (Matita_freescale_status.get_mem_desc Matita_freescale_opcode.HCS08 t s) (Matita_freescale_status.get_chk_desc Matita_freescale_opcode.HCS08 t s) addr sub val_) (function mem -> (Matita_datatypes_constructors.Some((Matita_freescale_status.set_mem_desc Matita_freescale_opcode.HCS08 t s mem))))))))))
150 | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (rS08_memory_filter_write_bit t s addr sub val_)))))))
154 let filtered_inc_w16 =
155 (function m -> (function t -> (function s -> (function w -> (Matita_freescale_status.get_pc_reg m t (Matita_freescale_status.set_pc_reg m t s (Matita_freescale_word16.succ_w16 w)))))))
158 let filtered_plus_w16 =
159 let rec filtered_plus_w16 =
160 (function m -> (function t -> (function s -> (function w -> (function n ->
162 Matita_nat_nat.O -> w
163 | Matita_nat_nat.S(n') -> (filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n'))
164 ))))) in filtered_plus_w16
168 (function m -> (function t -> (function s -> (let pc = (Matita_freescale_status.get_pc_reg m t s) in (let pc_next1 = (filtered_inc_w16 m t s pc) in (let pc_next2 = (filtered_inc_w16 m t s pc_next1) in
169 (match (memory_filter_read m t s pc) with
170 Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
171 | Matita_datatypes_constructors.Some(bh) ->
172 (match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Byte(bh))) with
173 Matita_datatypes_constructors.None ->
175 Matita_freescale_opcode.HC05 -> (FetchERR(ILL_OP))
176 | Matita_freescale_opcode.HC08 ->
177 (match (Matita_freescale_byte8.eq_b8 bh (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE))) with
178 Matita_datatypes_bool.True ->
179 (match (memory_filter_read m t s pc_next1) with
180 Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
181 | Matita_datatypes_constructors.Some(bl) ->
182 (match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Word((Matita_freescale_word16.Mk_word16(bh,bl))))) with
183 Matita_datatypes_constructors.None -> (FetchERR(ILL_OP))
184 | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next2)))
187 | Matita_datatypes_bool.False -> (FetchERR(ILL_OP)))
189 | Matita_freescale_opcode.HCS08 ->
190 (match (Matita_freescale_byte8.eq_b8 bh (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE))) with
191 Matita_datatypes_bool.True ->
192 (match (memory_filter_read m t s pc_next1) with
193 Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
194 | Matita_datatypes_constructors.Some(bl) ->
195 (match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Word((Matita_freescale_word16.Mk_word16(bh,bl))))) with
196 Matita_datatypes_constructors.None -> (FetchERR(ILL_OP))
197 | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next2)))
200 | Matita_datatypes_bool.False -> (FetchERR(ILL_OP)))
202 | Matita_freescale_opcode.RS08 -> (FetchERR(ILL_OP)))
204 | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next1)))
210 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (Matita_freescale_extra.opt_map (memory_filter_read m t s addr) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,(filtered_plus_w16 m t s cur_pc fetched)))))))))))))
214 (function m -> (function t -> (function s -> (function addr -> (function sub -> (function cur_pc -> (function fetched -> (Matita_freescale_extra.opt_map (memory_filter_read_bit m t s addr sub) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,(filtered_plus_w16 m t s cur_pc fetched))))))))))))))
218 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (Matita_freescale_extra.opt_map (memory_filter_read m t s addr) (function bh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (Matita_freescale_word16.succ_w16 addr)) (function bl -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(bh,bl)),(filtered_plus_w16 m t s cur_pc fetched)))))))))))))))
222 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (function writeb -> (Matita_freescale_extra.opt_map (memory_filter_write m t s addr writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,(filtered_plus_w16 m t s cur_pc fetched))))))))))))))
226 (function m -> (function t -> (function s -> (function addr -> (function sub -> (function cur_pc -> (function fetched -> (function writeb -> (Matita_freescale_extra.opt_map (memory_filter_write_bit m t s addr sub writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,(filtered_plus_w16 m t s cur_pc fetched)))))))))))))))
230 (function m -> (function t -> (function s -> (function addr -> (function cur_pc -> (function fetched -> (function writew -> (Matita_freescale_extra.opt_map (memory_filter_write m t s addr (Matita_freescale_word16.w16h writew)) (function tmps1 -> (Matita_freescale_extra.opt_map (memory_filter_write m t tmps1 (Matita_freescale_word16.succ_w16 addr) (Matita_freescale_word16.w16l writew)) (function tmps2 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps2,(filtered_plus_w16 m t tmps2 cur_pc fetched))))))))))))))))
233 type aux_load_typing = (Matita_freescale_status.any_status -> (Matita_freescale_word16.word16 -> (Matita_freescale_word16.word16 -> (Matita_nat_nat.nat -> ((Matita_freescale_status.any_status,unit (* TOO POLYMORPHIC TYPE *),Matita_freescale_word16.word16) Matita_freescale_extra.prod3T) Matita_datatypes_constructors.option))))
237 (function m -> (function t -> (function byteflag ->
239 Matita_datatypes_bool.True -> Obj.magic ((loadb_from m t))
240 | Matita_datatypes_bool.False -> Obj.magic ((loadw_from m t)))
244 type aux_write_typing = (Matita_freescale_status.any_status -> (Matita_freescale_word16.word16 -> (Matita_freescale_word16.word16 -> (Matita_nat_nat.nat -> (unit (* TOO POLYMORPHIC TYPE *) -> ((Matita_freescale_status.any_status,Matita_freescale_word16.word16) Matita_datatypes_constructors.prod) Matita_datatypes_constructors.option)))))
248 (function m -> (function t -> (function byteflag ->
250 Matita_datatypes_bool.True -> Obj.magic ((writeb_to m t))
251 | Matita_datatypes_bool.False -> Obj.magic ((writew_to m t)))
256 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,(filtered_inc_w16 m t s cur_pc)))))))))))
259 let mode_IMM1EXT_load =
260 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b)),(filtered_inc_w16 m t s cur_pc)))))))))))
264 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function bh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function bl -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(bh,bl)),(filtered_plus_w16 m t s cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))
268 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (aux_load m t byteflag s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))
271 let mode_DIR1n_load =
272 (function m -> (function t -> (function s -> (function cur_pc -> (function sub -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (loadbit_from m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) sub cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))
275 let mode_DIR1_write =
276 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (aux_write m t byteflag s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writebw)))))))))
279 let mode_DIR1n_write =
280 (function m -> (function t -> (function s -> (function cur_pc -> (function sub -> (function writeb -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addr -> (writebit_to m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),addr)) sub cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writeb)))))))))
284 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addrh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function addrl -> (aux_load m t byteflag s (Matita_freescale_word16.Mk_word16(addrh,addrl)) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))
287 let mode_DIR2_write =
288 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function addrh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function addrl -> (aux_write m t byteflag s (Matita_freescale_word16.Mk_word16(addrh,addrl)) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) writebw)))))))))))
292 (function m -> (function t -> (function s ->
294 Matita_freescale_opcode.HC05 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function indx -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),indx))))))
295 | Matita_freescale_opcode.HC08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s) (function indx -> (Matita_datatypes_constructors.Some(indx))))
296 | Matita_freescale_opcode.HCS08 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s) (function indx -> (Matita_datatypes_constructors.Some(indx))))
297 | Matita_freescale_opcode.RS08 -> (Matita_datatypes_constructors.None))
302 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (aux_load m t byteflag s addr cur_pc Matita_nat_nat.O))))))))
306 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (aux_write m t byteflag s addr cur_pc Matita_nat_nat.O writebw)))))))))
310 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))))
313 let mode_IX1ADD_load =
314 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function b -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b))),(filtered_inc_w16 m t s cur_pc)))))))))))))
318 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writebw)))))))))))
322 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))
325 let mode_IX2ADD_load =
326 (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function bh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function bl -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(bh,bl))),(filtered_plus_w16 m t s cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))
330 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (get_IX m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) writebw)))))))))))))
334 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O))))))))))))
338 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offs -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),offs))) cur_pc (Matita_nat_nat.S(Matita_nat_nat.O)) writebw)))))))))))
342 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_load m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))
346 (function byteflag -> (function m -> (function t -> (function s -> (function cur_pc -> (function writebw -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_sp_reg m t s) (function addr -> (Matita_freescale_extra.opt_map (memory_filter_read m t s cur_pc) (function offsh -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc)) (function offsl -> (aux_write m t byteflag s (Matita_freescale_word16.plus_w16nc addr (Matita_freescale_word16.Mk_word16(offsh,offsl))) cur_pc (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) writebw)))))))))))))
349 let aux_inc_indX_16 =
350 (function m -> (function t -> (function s -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_16_reg m t s) (function x_op -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_16_reg m t s (Matita_freescale_word16.succ_w16 x_op)) (function s_tmp -> (Matita_datatypes_constructors.Some(s_tmp)))))))))
353 let multi_mode_load =
354 (function byteflag -> (function m -> (function t ->
356 Matita_datatypes_bool.True -> Obj.magic ((function s -> (function cur_pc -> (function i ->
358 Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
359 | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_status.get_acc_8_low_reg m t s),cur_pc))))
360 | Matita_freescale_opcode.MODE_INHX -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function indx -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,indx,cur_pc))))))
361 | Matita_freescale_opcode.MODE_INHH -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_high_reg m t s) (function indx -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,indx,cur_pc))))))
362 | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
363 | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
364 | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
365 | Matita_freescale_opcode.MODE_IMM1 -> (mode_IMM1_load m t s cur_pc)
366 | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
367 | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
368 | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
369 | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_load Matita_datatypes_bool.True m t s cur_pc)
370 | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc)
371 | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc)
372 | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_load Matita_datatypes_bool.True m t s cur_pc)
373 | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_load Matita_datatypes_bool.True m t s cur_pc)
374 | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_load Matita_datatypes_bool.True m t s cur_pc)
375 | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
376 | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (mode_IMM1_load m t s cur_pc)
377 | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc)
378 | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
379 | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.None)
380 | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_datatypes_constructors.None)
381 | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
382 | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_datatypes_constructors.None)
383 | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_datatypes_constructors.None)
384 | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
385 | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_datatypes_constructors.None)
386 | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
387 | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_datatypes_constructors.None)
388 | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
389 | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
390 | Matita_freescale_opcode.MODE_TNY(e) -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,e))))) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,cur_pc))))))
391 | Matita_freescale_opcode.MODE_SRT(e) -> (Matita_freescale_extra.opt_map (memory_filter_read m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_aux_bases.byte8_of_bitrigesim e)))) (function b -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,b,cur_pc)))))))
393 | Matita_datatypes_bool.False -> Obj.magic ((function s -> (function cur_pc -> (function i ->
395 Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
396 | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.None)
397 | Matita_freescale_opcode.MODE_INHX -> (Matita_datatypes_constructors.None)
398 | Matita_freescale_opcode.MODE_INHH -> (Matita_datatypes_constructors.None)
399 | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_freescale_extra.opt_map (get_IX m t s) (function w -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,w,cur_pc))))))
400 | Matita_freescale_opcode.MODE_INHX1ADD -> (mode_IX1ADD_load m t s cur_pc)
401 | Matita_freescale_opcode.MODE_INHX2ADD -> (mode_IX2ADD_load m t s cur_pc)
402 | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
403 | Matita_freescale_opcode.MODE_IMM1EXT -> (mode_IMM1EXT_load m t s cur_pc)
404 | Matita_freescale_opcode.MODE_IMM2 -> (mode_IMM2_load m t s cur_pc)
405 | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.False m t s cur_pc)
406 | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_load Matita_datatypes_bool.False m t s cur_pc)
407 | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_load Matita_datatypes_bool.False m t s cur_pc)
408 | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_load Matita_datatypes_bool.False m t s cur_pc)
409 | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_load Matita_datatypes_bool.False m t s cur_pc)
410 | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_load Matita_datatypes_bool.False m t s cur_pc)
411 | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_load Matita_datatypes_bool.False m t s cur_pc)
412 | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (Matita_datatypes_constructors.None)
413 | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (Matita_datatypes_constructors.None)
414 | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_datatypes_constructors.None)
415 | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_datatypes_constructors.None)
416 | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc) (function s_immb_and_PC ->
417 (match s_immb_and_PC with
418 Matita_freescale_extra.TripleT(_,immb,cur_pc') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16((Matita_freescale_status.get_acc_8_low_reg m t s),immb)),cur_pc')))))
420 | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.get_indX_8_low_reg m t s) (function x_op -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc) (function s_immb_and_PC ->
421 (match s_immb_and_PC with
422 Matita_freescale_extra.TripleT(_,immb,cur_pc') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(x_op,immb)),cur_pc')))))
424 | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc) (function s_immb1_and_PC ->
425 (match s_immb1_and_PC with
426 Matita_freescale_extra.TripleT(_,immb1,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb2_and_PC ->
427 (match s_immb2_and_PC with
428 Matita_freescale_extra.TripleT(_,immb2,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(immb1,immb2)),cur_pc'')))))
431 | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc) (function s_dirb_and_PC ->
432 (match s_dirb_and_PC with
433 Matita_freescale_extra.TripleT(_,dirb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
434 (match s_immb_and_PC with
435 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(dirb,immb)),cur_pc'')))))
438 | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
439 (match s_ixb_and_PC with
440 Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
441 (match s_immb_and_PC with
442 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))
445 | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
446 (match s_ixb_and_PC with
447 Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
448 (match s_immb_and_PC with
449 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s) (function s' -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s',(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))))
452 | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
453 (match s_ixb_and_PC with
454 Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
455 (match s_immb_and_PC with
456 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))
459 | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc) (function s_ixb_and_PC ->
460 (match s_ixb_and_PC with
461 Matita_freescale_extra.TripleT(_,ixb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
462 (match s_immb_and_PC with
463 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s) (function s' -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s',(Matita_freescale_word16.Mk_word16(ixb,immb)),cur_pc'')))))))
466 | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_freescale_extra.opt_map (mode_SP1_load Matita_datatypes_bool.True m t s cur_pc) (function s_spb_and_PC ->
467 (match s_spb_and_PC with
468 Matita_freescale_extra.TripleT(_,spb,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
469 (match s_immb_and_PC with
470 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16(spb,immb)),cur_pc'')))))
473 | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
474 | Matita_freescale_opcode.MODE_DIRn_and_IMM1(msk) -> (Matita_freescale_extra.opt_map (mode_DIR1n_load m t s cur_pc msk) (function s_dirbn_and_PC ->
475 (match s_dirbn_and_PC with
476 Matita_freescale_extra.TripleT(_,dirbn,cur_pc') -> (Matita_freescale_extra.opt_map (mode_IMM1_load m t s cur_pc') (function s_immb_and_PC ->
477 (match s_immb_and_PC with
478 Matita_freescale_extra.TripleT(_,immb,cur_pc'') -> (Matita_datatypes_constructors.Some((Matita_freescale_extra.TripleT(s,(Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,
480 Matita_datatypes_bool.True -> Matita_freescale_exadecim.X1
481 | Matita_datatypes_bool.False -> Matita_freescale_exadecim.X0)
482 )),immb)),cur_pc'')))))
485 | Matita_freescale_opcode.MODE_TNY(_) -> (Matita_datatypes_constructors.None)
486 | Matita_freescale_opcode.MODE_SRT(_) -> (Matita_datatypes_constructors.None))
491 let multi_mode_write =
492 (function byteflag -> (function m -> (function t ->
494 Matita_datatypes_bool.True -> Obj.magic ((function s -> (function cur_pc -> (function i -> (function writeb ->
496 Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
497 | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s writeb),cur_pc))))
498 | Matita_freescale_opcode.MODE_INHX -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
499 | Matita_freescale_opcode.MODE_INHH -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_high_reg m t s writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
500 | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
501 | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
502 | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
503 | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
504 | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
505 | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
506 | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
507 | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_write Matita_datatypes_bool.True m t s cur_pc writeb)
508 | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb)
509 | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_write Matita_datatypes_bool.True m t s cur_pc writeb)
510 | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_write Matita_datatypes_bool.True m t s cur_pc writeb)
511 | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_write Matita_datatypes_bool.True m t s cur_pc writeb)
512 | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_write Matita_datatypes_bool.True m t s cur_pc writeb)
513 | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
514 | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
515 | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_freescale_extra.opt_map (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb) (function s_and_PC ->
517 Matita_datatypes_constructors.Pair(s_op,pC_op) -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s_op) (function s_op' -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_op',pC_op)))))))
519 | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_freescale_extra.opt_map (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb) (function s_and_PC ->
521 Matita_datatypes_constructors.Pair(s_op,pC_op) -> (Matita_freescale_extra.opt_map (aux_inc_indX_16 m t s_op) (function s_op' -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(s_op',pC_op)))))))
523 | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair((Matita_freescale_status.set_acc_8_low_reg m t s writeb),cur_pc))))
524 | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_freescale_extra.opt_map (Matita_freescale_status.set_indX_8_low_reg m t s writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
525 | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
526 | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
527 | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb)
528 | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
529 | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (mode_IX1_write Matita_datatypes_bool.True m t s cur_pc writeb)
530 | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
531 | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (mode_SP1_write Matita_datatypes_bool.True m t s cur_pc writeb)
532 | Matita_freescale_opcode.MODE_DIRn(msk) -> (mode_DIR1n_write m t s cur_pc msk (Matita_freescale_memory_struct.getn_array8T msk (Matita_freescale_memory_struct.bits_of_byte8 writeb)))
533 | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
534 | Matita_freescale_opcode.MODE_TNY(e) -> (Matita_freescale_extra.opt_map (memory_filter_write m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,e)))) writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc))))))
535 | Matita_freescale_opcode.MODE_SRT(e) -> (Matita_freescale_extra.opt_map (memory_filter_write m t s (Matita_freescale_word16.Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_aux_bases.byte8_of_bitrigesim e))) writeb) (function tmps -> (Matita_datatypes_constructors.Some((Matita_datatypes_constructors.Pair(tmps,cur_pc)))))))
537 | Matita_datatypes_bool.False -> Obj.magic ((function s -> (function cur_pc -> (function i -> (function writew ->
539 Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
540 | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.None)
541 | Matita_freescale_opcode.MODE_INHX -> (Matita_datatypes_constructors.None)
542 | Matita_freescale_opcode.MODE_INHH -> (Matita_datatypes_constructors.None)
543 | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
544 | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
545 | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
546 | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
547 | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
548 | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
549 | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.False m t s cur_pc writew)
550 | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_write Matita_datatypes_bool.False m t s cur_pc writew)
551 | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_write Matita_datatypes_bool.False m t s cur_pc writew)
552 | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_write Matita_datatypes_bool.False m t s cur_pc writew)
553 | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_write Matita_datatypes_bool.False m t s cur_pc writew)
554 | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_write Matita_datatypes_bool.False m t s cur_pc writew)
555 | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_write Matita_datatypes_bool.False m t s cur_pc writew)
556 | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (Matita_datatypes_constructors.None)
557 | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (Matita_datatypes_constructors.None)
558 | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_datatypes_constructors.None)
559 | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_datatypes_constructors.None)
560 | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.None)
561 | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_datatypes_constructors.None)
562 | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
563 | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_datatypes_constructors.None)
564 | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_datatypes_constructors.None)
565 | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
566 | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_datatypes_constructors.None)
567 | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
568 | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_datatypes_constructors.None)
569 | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
570 | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
571 | Matita_freescale_opcode.MODE_TNY(_) -> (Matita_datatypes_constructors.None)
572 | Matita_freescale_opcode.MODE_SRT(_) -> (Matita_datatypes_constructors.None))