freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index eb92c8f2d584f2603c07d34673950f28675c4a7b..62de47a89eb50603f63def979c402ab6f0c385e3 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -713,10 +713,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) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+  [ qu_O ⇒ e
+  | qu_S q' n' ⇒ ror_ex_n (ror_ex e) q' n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_ex ≝
@@ -762,10 +762,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) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+  [ qu_O ⇒ e
+  | qu_S q' n' ⇒ rol_ex_n (rol_ex e) q' n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_ex ≝
@@ -1378,9 +1378,12 @@ ndefinition compl_ex ≝
  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
 
-(* operatore x in [inf,sup] *)
+(* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_ex ≝
-λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup).
+λx,inf,sup:exadecim.
+ match le_ex inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_ex inf x) (le_ex x sup).
 
 (* iteratore sugli esadecimali *)
 ndefinition forall_ex ≝ λP.