freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
index 3f1a628396cb036815952ac7cdbecc9326efac12..e28410878155af6677e758afb3766818f11c99ac 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
@@ -275,11 +275,20 @@ ndefinition push_call_reg ≝
              | IP2022 ⇒ Some ? push_call_reg_IP2022 ])
  (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
 
-(* push debole di CALL *)
-ndefinition pushweak_call_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
- match push_call_reg m t s call' with
-  [ None ⇒ s | Some s' ⇒ s' ].
+(* pop forte di CALL *)
+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_call_reg_IP2022 (alu … s) with
+    [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ]
+  ].
 
 (* REGISTRO IP *)