(no commit message)

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma
index 1f4e5aa5a64ac361c6f8765a9a7416578c233abf..b2c2b46a706066265e5ca044dbf13edbe6bc2c6d 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma
@@ -150,7 +150,7 @@ ndefinition get_addr_reg ≝
  | HC08 ⇒ λalu.None ?
  | HCS08 ⇒ λalu.None ?
  | RS08 ⇒ λalu.None ?
- | IP2022 ⇒ λalu.Some ? (get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu)) ]
+ | IP2022 ⇒ λalu.Some ? (get_addr_reg_IP2022 alu) ]
  (alu m t s).
 
 (* getter di CALL, non esiste sempre *)
@@ -162,39 +162,9 @@ ndefinition get_call_reg ≝
  | HC08 ⇒ λalu.None ?
  | HCS08 ⇒ λalu.None ?
  | RS08 ⇒ λalu.None ?
- | IP2022 ⇒ λalu.Some ? (getn_array16T x0 ? (call_stack_IP2022 alu)) ]
+ | IP2022 ⇒ λalu.Some ? (get_call_reg_IP2022 alu) ]
  (alu m t s).
 
-ndefinition pop_call_reg ≝
-λm:mcu_type.
- match m
-  return λm.Πt.any_status m t → (option (ProdT word16 (any_status m t))) with 
- [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
- | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
- | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
- | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
- | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
-  match pop_callstack (call_stack_IP2022 (alu IP2022 t s)) with
-   [ pair val call' ⇒ Some ? (pair … val
-    (set_alu IP2022 t s
-     (mk_alu_IP2022
-      (acc_low_reg_IP2022 (alu IP2022 t s))
-      (mulh_reg_IP2022 (alu IP2022 t s))
-      (addrsel_reg_IP2022 (alu IP2022 t s))
-      (addr_array_IP2022 (alu IP2022 t s))
-      call'
-      (ip_reg_IP2022 (alu IP2022 t s))
-      (dp_reg_IP2022 (alu IP2022 t s))
-      (data_reg_IP2022 (alu IP2022 t s))
-      (sp_reg_IP2022 (alu IP2022 t s))
-      (pc_reg_IP2022 (alu IP2022 t s))
-      (speed_reg_IP2022 (alu IP2022 t s))
-      (page_reg_IP2022 (alu IP2022 t s))
-      (h_flag_IP2022 (alu IP2022 t s))
-      (z_flag_IP2022 (alu IP2022 t s))
-      (c_flag_IP2022 (alu IP2022 t s))
-      (skip_mode_IP2022 (alu IP2022 t s))))) ]].
-
 (* getter di IP, non esiste sempre *)
 ndefinition get_ip_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.