X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fload_write.ma;h=addedf2e3921ed2f7373da44a35921793549d59a;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=3e5ba4ed6544f8069907ac308d0964405e4807ca;hpb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
index 3e5ba4ed6..addedf2e3 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -90,7 +90,7 @@ match s with
 (* 
    accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
 *)
-        match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
+        match inrange_w16 addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
          [ true ⇒ fMEM mem chk (or_w16 (fst … (shr_w16 (fst … (shr_w16 〈psm:〈x0,x0〉〉))))
                                              (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
 (*
@@ -188,7 +188,7 @@ match s with
 (* 
    accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
 *)
-        match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
+        match inrange_w16 addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
          [ true ⇒ opt_map … (fMEM mem chk (or_w16 (fst … (shr_w16 (fst … (shr_w16 〈psm:〈x0,x0〉〉))))
                                                    (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
                    (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
@@ -391,39 +391,39 @@ ndefinition mode_IMM2_load ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (memory_filter_read m t s cur_pc)
   (λbh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-   (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
+   (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc nat2)))).
 
 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
 ndefinition mode_DIR1_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
+  (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc nat1).
 
 (* lettura da [byte [curpc]]: loadbit *)
 ndefinition mode_DIR1n_load ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
+  (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc nat1).
 
 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
 ndefinition mode_DIR1_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
+  (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc nat1 writebw).
 
 (* scrittura su [byte [curpc]]: writebit *)
 ndefinition mode_DIR1n_write ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
  opt_map … (memory_filter_read m t s cur_pc)
-  (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
+  (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc nat1 writeb).
 
 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
 ndefinition mode_DIR2_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (memory_filter_read m t s cur_pc)
   (λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-   (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
+   (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc nat2)).
 
 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
 ndefinition mode_DIR2_write ≝
@@ -431,7 +431,7 @@ ndefinition mode_DIR2_write ≝
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (memory_filter_read m t s cur_pc)
   (λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-   (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
+   (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc nat2 writebw)).
 
 ndefinition get_IX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
@@ -445,21 +445,21 @@ ndefinition get_IX ≝
 ndefinition mode_IX0_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (get_IX m t s)
-  (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
+  (λaddr.(aux_load m t byteflag) s addr cur_pc O).
 
 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
 ndefinition mode_IX0_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (get_IX m t s)
-  (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
+  (λaddr.(aux_write m t byteflag) s addr cur_pc O writebw).
 
 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
 ndefinition mode_IX1_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1)).
 
 (* lettura da X+[byte curpc] *)
 ndefinition mode_IX1ADD_load ≝
@@ -474,7 +474,7 @@ ndefinition mode_IX1_write ≝
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
+   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1 writebw)).
 
 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
 ndefinition mode_IX2_load ≝
@@ -482,7 +482,7 @@ ndefinition mode_IX2_load ≝
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
+    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2))).
 
 (* lettura da X+[word curpc] *)
 ndefinition mode_IX2ADD_load ≝
@@ -490,7 +490,7 @@ ndefinition mode_IX2ADD_load ≝
  opt_map … (memory_filter_read m t s cur_pc)
   (λbh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
    (λbl.opt_map … (get_IX m t s)
-    (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+    (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc nat2))))).
 
 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 ndefinition mode_IX2_write ≝
@@ -499,14 +499,14 @@ ndefinition mode_IX2_write ≝
  opt_map … (get_IX m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2 writebw))).
 
 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
 ndefinition mode_SP1_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+   (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1)).
 
 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
 ndefinition mode_SP1_write ≝
@@ -514,7 +514,7 @@ ndefinition mode_SP1_write ≝
 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
-   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
+   (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1 writebw)).
 
 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
 ndefinition mode_SP2_load ≝
@@ -522,7 +522,7 @@ ndefinition mode_SP2_load ≝
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
+    (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2))).
 
 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
 ndefinition mode_SP2_write ≝
@@ -531,7 +531,7 @@ ndefinition mode_SP2_write ≝
  opt_map … (get_sp_reg m t s)
   (λaddr.opt_map … (memory_filter_read m t s cur_pc)
    (λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
-    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+    (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2 writebw))).
 
 (* ************************************** *)
 (* raccordo di tutte le possibili letture *)
@@ -548,8 +548,8 @@ ndefinition aux_inc_indX_16 ≝
 ndefinition multi_mode_load ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
  match byteflag
- return λbyteflag:bool.any_status m t → word16 → instr_mode → 
-  option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
+  return λbyteflag:bool.any_status m t → word16 → instr_mode → 
+                        option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
  with
   (* lettura di un byte *)
   [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
@@ -628,7 +628,7 @@ ndefinition multi_mode_load ≝
    | MODE_TNY e           ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
                              (λb.Some ? (triple … s b cur_pc))
 (* preleva 1 byte da 0000 0000 000x xxxxb *)
-   | MODE_SRT e           ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
+   | MODE_SRT e           ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:(b8_of_bit e)〉)
                              (λb.Some ? (triple … s b cur_pc))
    ]
 (* lettura di una word *)
@@ -865,7 +865,7 @@ ndefinition multi_mode_write ≝
   | MODE_TNY e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
                    (λtmps.Some ? (pair … tmps cur_pc))
 (* scrive 1 byte su 0000 0000 000x xxxxb *)
-  | MODE_SRT e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
+  | MODE_SRT e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:(b8_of_bit e)〉 writeb)
                       (λtmps.Some ? (pair … tmps cur_pc)) ]
  (* scrittura di una word *)
  | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with