X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fstatus.ma;h=1354861e2a9858f0ef90c99e85917b6b1b04117b;hb=dc7e826399162e2fde3ddf1f02d5530d6cd11205;hp=b20d2e8145e2796411035267bde0a777a03c22d5;hpb=03ebff6c48be2253ad32b3b57f4e1d2b02acda86;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index b20d2e814..1354861e2 100755
--- 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) *)
@@ -165,38 +164,6 @@ nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
  clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
  }.
 
-ndefinition any_status_ind : 
- Πmcu.Πt.ΠP:any_status mcu t → Prop.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
-  Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Prop.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rec : 
- Πmcu.Πt.ΠP:any_status mcu t → Set.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
-  Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Set.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rect : 
- Πmcu.Πt.ΠP:any_status mcu t → Type.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
-  Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Type.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition alu ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status (x:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]) _ _ _ ⇒ x ].
-ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].     
-ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
-ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
-
 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80 
  for @{ 'mk_any_status $alu $mem $chk $clk }.
@@ -393,20 +360,6 @@ ndefinition get_irq_flag ≝
  | RS08 ⇒ λalu.None ? ]
  (alu m t s).
 
-(* DESCRITTORI ESTERNI ALLA ALU *)
-
-(* getter della ALU, esiste sempre *)
-ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
-
-(* getter della memoria, esiste sempre *)
-ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
-
-(* getter del descrittore, esiste sempre *)
-ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
-
-(* getter del clik, esiste sempre *)
-ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
-
 (* ***************************** *)
 (* SETTER SPECIFICI FORTI/DEBOLI *)
 (* ***************************** *)
@@ -428,23 +381,23 @@ ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
 (* setter forte della ALU *)
 ndefinition set_alu ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
- mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
+ mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
 
 (* setter forte della memoria *)
 ndefinition set_mem_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
- mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
+ mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
 
 (* setter forte del descrittore *)
 ndefinition set_chk_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
- mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
+ mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
 
 (* setter forte del clik *)
 ndefinition set_clk_desc ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
- mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
+ mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
 
 (* REGISTRO A *)
 
@@ -547,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
@@ -582,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
@@ -617,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
@@ -670,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
@@ -762,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 ?
@@ -793,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 ?
@@ -824,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 ?
@@ -859,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
@@ -912,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
@@ -965,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
@@ -1018,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
@@ -1193,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
@@ -1211,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 ⇒
@@ -1232,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 ⇒
@@ -1252,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 ⇒
@@ -1291,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 ⇒
@@ -1311,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] *)