X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fload_write.ma;h=28c78b6bb74164d64c5efd582fef2dc09451c5c6;hb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;hp=7f743cd3ea66b0033b0b3842b762dfec474defb2;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index 7f743cd3e..28c78b6bb 100644
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/load_write/".
-
-(*include "/media/VIRTUOSO/freescale/model.ma".*)
 include "freescale/model.ma".
 
 (* errori possibili nel fetch *)
@@ -97,7 +94,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
-         [ true ⇒ fMEM mem chk (or_w16 (fstT ?? (shr_w16 (fstT ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+         [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
                                              (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
 (*
    accesso normale
@@ -195,7 +192,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
-         [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fstT ?? (shr_w16 (fstT ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+         [ 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))
 (*
@@ -338,20 +335,20 @@ definition loadw_from ≝
 definition writeb_to ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
  opt_map ?? (memory_filter_write m t s addr writeb)
-  (λtmps.Some ? (pairT ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+  (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
 
 (* scrittura bit su addr *)
 definition writebit_to ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
  opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
-  (λtmps.Some ? (pairT ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+  (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
 
 (* scrittura word su addr *) 
 definition writew_to ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
  opt_map ?? (memory_filter_write m t s addr (w16h writew))
-  (λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
-    (λtmps'.Some ? (pairT ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
+  (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
+    (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
 
 (* ausiliari per definire i tipi e la lettura/scrittura *)
 
@@ -371,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 ≝
@@ -386,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.
@@ -461,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.
@@ -477,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.
@@ -549,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 *) 
@@ -618,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 *) 
@@ -744,22 +781,31 @@ 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 *)
   [ MODE_INH        ⇒ None ?
 (* scrive A *)
-  | MODE_INHA       ⇒ Some ? (pairT ?? (set_acc_8_low_reg m t s writeb) cur_pc)
+  | MODE_INHA       ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
 (* scrive X *)
   | MODE_INHX       ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
-                      (λtmps.Some ? (pairT ?? tmps cur_pc)) 
+                      (λtmps.Some ? (pair ?? tmps cur_pc)) 
 (* scrive H *)
   | MODE_INHH       ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
-                       (λtmps.Some ? (pairT ?? tmps cur_pc)) 
+                       (λ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 *)
@@ -783,22 +829,22 @@ definition multi_mode_write ≝
   | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
   | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
-                           (λS_and_PC.match S_and_PC with [ pairT S_op PC_op ⇒
+                           (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
                             (* H:X++ *)
                             opt_map ?? (aux_inc_indX_16 m t S_op)
-                             (λS_op'.Some ? (pairT ?? S_op' PC_op))])
+                             (λS_op'.Some ? (pair ?? S_op' PC_op))])
 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
   | MODE_DIR1_to_IX0p   ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
-                           (λS_and_PC.match S_and_PC with [ pairT S_op PC_op ⇒
+                           (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
                             (* H:X++ *)
                             opt_map ?? (aux_inc_indX_16 m t S_op)
-                             (λS_op'.Some ? (pairT ?? S_op' PC_op))])
+                             (λS_op'.Some ? (pair ?? S_op' PC_op))])
 
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
-  | MODE_INHA_and_IMM1 ⇒ Some ? (pairT ?? (set_acc_8_low_reg m t s writeb) cur_pc)
+  | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)  
   | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
-                           (λtmps.Some ? (pairT ?? tmps cur_pc)) 
+                           (λtmps.Some ? (pair ?? tmps cur_pc)) 
 (* NO: solo lettura word *) 
   | MODE_IMM1_and_IMM1 ⇒ None ?
 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *) 
@@ -820,10 +866,10 @@ definition multi_mode_write ≝
   | MODE_DIRn_and_IMM1 _ ⇒ None ?
 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
   | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
-                   (λtmps.Some ? (pairT ?? tmps cur_pc))
+                   (λ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)
-                      (λtmps.Some ? (pairT ?? tmps cur_pc)) ]
+                      (λ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
 (* NO: non ci sono indicazioni *)
@@ -835,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 *)