freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma
index b9d67c55482ec9b36ac64b61f953a579ea5cae27..e1e338b8181589f040612a0dee61ace4cf2a6078 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma
@@ -217,15 +217,11 @@ ndefinition mt_mem_read ≝
 (* CARICAMENTO PROGRAMMA/DATI *)
 (* ************************** *)
 
-(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
+(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
 nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8))))
-                               (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 ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
-  (* supera 0xFFFF, niente ricorsione *)
-  | false ⇒ mt_update ? old_mem addr hd
-  ]].
+                                (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
+  ].