--- /dev/null
+type alu_HC05 =
+Mk_alu_HC05 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
+;;
+
+let alu_HC05_rec =
+(function f -> (function a ->
+(match a with
+ Mk_alu_HC05(b,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7) -> (f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7))
+))
+;;
+
+let alu_HC05_rect =
+(function f -> (function a ->
+(match a with
+ Mk_alu_HC05(b,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7) -> (f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7))
+))
+;;
+
+let acc_low_reg_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> acc_low_reg_HC05)
+)
+;;
+
+let indX_low_reg_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> indX_low_reg_HC05)
+)
+;;
+
+let sp_reg_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_reg_HC05)
+)
+;;
+
+let sp_mask_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_mask_HC05)
+)
+;;
+
+let sp_fix_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_fix_HC05)
+)
+;;
+
+let pc_reg_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> pc_reg_HC05)
+)
+;;
+
+let pc_mask_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> pc_mask_HC05)
+)
+;;
+
+let h_flag_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> h_flag_HC05)
+)
+;;
+
+let i_flag_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> i_flag_HC05)
+)
+;;
+
+let n_flag_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> n_flag_HC05)
+)
+;;
+
+let z_flag_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> z_flag_HC05)
+)
+;;
+
+let c_flag_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> c_flag_HC05)
+)
+;;
+
+let irq_flag_HC05 =
+(function w ->
+(match w with
+ Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> irq_flag_HC05)
+)
+;;
+
+type alu_HC08 =
+Mk_alu_HC08 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
+;;
+
+let alu_HC08_rec =
+(function f -> (function a ->
+(match a with
+ Mk_alu_HC08(b,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9) -> (f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9))
+))
+;;
+
+let alu_HC08_rect =
+(function f -> (function a ->
+(match a with
+ Mk_alu_HC08(b,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9) -> (f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9))
+))
+;;
+
+let acc_low_reg_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> acc_low_reg_HC08)
+)
+;;
+
+let indX_low_reg_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> indX_low_reg_HC08)
+)
+;;
+
+let indX_high_reg_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> indX_high_reg_HC08)
+)
+;;
+
+let sp_reg_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> sp_reg_HC08)
+)
+;;
+
+let pc_reg_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> pc_reg_HC08)
+)
+;;
+
+let v_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> v_flag_HC08)
+)
+;;
+
+let h_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> h_flag_HC08)
+)
+;;
+
+let i_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> i_flag_HC08)
+)
+;;
+
+let n_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> n_flag_HC08)
+)
+;;
+
+let z_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> z_flag_HC08)
+)
+;;
+
+let c_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> c_flag_HC08)
+)
+;;
+
+let irq_flag_HC08 =
+(function w ->
+(match w with
+ Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> irq_flag_HC08)
+)
+;;
+
+type alu_RS08 =
+Mk_alu_RS08 of Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
+;;
+
+let alu_RS08_rec =
+(function f -> (function a ->
+(match a with
+ Mk_alu_RS08(b,w,w1,w2,b1,b2,b3,b4) -> (f b w w1 w2 b1 b2 b3 b4))
+))
+;;
+
+let alu_RS08_rect =
+(function f -> (function a ->
+(match a with
+ Mk_alu_RS08(b,w,w1,w2,b1,b2,b3,b4) -> (f b w w1 w2 b1 b2 b3 b4))
+))
+;;
+
+let acc_low_reg_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> acc_low_reg_RS08)
+)
+;;
+
+let pc_reg_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> pc_reg_RS08)
+)
+;;
+
+let pc_mask_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> pc_mask_RS08)
+)
+;;
+
+let spc_reg_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> spc_reg_RS08)
+)
+;;
+
+let x_map_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> x_map_RS08)
+)
+;;
+
+let ps_map_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> ps_map_RS08)
+)
+;;
+
+let z_flag_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> z_flag_RS08)
+)
+;;
+
+let c_flag_RS08 =
+(function w ->
+(match w with
+ Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> c_flag_RS08)
+)
+;;
+
+type any_status =
+Mk_any_status of unit (* TOO POLYMORPHIC TYPE *) * Matita_freescale_memory_abs.aux_mem_type * Matita_freescale_memory_abs.aux_chk_type * ((Matita_freescale_byte8.byte8,Matita_freescale_opcode.any_opcode,Matita_freescale_opcode.instr_mode,Matita_freescale_byte8.byte8,Matita_freescale_word16.word16) Matita_freescale_extra.prod5T) Matita_datatypes_constructors.option
+;;
+
+let any_status_rec =
+(function m -> (function m1 -> (function f -> (function a ->
+(match a with
+ Mk_any_status(x,a1,a2,o) -> (f x a1 a2 o))
+))))
+;;
+
+let any_status_rect =
+(function m -> (function m1 -> (function f -> (function a ->
+(match a with
+ Mk_any_status(x,a1,a2,o) -> (f x a1 a2 o))
+))))
+;;
+
+let alu =
+(function mcu -> (function t -> (function w ->
+(match w with
+ Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> alu)
+)))
+;;
+
+let mem_desc =
+(function mcu -> (function t -> (function w ->
+(match w with
+ Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> mem_desc)
+)))
+;;
+
+let chk_desc =
+(function mcu -> (function t -> (function w ->
+(match w with
+ Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> chk_desc)
+)))
+;;
+
+let clk_desc =
+(function mcu -> (function t -> (function w ->
+(match w with
+ Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> clk_desc)
+)))
+;;
+
+type ('x) aux_get_typing = (unit (* TOO POLYMORPHIC TYPE *) -> 'x)
+;;
+
+let get_acc_8_low_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (acc_low_reg_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (acc_low_reg_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (acc_low_reg_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (acc_low_reg_RS08))
+ (alu m t s)))))
+;;
+
+let get_indX_8_low_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC05 alu)))))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_indX_8_high_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_high_reg_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_high_reg_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_indX_16_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((indX_high_reg_HC08 alu),(indX_low_reg_HC08 alu)))))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((indX_high_reg_HC08 alu),(indX_low_reg_HC08 alu)))))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_sp_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC05 alu)))))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_pc_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (pc_reg_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (pc_reg_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (pc_reg_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (pc_reg_RS08))
+ (alu m t s)))))
+;;
+
+let get_spc_reg =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((spc_reg_RS08 alu))))))
+ (alu m t s)))))
+;;
+
+let get_x_map =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((x_map_RS08 alu))))))
+ (alu m t s)))))
+;;
+
+let get_ps_map =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((ps_map_RS08 alu))))))
+ (alu m t s)))))
+;;
+
+let get_v_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((v_flag_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((v_flag_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_h_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC05 alu)))))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_i_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC05 alu)))))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_n_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC05 alu)))))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_z_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (z_flag_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (z_flag_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (z_flag_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (z_flag_RS08))
+ (alu m t s)))))
+;;
+
+let get_c_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (c_flag_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (c_flag_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (c_flag_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (c_flag_RS08))
+ (alu m t s)))))
+;;
+
+let get_irq_flag =
+(function m -> (function t -> (function s -> (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC05 alu)))))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC08 alu)))))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC08 alu)))))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
+ (alu m t s)))))
+;;
+
+let get_alu =
+(function m -> (function t -> (function s -> (alu m t s))))
+;;
+
+let get_mem_desc =
+(function m -> (function t -> (function s -> (mem_desc m t s))))
+;;
+
+let get_chk_desc =
+(function m -> (function t -> (function s -> (chk_desc m t s))))
+;;
+
+let get_clk_desc =
+(function m -> (function t -> (function s -> (clk_desc m t s))))
+;;
+
+type ('x) aux_set_typing = (unit (* TOO POLYMORPHIC TYPE *) -> ('x -> unit (* TOO POLYMORPHIC TYPE *)))
+;;
+
+type ('x) aux_set_typing_opt = ((unit (* TOO POLYMORPHIC TYPE *) -> ('x -> unit (* TOO POLYMORPHIC TYPE *)))) Matita_datatypes_constructors.option
+;;
+
+let set_alu =
+(function m -> (function t -> (function s -> (function alu' ->
+(match s with
+ Mk_any_status(_,mem,chk,clk) -> (Mk_any_status(alu',mem,chk,clk)))
+))))
+;;
+
+let set_mem_desc =
+(function m -> (function t -> (function s -> (function mem' ->
+(match s with
+ Mk_any_status(alu,_,chk,clk) -> (Mk_any_status(alu,mem',chk,clk)))
+))))
+;;
+
+let set_chk_desc =
+(function m -> (function t -> (function s -> (function chk' ->
+(match s with
+ Mk_any_status(alu,mem,_,clk) -> (Mk_any_status(alu,mem,chk',clk)))
+))))
+;;
+
+let set_clk_desc =
+(function m -> (function t -> (function s -> (function clk' ->
+(match s with
+ Mk_any_status(alu,mem,chk,_) -> (Mk_any_status(alu,mem,chk,clk')))
+))))
+;;
+
+let set_acc_8_low_reg_HC05 =
+(function alu -> (function acclow' ->
+(match alu with
+ Mk_alu_HC05(_,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow',indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_acc_8_low_reg_HC08 =
+(function alu -> (function acclow' ->
+(match alu with
+ Mk_alu_HC08(_,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow',indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_acc_8_low_reg_RS08 =
+(function alu -> (function acclow' ->
+(match alu with
+ Mk_alu_RS08(_,pc,pcm,spc,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow',pc,pcm,spc,xm,psm,zfl,cfl)))
+))
+;;
+
+let set_acc_8_low_reg =
+(function m -> (function t -> (function s -> (function acclow' -> (set_alu m t s (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (set_acc_8_low_reg_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (set_acc_8_low_reg_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (set_acc_8_low_reg_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (set_acc_8_low_reg_RS08))
+ (alu m t s) acclow'))))))
+;;
+
+let set_indX_8_low_reg_HC05 =
+(function alu -> (function indxlow' ->
+(match alu with
+ Mk_alu_HC05(acclow,_,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow',sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_indX_8_low_reg_HC08 =
+(function alu -> (function indxlow' ->
+(match alu with
+ Mk_alu_HC08(acclow,_,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow',indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_indX_8_low_reg =
+(function m -> (function t -> (function s -> (function indxlow' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC05)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indxlow'))))))))))
+;;
+
+let setweak_indX_8_low_reg =
+(function m -> (function t -> (function s -> (function indxlow' ->
+(match (set_indX_8_low_reg m t s indxlow') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_indX_8_high_reg_HC08 =
+(function alu -> (function indxhigh' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,_,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh',sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_indX_8_high_reg =
+(function m -> (function t -> (function s -> (function indxhigh' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_high_reg_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_high_reg_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indxhigh'))))))))))
+;;
+
+let setweak_indX_8_high_reg =
+(function m -> (function t -> (function s -> (function indxhigh' ->
+(match (set_indX_8_high_reg m t s indxhigh') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_indX_16_reg_HC08 =
+(function alu -> (function indx16 ->
+(match alu with
+ Mk_alu_HC08(acclow,_,_,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,(Matita_freescale_word16.w16l indx16),(Matita_freescale_word16.w16h indx16),sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_indX_16_reg =
+(function m -> (function t -> (function s -> (function indx16 -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_16_reg_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_16_reg_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indx16))))))))))
+;;
+
+let setweak_indX_16_reg =
+(function m -> (function t -> (function s -> (function indx16 ->
+(match (set_indX_16_reg m t s indx16) with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_sp_reg_HC05 =
+(function alu -> (function sp' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,_,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,(Matita_freescale_word16.or_w16 (Matita_freescale_word16.and_w16 sp' spm) spf),spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_sp_reg_HC08 =
+(function alu -> (function sp' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,_,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp',pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_sp_reg =
+(function m -> (function t -> (function s -> (function sp' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC05)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) sp'))))))))))
+;;
+
+let setweak_sp_reg =
+(function m -> (function t -> (function s -> (function sp' ->
+(match (set_sp_reg m t s sp') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_pc_reg_HC05 =
+(function alu -> (function pc' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,_,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,(Matita_freescale_word16.and_w16 pc' pcm),pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_pc_reg_HC08 =
+(function alu -> (function pc' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,_,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc',vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_pc_reg_RS08 =
+(function alu -> (function pc' ->
+(match alu with
+ Mk_alu_RS08(acclow,_,pcm,spc,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,(Matita_freescale_word16.and_w16 pc' pcm),pcm,spc,xm,psm,zfl,cfl)))
+))
+;;
+
+let set_pc_reg =
+(function m -> (function t -> (function s -> (function pc' -> (set_alu m t s (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (set_pc_reg_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (set_pc_reg_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (set_pc_reg_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (set_pc_reg_RS08))
+ (alu m t s) pc'))))))
+;;
+
+let set_spc_reg_RS08 =
+(function alu -> (function spc' ->
+(match alu with
+ Mk_alu_RS08(acclow,pc,pcm,_,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,(Matita_freescale_word16.and_w16 spc' pcm),xm,psm,zfl,cfl)))
+))
+;;
+
+let set_spc_reg =
+(function m -> (function t -> (function s -> (function spc' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_spc_reg_RS08))))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) spc'))))))))))
+;;
+
+let setweak_spc_reg =
+(function m -> (function t -> (function s -> (function spc' ->
+(match (set_spc_reg m t s spc') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_x_map_RS08 =
+(function alu -> (function xm' ->
+(match alu with
+ Mk_alu_RS08(acclow,pc,pcm,spc,_,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm',psm,zfl,cfl)))
+))
+;;
+
+let set_x_map =
+(function m -> (function t -> (function s -> (function xm' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_x_map_RS08))))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) xm'))))))))))
+;;
+
+let setweak_x_map =
+(function m -> (function t -> (function s -> (function xm' ->
+(match (set_x_map m t s xm') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_ps_map_RS08 =
+(function alu -> (function psm' ->
+(match alu with
+ Mk_alu_RS08(acclow,pc,pcm,spc,xm,_,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm',zfl,cfl)))
+))
+;;
+
+let set_ps_map =
+(function m -> (function t -> (function s -> (function psm' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_ps_map_RS08))))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) psm'))))))))))
+;;
+
+let setweak_ps_map =
+(function m -> (function t -> (function s -> (function psm' ->
+(match (set_ps_map m t s psm') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_v_flag_HC08 =
+(function alu -> (function vfl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,_,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl',hfl,ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_v_flag =
+(function m -> (function t -> (function s -> (function vfl' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_v_flag_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_v_flag_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) vfl'))))))))))
+;;
+
+let setweak_v_flag =
+(function m -> (function t -> (function s -> (function vfl' ->
+(match (set_v_flag m t s vfl') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_h_flag_HC05 =
+(function alu -> (function hfl' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,_,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl',ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_h_flag_HC08 =
+(function alu -> (function hfl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,_,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl',ifl,nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_h_flag =
+(function m -> (function t -> (function s -> (function hfl' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC05)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) hfl'))))))))))
+;;
+
+let setweak_h_flag =
+(function m -> (function t -> (function s -> (function hfl' ->
+(match (set_h_flag m t s hfl') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_i_flag_HC05 =
+(function alu -> (function ifl' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,_,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl',nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_i_flag_HC08 =
+(function alu -> (function ifl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,_,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl',nfl,zfl,cfl,irqfl)))
+))
+;;
+
+let set_i_flag =
+(function m -> (function t -> (function s -> (function ifl' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC05)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) ifl'))))))))))
+;;
+
+let setweak_i_flag =
+(function m -> (function t -> (function s -> (function ifl' ->
+(match (set_i_flag m t s ifl') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_n_flag_HC05 =
+(function alu -> (function nfl' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,_,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl',zfl,cfl,irqfl)))
+))
+;;
+
+let set_n_flag_HC08 =
+(function alu -> (function nfl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,_,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl',zfl,cfl,irqfl)))
+))
+;;
+
+let set_n_flag =
+(function m -> (function t -> (function s -> (function nfl' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC05)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) nfl'))))))))))
+;;
+
+let setweak_n_flag =
+(function m -> (function t -> (function s -> (function nfl' ->
+(match (set_n_flag m t s nfl') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let set_z_flag_HC05 =
+(function alu -> (function zfl' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,_,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl',cfl,irqfl)))
+))
+;;
+
+let set_z_flag_HC08 =
+(function alu -> (function zfl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,_,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl',cfl,irqfl)))
+))
+;;
+
+let set_z_flag_RS08 =
+(function alu -> (function zfl' ->
+(match alu with
+ Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,_,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl',cfl)))
+))
+;;
+
+let set_z_flag =
+(function m -> (function t -> (function s -> (function zfl' -> (set_alu m t s (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (set_z_flag_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (set_z_flag_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (set_z_flag_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (set_z_flag_RS08))
+ (alu m t s) zfl'))))))
+;;
+
+let set_c_flag_HC05 =
+(function alu -> (function cfl' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,_,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl',irqfl)))
+))
+;;
+
+let set_c_flag_HC08 =
+(function alu -> (function cfl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,_,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl',irqfl)))
+))
+;;
+
+let set_c_flag_RS08 =
+(function alu -> (function cfl' ->
+(match alu with
+ Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,_) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl')))
+))
+;;
+
+let set_c_flag =
+(function m -> (function t -> (function s -> (function cfl' -> (set_alu m t s (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (set_c_flag_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (set_c_flag_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (set_c_flag_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (set_c_flag_RS08))
+ (alu m t s) cfl'))))))
+;;
+
+let set_irq_flag_HC05 =
+(function alu -> (function irqfl' ->
+(match alu with
+ Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,_) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl')))
+))
+;;
+
+let set_irq_flag_HC08 =
+(function alu -> (function irqfl' ->
+(match alu with
+ Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,_) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl')))
+))
+;;
+
+let set_irq_flag =
+(function m -> (function t -> (function s -> (function irqfl' -> (Matita_freescale_extra.opt_map
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC05)))
+ | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC08)))
+ | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC08)))
+ | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
+ (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) irqfl'))))))))))
+;;
+
+let setweak_irq_flag =
+(function m -> (function t -> (function s -> (function irqfl' ->
+(match (set_irq_flag m t s irqfl') with
+ Matita_datatypes_constructors.None -> s
+ | Matita_datatypes_constructors.Some(s') -> s')
+))))
+;;
+
+let eq_alu_HC05 =
+(function alu1 -> (function alu2 ->
+(match alu1 with
+ Mk_alu_HC05(acclow1,indxlow1,sp1,spm1,spf1,pc1,pcm1,hfl1,ifl1,nfl1,zfl1,cfl1,irqfl1) ->
+(match alu2 with
+ Mk_alu_HC05(acclow2,indxlow2,sp2,spm2,spf2,pc2,pcm2,hfl2,ifl2,nfl2,zfl2,cfl2,irqfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_byte8.eq_b8 indxlow1 indxlow2)) (Matita_freescale_word16.eq_w16 sp1 sp2)) (Matita_freescale_word16.eq_w16 spm1 spm2)) (Matita_freescale_word16.eq_w16 spf1 spf2)) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_word16.eq_w16 pcm1 pcm2)) (Matita_freescale_extra.eq_bool hfl1 hfl2)) (Matita_freescale_extra.eq_bool ifl1 ifl2)) (Matita_freescale_extra.eq_bool nfl1 nfl2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)) (Matita_freescale_extra.eq_bool irqfl1 irqfl2)))
+)
+))
+;;
+
+let eq_alu_HC08 =
+(function alu1 -> (function alu2 ->
+(match alu1 with
+ Mk_alu_HC08(acclow1,indxlow1,indxhigh1,sp1,pc1,vfl1,hfl1,ifl1,nfl1,zfl1,cfl1,irqfl1) ->
+(match alu2 with
+ Mk_alu_HC08(acclow2,indxlow2,indxhigh2,sp2,pc2,vfl2,hfl2,ifl2,nfl2,zfl2,cfl2,irqfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_byte8.eq_b8 indxlow1 indxlow2)) (Matita_freescale_byte8.eq_b8 indxhigh1 indxhigh2)) (Matita_freescale_word16.eq_w16 sp1 sp2)) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_extra.eq_bool vfl1 vfl2)) (Matita_freescale_extra.eq_bool hfl1 hfl2)) (Matita_freescale_extra.eq_bool ifl1 ifl2)) (Matita_freescale_extra.eq_bool nfl1 nfl2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)) (Matita_freescale_extra.eq_bool irqfl1 irqfl2)))
+)
+))
+;;
+
+let eq_alu_RS08 =
+(function alu1 -> (function alu2 ->
+(match alu1 with
+ Mk_alu_RS08(acclow1,pc1,pcm1,spc1,xm1,psm1,zfl1,cfl1) ->
+(match alu2 with
+ Mk_alu_RS08(acclow2,pc2,pcm2,spc2,xm2,psm2,zfl2,cfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_word16.eq_w16 pcm1 pcm2)) (Matita_freescale_word16.eq_w16 spc1 spc2)) (Matita_freescale_byte8.eq_b8 xm1 xm2)) (Matita_freescale_byte8.eq_b8 psm1 psm2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)))
+)
+))
+;;
+
+let eq_b8_opt =
+(function b1 -> (function b2 ->
+(match b1 with
+ Matita_datatypes_constructors.None ->
+(match b2 with
+ Matita_datatypes_constructors.None -> Matita_datatypes_bool.True
+ | Matita_datatypes_constructors.Some(_) -> Matita_datatypes_bool.False)
+
+ | Matita_datatypes_constructors.Some(b1') ->
+(match b2 with
+ Matita_datatypes_constructors.None -> Matita_datatypes_bool.False
+ | Matita_datatypes_constructors.Some(b2') -> (Matita_freescale_byte8.eq_b8 b1' b2'))
+)
+))
+;;
+
+let forall_memory_ranged =
+let rec forall_memory_ranged =
+(function t -> (function chk1 -> (function chk2 -> (function mem1 -> (function mem2 -> (function inf -> (function n ->
+(match n with
+ Matita_nat_nat.O -> (eq_b8_opt (Matita_freescale_memory_abs.mem_read t mem1 chk1 inf) (Matita_freescale_memory_abs.mem_read t mem2 chk2 inf))
+ | Matita_nat_nat.S(n') -> (Matita_freescale_extra.and_bool (eq_b8_opt (Matita_freescale_memory_abs.mem_read t mem1 chk1 (Matita_freescale_word16.plus_w16nc inf (Matita_freescale_word16.word16_of_nat n))) (Matita_freescale_memory_abs.mem_read t mem2 chk2 (Matita_freescale_word16.plus_w16nc inf (Matita_freescale_word16.word16_of_nat n)))) (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')))
+))))))) in forall_memory_ranged
+;;
+
+let eq_clk =
+(function m -> (function c1 -> (function c2 ->
+(match c1 with
+ Matita_datatypes_constructors.None ->
+(match c2 with
+ Matita_datatypes_constructors.None -> Matita_datatypes_bool.True
+ | Matita_datatypes_constructors.Some(_) -> Matita_datatypes_bool.False)
+
+ | Matita_datatypes_constructors.Some(c1') ->
+(match c2 with
+ Matita_datatypes_constructors.None -> Matita_datatypes_bool.False
+ | Matita_datatypes_constructors.Some(c2') -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 (Matita_freescale_extra.fst5T c1') (Matita_freescale_extra.fst5T c2')) (Matita_freescale_opcode.eqop m (Matita_freescale_extra.snd5T c1') (Matita_freescale_extra.snd5T c2'))) (Matita_freescale_opcode.eqim (Matita_freescale_extra.thd5T c1') (Matita_freescale_extra.thd5T c2'))) (Matita_freescale_byte8.eq_b8 (Matita_freescale_extra.frth5T c1') (Matita_freescale_extra.frth5T c2'))) (Matita_freescale_word16.eq_w16 (Matita_freescale_extra.ffth5T c1') (Matita_freescale_extra.ffth5T c2'))))
+)
+)))
+;;
+
+let eq_status =
+(function m -> (function t -> (function s1 -> (function s2 -> (function inf -> (function n ->
+(match s1 with
+ Mk_any_status(alu1,mem1,chk1,clk1) ->
+(match s2 with
+ Mk_any_status(alu2,mem2,chk2,clk2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (
+(match m with
+ Matita_freescale_opcode.HC05 -> Obj.magic (eq_alu_HC05)
+ | Matita_freescale_opcode.HC08 -> Obj.magic (eq_alu_HC08)
+ | Matita_freescale_opcode.HCS08 -> Obj.magic (eq_alu_HC08)
+ | Matita_freescale_opcode.RS08 -> Obj.magic (eq_alu_RS08))
+ alu1 alu2) (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n)) (eq_clk m clk1 clk2)))
+)
+))))))
+;;
+
projects / helm.git / blobdiff