X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fload_write.ma;h=28704ff34828f4db950c29e38d8ca28fcf930dff;hb=601baed778a190b580982b588ebe49ba3f762b30;hp=766be3772c7c876851c37ab2f80d59200fbfb79b;hpb=842e243be954d67360788d08701289f3237c2699;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 766be3772..28704ff34 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,8 +90,8 @@ 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 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+        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〉〉))
 (*
    accesso normale
@@ -181,21 +181,21 @@ match s with
    altrimenti sarebbero 2 indirezioni
 *)
       match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
-       [ true ⇒ opt_map ?? (fMEM mem chk 〈〈x0,x0〉:xm〉)
+       [ true ⇒ opt_map … (fMEM mem chk 〈〈x0,x0〉:xm〉)
                  (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
                                                       
        | false ⇒
 (* 
    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 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+        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))
 (*
    accesso normale
 *)
-         | false ⇒ opt_map ?? (fMEM mem chk addr)
+         | false ⇒ opt_map … (fMEM mem chk addr)
                     (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
 
 (* scrittura RS08 di un byte *)
@@ -217,13 +217,13 @@ ndefinition memory_filter_write ≝
 λm:mcu_type.λt:memory_impl.match m
  return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
-  opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
+  opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
-  opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
+  opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
-  opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
+  opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
   RS08_memory_filter_write t s addr val
@@ -233,13 +233,13 @@ ndefinition memory_filter_write_bit ≝
 λm:mcu_type.λt:memory_impl.match m
  return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
-  opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
+  opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
-  opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
+  opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
-  opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
+  opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
   RS08_memory_filter_write_bit t s addr sub val
@@ -312,40 +312,40 @@ ndefinition fetch ≝
 (* lettura byte da addr *)
 ndefinition loadb_from ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
- opt_map ?? (memory_filter_read m t s addr)
-  (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_read m t s addr)
+  (λb.Some ? (triple … s b (filtered_plus_w16 m t s cur_pc fetched))).
 
 (* lettura bit da addr *)
 ndefinition loadbit_from ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
- opt_map ?? (memory_filter_read_bit m t s addr sub)
-  (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_read_bit m t s addr sub)
+  (λb.Some ? (triple … s b (filtered_plus_w16 m t s cur_pc fetched))).
 
 (* lettura word da addr *)
 ndefinition loadw_from ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
- opt_map ?? (memory_filter_read m t s addr)
-  (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
-   (λbl.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
+ opt_map … (memory_filter_read m t s addr)
+  (λbh.opt_map … (memory_filter_read m t s (succ_w16 addr))
+   (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
 
 (* scrittura byte su addr *)
 ndefinition 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 ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_write m t s addr writeb)
+  (λtmps.Some ? (pair … tmps (filtered_plus_w16 m t s cur_pc fetched))).
 
 (* scrittura bit su addr *)
 ndefinition 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 ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_write_bit m t s addr sub writeb)
+  (λtmps.Some ? (pair … tmps (filtered_plus_w16 m t s cur_pc fetched))).
 
 (* scrittura word su addr *) 
 ndefinition 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))
-  (λ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)))).
+ opt_map … (memory_filter_write m t s addr (w16h writew))
+  (λ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 *)
 
@@ -377,160 +377,160 @@ ndefinition aux_write ≝
 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
 ndefinition mode_IMM1_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 ? (triple ??? s b (filtered_inc_w16 m t s cur_pc))).
+ opt_map … (memory_filter_read m t s cur_pc)
+  (λb.Some ? (triple … s b (filtered_inc_w16 m t s cur_pc))).
 
 (* lettura da [curpc]: IMM1 + estensione a word *)
 ndefinition 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 ? (triple ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
+ opt_map … (memory_filter_read m t s cur_pc)
+  (λb.Some ? (triple … s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
 
 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
 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)))).
+ 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)))).
 
 (* 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)
