(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/memory_trees/".
-
-(*include "/media/VIRTUOSO/freescale/memory_struct.ma".*)
include "freescale/memory_struct.ma".
(* ********************* *)
(* no i>s *)
| false ⇒ data
].
+
+definition mt_chk_get ≝
+λchk:Prod16T (Prod16T (Prod16T (Prod16T memory_type))).λaddr:word16.
+ match mt_visit ? chk addr 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
+ ].
(* scrivi controllando il tipo di memoria *)
definition mt_mem_update ≝
λmem:Prod16T (Prod16T (Prod16T (Prod16T byte8))).
-λchk:Prod16T (Prod16T (Prod16T (Prod16T memory_type))).
+λchk:Prod8T memory_type.
λaddr:word16.λv:byte8.
- match mt_visit ? chk addr with
+ match getn_array8T o0 ? chk with
(* ROM? ok, ma il valore viene perso *)
[ MEM_READ_ONLY ⇒ Some ? mem
(* RAM? ok *)