X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fmemory_abs.ma;h=d00efc3a332ae9dfe31c106f2b04522f78f7cfb1;hb=8ef11a4b981e6da3d60f353386b17f7692dc0ecd;hp=23f3f158a3ba1f3801bc29aee97ddcce8ef52129;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/memory_abs.ma b/helm/software/matita/library/freescale/memory_abs.ma
index 23f3f158a..d00efc3a3 100644
--- a/helm/software/matita/library/freescale/memory_abs.ma
+++ b/helm/software/matita/library/freescale/memory_abs.ma
@@ -24,13 +24,8 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/memory_abs/".
-
-(*include "/media/VIRTUOSO/freescale/memory_func.ma".*)
 include "freescale/memory_func.ma".
-(*include "/media/VIRTUOSO/freescale/memory_trees.ma".*)
 include "freescale/memory_trees.ma".
-(*include "/media/VIRTUOSO/freescale/memory_bits.ma".*)
 include "freescale/memory_bits.ma".
 
 (* ********************************************* *)
@@ -98,25 +93,27 @@ definition mem_read_abs ≝
                byte8_of_bits (mt_visit (Prod8T bool) m addr)
   ].
 
+(* unificazione del chk *)
+definition chk_get ≝
+λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
+ match t
+  return λt.aux_chk_type t → word16 → Prod8T memory_type
+ with
+  [ MEM_FUNC ⇒ mf_chk_get
+  | MEM_TREE ⇒ mt_chk_get
+  | MEM_BITS ⇒ mb_chk_get
+  ] c addr.
+
 (* unificazione della lettura con chk: mem_read mem chk addr *)
 definition mem_read ≝
-λt:memory_impl.
+λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.
  match t
   return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8 
  with
-  [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
-               λc:aux_chk_type MEM_FUNC.
-               λaddr:word16.
-               mf_mem_read m c addr
-  | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
-               λc:aux_chk_type MEM_TREE.
-               λaddr:word16.
-               mt_mem_read m c addr
-  | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
-               λc:aux_chk_type MEM_BITS.
-               λaddr:word16.
-               mb_mem_read m c addr
-  ].
+  [ MEM_FUNC ⇒ mf_mem_read
+  | MEM_TREE ⇒ mt_mem_read
+  | MEM_BITS ⇒ mb_mem_read
+  ] m c addr.
 
 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
 definition mem_read_bit ≝
@@ -145,26 +142,14 @@ definition mem_read_bit ≝
 
 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
 definition mem_update ≝
-λt:memory_impl.
+λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8.
  match t
-  return λt.aux_mem_type t → aux_chk_type t → word16 → byte8 → option (aux_mem_type t) 
+  return λt.aux_mem_type t → Prod8T memory_type → word16 → byte8 → option (aux_mem_type t)
  with
-  [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
-               λc:aux_chk_type MEM_FUNC.
-               λaddr:word16.
-               λv:byte8.
-               mf_mem_update m c addr v
-  | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
-               λc:aux_chk_type MEM_TREE.
-               λaddr:word16.
-               λv:byte8.
-               mt_mem_update m c addr v
-  | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
-               λc:aux_chk_type MEM_BITS.
-               λaddr:word16.
-               λv:byte8.
-               mb_mem_update m c addr v
-  ].
+  [ MEM_FUNC ⇒ mf_mem_update
+  | MEM_TREE ⇒ mt_mem_update
+  | MEM_BITS ⇒ mb_mem_update
+  ] m (chk_get t c addr) addr v.
 
 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
 definition mem_update_bit ≝
@@ -178,14 +163,14 @@ definition mem_update_bit ≝
                λo:oct.
                λv:bool.
                opt_map ?? (mf_mem_read m c addr)
-                (λb.mf_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
+                (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
                λc:aux_chk_type MEM_TREE.
                λaddr:word16.
                λo:oct.
                λv:bool.
                opt_map ?? (mt_mem_read m c addr)
-                (λb.mt_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
+                (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
                λc:aux_chk_type MEM_BITS.
                λaddr:word16.
@@ -196,23 +181,14 @@ definition mem_update_bit ≝
 
 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
 definition load_from_source_at ≝
-λt:memory_impl.
+λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16.
  match t
   return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t 
  with
-  [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
-               λl:list byte8.
-               λaddr:word16.
-               mf_load_from_source_at m l addr
-  | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
-               λl:list byte8.
-               λaddr:word16.
-               mt_load_from_source_at m l addr
-  | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
-               λl:list byte8.
-               λaddr:word16.
-               mb_load_from_source_at m l addr
-  ].
+  [ MEM_FUNC ⇒ mf_load_from_source_at
+  | MEM_TREE ⇒ mt_load_from_source_at
+  | MEM_BITS ⇒ mb_load_from_source_at
+  ] m l addr.
 
 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
 definition check_update_ranged ≝