freescale porting, work in progress

[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 88cbe3563c088306572d1b34212d9da6c37c2abd..7dd405eebcde214f4c503e128f0bfe88553126f1 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -90,10 +90,10 @@ ndefinition ror_w16 ≝
    | false ⇒ mk_word16 wh' wl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_w16_n (w:word16) (n:nat) on n ≝
- match n with
-  [ O ⇒ w
-  | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
+nlet rec ror_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
+ match r with
+  [ ex_O ⇒ w
+  | ex_S t n' ⇒ ror_w16_n (ror_w16 w) t n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_w16 ≝
@@ -116,10 +116,10 @@ ndefinition rol_w16 ≝
    | false ⇒ mk_word16 wh' wl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_w16_n (w:word16) (n:nat) on n ≝
- match n with
-  [ O ⇒ w
-  | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
+nlet rec rol_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
+ match r with
+  [ ex_O ⇒ w
+  | ex_S t n' ⇒ rol_w16_n (rol_w16 w) t n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_w16 ≝
@@ -164,9 +164,6 @@ ndefinition plus_w16_d_c ≝
 (* operatore Most Significant Bit *)
 ndefinition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
 
-(* word → naturali *)
-ndefinition nat_of_word16 ≝ λw:word16. 256 * (nat_of_byte8 (w16h w)) + (nat_of_byte8 (w16l w)).
-
 (* operatore predecessore *)
 ndefinition pred_w16 ≝
 λw:word16.match eq_b8 (w16l w) (mk_byte8 x0 x0) with
@@ -203,15 +200,15 @@ ndefinition mul_b8 ≝
 ]]]]]].
 
 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
+nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:oct) (rc:rec_oct c) on rc ≝
  let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
-  match c with
-  [ O ⇒ match le_w16 divs divd with
+  match rc with
+  [ oc_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〉)) ]
-  | 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' ]].
+  | oc_S t c' ⇒ match le_w16 divs divd with
+   [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) t c'
+   | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q t c' ]].
 
 ndefinition div_b8 ≝
 λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
@@ -227,15 +224,240 @@ ndefinition div_b8 ≝
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 (*    puo' essere sottratto al dividendo *) 
-  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
+  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]].
 
 (* operatore x in [inf,sup] *)
-ndefinition in_range ≝
+ndefinition inrange_w16 ≝
 λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
 
 (* iteratore sulle word *)
-ndefinition forall_word16 ≝
+ndefinition forall_w16 ≝
  λP.
