- setters for data structures now support "commuting conversion"-like

[helm.git] / helm / software / matita / contribs / assembly / freescale / status.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/status.ma b/helm/software/matita/contribs/assembly/freescale/status.ma
index 4072f445fa02952d817490c05532ba1d7d0dbe5e..e630438dc32b6af51855be797ab37a13cd1422ad 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/assembly/freescale/status.ma
@@ -397,44 +397,74 @@ definition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
 
 (* setter forte della ALU *)
 definition set_alu ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.match s with
- [ mk_any_status _ mem chk clk ⇒ mk_any_status m t alu' mem chk clk ].
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
+ mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
 
 (* setter forte della memoria *)
 definition set_mem_desc ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.match s with
- [ mk_any_status alu _ chk clk ⇒ mk_any_status m t alu mem' chk clk ].
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
+ mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
 
 (* setter forte del descrittore *)
 definition set_chk_desc ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.match s with
- [ mk_any_status alu mem _ clk ⇒ mk_any_status m t alu mem chk' clk ].
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
+ mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
 
 (* setter forte del clik *)
 definition set_clk_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
-λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).match s with
- [ mk_any_status alu mem chk _ ⇒ mk_any_status m t alu mem chk clk' ].
+λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
+ mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
 
 (* REGISTRO A *)
 
 (* setter specifico HC05 di A *)
 definition set_acc_8_low_reg_HC05 ≝
-λalu.λacclow':byte8.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 ].
+λalu.λacclow':byte8.
+ mk_alu_HC05
+  acclow'
+  (indX_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di A *)
 definition set_acc_8_low_reg_HC08 ≝
-λalu.λacclow':byte8.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 ].
+λalu.λacclow':byte8.
+ mk_alu_HC08
+  acclow'
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter specifico RS08 di A *)
 definition set_acc_8_low_reg_RS08 ≝ 
-λalu.λacclow':byte8.match alu with 
- [ mk_alu_RS08 _ pc pcm spc xm psm zfl cfl ⇒
-  mk_alu_RS08 acclow' pc pcm spc xm psm zfl cfl ].
+λalu.λacclow':byte8.
+ mk_alu_RS08
+  acclow'
+  (pc_reg_RS08 alu)
+  (pc_mask_RS08 alu)
+  (spc_reg_RS08 alu)
+  (x_map_RS08 alu)
+  (ps_map_RS08 alu)
+  (z_flag_RS08 alu)
+  (c_flag_RS08 alu).
 
 (* setter forte di A *)
 definition set_acc_8_low_reg ≝
@@ -451,15 +481,38 @@ definition set_acc_8_low_reg ≝
 
 (* setter specifico HC05 di X *)
 definition set_indX_8_low_reg_HC05 ≝
-λalu.λindxlow':byte8.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 ].
+λalu.λindxlow':byte8.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  indxlow'
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di X *)
 definition set_indX_8_low_reg_HC08 ≝
-λalu.λindxlow':byte8.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 ].
+λalu.λindxlow':byte8.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  indxlow'
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di X *)
 definition set_indX_8_low_reg ≝
@@ -481,9 +534,20 @@ definition setweak_indX_8_low_reg ≝
 
 (* setter specifico HC08/HCS08 di H *)
 definition set_indX_8_high_reg_HC08 ≝
-λalu.λindxhigh':byte8.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 ].
+λalu.λindxhigh':byte8.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  indxhigh'
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di H *)
 definition set_indX_8_high_reg ≝
@@ -505,9 +569,20 @@ definition setweak_indX_8_high_reg ≝
 
 (* setter specifico HC08/HCS08 di H:X *)
 definition set_indX_16_reg_HC08 ≝
-λalu.λindx16:word16.match alu with 
- [ mk_alu_HC08 acclow _ _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
-  mk_alu_HC08 acclow (w16l indx16) (w16h indx16) sp pc vfl hfl ifl nfl zfl cfl irqfl ].
+λalu.λindx16:word16.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (w16l indx16)
+  (w16h indx16)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di H:X *)
 definition set_indX_16_reg ≝
@@ -529,15 +604,38 @@ definition setweak_indX_16_reg ≝
 
 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
 definition set_sp_reg_HC05 ≝
-λalu.λsp':word16.match alu with 
- [ mk_alu_HC05 acclow indxlow _ spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
-  mk_alu_HC05 acclow indxlow (or_w16 (and_w16 sp' spm) spf) spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
+λalu.λsp':word16.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di SP *)
 definition set_sp_reg_HC08 ≝
-λalu.λsp':word16.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 ].
+λalu.λsp':word16.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  sp'
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di SP *)
 definition set_sp_reg ≝
@@ -559,21 +657,51 @@ definition setweak_sp_reg ≝
 
 (* setter specifico HC05 di PC, effettua PC∧mask *)
 definition set_pc_reg_HC05 ≝
-λalu.λpc':word16.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 (and_w16 pc' pcm) pcm hfl ifl nfl zfl cfl irqfl ].
+λalu.λpc':word16.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (and_w16 pc' (pc_mask_HC05 alu))
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di PC *)
 definition set_pc_reg_HC08 ≝
