From 6e5ea07197f737e3e77c50d4e0a68f9495c4a5a8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 3 Jan 2017 13:50:10 -0500 Subject: Add ZToWord,wordToZ --- src/Util/FixedWordSizes.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/Util/FixedWordSizes.v') diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v index b49e67c9a..df5d5240d 100644 --- a/src/Util/FixedWordSizes.v +++ b/src/Util/FixedWordSizes.v @@ -1,3 +1,4 @@ +Require Import Coq.ZArith.ZArith. Require Import Coq.NArith.BinNat. Require Import Coq.Arith.Arith. Require Import Bedrock.Word. @@ -19,6 +20,8 @@ Definition word_case {T : nat -> Type} (logsz : nat) | logsz' => default _ end. +Definition ZToWord32 (v : Z) : word32 := NToWord _ (Z.to_N v). +Definition word32ToZ (v : word32) : Z := Z.of_N (wordToN v). Definition wadd32 : word32 -> word32 -> word32 := @wplus _. Definition wsub32 : word32 -> word32 -> word32 := @wminus _. Definition wmul32 : word32 -> word32 -> word32 := @wmult _. @@ -27,6 +30,8 @@ Definition wshr32 : word32 -> word32 -> word32 := @wordBin N.shiftr _. Definition wland32 : word32 -> word32 -> word32 := @wand _. Definition wlor32 : word32 -> word32 -> word32 := @wor _. +Definition ZToWord64 (v : Z) : word64 := NToWord _ (Z.to_N v). +Definition word64ToZ (v : word64) : Z := Z.of_N (wordToN v). Definition wadd64 : word64 -> word64 -> word64 := @wplus _. Definition wsub64 : word64 -> word64 -> word64 := @wminus _. Definition wmul64 : word64 -> word64 -> word64 := @wmult _. @@ -35,6 +40,8 @@ Definition wshr64 : word64 -> word64 -> word64 := @wordBin N.shiftr _. Definition wland64 : word64 -> word64 -> word64 := @wand _. Definition wlor64 : word64 -> word64 -> word64 := @wor _. +Definition ZToWord128 (v : Z) : word128 := NToWord _ (Z.to_N v). +Definition word128ToZ (v : word128) : Z := Z.of_N (wordToN v). Definition wadd128 : word128 -> word128 -> word128 := @wplus _. Definition wsub128 : word128 -> word128 -> word128 := @wminus _. Definition wmul128 : word128 -> word128 -> word128 := @wmult _. @@ -43,6 +50,12 @@ Definition wshr128 : word128 -> word128 -> word128 := @wordBin N.shiftr _. Definition wland128 : word128 -> word128 -> word128 := @wand _. Definition wlor128 : word128 -> word128 -> word128 := @wor _. +Definition ZToWord {logsz} + := word_case (T:=fun sz => Z -> word sz) + logsz ZToWord32 ZToWord64 ZToWord128 (fun _ v => NToWord _ (Z.to_N v)). +Definition wordToZ {logsz} + := word_case (T:=fun sz => word sz -> Z) + logsz word32ToZ word64ToZ word128ToZ (fun _ v => Z.of_N (wordToN v)). Definition wadd {logsz} := word_case (T:=fun sz => word sz -> word sz -> word sz) logsz wadd32 wadd64 wadd128 (fun _ => @wplus _). -- cgit v1.2.3