X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fmemory_trees.ma;h=e696ca44195705c7f306b1b8a7d728b67238f115;hb=1ba7566bacd8d29e772646b3c86c7d5c944e9a6e;hp=9fba644dcef004a46909bc19f88d2a63a10352c0;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/memory_trees.ma b/helm/software/matita/library/freescale/memory_trees.ma
index 9fba644dc..e696ca441 100644
--- a/helm/software/matita/library/freescale/memory_trees.ma
+++ b/helm/software/matita/library/freescale/memory_trees.ma
@@ -24,9 +24,6 @@
 (*                    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".
 
 (* ********************* *)
@@ -185,13 +182,21 @@ definition mt_update_ranged ≝
  (* 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 *)