freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / read_write / RS08_read_write.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma
index bec7454a4ce2f650b3832a5ab3adafa9d190772c..08beb8b213103ce9a521a455bec9101ebb39dfcb 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/RS08_read_write.ma
@@ -61,13 +61,13 @@ ndefinition RS08_memory_filter_read_aux ≝
 (* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging 
    altrimenti sarebbero 2 indirezioni *)
  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
-  [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉
+  [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈x0,x0〉:(x_map_RS08 (alu … s))〉)
   | false ⇒ 
 (* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
  match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
   [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) 
-                (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
-                                         (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉)
+                (ext_word32 (or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
+                                    (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉)))
 (* accesso normale *)
   | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr ]]]]].
 
@@ -121,14 +121,14 @@ ndefinition RS08_memory_filter_write_aux ≝
 (* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging 
    altrimenti sarebbero 2 indirezioni *)
  match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
-  [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉)
+  [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) (ext_word32 〈〈x0,x0〉:(x_map_RS08 (alu … s))〉))
             (λmem'.Some ? (set_mem_desc … s mem'))
   | false ⇒
 (* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
  match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
   [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s)
-                           (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
-                                                    (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉))
+                           (ext_word32 (or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
+                                               (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))))
             (λmem'.Some ? (set_mem_desc … s mem'))
 (* accesso normale *)
   | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)