X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_load_write.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_load_write.ml;h=22876976d8f23778281e5b35fa682500716685d4;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_load_write.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_load_write.ml
new file mode 100644
index 000000000..22876976d
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_load_write.ml
@@ -0,0 +1,575 @@
+type error_type =
+ILL_OP
+ | ILL_FETCH_AD
+ | ILL_EX_AD
+;;
+
+let error_type_rec =
+(function p -> (function p1 -> (function p2 -> (function e -> 
+(match e with 
+   ILL_OP -> p
+ | ILL_FETCH_AD -> p1
+ | ILL_EX_AD -> p2)
+))))
+;;
+
+let error_type_rect =
+(function p -> (function p1 -> (function p2 -> (function e -> 
+(match e with 
+   ILL_OP -> p
+ | ILL_FETCH_AD -> p1
+ | ILL_EX_AD -> p2)
+))))
+;;
+
+type ('a) fetch_result =
+FetchERR of error_type
+ | FetchOK of 'a * Matita_freescale_word16.word16
+;;
+
+let fetch_result_rec =
+(function f -> (function f1 -> (function f2 -> 
+(match f2 with 
+   FetchERR(e) -> (f e)
+ | FetchOK(t,w) -> (f1 t w))
+)))
+;;
+
+let fetch_result_rect =
+(function f -> (function f1 -> (function f2 -> 
+(match f2 with 
+   FetchERR(e) -> (f e)
+ | FetchOK(t,w) -> (f1 t w))
+)))
+;;
+
+let rS08_memory_filter_read_aux =
+(function t -> (function s -> (function addr -> (function fREG -> (function fMEM -> 
+(match s with 
+   Matita_freescale_status.Mk_any_status(alu,mem,chk,_) -> 
+(match Obj.magic(alu) with 
+   Matita_freescale_status.Mk_alu_RS08(_,_,_,_,xm,psm,_,_) -> 
+(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 
+   Matita_datatypes_bool.True -> (fREG xm)
+ | Matita_datatypes_bool.False -> 
+(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 
+   Matita_datatypes_bool.True -> (fREG psm)
+ | Matita_datatypes_bool.False -> 
+(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 
+   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)))
+ | Matita_datatypes_bool.False -> 
+(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 
+   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)))))))
+ | Matita_datatypes_bool.False -> (fMEM mem chk addr))
+)
+)
+)
+)
+)
+)))))
+;;
+
+let rS08_memory_filter_read =
+(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))))))))
+;;
+
+let rS08_memory_filter_read_bit =
+(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)))))))))
+;;
+
+let memory_filter_read =
+(function m -> (function t -> 
+(match m with 
+   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))))
+ | 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))))
+ | 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))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (rS08_memory_filter_read t s addr)))))
+))
+;;
+
+let memory_filter_read_bit =
+(function m -> (function t -> 
+(match m with 
+   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)))))
+ | 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)))))
+ | 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)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (rS08_memory_filter_read_bit t s addr sub))))))
+))
+;;
+
+let rS08_memory_filter_write_aux =
+(function t -> (function s -> (function addr -> (function fREG -> (function fMEM -> 
+(match s with 
+   Matita_freescale_status.Mk_any_status(alu,mem,chk,clk) -> 
+(match Obj.magic(alu) with 
+   Matita_freescale_status.Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl) -> 
+(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 
+   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))))
+ | Matita_datatypes_bool.False -> 
+(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 
+   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))))
+ | Matita_datatypes_bool.False -> 
+(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 
+   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))))))
+ | Matita_datatypes_bool.False -> 
+(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 
+   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))))))
+ | 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)))))))
+)
+)
+)
+)
+)
+)))))
+;;
+
+let rS08_memory_filter_write =
+(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_)))))))))
+;;
+
+let rS08_memory_filter_write_bit =
+(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_))))))))))
+;;
+
+let memory_filter_write =
+(function m -> (function t -> 
+(match m with 
+   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)))))))))
+ | 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)))))))))
+ | 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)))))))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function val_ -> (rS08_memory_filter_write t s addr val_))))))
+))
+;;
+
+let memory_filter_write_bit =
+(function m -> (function t -> 
+(match m with 
+   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))))))))))
+ | 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))))))))))
+ | 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))))))))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function s -> (function addr -> (function sub -> (function val_ -> (rS08_memory_filter_write_bit t s addr sub val_)))))))
+))
+;;
+
+let filtered_inc_w16 =
+(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)))))))
+;;
+
+let filtered_plus_w16 =
+let rec filtered_plus_w16 = 
+(function m -> (function t -> (function s -> (function w -> (function n -> 
+(match n with 
+   Matita_nat_nat.O -> w
+ | Matita_nat_nat.S(n') -> (filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n'))
+))))) in filtered_plus_w16
+;;
+
+let fetch =
+(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 
+(match (memory_filter_read m t s pc) with 
+   Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
+ | Matita_datatypes_constructors.Some(bh) -> 
+(match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Byte(bh))) with 
+   Matita_datatypes_constructors.None -> 
+(match m with 
+   Matita_freescale_opcode.HC05 -> (FetchERR(ILL_OP))
+ | Matita_freescale_opcode.HC08 -> 
+(match (Matita_freescale_byte8.eq_b8 bh (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE))) with 
+   Matita_datatypes_bool.True -> 
+(match (memory_filter_read m t s pc_next1) with 
+   Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
+ | Matita_datatypes_constructors.Some(bl) -> 
+(match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Word((Matita_freescale_word16.Mk_word16(bh,bl))))) with 
+   Matita_datatypes_constructors.None -> (FetchERR(ILL_OP))
+ | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next2)))
+)
+
+ | Matita_datatypes_bool.False -> (FetchERR(ILL_OP)))
+
+ | Matita_freescale_opcode.HCS08 -> 
+(match (Matita_freescale_byte8.eq_b8 bh (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X9,Matita_freescale_exadecim.XE))) with 
+   Matita_datatypes_bool.True -> 
+(match (memory_filter_read m t s pc_next1) with 
+   Matita_datatypes_constructors.None -> (FetchERR(ILL_FETCH_AD))
+ | Matita_datatypes_constructors.Some(bl) -> 
+(match (Matita_freescale_translation.full_info_of_word16 m (Matita_freescale_opcode.Word((Matita_freescale_word16.Mk_word16(bh,bl))))) with 
+   Matita_datatypes_constructors.None -> (FetchERR(ILL_OP))
+ | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next2)))
+)
+
+ | Matita_datatypes_bool.False -> (FetchERR(ILL_OP)))
+
+ | Matita_freescale_opcode.RS08 -> (FetchERR(ILL_OP)))
+
+ | Matita_datatypes_constructors.Some(info) -> (FetchOK(info,pc_next1)))
+)
+))))))
+;;
+
+let loadb_from =
+(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)))))))))))))
+;;
+
+let loadbit_from =
+(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))))))))))))))
+;;
+
+let loadw_from =
+(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)))))))))))))))
+;;
+
+let writeb_to =
+(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))))))))))))))
+;;
+
+let writebit_to =
+(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)))))))))))))))
+;;
+
+let writew_to =
+(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))))))))))))))))
+;;
+
+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))))
+;;
+
+let aux_load =
+(function m -> (function t -> (function byteflag -> 
+(match byteflag with 
+   Matita_datatypes_bool.True -> Obj.magic ((loadb_from m t))
+ | Matita_datatypes_bool.False -> Obj.magic ((loadw_from m t)))
+)))
+;;
+
+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)))))
+;;
+
+let aux_write =
+(function m -> (function t -> (function byteflag -> 
+(match byteflag with 
+   Matita_datatypes_bool.True -> Obj.magic ((writeb_to m t))
+ | Matita_datatypes_bool.False -> Obj.magic ((writew_to m t)))
+)))
+;;
+
+let mode_IMM1_load =
+(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)))))))))))
+;;
+
+let mode_IMM1EXT_load =
+(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)))))))))))
+;;
+
+let mode_IMM2_load =
+(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)))))))))))))))))
+;;
+
+let mode_DIR1_load =
+(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))))))))))
+;;
+
+let mode_DIR1n_load =
+(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))))))))))
+;;
+
+let mode_DIR1_write =
+(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)))))))))
+;;
+
+let mode_DIR1n_write =
+(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)))))))))
+;;
+
+let mode_DIR2_load =
+(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))))))))))))))
+;;
+
+let mode_DIR2_write =
+(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)))))))))))
+;;
+
+let get_IX =
+(function m -> (function t -> (function s -> 
+(match m with 
+   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))))))
+ | 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))))
+ | 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))))
+ | Matita_freescale_opcode.RS08 -> (Matita_datatypes_constructors.None))
+)))
+;;
+
+let mode_IX0_load =
+(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))))))))
+;;
+
+let mode_IX0_write =
+(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)))))))))
+;;
+
+let mode_IX1_load =
+(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))))))))))))
+;;
+
+let mode_IX1ADD_load =
+(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)))))))))))))
+;;
+
+let mode_IX1_write =
+(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)))))))))))
+;;
+
+let mode_IX2_load =
+(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))))))))))))))))
+;;
+
+let mode_IX2ADD_load =
+(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)))))))))))))))))))
+;;
+
+let mode_IX2_write =
+(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)))))))))))))
+;;
+
+let mode_SP1_load =
+(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))))))))))))
+;;
+
+let mode_SP1_write =
+(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)))))))))))
+;;
+
+let mode_SP2_load =
+(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))))))))))))))))
+;;
+
+let mode_SP2_write =
+(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)))))))))))))
+;;
+
+let aux_inc_indX_16 =
+(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)))))))))
+;;
+
+let multi_mode_load =
+(function byteflag -> (function m -> (function t -> 
+(match byteflag with 
+   Matita_datatypes_bool.True -> Obj.magic ((function s -> (function cur_pc -> (function i -> 
+(match i with 
+   Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
+ | 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))))
+ | 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))))))
+ | 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))))))
+ | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1 -> (mode_IMM1_load m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (mode_IMM1_load m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (mode_IX0_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (mode_DIR1_load Matita_datatypes_bool.True m t s cur_pc)
+ | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
+ | 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))))))
+ | 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)))))))
+))))
+ | Matita_datatypes_bool.False -> Obj.magic ((function s -> (function cur_pc -> (function i -> 
+(match i with 
+   Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHH -> (Matita_datatypes_constructors.None)
+ | 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))))))
+ | Matita_freescale_opcode.MODE_INHX1ADD -> (mode_IX1ADD_load m t s cur_pc)
+ | Matita_freescale_opcode.MODE_INHX2ADD -> (mode_IX2ADD_load m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1EXT -> (mode_IMM1EXT_load m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IMM2 -> (mode_IMM2_load m t s cur_pc)
+ | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_load Matita_datatypes_bool.False m t s cur_pc)
+ | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_datatypes_constructors.None)
+ | 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 -> 
+(match s_immb_and_PC with 
+   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')))))
+))
+ | 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 -> 
+(match s_immb_and_PC with 
+   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')))))
+))))
+ | 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 -> 
+(match s_immb1_and_PC with 
+   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 -> 
+(match s_immb2_and_PC with 
+   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'')))))
+)))
+))
+ | 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 -> 
+(match s_dirb_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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'')))))
+)))
+))
+ | 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 -> 
+(match s_ixb_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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'')))))
+)))
+))
+ | 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 -> 
+(match s_ixb_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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'')))))))
+)))
+))
+ | 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 -> 
+(match s_ixb_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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'')))))
+)))
+))
+ | 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 -> 
+(match s_ixb_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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'')))))))
+)))
+))
+ | 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 -> 
+(match s_spb_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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'')))))
+)))
+))
+ | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
+ | 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 -> 
+(match s_dirbn_and_PC with 
+   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 -> 
+(match s_immb_and_PC with 
+   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,
+(match dirbn with 
+   Matita_datatypes_bool.True -> Matita_freescale_exadecim.X1
+ | Matita_datatypes_bool.False -> Matita_freescale_exadecim.X0)
+)),immb)),cur_pc'')))))
+)))
+))
+ | Matita_freescale_opcode.MODE_TNY(_) -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_SRT(_) -> (Matita_datatypes_constructors.None))
+)))))
+)))
+;;
+
+let multi_mode_write =
+(function byteflag -> (function m -> (function t -> 
+(match byteflag with 
+   Matita_datatypes_bool.True -> Obj.magic ((function s -> (function cur_pc -> (function i -> (function writeb -> 
+(match i with 
+   Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
+ | 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))))
+ | 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))))))
+ | 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))))))
+ | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | 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 -> 
+(match s_and_PC with 
+   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)))))))
+))
+ | 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 -> 
+(match s_and_PC with 
+   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)))))))
+))
+ | 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))))
+ | 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))))))
+ | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (mode_DIR1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (mode_IX0_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (mode_IX1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (mode_SP1_write Matita_datatypes_bool.True m t s cur_pc writeb)
+ | 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)))
+ | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
+ | 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))))))
+ | 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)))))))
+)))))
+ | Matita_datatypes_bool.False -> Obj.magic ((function s -> (function cur_pc -> (function i -> (function writew -> 
+(match i with 
+   Matita_freescale_opcode.MODE_INH -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHA -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHH -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX0ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX1ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX2ADD -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1EXT -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM2 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1 -> (mode_DIR1_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_DIR2 -> (mode_DIR2_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_IX0 -> (mode_IX0_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_IX1 -> (mode_IX1_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_IX2 -> (mode_IX2_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_SP1 -> (mode_SP1_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_SP2 -> (mode_SP2_write Matita_datatypes_bool.False m t s cur_pc writew)
+ | Matita_freescale_opcode.MODE_DIR1_to_DIR1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1_to_DIR1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX0p_to_DIR1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1_to_IX0p -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHA_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_INHX_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IMM1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIR1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX0_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX0p_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_IX1p_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_SP1_and_IMM1 -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIRn(_) -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_DIRn_and_IMM1(_) -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_TNY(_) -> (Matita_datatypes_constructors.None)
+ | Matita_freescale_opcode.MODE_SRT(_) -> (Matita_datatypes_constructors.None))
+))))))
+)))
+;;