1 files changed, 39 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/InvertHighLow.v b/src/PushButtonSynthesis/InvertHighLow.v
new file mode 100644
index 000000000..f7deb4145
--- /dev/null
+++ b/src/PushButtonSynthesis/InvertHighLow.v
@@ -0,0 +1,39 @@
+(** * Push-Button Synthesis fancy argument definitions *)
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Section with_wordmax.
+  Context (log2wordmax : Z) (consts : list Z).
+  Let wordmax := 2 ^ log2wordmax.
+  Let half_bits := log2wordmax / 2.
+  Let wordmax_half_bits := 2 ^ half_bits.
+
+  Inductive kind_of_constant := upper_half (c : BinInt.Z) | lower_half (c : BinInt.Z).
+
+  Definition constant_to_scalar_single (const x : BinInt.Z) : option kind_of_constant :=
+    if x =? (BinInt.Z.shiftr const half_bits)
+    then Some (upper_half const)
+    else if x =? (BinInt.Z.land const (wordmax_half_bits - 1))
+         then Some (lower_half const)
+         else None.
+
+  Definition constant_to_scalar (x : BinInt.Z)
+    : option kind_of_constant :=
+    fold_right (fun c res => match res with
+                             | Some s => Some s
+                             | None => constant_to_scalar_single c x
+                             end) None consts.
+
+  Definition invert_low (v : BinInt.Z) : option BinInt.Z
+    := match constant_to_scalar v with
+       | Some (lower_half v) => Some v
+       | _ => None
+       end.
+
+  Definition invert_high (v : BinInt.Z) : option BinInt.Z
+    := match constant_to_scalar v with
+       | Some (upper_half v) => Some v
+       | _ => None
+       end.
+End with_wordmax.