New version of freescale:

[helm.git] / helm / software / matita / library / freescale / load_write.ma

diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index a5fae5375e8f52197421f35ffddded2e7e5e6fdf..28c78b6bb74164d64c5efd582fef2dc09451c5c6 100644 (file)
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -260,12 +260,10 @@ definition filtered_inc_w16 ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
  get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
 
-definition filtered_plus_w16 := \lambda m:mcu_type.
-let rec filtered_plus_w16  (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
+let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
  match n with
   [ O ⇒ w
-  | S n' ⇒ filtered_plus_w16 t s (filtered_inc_w16 m t s w) n' ]
-in filtered_plus_w16.
+  | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
 
 (* 
    errore1: non esiste traduzione ILL_OP
@@ -385,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.
@@ -460,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.
@@ -476,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.
@@ -548,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 *) 
@@ -617,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 *) 
@@ -757,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 *)
@@ -834,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 *)