X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus.ma;h=9462c455b8a2da7ba87da795f9ddeb6b085ef941;hb=a79bf6edc13daaea8135ca71fdc92e02e229f030;hp=ae5c97c7c4ecb12bd2e395a681c764f1234abead;hpb=0f13d14b63b012e0ea8ce0d0e71bf808fdd444eb;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
index ae5c97c7c..9462c455b 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
@@ -24,6 +24,7 @@ include "emulator/memory/memory_abs.ma".
 include "emulator/status/HC05_status.ma".
 include "emulator/status/HC08_status.ma".
 include "emulator/status/RS08_status.ma".
+include "emulator/status/IP2022_status.ma".
 include "emulator/opcodes/opcode.ma".
 
 (* *********************************** *)
@@ -39,7 +40,8 @@ ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_op_type m) (aux_im_t
 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
  {
  alu : match mcu with
-  [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
+  [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+  | IP2022 ⇒ alu_IP2022 ];
 
  (* descritore della memoria *)
  mem_desc : aux_mem_type t;
@@ -64,15 +66,18 @@ ndefinition eq_alu ≝
  match m
   return λm.
    match m with
-    [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
+    [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+    | IP2022 ⇒ alu_IP2022 ] →
    match m with
-    [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
+    [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+    | IP2022 ⇒ alu_IP2022 ] →
    bool
  with
   [ HC05 ⇒ eq_HC05_alu
   | HC08 ⇒ eq_HC08_alu
   | HCS08 ⇒ eq_HC08_alu
   | RS08 ⇒ eq_RS08_alu
+  | IP2022 ⇒ eq_IP2022_alu
   ].
 
 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
@@ -83,23 +88,12 @@ nlet rec forall_memory_ranged
  (addrl:list word32) on addrl ≝
  match addrl return λ_.bool with
   [ nil ⇒ true
-  | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
-                            (mem_read t mem2 chk2 hd) eq_b8) ⊗
+  | cons hd tl ⇒ (eq_option byte8 eq_b8 (mem_read t mem1 chk1 hd)
+                                        (mem_read t mem2 chk2 hd)) ⊗
                  (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
   ].
 
-ndefinition eq_clk ≝
-λm:mcu_type.λc1,c2:option (aux_clk_type m).
- match c1 with
-  [ None ⇒ match c2 with
-   [ None ⇒ true | Some _ ⇒ false ]
-  | Some c1' ⇒ match c2 with
-   [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
-                               (eq_op m (snd5T … c1') (snd5T … c2')) ⊗
-                               (eq_im m (thd5T … c1') (thd5T … c2')) ⊗
-                               (eq_b8 (fth5T … c1') (fth5T … c2')) ⊗
-                               (eq_w16 (fft5T … c1') (fft5T … c2')) ]
-  ].
+ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_op m) (eq_im m) eq_b8 eq_w16).
 
 (* generalizzazione del confronto fra stati *)
 ndefinition eq_anystatus ≝