(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/memory_func/".
-
-(*include "/media/VIRTUOSO/freescale/memory_struct.ma".*)
include "freescale/memory_struct.ma".
(* ********************* *)
(* tutta la memoria non installata *)
definition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND.
-(* (mf_mem_update mem check addr val) = scrivi controllando il tipo di memoria *)
-definition mf_mem_update ≝
-λf:word16 → byte8.λc:word16 → memory_type.λa.λv.
+definition mf_chk_get ≝
+λc:word16 → memory_type.λa:word16.
match c a with
+ [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
+ | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
+ | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
+ ].
+
+(* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
+definition mf_mem_update ≝
+λf:word16 → byte8.λc:Prod8T memory_type.λa:word16.λv:byte8.
+ match getn_array8T o0 ? c with
(* ROM? ok, ma il valore viene perso *)
[ MEM_READ_ONLY ⇒ Some ? f
(* RAM? ok *)