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 ad920e7..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
@@ -42,11 +42,11 @@ ndefinition new_callstack ≝
 
 ndefinition pop_callstack ≝
 λcs:aux_callstack_type.
- pair ?? (a16_1 ? cs)
-         (mk_Array16T ? (a16_2 ? cs)  (a16_3 ? cs)  (a16_4 ? cs)  (a16_5 ? cs)
-                        (a16_6 ? cs)  (a16_7 ? cs)  (a16_8 ? cs)  (a16_9 ? cs)
-                        (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
-                        (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
+ pair … (a16_1 ? cs)
+        (mk_Array16T ? (a16_2 ? cs)  (a16_3 ? cs)  (a16_4 ? cs)  (a16_5 ? cs)
+                       (a16_6 ? cs)  (a16_7 ? cs)  (a16_8 ? cs)  (a16_9 ? cs)
+                       (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
+                       (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
 
 ndefinition push_callstack ≝
 λcs:aux_callstack_type.λtop.
@@ -66,19 +66,13 @@ ndefinition new_addrarray ≝
               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
 
-ndefinition get_low3bits ≝
-λaddrsel:byte8.
- match cnL ? addrsel with
-  [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
-  | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
-
 ndefinition get_addrarray ≝
 λaddrsel:byte8.λaa:aux_addrarray_type.
- getn_array8T (get_low3bits addrsel) ? aa.
+ getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
 
 ndefinition set_addrarray ≝
 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
- setn_array8T (get_low3bits addrsel) ? aa v.
+ setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -221,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.
@@ -242,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
@@ -262,6 +282,10 @@ ndefinition push_call_reg_IP2022 ≝
   (c_flag_IP2022 alu)
   (skip_mode_IP2022 alu).
 
+ndefinition pop_call_reg_IP2022 ≝
+λ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 ≝
 λalu.λip':word16.