added auto_cache in the dupable status after an

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index 6a0f81887ef4431385fb048784bf9beecdd1e4a2..1354861e2a9858f0ef90c99e85917b6b1b04117b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
@@ -15,14 +15,13 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 include "freescale/memory_abs.ma".
 include "freescale/opcode_base.ma".
-include "freescale/prod.ma".
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -501,7 +500,7 @@ ndefinition set_indX_8_low_reg_HC08 ≝
 (* setter forte di X *)
 ndefinition set_indX_8_low_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
              [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
              | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
              | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
@@ -536,7 +535,7 @@ ndefinition set_indX_8_high_reg_HC08 ≝
 (* setter forte di H *)
 ndefinition set_indX_8_high_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
              [ HC05 ⇒ None ?
              | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
              | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
@@ -571,7 +570,7 @@ ndefinition set_indX_16_reg_HC08 ≝
 (* setter forte di H:X *)
 ndefinition set_indX_16_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
- opt_map ?? (match m return aux_set_typing_opt word16 with
+ opt_map … (match m return aux_set_typing_opt word16 with
              [ HC05 ⇒ None ?
              | HC08 ⇒ Some ? set_indX_16_reg_HC08
              | HCS08 ⇒ Some ? set_indX_16_reg_HC08
@@ -624,7 +623,7 @@ ndefinition set_sp_reg_HC08 ≝
 (* setter forte di SP *)
 ndefinition set_sp_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
- opt_map ?? (match m return aux_set_typing_opt word16 with
+ opt_map … (match m return aux_set_typing_opt word16 with
              [ HC05 ⇒ Some ? set_sp_reg_HC05
              | HC08 ⇒ Some ? set_sp_reg_HC08
              | HCS08 ⇒ Some ? set_sp_reg_HC08
@@ -716,7 +715,7 @@ ndefinition set_spc_reg_RS08 ≝
 (* setter forte di SPC *)
 ndefinition set_spc_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
- opt_map ?? (match m return aux_set_typing_opt word16 with
+ opt_map … (match m return aux_set_typing_opt word16 with
              [ HC05 ⇒ None ?
              | HC08 ⇒ None ?
              | HCS08 ⇒ None ?
@@ -747,7 +746,7 @@ ndefinition set_x_map_RS08 ≝
 (* setter forte di memory mapped X *)
 ndefinition set_x_map ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
              [ HC05 ⇒ None ?
              | HC08 ⇒ None ?
              | HCS08 ⇒ None ?
@@ -778,7 +777,7 @@ ndefinition set_ps_map_RS08 ≝
 (* setter forte di memory mapped PS *)
 ndefinition set_ps_map ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
              [ HC05 ⇒ None ?
              | HC08 ⇒ None ?
              | HCS08 ⇒ None ?
@@ -813,7 +812,7 @@ ndefinition set_v_flag_HC08 ≝
 (* setter forte di V *)
 ndefinition set_v_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
              [ HC05 ⇒ None ?
              | HC08 ⇒ Some ? set_v_flag_HC08
              | HCS08 ⇒ Some ? set_v_flag_HC08
@@ -866,7 +865,7 @@ ndefinition set_h_flag_HC08 ≝
 (* setter forte di H *)
 ndefinition set_h_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
              [ HC05 ⇒ Some ? set_h_flag_HC05
              | HC08 ⇒ Some ? set_h_flag_HC08
              | HCS08 ⇒ Some ? set_h_flag_HC08
@@ -919,7 +918,7 @@ ndefinition set_i_flag_HC08 ≝
 (* setter forte di I *)
 ndefinition set_i_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
              [ HC05 ⇒ Some ? set_i_flag_HC05
              | HC08 ⇒ Some ? set_i_flag_HC08
              | HCS08 ⇒ Some ? set_i_flag_HC08
@@ -972,7 +971,7 @@ ndefinition set_n_flag_HC08 ≝
 (* setter forte di N *)
 ndefinition set_n_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
              [ HC05 ⇒ Some ? set_n_flag_HC05
              | HC08 ⇒ Some ? set_n_flag_HC08
              | HCS08 ⇒ Some ? set_n_flag_HC08
@@ -1147,7 +1146,7 @@ ndefinition set_irq_flag_HC08 ≝
 (* setter forte di IRQ *)
 ndefinition set_irq_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
              [ HC05 ⇒ Some ? set_irq_flag_HC05
              | HC08 ⇒ Some ? set_irq_flag_HC08
              | HCS08 ⇒ Some ? set_irq_flag_HC08
@@ -1165,7 +1164,7 @@ ndefinition setweak_irq_flag ≝
 (* ***************** *)
 
 (* confronto registro per registro dell'HC05 *)
-ndefinition eq_alu_HC05 ≝
+ndefinition eq_aluHC05 ≝
 λalu1,alu2:alu_HC05.
  match alu1 with
   [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
@@ -1186,7 +1185,7 @@ ndefinition eq_alu_HC05 ≝
    (eq_bool irqfl1 irqfl2) ]].
 
 (* confronto registro per registro dell'HC08 *)
-ndefinition eq_alu_HC08 ≝
+ndefinition eq_aluHC08 ≝
 λalu1,alu2:alu_HC08.
  match alu1 with
   [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
@@ -1206,7 +1205,7 @@ ndefinition eq_alu_HC08 ≝
    (eq_bool irqfl1 irqfl2) ]].
 
 (* confronto registro per registro dell'RS08 *)
-ndefinition eq_alu_RS08 ≝
+ndefinition eq_aluRS08 ≝
 λalu1,alu2:alu_RS08.
  match alu1 with
   [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
@@ -1245,15 +1244,15 @@ ndefinition eq_clk ≝
   [ None ⇒ match c2 with
    [ None ⇒ true | Some _ ⇒ false ]
   | Some c1' ⇒ match c2 with
-   [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
-                               (eq_anyop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
-                               (eq_instrmode (thd5T ????? c1') (thd5T ????? c2')) ⊗
-                               (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
-                               (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
+   [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
+                               (eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗
+                               (eq_im (thd5T … c1') (thd5T … c2')) ⊗
+                               (eq_b8 (frth5T … c1') (frth5T … c2')) ⊗
+                               (eq_w16 (ffth5T … c1') (ffth5T … c2')) ]
   ].
 
 (* generalizzazione del confronto fra stati *)
-ndefinition eq_status ≝
+ndefinition eq_anystatus ≝
 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
  match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
  match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
@@ -1265,7 +1264,7 @@ ndefinition eq_status ≝
    match m with
     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
    bool with
-  [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
+  [ HC05 ⇒ eq_aluHC05 | HC08 ⇒ eq_aluHC08 | HCS08 ⇒ eq_aluHC08 | RS08 ⇒ eq_aluRS08 ]
  alu1 alu2) ⊗
 
  (* 2) confronto della memoria in [inf,inf+n] *)