(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝
(* 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 ≝