freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
index 74e04a498bdd838e1299482a7621f3ae26f3c9b9..9270e8ea8a8452fafd90480d43eef6ea51dcf185 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
@@ -21,15 +21,14 @@
 (* ********************************************************************** *)
 
 include "freescale/bool.ma".
+include "freescale/quatern.ma".
+include "freescale/oct.ma".
 include "freescale/prod.ma".
-include "freescale/nat.ma".
 
 (* *********** *)
 (* ESADECIMALI *)
 (* *********** *)
 
-(* non riesce a terminare l'esecuzione !!! *)
-
 ninductive exadecim : Type ≝
   x0: exadecim
 | x1: exadecim
@@ -52,86 +51,22 @@ ninductive exadecim : Type ≝
 ndefinition eq_ex ≝
 λe1,e2:exadecim.
  match e1 with
-  [ x0 ⇒ match e2 with
-   [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x1 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x2 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x3 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x4 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x5 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x6 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x7 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true 
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x8 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | x9 ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | xA ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | xB ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | xC ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-  | xD ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ] 
-  | xE ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ] 
-  | xF ⇒ match e2 with
-   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+  [ x0 ⇒ match e2 with [ x0 ⇒ true  | _ ⇒ false ]
+  | x1 ⇒ match e2 with [ x1 ⇒ true  | _ ⇒ false ]
+  | x2 ⇒ match e2 with [ x2 ⇒ true  | _ ⇒ false ]
+  | x3 ⇒ match e2 with [ x3 ⇒ true  | _ ⇒ false ]
+  | x4 ⇒ match e2 with [ x4 ⇒ true  | _ ⇒ false ]
+  | x5 ⇒ match e2 with [ x5 ⇒ true  | _ ⇒ false ]
+  | x6 ⇒ match e2 with [ x6 ⇒ true  | _ ⇒ false ]
+  | x7 ⇒ match e2 with [ x7 ⇒ true  | _ ⇒ false ]
+  | x8 ⇒ match e2 with [ x8 ⇒ true  | _ ⇒ false ]
+  | x9 ⇒ match e2 with [ x9 ⇒ true  | _ ⇒ false ]
+  | xA ⇒ match e2 with [ xA ⇒ true  | _ ⇒ false ]
+  | xB ⇒ match e2 with [ xB ⇒ true  | _ ⇒ false ]
+  | xC ⇒ match e2 with [ xC ⇒ true  | _ ⇒ false ]
+  | xD ⇒ match e2 with [ xD ⇒ true  | _ ⇒ false ]
+  | xE ⇒ match e2 with [ xE ⇒ true  | _ ⇒ false ]
+  | xF ⇒ match e2 with [ xF ⇒ true  | _ ⇒ false ]
   ].
 
 (* operatore < *)
@@ -777,10 +712,10 @@ ndefinition ror_ex ≝
  | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
- match n with
-  [ O ⇒ e
-  | S n' ⇒ ror_ex_n (ror_ex e) n' ].
+nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
+ match r with
+  [ qu_O ⇒ e
+  | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_ex ≝
@@ -826,10 +761,10 @@ ndefinition rol_ex ≝
  | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
- match n with
-  [ O ⇒ e
-  | S n' ⇒ rol_ex_n (rol_ex e) n' ].
+nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
+ match r with
+  [ qu_O ⇒ e
+  | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_ex ≝
@@ -1420,13 +1355,6 @@ ndefinition MSB_ex ≝
  | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ].
 
-(* esadecimali → naturali *)
-ndefinition nat_of_exadecim : exadecim → nat ≝
-λe:exadecim.
- match e with
-  [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2  | x3 ⇒ 3  | x4 ⇒ 4  | x5 ⇒ 5  | x6 ⇒ 6  | x7 ⇒ 7
-  | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
-
 (* operatore predecessore *)
 ndefinition pred_ex ≝
 λe:exadecim.
@@ -1450,6 +1378,42 @@ ndefinition compl_ex ≝
  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
 
 (* iteratore sugli esadecimali *)
-ndefinition forall_exadecim ≝ λP.
+ndefinition forall_ex ≝ λP.
  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
  P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
+
+(* esadecimali ricorsivi *)
+ninductive rec_exadecim : exadecim → Type ≝
+  ex_O : rec_exadecim x0
+| ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
+
+(* esadecimali → esadecimali ricorsivi *)
+ndefinition ex_to_recex ≝
+λn.match n return λx.rec_exadecim x with
+ [ x0 ⇒ ex_O
+ | x1 ⇒ ex_S ? ex_O
+ | x2 ⇒ ex_S ? (ex_S ? ex_O)
+ | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
+ | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
+ | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
+ | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
+ | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
+ | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
+ | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
+ | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
+ | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))
+ | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))
+ | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))
+ | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))
+ | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))))
+ ].
+
+(* quaternari → esadecimali *)
+ndefinition ex_of_qu ≝
+λn.match n with
+ [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
+
+(* ottali → esadecimali *)
+ndefinition ex_of_oct ≝
+λn.match n with
+ [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].