(* 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".
(* ********************************************* *)
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 ≝
(* 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 ≝
λ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.
(* 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 ≝