X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_status.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_status.ml;h=728d3abe594602374b017701ba14e4a8fc7b2799;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_status.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_status.ml new file mode 100644 index 000000000..728d3abe5 --- /dev/null +++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_status.ml @@ -0,0 +1,1097 @@ +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))) +) +)))))) +;; +