...

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
index 2b0b736245ce7c4990a8a462e0c2a541a7627704..c49be931a4594557c071b882db33619a67513a94 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.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_trees.ma".
@@ -153,14 +149,14 @@ let newbit7 ≝ match getn_array8T o7 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-       opt_map ?? newbit0
- (λnb0.opt_map ?? newbit1
- (λnb1.opt_map ?? newbit2
- (λnb2.opt_map ?? newbit3
- (λnb3.opt_map ?? newbit4
- (λnb4.opt_map ?? newbit5
- (λnb5.opt_map ?? newbit6
- (λnb6.opt_map ?? newbit7
+       opt_map … newbit0
+ (λnb0.opt_map … newbit1
+ (λnb1.opt_map … newbit2
+ (λnb2.opt_map … newbit3
+ (λnb3.opt_map … newbit4
+ (λnb4.opt_map … newbit5
+ (λnb5.opt_map … newbit6
+ (λnb6.opt_map … newbit7
  (λnb7.Some ? (mt_update (Array8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 
 (* leggi controllando il tipo di memoria *)
@@ -203,14 +199,14 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-       opt_map ?? newbit0
- (λnb0.opt_map ?? newbit1
- (λnb1.opt_map ?? newbit2
- (λnb2.opt_map ?? newbit3
- (λnb3.opt_map ?? newbit4
- (λnb4.opt_map ?? newbit5
- (λnb5.opt_map ?? newbit6
- (λnb6.opt_map ?? newbit7
+       opt_map … newbit0
+ (λnb0.opt_map … newbit1
+ (λnb1.opt_map … newbit2
+ (λnb2.opt_map … newbit3
+ (λnb3.opt_map … newbit4
+ (λnb4.opt_map … newbit5
+ (λnb5.opt_map … newbit6
+ (λnb6.opt_map … newbit7
  (λnb7.Some ? (byte8_of_bits (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 
 (* ************************** *)
@@ -219,13 +215,9 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
 
 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 nlet rec mb_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))))
-                               (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
-  (* non supera 0xFFFF, ricorsione *)
-  [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
-  (* supera 0xFFFF, niente ricorsione *)
-  | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)
-  ]].
+                                (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
+  ].