-λalu.λpc':word16.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 ].
+λalu.λpc':word16.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  pc'
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter specifico RS08 di PC, effettua PC∧mask *)
 definition set_pc_reg_RS08 ≝ 
-λalu.λpc':word16.match alu with 
- [ mk_alu_RS08 acclow _ pcm spc xm psm zfl cfl ⇒
-  mk_alu_RS08 acclow (and_w16 pc' pcm) pcm spc xm psm zfl cfl ].
+λalu.λpc':word16.
+ mk_alu_RS08
+  (acc_low_reg_RS08 alu)
+  (and_w16 pc' (pc_mask_RS08 alu))
+  (pc_mask_RS08 alu)
+  (spc_reg_RS08 alu)
+  (x_map_RS08 alu)
+  (ps_map_RS08 alu)
+  (z_flag_RS08 alu)
+  (c_flag_RS08 alu).
 
 (* setter forte di PC *)
 definition set_pc_reg ≝
@@ -590,9 +718,16 @@ definition set_pc_reg ≝
 
 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
 definition set_spc_reg_RS08 ≝ 
-λalu.λspc':word16.match alu with 
- [ mk_alu_RS08 acclow pc pcm _ xm psm zfl cfl ⇒
-  mk_alu_RS08 acclow pc pcm (and_w16 spc' pcm) xm psm zfl cfl ].
+λalu.λspc':word16.
+ mk_alu_RS08
+  (acc_low_reg_RS08 alu)
+  (pc_reg_RS08 alu)
+  (pc_mask_RS08 alu)
+  (and_w16 spc' (pc_mask_RS08 alu))
+  (x_map_RS08 alu)
+  (ps_map_RS08 alu)
+  (z_flag_RS08 alu)
+  (c_flag_RS08 alu).
 
 (* setter forte di SPC *)
 definition set_spc_reg ≝
@@ -614,9 +749,16 @@ definition setweak_spc_reg ≝
 
 (* setter specifico RS08 di memory mapped X *)
 definition set_x_map_RS08 ≝ 
-λalu.λxm':byte8.match alu with 
- [ mk_alu_RS08 acclow pc pcm spc _ psm zfl cfl ⇒
-  mk_alu_RS08 acclow pc pcm spc xm' psm zfl cfl ].
+λalu.λxm':byte8.
+ mk_alu_RS08
+  (acc_low_reg_RS08 alu)
+  (pc_reg_RS08 alu)
+  (pc_mask_RS08 alu)
+  (spc_reg_RS08 alu)
+  xm'
+  (ps_map_RS08 alu)
+  (z_flag_RS08 alu)
+  (c_flag_RS08 alu).
 
 (* setter forte di memory mapped X *)
 definition set_x_map ≝
@@ -638,9 +780,16 @@ definition setweak_x_map ≝
 
 (* setter specifico RS08 di memory mapped PS *)
 definition set_ps_map_RS08 ≝ 
-λalu.λpsm':byte8.match alu with 
- [ mk_alu_RS08 acclow pc pcm spc xm _ zfl cfl ⇒
-  mk_alu_RS08 acclow pc pcm spc xm psm' zfl cfl ].
+λalu.λpsm':byte8.
+ mk_alu_RS08
+  (acc_low_reg_RS08 alu)
+  (pc_reg_RS08 alu)
+  (pc_mask_RS08 alu)
+  (spc_reg_RS08 alu)
+  (x_map_RS08 alu)
+  psm'
+  (z_flag_RS08 alu)
+  (c_flag_RS08 alu).
 
 (* setter forte di memory mapped PS *)
 definition set_ps_map ≝
@@ -662,9 +811,20 @@ definition setweak_ps_map ≝
 
 (* setter specifico HC08/HCS08 di V *)
 definition set_v_flag_HC08 ≝
-λalu.λvfl':bool.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 ].
+λalu.λvfl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  vfl'
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di V *)
 definition set_v_flag ≝
@@ -686,15 +846,38 @@ definition setweak_v_flag ≝
 
 (* setter specifico HC05 di H *)
 definition set_h_flag_HC05 ≝
-λalu.λhfl':bool.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 ].
+λalu.λhfl':bool.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  hfl'
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di H *)
 definition set_h_flag_HC08 ≝
-λalu.λhfl':bool.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 ].
+λalu.λhfl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  hfl'
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di H *)
 definition set_h_flag ≝
@@ -716,15 +899,38 @@ definition setweak_h_flag ≝
 
 (* setter specifico HC05 di I *)
 definition set_i_flag_HC05 ≝
-λalu.λifl':bool.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 ].
+λalu.λifl':bool.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  ifl'
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di I *)
 definition set_i_flag_HC08 ≝
-λalu.λifl':bool.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 ].
+λalu.λifl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  ifl'
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di I *)
 definition set_i_flag ≝
@@ -746,15 +952,38 @@ definition setweak_i_flag ≝
 
 (* setter specifico HC05 di N *)
 definition set_n_flag_HC05 ≝
-λalu.λnfl':bool.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 ].
+λalu.λnfl':bool.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  nfl'
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di N *)
 definition set_n_flag_HC08 ≝
-λalu.λnfl':bool.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 ].
+λalu.λnfl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  nfl'
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter forte di N *)
 definition set_n_flag ≝
@@ -776,21 +1005,51 @@ definition setweak_n_flag ≝
 
 (* setter specifico HC05 di Z *)
 definition set_z_flag_HC05 ≝
-λalu.λzfl':bool.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 ].
+λalu.λzfl':bool.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  zfl'
+  (c_flag_HC05 alu)
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di Z *)
 definition set_z_flag_HC08 ≝
