(* ********************************************************************** *)
(* 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 *)
(* *)
(* ********************************************************************** *)
| MEM_TREE: memory_impl
| MEM_BITS: memory_impl.
-ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
-λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
-
-ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
-λP:memory_impl → Set.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
-
-ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
-λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
- match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
-
(* ausiliario per il tipo della memoria *)
ndefinition aux_mem_type ≝
λt:memory_impl.match t with
λ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.