Add a file to parse taps with Coq notations

3 files changed, 42 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index ed4cabd28..9e0dc9859 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6464,6 +6464,7 @@ src/Util/NatUtil.v
 src/Util/Notations.v
 src/Util/NumTheoryUtil.v
 src/Util/Option.v
+src/Util/ParseTaps.v
 src/Util/PartiallyReifiedProp.v
 src/Util/PointedProp.v
 src/Util/Pos.v
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index af1fcb6be..3510e0a0b 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -30,6 +30,7 @@ Reserved Infix ".+" (at level 50).
 Reserved Infix ".*" (at level 50).
 Reserved Notation "x ^ 2" (at level 30, format "x ^ 2").
 Reserved Notation "x ^ 3" (at level 30, format "x ^ 3").
+Reserved Notation "2 ^ e" (at level 30, format "2 ^ e", only printing).
 Reserved Infix "mod" (at level 40, no associativity).
 Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50).
 Reserved Notation "@ 'is_eq_dec' T R" (at level 10, T at level 8, R at level 8).
diff --git a/src/Util/ParseTaps.v b/src/Util/ParseTaps.v
new file mode 100644
index 000000000..35bc380fd
--- /dev/null
+++ b/src/Util/ParseTaps.v
@@ -0,0 +1,40 @@
+Require Import Coq.Lists.List.
+Require Import Coq.ZArith.BinInt.
+Require Import Crypto.Util.Notations.
+Import ListNotations.
+
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+
+Definition tap := (Z * Z)%type.
+Definition taps := list tap.
+Delimit Scope tap_scope with tap.
+Delimit Scope taps_scope with taps.
+Bind Scope tap_scope with tap.
+Bind Scope taps_scope with taps.
+
+Coercion Z_to_tap (v : Z) : tap := (v, 0).
+Coercion tap_to_taps (v : tap) : taps := [v].
+Definition make_tap (b e : Z) : tap := (b, e).
+
+Definition scmul_tap (c : Z) (t : tap) : tap
+  := let '(c', e) := t in (c * c', e).
+Definition neg_tap (t : tap) : tap
+  := let '(c, e) := t in (-c, e).
+Definition add_taps : taps -> taps -> taps := @List.app _.
+
+Notation "b ^ e" := (make_tap (Z.log2 b) e) : tap_scope.
+Notation "2 ^ e" := [(1, e%Z)] (only printing) : tap_scope.
+Notation "x * y" := (scmul_tap x y) : tap_scope.
+Notation "- a" := (neg_tap a) : tap_scope.
+
+Notation "b ^ e" := (b^e)%tap (only printing) : taps_scope.
+Notation "x * y" := (x * y)%tap (only printing) : taps_scope.
+Notation "- a" := (-a)%tap (only printing) : taps_scope.
+Notation "b ^ e" := (tap_to_taps (b ^ e)) : taps_scope.
+Notation "x * y" := (tap_to_taps (x * y)) : taps_scope.
+Notation "- a" := (tap_to_taps (-a)) : taps_scope.
+
+Notation "a + b" := (add_taps a b) : taps_scope.
+Notation "a - b" := (add_taps a (neg_tap (Z_to_tap (Zpos b)))) : taps_scope.
+Notation "a - b" := (add_taps a (- b)) : taps_scope.