X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword16.ma;h=80281eeea6d64064dbfa4b208a4834adbd32b3c2;hb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;hp=df45e02a725aa93aaef11732dbb00114383cd45b;hpb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index df45e02a7..80281eeea 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -28,6 +28,8 @@ include "num/byte8.ma".
 
 ndefinition word16 ≝ comp_num byte8.
 ndefinition mk_word16 ≝ λb1,b2.mk_comp_num byte8 b1 b2.
+ndefinition ext_word16 ≝ λb2.mk_comp_num byte8 〈x0,x0〉 b2.
+ndefinition ext2_word16 ≝ λe2.mk_comp_num byte8 〈x0,x0〉 〈x0,e2〉.
 
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
@@ -63,10 +65,24 @@ ndefinition xor_w16 ≝ fop2_cn ? xor_b8.
 (* operatore Most Significant Bit *)
 ndefinition getMSB_w16 ≝ getOPH_cn ? getMSB_b8.
 ndefinition setMSB_w16 ≝ setOPH_cn ? setMSB_b8.
+ndefinition clrMSB_w16 ≝ setOPH_cn ? clrMSB_b8.
 
 (* operatore Least Significant Bit *)
 ndefinition getLSB_w16 ≝ getOPL_cn ? getLSB_b8.
 ndefinition setLSB_w16 ≝ setOPL_cn ? setLSB_b8.
+ndefinition clrLSB_w16 ≝ setOPL_cn ? clrLSB_b8.
+
+(* operatore estensione unsigned *)
+ndefinition extu_w16 ≝ λb2.〈〈x0,x0〉:b2〉.
+ndefinition extu2_w16 ≝ λe2.〈〈x0,x0〉:〈x0,e2〉〉.
+
+(* operatore estensione signed *)
+ndefinition exts_w16 ≝
+λb2.〈(match getMSB_b8 b2 with
+      [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]):b2〉.
+ndefinition exts2_w16 ≝
+λe2.(match getMSB_ex e2 with
+      [ true ⇒ 〈〈xF,xF〉:〈xF,e2〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,e2〉〉 ]).
 
 (* operatore rotazione destra con carry *)
 ndefinition rcr_w16 ≝ opcr_cn ? rcr_b8.