From efb855b7ca6c9a917fd0c5993f29d3856185ce5f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 31 Oct 2017 20:21:28 -0400
Subject: Add Bedrock.Word.ZToWord

---
 Bedrock/Word.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'Bedrock')

diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index 2726a03c3..016903a7f 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -1001,7 +1001,7 @@ Ltac word_contra1 := match goal with
 Open Scope word_scope.
 
 (** * Signed Logic **)
-Fixpoint wordToZ sz (w : word sz) : Z :=
+Definition wordToZ sz (w : word sz) : Z :=
   if wmsb w true then
     (** Negative **)
     match wordToN (wneg w) with
@@ -1014,6 +1014,13 @@ Fixpoint wordToZ sz (w : word sz) : Z :=
       | N0 => 0%Z
       | Npos x => Zpos x
     end.
+Definition ZToWord sz (v : Z) : word sz :=
+  if (v <? 0)%Z then
+    (** Negative **)
+    wneg (NToWord (Z.to_N (-v)))
+  else
+    (** Positive **)
+    wordToN (Z.to_N v).
 
 (** * Comparison Predicates and Deciders **)
 Definition wlt sz (l r : word sz) : Prop :=
-- 
cgit v1.2.3