From c07e8d7dd27750737d80c35d0eec124ae48196d9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 3 Jan 2017 14:47:45 -0500 Subject: Better word operations --- src/Util/FixedWordSizes.v | 79 +++++++++++++++++++++++++++++------------------ 1 file changed, 49 insertions(+), 30 deletions(-) (limited to 'src/Util/FixedWordSizes.v') diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v index df5d5240d..8e2484ff6 100644 --- a/src/Util/FixedWordSizes.v +++ b/src/Util/FixedWordSizes.v @@ -8,20 +8,39 @@ Definition word64 := word 64. (* 2^6 *) Definition word128 := word 128. (* 2^7 *) Definition word_case {T : nat -> Type} (logsz : nat) - (case32 : T 32) - (case64 : T 64) - (case128 : T 128) - (default : forall k, T (2^k)) - : T (2^logsz) - := match logsz return T (2^logsz) with + (case32 : T 5) + (case64 : T 6) + (case128 : T 7) + (default : forall k, T k) + : T logsz + := match logsz return T logsz with | 5 => case32 | 6 => case64 | 7 => case128 | logsz' => default _ end. -Definition ZToWord32 (v : Z) : word32 := NToWord _ (Z.to_N v). -Definition word32ToZ (v : word32) : Z := Z.of_N (wordToN v). +Definition wordT logsz := word_case (T:=fun _ => Set) logsz word32 word64 word128 (fun logsz => word (2^logsz)). + +Definition word_case_dep {T : nat -> Set -> Type} (logsz : nat) + (case32 : T 5 word32) + (case64 : T 6 word64) + (case128 : T 7 word128) + (default : forall k, T k (word (2^k))) + : T logsz (wordT logsz) + := match logsz return T logsz (wordT logsz) with + | 5 => case32 + | 6 => case64 + | 7 => case128 + | logsz' => default _ + end. + +Definition ZToWord_gen {sz} (v : Z) : word sz := NToWord _ (Z.to_N v). +Definition wordToZ_gen {sz} (v : word sz) : Z := Z.of_N (wordToN v). + + +Definition ZToWord32 : Z -> word32 := @ZToWord_gen _. +Definition word32ToZ : word32 -> Z := @wordToZ_gen _. Definition wadd32 : word32 -> word32 -> word32 := @wplus _. Definition wsub32 : word32 -> word32 -> word32 := @wminus _. Definition wmul32 : word32 -> word32 -> word32 := @wmult _. @@ -30,8 +49,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 ZToWord64 : Z -> word64 := @ZToWord_gen _. +Definition word64ToZ : word64 -> Z := @wordToZ_gen _. Definition wadd64 : word64 -> word64 -> word64 := @wplus _. Definition wsub64 : word64 -> word64 -> word64 := @wminus _. Definition wmul64 : word64 -> word64 -> word64 := @wmult _. @@ -40,8 +59,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 ZToWord128 : Z -> word128 := @ZToWord_gen _. +Definition word128ToZ : word128 -> Z := @wordToZ_gen _. Definition wadd128 : word128 -> word128 -> word128 := @wplus _. Definition wsub128 : word128 -> word128 -> word128 := @wminus _. Definition wmul128 : word128 -> word128 -> word128 := @wmult _. @@ -51,29 +70,29 @@ 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)). + := word_case_dep (T:=fun _ word => Z -> word) + logsz ZToWord32 ZToWord64 ZToWord128 (fun _ => @ZToWord_gen _). Definition wordToZ {logsz} - := word_case (T:=fun sz => word sz -> Z) - logsz word32ToZ word64ToZ word128ToZ (fun _ v => Z.of_N (wordToN v)). + := word_case_dep (T:=fun _ word => word -> Z) + logsz word32ToZ word64ToZ word128ToZ (fun _ => @wordToZ_gen _). Definition wadd {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wadd32 wadd64 wadd128 (fun _ => @wplus _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wadd32 wadd64 wadd128 (fun _ => @wplus _). Definition wsub {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wsub32 wsub64 wsub128 (fun _ => @wminus _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wsub32 wsub64 wsub128 (fun _ => @wminus _). Definition wmul {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wmul32 wmul64 wmul128 (fun _ => @wmult _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wmul32 wmul64 wmul128 (fun _ => @wmult _). Definition wshl {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _). Definition wshr {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _). Definition wland {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wland32 wland64 wland128 (fun _ => @wand _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wland32 wland64 wland128 (fun _ => @wand _). Definition wlor {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wlor32 wlor64 wlor128 (fun _ => @wor _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wlor32 wlor64 wlor128 (fun _ => @wor _). -- cgit v1.2.3