X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_abs.ma;h=736f4aaea618371be61ba9aa3e6b957bd88f75d1;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=d1934684dfbe4fdb9e5e577be955dcc9652dd6ff;hpb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;p=helm.git

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 d1934684d..736f4aaea 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/memory_func.ma".
@@ -38,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
@@ -137,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.
@@ -174,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.