-λalu.λzfl':bool.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 ].
+λalu.λzfl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  zfl'
+  (c_flag_HC08 alu)
+  (irq_flag_HC08 alu).
 
 (* setter sprcifico RS08 di Z *)
 definition set_z_flag_RS08 ≝ 
-λalu.λzfl':bool.match alu with 
- [ mk_alu_RS08 acclow pc pcm spc xm psm _ cfl ⇒
-  mk_alu_RS08 acclow pc pcm spc xm psm zfl' cfl ].
+λalu.λzfl':bool.
+ mk_alu_RS08
+  (acc_low_reg_RS08 alu)
+  (pc_reg_RS08 alu)
+  (pc_mask_RS08 alu)
+  (spc_reg_RS08 alu)
+  (x_map_RS08 alu)
+  (ps_map_RS08 alu)
+  zfl'
+  (c_flag_RS08 alu).
 
 (* setter forte di Z *)
 definition set_z_flag ≝
@@ -807,21 +1066,51 @@ definition set_z_flag ≝
 
 (* setter specifico HC05 di C *)
 definition set_c_flag_HC05 ≝
-λalu.λcfl':bool.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 ].
+λalu.λcfl':bool.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  cfl'
+  (irq_flag_HC05 alu).
 
 (* setter specifico HC08/HCS08 di C *)
 definition set_c_flag_HC08 ≝
-λalu.λcfl':bool.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 ].
+λalu.λcfl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  cfl'
+  (irq_flag_HC08 alu).
 
 (* setter specifico RS08 di C *)
 definition set_c_flag_RS08 ≝ 
-λalu.λcfl':bool.match alu with 
- [ mk_alu_RS08 acclow pc pcm spc xm psm zfl _ ⇒
-  mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl' ].
+λalu.λcfl':bool.
+ mk_alu_RS08
+  (acc_low_reg_RS08 alu)
+  (pc_reg_RS08 alu)
+  (pc_mask_RS08 alu)
+  (spc_reg_RS08 alu)
+  (x_map_RS08 alu)
+  (ps_map_RS08 alu)
+  (z_flag_RS08 alu)
+  cfl'.
 
 (* setter forte di C *)
 definition set_c_flag ≝
@@ -838,15 +1127,38 @@ definition set_c_flag ≝
 
 (* setter specifico HC05 di IRQ *)
 definition set_irq_flag_HC05 ≝
-λalu.λirqfl':bool.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' ].
+λalu.λirqfl':bool.
+ mk_alu_HC05
+  (acc_low_reg_HC05 alu)
+  (indx_low_reg_HC05 alu)
+  (sp_reg_HC05 alu)
+  (sp_mask_HC05 alu)
+  (sp_fix_HC05 alu)
+  (pc_reg_HC05 alu)
+  (pc_mask_HC05 alu)
+  (h_flag_HC05 alu)
+  (i_flag_HC05 alu)
+  (n_flag_HC05 alu)
+  (z_flag_HC05 alu)
+  (c_flag_HC05 alu)
+  irqfl'.
 
 (* setter specifico HC08/HCS08 di IRQ *)
 definition set_irq_flag_HC08 ≝
-λalu.λirqfl':bool.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' ].
+λalu.λirqfl':bool.
+ mk_alu_HC08
+  (acc_low_reg_HC08 alu)
+  (indX_low_reg_HC08 alu)
+  (indX_high_reg_HC08 alu)
+  (sp_reg_HC08 alu)
+  (pc_reg_HC08 alu)
+  (v_flag_HC08 alu)
+  (h_flag_HC08 alu)
+  (i_flag_HC08 alu)
+  (n_flag_HC08 alu)
+  (z_flag_HC08 alu)
+  (c_flag_HC08 alu)
+  irqfl'.
 
 (* setter forte di IRQ *)
 definition set_irq_flag ≝