freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / memory_abs.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
index 8e9f08c055b16b85a40fea3e3aab1853130771c7..736f4aaea618371be61ba9aa3e6b957bd88f75d1 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          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                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -34,18 +34,6 @@ ninductive memory_impl : Type ≝
 | 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
@@ -133,13 +121,13 @@ ndefinition mem_read_bit ≝
                λ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.
@@ -170,14 +158,14 @@ ndefinition mem_update_bit ≝
                λ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.