--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/status/status.ma".
+
+(* ***************************** *)
+(* SETTER SPECIFICI FORTI/DEBOLI *)
+(* ***************************** *)
+
+(* funzione ausiliaria per il tipaggio dei setter forti *)
+ndefinition aux_set_type ≝ λx:Type.λm:mcu_type.
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
+ → x →
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
+
+(* funzione ausiliaria per il tipaggio dei setter deboli *)
+ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
+ (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
+ → x →
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
+
+(* DESCRITTORI ESTERNI ALLA ALU *)
+
+(* setter forte della ALU *)
+ndefinition set_alu ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
+ mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
+
+(* setter forte della memoria *)
+ndefinition set_mem_desc ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
+ mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
+
+(* setter forte del descrittore *)
+ndefinition set_chk_desc ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
+ mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
+
+(* setter forte del clik *)
+ndefinition set_clk_desc ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λclk':option (aux_clk_type m).
+ mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
+
+(* REGISTRO A *)
+
+(* setter specifico HC05 di A *)
+ndefinition set_acc_8_low_reg_HC05 ≝
+λ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 *)
+ndefinition set_acc_8_low_reg_HC08 ≝
+λ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 *)
+ndefinition set_acc_8_low_reg_RS08 ≝
+λ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 *)
+ndefinition set_acc_8_low_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
+ set_alu m t s
+ (match m return aux_set_type byte8 with
+ [ HC05 ⇒ set_acc_8_low_reg_HC05
+ | HC08 ⇒ set_acc_8_low_reg_HC08
+ | HCS08 ⇒ set_acc_8_low_reg_HC08
+ | RS08 ⇒ set_acc_8_low_reg_RS08
+ ] (alu m t s) acclow').
+
+(* REGISTRO X *)
+
+(* setter specifico HC05 di X *)
+ndefinition set_indX_8_low_reg_HC05 ≝
+λ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 *)
+ndefinition set_indX_8_low_reg_HC08 ≝
+λ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 *)
+ndefinition set_indX_8_low_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+ [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
+ | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
+ | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
+
+(* setter debole di X *)
+ndefinition setweak_indX_8_low_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
+ match set_indX_8_low_reg m t s indxlow' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO H *)
+
+(* setter specifico HC08/HCS08 di H *)
+ndefinition set_indX_8_high_reg_HC08 ≝
+λ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 *)
+ndefinition set_indX_8_high_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
+ | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
+
+(* setter debole di H *)
+ndefinition setweak_indX_8_high_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
+ match set_indX_8_high_reg m t s indxhigh' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO H:X *)
+
+(* setter specifico HC08/HCS08 di H:X *)
+ndefinition set_indX_16_reg_HC08 ≝
+λ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 *)
+ndefinition set_indX_16_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ Some ? set_indX_16_reg_HC08
+ | HCS08 ⇒ Some ? set_indX_16_reg_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
+
+(* setter debole di H:X *)
+ndefinition setweak_indX_16_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
+ match set_indX_16_reg m t s indx16 with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO SP *)
+
+(* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
+ndefinition set_sp_reg_HC05 ≝
+λ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 *)
+ndefinition set_sp_reg_HC08 ≝
+λ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 *)
+ndefinition set_sp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ Some ? set_sp_reg_HC05
+ | HC08 ⇒ Some ? set_sp_reg_HC08
+ | HCS08 ⇒ Some ? set_sp_reg_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
+
+(* setter debole di SP *)
+ndefinition setweak_sp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
+ match set_sp_reg m t s sp' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO PC *)
+
+(* setter specifico HC05 di PC, effettua PC∧mask *)
+ndefinition set_pc_reg_HC05 ≝
+λ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 *)
+ndefinition set_pc_reg_HC08 ≝
+λ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 *)
+ndefinition set_pc_reg_RS08 ≝
+λ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 *)
+ndefinition set_pc_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
+ set_alu m t s
+ (match m return aux_set_type word16 with
+ [ HC05 ⇒ set_pc_reg_HC05
+ | HC08 ⇒ set_pc_reg_HC08
+ | HCS08 ⇒ set_pc_reg_HC08
+ | RS08 ⇒ set_pc_reg_RS08
+ ] (alu m t s) pc').
+
+(* REGISTRO SPC *)
+
+(* setter specifico RS08 di SPC, effettua SPC∧mask *)
+ndefinition set_spc_reg_RS08 ≝
+λ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 *)
+ndefinition set_spc_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ Some ? set_spc_reg_RS08 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
+
+(* setter debole di SPC *)
+ndefinition setweak_spc_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
+ match set_spc_reg m t s spc' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO MEMORY MAPPED X *)
+
+(* setter specifico RS08 di memory mapped X *)
+ndefinition set_x_map_RS08 ≝
+λ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 *)
+ndefinition set_x_map ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ Some ? set_x_map_RS08 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
+
+(* setter debole di memory mapped X *)
+ndefinition setweak_x_map ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
+ match set_x_map m t s xm' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO MEMORY MAPPED PS *)
+
+(* setter specifico RS08 di memory mapped PS *)
+ndefinition set_ps_map_RS08 ≝
+λ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 *)
+ndefinition set_ps_map ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ Some ? set_ps_map_RS08 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
+
+(* setter debole di memory mapped PS *)
+ndefinition setweak_ps_map ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
+ match set_ps_map m t s psm' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* FLAG V *)
+
+(* setter specifico HC08/HCS08 di V *)
+ndefinition set_v_flag_HC08 ≝
+λ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 *)
+ndefinition set_v_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ Some ? set_v_flag_HC08
+ | HCS08 ⇒ Some ? set_v_flag_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
+
+(* setter debole di V *)
+ndefinition setweak_v_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
+ match set_v_flag m t s vfl' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* FLAG H *)
+
+(* setter specifico HC05 di H *)
+ndefinition set_h_flag_HC05 ≝
+λ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 *)
+ndefinition set_h_flag_HC08 ≝
+λ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 *)
+ndefinition set_h_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+ [ HC05 ⇒ Some ? set_h_flag_HC05
+ | HC08 ⇒ Some ? set_h_flag_HC08
+ | HCS08 ⇒ Some ? set_h_flag_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
+
+(* setter debole di H *)
+ndefinition setweak_h_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
+ match set_h_flag m t s hfl' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* FLAG I *)
+
+(* setter specifico HC05 di I *)
+ndefinition set_i_flag_HC05 ≝
+λ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 *)
+ndefinition set_i_flag_HC08 ≝
+λ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 *)
+ndefinition set_i_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+ [ HC05 ⇒ Some ? set_i_flag_HC05
+ | HC08 ⇒ Some ? set_i_flag_HC08
+ | HCS08 ⇒ Some ? set_i_flag_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
+
+(* setter debole di I *)
+ndefinition setweak_i_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
+ match set_i_flag m t s ifl' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* FLAG N *)
+
+(* setter specifico HC05 di N *)
+ndefinition set_n_flag_HC05 ≝
+λ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 *)
+ndefinition set_n_flag_HC08 ≝
+λ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 *)
+ndefinition set_n_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+ [ HC05 ⇒ Some ? set_n_flag_HC05
+ | HC08 ⇒ Some ? set_n_flag_HC08
+ | HCS08 ⇒ Some ? set_n_flag_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
+
+(* setter debole di N *)
+ndefinition setweak_n_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
+ match set_n_flag m t s nfl' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* FLAG Z *)
+
+(* setter specifico HC05 di Z *)
+ndefinition set_z_flag_HC05 ≝
+λ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 *)
+ndefinition set_z_flag_HC08 ≝
+λ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 *)
+ndefinition set_z_flag_RS08 ≝
+λ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 *)
+ndefinition set_z_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
+ set_alu m t s
+ (match m return aux_set_type bool with
+ [ HC05 ⇒ set_z_flag_HC05
+ | HC08 ⇒ set_z_flag_HC08
+ | HCS08 ⇒ set_z_flag_HC08
+ | RS08 ⇒ set_z_flag_RS08
+ ] (alu m t s) zfl').
+
+(* FLAG C *)
+
+(* setter specifico HC05 di C *)
+ndefinition set_c_flag_HC05 ≝
+λ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 *)
+ndefinition set_c_flag_HC08 ≝
+λ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 *)
+ndefinition set_c_flag_RS08 ≝
+λ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 *)
+ndefinition set_c_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
+ set_alu m t s
+ (match m return aux_set_type bool with
+ [ HC05 ⇒ set_c_flag_HC05
+ | HC08 ⇒ set_c_flag_HC08
+ | HCS08 ⇒ set_c_flag_HC08
+ | RS08 ⇒ set_c_flag_RS08
+ ] (alu m t s) cfl').
+
+(* FLAG IRQ *)
+
+(* setter specifico HC05 di IRQ *)
+ndefinition set_irq_flag_HC05 ≝
+λ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 *)
+ndefinition set_irq_flag_HC08 ≝
+λ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 *)
+ndefinition set_irq_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+ [ HC05 ⇒ Some ? set_irq_flag_HC05
+ | HC08 ⇒ Some ? set_irq_flag_HC08
+ | HCS08 ⇒ Some ? set_irq_flag_HC08
+ | RS08 ⇒ None ? ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
+
+(* setter debole di IRQ *)
+ndefinition setweak_irq_flag ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
+ match set_irq_flag m t s irqfl' with
+ [ None ⇒ s | Some s' ⇒ s' ].
projects / helm.git / blobdiff