(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
λc:aux_chk_type MEM_FUNC.
λaddr:word16.
λo:oct.
- opt_map ?? (mf_mem_read m c addr)
+ opt_map … (mf_mem_read m c addr)
(λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
| MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
λc:aux_chk_type MEM_TREE.
λaddr:word16.
λo:oct.
- opt_map ?? (mt_mem_read m c addr)
+ opt_map … (mt_mem_read m c addr)
(λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
| MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
λc:aux_chk_type MEM_BITS.
λaddr:word16.
λo:oct.
λv:bool.
- opt_map ?? (mf_mem_read m c addr)
+ opt_map … (mf_mem_read m c addr)
(λ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)
+ opt_map … (mt_mem_read m c addr)
(λ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.