mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_trees.ma
old mode 100755 (executable)
new mode 100644 (file)
index 45bae96..1319a04
--- a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_trees.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_trees.ma
@@ -74,34 +74,34 @@ ndefinition mt_zero_memory ≝ aux_32B_filler ? 〈x0,x0〉.
 (* visita di un albero da 4GB di elementi: ln16(4GB)=8 passaggi *)
 ndefinition mt_visit ≝
 λT:Type.λdata:aux_32B_type T.λaddr:word32.
- getn_array16T (b8l (w16l (w32l addr))) ?
-  (getn_array16T (b8h (w16l (w32l addr))) ?
-   (getn_array16T (b8l (w16h (w32l addr))) ?
-    (getn_array16T (b8h (w16h (w32l addr))) ?
-     (getn_array16T (b8l (w16l (w32h addr))) ?
-      (getn_array16T (b8h (w16l (w32h addr))) ?
-       (getn_array16T (b8l (w16h (w32h addr))) ?
-        (getn_array16T (b8h (w16h (w32h addr))) ? data))))))).
+ getn_array16T (cnL ? (cnL ? (cnL ? addr))) ?
+  (getn_array16T (cnH ? (cnL ? (cnL ? addr))) ?
+   (getn_array16T (cnL ? (cnH ? (cnL ? addr))) ?
+    (getn_array16T (cnH ? (cnH ? (cnL ? addr))) ?
+     (getn_array16T (cnL ? (cnL ? (cnH ? addr))) ?
+      (getn_array16T (cnH ? (cnL ? (cnH ? addr))) ?
+       (getn_array16T (cnL ? (cnH ? (cnH ? addr))) ?
+        (getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data))))))).
 
 (* scrittura di un elemento in un albero da 4GB *)
 ndefinition mt_update ≝
 λT:Type.λdata:aux_32B_type T.λaddr:word32.λv:T.
- let lev2 ≝ getn_array16T (b8h (w16h (w32h addr))) ? data in
- let lev3 ≝ getn_array16T (b8l (w16h (w32h addr))) ? lev2 in
- let lev4 ≝ getn_array16T (b8h (w16l (w32h addr))) ? lev3 in
- let lev5 ≝ getn_array16T (b8l (w16l (w32h addr))) ? lev4 in
- let lev6 ≝ getn_array16T (b8h (w16h (w32l addr))) ? lev5 in
- let lev7 ≝ getn_array16T (b8l (w16h (w32l addr))) ? lev6 in
- let lev8 ≝ getn_array16T (b8h (w16l (w32l addr))) ? lev7 in
+ let lev2 ≝ getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data in
+ let lev3 ≝ getn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2 in
+ let lev4 ≝ getn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3 in
+ let lev5 ≝ getn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4 in
+ let lev6 ≝ getn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5 in
+ let lev7 ≝ getn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6 in
+ let lev8 ≝ getn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7 in
 
- setn_array16T (b8h (w16h (w32h addr))) ? data
-  (setn_array16T (b8l (w16h (w32h addr))) ? lev2
-   (setn_array16T (b8h (w16l (w32h addr))) ? lev3
-    (setn_array16T (b8l (w16l (w32h addr))) ? lev4
-     (setn_array16T (b8h (w16h (w32l addr))) ? lev5
-      (setn_array16T (b8l (w16h (w32l addr))) ? lev6
-       (setn_array16T (b8h (w16l (w32l addr))) ? lev7
-        (setn_array16T (b8l (w16l (w32l addr))) T lev8 v))))))).
+ setn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data
+  (setn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2
+   (setn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3
+    (setn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4
+     (setn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5
+      (setn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6
+       (setn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7
+        (setn_array16T (cnL ? (cnL ? (cnL ? addr))) T lev8 v))))))).
 
 (* scrittura di un range (max 64KB) in un albero da 4GB *)
 nlet rec mt_update_ranged (T:Type) (data:aux_32B_type T) (addr:word32) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