| 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 *)
| 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.