X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fload_write.ma;h=28c78b6bb74164d64c5efd582fef2dc09451c5c6;hb=7845d9d0221d94418beecf3d7c3aed3efb2af7fc;hp=16df9aae4a1874b3168337a0e353656dc960b7ee;hpb=09e3a050664b07c961a92bf16245a7345346f964;p=helm.git

diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index 16df9aae4..28c78b6bb 100644
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -368,7 +368,7 @@ definition aux_write_typing ≝
 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  any_status m t → word16 → word16 → nat →
  match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
- option (ProdT (any_status m t) word16).
+ option (Prod (any_status m t) word16).
 
 (* per non dover ramificare i vari load in byte/word *)
 definition aux_write ≝
@@ -383,6 +383,12 @@ definition mode_IMM1_load ≝
  opt_map ?? (memory_filter_read m t s cur_pc)
   (λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
 
+(* lettura da [curpc]: IMM1 + estensione a word *)
+definition mode_IMM1EXT_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)
+  (λb.Some ? (tripleT ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
+
 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
 definition mode_IMM2_load ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
@@ -458,6 +464,13 @@ definition mode_IX1_load ≝
   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
    (λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
 
+(* lettura da X+[byte curpc] *)
+definition mode_IX1ADD_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)
+  (λb.opt_map ?? (get_IX m t s)
+   (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
+
 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
 definition mode_IX1_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
@@ -474,6 +487,14 @@ definition mode_IX2_load ≝
    (λ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_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
 
+(* lettura da X+[word curpc] *)
+definition mode_IX2ADD_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.opt_map ?? (get_IX m t s)
+    (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+
 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 definition mode_IX2_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
@@ -546,8 +567,17 @@ definition multi_mode_load ≝
    | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
                   (λindx.Some ? (tripleT ??? s indx cur_pc))
 
+(* NO: solo lettura word *)
+  | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_INHX2ADD ⇒ None ?
+
 (* preleva 1 byte immediato *) 
    | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
+(* NO: solo lettura word *)
+   | MODE_IMM1EXT ⇒ None ?
 (* NO: solo lettura word *)
    | MODE_IMM2 ⇒ None ?
 (* preleva 1 byte da indirizzo diretto 1 byte *) 
@@ -615,8 +645,18 @@ definition multi_mode_load ≝
 (* NO: solo lettura/scrittura byte *)
    | MODE_INHH ⇒ None ?
 
+(* preleva 1 word immediato *) 
+  | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
+                     (λw.Some ? (tripleT ??? s w cur_pc))
+(* preleva 1 word immediato *) 
+  | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
+(* preleva 1 word immediato *) 
+  | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
+
 (* NO: solo lettura byte *)
    | MODE_IMM1 ⇒ None ?
+(* preleva 1 word immediato *) 
+   | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
 (* preleva 1 word immediato *) 
    | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
 (* preleva 1 word da indirizzo diretto 1 byte *) 
@@ -741,7 +781,7 @@ definition multi_mode_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
  return λbyteflag:bool.any_status m t → word16 → instr_mode →
   match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
-  option (ProdT (any_status m t) word16) with
+  option (Prod (any_status m t) word16) with
  (* scrittura di un byte *)
  [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
 (* NO: non ci sono indicazioni *)
@@ -755,8 +795,17 @@ definition multi_mode_write ≝
   | MODE_INHH       ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
                        (λtmps.Some ? (pair ?? tmps cur_pc)) 
 
+(* NO: solo lettura word *)
+  | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_INHX2ADD ⇒ None ?
+
 (* NO: solo lettura byte *)
   | MODE_IMM1       ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_IMM1EXT    ⇒ None ?
 (* NO: solo lettura word *)
   | MODE_IMM2       ⇒ None ?
 (* scrive 1 byte su indirizzo diretto 1 byte *)
@@ -832,8 +881,17 @@ definition multi_mode_write ≝
 (* NO: solo lettura/scrittura byte *)
   | MODE_INHH       ⇒ None ?
 
+(* NO: solo lettura word *)
+  | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_INHX2ADD ⇒ None ?
+
 (* NO: solo lettura byte *)
   | MODE_IMM1       ⇒ None ?
+(* NO: solo lettura word *)
+  | MODE_IMM1EXT    ⇒ None ?
 (* NO: solo lettura word *)
   | MODE_IMM2       ⇒ None ?
 (* scrive 1 word su indirizzo diretto 1 byte *)