(no commit message)

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
index be27f55478513b6bb891537610f051dac15f3523..831c75a1aff6d78b9f7caab6ebeb6c5a918e8552 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
@@ -13,21 +13,17 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           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_struct.ma".
-include "freescale/word16.ma".
-include "freescale/option.ma".
-include "freescale/theory.ma".
+include "num/word16.ma".
+include "common/option.ma".
+include "common/list.ma".
 
 (* ********************* *)
 (* MEMORIA E DESCRITTORE *)
@@ -35,8 +31,8 @@ include "freescale/theory.ma".
 
 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
 ndefinition mf_check_update_ranged ≝
-λf:word16 → memory_type.λi.λs.λv.
- λx.match in_range x i s with
+λf:word16 → memory_type.λinf.λsup.λv.
+ λx.match inrange_w16 x inf sup with
   [ true ⇒ v
   | false ⇒ f x ].
 
@@ -77,19 +73,15 @@ ndefinition mf_mem_read ≝
 (* CARICAMENTO PROGRAMMA/DATI *)
 (* ************************** *)
 
-(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
-nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
-  (* e' prima di source: carica da old_mem *)
-  [ true ⇒ old_mem x
-  | false ⇒ match eq_w16 x addr with
+(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
+nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ λx:word16.match eq_w16 addr x with
    (* la locazione corrisponde al punto corrente di source *)
    [ true ⇒ hd
-   (* la locazione e' piu' avanti: ricorsione *)
+   (* la locazione e' piu' avanti? ricorsione *)
    | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)) x
    ]
-  ]
- ].
+  ].