From 871a247d3e37962d7c5fc34df32b4ef90597ea8d Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 3 Jan 2017 13:44:14 -0500
Subject: Add fixed word size definitions

---
 _CoqProject               |  1 +
 src/Util/FixedWordSizes.v | 66 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 src/Util/FixedWordSizes.v

diff --git a/_CoqProject b/_CoqProject
index b521cb557..f6d2f69f0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -361,6 +361,7 @@ src/Util/CaseUtil.v
 src/Util/Decidable.v
 src/Util/Equality.v
 src/Util/FixCoqMistakes.v
+src/Util/FixedWordSizes.v
 src/Util/GlobalSettings.v
 src/Util/HList.v
 src/Util/HProp.v
diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v
new file mode 100644
index 000000000..b49e67c9a
--- /dev/null
+++ b/src/Util/FixedWordSizes.v
@@ -0,0 +1,66 @@
+Require Import Coq.NArith.BinNat.
+Require Import Coq.Arith.Arith.
+Require Import Bedrock.Word.
+
+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 32)
+           (case64 : T 64)
+           (case128 : T 128)
+           (default : forall k, T (2^k))
+  : T (2^logsz)
+  := match logsz return T (2^logsz) with
+     | 5 => case32
+     | 6 => case64
+     | 7 => case128
+     | logsz' => default _
+     end.
+
+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 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 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 wadd {logsz}
+  := word_case (T:=fun sz => word sz -> word sz -> word sz)
+               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 _).
+Definition wmul {logsz}
+  := word_case (T:=fun sz => word sz -> word sz -> word sz)
+               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 _).
+Definition wshr {logsz}
+  := word_case (T:=fun sz => word sz -> word sz -> word sz)
+               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 _).
+Definition wlor {logsz}
+  := word_case (T:=fun sz => word sz -> word sz -> word sz)
+               logsz wlor32 wlor64 wlor128 (fun _ => @wor _).
-- 
cgit v1.2.3