mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / status / HC05_status.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma
old mode 100755 (executable)
new mode 100644 (file)
index 4e73b57..b6367ab
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma
@@ -68,6 +68,190 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg'
 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow 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).
 
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* 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 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 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 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 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 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 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 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 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 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'.
+
 (* ***************** *)
 (* CONFRONTO FRA ALU *)
 (* ***************** *)