(* 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".
(* ********************* *)
(* 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