mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
old mode 100755 (executable)
new mode 100644 (file)
index 875ee24..4a4a20e
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
@@ -215,6 +215,9 @@ ndefinition set_addr_reg_IP2022 ≝
   (c_flag_IP2022 alu)
   (skip_mode_IP2022 alu).
 
+ndefinition get_addr_reg_IP2022 ≝
+λalu.get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu).
+
 (* setter specifico IP2022 di CALL *)
 ndefinition set_call_reg_IP2022 ≝
 λalu.λcall':word16.
@@ -236,6 +239,29 @@ ndefinition set_call_reg_IP2022 ≝
   (c_flag_IP2022 alu)
   (skip_mode_IP2022 alu).
 
+ndefinition get_call_reg_IP2022 ≝
+λalu.getn_array16T x0 ? (call_stack_IP2022 alu).
+
+ndefinition set_call_stack_IP2022 ≝
+λalu.λcall':aux_callstack_type.
+ mk_alu_IP2022
+  (acc_low_reg_IP2022 alu)
+  (mulh_reg_IP2022 alu)
+  (addrsel_reg_IP2022 alu)
+  (addr_array_IP2022 alu)
+  call'
+  (ip_reg_IP2022 alu)
+  (dp_reg_IP2022 alu)
+  (data_reg_IP2022 alu)
+  (sp_reg_IP2022 alu)
+  (pc_reg_IP2022 alu)
+  (speed_reg_IP2022 alu)
+  (page_reg_IP2022 alu)
+  (h_flag_IP2022 alu)
+  (z_flag_IP2022 alu)
+  (c_flag_IP2022 alu)
+  (skip_mode_IP2022 alu).
+
 ndefinition push_call_reg_IP2022 ≝
 λalu.λcall':word16.
  mk_alu_IP2022
@@ -257,27 +283,8 @@ ndefinition push_call_reg_IP2022 ≝
   (skip_mode_IP2022 alu).
 
 ndefinition pop_call_reg_IP2022 ≝
-λalu.
- match pop_callstack (call_stack_IP2022 alu) with
-  [ pair val call' ⇒
- pair … val
-        (mk_alu_IP2022
-         (acc_low_reg_IP2022 alu)
-         (mulh_reg_IP2022 alu)
-         (addrsel_reg_IP2022 alu)
-         (addr_array_IP2022 alu)
-         call'
-         (ip_reg_IP2022 alu)
-         (dp_reg_IP2022 alu)
-         (data_reg_IP2022 alu)
-         (sp_reg_IP2022 alu)
-         (pc_reg_IP2022 alu)
-         (speed_reg_IP2022 alu)
-         (page_reg_IP2022 alu)
-         (h_flag_IP2022 alu)
-         (z_flag_IP2022 alu)
-         (c_flag_IP2022 alu)
-         (skip_mode_IP2022 alu)) ].
+λalu.match pop_callstack (call_stack_IP2022 alu) with
+      [ pair val call' ⇒ pair … val (set_call_stack_IP2022 alu call') ].
 
 (* setter specifico IP2022 di IP *)
 ndefinition set_ip_reg_IP2022 ≝