+ opt_map … (memory_filter_read m t s cur_pc)
   (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
 
 (* 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)
+ opt_map … (memory_filter_read m t s cur_pc)
   (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
 
 (* 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)
+ opt_map … (memory_filter_read m t s cur_pc)
   (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 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)
+ opt_map … (memory_filter_read m t s cur_pc)
   (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 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))
+ 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)).
 
 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
 ndefinition mode_DIR2_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)
-  (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ 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)).
 
 ndefinition get_IX ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  match m with
-  [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉) 
-  | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx) 
-  | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx) 
+  [ HC05 ⇒ opt_map … (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉) 
+  | HC08 ⇒ opt_map … (get_indX_16_reg m t s) (λindx.Some ? indx) 
+  | HCS08 ⇒ opt_map … (get_indX_16_reg m t s) (λindx.Some ? indx) 
   | RS08 ⇒ None ? ].
 
 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
 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)
+ opt_map … (get_IX m t s)
   (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
 
 (* 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)
+ opt_map … (get_IX m t s)
   (λaddr.(aux_write m t byteflag) s addr cur_pc 0 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)
+ 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)).
 
 (* lettura da X+[byte curpc] *)
 ndefinition 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 ? (triple ??? s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
+ opt_map … (memory_filter_read m t s cur_pc)
+  (λb.opt_map … (get_IX m t s)
+   (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
 
 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
 ndefinition mode_IX1_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.opt_map ?? (memory_filter_read m t s cur_pc)
+ 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)).
 
 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
 ndefinition mode_IX2_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)
-   (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ 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))).
 
 (* lettura da X+[word curpc] *)
 ndefinition 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 ? (triple ??? s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+ 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))))).
 
 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 ndefinition mode_IX2_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.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))
+ 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))).
 
 (* 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)
+ 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)).
 
 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
 ndefinition mode_SP1_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_sp_reg m t s)
-  (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
+ 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)).
 
 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
 ndefinition mode_SP2_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)
-   (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ 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))).
 
 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
 ndefinition mode_SP2_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_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))
+ 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))).
 
 (* ************************************** *)
@@ -540,29 +540,29 @@ ndefinition mode_SP2_write ≝
 (* H:X++ *)
 ndefinition aux_inc_indX_16 ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
- opt_map ?? (get_indX_16_reg m t s)
-  (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
+ opt_map … (get_indX_16_reg m t s)
+  (λX_op.opt_map … (set_indX_16_reg m t s (succ_w16 X_op))
    (λs_tmp.Some ? s_tmp)).
 
 (* tutte le modalita' di lettura: false=loadb true=loadw *)
 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
 (* NO: non ci sono indicazioni *)
    [ MODE_INH  ⇒ None ?
 (* restituisce A *)
-   | MODE_INHA ⇒ Some ? (triple ??? s (get_acc_8_low_reg m t s) cur_pc)
+   | MODE_INHA ⇒ Some ? (triple … s (get_acc_8_low_reg m t s) cur_pc)
 (* restituisce X *)
-   | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
-                  (λindx.Some ? (triple ??? s indx cur_pc))
+   | MODE_INHX ⇒ opt_map … (get_indX_8_low_reg m t s)
+                  (λindx.Some ? (triple … s indx cur_pc))
 (* restituisce H *)
-   | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
-                  (λindx.Some ? (triple ??? s indx cur_pc))
+   | MODE_INHH ⇒ opt_map … (get_indX_8_high_reg m t s)
+                  (λindx.Some ? (triple … s indx cur_pc))
 
 (* NO: solo lettura word *)
   | MODE_INHX0ADD ⇒ None ?
@@ -625,11 +625,11 @@ ndefinition multi_mode_load ≝
 (* NO: solo lettura word *)
    | MODE_DIRn_and_IMM1 _ ⇒ None ?
 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
-   | MODE_TNY e           ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
-                             (λb.Some ? (triple ??? s b cur_pc))
+   | 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)〉)
-                             (λb.Some ? (triple ??? s b cur_pc))
+   | 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 *)
   | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
