1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
index 90ebbe8ae23a4e8234d018982c6bbd112c82fae9..88cbe3563c088306572d1b34212d9da6c37c2abd 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -32,21 +32,6 @@ nrecord word16 : Type ≝
  w16l: byte8
  }.
 
-ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Prop.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition word16_rec : ΠP:word16 → Set.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Set.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition word16_rect : ΠP:word16 → Type.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Type.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition w16h ≝ λw:word16.match w with [ mk_word16 x _ ⇒ x ].
-ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].
-
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
  for @{ 'mk_word16 $x $y }.
@@ -88,13 +73,13 @@ ndefinition xor_w16 ≝
 ndefinition rcr_w16 ≝
 λw:word16.λc:bool.match rcr_b8 (w16h w) c with
  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
-  [ pair wl' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]]. 
+  [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. 
 
 (* operatore shift destro *)
 ndefinition shr_w16 ≝
 λw:word16.match rcr_b8 (w16h w) false with
  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
-  [ pair wl' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
+  [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_w16 ≝
@@ -114,13 +99,13 @@ nlet rec ror_w16_n (w:word16) (n:nat) on n ≝
 ndefinition rcl_w16 ≝
 λw:word16.λc:bool.match rcl_b8 (w16l w) c with
  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
-  [ pair wh' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]]. 
+  [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. 
 
 (* operatore shift sinistro *)
 ndefinition shl_w16 ≝
 λw:word16.match rcl_b8 (w16l w) false with
  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
-  [ pair wh' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
+  [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_w16 ≝
@@ -145,7 +130,7 @@ ndefinition plus_w16_dc_dc ≝
 λw1,w2:word16.λc:bool.
  match plus_b8_dc_dc (w16l w1) (w16l w2) c with
   [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with
-   [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h:l〉 c' ]].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_w16_dc_d ≝
@@ -163,7 +148,7 @@ ndefinition plus_w16_d_dc ≝
 λw1,w2:word16.
  match plus_b8_d_dc (w16l w1) (w16l w2) with
   [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with
-   [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h:l〉 c' ]].
 
 (* operatore somma con data → data *)
 ndefinition plus_w16_d_d ≝
@@ -222,8 +207,8 @@ nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) o
  let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
   match c with
   [ O ⇒ match le_w16 divs divd with
-   [ true ⇒ triple ??? (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
-   | false ⇒ triple ??? q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
+   [ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
+   | false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
   | S c' ⇒ match le_w16 divs divd with
    [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
    | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q c' ]].
@@ -233,10 +218,10 @@ ndefinition div_b8 ≝
 (* 
    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
 *)
- [ true ⇒ triple ??? 〈xF,xF〉 (w16l w) true
+ [ true ⇒ triple … 〈xF,xF〉 (w16l w) true
  | false ⇒ match eq_w16 w 〈〈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〉 false
+  [ true ⇒ triple … 〈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 *)