(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
| 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 ≝
| 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 ≝
| x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
| xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_ex ≝
+λ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.
P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