@@ -643,8 +643,8 @@ ndefinition multi_mode_load ≝
    | MODE_INHH ⇒ None ?
 
 (* preleva 1 word immediato *) 
-  | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
-                     (λw.Some ? (triple ??? s w cur_pc))
+  | MODE_INHX0ADD ⇒ opt_map … (get_IX m t s)
+                     (λw.Some ? (triple … s w cur_pc))
 (* preleva 1 word immediato *) 
   | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
 (* preleva 1 word immediato *) 
@@ -681,87 +681,87 @@ ndefinition multi_mode_load ≝
    | MODE_DIR1_to_IX0p ⇒ None ?
 
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
+   | MODE_INHA_and_IMM1 ⇒ opt_map … (mode_IMM1_load m t s cur_pc)
                            (λS_immb_and_PC.match S_immb_and_PC with
                             [ triple _ immb cur_pc' ⇒
-                             Some ? (triple ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
+                             Some ? (triple … s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
-                           (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
+   | MODE_INHX_and_IMM1 ⇒ opt_map … (get_indX_8_low_reg m t s)
+                           (λX_op.opt_map … (mode_IMM1_load m t s cur_pc)
                             (λS_immb_and_PC.match S_immb_and_PC with
                              [ triple _ immb cur_pc' ⇒
-                              Some ? (triple ??? s 〈X_op:immb〉 cur_pc')]))
+                              Some ? (triple … s 〈X_op:immb〉 cur_pc')]))
 (* preleva 2 byte, NO possibilita' modificare Io argomento *)               
-   | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
+   | MODE_IMM1_and_IMM1 ⇒ opt_map … (mode_IMM1_load m t s cur_pc)
                            (λS_immb1_and_PC.match S_immb1_and_PC with
                             [ triple _ immb1 cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb2_and_PC.match S_immb2_and_PC with
                                [ triple _ immb2 cur_pc'' ⇒
-                                Some ? (triple ??? s 〈immb1:immb2〉 cur_pc'')])])
+                                Some ? (triple … s 〈immb1:immb2〉 cur_pc'')])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
+   | MODE_DIR1_and_IMM1 ⇒ opt_map … (mode_DIR1_load true m t s cur_pc)
                            (λS_dirb_and_PC.match S_dirb_and_PC with
                             [ triple _ dirb cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb_and_PC.match S_immb_and_PC with
                                [ triple _ immb cur_pc'' ⇒
-                                Some ? (triple ??? s 〈dirb:immb〉 cur_pc'')])])
+                                Some ? (triple … s 〈dirb:immb〉 cur_pc'')])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_IX0_and_IMM1  ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
+   | MODE_IX0_and_IMM1  ⇒ opt_map … (mode_IX0_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ triple _ ixb cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb_and_PC.match S_immb_and_PC with
                                [ triple _ immb cur_pc'' ⇒
-                                Some ? (triple ??? s 〈ixb:immb〉 cur_pc'')])])
+                                Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
-   | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
+   | MODE_IX0p_and_IMM1 ⇒ opt_map … (mode_IX0_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ triple _ ixb cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb_and_PC.match S_immb_and_PC with
                                [ triple _ immb cur_pc'' ⇒
                                 (* H:X++ *)
-                                opt_map ?? (aux_inc_indX_16 m t s)
-                                 (λs'.Some ? (triple ??? s' 〈ixb:immb〉 cur_pc''))])])
+                                opt_map … (aux_inc_indX_16 m t s)
+                                 (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_IX1_and_IMM1  ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
+   | MODE_IX1_and_IMM1  ⇒ opt_map … (mode_IX1_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ triple _ ixb cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb_and_PC.match S_immb_and_PC with
                                [ triple _ immb cur_pc'' ⇒
-                                Some ? (triple ??? s 〈ixb:immb〉 cur_pc'')])])
+                                Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
-   | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
+   | MODE_IX1p_and_IMM1 ⇒ opt_map … (mode_IX1_load true m t s cur_pc)
                            (λS_ixb_and_PC.match S_ixb_and_PC with
                             [ triple _ ixb cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb_and_PC.match S_immb_and_PC with
                                [ triple _ immb cur_pc'' ⇒
                                 (* H:X++ *)
-                                opt_map ?? (aux_inc_indX_16 m t s)
-                                 (λs'.Some ? (triple ??? s' 〈ixb:immb〉 cur_pc''))])])
+                                opt_map … (aux_inc_indX_16 m t s)
+                                 (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
 (* preleva 2 byte, possibilita' modificare Io argomento *)
-   | MODE_SP1_and_IMM1  ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
+   | MODE_SP1_and_IMM1  ⇒ opt_map … (mode_SP1_load true m t s cur_pc)
                            (λS_spb_and_PC.match S_spb_and_PC with
                             [ triple _ spb cur_pc' ⇒
-                             opt_map ?? (mode_IMM1_load m t s cur_pc')
+                             opt_map … (mode_IMM1_load m t s cur_pc')
                               (λS_immb_and_PC.match S_immb_and_PC with
                                [ triple _ immb cur_pc'' ⇒
-                                Some ? (triple ??? s 〈spb:immb〉 cur_pc'')])])
+                                Some ? (triple … s 〈spb:immb〉 cur_pc'')])])
 
 (* NO: solo scrittura byte *)
    | MODE_DIRn _            ⇒ None ?
 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
