X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fread_write%2FRS08_read_write.ma;h=08beb8b213103ce9a521a455bec9101ebb39dfcb;hb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;hp=bec7454a4ce2f650b3832a5ab3adafa9d190772c;hpb=b082cb1e1fc9dbd471d16d2eb231e883e96e588f;p=helm.git

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 bec7454a4..08beb8b21 100755
--- 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)