freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index 4c6d8101b2fbc978375fcaff46f4ff314a96549e..7be3a53c5fd90a6b58982bbe51e886dc7585f569 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -28,6 +28,7 @@ include "num/word16.ma".
 
 ndefinition word32 ≝ comp_num word16.
 ndefinition mk_word32 ≝ λw1,w2.mk_comp_num word16 w1 w2.
+ndefinition ext_word32 ≝ λw2.mk_comp_num word16 〈〈x0,x0〉:〈x0,x0〉〉 w2.
 
 (* \langle \rangle *)
 notation "〈x.y〉" non associative with precedence 80
@@ -68,6 +69,22 @@ ndefinition setMSB_w32 ≝ setOPH_cn ? setMSB_w16.
 ndefinition getLSB_w32 ≝ getOPL_cn ? getLSB_w16.
 ndefinition setLSB_w32 ≝ setOPL_cn ? setLSB_w16.
 
+(* operatore estensione unsigned *)
+ndefinition extu_w32 ≝ λw2.〈〈〈x0,x0〉:〈x0,x0〉〉.w2〉.
+ndefinition extu2_w32 ≝ λb2.〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:b2〉〉.
+ndefinition extu3_w32 ≝ λe2.〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,e2〉〉〉.
+
+(* operatore estensione signed *)
+ndefinition exts_w32 ≝
+λw2.〈(match getMSB_w16 w2 with
+      [ true ⇒ 〈〈xF,xF〉:〈xF,xF〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,x0〉〉 ]).w2〉.
+ndefinition exts2_w32 ≝
+λb2.(match getMSB_b8 b2 with
+      [ true ⇒ 〈〈〈xF,xF〉:〈xF,xF〉〉.〈〈xF,xF〉:b2〉〉 | false ⇒ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:b2〉〉 ]).
+ndefinition exts3_w32 ≝
+λe2.(match getMSB_ex e2 with
+      [ true ⇒ 〈〈〈xF,xF〉:〈xF,xF〉〉.〈〈xF,xF〉:〈xF,e2〉〉〉 | false ⇒ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,e2〉〉〉 ]).
+
 (* operatore rotazione destra con carry *)
 ndefinition rcr_w32 ≝ opcr_cn ? rcr_w16.