-   | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
+   | MODE_DIRn_and_IMM1 msk ⇒ opt_map … (mode_DIR1n_load m t s cur_pc msk)
                                (λS_dirbn_and_PC.match S_dirbn_and_PC with
                                 [ triple _ dirbn cur_pc'   ⇒
-                                 opt_map ?? (mode_IMM1_load m t s cur_pc')
+                                 opt_map … (mode_IMM1_load m t s cur_pc')
                                   (λS_immb_and_PC.match S_immb_and_PC with
                                    [ triple _ immb cur_pc'' ⇒
-                                     Some ? (triple ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
+                                     Some ? (triple … s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
 (* NO: solo lettura/scrittura byte *)
    | MODE_TNY _             ⇒ None ?
 (* NO: solo lettura/scrittura byte *)
@@ -784,13 +784,13 @@ ndefinition multi_mode_write ≝
 (* NO: non ci sono indicazioni *)
   [ MODE_INH        ⇒ None ?
 (* scrive A *)
-  | MODE_INHA       ⇒ Some ? (pair ?? (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 ? (pair ?? tmps cur_pc)) 
+  | MODE_INHX       ⇒ opt_map … (set_indX_8_low_reg m t s writeb)
+                      (λtmps.Some ? (pair … tmps cur_pc)) 
 (* scrive H *)
-  | MODE_INHH       ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
-                       (λtmps.Some ? (pair ?? tmps cur_pc)) 
+  | 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 ?
@@ -825,23 +825,23 @@ ndefinition multi_mode_write ≝
 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
   | 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)
+  | MODE_IX0p_to_DIR1   ⇒ opt_map … (mode_DIR1_write true m t s cur_pc writeb)
                            (λ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 ? (pair ?? S_op' PC_op))])
+                            opt_map … (aux_inc_indX_16 m t S_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)
+  | MODE_DIR1_to_IX0p   ⇒ opt_map … (mode_IX0_write true m t s cur_pc writeb)
                            (λ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 ? (pair ?? S_op' PC_op))])
+                            opt_map … (aux_inc_indX_16 m t S_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 ? (pair ?? (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 ? (pair ?? tmps cur_pc)) 
+  | MODE_INHX_and_IMM1 ⇒ opt_map … (set_indX_8_low_reg m t s writeb)
+                           (λ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 *) 
@@ -862,11 +862,11 @@ ndefinition multi_mode_write ≝
 (* NO: solo lettura word *)
   | 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 ? (pair ?? tmps cur_pc))
+  | 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)
-                      (λtmps.Some ? (pair ?? tmps cur_pc)) ]
+  | 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
 (* NO: non ci sono indicazioni *)