X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fload_write.ma;h=2eee12532fbf9efdd5b71248c1f668a1dca83800;hb=1ba7566bacd8d29e772646b3c86c7d5c944e9a6e;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..2eee12532 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 ≝
@@ -744,19 +741,19 @@ 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 byte *)
   | MODE_IMM1       ⇒ None ?
@@ -783,22 +780,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 +817,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 *)