From d20b2cbc862fb35b5e059cbfafaaa9360fb6afce Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Fri, 26 Apr 2019 16:33:54 -0400 Subject: Remove BoundedWord Remove Util/BoundedWord.v and its reverse dependencies Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no longer in use. --- src/Util/FixedWordSizes.v | 122 ---------------------------------------------- 1 file changed, 122 deletions(-) delete mode 100644 src/Util/FixedWordSizes.v (limited to 'src/Util/FixedWordSizes.v') diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v deleted file mode 100644 index 10a7d78ff..000000000 --- a/src/Util/FixedWordSizes.v +++ /dev/null @@ -1,122 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.NArith.BinNat. -Require Import Coq.Arith.Arith. -Require Import bbv.WordScope. - -Definition word32 := word 32. (* 2^5 *) -Definition word64 := word 64. (* 2^6 *) -Definition word128 := word 128. (* 2^7 *) - -Definition word_case {T : nat -> Type} (logsz : nat) - (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 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 ZToSignedWord_gen {sz} (v : Z) : word sz := Word.ZToWord _ v. -Definition signedWordToZ_gen {sz} (v : word sz) : Z := Word.wordToZ v. - -Definition ZToWord32 : Z -> word32 := @ZToWord_gen _. -Definition word32ToZ : word32 -> Z := @wordToZ_gen _. -Definition ZToSignedWord32 : Z -> word32 := @ZToSignedWord_gen _. -Definition signedWord32ToZ : word32 -> Z := @signedWordToZ_gen _. -Definition wadd32 : word32 -> word32 -> word32 := @wplus _. -Definition wsub32 : word32 -> word32 -> word32 := @wminus _. -Definition wmul32 : word32 -> word32 -> word32 := @wmult _. -Definition wshl32 : word32 -> word32 -> word32 := @wordBin N.shiftl _. -Definition wshr32 : word32 -> word32 -> word32 := @wordBin N.shiftr _. -Definition wland32 : word32 -> word32 -> word32 := @wand _. -Definition wlor32 : word32 -> word32 -> word32 := @wor _. - -Definition ZToWord64 : Z -> word64 := @ZToWord_gen _. -Definition word64ToZ : word64 -> Z := @wordToZ_gen _. -Definition ZToSignedWord64 : Z -> word64 := @ZToSignedWord_gen _. -Definition signedWord64ToZ : word64 -> Z := @signedWordToZ_gen _. -Definition wadd64 : word64 -> word64 -> word64 := @wplus _. -Definition wsub64 : word64 -> word64 -> word64 := @wminus _. -Definition wmul64 : word64 -> word64 -> word64 := @wmult _. -Definition wshl64 : word64 -> word64 -> word64 := @wordBin N.shiftl _. -Definition wshr64 : word64 -> word64 -> word64 := @wordBin N.shiftr _. -Definition wland64 : word64 -> word64 -> word64 := @wand _. -Definition wlor64 : word64 -> word64 -> word64 := @wor _. - -Definition ZToWord128 : Z -> word128 := @ZToWord_gen _. -Definition word128ToZ : word128 -> Z := @wordToZ_gen _. -Definition ZToSignedWord128 : Z -> word128 := @ZToSignedWord_gen _. -Definition signedWord128ToZ : word128 -> Z := @signedWordToZ_gen _. -Definition wadd128 : word128 -> word128 -> word128 := @wplus _. -Definition wsub128 : word128 -> word128 -> word128 := @wminus _. -Definition wmul128 : word128 -> word128 -> word128 := @wmult _. -Definition wshl128 : word128 -> word128 -> word128 := @wordBin N.shiftl _. -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_dep (T:=fun _ word => Z -> word) - logsz ZToWord32 ZToWord64 ZToWord128 (fun _ => @ZToWord_gen _). -Definition wordToZ {logsz} - := word_case_dep (T:=fun _ word => word -> Z) - logsz word32ToZ word64ToZ word128ToZ (fun _ => @wordToZ_gen _). -Definition ZToSignedWord {logsz} - := word_case_dep (T:=fun _ word => Z -> word) - logsz ZToSignedWord32 ZToSignedWord64 ZToSignedWord128 (fun _ => @ZToSignedWord_gen _). -Definition signedWordToZ {logsz} - := word_case_dep (T:=fun _ word => word -> Z) - logsz signedWord32ToZ signedWord64ToZ signedWord128ToZ (fun _ => @signedWordToZ_gen _). -Definition wadd {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wadd32 wadd64 wadd128 (fun _ => @wplus _). -Definition wsub {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wsub32 wsub64 wsub128 (fun _ => @wminus _). -Definition wmul {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wmul32 wmul64 wmul128 (fun _ => @wmult _). -Definition wshl {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _). -Definition wshr {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _). -Definition wland {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wland32 wland64 wland128 (fun _ => @wand _). -Definition wlor {logsz} - := word_case_dep (T:=fun _ word => word -> word -> word) - logsz wlor32 wlor64 wlor128 (fun _ => @wor _). - -Create HintDb fixed_size_constants discriminated. -Hint Unfold word32 word64 word128 - wadd wadd32 wadd64 wadd128 - wsub wsub32 wsub64 wsub128 - wmul wmul32 wmul64 wmul128 - wshl wshl32 wshl64 wshl128 - wshr wshr32 wshr64 wshr128 - wland wland32 wland64 wland128 - wlor wlor32 wlor64 wlor128 : fixed_size_constants. -- cgit v1.2.3