X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fmemory_func.ma;h=490261fdb2183337571b57a5952f34733c014392;hb=09e3a050664b07c961a92bf16245a7345346f964;hp=44b252434832e08db0a567948d5be49879fefb15;hpb=e44ebf8a8c659b408fa765d30faf1b8c8ff2adb0;p=helm.git

diff --git a/helm/software/matita/library/freescale/memory_func.ma b/helm/software/matita/library/freescale/memory_func.ma
index 44b252434..490261fdb 100644
--- a/helm/software/matita/library/freescale/memory_func.ma
+++ b/helm/software/matita/library/freescale/memory_func.ma
@@ -24,9 +24,6 @@
 (*                    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".
 
 (* ********************* *)
@@ -43,10 +40,18 @@ definition mf_check_update_ranged ≝
 (* 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 *)