for @{ 'mk_word24 $x $y $z }.
interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
+(* iteratore sulle word *)
+ndefinition forall_w24 ≝
+ λP.
+ forall_b8 (λbx.
+ forall_b8 (λbh.
+ forall_b8 (λbl.
+ P (mk_word24 bx bh bl )))).
+
(* operatore = *)
ndefinition eq_w24 ≝
λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
(xor_b8 (w24h w1) (w24h w2))
(xor_b8 (w24l w1) (w24l w2)).
+(* operatore Most Significant Bit *)
+ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
+ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
+ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
+
+(* operatore Least Significant Bit *)
+ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
+ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
+ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
+
(* 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''' ]]].
+λc:bool.λw:word24.match rcr_b8 c (w24x w) with
+ [ pair c' wx' ⇒ match rcr_b8 c' (w24h w) with
+ [ pair c'' wh' ⇒ match rcr_b8 c'' (w24l w) with
+ [ pair c''' wl' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
(* 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''' ]]].
+ndefinition shr_w24 ≝ rcr_w24 false.
(* 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' ].
+λw.match shr_w24 w with
+ [ pair c w' ⇒ match c with
+ [ true ⇒ setMSB_w24 w' | false ⇒ w' ]].
(* 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''' ]]].
+λc:bool.λw:word24.match rcl_b8 c (w24l w) with
+ [ pair c' wl' ⇒ match rcl_b8 c' (w24h w) with
+ [ pair c'' wh' ⇒ match rcl_b8 c'' (w24x w) with
+ [ pair c''' wx' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
(* 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''' ]]].
+ndefinition shl_w24 ≝ rcl_w24 false.
(* 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' ].
+λw.match shl_w24 w with
+ [ pair c w' ⇒ match c with
+ [ true ⇒ setLSB_w24 w' | false ⇒ w' ]].
(* operatore not/complemento a 1 *)
ndefinition not_w24 ≝
(* 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''' ]]].
+λc:bool.λw1,w2:word24.
+ match plus_b8_dc_dc c (w24l w1) (w24l w2) with
+ [ pair c' l ⇒ match plus_b8_dc_dc c' (w24h w1) (w24h w2) with
+ [ pair c'' h ⇒ match plus_b8_dc_dc c'' (w24x w1) (w24x w2) with
+ [ pair c''' x ⇒ pair … c''' 〈x;h;l〉 ]]].
(* 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〉 ]].
+ndefinition plus_w24_dc_d ≝ λc,w1,w2.snd … (plus_w24_dc_dc c w1 w2).
(* 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)).
+ndefinition plus_w24_dc_c ≝ λc,w1,w2.fst … (plus_w24_dc_dc c w1 w2).
(* 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'' ]]].
+ndefinition plus_w24_d_dc ≝ plus_w24_dc_dc false.
(* 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〉 ]].
+ndefinition plus_w24_d_d ≝ λw1,w2.snd … (plus_w24_d_dc w1 w2).
(* 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))).
+ndefinition plus_w24_d_c ≝ λw1,w2.fst … (plus_w24_d_dc w1 w2).
(* 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
+λw:word24.match eq_b8 (w24l w) 〈x0,x0〉 with
+ [ true ⇒ match eq_b8 (w24h w) 〈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
+λw:word24.match eq_b8 (w24l w) 〈xF,xF〉 with
+ [ true ⇒ match eq_b8 (w24h w) 〈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
+λw:word24.match getMSB_w24 w with
[ true ⇒ succ_w24 (not_w24 w)
| false ⇒ not_w24 (pred_w24 w) ].
+(* operatore abs *)
+ndefinition abs_w24 ≝
+λw:word24.match getMSB_w24 w with
+ [ true ⇒ compl_w24 w | false ⇒ 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