A) New version.

[helm.git] / helm / software / matita / library / freescale / memory_bits.ma

diff --git a/helm/software/matita/library/freescale/memory_bits.ma b/helm/software/matita/library/freescale/memory_bits.ma
index d7425bff6ee38c2d9c67572d9b75614de8e20918..dda2760ff1abccb6c6e117095e64343b0679df33 100644 (file)
--- a/helm/software/matita/library/freescale/memory_bits.ma
+++ b/helm/software/matita/library/freescale/memory_bits.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/memory_bits/".
-
-(*include "/media/VIRTUOSO/freescale/memory_trees.ma".*)
 include "freescale/memory_trees.ma".
 
 (* ********************* *)
@@ -108,44 +105,51 @@ definition mb_mem_read_bit ≝
   (* NON INSTALLATA? no *)
   | MEM_OUT_OF_BOUND ⇒ None ? ]. 
 
+definition mb_chk_get ≝
+λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).λaddr:word16.
+let c ≝ mt_visit (Prod8T memory_type) chk addr in
+array_8T ? (getn_array8T o7 ? c) (getn_array8T o6 ? c)
+           (getn_array8T o5 ? c) (getn_array8T o4 ? c)
+           (getn_array8T o3 ? c) (getn_array8T o2 ? c)
+           (getn_array8T o1 ? c) (getn_array8T o0 ? c).
+
 (* scrivi controllando il tipo di memoria *)
 (* NB: devono esistere tutti i bit *)
 definition mb_mem_update ≝
 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
-λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
+λchk:Prod8T memory_type.
 λaddr:word16.λv:byte8.
-let bit_types ≝ mt_visit (Prod8T memory_type) chk addr in
 let old_value ≝ mt_visit (Prod8T bool) mem addr in
 let new_value ≝ bits_of_byte8 v in
-let newbit0 ≝ match getn_array8T o0 memory_type bit_types with
+let newbit0 ≝ match getn_array8T o0 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit1 ≝ match getn_array8T o1 memory_type bit_types with
+let newbit1 ≝ match getn_array8T o1 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit2 ≝ match getn_array8T o2 memory_type bit_types with
+let newbit2 ≝ match getn_array8T o2 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit3 ≝ match getn_array8T o3 memory_type bit_types with
+let newbit3 ≝ match getn_array8T o3 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit4 ≝ match getn_array8T o4 memory_type bit_types with
+let newbit4 ≝ match getn_array8T o4 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit5 ≝ match getn_array8T o5 memory_type bit_types with
+let newbit5 ≝ match getn_array8T o5 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit6 ≝ match getn_array8T o6 memory_type bit_types with
+let newbit6 ≝ match getn_array8T o6 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
+let newbit7 ≝ match getn_array8T o7 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in