1 files changed, 49 insertions, 0 deletions
diff --git a/src/RewriterFull.v b/src/RewriterFull.v
new file mode 100644
index 000000000..772732442
--- /dev/null
+++ b/src/RewriterFull.v
@@ -0,0 +1,49 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.RewriterRules.
+Require Import Crypto.Rewriter.
+Local Open Scope Z_scope.
+
+Import Compilers.RewriteRules.GoalType.
+Import Compilers.RewriteRules.Tactic.
+
+Module Compilers.
+  Module RewriteRules.
+    Definition RewriterNBE : RewriterT.
+    Proof. make_Rewriter true nbe_rewrite_rulesT. Defined.
+
+    Definition RewriterArith (max_const_val : Z) : RewriterT.
+    Proof. make_Rewriter false (arith_rewrite_rulesT max_const_val). Defined.
+
+    Definition RewriterArithWithCasts : RewriterT.
+    Proof. make_Rewriter false arith_with_casts_rewrite_rulesT. Defined.
+
+    Definition RewriterStripLiteralCasts : RewriterT.
+    Proof. make_Rewriter false strip_literal_casts_rewrite_rulesT. Defined.
+
+    Definition RewriterToFancy
+               (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
+      : RewriterT.
+    Proof. make_Rewriter false fancy_rewrite_rulesT. Defined.
+
+    Definition RewriterToFancyWithCasts
+               (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z)
+               (value_range flag_range : zrange)
+      : RewriterT.
+    Proof. make_Rewriter false (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Defined.
+
+    Definition RewriteNBE {t} := Eval hnf in @Rewrite RewriterNBE t.
+    Definition RewriteArith max_const_val {t} := Eval hnf in @Rewrite (RewriterArith max_const_val) t.
+    Definition RewriteArithWithCasts {t} := Eval hnf in @Rewrite RewriterArithWithCasts t.
+    Definition RewriteStripLiteralCasts {t} := Eval hnf in @Rewrite RewriterStripLiteralCasts t.
+    Definition RewriteToFancy invert_low invert_high {t}
+      := Eval hnf in @Rewrite (RewriterToFancy invert_low invert_high) t.
+    Definition RewriteToFancyWithCasts invert_low invert_high value_range flag_range {t}
+      := Eval hnf in @Rewrite (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) t.
+  End RewriteRules.
+
+  Import Language.Compilers.defaults.
+
+  Definition PartialEvaluate {t} (e : Expr t) : Expr t
+    := RewriteRules.RewriteNBE e.
+End Compilers.