mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
old mode 100755 (executable)
new mode 100644 (file)
index deaf39a..927da3d
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
@@ -25,7 +25,7 @@ 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".
+include "emulator/opcodes/pseudo.ma".
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -34,7 +34,7 @@ include "emulator/opcodes/opcode.ma".
 (* descrittore del click = stato di avanzamento dell'esecuzione *)
 (* 1) None = istruzione eseguita, attesa del fetch *)
 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *)
-ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_op_type m) (aux_im_type m) byte8 word16.
+ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
 
 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
@@ -93,18 +93,7 @@ nlet rec forall_memory_ranged
                  (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_pseudo m) (eq_im m) eq_b8 eq_w16).
 
 (* generalizzazione del confronto fra stati *)
 ndefinition eq_anystatus ≝