--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/byte8.ma".
+
+(* ********* *)
+(* BYTE+WORD *)
+(* ********* *)
+
+nrecord word24 : Type ≝
+ {
+ w24x: byte8;
+ w24h: byte8;
+ w24l: byte8
+ }.
+
+(* \langle \rangle *)
+notation "〈x;y;z〉" non associative with precedence 80
+ for @{ 'mk_word24 $x $y $z }.
+interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
+
+(* operatore = *)
+ndefinition eq_w24 ≝
+λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
+ (eq_b8 (w24h w1) (w24h w2)) ⊗
+ (eq_b8 (w24l w1) (w24l w2)).
+
+(* operatore < *)
+ndefinition lt_w24 ≝
+λw1,w2:word24.
+ (lt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (lt_b8 (w24l w1) (w24l w2))))).
+
+(* operatore ≤ *)
+ndefinition le_w24 ≝
+λw1,w2:word24.
+ (lt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (le_b8 (w24l w1) (w24l w2))))).
+
+(* operatore > *)
+ndefinition gt_w24 ≝
+λw1,w2:word24.
+ (gt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (gt_b8 (w24l w1) (w24l w2))))).
+
+(* operatore ≥ *)
+ndefinition ge_w24 ≝
+λw1,w2:word24.
+ (gt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (ge_b8 (w24l w1) (w24l w2))))).
+
+(* operatore and *)
+ndefinition and_w24 ≝
+λw1,w2:word24.
+ mk_word24 (and_b8 (w24x w1) (w24x w2))
+ (and_b8 (w24h w1) (w24h w2))
+ (and_b8 (w24l w1) (w24l w2)).
+
+(* operatore or *)
+ndefinition or_w24 ≝
+λw1,w2:word24.
+ mk_word24 (or_b8 (w24x w1) (w24x w2))
+ (or_b8 (w24h w1) (w24h w2))
+ (or_b8 (w24l w1) (w24l w2)).
+
+(* operatore xor *)
+ndefinition xor_w24 ≝
+λw1,w2:word24.
+ mk_word24 (xor_b8 (w24x w1) (w24x w2))
+ (xor_b8 (w24h w1) (w24h w2))
+ (xor_b8 (w24l w1) (w24l w2)).
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_w24 ≝
+λw:word24.λc:bool.match rcr_b8 (w24x w) c with
+ [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
+ [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore shift destro *)
+ndefinition shr_w24 ≝
+λw:word24.match shr_b8 (w24x w) with
+ [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
+ [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore rotazione destra *)
+ndefinition ror_w24 ≝
+λw:word24.match shr_b8 (w24x w) with
+ [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
+ [ pair wl' c''' ⇒ match c''' with
+ [ true ⇒ mk_word24 (or_b8 (mk_byte8 x8 x0) wx') wh' wl'
+ | false ⇒ mk_word24 wx' wh' wl' ]]]].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ w
+ | bi_S t' n' ⇒ ror_w24_n (ror_w24 w) t' n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_w24 ≝
+λw:word24.λc:bool.match rcl_b8 (w24l w) c with
+ [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
+ [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore shift sinistro *)
+ndefinition shl_w24 ≝
+λw:word24.match shl_b8 (w24l w) with
+ [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
+ [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_w24 ≝
+λw:word24.match shl_b8 (w24l w) with
+ [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
+ [ pair wx' c''' ⇒ match c''' with
+ [ true ⇒ mk_word24 wx' wh' (or_b8 (mk_byte8 x0 x1) wl')
+ | false ⇒ mk_word24 wx' wh' wl' ]]]].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ w
+ | bi_S t' n' ⇒ rol_w24_n (rol_w24 w) t' n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_w24 ≝
+λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_w24_dc_dc ≝
+λw1,w2:word24.λc:bool.
+ match plus_b8_dc_dc (w24l w1) (w24l w2) c with
+ [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
+ [ pair h c'' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c'' with
+ [ pair x c''' ⇒ pair … 〈x;h;l〉 c''' ]]].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_w24_dc_d ≝
+λw1,w2:word24.λc:bool.
+ match plus_b8_dc_dc (w24l w1) (w24l w2) c with
+ [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
+ [ pair h c'' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c'';h;l〉 ]].
+
+(* operatore somma con data+carry → c *)
+ndefinition plus_w24_dc_c ≝
+λw1,w2:word24.λc:bool.
+ plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_dc_c (w24l w1) (w24l w2) c)).
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_w24_d_dc ≝
+λw1,w2:word24.
+ match plus_b8_d_dc (w24l w1) (w24l w2) with
+ [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
+ [ pair h c' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c' with
+ [ pair x c'' ⇒ pair … 〈x;h;l〉 c'' ]]].
+
+(* operatore somma con data → data *)
+ndefinition plus_w24_d_d ≝
+λw1,w2:word24.
+ match plus_b8_d_dc (w24l w1) (w24l w2) with
+ [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
+ [ pair h c' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c';h;l〉 ]].
+
+(* operatore somma con data → c *)
+ndefinition plus_w24_d_c ≝
+λw1,w2:word24.
+ plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_d_c (w24l w1) (w24l w2))).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_w24 ≝ λw:word24.eq_ex x8 (and_ex x8 (b8h (w24x w))).
+
+(* operatore predecessore *)
+ndefinition pred_w24 ≝
+λw:word24.match eq_b8 (w24l w) (mk_byte8 x0 x0) with
+ [ true ⇒ match eq_b8 (w24h w) (mk_byte8 x0 x0) with
+ [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
+ | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
+ | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
+
+(* operatore successore *)
+ndefinition succ_w24 ≝
+λw:word24.match eq_b8 (w24l w) (mk_byte8 xF xF) with
+ [ true ⇒ match eq_b8 (w24h w) (mk_byte8 xF xF) with
+ [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
+ | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
+ | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_w24 ≝
+λw:word24.match MSB_w24 w with
+ [ true ⇒ succ_w24 (not_w24 w)
+ | false ⇒ not_w24 (pred_w24 w) ].
+
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_w24 ≝
+λx,inf,sup:word24.
+ match le_w24 inf sup with
+ [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_w24 inf x) (le_w24 x sup).
+
+(* iteratore sulle word *)
+ndefinition forall_w24 ≝
+ λP.
+ forall_b8 (λbx.
+ forall_b8 (λbh.
+ forall_b8 (λbl.
+ P (mk_word24 bx bh bl )))).
projects / helm.git / blobdiff