X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2FHC08_status.ma;h=dd8234161ad4e5f7ce25c66202d776e2951a7cb3;hb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;hp=8c6ab8f85a774324c19657233315ef8b64c62f8d;hpb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma
index 8c6ab8f85..dd8234161 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma
@@ -63,6 +63,231 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg'
 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow 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).
 
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* 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 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 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 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 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 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 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 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 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 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 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 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 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'.
+
 (* ***************** *)
 (* CONFRONTO FRA ALU *)
 (* ***************** *)