-  forall_byte8 (λbh.
-  forall_byte8 (λbl.
+  forall_b8 (λbh.
+  forall_b8 (λbl.
    P (mk_word16 bh bl ))).
+
+(* word16 ricorsive *)
+ninductive rec_word16 : word16 → Type ≝
+  w16_O : rec_word16 〈〈x0,x0〉:〈x0,x0〉〉
+| w16_S : ∀n.rec_word16 n → rec_word16 (succ_w16 n).
+
+(* word16 → word16 ricorsive *)
+ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_2 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x2,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_1 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_3 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x3,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_2 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_4 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x4,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_3 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_5 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x5,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_4 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_6 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x6,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_5 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_7 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x7,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_6 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_8 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x8,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_7 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_9 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x9,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_8 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_10 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xA,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_9 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_11 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xB,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_10 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_12 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xC,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_11 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_13 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xD,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_12 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_14 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xE,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_13 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1_15 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xF,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_14 ? recw)
+ ))))))))))))))).
+
+ndefinition w16_to_recw16_aux1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈(succ_b8 n):〈x0,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_15 ? recw)
+ ))))))))))))))).
+
+(* ... cifra byte superiore *)
+nlet rec w16_to_recw16_aux2 (n:byte8) (r:rec_byte8 n) on r ≝
+ match r return λx.λy:rec_byte8 x.rec_word16 〈x:〈x0,x0〉〉 with
+  [ b8_O ⇒ w16_O
+  | b8_S t n' ⇒ w16_to_recw16_aux1 ? (w16_to_recw16_aux2 t n')
+  ].
+
+(* ... cifra esadecimale n.2 *)
+ndefinition w16_to_recw16_aux3 ≝
+λb,n.λrecw:rec_word16 〈b:〈x0,x0〉〉.
+ match n return λx.rec_word16 〈b:〈x,x0〉〉 with
+ [ x0 ⇒ recw
+ | x1 ⇒ w16_to_recw16_aux1_1 ? recw
+ | x2 ⇒ w16_to_recw16_aux1_2 ? recw
+ | x3 ⇒ w16_to_recw16_aux1_3 ? recw
+ | x4 ⇒ w16_to_recw16_aux1_4 ? recw
+ | x5 ⇒ w16_to_recw16_aux1_5 ? recw
+ | x6 ⇒ w16_to_recw16_aux1_6 ? recw
+ | x7 ⇒ w16_to_recw16_aux1_7 ? recw
+ | x8 ⇒ w16_to_recw16_aux1_8 ? recw
+ | x9 ⇒ w16_to_recw16_aux1_9 ? recw
+ | xA ⇒ w16_to_recw16_aux1_10 ? recw
+ | xB ⇒ w16_to_recw16_aux1_11 ? recw
+ | xC ⇒ w16_to_recw16_aux1_12 ? recw
+ | xD ⇒ w16_to_recw16_aux1_13 ? recw
+ | xE ⇒ w16_to_recw16_aux1_14 ? recw
+ | xF ⇒ w16_to_recw16_aux1_15 ? recw
+ ].
+
+nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? input).
+nqed.
+
+nlemma w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_1 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_3 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x3〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_2 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_4 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x4〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_3 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_5 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x5〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_4 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_6 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x6〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_5 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_7 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x7〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_6 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_8 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x8〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_7 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_9 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x9〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_8 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_10 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xA〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_9 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_11 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xB〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_10 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_12 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xC〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_11 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_13 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xD〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_12 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_14 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xE〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_13 … input)).
+nqed.
+
+nlemma w16_to_recw16_aux4_15 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xF〉〉.
+ #n; #e; nelim e; #input; napply (w16_S ? (w16_to_recw16_aux4_14 … input)).
+nqed.
+
+(* ... cifra esadecimale n.1 *)
+ndefinition w16_to_recw16_aux4 ≝
+λb,e,n.λrecw:rec_word16 〈b:〈e,x0〉〉.
+ match n return λx.rec_word16 〈b:〈e,x〉〉 with
+ [ x0 ⇒ recw
+ | x1 ⇒ w16_to_recw16_aux4_1 … recw
+ | x2 ⇒ w16_to_recw16_aux4_2 … recw
+ | x3 ⇒ w16_to_recw16_aux4_3 … recw
+ | x4 ⇒ w16_to_recw16_aux4_4 … recw
+ | x5 ⇒ w16_to_recw16_aux4_5 … recw
+ | x6 ⇒ w16_to_recw16_aux4_6 … recw
+ | x7 ⇒ w16_to_recw16_aux4_7 … recw
+ | x8 ⇒ w16_to_recw16_aux4_8 … recw
+ | x9 ⇒ w16_to_recw16_aux4_9 … recw
+ | xA ⇒ w16_to_recw16_aux4_10 … recw
+ | xB ⇒ w16_to_recw16_aux4_11 … recw
+ | xC ⇒ w16_to_recw16_aux4_12 … recw
+ | xD ⇒ w16_to_recw16_aux4_13 … recw
+ | xE ⇒ w16_to_recw16_aux4_14 … recw
+ | xF ⇒ w16_to_recw16_aux4_15 … recw
+ ].
+
+nlemma w16_to_recw16_aux5 : ∀b.rec_byte8 (〈b8h b,b8l b〉) → rec_byte8 b.
+ #b; nelim b; #e1; #e2; nnormalize; #input; napply input. nqed.
+
+ndefinition w16_to_recw16 ≝
+λn.w16_to_recw16_aux4 (w16h n) (b8h (w16l n)) (b8l (w16l n))
+    (w16_to_recw16_aux3 (w16h n) (b8h (w16l n)) (w16_to_recw16_aux2 (w16h n) ?)).
+ nelim n; #b1; #b2;
+ nchange with (rec_byte8 b1);
+ napply (w16_to_recw16_aux5 b1);
+ napply (b8_to_recb8 b1).
+nqed.