1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / word32.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
index 0887f799148f14428e3e9202adac0047f3033a6e..fa57c68f5f919063c785578cc226ad81a2e6089d 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
@@ -73,13 +73,13 @@ ndefinition xor_w32 ≝
 ndefinition rcr_w32 ≝
 λdw:word32.λc:bool.match rcr_w16 (w32h dw) c with
  [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
-  [ pair wl' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]]. 
+  [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. 
 
 (* operatore shift destro *)
 ndefinition shr_w32 ≝
 λdw:word32.match rcr_w16 (w32h dw) false with
  [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
-  [ pair wl' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
+  [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_w32 ≝
@@ -99,13 +99,13 @@ nlet rec ror_w32_n (dw:word32) (n:nat) on n ≝
 ndefinition rcl_w32 ≝
 λdw:word32.λc:bool.match rcl_w16 (w32l dw) c with
  [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
-  [ pair wh' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]]. 
+  [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. 
 
 (* operatore shift sinistro *)
 ndefinition shl_w32 ≝
 λdw:word32.match rcl_w16 (w32l dw) false with
  [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
-  [ pair wh' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
+  [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_w32 ≝
@@ -130,7 +130,7 @@ ndefinition plus_w32_dc_dc ≝
 λdw1,dw2:word32.λc:bool.
  match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
   [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
-   [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_w32_dc_d ≝
@@ -148,7 +148,7 @@ ndefinition plus_w32_d_dc ≝
 λdw1,dw2:word32.
  match plus_w16_d_dc (w32l dw1) (w32l dw2) with
   [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
-   [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
 
 (* operatore somma con data → data *)
 ndefinition plus_w32_d_d ≝
@@ -207,8 +207,8 @@ nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat
   let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
    match c with
    [ O ⇒ match le_w32 divs divd with
-    [ true ⇒ triple ??? (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
-    | false ⇒ triple ??? q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
+    [ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
+    | false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
    | S c' ⇒ match le_w32 divs divd with
     [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
     | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q c' ]].
@@ -218,10 +218,10 @@ ndefinition div_w16 ≝
 (* 
    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
 *)
- [ true ⇒ triple ??? 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
+ [ true ⇒ triple … 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
  | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 with
 (* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
-  [ true ⇒ triple ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
+  [ true ⇒ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
 (* 1) e' una divisione sensata che produrra' overflow/risultato *)
 (* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)