Add faster arithmetic unfolding

3 files changed, 142 insertions, 0 deletions

diff --git a/src/Arithmetic/Saturated/CoreUnfolder.v b/src/Arithmetic/Saturated/CoreUnfolder.v
new file mode 100644
index 000000000..243f8ea2b
--- /dev/null
+++ b/src/Arithmetic/Saturated/CoreUnfolder.v
@@ -0,0 +1,81 @@
+Require Import Crypto.Arithmetic.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.Core.
+
+Module Columns.
+  (**
+<<
+#!/bin/bash
+for i in eval eval_from compact_digit_cps compact_digit compact_step_cps compact_step compact_cps compact cons_to_nth_cps cons_to_nth nils from_associational_cps from_associational; do
+    echo "  Definition ${i}_sig := parameterize_sig (@Core.Columns.${i}).";
+    echo "  Definition ${i} := parameterize_from_sig ${i}_sig.";
+    echo "  Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "  Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
+done
+echo "End Columns."
+>> *)
+  Definition eval_sig := parameterize_sig (@Core.Columns.eval).
+  Definition eval := parameterize_from_sig eval_sig.
+  Definition eval_eq := parameterize_eq eval eval_sig.
+  Hint Rewrite <- eval_eq : pattern_runtime.
+
+  Definition eval_from_sig := parameterize_sig (@Core.Columns.eval_from).
+  Definition eval_from := parameterize_from_sig eval_from_sig.
+  Definition eval_from_eq := parameterize_eq eval_from eval_from_sig.
+  Hint Rewrite <- eval_from_eq : pattern_runtime.
+
+  Definition compact_digit_cps_sig := parameterize_sig (@Core.Columns.compact_digit_cps).
+  Definition compact_digit_cps := parameterize_from_sig compact_digit_cps_sig.
+  Definition compact_digit_cps_eq := parameterize_eq compact_digit_cps compact_digit_cps_sig.
+  Hint Rewrite <- compact_digit_cps_eq : pattern_runtime.
+
+  Definition compact_digit_sig := parameterize_sig (@Core.Columns.compact_digit).
+  Definition compact_digit := parameterize_from_sig compact_digit_sig.
+  Definition compact_digit_eq := parameterize_eq compact_digit compact_digit_sig.
+  Hint Rewrite <- compact_digit_eq : pattern_runtime.
+
+  Definition compact_step_cps_sig := parameterize_sig (@Core.Columns.compact_step_cps).
+  Definition compact_step_cps := parameterize_from_sig compact_step_cps_sig.
+  Definition compact_step_cps_eq := parameterize_eq compact_step_cps compact_step_cps_sig.
+  Hint Rewrite <- compact_step_cps_eq : pattern_runtime.
+
+  Definition compact_step_sig := parameterize_sig (@Core.Columns.compact_step).
+  Definition compact_step := parameterize_from_sig compact_step_sig.
+  Definition compact_step_eq := parameterize_eq compact_step compact_step_sig.
+  Hint Rewrite <- compact_step_eq : pattern_runtime.
+
+  Definition compact_cps_sig := parameterize_sig (@Core.Columns.compact_cps).
+  Definition compact_cps := parameterize_from_sig compact_cps_sig.
+  Definition compact_cps_eq := parameterize_eq compact_cps compact_cps_sig.
+  Hint Rewrite <- compact_cps_eq : pattern_runtime.
+
+  Definition compact_sig := parameterize_sig (@Core.Columns.compact).
+  Definition compact := parameterize_from_sig compact_sig.
+  Definition compact_eq := parameterize_eq compact compact_sig.
+  Hint Rewrite <- compact_eq : pattern_runtime.
+
+  Definition cons_to_nth_cps_sig := parameterize_sig (@Core.Columns.cons_to_nth_cps).
+  Definition cons_to_nth_cps := parameterize_from_sig cons_to_nth_cps_sig.
+  Definition cons_to_nth_cps_eq := parameterize_eq cons_to_nth_cps cons_to_nth_cps_sig.
+  Hint Rewrite <- cons_to_nth_cps_eq : pattern_runtime.
+
+  Definition cons_to_nth_sig := parameterize_sig (@Core.Columns.cons_to_nth).
+  Definition cons_to_nth := parameterize_from_sig cons_to_nth_sig.
+  Definition cons_to_nth_eq := parameterize_eq cons_to_nth cons_to_nth_sig.
+  Hint Rewrite <- cons_to_nth_eq : pattern_runtime.
+
+  Definition nils_sig := parameterize_sig (@Core.Columns.nils).
+  Definition nils := parameterize_from_sig nils_sig.
+  Definition nils_eq := parameterize_eq nils nils_sig.
+  Hint Rewrite <- nils_eq : pattern_runtime.
+
+  Definition from_associational_cps_sig := parameterize_sig (@Core.Columns.from_associational_cps).
+  Definition from_associational_cps := parameterize_from_sig from_associational_cps_sig.
+  Definition from_associational_cps_eq := parameterize_eq from_associational_cps from_associational_cps_sig.
+  Hint Rewrite <- from_associational_cps_eq : pattern_runtime.
+
+  Definition from_associational_sig := parameterize_sig (@Core.Columns.from_associational).
+  Definition from_associational := parameterize_from_sig from_associational_sig.
+  Definition from_associational_eq := parameterize_eq from_associational from_associational_sig.
+  Hint Rewrite <- from_associational_eq : pattern_runtime.
+
+End Columns.
diff --git a/src/Arithmetic/Saturated/FreezeUnfolder.v b/src/Arithmetic/Saturated/FreezeUnfolder.v
new file mode 100644
index 000000000..9545e23ed
--- /dev/null
+++ b/src/Arithmetic/Saturated/FreezeUnfolder.v
@@ -0,0 +1,24 @@
+Require Import Crypto.Arithmetic.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.WrappersUnfolder.
+Require Import Crypto.Arithmetic.Saturated.Freeze.
+
+(**
+<<
+#!/bin/bash
+for i in freeze freeze_cps; do
+    echo "Definition ${i}_sig := parameterize_sig (@Freeze.${i}).";
+    echo "Definition ${i} := parameterize_from_sig ${i}_sig.";
+    echo "Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
+done
+>> *)
+Definition freeze_cps_sig := parameterize_sig (@Freeze.freeze_cps).
+Definition freeze_cps := parameterize_from_sig freeze_cps_sig.
+Definition freeze_cps_eq := parameterize_eq freeze_cps freeze_cps_sig.
+Hint Rewrite <- freeze_cps_eq : pattern_runtime.
+
+Definition freeze_sig := parameterize_sig (@Freeze.freeze).
+Definition freeze := parameterize_from_sig freeze_sig.
+Definition freeze_eq := parameterize_eq freeze freeze_sig.
+Hint Rewrite <- freeze_eq : pattern_runtime.
diff --git a/src/Arithmetic/Saturated/WrappersUnfolder.v b/src/Arithmetic/Saturated/WrappersUnfolder.v
new file mode 100644
index 000000000..20df67b58
--- /dev/null
+++ b/src/Arithmetic/Saturated/WrappersUnfolder.v
@@ -0,0 +1,37 @@
+Require Import Crypto.Arithmetic.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.Wrappers.
+
+Module Columns.
+  (**
+<<
+#!/bin/bash
+for i in add_cps unbalanced_sub_cps mul_cps conditional_add_cps; do
+    echo "  Definition ${i}_sig := parameterize_sig (@Wrappers.Columns.${i}).";
+    echo "  Definition ${i} := parameterize_from_sig ${i}_sig.";
+    echo "  Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "  Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
+done
+echo "End Columns."
+>> *)
+  Definition add_cps_sig := parameterize_sig (@Wrappers.Columns.add_cps).
+  Definition add_cps := parameterize_from_sig add_cps_sig.
+  Definition add_cps_eq := parameterize_eq add_cps add_cps_sig.
+  Hint Rewrite <- add_cps_eq : pattern_runtime.
+
+  Definition unbalanced_sub_cps_sig := parameterize_sig (@Wrappers.Columns.unbalanced_sub_cps).
+  Definition unbalanced_sub_cps := parameterize_from_sig unbalanced_sub_cps_sig.
+  Definition unbalanced_sub_cps_eq := parameterize_eq unbalanced_sub_cps unbalanced_sub_cps_sig.
+  Hint Rewrite <- unbalanced_sub_cps_eq : pattern_runtime.
+
+  Definition mul_cps_sig := parameterize_sig (@Wrappers.Columns.mul_cps).
+  Definition mul_cps := parameterize_from_sig mul_cps_sig.
+  Definition mul_cps_eq := parameterize_eq mul_cps mul_cps_sig.
+  Hint Rewrite <- mul_cps_eq : pattern_runtime.
+
+  Definition conditional_add_cps_sig := parameterize_sig (@Wrappers.Columns.conditional_add_cps).
+  Definition conditional_add_cps := parameterize_from_sig conditional_add_cps_sig.
+  Definition conditional_add_cps_eq := parameterize_eq conditional_add_cps conditional_add_cps_sig.
+  Hint Rewrite <- conditional_add_cps_eq : pattern_runtime.
+
+End Columns.